www

commit b3fb830a46f62838f9febe6dcda7d29542bb7424
parent cef8660c750084e93250d31e08651d8d076d0fad
Author: Stephen Chang <stchang@ccs.neu.edu>
Date:   Tue, 12 Jul 2016 16:52:43 -0400

add parameters

Diffstat:
M
turnstile/examples/rosette/bv.rkt
 | 
15
+++++++++++++++

1 file changed, 15 insertions(+), 0 deletions(-)
diff --git 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