From b3fb830a46f62838f9febe6dcda7d29542bb7424 Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 12 Jul 2016 16:52:43 -0400
Subject: [PATCH] add parameters

---
 turnstile/examples/rosette/bv.rkt | 15 +++++++++++++++
 1 file changed, 15 insertions(+)

diff --git a/turnstile/examples/rosette/bv.rkt b/turnstile/examples/rosette/bv.rkt
index 9af1920..e08804d 100644
--- a/turnstile/examples/rosette/bv.rkt
+++ b/turnstile/examples/rosette/bv.rkt
@@ -28,6 +28,11 @@
           (define-syntax- x (make-rename-transformer (⊢ y : ty.norm))) ...
           (ro:define-symbolic y ... pred-))]])
 
+;; ----------------------------------------------------------------------------
+;; Racket stuff
+
+(define-type-constructor Param #:arity = 1)
+
 (define-rosette-primop boolean? : (→ Bool Bool))
 (define-rosette-primop integer? : (→ Int Bool))
 (define-rosette-primop string? : (→ String Bool))
@@ -46,6 +51,16 @@
    --------
    [⊢ [[_ ≫ (ro:if e_tst- e1- e2-)] ⇒ : (⊔ τ1 τ2)]]])
 
+(define-typed-syntax make-parameter
+  [(_ e) ⇐ : (~Param τ_expected) ≫
+   [⊢ [[e ≫ e-] ⇐ : τ_expected]]
+   --------
+   [⊢ [[_ ≫ (ro:make-parameter e-)]]]]
+  [(_ e) ≫
+   [⊢ [[e ≫ e-] ⇒ : τ]]
+   --------
+   [⊢ [[_ ≫ (ro:make-parameter e-)] ⇒ : (Param τ)]]])
+
 ;; ----------------------------------------------------------------------------
 ;; BV stuff