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

[FAILS] Π-types cannot appears in app position

Browse Source 
Not sure why I thought they coud; fixed, but some tests not
passing.
This commit is contained in:
William J. Bowman 2016-01-01 17:11:11 -05:00
parent c978b2e45e
commit 588d5b3758
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 5 additions and 6 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

11
curnel/redex-core.rkt
View File

@ -137,6 +137,7 @@
(module+ test (module+ test
(default-equiv (lambda (x y) (term (α-equivalent ,x ,y))))) (default-equiv (lambda (x y) (term (α-equivalent ,x ,y)))))
;; Replace x by t_1 in t_0
(define-metafunction ttL (define-metafunction ttL
subst : t x t -> t subst : t x t -> t
[(subst t_0 x t_1) [(subst t_0 x t_1)
@ -545,7 +546,7 @@
(define tt--> (define tt-->
(reduction-relation tt-redL (reduction-relation tt-redL
(--> (Σ (in-hole E ((any (x : t_0) t_1) t_2))) (--> (Σ (in-hole E ((λ (x : t_0) t_1) t_2)))
(Σ (in-hole E (subst t_1 x t_2))) (Σ (in-hole E (subst t_1 x t_2)))
-->β) -->β)
(--> (Σ (in-hole E (in-hole Θv ((elim x_D U) v_P)))) (--> (Σ (in-hole E (in-hole Θv ((elim x_D U) v_P))))
@ -606,8 +607,8 @@
(module+ test (module+ test
(check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0))) (check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
(check-equiv? (term (reduce ∅ ((λ (x : t) x) (Unv 0)))) (term (Unv 0))) (check-equiv? (term (reduce ∅ ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))
(check-equiv? (term (reduce ∅ ((Π (x : t) x) (Unv 0)))) (term (Unv 0))) (check-not-equiv? (term (reduce ∅ ((Π (x : t) x) (Unv 0)))) (term (Unv 0)))
(check-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0))))) (check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0)))))
(term (Π (x : t) (Unv 0)))) (term (Π (x : t) (Unv 0))))
(check-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x)))) (check-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
(term (Π (x : t) (x x)))) (term (Π (x : t) (x x))))
@ -873,9 +874,7 @@
[(type-infer Σ Γ e_0 (Π (x_0 : t_0) t_1)) [(type-infer Σ Γ e_0 (Π (x_0 : t_0) t_1))
(type-check Σ Γ e_1 t_0) (type-check Σ Γ e_1 t_0)
;; TODO: Not sure why this explicit reduction is necessary, since type-check should check modulo (where t_3 (subst t_1 x_0 e_1))
;; equivalence.
(where t_3 (reduce Σ ((Π (x_0 : t_0) t_1) e_1)))
----------------- "DTR-Application" ----------------- "DTR-Application"
(type-infer Σ Γ (e_0 e_1) t_3)] (type-infer Σ Γ (e_0 e_1) t_3)]