suzanne.soy/macrotypes
1
0
Fork 0
Code Issues Pull Requests Actions Packages Projects Releases Wiki Activity

check for constants in forall and exists

Browse Source
This commit is contained in:
Stephen Chang 2016-09-07 19:26:05 -04:00
parent 2e7e6a5d5c
commit a605de099b
2 changed files with 50 additions and 5 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

44
turnstile/examples/rosette/rosette2.rkt
View File

@ -1042,16 +1042,50 @@
(define-base-types CSolution CPict)
(provide (rosette-typed-out [core : (C→ CSolution (U (Listof Any) CFalse))]
; TODO: implement hash
[model : (C→ CSolution (CHashTable Any Any))]
[sat : (Ccase-> (C→ CSolution)
(C→ (CHashTable Any Any) CSolution))]
[sat? : (C→ Any Bool)]
[unsat? : (C→ Any Bool)]
[unsat : (Ccase-> (C→ CSolution)
(C→ (CListof Bool) CSolution))]
[forall : (C→ (CListof Any) Bool Bool)]
[exists : (C→ (CListof Any) Bool Bool)]))
(C→ (CListof Bool) CSolution))]))
;(define-rosette-primop forall : (C→ (CListof Any) Bool Bool))
;(define-rosette-primop exists : (C→ (CListof Any) Bool Bool))
(define-typed-syntax forall
[(_ vs body) ≫
[⊢ [vs ≫ vs- ⇒ : (~CListof ~! ty)]]
#:fail-unless (Constant*? #'ty)
(format "Expected list of symbolic constants, given list of ~a"
(type->str #'ty))
[⊢ [body ≫ body- ⇐ : Bool]]
--------
[⊢ [_ ≫ (ro:forall vs- body-) ⇒ : Bool]]]
[(_ vs body) ≫
[⊢ [vs ≫ vs- ⇒ : (~CList ~! ty ...)]]
#:fail-unless (stx-andmap Constant*? #'(ty ...))
(format "Expected list of symbolic constants, given list containing: ~a"
(string-join (stx-map type->str #'(ty ...)) ", "))
[⊢ [body ≫ body- ⇐ : Bool]]
--------
[⊢ [_ ≫ (ro:forall vs- body-) ⇒ : Bool]]])
(define-typed-syntax exists
[(_ vs body) ≫
[⊢ [vs ≫ vs- ⇒ : (~CListof ~! ty)]]
#:fail-unless (Constant*? #'ty)
(format "Expected list of symbolic constants, given list of ~a"
(type->str #'ty))
[⊢ [body ≫ body- ⇐ : Bool]]
--------
[⊢ [_ ≫ (ro:exists vs- body-) ⇒ : Bool]]]
[(_ vs body) ≫
[⊢ [vs ≫ vs- ⇒ : (~CList ~! ty ...)]]
#:fail-unless (stx-andmap Constant*? #'(ty ...))
(format "Expected list of symbolic constants, given list containing: ~a"
(string-join (stx-map type->str #'(ty ...)) ", "))
[⊢ [body ≫ body- ⇐ : Bool]]
--------
[⊢ [_ ≫ (ro:exists vs- body-) ⇒ : Bool]]])
(define-typed-syntax verify
[(_ e) ≫
@ -1071,7 +1105,7 @@
--------
[⊢ [_ ≫ (ro:evaluate v- s-) ⇒ : ty]]])
;; TODO: enforce list of constants?
(define-typed-syntax synthesize
[(_ #:forall ie #:guarantee ge) ≫
[⊢ [ie ≫ ie- ⇐ : (CListof Any)]]

11
turnstile/examples/tests/rosette/rosette-guide-sec4-tests.rkt
View File

@ -231,6 +231,17 @@
(define-symbolic a1 b1 integer?)
(check-type (forall (list) (= a1 b1)) : Bool -> (= a1 b1))
(define f1 (forall (list a1) (exists (list b1) (= a1 (+ a1 b1))))) ; no free constants
(check-type (list 1) : (CListof PosInt))
(check-type (list 1) : (CList PosInt))
(typecheck-fail (exists (list 1) (= a1 b1))
#:with-msg "Expected list of symbolic constants, given list containing: PosInt")
(typecheck-fail (exists (list (+ a1 b1)) (= a1 b1))
#:with-msg "Expected list of symbolic constants, given list containing: Int")
(check-type (cons a1 (cons b (list))) : (CList (Constant Int) (Constant Bool)))
(typecheck-fail (forall (list 1) (= a1 b1))
#:with-msg "Expected list of symbolic constants, given list containing: PosInt")
(typecheck-fail (forall (list (+ a1 b1)) (= a1 b1))
#:with-msg "Expected list of symbolic constants, given list containing: Int")
; so the model has no bindings
(define sol1 (solve (assert f1)))
(check-type sol1 : CSolution)