@ -28,14 +28,19 @@
( U ::= ( Unv i ) )
( D x c ::= variable-not-otherwise-mentioned )
( Δ ::= ∅ ( Δ ( D : t ( ( c : t ) ... ) ) ) )
( t e ::= U ( λ ( x : e ) e ) x ( Π ( x : e ) e ) ( e e )
;; TODO: Might make more sense for methods to come first
( t e ::= U ( λ ( x : t ) e ) x ( Π ( x : t ) t ) ( e e )
;; (elim inductive-type motive (indices ...) (methods ...) discriminant)
( elim D e ( e ... ) ( e ... ) e ) )
#:binding-forms
( λ ( x : t ) e #:refers-to x )
( Π ( x : t_0 ) t_1 #:refers-to x ) )
( define x? ( redex-match? ttL x ) )
( define t? ( redex-match? ttL t ) )
( define e? ( redex-match? ttL e ) )
( define U? ( redex-match? ttL U ) )
( define Δ? ( redex-match? ttL Δ ) )
;;; ------------------------------------------------------------------------
;;; Universe typing
@ -62,95 +67,79 @@
----------------
( unv-pred ( Unv i_1 ) ( Unv i_2 ) ( Unv i_3 ) ) ] )
( define-metafunction ttL
α : t t -> #t or #f
[ ( α t_0 t_1 )
, ( alpha-equivalent? ttL ( term t_0 ) ( term t_1 ) ) ] )
;; Replace x by t_1 in t_0
( define-metafunction ttL
subst : t x t -> t
[ ( subst t_0 x t_1 )
( substitute t_0 x t_1 ) ] )
( define-metafunction ttL
subst-all : t ( x ... ) ( e ... ) -> t
[ ( subst-all t ( ) ( ) ) t ]
[ ( subst-all t ( x_0 x ... ) ( e_0 e ... ) )
( subst-all ( subst t x_0 e_0 ) ( x ... ) ( e ... ) ) ] )
;;; ------------------------------------------------------------------------
;;; Primitive Operations on signatures Δ (those operations that do not require contexts)
;; TODO: Define generic traversals of Δ and Γ ?
( define-metafunction ttL
Δ-in-dom : Δ D -> #t or #f
[ ( Δ-in-dom ∅ D )
#f ]
[ ( Δ-in-dom ( Δ ( D : t any ) ) D )
#t ]
[ ( Δ-in-dom ( Δ ( D_!_0 : any_D any ) ) ( name D D_!_0 ) )
( Δ-in-dom Δ D ) ] )
( define-metafunction ttL
Δ-in-constructor-dom : Δ c -> #t or #f
[ ( Δ-in-constructor-dom ∅ c )
#f ]
[ ( Δ-in-constructor-dom ( Δ ( D : any_D ( ( c_!_0 : any ) ... ( c_i : any_i ) any_r ... ) ) ) ( name c_i c_!_0 ) )
#t ]
[ ( Δ-in-constructor-dom ( Δ ( D : any_D ( ( c_!_0 : any ) ... ) ) ) ( name c c_!_0 ) )
( Δ-in-constructor-dom Δ c ) ] )
;;; TODO: Might be worth maintaining the above bijection between Δ and maps for performance reasons
( define-metafunction ttL
Δ-ref-type : Δ_0 D_0 -> t
#:pre ( Δ-in-dom Δ_0 D_0 )
[ ( Δ-ref-type ( Δ ( D : t any ) ) D )
t ]
[ ( Δ-ref-type ( Δ ( D_!_0 : t any ) ) ( name D D_!_0 ) )
( Δ-ref-type Δ D ) ] )
;; Returns the inductively defined type that x constructs
;; TODO: This is doing too many things
;; NB: Depends on clause order
( define-metafunction ttL
Δ-key-by-constructor : Δ_0 c_0 -> D
#:pre ( Δ-in-constructor-dom Δ_0 c_0 )
[ ( Δ-key-by-constructor ( Δ ( D : any_D ( ( c_!_0 : any_c ) ... ( c : any_ci ) any_r ... ) ) ) ( name c c_!_0 ) )
D ]
[ ( Δ-key-by-constructor ( Δ ( D : any_D ( ( c_!_0 : any_c ) ... ) ) ) ( name c c_!_0 ) )
( Δ-key-by-constructor Δ c ) ] )
;; Returns the constructor map for the inductively defined type D in the signature Δ
( define-metafunction ttL
Δ-ref-constructor-map : Δ_0 D_0 -> ( ( c : t ) ... )
#:pre ( Δ-in-dom Δ_0 D_0 )
[ ( Δ-ref-constructor-map ( Δ ( D : any_D any ) ) D )
any ]
[ ( Δ-ref-constructor-map ( Δ ( D_!_0 : any_D any ) ) ( name D D_!_0 ) )
( Δ-ref-constructor-map Δ D ) ] )
;; Return the type of the constructor c_i
( define-metafunction ttL
Δ-ref-constructor-type : Δ_0 c_0 -> t
#:pre ( Δ-in-constructor-dom Δ_0 c_0 )
[ ( Δ-ref-constructor-type Δ c )
t
( where D ( Δ-key-by-constructor Δ c ) )
( where ( any_1 ... ( c : t ) any_0 ... )
( Δ-ref-constructor-map Δ D ) ) ] )
Δ-ref-type : Δ x -> t or #f
[ ( Δ-ref-type ∅ x ) #f ]
[ ( Δ-ref-type ( Δ ( x : t any ) ) x ) t ]
[ ( Δ-ref-type ( Δ ( x_0 : t_0 ( ( x_1 : t_1 ) ... ( x : t ) ( x_2 : t_2 ) ... ) ) ) x ) t ]
[ ( Δ-ref-type ( Δ ( x_0 : t_0 any ) ) x ) ( Δ-ref-type Δ x ) ] )
( define-metafunction ttL
Δ-ref-constructors : Δ_0 D_0 -> ( c ... )
#:pre ( Δ-in-dom Δ_0 D_0 )
[ ( Δ-ref-constructors Δ D )
( c ... )
( where ( ( c : any ) ... ) ( Δ-ref-constructor-map Δ D ) ) ] )
Δ-set : Δ x t ( ( x : t ) ... ) -> Δ
[ ( Δ-set Δ x t any ) ( Δ ( x : t any ) ) ] )
( define-metafunction ttL
Δ-union : Δ Δ -> Δ
[ ( Δ-union Δ ∅ ) Δ ]
[ ( Δ-union Δ_2 ( Δ_1 ( x : t any ) ) )
( ( Δ-union Δ_2 Δ_1 ) ( x : t any ) ) ] )
;; TODO: Should not use Δ-ref-type
( define-metafunction ttL
Δ-ref-constructor-type : Δ x x -> t
[ ( Δ-ref-constructor-type Δ x_D x_ci )
( Δ-ref-type Δ x_ci ) ] )
;; Get the list of constructors for the inducitvely defined type x_D
;; NB: Depends on clause order
( define-metafunction ttL
Δ-ref-constructors : Δ x -> ( x ... ) or #f
[ ( Δ-ref-constructors ∅ x_D ) #f ]
[ ( Δ-ref-constructors ( Δ ( x_D : t_D ( ( x : t ) ... ) ) ) x_D )
( x ... ) ]
[ ( Δ-ref-constructors ( Δ ( x_1 : t_1 any ) ) x_D )
( Δ-ref-constructors Δ x_D ) ] )
;; TODO: Mix of pure Redex/escaping to Racket sometimes is getting confusing.
;; TODO: Justify, or stop.
;; NB: Depends on clause order
( define-metafunction ttL
sequence-index-of : any ( any ... ) -> natural
[ ( sequence-index-of any_0 ( any_0 any ... ) )
0 ]
[ ( sequence-index-of ( name any_0 any_!_0 ) ( any_!_0 any ... ) )
[ ( sequence-index-of any_0 ( any_1 any ... ) )
, ( add1 ( term ( sequence-index-of any_0 ( any ... ) ) ) ) ] )
;; Get the index of the constructor c_i
;; Get the index of the constructor x_ci in the list of constructors for x_D
( define-metafunction ttL
Δ-constructor-index : Δ_0 c_0 -> natural
#:pre ( Δ-in-constructor-dom Δ_0 c_0 )
[ ( Δ-constructor-index Δ c )
( sequence-index-of c ( Δ-ref-constructors Δ D ) )
( where D ( Δ-key-by-constructor Δ c ) ) ] )
Δ-constructor-index : Δ x x -> natural
[ ( Δ-constructor-index Δ x_D x_ci )
( sequence-index-of x_ci ( Δ-ref-constructors Δ x_D ) ) ] )
;;; ------------------------------------------------------------------------
;;; Operations that involve contexts.
@ -163,15 +152,31 @@
;; NB: There is a bijection between this an a vector expressions
( Θ ::= hole ( Θ e ) ) )
( define Ξ? ( redex-match? tt-ctxtL Ξ ) )
( define Φ? ( redex-match? tt-ctxtL Φ ) )
( define Θ? ( redex-match? tt-ctxtL Θ ) )
;; TODO: Might be worth it to actually maintain the above bijections, for performance reasons.
;; Applies the term t to the telescope Ξ.
;; TODO: Test
#| TODO:
| This essentially eta-expands t at the type-level. Why is this necessary? Shouldn ' t it be true
| that ( convert t ( Ξ-apply Ξ t ) ) ?
| Maybe not. t is a lambda whose type is convert to ( Ξ-apply Ξ t ) ? Yes.
| #
( define-metafunction tt-ctxtL
Ξ-apply : Ξ t -> t
[ ( Ξ-apply hole t ) t ]
[ ( Ξ-apply ( Π ( x : t ) Ξ ) t_0 ) ( Ξ-apply Ξ ( t_0 x ) ) ] )
;; Compute the number of arguments in a Ξ
( define-metafunction tt-ctxtL
Ξ-length : Ξ -> natural
[ ( Ξ-length hole ) 0 ]
[ ( Ξ-length ( Π ( x : t ) Ξ ) ) , ( add1 ( term ( Ξ-length Ξ ) ) ) ] )
( define-metafunction tt-ctxtL
list->Θ : ( e ... ) -> Θ
[ ( list->Θ ( ) ) hole ]
@ -183,101 +188,115 @@
[ ( apply e_f e ... )
( in-hole ( list->Θ ( e ... ) ) e_f ) ] )
;; Reference an expression in Θ by index; index 0 corresponds to the the expression applied to a hole.
( define-metafunction tt-ctxtL
Θ-ref : Θ natural -> e or #f
[ ( Θ-ref hole natural ) #f ]
[ ( Θ-ref ( in-hole Θ ( hole e ) ) 0 ) e ]
[ ( Θ-ref ( in-hole Θ ( hole e ) ) natural ) ( Θ-ref Θ , ( sub1 ( term natural ) ) ) ] )
;;; ------------------------------------------------------------------------
;;; Computing the types of eliminators
;; Return the indices of D as a telescope Ξ
;; Return the parameters of x_D as a telescope Ξ
;; TODO: Define generic traversals of Δ and Γ ?
( define-metafunction tt-ctxtL
Δ-ref-index-Ξ : Δ_0 D_0 -> Ξ
#:pre ( Δ-in-dom Δ_0 D_0 )
[ ( Δ-ref-index-Ξ any_Δ any_D )
Ξ
( where ( in-hole Ξ U ) ( Δ-ref-type any_Δ any_D ) ) ] )
Δ-ref-parameter-Ξ : Δ x -> Ξ or #f
[ ( Δ-ref-parameter-Ξ ( Δ ( x_D : ( in-hole Ξ U ) any ) ) x_D )
Ξ ]
[ ( Δ-ref-parameter-Ξ ( Δ ( x_1 : t_1 any ) ) x_D )
( Δ-ref-parameter-Ξ Δ x_D ) ]
[ ( Δ-ref-parameter-Ξ Δ x )
#f ] )
;; Returns the telescope of the arguments for the constructor c_i of the inductively defined type D
;; Returns the telescope of the arguments for the constructor x_ ci of the inductively defined type x_ D
( define-metafunction tt-ctxtL
Δ-constructor-telescope : Δ_0 c_0 -> Ξ
#:pre ( Δ-in-constructor-dom Δ_0 c_0 )
[ ( Δ-constructor-telescope Δ c )
Δ-constructor-telescope : Δ x x -> Ξ
[ ( Δ-constructor-telescope Δ x_D x_ci )
Ξ
( where D ( Δ-key-by-constructor Δ c ) )
( where ( in-hole Ξ ( in-hole Θ D ) )
( Δ-ref-constructor-type Δ c ) ) ] )
( where ( in-hole Ξ ( in-hole Θ x_D ) )
( Δ-ref-constructor-type Δ x_D x_ci ) ) ] )
;; Returns the index arguments as an apply context of the constructor c_ i of the inductively
;; defined type D
;; Returns the parameter arguments as an apply context of the constructor x_ ci of the inductively
;; defined type x_ D
( define-metafunction tt-ctxtL
Δ-constructor-indices : Δ_0 c_0 -> Θ
#:pre ( Δ-in-constructor-dom Δ_0 c_0 )
[ ( Δ-constructor-indices Δ c )
Δ-constructor-parameters : Δ x x -> Θ
[ ( Δ-constructor-parameters Δ x_D x_ci )
Θ
( where D ( Δ-key-by-constructor Δ c ) )
( where ( in-hole Ξ ( in-hole Θ D ) )
( Δ-ref-constructor-type Δ c ) ) ] )
( where ( in-hole Ξ ( in-hole Θ x_D ) )
( Δ-ref-constructor-type Δ x_D x_ci ) ) ] )
;; Fold over the telescope Φ building a new telescope with only arguments of type D
;; Inner loop for Δ-constructor-inductive-telescope
;; NB: Depends on clause order
( define-metafunction tt-ctxtL
inductive-loop : D Φ -> Φ
[ ( inductive-loop hole ) hole ]
[ ( inductive-loop ( Π ( x : ( in-hole Φ ( in-hole Θ ) ) ) Φ_1 ) )
( Π ( x : ( in-hole Φ ( in-hole Θ ) ) ) ( inductive-loop Φ_1 ) ) ]
[ ( inductive-loop ( Π ( x : t ) Φ_1 ) )
( inductive-loop Φ_1 ) ] )
inductive-loop : x Φ -> Φ
[ ( inductive-loop x_ D hole ) hole ]
[ ( inductive-loop x_ D ( Π ( x : ( in-hole Φ ( in-hole Θ x_ D) ) ) Φ_1 ) )
( Π ( x : ( in-hole Φ ( in-hole Θ x_ D) ) ) ( inductive-loop x_ D Φ_1 ) ) ]
[ ( inductive-loop x_ D ( Π ( x : t ) Φ_1 ) )
( inductive-loop x_ D Φ_1 ) ] )
;; Returns the inductive arguments to the constructor c_i
;; Returns the inductive arguments to the constructor x_ci of the inducitvely defined type x_D
( define-metafunction tt-ctxtL
Δ-constructor-inductive-telescope : Δ_0 c_0 -> Ξ
#:pre ( Δ-in-constructor-dom Δ_0 c_0 )
[ ( Δ-constructor-inductive-telescope Δ c )
( inductive-loop D ( Δ-constructor-telescope Δ c ) )
( where D ( Δ-key-by-constructor Δ c ) ) ] )
Δ-constructor-inductive-telescope : Δ x x -> Ξ
[ ( Δ-constructor-inductive-telescope Δ x_D x_ci )
( inductive-loop x_D ( Δ-constructor-telescope Δ x_D x_ci ) ) ] )
;; Fold over the telescope Φ computing a new telescope with all
;; inductive arguments of type D modified to an inductive hypotheses
;; computed from the motive t.
;; Returns the inductive hypotheses required for eliminating the inductively defined type x_D with
;; motive t_P, where the telescope Φ are the inductive arguments to a constructor for x_D
( define-metafunction tt-ctxtL
hypotheses-loop : D t Φ -> Φ
[ ( hypotheses-loop D t_P hole ) hole ]
[ ( hypotheses-loop D t_P ( name any_0 ( Π ( x : ( in-hole Φ ( in-hole Θ D ) ) ) Φ_1 ) ) )
hypotheses-loop : x t Φ -> Φ
[ ( hypotheses-loop x_D t_P hole ) hole ]
[ ( hypotheses-loop x_D t_P ( name any_0 ( Π ( x : ( in-hole Φ ( in-hole Θ x_D ) ) ) Φ_1 ) ) )
;; TODO: Instead of this nonsense, it might be simpler to pass in the type of t_P and use that
;; as/to compute the type of the hypothesis.
( Π ( x_h : ( in-hole Φ ( ( in-hole Θ t_P ) ( Ξ-apply Φ x ) ) ) )
( hypotheses-loop D t_P Φ_1 ) )
( where x_h , ( variable-not-in ( term ( D t_P any_0 ) ) ' x-ih ) ) ] )
( hypotheses-loop x_D t_P Φ_1 ) )
( where x_h , ( variable-not-in ( term ( x_D t_P any_0 ) ) ' x-ih ) ) ] )
;; 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
;; Returns the inductive hypotheses required for the elimination method of constructor c_i for
;; inductive type D, when eliminating with motive t_P.
( define-metafunction tt-ctxtL
Δ-constructor-inductive-hypotheses : Δ_0 c_0 t -> Ξ
#:pre ( Δ-in-constructor-dom Δ_0 c_0 )
[ ( Δ-constructor-inductive-hypotheses Δ c_i t_P )
( hypotheses-loop D t_P ( Δ-constructor-inductive-telescope Δ c_i ) )
( where D ( Δ-key-by-constructor Δ c_i ) ) ] )
Δ-constructor-inductive-hypotheses : Δ D c t -> Ξ
[ ( Δ-constructor-inductive-hypotheses Δ D c_i t_P )
( hypotheses-loop D t_P ( Δ-constructor-inductive-telescope Δ D c_i ) ) ] )
;; Returns the type of the method corresponding to c_i
( define-metafunction tt-ctxtL
Δ-constructor-method-type : Δ_0 c_0 t -> t
#:pre ( Δ-in-constructor-dom Δ_0 c_0 )
[ ( Δ-constructor-method-type Δ c_i t_P )
Δ-constructor-method-type : Δ D c t -> t
[ ( Δ-constructor-method-type Δ D c_i t_P )
( in-hole Ξ_a ( in-hole Ξ_h ( ( in-hole Θ_p t_P ) ( Ξ-apply Ξ_a c_i ) ) ) )
( where Θ_p ( Δ-constructor- indices Δ c_i ) )
( where Ξ_a ( Δ-constructor-telescope Δ ) )
( where Ξ_h ( Δ-constructor-inductive-hypotheses Δ t_P ) ) ] )
( where Θ_p ( Δ-constructor- parameters Δ D c_i ) )
( where Ξ_a ( Δ-constructor-telescope Δ D c_i) )
( where Ξ_h ( Δ-constructor-inductive-hypotheses Δ D c_i t_P ) ) ] )
;; Return the types of the methods required to eliminate D with motive e
( define-metafunction tt-ctxtL
Δ-method-types : Δ_0 D_0 e -> ( t ... )
#:pre ( Δ-in-dom Δ_0 D_0 )
Δ-method-types : Δ D e -> ( t ... )
[ ( Δ-method-types Δ D e )
, ( map ( lambda ( c ) ( term ( Δ-constructor-method-type Δ , c e ) ) ) ( term ( c ... ) ) )
, ( map ( lambda ( c ) ( term ( Δ-constructor-method-type Δ D , c e ) ) ) ( term ( c ... ) ) )
( where ( c ... ) ( Δ-ref-constructors Δ D ) ) ] )
;; Return the type of the motive to eliminate D
( define-metafunction tt-ctxtL
Δ-motive-type : Δ_0 D_0 U -> t
#:pre ( Δ-in-dom Δ_0 D_0 )
Δ-motive-type : Δ D U -> t
[ ( Δ-motive-type Δ D U )
( in-hole Ξ_P*D U )
( where Ξ ( Δ-ref- index -Ξ Δ D ) )
( where Ξ ( Δ-ref- parameter -Ξ Δ D ) )
;; A fresh name to bind the discriminant
( where x , ( variable-not-in ( term ( Δ D Ξ ) ) ' x-D ) )
;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
@ -291,22 +310,51 @@
;;; inductively defined type x with a motive whose result is in universe U
( define-extended-language tt-redL tt-ctxtL
( C-elim ::= ( elim D t_P ( e_i ... ) ( e_m ... ) hole ) ) )
( v ::= x U ( Π ( x : t ) t ) ( λ ( x : t ) t ) ( in-hole Θv c ) )
( Θv ::= hole ( Θv v ) )
( C-elim ::= ( elim D t_P ( e_i ... ) ( e_m ... ) hole ) )
;; call-by-value
( E ::= hole ( E e ) ( v E )
( elim D e ( e ... ) ( v ... E e ... ) e )
( elim D e ( e ... ) ( v ... ) E )
;; reduce under Π (helps with typing checking)
;; TODO: Should be done in conversion judgment
( Π ( x : v ) E ) ( Π ( x : E ) e ) ) )
( define Θv? ( redex-match? tt-redL Θv ) )
( define E? ( redex-match? tt-redL E ) )
( define v? ( redex-match? tt-redL v ) )
#|
| The elim form must appear applied like so:
| ( elim D U v_P m_0 ... m_i m_j ... m_n p ... ( c_i a ... ) )
|
| Where:
| D is the inductive being eliminated
| U is the universe of the result of the motive
| v_P is the motive
| m_ { 0..n } are the methods
| p ... are the parameters of x_D
| c_i is a constructor of x_d
| a ... are the arguments to c_i
|
| Using contexts , this appears as ( in-hole Θ ( ( elim D U ) v_P ) )
| #
( define-metafunction tt-ctxtL
is-inductive-argument : Δ_0 D_0 t -> #t or #f
#:pre ( Δ-in-dom Δ_0 D_0 )
is-inductive-argument : Δ D t -> #t or #f
;; Think this only works in call-by-value. A better solution would
;; be to check position of the argument w.r.t. the current
;; method. requires more arguments, and more though.q
[ ( is-inductive-argument Δ D ( in-hole Θ c_i ) )
, ( and ( memq ( term c_i ) ( term ( Δ-ref-constructors Δ D ) ) ) #t ) ] )
;; Generate recursive applications of the eliminator for each inductive argument in Θ.
;; Generate recursive applications of the eliminator for each inductive argument of type x_D.
;; In more detail, given motive t_P, parameters Θ_p, methods Θ_m, and arguments Θ_i to constructor
;; x_ci for x_D, for each inductively smaller term t_i of type (in-hole Θ_p x_D) inside Θ_i,
;; generate: (elim x_D U t_P Θ_m ... Θ_p ... t_i)
;; TODO TTEESSSSSTTTTTTTT
( define-metafunction tt-redL
Δ-inductive-elim : Δ_0 D_0 C-elim Θ -> Θ
#:pre ( Δ-in-dom Δ_0 D_0 )
Δ-inductive-elim : Δ D C-elim Θ -> Θ
;; NB: If metafunction fails, recursive
;; NB: elimination will be wrong. This will introduced extremely sublte bugs,
;; NB: inconsistency, failure of type safety, and other bad things.
@ -320,70 +368,33 @@
[ ( Δ-inductive-elim any ... ( Θ_c t_i ) )
( Δ-inductive-elim any ... Θ_c ) ] )
#|
| The elim form must appear applied like so:
| ( elim D v_P ( i ... ) ( m_0 ... m_i m_j ... m_n ) ( c_i a ... ) )
|
| Where:
| D is the inductive being eliminated
| v_P is the motive
| m_ { 0..n } are the methods
| i ... are the indices of D
| c_i is a constructor of D
| a ... are the arguments to c_i
|
| Steps to ( m_i a ... ih ... ) , where ih are computed from the recursive arguments to c_i
| #
( define ( tt--> D )
( term-let ( [ Δ D ] )
( reduction-relation tt-redL
( --> ( ( λ ( x : t_0 ) t_1 ) t_2 )
( subst t_1 x t_2 )
-->β )
( --> ( elim D e_motive ( e_i ... ) ( e_m ... ) ( in-hole Θ_c c ) )
( in-hole Θ_mi e_mi )
( side-condition ( term ( Δ-in-constructor-dom Δ c ) ) )
;; Find the method for constructor c_i, relying on the order of the arguments.
( where natural ( Δ-constructor-index Δ c ) )
( where e_mi , ( list-ref ( term ( e_m ... ) ) ( term natural ) ) )
;; Generate the inductive recursion
( where Θ_ih ( Δ-inductive-elim Δ D ( elim D e_motive ( e_i ... ) ( e_m ... ) hole ) Θ_c ) )
( where Θ_mi ( in-hole Θ_ih Θ_c ) )
-->elim ) ) ) )
( define tt-->
( reduction-relation tt-redL
( --> ( Δ ( in-hole E ( ( λ ( x : t_0 ) t_1 ) t_2 ) ) )
( Δ ( in-hole E ( subst t_1 x t_2 ) ) )
-->β )
( --> ( Δ ( in-hole E ( elim D e_motive ( e_i ... ) ( v_m ... ) ( in-hole Θv_c c ) ) ) )
( Δ ( in-hole E ( in-hole Θ_mi v_mi ) ) )
;; Find the method for constructor c_i, relying on the order of the arguments.
( where natural ( Δ-constructor-index Δ D c ) )
( where v_mi , ( list-ref ( term ( v_m ... ) ) ( term natural ) ) )
;; Generate the inductive recursion
( where Θ_ih ( Δ-inductive-elim Δ D ( elim D e_motive ( e_i ... ) ( v_m ... ) hole ) Θv_c ) )
( where Θ_mi ( in-hole Θ_ih Θv_c ) )
-->elim ) ) )
( define-extended-language tt-cbvL tt-redL
;; NB: Not exactly right; only true when c is a constructor
( v ::= x U ( Π ( x : t ) t ) ( λ ( x : t ) t ) ( in-hole Θv c ) )
( Θv ::= hole ( Θv v ) )
( E ::= hole ( E e ) ( v E )
( elim D e ( e ... ) ( v ... E e ... ) e )
( elim D e ( e ... ) ( v ... ) E )
;; NB: These seem necessary, despite fixed conversion relation.
( Π ( x : E ) e ) ( Π ( x : v ) E ) ) )
( define-extended-language tt-cbnL tt-cbvL
( E ::= hole ( E e ) ( elim D e ( e ... ) ( e ... ) E ) ) )
( define-extended-language tt-head-redL tt-cbvL
( C-λ ::= Θ ( λ ( x : t ) C-λ ) )
( λv ::= x U ( Π ( x : t ) t ) ( elim D e ( e ... ) ( e ... ) ( in-hole C-λ x ) ) )
( v ::= ( in-hole C-λ λv ) ) )
;; Lazyness has lots of implications, such as on conversion and test suite.
( define ( tt-->cbn D ) ( context-closure ( tt--> D ) tt-cbnL E ) )
;; NB: Note that CIC specifies reduction via "contextual closure".
;; Perhaps they mean compatible-closure. Unfortunately, it's too slow.
( define ( tt-->full D ) ( compatible-closure ( tt--> D ) tt-redL e ) )
;; Head reduction
( define ( tt-->head-red D ) ( context-closure ( tt--> D ) tt-head-redL C-λ ) )
;; CBV, plus under Π
( define ( tt-->cbv D ) ( context-closure ( tt--> D ) tt-cbvL E ) )
( define-metafunction tt-redL
step : Δ e -> e
[ ( step Δ e )
e_r
( where ( _ e_r ) , ( car ( apply-reduction-relation tt--> ( term ( Δ e ) ) ) ) ) ] )
( define-metafunction tt-redL
reduce : Δ e -> e
[ ( reduce Δ e )
, ( car ( apply-reduction-relation* ( tt-->cbv ( term Δ ) ) ( term e ) #:cache-all? #t ) ) ] )
e_r
( where ( _ e_r )
, ( car ( apply-reduction-relation* tt--> ( term ( Δ e ) ) #:cache-all? #t ) ) ) ] )
;;; ------------------------------------------------------------------------
;;; Type checking and synthesis
@ -392,54 +403,49 @@
;; 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 Γ ) )
( define-judgment-form tt-typingL
#:mode ( convert I I I I )
#:contract ( convert Δ Γ t t )
[ ----------------- " ≡-Base "
( convert Δ Γ t t ) ]
[ ( where ( t_!_0 ... ) ( t_0 t_1 ) )
( where ( t t ) ( ( reduce Δ t_0 ) ( reduce Δ t_1 ) ) )
----------------- " ≡-Normal "
( convert Δ Γ t_0 t_1 ) ] )
( define-judgment-form tt-typingL
#:mode ( subtype I I I I )
#:contract ( subtype Δ Γ t t )
[ ( convert Δ Γ t_0 t_1 )
------------- " ≼-≡ "
( subtype Δ Γ t_0 t_1 ) ]
[ ( side-condition , ( <= ( term i_0 ) ( term i_1 ) ) )
----------------- " ≼-Unv "
( subtype Δ Γ ( Unv i_0 ) ( Unv i_1 ) ) ]
( convert Δ Γ ( Unv i_0 ) ( Unv i_1 ) ) ]
[ ( convert Δ Γ t_0 t_1 )
( subtype Δ ( Γ x_0 : t_0 ) e_0 ( subst e_1 x_1 x_0 ) )
[ ( where t_2 ( reduce Δ t_0 ) )
( where t_3 ( reduce Δ t_1 ) )
( side-condition ( α t_2 t_3 ) )
----------------- " ≼-αβ "
( convert Δ Γ t_0 t_1 ) ]
[ ( convert Δ ( Γ x : t_0 ) t_1 t_2 )
----------------- " ≼-Π "
( subtype Δ Γ ( Π ( x_0 : t_0 ) e_0 ) ( Π ( x_1 : t_1 ) e_1 ) ) ] )
( convert Δ Γ ( Π ( x : t_0 ) t_1 ) ( Π ( x : t_0 ) t_2 ) ) ] )
( define-metafunction tt-typingL
Γ-in-dom : Γ x -> #t or #f
[ ( Γ-in-dom ∅ x )
#f ]
[ ( Γ-in-dom ( Γ x : t ) x )
#t ]
[ ( Γ-in-dom ( Γ x_!_0 : t ) ( name x x_!_0 ) )
( Γ-in-dom Γ x ) ] )
Γ-union : Γ Γ -> Γ
[ ( Γ-union Γ ∅ ) Γ ]
[ ( Γ-union Γ_2 ( Γ_1 x : t ) )
( ( Γ-union Γ_2 Γ_1 ) x : t ) ] )
( define-metafunction tt-typingL
Γ-ref : Γ_0 x_0 -> t
#:pre ( Γ-in-dom Γ_0 x_0 )
[ ( Γ-ref ( Γ x : t ) x )
t ]
[ ( Γ-ref ( Γ x_!_0 : t_0 ) ( name x_1 x_!_0 ) )
( Γ-ref Γ x_1 ) ] )
Γ-set : Γ x t -> Γ
[ ( Γ-set Γ x t ) ( Γ x : t ) ] )
;; TODO: After reading https://coq.inria.fr/doc/Reference-Manual006.html#sec209, not convinced this is right.
;; NB: Depends on clause order
( define-metafunction tt-typingL
Γ-ref : Γ x -> t or #f
[ ( Γ-ref ∅ x ) #f ]
[ ( Γ-ref ( Γ x : t ) x ) t ]
[ ( Γ-ref ( Γ x_0 : t_0 ) x_1 ) ( Γ-ref Γ x_1 ) ] )
;; NB: Depends on clause order
( define-metafunction tt-typingL
Γ-remove : Γ x -> Γ
[ ( Γ-remove ∅ x ) ∅ ]
[ ( Γ-remove ( Γ x : t ) x ) Γ ]
[ ( Γ-remove ( Γ x_0 : t_0 ) x_1 ) ( Γ-remove Γ x_1 ) ] )
( define-metafunction tt-typingL
nonpositive : x t -> #t or #f
@ -461,44 +467,39 @@
, ( and ( term ( nonpositive x t_0 ) ) ( term ( positive x t ) ) ) ]
[ ( positive x t ) #t ] )
;; 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
#:mode ( valid I )
#:contract ( valid Δ )
[ -------- " Valid-Empty "
( valid ∅ ) ]
[ ( valid Δ )
( type-infer Δ ∅ t_D U_D )
( valid-constructor D t_c ) ...
( type-infer Δ ( ∅ D : t_D ) t_c U_c ) ...
----------------- " Valid-Inductive "
( valid ( Δ ( D : t_D ( ( c : t_c ) ... ) ) ) ) ] )
( define-metafunction tt-typingL
positive* : x ( t ... ) -> #t or #f
[ ( positive* x_D ( ) ) #t ]
[ ( positive* x_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 x_D ( in-hole Ξ ( Unv 0 ) ) ) ) ( term ( positive* x_D ( t_rest ... ) ) ) )
( where ( in-hole Ξ ( in-hole Θ x_D ) ) t_c ) ] )
;; Holds when the signature Δ and typing context Γ are well-formed.
( define-judgment-form tt-typingL
#:mode ( wf I I )
#:contract ( wf Δ Γ )
[ ( valid Δ )
----------------- " WF-Empty "
( wf Δ ∅ ) ]
[ ----------------- " WF-Empty "
( wf ∅ ∅ ) ]
[ ( type-infer Δ Γ t t_0 )
( wf Δ Γ )
----------------- " WF-Var "
( wf Δ ( Γ x : t ) ) ] )
( wf Δ ( Γ x : t ) ) ]
[ ( wf Δ ∅ )
( type-infer Δ ∅ t_D U_D )
( type-infer Δ ( ∅ x_D : t_D ) t_c U_c ) ...
;; NB: Ugh this should be possible with pattern matching alone ....
( side-condition , ( map ( curry equal? ( term x_D ) ) ( term ( x_D* ... ) ) ) )
( side-condition ( positive* x_D ( t_c ... ) ) )
----------------- " WF-Inductive "
( wf ( Δ ( x_D : t_D
;; 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 Ξ ( in-hole Θ x_D* ) ) ) ) ... ) ) ) ∅ ) ] )
;; TODO: Bi-directional and inference?
;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
@ -513,36 +514,28 @@
----------------- " DTR-Unv "
( type-infer Δ Γ U_0 U_1 ) ]
[ ( side-condition ( Δ-in-dom Δ x ) )
( where t ( Δ-ref-type Δ x ) )
( wf Δ Γ )
[ ( where t ( Δ-ref-type Δ x ) )
----------------- " DTR-Inductive "
( type-infer Δ Γ x t ) ]
[ ( side-condition ( Δ-in-constructor-dom Δ x ) )
( where t ( Δ-ref-constructor-type Δ x ) )
( wf Δ Γ )
----------------- " DTR-Constructor "
( type-infer Δ Γ x t ) ]
[ ( side-condition ( Γ-in-dom Γ x ) )
( where t ( Γ-ref Γ x ) )
( wf Δ Γ )
[ ( where t ( Γ-ref Γ x ) )
----------------- " DTR-Start "
( type-infer Δ Γ x t ) ]
[ ( type-infer -normal Δ ( Γ x : t_0 ) e t_1 )
( type-infer -normal Δ Γ ( Π ( x : t_0 ) t_1 ) U )
[ ( type-infer Δ ( Γ x : t_0 ) e t_1 )
( type-infer Δ Γ ( Π ( x : t_0 ) t_1 ) U )
----------------- " DTR-Abstraction "
( type-infer Δ Γ ( λ ( x : t_0 ) e ) ( Π ( x : t_0 ) t_1 ) ) ]
[ ( type-infer -normal Δ Γ t_0 U_1 )
( type-infer -normal Δ ( Γ x : t_0 ) t U_2 )
[ ( type-infer Δ Γ t_0 U_1 )
( type-infer Δ ( Γ x : t_0 ) t U_2 )
( unv-pred U_1 U_2 U )
----------------- " DTR-Product "
( type-infer Δ Γ ( Π ( x : t_0 ) t ) U ) ]
[ ( type-infer-normal Δ Γ e_0 ( Π ( x_0 : t_0 ) t_1 ) )
[ ( type-infer Δ Γ e_0 t )
;; Cannot rely on type-infer producing normal forms.
( where ( Π ( x_0 : t_0 ) t_1 ) ( reduce Δ t ) )
( type-check Δ Γ e_1 t_0 )
( where t_3 ( subst t_1 x_0 e_1 ) )
----------------- " DTR-Application "
@ -550,32 +543,20 @@
[ ( type-check Δ Γ e_c ( apply D e_i ... ) )
( type-infer -normal Δ Γ e_motive ( name t_motive ( in-hole Ξ U ) ) )
( subtype Δ Γ t_motive ( Δ-motive-type Δ D U ) )
( type-infer Δ Γ e_motive ( name t_motive ( in-hole Ξ U ) ) )
( convert Δ Γ t_motive ( Δ-motive-type Δ D U ) )
( where ( t_m ... ) ( Δ-method-types Δ D e_motive ) )
( type-check Δ Γ e_m t_m ) ...
----------------- " DTR-Elim_D "
( type-infer Δ Γ ( elim D e_motive ( e_i ... ) ( e_m ... ) e_c )
( apply e_motive e_i ... e_c ) ) ] )
;; Try to keep types in normal form, which simplifies a few things
( define-judgment-form tt-typingL
#:mode ( type-infer-normal I I I O )
#:contract ( type-infer-normal Δ Γ e t )
[ ( type-infer Δ Γ e t )
----------------- " DTR-Red "
( type-infer-normal Δ Γ e ( reduce Δ t ) ) ] )
( define-judgment-form tt-typingL
#:mode ( type-check I I I I )
#:contract ( type-check Δ Γ e t )
[ ( type-infer Δ Γ e t_0 )
( type-infer Δ Γ t U )
( subtype Δ Γ t t_0 )
( convert Δ Γ t t_0 )
----------------- " DTR-Check "
( type-check Δ Γ e t ) ] )