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

Reorganized eliminator typing

Browse Source 
Typing of eliminators is now entirely in metafunctions. It is easier to
understand, and should lead to more efficient typing. Some of these
functions should be exposed via reflection.
This commit is contained in:
William J. Bowman 2015-10-01 17:45:37 -04:00
parent bd2e06acce
commit fd455b7a07
No known key found for this signature in database
GPG Key ID: DDD48D26958F0D1A
1 changed files with 45 additions and 37 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

82
curnel/redex-core.rkt
View File

@ -372,9 +372,8 @@
[(Θ-ref (in-hole Θ (hole e)) 0) e]
[(Θ-ref (in-hole Θ (hole e)) natural) (Θ-ref Θ ,(sub1 (term natural)))])
;; 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
;;; ------------------------------------------------------------------------
;;; Computing the types of eliminators
;; Returns the telescope of the arguments for the constructor x_ci of the inductively defined type x_D
(define-metafunction tt-ctxtL
@ -497,6 +496,45 @@
(term (Σ-methods-telescope ,sigma false (λ (y : false) (Π (x : Type) x))))
(term hole)))
;; Computes the type of the eliminator for the inductively defined type x_D with a motive whose result
;; is in universe U.
;;
;; The type of (elim x_D U) is something like:
;; (∀ (P : (∀ a -> ... -> (D a ...) -> U))
;; (method_ci ...) -> ... ->
;; (a -> ... -> (D a ...) ->
;; (P a ... (D a ...))))
;;
;; x_D is an inductively defined type
;; U is the sort the motive
;; x_P is the name of the motive
;; Ξ_P*D is the telescope of the parameters of x_D and
;; the witness of type x_D (applied to the parameters)
;; Ξ_m is the telescope of the methods for x_D
(define-metafunction tt-ctxtL
Σ-elim-type : Σ x U -> t
[(Σ-elim-type Σ x_D U)
(Π (x_P : (in-hole Ξ_P*D U))
;; The methods Ξ_m for each constructor of type x_D
(in-hole Ξ_m
;; And finally, the parameters and discriminant
(in-hole Ξ_P*D
;; The result is (P a ... (x_D a ...)), i.e., the motive
;; applied to the paramters and discriminant
(Ξ-apply Ξ_P*D x_P))))
;; Get the parameters of x_D
(where Ξ (Σ-ref-parameter-Ξ Σ x_D))
;; A fresh name to bind the discriminant
(where x ,(variable-not-in (term (Σ Γ x_D Ξ)) 'x-D))
;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
;; of the parameters and the inductive type applied to the
;; parameters
(where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ x_D)) hole)))
;; A fresh name for the motive
(where x_P ,(variable-not-in (term (Σ Γ x_D Ξ Ξ_P*D x)) 'x-P))
;; The types of the methods for this inductive.
(where Ξ_m (Σ-methods-telescope Σ x_D x_P))])
;;; ------------------------------------------------------------------------
;;; Dynamic semantics
;;; The majority of this section is dedicated to evaluation of (elim x U), the eliminator for the
@ -521,7 +559,6 @@
;; Create the recursive applications of elim to the recursive
;; arguments of an inductive constructor.
;; TODO: Poorly documented, and poorly tested.
;; Probably the source of issue #20
(define-metafunction tt-redL
elim-recur : x U e Θ Θ Θ (x ...) -> Θ
[(elim-recur x_D U e_P Θ
@ -857,40 +894,11 @@
----------------- "DTR-Abstraction"
(type-infer Σ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
[(type-infer Σ Γ x_D (in-hole Ξ t_D))
(where Ξ (Σ-ref-parameter-Ξ Σ x_D))
;; A fresh name to bind the discriminant
(where x ,(variable-not-in (term (Σ Γ x_D Ξ)) 'x-D))
;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
;; of the parameters and the inductive type applied to the
;; parameters
(where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ x_D)) hole)))
;; A fresh name for the motive
(where x_P ,(variable-not-in (term (Σ Γ x_D Ξ Ξ_P*D x)) 'x-P))
;; The types of the methods for this inductive.
(where Ξ_m (Σ-methods-telescope Σ x_D x_P))
;; NB: Sort of redundant since we will actually infer this exact type for x_D
;; TODO: Do we want to check the Σ-elim-telescope is well-formed?
[(type-check Σ Γ x_D (Σ-ref-type Σ x_D))
----------------- "DTR-Elim_D"
(type-infer Σ Γ (elim x_D U)
;; The type of (elim x_D U) is something like:
;; (∀ (P : (∀ a -> ... -> (D a ...) -> U))
;; (method_ci ...) -> ... ->
;; (a -> ... -> (D a ...) ->
;; (P a ... (D a ...))))
;;
;; x_D is an inductively defined type
;; U is the sort the motive
;; x_P is the name of the motive
;; Ξ_P*D is the telescope of the parameters of x_D and
;; the witness of type x_D (applied to the parameters)
;; Ξ_m is the telescope of the methods for x_D
(Π (x_P : (in-hole Ξ_P*D U))
;; The methods Ξ_m for each constructor of type x_D
(in-hole Ξ_m
;; And finally, the parameters and discriminant
(in-hole Ξ_P*D
;; The result is (P a ... (x_D a ...)), i.e., the motive
;; applied to the paramters and discriminant
(Ξ-apply Ξ_P*D x_P)))))])
(type-infer Σ Γ (elim x_D U) (Σ-elim-type Σ x_D U))])
(define-judgment-form tt-typingL
#:mode (type-check I I I I)