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

Added TODO; Δ depends on order, but dict unordered

Browse Source
This commit is contained in:
William J. Bowman 2016-01-11 19:25:31 -05:00
parent 97a11ea253
commit 302d8014fa
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
2 changed files with 2 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

1
cur-lib/cur/curnel/hybrid-core.rkt
View File

@ -558,6 +558,7 @@
(wf Δ (Γ x : t))]
[(side-condition ,(not (empty-Δ? (term Δ_1))))
;; TODO: Depends on order, but "first" here is nondeterministic/unspecified
(where x_D ,(dict-iterate-key (term Δ_1) (dict-iterate-first (term Δ_1))))
(where t_D (Δ-ref-type Δ_1 x_D))
(where (x_c ...) (Δ-ref-constructors Δ_1 x_D))

1
cur-test/cur/tests/hybrid-core.rkt
View File

@ -61,6 +61,7 @@
(nat (Unv 0) ())
(heap (Unv 0) ())
(pre (Π (temp808 : heap) (Unv 0)) ()))))
(displayln sigma)
(check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (true (Unv 0) ((T : true)))))))
(check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (false (Unv 0) ())))))
(check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (equal (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))