add remaining libs; add sec6 guide tests

This commit is contained in:
Stephen Chang 2016-09-11 15:36:54 -04:00
parent 60c13fdd18
commit 583469c25f
6 changed files with 132 additions and 6 deletions

View File

@ -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 ...)]]])

View File

@ -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-))]])

View File

@ -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)

View File

@ -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)]

View File

@ -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)))

View File

@ -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")