commit 90e9517b3a53f1be3b2dc2b499a884b4a030cf8c
parent 60fa8ab91f62e6e2bb07b7dc7400498d6d9dff67
Author: Stephen Chang <stchang@ccs.neu.edu>
Date: Wed, 31 Aug 2016 15:02:21 -0400
add synthesize and lib/synthax
Diffstat:
6 files changed, 65 insertions(+), 7 deletions(-)
diff --git a/turnstile/examples/rosette/lib/render.rkt b/turnstile/examples/rosette/lib/render.rkt
@@ -4,13 +4,13 @@
(prefix-in ro: rosette/lib/render))
(define-typed-syntax render
- [(r s) ≫
+ [(_ s) ≫
[⊢ [s ≫ s- ⇐ : t/ro:CSolution]]
--------
- [⊢ [_ ≫ (#,(syntax/loc #'r ro:render) s-) ⇒ : t/ro:CPict]]]
- [(r s sz) ≫
+ [⊢ [_ ≫ (ro:render s-) ⇒ : t/ro:CPict]]]
+ [(_ s sz) ≫
[⊢ [s ≫ s- ⇐ : t/ro:CSolution]]
[⊢ [sz ≫ sz- ⇐ : t/ro:CNat]]
--------
- [⊢ [_ ≫ (#,(syntax/loc #'r ro:render) s- sz-) ⇒ : t/ro:CPict]]])
+ [⊢ [_ ≫ (ro:render s- sz-) ⇒ : t/ro:CPict]]])
diff --git a/turnstile/examples/rosette/lib/synthax.rkt b/turnstile/examples/rosette/lib/synthax.rkt
@@ -0,0 +1,21 @@
+#lang turnstile
+(require
+ (prefix-in t/ro: (only-in "../rosette2.rkt" Int Bool type C→ CSolution Unit))
+ (prefix-in ro: rosette/lib/synthax))
+
+(provide print-forms)
+
+(define-typed-syntax ??
+ [(qq) ≫
+ #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
+ --------
+ [⊢ [_ ≫ (??/progsrc) ⇒ : t/ro:Int]]]
+ [(qq pred : ty:t/ro:type) ≫
+ #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
+ [⊢ [pred ≫ pred- ⇐ : (t/ro:C→ ty.norm t/ro:Bool)]]
+ --------
+ [⊢ [_ ≫ (??/progsrc pred-) ⇒ : ty.norm]]])
+
+(define-syntax print-forms
+ (make-variable-like-transformer
+ (assign-type #'ro:print-forms #'(t/ro:C→ t/ro:CSolution t/ro:Unit))))
diff --git a/turnstile/examples/rosette/query/debug.rkt b/turnstile/examples/rosette/query/debug.rkt
@@ -4,14 +4,14 @@
(prefix-in ro: rosette/query/debug))
(define-typed-syntax define/debug #:datum-literals (: -> →)
- [(d x:id e) ≫
+ [(_ 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 ...+) ≫
+ [(_ (f [x : ty] ... (~or → ->) ty_out) e ...+) ≫
; [⊢ [e ≫ e- ⇒ : ty_e]]
#:with f- (generate-temporary #'f)
--------
@@ -22,7 +22,7 @@
(t/ro:ann (t/ro:begin e ...) : ty_out))))]])
(define-typed-syntax debug
- [(d (solvable-pred ...+) e) ≫
+ [(_ (solvable-pred ...+) e) ≫
[⊢ [solvable-pred ≫ solvable-pred- ⇐ : (t/ro:C→ t/ro:Nothing t/ro:Bool)]] ...
[⊢ [e ≫ e- ⇒ : τ]]
--------
diff --git a/turnstile/examples/rosette/rosette-notes.txt b/turnstile/examples/rosette/rosette-notes.txt
@@ -1,5 +1,11 @@
2016-08-31 --------------------
+Rosette TODO:
+- fix documentation of synthesize
+ - #:forall accepts everything, not just constant?s
+
+2016-08-31 --------------------
+
Adding typed define/debug, debug (from query/debug), render (from lib/query):
- revealed problems with the way Rosette tracks source locations
- in query/debug.rkt: https://github.com/emina/rosette/blob/cb877b9094f368c5f392518e7538ae8a061433a2/rosette/query/debug.rkt#L38
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
@@ -571,6 +571,20 @@
[⊢ [_ ≫ (ro:evaluate v- s-) ⇒ : ty]]])
(define-rosette-primop core : (C→ Any Any))
+(define-rosette-primop sat? : (C→ Any Bool))
+
+(define-typed-syntax synthesize
+ [(_ #:forall ie #:guarantee ge) ≫
+ [⊢ [ie ≫ ie- ⇐ : (CListof Any)]]
+ [⊢ [ge ≫ ge- ⇒ : _]]
+ --------
+ [⊢ [_ ≫ (ro:synthesize #:forall ie- #:guarantee ge-) ⇒ : CSolution]]]
+ [(_ #:forall ie #:assume ae #:guarantee ge) ≫
+ [⊢ [ie ≫ ie- ⇐ : (CListof Any)]]
+ [⊢ [ae ≫ ae- ⇒ : _]]
+ [⊢ [ge ≫ ge- ⇒ : _]]
+ --------
+ [⊢ [_ ≫ (ro:synthesize #:forall ie- #:assume ae- #:guarantee ge-) ⇒ : CSolution]]])
;; ---------------------------------
;; Subtyping
diff --git a/turnstile/examples/tests/rosette/rosette-guide-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-tests.rkt
@@ -95,4 +95,21 @@
(define ucore (debug [integer?] (same poly factored/d 12)))
(check-type ucore : CSolution)
+;; TESTING TODO: requires visual inspection (in DrRacket)
(check-type (render ucore) : CPict)
+
+(require "../../rosette/lib/synthax.rkt")
+(define (factored/?? [x : Int] -> Int)
+ (* (+ x (??)) (+ x 1) (+ x (??)) (+ x (??))))
+
+(define binding
+ (synthesize #:forall (list i)
+ #:guarantee (same poly factored/?? i)))
+(check-type binding : CSolution)
+(check-type (sat? binding) : Bool -> #t)
+;; TESTING TODO: requires visual inspection of stdout
+(check-type (print-forms binding) : Unit -> (void))
+;; typed/rosette should print:
+;; '(define (factored/?? (x : Int) -> Int) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0)))
+;; (untyped) rosette should print:
+;; '(define (factored x) (* (+ x 3) (+ x 1) (+ x 2) (+ x 0)))
