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

Separate judgment for checking constructors

Browse Source
This commit is contained in:
William J. Bowman 2016-03-25 13:42:23 -04:00
parent 8b58736101
commit 3de6a132cd
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
2 changed files with 27 additions and 23 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

26
cur-lib/cur/curnel/redex-core.rkt
View File

@ -445,14 +445,15 @@
,(and (term (nonpositive x t_0)) (term (positive x t)))]
[(positive x t) #t])
(define-metafunction tt-typingL
positive* : x (t ...) -> #t or #f
[(positive* D ()) #t]
[(positive* D (t_c t_rest ...))
;; Replace the result of the constructor with (Unv 0), to avoid the result being considered a
;; nonpositive position.
,(and (term (positive D (in-hole Ξ (Unv 0)))) (term (positive* D (t_rest ...))))
(where (in-hole Ξ (in-hole Θ D)) t_c)])
;; Holds when the type t is a valid type for a constructor of D
(define-judgment-form tt-typingL
#:mode (valid-constructor I I)
#:contract (valid-constructor D t)
;; NB TODO: Ignore the "positive" occurrence of D in the result; this is hacky way to do this
[(side-condition (positive D (in-hole Ξ (Unv 0))))
---------------------------------------------------------
(valid-constructor D (name t_c (in-hole Ξ (in-hole Θ D))))])
;; Holds when the signature Δ is valid
(define-judgment-form tt-typingL
@ -464,15 +465,10 @@
[(valid Δ)
(type-infer Δ ∅ t_D U_D)
(valid-constructor D t_c) ...
(type-infer Δ (∅ D : t_D) t_c U_c) ...
;; NB: Ugh this should be possible with pattern matching alone ....
(side-condition ,(andmap (curry equal? (term D)) (term (D_0 ...))))
(side-condition (positive* D (t_c ...)))
----------------- "Valid-Inductive"
(valid (Δ (D : t_D
;; Checks that a constructor for x actually produces an x, i.e., that
;; the constructor is well-formed.
((c : (name t_c (in-hole Ξ (in-hole Θ D_0)))) ...))))])
(valid (Δ (D : t_D ((c : t_c) ...))))])
;; Holds when the signature Δ and typing context Γ are well-formed.
(define-judgment-form tt-typingL

24
cur-test/cur/tests/redex-core.rkt
View File

@ -225,19 +225,26 @@
;; Test static semantics
;; ------------------------------------------------------------------------
(check-true (term (positive* nat (nat))))
(check-true (term (positive* nat ((Π (x : (Unv 0)) (Π (y : (Unv 0)) nat))))))
(check-true (term (positive* nat ((Π (x : nat) nat)))))
(check-holds
(valid-constructor nat nat))
(check-holds
(valid-constructor nat (Π (x : (Unv 0)) (Π (y : (Unv 0)) nat))))
(check-holds
(valid-constructor nat (Π (x : nat) nat)))
;; (nat -> nat) -> nat
;; Not sure if this is actually supposed to pass
(check-false (term (positive* nat ((Π (x : (Π (y : nat) nat)) nat)))))
(check-not-holds
(valid-constructor nat (Π (x : (Π (y : nat) nat)) nat)))
;; ((Unv 0) -> nat) -> nat
(check-true (term (positive* nat ((Π (x : (Π (y : (Unv 0)) nat)) nat)))))
(check-holds
(valid-constructor nat (Π (x : (Π (y : (Unv 0)) nat)) nat)))
;; (((nat -> (Unv 0)) -> nat) -> nat)
(check-true (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat)))))
(check-holds
(valid-constructor nat (Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat)))
;; Not sure if this is actually supposed to pass
;; ((nat -> nat) -> nat) -> nat
(check-false (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat)))))
(check-not-holds
(valid-constructor nat (Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat)))
(check-true (judgment-holds (wf ,Δ0 ∅)))
(check-true (redex-match? tt-redL (in-hole Ξ (Unv 0)) (term (Unv 0))))
@ -280,7 +287,8 @@
(check-holds (type-infer ∅ ∅ (Unv 0) U))
(check-holds (type-infer ∅ (∅ nat : (Unv 0)) nat U))
(check-holds (type-infer ∅ (∅ nat : (Unv 0)) (Π (x : nat) nat) U))
(check-true (term (positive* nat (nat (Π (x : nat) nat)))))
(check-holds (valid-constructor nat nat))
(check-holds (valid-constructor nat (Π (x : nat) nat)))
(check-holds
(wf (∅ (nat : (Unv 0) ((zero : nat)))) ∅))
(check-holds