From 302d8014fa489a92eb6b77f0cde08dca6adcf078 Mon Sep 17 00:00:00 2001 From: "William J. Bowman" <wjb@williamjbowman.com> Date: Mon, 11 Jan 2016 19:25:31 -0500 Subject: [PATCH] =?UTF-8?q?Added=20TODO;=20=CE=94=20depends=20on=20order,?= =?UTF-8?q?=20but=20dict=20unordered?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- cur-lib/cur/curnel/hybrid-core.rkt | 1 + cur-test/cur/tests/hybrid-core.rkt | 1 + 2 files changed, 2 insertions(+) diff --git a/cur-lib/cur/curnel/hybrid-core.rkt b/cur-lib/cur/curnel/hybrid-core.rkt index ecdbbbc..177ff6a 100644 --- a/cur-lib/cur/curnel/hybrid-core.rkt +++ b/cur-lib/cur/curnel/hybrid-core.rkt @@ -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)) diff --git a/cur-test/cur/tests/hybrid-core.rkt b/cur-test/cur/tests/hybrid-core.rkt index 6a89fff..3bb117a 100644 --- a/cur-test/cur/tests/hybrid-core.rkt +++ b/cur-test/cur/tests/hybrid-core.rkt @@ -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)))