cur-lib/cur/curnel/redex-core-api.rkt

@@ -1,65 +0,0 @@
-#lang racket/base
-
-;; Additional API utilities for interacting with the core, but aren't necessary for the model of the core language.
-(require
- (except-in
-  "redex-core.rkt"
-  apply)
-  redex/reduction-semantics)
-
-(provide
- (all-from-out "redex-core.rkt")
- (all-defined-out))
-
-(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 Δ))
-(define Γ? (redex-match? tt-typingL Γ))
-(define Ξ? (redex-match? tt-ctxtL Ξ))
-(define Φ? (redex-match? tt-ctxtL Φ))
-(define Θ? (redex-match? tt-ctxtL Θ))
-(define Θv? (redex-match? tt-cbvL Θv))
-(define E? (redex-match? tt-cbvL E))
-(define v? (redex-match? tt-cbvL v))
-
-(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 ...))])
-
-(define-metafunction ttL
-  Δ-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))])
-
-(define-metafunction tt-redL
-  step : Δ e -> e
-  [(step Δ e)
-   ,(car (apply-reduction-relation (tt-->cbv (term Δ)) (term e)))])
-
-(define-metafunction tt-typingL
-  Γ-union : Γ Γ -> Γ
-  [(Γ-union Γ ∅) Γ]
-  [(Γ-union Γ_2 (Γ_1 x : t))
-   ((Γ-union Γ_2 Γ_1) x : t)])
-
-(define-metafunction tt-typingL
-  Γ-set : Γ x t -> Γ
-  [(Γ-set Γ x t) (Γ x : t)])
-
-;; 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)])
-
-

cur-lib/cur/curnel/redex-core.rkt

@@ -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)
+  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e)
-     ;; TODO: Might make more sense for methods to come first
      ;; (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
+  α-equivalent?  : t t -> #t or #f
+  [(α-equivalent? 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
+  Δ-ref-type : Δ x -> t or #f
-  #:pre (Δ-in-constructor-dom Δ_0 c_0)
+  [(Δ-ref-type ∅ x) #f]
-  [(Δ-key-by-constructor (Δ (D : any_D ((c_!_0 : any_c) ... (c : any_ci) any_r ...))) (name c c_!_0))
+  [(Δ-ref-type (Δ (x : t any)) x) t]
-   D]
+  [(Δ-ref-type (Δ (x_0 : t_0 ((x_1 : t_1) ... (x : t) (x_2 : t_2) ...))) x) t]
-  [(Δ-key-by-constructor (Δ (D : any_D ((c_!_0 : any_c) ...))) (name c c_!_0))
+  [(Δ-ref-type (Δ (x_0 : t_0 any)) x) (Δ-ref-type Δ x)])
-   (Δ-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))])
 
 (define-metafunction ttL
-  Δ-ref-constructors : Δ_0 D_0 -> (c ...)
+  Δ-set : Δ x t ((x : t) ...) -> Δ
-  #:pre (Δ-in-dom Δ_0 D_0)
+  [(Δ-set Δ x t any) (Δ (x : t any))])
-  [(Δ-ref-constructors Δ D)
+
-   (c ...)
+(define-metafunction ttL
-   (where ((c : any) ...) (Δ-ref-constructor-map Δ D))])
+  Δ-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
+  Δ-constructor-index : Δ x x -> natural
-  #:pre (Δ-in-constructor-dom Δ_0 c_0)
+  [(Δ-constructor-index Δ x_D x_ci)
-  [(Δ-constructor-index Δ c)
+   (sequence-index-of x_ci (Δ-ref-constructors Δ x_D))])
-   (sequence-index-of c (Δ-ref-constructors Δ D))
-   (where D (Δ-key-by-constructor Δ c))])
 
 ;;; ------------------------------------------------------------------------
 ;;; 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 -> Ξ
+  Δ-ref-parameter-Ξ : Δ x -> Ξ or #f
-  #:pre (Δ-in-dom Δ_0 D_0)
+  [(Δ-ref-parameter-Ξ (Δ (x_D : (in-hole Ξ U) any)) x_D)
-  [(Δ-ref-index-Ξ any_Δ any_D)
+   Ξ]
-   Ξ
+  [(Δ-ref-parameter-Ξ (Δ (x_1 : t_1 any)) x_D)
-   (where (in-hole Ξ U) (Δ-ref-type any_Δ any_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 -> Ξ
+  Δ-constructor-telescope : Δ x x -> Ξ
-  #:pre (Δ-in-constructor-dom Δ_0 c_0)
+  [(Δ-constructor-telescope Δ x_D x_ci)
-  [(Δ-constructor-telescope Δ c)
    Ξ
-   (where D (Δ-key-by-constructor Δ c))
+   (where (in-hole Ξ (in-hole Θ x_D))
-   (where (in-hole Ξ (in-hole Θ D))
+     (Δ-ref-constructor-type Δ x_D x_ci))])
-     (Δ-ref-constructor-type Δ c))])
 
-;; Returns the index arguments as an apply context of the constructor c_i of the inductively
+;; Returns the parameter arguments as an apply context of the constructor x_ci of the inductively
-;; defined type D
+;; defined type x_D
 (define-metafunction tt-ctxtL
-  Δ-constructor-indices : Δ_0 c_0 -> Θ
+  Δ-constructor-parameters : Δ x x -> Θ
-  #:pre (Δ-in-constructor-dom Δ_0 c_0)
+  [(Δ-constructor-parameters Δ x_D x_ci)
-  [(Δ-constructor-indices Δ c)
    Θ
-   (where D (Δ-key-by-constructor Δ c))
+   (where (in-hole Ξ (in-hole Θ x_D))
-   (where (in-hole Ξ (in-hole Θ D))
+     (Δ-ref-constructor-type Δ x_D x_ci))])
-     (Δ-ref-constructor-type Δ c))])
 
-;; 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 : x Φ -> Φ
-  [(inductive-loop D hole) hole]
+  [(inductive-loop x_D hole) hole]
-  [(inductive-loop D (Π (x : (in-hole Φ (in-hole Θ D))) Φ_1))
+  [(inductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
-   (Π (x : (in-hole Φ (in-hole Θ D))) (inductive-loop D Φ_1))]
+   (Π (x : (in-hole Φ (in-hole Θ x_D))) (inductive-loop x_D Φ_1))]
-  [(inductive-loop D (Π (x : t) Φ_1))
+  [(inductive-loop x_D (Π (x : t) Φ_1))
-   (inductive-loop D Φ_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 -> Ξ
+  Δ-constructor-inductive-telescope : Δ x x -> Ξ
-  #:pre (Δ-in-constructor-dom Δ_0 c_0)
+  [(Δ-constructor-inductive-telescope Δ x_D x_ci)
-  [(Δ-constructor-inductive-telescope Δ c)
+   (inductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
-   (inductive-loop D (Δ-constructor-telescope Δ c))
-   (where D (Δ-key-by-constructor Δ c))])
 
-;; Fold over the telescope Φ computing a new telescope with all
+;; Returns the inductive hypotheses required for eliminating the inductively defined type x_D with
-;; inductive arguments of type D modified to an inductive hypotheses
+;; motive t_P, where the telescope Φ are the inductive arguments to a constructor for x_D
-;; computed from the motive t.
 (define-metafunction tt-ctxtL
-  hypotheses-loop : D t Φ -> Φ
+  hypotheses-loop : x t Φ -> Φ
-  [(hypotheses-loop D t_P hole) hole]
+  [(hypotheses-loop x_D t_P hole) hole]
-  [(hypotheses-loop D t_P (name any_0 (Π (x : (in-hole Φ (in-hole Θ D))) Φ_1)))
+  [(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))
+      (hypotheses-loop x_D t_P Φ_1))
-   (where x_h ,(variable-not-in (term (D t_P any_0)) 'x-ih))])
+   (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 -> Ξ
+  Δ-constructor-inductive-hypotheses : Δ D c t -> Ξ
-  #:pre (Δ-in-constructor-dom Δ_0 c_0)
+  [(Δ-constructor-inductive-hypotheses Δ D c_i t_P)
-  [(Δ-constructor-inductive-hypotheses Δ c_i t_P)
+   (hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ D c_i))])
-   (hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ c_i))
-   (where D (Δ-key-by-constructor Δ c_i))])
 
 ;; Returns the type of the method corresponding to c_i
 (define-metafunction tt-ctxtL
-  Δ-constructor-method-type : Δ_0 c_0 t -> t
+  Δ-constructor-method-type : Δ D c t -> t
-  #:pre (Δ-in-constructor-dom Δ_0 c_0)
+  [(Δ-constructor-method-type Δ D c_i t_P)
-  [(Δ-constructor-method-type Δ 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 Θ_p (Δ-constructor-parameters Δ D c_i))
-   (where Ξ_a (Δ-constructor-telescope Δ c_i))
+   (where Ξ_a (Δ-constructor-telescope Δ D c_i))
-   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ c_i t_P))])
+   (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 ...)
+  Δ-method-types : Δ D e -> (t ...)
-  #:pre (Δ-in-dom Δ_0 D_0)
   [(Δ-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
+  Δ-motive-type : Δ D U -> t
-  #:pre (Δ-in-dom Δ_0 D_0)
   [(Δ-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
+  is-inductive-argument : Δ D t -> #t or #f
-  #:pre (Δ-in-dom Δ_0 D_0)
   ;; 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 Θ -> Θ
+  Δ-inductive-elim : Δ D C-elim Θ -> Θ
-  #:pre (Δ-in-dom Δ_0 D_0)
   ;; 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)])
 
-#|
+(define tt-->
- | The elim form must appear applied like so:
+  (reduction-relation tt-redL
- | (elim D v_P (i ...) (m_0 ... m_i m_j ... m_n) (c_i a ...))
+    (--> (Δ (in-hole E ((λ (x : t_0) t_1) t_2)))
- |
+         (Δ (in-hole E (subst t_1 x t_2)))
- | Where:
+         -->β)
- |   D       is the inductive being eliminated
+    (--> (Δ (in-hole E (elim D e_motive (e_i ...) (v_m ...) (in-hole Θv_c c))))
- |   v_P       is the motive
+         (Δ (in-hole E (in-hole Θ_mi v_mi)))
- |   m_{0..n}  are the methods
+         ;; Find the method for constructor c_i, relying on the order of the arguments.
- |   i ...     are the indices of D
+         (where natural (Δ-constructor-index Δ D c))
- |   c_i       is a constructor of D
+         (where v_mi ,(list-ref (term (v_m ...)) (term natural)))
- |   a ...     are the arguments to c_i
+         ;; Generate the inductive recursion
- |
+         (where Θ_ih (Δ-inductive-elim Δ D (elim D e_motive (e_i ...) (v_m ...) hole) Θv_c))
- | Steps to (m_i a ... ih ...), where ih are computed from the recursive arguments to c_i
+         (where Θ_mi (in-hole Θ_ih Θv_c))
- |#
+         -->elim)))
-(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-extended-language tt-cbvL tt-redL
+(define-metafunction tt-redL
-  ;; NB: Not exactly right; only true when c is a constructor
+  step : Δ e -> e
-  (v  ::= x U (Π (x : t) t) (λ (x : t) t) (in-hole Θv c))
+  [(step Δ e)
-  (Θv ::= hole (Θv v))
+   e_r
-  (E  ::= hole (E e) (v E)
+   (where (_ e_r) ,(car (apply-reduction-relation tt--> (term (Δ 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
   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)
+  [(where t_2 (reduce Δ t_0))
-   (subtype Δ (Γ x_0 : t_0) e_0 (subst e_1 x_1 x_0))
+   (where t_3 (reduce Δ t_1))
+   (side-condition (α-equivalent? 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
+  Γ-union : Γ Γ -> Γ
-  [(Γ-in-dom ∅ x)
+  [(Γ-union Γ ∅) Γ]
-   #f]
+  [(Γ-union Γ_2 (Γ_1 x : t))
-  [(Γ-in-dom (Γ x : t) x)
+   ((Γ-union Γ_2 Γ_1) x : t)])
-   #t]
-  [(Γ-in-dom (Γ x_!_0 : t) (name x x_!_0))
-   (Γ-in-dom Γ x)])
 
 (define-metafunction tt-typingL
-  Γ-ref : Γ_0 x_0 -> t
+  Γ-set : Γ x t -> Γ
-  #:pre (Γ-in-dom Γ_0 x_0)
+  [(Γ-set Γ x t) (Γ x : t)])
-  [(Γ-ref (Γ x : t) x)
-   t]
-  [(Γ-ref (Γ x_!_0 : t_0) (name x_1 x_!_0))
-   (Γ-ref Γ x_1)])
 
-;; 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-metafunction tt-typingL
-(define-judgment-form tt-typingL
+  positive* : x (t ...) -> #t or #f
-  #:mode (valid-constructor I I)
+  [(positive* x_D ()) #t]
-  #:contract (valid-constructor 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
-  ;; NB TODO: Ignore the "positive" occurrence of D in the result; this is hacky way to do this
+   ;; nonpositive position.
-  [(side-condition (positive D (in-hole Ξ (Unv 0))))
+   ,(and (term (positive x_D (in-hole Ξ (Unv 0)))) (term (positive* x_D (t_rest ...))))
-   ---------------------------------------------------------
+   (where (in-hole Ξ (in-hole Θ x_D)) t_c)])
-   (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) ...))))])
 
 ;; 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-Empty"
+   (wf ∅ ∅)]
-   (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))
-   (where t (Δ-ref-type Δ x))
-   (wf Δ Γ)
    ----------------- "DTR-Inductive"
    (type-infer Δ Γ x t)]
 
-  [(side-condition (Δ-in-constructor-dom Δ x))
+  [(where t (Γ-ref Γ x))
-   (where t (Δ-ref-constructor-type Δ x))
-   (wf Δ Γ)
-   ----------------- "DTR-Constructor"
-   (type-infer Δ Γ x t)]
-
-  [(side-condition (Γ-in-dom Γ x))
-   (where t (Γ-ref Γ x))
-   (wf Δ Γ)
    ----------------- "DTR-Start"
    (type-infer Δ Γ x t)]
 
-  [(type-infer-normal Δ (Γ x : t_0) e t_1)
+  [(type-infer Δ (Γ x : t_0) e t_1)
-   (type-infer-normal Δ Γ (Π (x : t_0) t_1) U)
+   (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 Δ Γ t_0 U_1)
-   (type-infer-normal Δ (Γ x : t_0) t U_2)
+   (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)))
+   (type-infer Δ Γ e_motive (name t_motive (in-hole Ξ U)))
-   (subtype Δ Γ t_motive (Δ-motive-type Δ D 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)
+   (convert Δ Γ t t_0)
-   (subtype Δ Γ t t_0)
    ----------------- "DTR-Check"
    (type-check Δ Γ e t)])
-

cur-lib/cur/curnel/redex-lang.rkt

@@ -2,7 +2,7 @@
 ;; This module just provide module language sugar over the redex model.
 
 (require
-  "redex-core-api.rkt"
+  (except-in "redex-core.rkt" apply)
   redex/reduction-semantics
   racket/provide-syntax
   (for-syntax
@@ -11,7 +11,7 @@
     racket/syntax
     (except-in racket/provide-transform export)
     racket/require-transform
-    "redex-core-api.rkt"
+    (except-in "redex-core.rkt" apply)
     redex/reduction-semantics))
 (provide
   ;; Basic syntax
@@ -273,9 +273,8 @@
   (define (cur-identifier-bound? id)
     (let ([x (syntax->datum id)])
       (and (x? x)
-        (or (term (Γ-in-dom ,(gamma) ,x))
+        (or (term (Γ-ref ,(gamma) ,x))
-            (term (Δ-in-dom ,(delta) ,x))
+          (term (Δ-ref-type ,(delta) ,x))))))
-            (term (Δ-in-constructor-dom ,(delta) ,x))))))
 
   (define (filter-cur-exports syn modes)
     (partition (compose cur-identifier-bound? export-local-id)

cur-test/cur/tests/redex-core.rkt

@@ -1,7 +1,7 @@
 #lang racket/base
 (require
  redex/reduction-semantics
- cur/curnel/redex-core-api
+ cur/curnel/redex-core
  rackunit
  racket/function
  (only-in racket/set set=?))
@@ -16,9 +16,7 @@
 (define-syntax-rule (check-not-equiv? e1 e2)
   (check (compose not (default-equiv)) e1 e2))
 
-(default-equiv (curry alpha-equivalent? ttL))
+(default-equiv (lambda (x y) (term (α-equivalent? ,x ,y))))
-
-(check-redundancy #t)
 
 ;; Syntax tests
 ;; ------------------------------------------------------------------------
@@ -75,10 +73,13 @@
 (check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B))))))
 
 
-;; alpha-equivalent and subst tests
+;; α-equiv and subst tests
-(check-equiv?
+;; ------------------------------------------------------------------------
- (term (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))
+(check-true
- (term (Π (a : S) (Π (b : B) ((and S) B)))))
+ (term
+  (α-equivalent?
+   (Π (a : S) (Π (b : B) ((and S) B)))
+   (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
 
 ;; Telescope tests
 ;; ------------------------------------------------------------------------
@@ -91,10 +92,10 @@
   (check (compose not telescope-equiv) e1 e2))
 
 (check-telescope-equiv?
- (term (Δ-ref-index-Ξ ,Δ nat))
+ (term (Δ-ref-parameter-Ξ ,Δ nat))
  (term hole))
 (check-telescope-equiv?
- (term (Δ-ref-index-Ξ ,Δ4 and))
+ (term (Δ-ref-parameter-Ξ ,Δ4 and))
  (term (Π (A : Type) (Π (B : Type) hole))))
 
 (check-true (x? (term false)))
@@ -104,7 +105,7 @@
 
 ;; Tests for inductive elimination
 ;; ------------------------------------------------------------------------
-;; TODO: Insufficient tests, no tests of inductives with indices, or complex induction.
+;; TODO: Insufficient tests, no tests of inductives with parameters, or complex induction.
 (check-true
  (redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
 (check-telescope-equiv?
@@ -153,7 +154,7 @@
 (check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
                   (term (Π (x : t) (x x))))
 
-(check-equal? (term (Δ-constructor-index ,Δ zero)) 0)
+(check-equal? (term (Δ-constructor-index ,Δ nat zero)) 0)
 (check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
                                      ()
                                      ((s zero)
@@ -216,7 +217,7 @@
           zero)))))
 
 (define-syntax-rule (check-equivalent e1 e2)
-  (check-holds (subtype ∅ ∅ e1 e2)))
+  (check-holds (convert ∅ ∅ e1 e2)))
 (check-equivalent
  (λ (x : Type) x) (λ (y : Type) y))
 (check-equivalent
@@ -225,26 +226,19 @@
 ;; Test static semantics
 ;; ------------------------------------------------------------------------
 
-(check-holds
+(check-true (term (positive* nat (nat))))
- (valid-constructor nat nat))
+(check-true (term (positive* nat ((Π (x : (Unv 0)) (Π (y : (Unv 0)) nat))))))
-(check-holds
+(check-true (term (positive* nat ((Π (x : nat) nat)))))
- (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-not-holds
+(check-false (term (positive* nat ((Π (x : (Π (y : nat) nat)) nat)))))
- (valid-constructor nat (Π (x : (Π (y : nat) nat)) nat)))
 ;; ((Unv 0) -> nat) -> nat
-(check-holds
+(check-true (term (positive* nat ((Π (x : (Π (y : (Unv 0)) nat)) nat)))))
- (valid-constructor nat (Π (x : (Π (y : (Unv 0)) nat)) nat)))
 ;; (((nat -> (Unv 0)) -> nat) -> nat)
-(check-holds
+(check-true (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) (Unv 0))) nat)) nat)))))
- (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-not-holds
+(check-false (term (positive* nat ((Π (x : (Π (y : (Π (x : nat) nat)) nat)) nat)))))
- (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))))
@@ -287,8 +281,7 @@
 (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-holds (valid-constructor nat nat))
+(check-true (term (positive* nat (nat (Π (x : nat) nat)))))
-(check-holds (valid-constructor nat (Π (x : nat) nat)))
 (check-holds
  (wf (∅ (nat : (Unv 0) ((zero : nat)))) ∅))
 (check-holds
@@ -338,13 +331,12 @@
 
 (check-holds (type-check ,Δtruth ∅ (λ (x : truth) (Unv 1)) (Π (x : truth) (Unv 2))))
 
-(require (only-in cur/curnel/redex-core apply))
 (check-equiv?
  (term (apply (λ (x : truth) (Unv 1)) T))
  (term ((λ (x : truth) (Unv 1)) T)))
 
 (check-holds
- (subtype ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1)))
+ (convert ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1)))
 
 (check-holds (type-infer ,Δtruth
                          ∅
@@ -509,7 +501,7 @@
                                            ((and B) A))))
              (in-hole Ξ (Π (x : (in-hole Θ and)) U))))
 (check-holds
- (subtype ,Δ4 ∅
+ (convert ,Δ4 ∅
              (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))
              (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : ((and P) Q)) (Unv 0))))))
 (check-holds
@@ -650,7 +642,7 @@
   (term (((((hole
              (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true)))))
 (check-telescope-equiv?
- (term (Δ-ref-index-Ξ ,Δ= ==))
+ (term (Δ-ref-parameter-Ξ ,Δ= ==))
  (term (Π (A : Type) (Π (a : A) (Π (b : A) hole)))))
 (check-equal?
  (term (reduce ,Δ= ,refl-elim))