commit 10a143a16d6abb31c22915a1075afa694bea809a
parent 2a6167e4d0d2bc78c8378f96b1fe882e53c06b63
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Tue, 30 Aug 2016 16:58:15 -0400
add verify, evaluate; and debug, render in separate libs
Diffstat:
6 files changed, 150 insertions(+), 19 deletions(-)
diff --git a/macrotypes/stx-utils.rkt b/macrotypes/stx-utils.rkt
@@ -73,6 +73,8 @@
;; transfers properties and src loc from orig to new
(define (transfer-stx-props new orig #:ctx [ctx new])
(datum->syntax ctx (syntax-e new) orig orig))
+(define (replace-stx-loc old new)
+ (datum->syntax old (syntax-e old) new old))
;; set-stx-prop/preserved : Stx Any Any -> Stx
;; Returns a new syntax object with the prop property set to val. If preserved
diff --git a/turnstile/examples/rosette/lib/render.rkt b/turnstile/examples/rosette/lib/render.rkt
@@ -0,0 +1,16 @@
+#lang turnstile
+(require
+ (prefix-in t/ro: (only-in "../rosette2.rkt" CNat CSolution CPict))
+ (prefix-in ro: rosette/lib/render))
+
+(define-typed-syntax render
+ [(r s) ≫
+ [⊢ [s ≫ s- ⇐ : t/ro:CSolution]]
+ --------
+ [⊢ [_ ≫ (#,(syntax/loc #'r ro:render) s-) ⇒ : t/ro:CPict]]]
+ [(r s sz) ≫
+ [⊢ [s ≫ s- ⇐ : t/ro:CSolution]]
+ [⊢ [sz ≫ sz- ⇐ : t/ro:CNat]]
+ --------
+ [⊢ [_ ≫ (#,(syntax/loc #'r ro:render) s- sz-) ⇒ : t/ro:CPict]]])
+
diff --git a/turnstile/examples/rosette/query/debug.rkt b/turnstile/examples/rosette/query/debug.rkt
@@ -0,0 +1,30 @@
+#lang turnstile
+(require
+ (prefix-in t/ro: (only-in "../rosette2.rkt" λ ann begin C→ Nothing Bool CSolution))
+ (prefix-in ro: rosette/query/debug))
+
+(define-typed-syntax define/debug #:datum-literals (: -> →)
+ [(d x:id e) ≫
+ [⊢ [e ≫ e- ⇒ : τ]]
+ #:with y (generate-temporary #'x)
+ --------
+ [_ ≻ (begin-
+ (define-syntax- x (make-rename-transformer (⊢ y : τ)))
+ (ro:define/debug y e-))]]
+ [(d (f [x : ty] ... (~or → ->) ty_out) e ...+) ≫
+; [⊢ [e ≫ e- ⇒ : ty_e]]
+ #:with f- (generate-temporary #'f)
+ --------
+ [_ ≻ (begin-
+ (define-syntax- f (make-rename-transformer (⊢ f- : (t/ro:C→ ty ... ty_out))))
+ (ro:define/debug f-
+ (t/ro:λ ([x : ty] ...)
+ (t/ro:ann (t/ro:begin e ...) : ty_out))))]])
+
+(define-typed-syntax debug
+ [(d (solvable-pred ...+) e) ≫
+ [⊢ [solvable-pred ≫ solvable-pred- ⇐ : (t/ro:C→ t/ro:Nothing t/ro:Bool)]] ...
+ [⊢ [e ≫ e- ⇒ : τ]]
+ --------
+ [⊢ [_ ≫ (ro:debug (solvable-pred- ...) e-) ⇒ : t/ro:CSolution]]])
+
diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt
@@ -20,6 +20,14 @@ TODOs:
- STARTED 2016-08-26
- support internal definition contexts
- fix type of Vector and List to differentiate homogeneous/hetero
+- variable arity polymorphism
+- CSolution?
+- make libs have appropriate require paths
+ - eg typed/rosette/query/debug
+- make typed/rosette a separate pkg
+ - depends on macrotypes and rosette
+- create version of turnstile that does not provide #%module-begin
+ - eg rename existing turnstile to turnstile/lang?
2016-08-25 --------------------
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -6,7 +6,7 @@
(reuse define-named-type-alias #:from "../stlc+union.rkt")
(reuse void list #:from "../stlc+cons.rkt")
-(provide Any
+(provide Any Nothing
CU U
C→ → (for-syntax ~C→ C→?)
Ccase-> ; TODO: symbolic case-> not supported yet
@@ -246,13 +246,16 @@
(define-typed-syntax app #:export-as #%app
[(_ e_fn e_arg ...) ≫
[⊢ [e_fn ≫ e_fn- ⇒ : (~C→ ~! τ_in ... τ_out)]]
+ #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
#:fail-unless (stx-length=? #'[τ_in ...] #'[e_arg ...])
(num-args-fail-msg #'e_fn #'[τ_in ...] #'[e_arg ...])
[⊢ [e_arg ≫ e_arg- ⇐ : τ_in] ...]
--------
+ ;; TODO: use e_fn/progsrc- (currently causing "cannot use id tainted in macro trans" err)
[⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]]
[(_ e_fn e_arg ...) ≫
[⊢ [e_fn ≫ e_fn- ⇒ : (~Ccase-> ~! . (~and ty_fns ((~C→ . _) ...)))]]
+ #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
[⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
#:with τ_out
(for/first ([ty_f (stx->list #'ty_fns)]
@@ -282,25 +285,27 @@
(string-join (stx-map type->str τs_given) ", ")
(string-join (map ~s (stx-map syntax->datum expressions)) ", ")))])
--------
- [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : τ_out]]]
+ [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : τ_out]]]
[(_ e_fn e_arg ...) ≫
[⊢ [e_fn ≫ e_fn- ⇒ : (~CU* τ_f ...)]]
+ #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
[⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
#:with (f a ...) (generate-temporaries #'(e_fn e_arg ...))
[([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...)
⊢ [(app f a ...) ≫ _ ⇒ : τ_out]]
...
--------
- [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : (CU τ_out ...)]]]
+ [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (CU τ_out ...)]]]
[(_ e_fn e_arg ...) ≫
[⊢ [e_fn ≫ e_fn- ⇒ : (~U* τ_f ...)]]
+ #:with e_fn/progsrc- (replace-stx-loc #'e_fn- #'e_fn)
[⊢ [e_arg ≫ e_arg- ⇒ : τ_arg] ...]
#:with (f a ...) (generate-temporaries #'(e_fn e_arg ...))
[([f ≫ _ : τ_f] [a ≫ _ : τ_arg] ...)
⊢ [(app f a ...) ≫ _ ⇒ : τ_out]]
...
--------
- [⊢ [_ ≫ (ro:#%app e_fn- e_arg- ...) ⇒ : (U τ_out ...)]]])
+ [⊢ [_ ≫ (ro:#%app e_fn/progsrc- e_arg- ...) ⇒ : (U τ_out ...)]]])
;; ---------------------------------
;; if
@@ -356,7 +361,7 @@
[⊢ [e_unit ≫ e_unit- ⇒ : _] ...]
[⊢ [e ≫ e- ⇐ : τ_expected]]
--------
- [⊢ [_ ≫ (begin- e_unit- ... e-) ⇐ : _]]]
+ [⊢ [_ ≫ (ro:begin e_unit- ... e-) ⇐ : _]]]
[(begin e_unit ... e) ≫
[⊢ [e_unit ≫ e_unit- ⇒ : _] ...]
[⊢ [e ≫ e- ⇒ : τ_e]]
@@ -410,11 +415,41 @@
(C→ CInt CInt)
(C→ Int Int)))
(define-rosette-primop + : (Ccase-> (C→ CNat CNat CNat)
+ (C→ CNat CNat CNat CNat)
+ (C→ CNat CNat CNat CNat CNat)
+ (C→ Nat Nat Nat)
+ (C→ Nat Nat Nat Nat)
+ (C→ Nat Nat Nat Nat Nat)
+ (C→ CInt CInt CInt)
+ (C→ CInt CInt CInt CInt)
+ (C→ CInt CInt CInt CInt CInt)
+ (C→ Int Int Int)
+ (C→ Int Int Int Int)
+ (C→ Int Int Int Int Int)
+ (C→ CNum CNum CNum)
+ (C→ CNum CNum CNum CNum)
+ (C→ CNum CNum CNum CNum CNum)
+ (C→ Num Num Num)
+ (C→ Num Num Num Num)
+ (C→ Num Num Num Num Num)))
+(define-rosette-primop * : (Ccase-> (C→ CNat CNat CNat)
+ (C→ CNat CNat CNat CNat)
+ (C→ CNat CNat CNat CNat CNat)
(C→ Nat Nat Nat)
+ (C→ Nat Nat Nat Nat)
+ (C→ Nat Nat Nat Nat Nat)
(C→ CInt CInt CInt)
+ (C→ CInt CInt CInt CInt)
+ (C→ CInt CInt CInt CInt CInt)
(C→ Int Int Int)
+ (C→ Int Int Int Int)
+ (C→ Int Int Int Int Int)
(C→ CNum CNum CNum)
- (C→ Num Num Num)))
+ (C→ CNum CNum CNum CNum)
+ (C→ CNum CNum CNum CNum CNum)
+ (C→ Num Num Num)
+ (C→ Num Num Num Num)
+ (C→ Num Num Num Num Num)))
(define-rosette-primop = : (Ccase-> (C→ CInt CInt CBool)
(C→ Int Int Bool)))
(define-rosette-primop < : (Ccase-> (C→ CInt CInt CBool)
@@ -513,6 +548,31 @@
[⊢ [_ ≫ (ro:|| e- ...) ⇒ : Bool]]])
;; ---------------------------------
+;; solver forms
+
+(define-base-types CSolution CPict)
+
+(define-typed-syntax verify
+ [(_ e) ≫
+ [⊢ [e ≫ e- ⇒ : _]]
+ --------
+ [⊢ [_ ≫ (ro:verify e-) ⇒ : CSolution]]]
+ [(_ #:assume ae #:guarantee ge) ≫
+ [⊢ [ae ≫ ae- ⇒ : _]]
+ [⊢ [ge ≫ ge- ⇒ : _]]
+ --------
+ [⊢ [_ ≫ (ro:verify #:assume ae- #:guarantee ge-) ⇒ : CSolution]]])
+
+(define-typed-syntax evaluate
+ [(_ v s) ≫
+ [⊢ [v ≫ v- ⇒ : ty]]
+ [⊢ [s ≫ s- ⇐ : CSolution]]
+ --------
+ [⊢ [_ ≫ (ro:evaluate v- s-) ⇒ : ty]]])
+
+(define-rosette-primop core : (C→ Any Any))
+
+;; ---------------------------------
;; Subtyping
(begin-for-syntax
diff --git a/turnstile/examples/tests/rosette/rosette-guide-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-tests.rkt
@@ -68,16 +68,31 @@
(check-type (asserts) : (CListof Bool) -> (list))
;; sec 2.3
-;; (define (poly [x : Int] -> Int)
-;; (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))
-
-;; (define (factored [x : Int] -> Int)
-;; (* x (+ x 1) (+ x 2) (+ x 2)))
-
-;; (define (same p f x)
-;; (assert (= (p x) (f x))))
-
-;; ; check zeros; all seems well ...
-;; > (same poly factored 0)
-;; > (same poly factored -1)
-;; > (same poly factored -2)
+(define (poly [x : Int] -> Int)
+ (+ (* x x x x) (* 6 x x x) (* 11 x x) (* 6 x)))
+
+(define (factored [x : Int] -> Int)
+ (* x (+ x 1) (+ x 2) (+ x 2)))
+
+(define (same [p : (C→ Int Int)] [f : (C→ Int Int)] [x : Int] -> Unit)
+ (assert (= (p x) (f x))))
+
+; check zeros; all seems well ...
+(check-type+asserts (same poly factored 0) : Unit -> (void) (list))
+(check-type+asserts (same poly factored -1) : Unit -> (void) (list))
+(check-type+asserts (same poly factored -2) : Unit -> (void) (list))
+
+(define-symbolic i integer? : Int)
+(define cex (verify (same poly factored i)))
+(check-type (evaluate i cex) : Int -> 12)
+(check-runtime-exn (same poly factored 12))
+(clear-asserts!)
+
+(require "../../rosette/query/debug.rkt"
+ "../../rosette/lib/render.rkt")
+(define/debug (factored/d [x : Int] -> Int)
+ (* x (+ x 1) (+ x 2) (+ x 2)))
+
+(define ucore (debug [integer?] (same poly factored/d 12)))
+(check-type ucore : CSolution)
+(check-type (render ucore) : CPict)
