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

start hash tables

Browse Source
This commit is contained in:
Stephen Chang 2016-09-03 21:29:38 -04:00
parent 4007d64ff1
commit c601a4f46b
2 changed files with 13 additions and 4 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -84,6 +84,8 @@
(define-type-constructor CIVectorof #:arity = 1)
(define-type-constructor CMVectorof #:arity = 1)
(define-type-constructor CBoxof #:arity = 1)
;; TODO: Hash subtyping?
(define-type-constructor HashTable #:arity = 2)
(define-named-type-alias (CVectorof X) (CU (CIVectorof X) (CMVectorof X)))
(define-type-constructor CList #:arity >= 0)
@ -450,6 +452,11 @@
#'(CIVectorof (CU τ ...))
#'(CIVectorof (U τ ...)))]]])
;; ---------------------------------
;; hash tables
(define-rosette-primop hash-keys : (C→ (HashTable Any Any) (CListof Any)))
;; ---------------------------------
;; lists
@ -918,16 +925,16 @@
(provide (rosette-typed-out [core : (C→ CSolution (U (Listof Any) CFalse))]
; TODO: implement hash
[model : (C→ CSolution Any)]
[model : (C→ CSolution (HashTable Any Any))]
[sat : (Ccase-> (C→ CSolution)
(C→ Any CSolution))]
(C→ (HashTable 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)]))
(define-typed-syntax verify
[(_ e) ≫
[⊢ [e ≫ e- ⇒ : _]]

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

@ -232,7 +232,9 @@
(define f1 (forall (list a1) (exists (list b1) (= a1 (+ a1 b1))))) ; no free constants
; so the model has no bindings
(define sol1 (solve (assert f1)))
(check-type sol1 : CSolution) ; -> (sat) ; TODO: how to check empty model?
(check-type sol1 : CSolution)
(check-type (model sol1) : (HashTable Any Any))
(check-type (hash-keys (model sol1)) : (CListof Any) -> (list)) ; empty solution
(check-type (sat? sol1) : Bool -> #t)
(define g1 (forall (list a1) (= a1 (+ a1 b1)))) ; b is free in g
; so the model has a binding for b