From 583469c25ff186e1876d9054062605576da157ac Mon Sep 17 00:00:00 2001
From: Stephen Chang <stchang@ccs.neu.edu>
Date: Sun, 11 Sep 2016 15:36:54 -0400
Subject: [PATCH] add remaining libs; add sec6 guide tests

---
 turnstile/examples/rosette/lib/angelic.rkt    | 13 +++++
 turnstile/examples/rosette/lib/synthax.rkt    | 51 +++++++++++++++++-
 turnstile/examples/rosette/query/debug.rkt    |  5 +-
 turnstile/examples/rosette/rosette2.rkt       | 14 ++++-
 .../rosette/rosette-guide-sec6-tests.rkt      | 52 +++++++++++++++++++
 .../rosette/run-all-rosette-tests-script.rkt  |  3 +-
 6 files changed, 132 insertions(+), 6 deletions(-)
 create mode 100644 turnstile/examples/rosette/lib/angelic.rkt
 create mode 100644 turnstile/examples/tests/rosette/rosette-guide-sec6-tests.rkt

diff --git a/turnstile/examples/rosette/lib/angelic.rkt b/turnstile/examples/rosette/lib/angelic.rkt
new file mode 100644
index 0000000..cc107b0
--- /dev/null
+++ b/turnstile/examples/rosette/lib/angelic.rkt
@@ -0,0 +1,13 @@
+#lang turnstile
+(require
+ (prefix-in t/ro: (only-in "../rosette2.rkt" U))
+ (prefix-in ro: rosette/lib/angelic))
+
+(define-typed-syntax choose*
+  [(ch e ...+) ≫
+   [⊢ [e ≫ e- ⇒ : ty]] ...
+   #:with (e/disarmed ...) (stx-map replace-stx-loc #'(e- ...) #'(e ...))
+   --------
+   ;; the #'choose* identifier itself must have the location of its use
+   ;; see define-synthax implementation, specifically syntax/source in utils
+   [⊢ [_ ≫ (#,(syntax/loc #'ch ro:choose*) e/disarmed ...) ⇒ : (t/ro:U ty ...)]]])
diff --git a/turnstile/examples/rosette/lib/synthax.rkt b/turnstile/examples/rosette/lib/synthax.rkt
index e2bc854..1ed797e 100644
--- a/turnstile/examples/rosette/lib/synthax.rkt
+++ b/turnstile/examples/rosette/lib/synthax.rkt
@@ -1,12 +1,14 @@
 #lang turnstile
 (require
  (only-in "../rosette2.rkt" rosette-typed-out)
- (prefix-in t/ro: (only-in "../rosette2.rkt" Int Bool C→ CSolution Unit))
+ (prefix-in t/ro: (only-in "../rosette2.rkt" U Int Bool type C→ CSolution Unit CSyntax CListof))
  (prefix-in ro: rosette/lib/synthax))
 
 (provide (rosette-typed-out [print-forms : (t/ro:C→ t/ro:CSolution t/ro:Unit)])
          ??)
 
+(provide print-forms generate-forms)
+
 (define-typed-syntax ??
   [(qq) ≫
    #:with ??/progsrc (datum->syntax #'here 'ro:?? #'qq)
@@ -27,3 +29,50 @@
 (define-syntax print-forms
   (make-variable-like-transformer
    (assign-type #'ro:print-forms #'(t/ro:C→ t/ro:CSolution t/ro:Unit))))
+
+(define-syntax generate-forms
+  (make-variable-like-transformer
+   (assign-type #'ro:generate-forms #'(t/ro:C→ t/ro:CSolution (t/ro:CListof t/ro:CSyntax)))))
+
+(define-typed-syntax choose
+  [(ch e ...+) ≫
+   [⊢ [e ≫ e- ⇒ : ty]] ...
+   #:with (e/disarmed ...) (stx-map replace-stx-loc #'(e- ...) #'(e ...))
+   --------
+   ;; the #'choose identifier itself must have the location of its use
+   ;; see define-synthax implementation, specifically syntax/source in utils
+   [⊢ [_ ≫ (#,(syntax/loc #'ch ro:choose) e/disarmed ...) ⇒ : (t/ro:U ty ...)]]])
+
+;; TODO: not sure how to handle define-synthax
+;; it defines a macro, but may refer to itself in #:base and #:else
+;; - so must expand "be" and "ee", but what to do about self reference?
+;; - the current letrec-like implementation results in an #%app of the the f macro
+;;   which isnt quite right
+#;(define-typed-syntax define-synthax #:datum-literals (: -> →)
+  #;[(_ x:id ([pat e] ...+)) ≫
+   [⊢ [e ≫ e- ⇒ : τ]] ...
+   #:with y (generate-temporary #'x)
+   --------
+   [_ ≻ (begin-
+          (define-syntax- x (make-rename-transformer (⊢ y : t/ro:Int)))
+          (ro:define-synthax y ([pat e-] ...)))]]
+  [(_ (f [x:id : ty] ... [k:id : tyk] -> ty_out) #:base be #:else ee) ≫
+   #:with (e ...) #'(be ee)
+   [() ([x ≫ x- : ty] ... [k ≫ k- : tyk] [f ≫ f- : (t/ro:C→ ty ... tyk ty_out)]) ⊢ 
+    [e ≫ e- ⇒ : ty_e] ...]
+   #:with (be- ee-) #'(e- ...)
+   #:with f* (generate-temporary)
+   #:with app-f (format-id #'f "apply-~a" #'f)
+   --------
+   [_ ≻ (begin-
+          (ro:define-synthax (f- x- ... k-) #:base be- #:else ee-)
+          (define-syntax- app-f
+            (syntax-parser
+              [(_ . es)
+               ;; TODO: typecheck es
+               #:with es- (stx-map expand/df #'es)
+;               #:with es/fixsrc (stx-map replace-stx-loc #'es- #'es)
+               (assign-type #'(f- . es) #'ty_out)])))]])
+;             (⊢ f- : (t/ro:C→ ty ... tyk ty_out))
+;          #;(ro:define-synthax (f- x- ... k-)
+;            #:base be- #:else ee-))]])
diff --git a/turnstile/examples/rosette/query/debug.rkt b/turnstile/examples/rosette/query/debug.rkt
index 19c8a2d..6c9c9bb 100644
--- a/turnstile/examples/rosette/query/debug.rkt
+++ b/turnstile/examples/rosette/query/debug.rkt
@@ -19,11 +19,10 @@
    #:with f- (generate-temporary #'f)
    --------
    [_ ≻ (begin-
-          (define-syntax- f
-            (make-rename-transformer (⊢ f- : (t/ro:C→ ty ... ty_out))))
+          (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))))]])
+                    (t/ro:ann (t/ro:begin e ...) : ty_out))))]])
 
 (define-typed-syntax debug
   [(_ (pred? ...+) e) ≫
diff --git a/turnstile/examples/rosette/rosette2.rkt b/turnstile/examples/rosette/rosette2.rkt
index 89ed43e..174c638 100644
--- a/turnstile/examples/rosette/rosette2.rkt
+++ b/turnstile/examples/rosette/rosette2.rkt
@@ -1321,11 +1321,23 @@
                             [=> : (C→ Bool Bool Bool)]))
 
 (define-typed-syntax &&
+  [_:id ≫
+   --------
+   [⊢ [_ ≫ ro:&& ⇒ :
+           (Ccase-> (C→ Bool)
+                    (C→ Bool Bool)
+                    (C→ Bool Bool Bool))]]]
   [(_ e ...) ≫
    [⊢ [e ≫ e- ⇐ : Bool] ...]
    --------
    [⊢ [_ ≫ (ro:&& e- ...) ⇒ : Bool]]])
 (define-typed-syntax ||
+  [_:id ≫
+   --------
+   [⊢ [_ ≫ ro:|| ⇒ :
+           (Ccase-> (C→ Bool)
+                    (C→ Bool Bool)
+                    (C→ Bool Bool Bool))]]]
   [(_ e ...) ≫
    [⊢ [e ≫ e- ⇐ : Bool] ...]
    --------
@@ -1380,7 +1392,7 @@
 ;; ---------------------------------
 ;; solver forms
 
-(define-base-types CSolution CSolver CPict)
+(define-base-types CSolution CSolver CPict CSyntax)
 
 (provide (rosette-typed-out [sat? : (C→ Any Bool)]
                             [unsat? : (C→ Any Bool)]
diff --git a/turnstile/examples/tests/rosette/rosette-guide-sec6-tests.rkt b/turnstile/examples/tests/rosette/rosette-guide-sec6-tests.rkt
new file mode 100644
index 0000000..a57c2f5
--- /dev/null
+++ b/turnstile/examples/tests/rosette/rosette-guide-sec6-tests.rkt
@@ -0,0 +1,52 @@
+#lang s-exp "../../rosette/rosette2.rkt"
+(require "../rackunit-typechecking.rkt")
+
+;; Examples from the Rosette Guide, Section 6 Libraries
+
+;; 6.2.1 Synthesis library
+(require "../../rosette/lib/synthax.rkt")
+
+;; choose
+(define (div2 [x : BV] -> BV)
+  ([choose bvshl bvashr bvlshr bvadd bvsub bvmul] x (?? (bitvector 8))))
+(define-symbolic i (bitvector 8))
+(print-forms
+ (synthesize #:forall (list i)
+             #:guarantee (assert (equal? (div2 i) (bvudiv i (bv 2 8))))))
+(printf "expected output:\n~a\n" 
+        "'(define (div2 [x : BV] -> BV) (bvlshr x (bv 1 8)))")
+
+;; TODO: define-synthax
+; Defines a grammar for boolean expressions
+; in negation normal form (NNF).
+#;(define-synthax (nnf [x : Bool] [y : Bool] [depth : Int] -> Bool)
+ #:base (choose x (! x) y (! y))
+ #:else (choose
+         x (! x) y (! y)
+         ((choose && ||) (nnf x y (- depth 1))
+                         (nnf x y (- depth 1)))))
+ 
+; The body of nnf=> is a hole to be filled with an
+; expression of depth (up to) 1 from the NNF grammar.
+#;(define (nnf=> [x : Bool] [y : Bool] -> Bool)
+  (apply-nnf x y 1))
+ 
+;; (define-symbolic a b boolean?)
+;; (print-forms
+;;    (synthesize
+;;     #:forall (list a b)
+;;     #:guarantee (assert (equal? (=> a b) (nnf=> a b)))))
+;; (printf "expected output:\n~a\n"
+;;         "'(define (nnf=> [x : Bool] [y : Bool] -> Bool) (|| (! x) y))")
+
+;; 6.2.2 Angelic Execution Library
+(require "../../rosette/lib/angelic.rkt")
+
+(define (static -> Int)  (choose 1 2 3))
+(define (dynamic -> Int) (choose* 1 2 3))
+(check-type (equal? (static) (static)) : Bool -> #t)
+(define dyn1 (dynamic))
+(define dyn2 (dynamic))
+(check-type (equal? dyn1 dyn2) : Bool -> (equal? dyn1 dyn2))
+;(= (ite xi?$4 1 (ite xi?$5 2 3)) (ite xi?$6 1 (ite xi?$7 2 3)))
+
diff --git a/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt b/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt
index 2882b41..6117282 100644
--- a/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt
+++ b/turnstile/examples/tests/rosette/run-all-rosette-tests-script.rkt
@@ -12,7 +12,8 @@
           "rosette-guide-sec46-tests.rkt" "Rosette Guide, Section 4.6-4.8"
           "rosette-guide-sec49-tests.rkt" "Rosette Guide, Section 4.9")
 
-(do-tests "rosette-guide-sec5-tests.rkt" "Rosette Guide, Section 5 Structures")
+(do-tests "rosette-guide-sec5-tests.rkt" "Rosette Guide, Section 5 Structures"
+          "rosette-guide-sec6-tests.rkt" "Rosette Guide, Section 6 Libraries")
 
 (do-tests "bv-tests.rkt" "BV SDSL - General"
           "bv-ref-tests.rkt" "BV SDSL - Hacker's Delight synthesis")