From 10a143a16d6abb31c22915a1075afa694bea809a Mon Sep 17 00:00:00 2001 From: Stephen Chang Date: Tue, 30 Aug 2016 16:58:15 -0400 Subject: [PATCH] add verify, evaluate; and debug, render in separate libs --- macrotypes/stx-utils.rkt | 2 + turnstile/examples/rosette/lib/render.rkt | 16 +++++ turnstile/examples/rosette/query/debug.rkt | 30 ++++++++ turnstile/examples/rosette/rosette-notes.txt | 8 +++ turnstile/examples/rosette/rosette2.rkt | 72 +++++++++++++++++-- .../tests/rosette/rosette-guide-tests.rkt | 35 ++++++--- 6 files changed, 147 insertions(+), 16 deletions(-) create mode 100644 turnstile/examples/rosette/lib/render.rkt create mode 100644 turnstile/examples/rosette/query/debug.rkt diff --git a/macrotypes/stx-utils.rkt b/macrotypes/stx-utils.rkt index ab7268c..81c5bdc 100644 --- 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 new file mode 100644 index 0000000..aa17190 --- /dev/null +++ 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 new file mode 100644 index 0000000..0079949 --- /dev/null +++ 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 index 4958fc8..cc73732 100644 --- 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 index 51306c5..aa30114 100644 --- 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→ 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→ 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→ CInt CInt CBool) (C→ Int Int Bool))) (define-rosette-primop < : (Ccase-> (C→ CInt CInt CBool) @@ -512,6 +547,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 diff --git a/turnstile/examples/tests/rosette/rosette-guide-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-tests.rkt index c4d2c8e..345809f 100644 --- 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 (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 (factored [x : Int] -> Int) + (* x (+ x 1) (+ x 2) (+ x 2))) -;; (define (same p f x) -;; (assert (= (p x) (f x)))) +(define (same [p : (C→ Int Int)] [f : (C→ Int Int)] [x : Int] -> Unit) + (assert (= (p x) (f x)))) -;; ; check zeros; all seems well ... -;; > (same poly factored 0) -;; > (same poly factored -1) -;; > (same poly factored -2) +; 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)