Trying to fix performance bugs with conversion

Previously, wf was serving double-duty checking that Γ was well-formed
w.r.t. Δ, and then checking that Δ was valid (i.e. satisfied
positivity conditions and such).

Now these are different judgments.

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

@@ -0,0 +1,65 @@
+#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,19 +28,14 @@
   (U ::= (Unv i))
   (D x c ::= variable-not-otherwise-mentioned)
   (Δ   ::= ∅ (Δ (D : t ((c : t) ...))))
-  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e)
+  (t e ::= U (λ (x : e) e) x (Π (x : e) e) (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
 
@@ -67,79 +62,95 @@
    ----------------
    (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
-
-;; TODO: This is doing too many things
-;; NB: Depends on clause order
 (define-metafunction ttL
-  Δ-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)])
+  Δ-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
+(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))])
 
 (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))])
-
-;; 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)])
+  Δ-ref-constructors : Δ_0 D_0 -> (c ...)
+  #:pre (Δ-in-dom Δ_0 D_0)
+  [(Δ-ref-constructors Δ D)
+   (c ...)
+   (where ((c : any) ...) (Δ-ref-constructor-map Δ 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 any_0 (any_1 any ...))
+  [(sequence-index-of (name any_0 any_!_0) (any_!_0 any ...))
    ,(add1 (term (sequence-index-of any_0 (any ...))))])
 
-;; Get the index of the constructor x_ci in the list of constructors for x_D
+;; Get the index of the constructor c_i
 (define-metafunction ttL
-  Δ-constructor-index : Δ x x -> natural
-  [(Δ-constructor-index Δ x_D x_ci)
-   (sequence-index-of x_ci (Δ-ref-constructors Δ x_D))])
+  Δ-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))])
 
 ;;; ------------------------------------------------------------------------
 ;;; Operations that involve contexts.
@@ -152,31 +163,15 @@
   ;; 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]
@@ -188,115 +183,101 @@
   [(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 parameters of x_D as a telescope Ξ
-;; TODO: Define generic traversals of Δ and Γ ?
+;; Return the indices of D as a telescope Ξ
 (define-metafunction tt-ctxtL
-  Δ-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 x_ci of the inductively defined type x_D
-(define-metafunction tt-ctxtL
-  Δ-constructor-telescope : Δ x x -> Ξ
-  [(Δ-constructor-telescope Δ x_D x_ci)
+  Δ-ref-index-Ξ : Δ_0 D_0 -> Ξ
+  #:pre (Δ-in-dom Δ_0 D_0)
+  [(Δ-ref-index-Ξ any_Δ any_D)
    Ξ
-   (where (in-hole Ξ (in-hole Θ x_D))
-     (Δ-ref-constructor-type Δ x_D x_ci))])
+   (where (in-hole Ξ U) (Δ-ref-type any_Δ any_D))])
 
-;; Returns the parameter arguments as an apply context of the constructor x_ci of the inductively
-;; defined type x_D
+;; Returns the telescope of the arguments for the constructor c_i of the inductively defined type D
 (define-metafunction tt-ctxtL
-  Δ-constructor-parameters : Δ x x -> Θ
-  [(Δ-constructor-parameters Δ x_D x_ci)
-   Θ
-   (where (in-hole Ξ (in-hole Θ x_D))
-     (Δ-ref-constructor-type Δ x_D x_ci))])
+  Δ-constructor-telescope : Δ_0 c_0 -> Ξ
+  #:pre (Δ-in-constructor-dom Δ_0 c_0)
+  [(Δ-constructor-telescope Δ c)
+   Ξ
+   (where D (Δ-key-by-constructor Δ c))
+   (where (in-hole Ξ (in-hole Θ D))
+     (Δ-ref-constructor-type Δ c))])
 
-;; Inner loop for Δ-constructor-inductive-telescope
+;; Returns the index arguments as an apply context of the constructor c_i of the inductively
+;; defined type D
+(define-metafunction tt-ctxtL
+  Δ-constructor-indices : Δ_0 c_0 -> Θ
+  #:pre (Δ-in-constructor-dom Δ_0 c_0)
+  [(Δ-constructor-indices Δ c)
+   Θ
+   (where D (Δ-key-by-constructor Δ c))
+   (where (in-hole Ξ (in-hole Θ D))
+     (Δ-ref-constructor-type Δ c))])
+
+;; Fold over the telescope Φ building a new telescope with only arguments of type D
 ;; NB: Depends on clause order
 (define-metafunction tt-ctxtL
-  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)])
+  inductive-loop : D Φ -> Φ
+  [(inductive-loop D hole) hole]
+  [(inductive-loop D (Π (x : (in-hole Φ (in-hole Θ D))) Φ_1))
+   (Π (x : (in-hole Φ (in-hole Θ D))) (inductive-loop D Φ_1))]
+  [(inductive-loop D (Π (x : t) Φ_1))
+   (inductive-loop D Φ_1)])
 
-;; Returns the inductive arguments to the constructor x_ci of the inducitvely defined type x_D
+;; Returns the inductive arguments to the constructor c_i
 (define-metafunction tt-ctxtL
-  Δ-constructor-inductive-telescope : Δ x x -> Ξ
-  [(Δ-constructor-inductive-telescope Δ x_D x_ci)
-   (inductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
+  Δ-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))])
 
-;; 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
+;; 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.
 (define-metafunction tt-ctxtL
-  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.
+  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)))
    (Π (x_h : (in-hole Φ ((in-hole Θ t_P) (Ξ-apply Φ x))))
-      (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
+      (hypotheses-loop D t_P Φ_1))
+   (where x_h ,(variable-not-in (term (D t_P any_0)) 'x-ih))])
 
 ;; 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 : Δ D c t -> Ξ
-  [(Δ-constructor-inductive-hypotheses Δ D c_i t_P)
-   (hypotheses-loop D t_P (Δ-constructor-inductive-telescope Δ D c_i))])
+  Δ-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))])
 
 ;; Returns the type of the method corresponding to c_i
 (define-metafunction tt-ctxtL
-  Δ-constructor-method-type : Δ D c t -> t
-  [(Δ-constructor-method-type Δ D c_i t_P)
+  Δ-constructor-method-type : Δ_0 c_0 t -> t
+  #:pre (Δ-in-constructor-dom Δ_0 c_0)
+  [(Δ-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-parameters Δ D c_i))
-   (where Ξ_a (Δ-constructor-telescope Δ D c_i))
-   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ D c_i t_P))])
+   (where Θ_p (Δ-constructor-indices Δ c_i))
+   (where Ξ_a (Δ-constructor-telescope Δ c_i))
+   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ c_i t_P))])
 
+;; Return the types of the methods required to eliminate D with motive e
 (define-metafunction tt-ctxtL
-  Δ-method-types : Δ D e -> (t ...)
+  Δ-method-types : Δ_0 D_0 e -> (t ...)
+  #:pre (Δ-in-dom Δ_0 D_0)
   [(Δ-method-types Δ D e)
-   ,(map (lambda (c) (term (Δ-constructor-method-type Δ D ,c e))) (term (c ...)))
+   ,(map (lambda (c) (term (Δ-constructor-method-type Δ ,c e))) (term (c ...)))
    (where (c ...) (Δ-ref-constructors Δ D))])
 
+;; Return the type of the motive to eliminate D
 (define-metafunction tt-ctxtL
-  Δ-motive-type : Δ D U -> t
+  Δ-motive-type : Δ_0 D_0 U -> t
+  #:pre (Δ-in-dom Δ_0 D_0)
   [(Δ-motive-type Δ D U)
    (in-hole Ξ_P*D U)
-   (where Ξ (Δ-ref-parameter-Ξ Δ D))
+   (where Ξ (Δ-ref-index-Ξ Δ 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.,
@@ -310,51 +291,22 @@
 ;;; inductively defined type x with a motive whose result is in universe U
 
 (define-extended-language tt-redL tt-ctxtL
-  (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)))
+  (C-elim  ::= (elim D t_P (e_i ...) (e_m ...) hole)))
 
-(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 : Δ D t -> #t or #f
+  is-inductive-argument : Δ_0 D_0 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 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)
+;; Generate recursive applications of the eliminator for each inductive argument in Θ.
 ;; TODO TTEESSSSSTTTTTTTT
 (define-metafunction tt-redL
-  Δ-inductive-elim : Δ D C-elim Θ -> Θ
+  Δ-inductive-elim : Δ_0 D_0 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.
@@ -368,33 +320,70 @@
   [(Δ-inductive-elim any ... (Θ_c t_i))
    (Δ-inductive-elim any ... Θ_c)])
 
-(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)))
+#|
+ | 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-metafunction tt-redL
-  step : Δ e -> e
-  [(step Δ e)
-   e_r
-   (where (_ e_r) ,(car (apply-reduction-relation tt--> (term (Δ e)))))])
+(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
   reduce : Δ e -> e
   [(reduce Δ e)
-   e_r
-   (where (_ e_r)
-          ,(car (apply-reduction-relation* tt--> (term (Δ e)) #:cache-all? #t)))])
+   ,(car (apply-reduction-relation* (tt-->cbv (term Δ)) (term e) #:cache-all? #t))])
 
 ;;; ------------------------------------------------------------------------
 ;;; Type checking and synthesis
@@ -403,49 +392,54 @@
   ;; 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"
-   (convert Δ Γ (Unv i_0) (Unv i_1))]
+   (subtype Δ Γ (Unv i_0) (Unv i_1))]
 
-  [(where t_2 (reduce Δ t_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)
+  [(convert Δ Γ t_0 t_1)
+   (subtype Δ (Γ x_0 : t_0) e_0 (subst e_1 x_1 x_0))
    ----------------- "≼-Π"
-   (convert Δ Γ (Π (x : t_0) t_1) (Π (x : t_0) t_2))])
+   (subtype Δ Γ (Π (x_0 : t_0) e_0) (Π (x_1 : t_1) e_1))])
 
 (define-metafunction tt-typingL
-  Γ-union : Γ Γ -> Γ
-  [(Γ-union Γ ∅) Γ]
-  [(Γ-union Γ_2 (Γ_1 x : t))
-   ((Γ-union Γ_2 Γ_1) x : t)])
+  Γ-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)])
 
 (define-metafunction tt-typingL
-  Γ-set : Γ x t -> Γ
-  [(Γ-set Γ x t) (Γ x : t)])
+  Γ-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)])
 
-;; 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)])
+;; TODO: After reading https://coq.inria.fr/doc/Reference-Manual006.html#sec209, not convinced this is right.
 
 (define-metafunction tt-typingL
   nonpositive : x t -> #t or #f
@@ -467,39 +461,44 @@
    ,(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* 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 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) ...))))])
 
 ;; Holds when the signature Δ and typing context Γ are well-formed.
 (define-judgment-form tt-typingL
   #:mode (wf I I)
   #:contract (wf Δ Γ)
 
-  [----------------- "WF-Empty"
-   (wf ∅ ∅)]
+  [(valid Δ)
+   ----------------- "WF-Empty"
+   (wf Δ ∅)]
 
   [(type-infer Δ Γ t t_0)
    (wf Δ Γ)
    ----------------- "WF-Var"
-   (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*)))) ...))) ∅)])
+   (wf Δ (Γ x : t))])
 
 ;; TODO: Bi-directional and inference?
 ;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
@@ -514,28 +513,36 @@
    ----------------- "DTR-Unv"
    (type-infer Δ Γ U_0 U_1)]
 
-  [(where t (Δ-ref-type Δ x))
+  [(side-condition (Δ-in-dom Δ x))
+   (where t (Δ-ref-type Δ x))
+   (wf Δ Γ)
    ----------------- "DTR-Inductive"
    (type-infer Δ Γ x t)]
 
-  [(where t (Γ-ref Γ x))
+  [(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 Δ Γ)
    ----------------- "DTR-Start"
    (type-infer Δ Γ x t)]
 
-  [(type-infer Δ (Γ x : t_0) e t_1)
-   (type-infer Δ Γ (Π (x : t_0) t_1) U)
+  [(type-infer-normal Δ (Γ x : t_0) e t_1)
+   (type-infer-normal Δ Γ (Π (x : t_0) t_1) U)
    ----------------- "DTR-Abstraction"
    (type-infer Δ Γ (λ (x : t_0) e) (Π (x : t_0) t_1))]
 
-  [(type-infer Δ Γ t_0 U_1)
-   (type-infer Δ (Γ x : t_0) t U_2)
+  [(type-infer-normal Δ Γ t_0 U_1)
+   (type-infer-normal Δ (Γ x : t_0) t U_2)
    (unv-pred U_1 U_2 U)
    ----------------- "DTR-Product"
    (type-infer Δ Γ (Π (x : t_0) t) U)]
 
-  [(type-infer Δ Γ e_0 t)
-   ;; Cannot rely on type-infer producing normal forms.
-   (where (Π (x_0 : t_0) t_1) (reduce Δ t))
+  [(type-infer-normal Δ Γ e_0 (Π (x_0 : t_0) t_1))
    (type-check Δ Γ e_1 t_0)
    (where t_3 (subst t_1 x_0 e_1))
    ----------------- "DTR-Application"
@@ -543,20 +550,32 @@
 
   [(type-check Δ Γ e_c (apply D e_i ...))
 
-   (type-infer Δ Γ e_motive (name t_motive (in-hole Ξ U)))
-   (convert Δ Γ t_motive (Δ-motive-type Δ D U))
+   (type-infer-normal Δ Γ e_motive (name t_motive (in-hole Ξ U)))
+   (subtype Δ Γ 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)
-   (convert Δ Γ t t_0)
+   (type-infer Δ Γ t U)
+   (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
-  (except-in "redex-core.rkt" apply)
+  "redex-core-api.rkt"
   redex/reduction-semantics
   racket/provide-syntax
   (for-syntax
@@ -11,7 +11,7 @@
     racket/syntax
     (except-in racket/provide-transform export)
     racket/require-transform
-    (except-in "redex-core.rkt" apply)
+    "redex-core-api.rkt"
     redex/reduction-semantics))
 (provide
   ;; Basic syntax
@@ -273,8 +273,9 @@
   (define (cur-identifier-bound? id)
     (let ([x (syntax->datum id)])
       (and (x? x)
-        (or (term (Γ-ref ,(gamma) ,x))
-          (term (Δ-ref-type ,(delta) ,x))))))
+        (or (term (Γ-in-dom ,(gamma) ,x))
+            (term (Δ-in-dom ,(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
+ cur/curnel/redex-core-api
  rackunit
  racket/function
  (only-in racket/set set=?))
@@ -16,7 +16,9 @@
 (define-syntax-rule (check-not-equiv? e1 e2)
   (check (compose not (default-equiv)) e1 e2))
 
-(default-equiv (lambda (x y) (term (α-equivalent? ,x ,y))))
+(default-equiv (curry alpha-equivalent? ttL))
+
+(check-redundancy #t)
 
 ;; Syntax tests
 ;; ------------------------------------------------------------------------
@@ -73,13 +75,10 @@
 (check-true (t? (term (Π (a : A) (Π (b : B) ((and A) B))))))
 
 
-;; α-equiv and subst tests
-;; ------------------------------------------------------------------------
-(check-true
- (term
-  (α-equivalent?
-   (Π (a : S) (Π (b : B) ((and S) B)))
-   (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))))
+;; alpha-equivalent and subst tests
+(check-equiv?
+ (term (subst (Π (a : A) (Π (b : B) ((and A) B))) A S))
+ (term (Π (a : S) (Π (b : B) ((and S) B)))))
 
 ;; Telescope tests
 ;; ------------------------------------------------------------------------
@@ -92,10 +91,10 @@
   (check (compose not telescope-equiv) e1 e2))
 
 (check-telescope-equiv?
- (term (Δ-ref-parameter-Ξ ,Δ nat))
+ (term (Δ-ref-index-Ξ ,Δ nat))
  (term hole))
 (check-telescope-equiv?
- (term (Δ-ref-parameter-Ξ ,Δ4 and))
+ (term (Δ-ref-index-Ξ ,Δ4 and))
  (term (Π (A : Type) (Π (B : Type) hole))))
 
 (check-true (x? (term false)))
@@ -105,7 +104,7 @@
 
 ;; Tests for inductive elimination
 ;; ------------------------------------------------------------------------
-;; TODO: Insufficient tests, no tests of inductives with parameters, or complex induction.
+;; TODO: Insufficient tests, no tests of inductives with indices, or complex induction.
 (check-true
  (redex-match? tt-ctxtL (in-hole Θ_i (hole (in-hole Θ_r zero))) (term (hole zero))))
 (check-telescope-equiv?
@@ -154,7 +153,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 ,Δ nat zero)) 0)
+(check-equal? (term (Δ-constructor-index ,Δ zero)) 0)
 (check-equiv? (term (reduce ,Δ (elim nat (λ (x : nat) nat)
                                      ()
                                      ((s zero)
@@ -217,7 +216,7 @@
           zero)))))
 
 (define-syntax-rule (check-equivalent e1 e2)
-  (check-holds (convert ∅ ∅ e1 e2)))
+  (check-holds (subtype ∅ ∅ e1 e2)))
 (check-equivalent
  (λ (x : Type) x) (λ (y : Type) y))
 (check-equivalent
@@ -226,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))))
@@ -281,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
@@ -331,12 +338,13 @@
 
 (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
- (convert ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1)))
+ (subtype ,Δtruth ∅ (apply (λ (x : truth) (Unv 1)) T) (Unv 1)))
 
 (check-holds (type-infer ,Δtruth
                          ∅
@@ -501,7 +509,7 @@
                                            ((and B) A))))
              (in-hole Ξ (Π (x : (in-hole Θ and)) U))))
 (check-holds
- (convert ,Δ4 ∅
+ (subtype ,Δ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
@@ -642,7 +650,7 @@
   (term (((((hole
              (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true)))))
 (check-telescope-equiv?
- (term (Δ-ref-parameter-Ξ ,Δ= ==))
+ (term (Δ-ref-index-Ξ ,Δ= ==))
  (term (Π (A : Type) (Π (a : A) (Π (b : A) hole)))))
 (check-equal?
  (term (reduce ,Δ= ,refl-elim))