From bd2e06acce6e6bd88c4bead895b0270cb6e8a2ba Mon Sep 17 00:00:00 2001 From: "William J. Bowman" Date: Thu, 1 Oct 2015 16:54:21 -0400 Subject: [PATCH] Removed unused judgment --- curnel/redex-core.rkt | 66 ++++++------------------------------------- 1 file changed, 9 insertions(+), 57 deletions(-) diff --git a/curnel/redex-core.rkt b/curnel/redex-core.rkt index 247eb16..5abdf20 100644 --- a/curnel/redex-core.rkt +++ b/curnel/redex-core.rkt @@ -375,12 +375,6 @@ ;; TODO: The next 3 metafunctons are a mess. They should probably be organized like this: ;; Σ-elim-telescope : Σ x_D U -> Ξ ;; This one should do all the work currently done in DTR-Elim_D -;; Σ-methods-telescope : Σ x_D t_P -> Ξ -;; Σ-constructor-method-telescope : Σ x_D x_c t_P -> Ξ -;; Σ-constructor-inductive-telescope : Σ x_D x_c -> Ξ -;; Σ-constructor-inductive-hypotheses : Σ x_D x_c t_P -> Ξ -;; Returns the inductive arguments to the constructor x_ci of the -;; inducitvely defined type x_D ;; Returns the telescope of the arguments for the constructor x_ci of the inductively defined type x_D (define-metafunction tt-ctxtL @@ -482,13 +476,11 @@ (term (Π (m-zero : (P zero)) (Π (m-s : (Π (x : nat) (Π (ih-x : (P x)) (P (s x))))) hole)))) - ;; TODO: After reduce, check that this is equivalent to the expected this. (check-equiv? (term (Σ-methods-telescope ,Σ nat (λ (x : nat) nat))) (term (Π (m-zero : ((λ (x : nat) nat) zero)) (Π (m-s : (Π (x : nat) (Π (ih-x : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x))))) hole)))) - ;; TODO: After reduce, check that this is equivalent to the expected this. (check-equiv? (term (Σ-methods-telescope ,Σ4 and (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true))))) (term (Π (m-conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B) @@ -507,10 +499,11 @@ ;;; ------------------------------------------------------------------------ ;;; Dynamic semantics +;;; The majority of this section is dedicated to evaluation of (elim x U), the eliminator for the +;;; inductively defined type x with a motive whose result is in universe U (define-extended-language tt-redL tt-ctxtL ;; NB: (in-hole Θv (elim x U)) is only a value when it's a partially applied elim. - ;; TODO: Perhaps (elim x U) should step to an eta-expanded version of elim (v ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U))) (Θv ::= hole (Θv v)) ;; call-by-value, plus reduce under Π (helps with typing checking) @@ -692,9 +685,12 @@ ----------------- "≡-αβ" (equivalent Σ t_0 t_1)]) +;;; ------------------------------------------------------------------------ +;;; Type checking and synthesis + (define-extended-language tt-typingL tt-redL - ;; NB: There may be a bijection between Γ and Ξ. That's - ;; NB: interesting. + ;; NB: There may be a bijection between Γ and Ξ. That's interesting. + ;; NB: Also a bijection between Γ and a list of maps from x to t. (Γ ::= ∅ (Γ x : t))) (define Γ? (redex-match? tt-typingL Γ)) @@ -722,6 +718,7 @@ (define-metafunction ttL positive : t any -> #t or #f [(positive any_1 any_2) #t]) + ;; NB: These tests may or may not fail because positivity checking is not implemented. (module+ test (check-true (term (positive nat nat))) @@ -764,6 +761,7 @@ ;; Checks that a constructor for x actually produces an x, i.e., that ;; the constructor is well-formed. ((x_c : (name t_c (in-hole Ξ_D* (in-hole Φ (in-hole Θ x_D*))))) ...))) ∅)]) + (module+ test (check-true (judgment-holds (wf ,Σ0 ∅))) (check-true (redex-match? tt-redL (in-hole Ξ (Unv 0)) (term (Unv 0)))) @@ -821,48 +819,6 @@ (check-holds (wf (∅ (nat : (Unv 0) ())) (∅ x : (Π (x : nat) nat))))) -;; Holds when an apply context Θ provides arguments that match the -;; telescope Ξ -(define-judgment-form tt-typingL - #:mode (telescope-types I I I I) - #:contract (telescope-types Σ Γ Θ Ξ) - - [----------------- "TT-Hole" - (telescope-types Σ Γ hole hole)] - - [(type-check Σ Γ e t) - (telescope-types Σ Γ Θ Ξ) - ----------------- "TT-Match" - (telescope-types Σ Γ (in-hole Θ (hole e)) (Π (x : t) Ξ))]) -(module+ test - (check-holds - (telescope-types ,Σ ∅ (hole zero) (Π (x : nat) hole))) - (check-true - (redex-match? tt-redL (in-hole Θ (hole e)) - (term ((hole zero) (λ (x : nat) x))))) - ;; TODO: Why should this be true? (hole zero) seems to simple. - (check-holds - (telescope-types ,Σ ∅ (hole zero) - (Σ-methods-telescope ,Σ nat (λ (x : nat) nat)))) - (check-holds - (type-check ,Σ ∅ (λ (x : nat) (λ (ih-x : nat) x)) - (Π (x : nat) (Π (ih-x : nat) nat)))) - (check-holds - (telescope-types ,Σ ∅ - ((hole zero) - (λ (x : nat) (λ (ih-x : nat) x))) - (Σ-methods-telescope ,Σ nat (λ (x : nat) nat)))) - (check-holds - (telescope-types (,Σ4 (true : (Unv 0) ((tt : true)))) - ∅ (hole (λ (A : (Unv 0)) (λ (B : (Unv 0)) - (λ (a : A) (λ (b : B) tt))))) - (Σ-methods-telescope ,Σ4 and - (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))))) - (check-holds - (telescope-types ,sigma (∅ x : false) - hole - (Σ-methods-telescope ,sigma false (λ (y : false) (Π (x : Type) x)))))) - ;; TODO: Bi-directional and inference? ;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf @@ -976,13 +932,9 @@ (check-holds (type-infer ,Σtruth ∅ (λ (x : truth) (Unv 1)) (in-hole Ξ (Π (x : (in-hole Θ truth)) U)))) - ;; TODO: ensure equivalent to expected result (check-equiv? (term (Σ-methods-telescope ,Σtruth truth (λ (x : truth) (Unv 1)))) (term (Π (m-T : ((λ (x : truth) (Unv 1)) T)) hole))) - (check-holds (telescope-types ,Σtruth ∅ (hole (Unv 0)) - (Σ-methods-telescope ,Σtruth truth - (λ (x : truth) (Unv 1))))) (check-holds (type-infer ,Σtruth ∅ (elim truth Type) t)) (check-holds (type-check (∅ (truth : (Unv 0) ((T : truth)))) ∅