Added TODO; Δ depends on order, but dict unordered

* Ported the redex-core test-suite to hybrid-core. This test suite badly
  in need of abstraction.
* Tested and fixed the hybrid core; now runs

cur-lib/cur/cur.rkt

@@ -5,7 +5,7 @@
     racket/syntax
     syntax/parse
     (for-template
-      (only-in "curnel/redex-lang.rkt"
+      (only-in "curnel/hybrid-lang.rkt"
        cur-expand)))
 
   (provide cur-match)
@@ -17,7 +17,7 @@
            [pattern body] ...)])))
 
 (require
-  (rename-in "curnel/redex-lang.rkt" [provide -provide])
+  (rename-in "curnel/hybrid-lang.rkt" [provide -provide])
   (only-in racket/base eof)
   (for-syntax 'extra)
   'extra)
@@ -27,5 +27,5 @@
   (except-out
     (all-from-out
      'extra
-     "curnel/redex-lang.rkt")
+     "curnel/hybrid-lang.rkt")
     -provide))

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

@@ -0,0 +1,648 @@
+#lang racket/base
+
+;; A mostly Redex core, with parts written in Racket for performance reasons
+
+(require
+  racket/dict
+  racket/function
+  racket/list
+  redex/reduction-semantics)
+
+(provide
+  (all-defined-out))
+
+(set-cache-size! 10000)
+
+(define-language base
+  (dict ::= any))
+;; TODO: More abstractions for Redex dictionaries.
+
+(define make-dict make-immutable-hash)
+
+#| ttL is the core language of Cur. Very similar to TT (Idirs core) and Luo's UTT. Surface
+ | langauge should provide short-hand, such as -> for non-dependent function types, and type
+ | inference.
+ |#
+(define-extended-language ttL base
+  (i j k  ::= natural)
+  (U ::= (Unv i))
+  (t e ::= U (λ (x : t) e) x (Π (x : t) t) (e e) (elim D U))
+  (Δ   ::= dict)
+  (D x c ::= variable-not-otherwise-mentioned)
+  #: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))
+
+;; TODO: Constracts
+;; An inductive-decl contains the type of the type being declared,
+;; a t?, and a dictionary of constructor names (x?) mapped to their
+;; types (t?), the original syntax/order of the constructor
+;; declaration ((x : t) ...), and the list of constructors in the
+;; original order (x ...)
+(define-struct inductive-decl (type constr-dict constr-decl constr-ls) #:prefab)
+
+;; A Δ is a dict mapping names x? to inductive-decl?
+(define Δ? dict?)
+(define make-empty-Δ make-dict)
+(define empty-Δ? dict-empty?)
+
+;;; ------------------------------------------------------------------------
+;;; Universe typing
+
+(define-judgment-form ttL
+  #:mode (unv-type I O)
+  #:contract (unv-type U U)
+
+  [(where i_1 ,(add1 (term i_0)))
+   -----------------
+   (unv-type (Unv i_0) (Unv i_1))])
+
+;; Universe predicativity rules. Impredicative in (Unv 0)
+(define-judgment-form ttL
+  #:mode (unv-pred I I O)
+  #:contract (unv-pred U U U)
+
+  [----------------
+   (unv-pred (Unv i) (Unv 0) (Unv 0))]
+
+  [(where i_3 ,(max (term i_1) (term i_2)))
+   ----------------
+   (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: Maybe shouldn't fall back, but maintains redex-core interface.
+;; Get the type of x as declared in Δ, as either a constructor or an inductive type
+(define-metafunction ttL
+  Δ-ref-type : Δ x -> t or #f
+  [(Δ-ref-type Δ x)
+   ,(cond
+      [(dict-ref (term Δ) (term x) (thunk #f))
+       => inductive-decl-type]
+      [else (term (Δ-ref-constructor-type Δ foo x))])])
+
+;; Get the type of a constructor x in the inductive declaration Δ
+;; TODO: Doesn't need x_D anymore
+(define-metafunction ttL
+  Δ-ref-constructor-type : Δ x x -> t or #f
+  [(Δ-ref-constructor-type Δ x_D x)
+   ,(cond
+     [(for/or ([(D idecl) (in-dict (term Δ))])
+       (let ([constr-dict (inductive-decl-constr-dict idecl)])
+         (and (dict-has-key? constr-dict (term x)) constr-dict)))
+      =>
+      (curryr dict-ref (term x))]
+     [else #f])])
+
+;; Add an inductive declaration to Δ
+(define-metafunction ttL
+  Δ-set : Δ x t ((x : t) ...) -> Δ
+  [(Δ-set Δ x t (name decl ((c : t_c) ...)))
+   ,(dict-set
+     (term Δ)
+     (term x)
+     (inductive-decl
+      (term t)
+      (for/fold ([d (make-dict)])
+                ([constr-decl (term decl)])
+        (dict-set d (first constr-decl) (third constr-decl)))
+      (term decl)
+      (term (c ...))))])
+
+;; Merge two inductive declarations
+(define-metafunction ttL
+  Δ-union : Δ Δ -> Δ
+  [(Δ-union Δ_1 Δ_2)
+   ,(for/fold ([d (term Δ_1)])
+              ([(k v) (in-dict (term Δ_2))])
+      (dict-set d k v))])
+
+(define-metafunction ttL
+  Δ-set* : Δ (x t ((x : t) ...)) ... -> Δ
+  [(Δ-set* Δ) Δ]
+  [(Δ-set* Δ (D t_D ((c : t_c) ...)) any_r ...)
+   (Δ-set* (Δ-set Δ D t_D ((c : t_c) ...)) any_r ...)])
+
+;; Returns the inductively defined type that x constructs
+(define-metafunction ttL
+  Δ-key-by-constructor : Δ x -> x or #f
+  [(Δ-key-by-constructor Δ x_c)
+   ,(for/or ([(k v) (in-dict (term Δ))])
+      (and (dict-has-key? (inductive-decl-constr-dict v) (term x_c)) k))])
+
+;; Returns the constructor map for the inductively defined type x_D in the signature Δ
+(define-metafunction ttL
+  Δ-ref-constructor-map : Δ x -> ((x : t) ...) or #f
+  [(Δ-ref-constructor-map Δ x_D)
+   ,(cond
+      [(dict-ref (term Δ) (term x_D) (thunk #f)) =>
+       inductive-decl-constr-decl]
+      [else #f])])
+
+;; Get the list of constructors for the inducitvely defined type x_D
+(define-metafunction ttL
+  Δ-ref-constructors : Δ x -> (x ...) or #f
+  [(Δ-ref-constructors Δ x_D)
+   ,(inductive-decl-constr-ls (dict-ref (term Δ) (term x_D)))])
+
+;; 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 ...))
+   ,(add1 (term (sequence-index-of any_0 (any ...))))])
+
+;; Get the index of the constructor x_ci in the list of constructors for x_D
+(define-metafunction ttL
+  Δ-constructor-index : Δ x x -> natural
+  [(Δ-constructor-index Δ x_D x_ci)
+   (sequence-index-of x_ci (Δ-ref-constructors Δ x_D))])
+
+;;; ------------------------------------------------------------------------
+;;; Operations that involve contexts.
+
+(define-extended-language tt-ctxtL ttL
+  ;; Telescope.
+  ;; NB: There is a bijection between this an a vector of maps from x to t
+  (Ξ Φ ::= hole (Π (x : t) Ξ))
+  ;; Apply context
+  ;; 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.
+
+;; Return the parameters of x_D as a telescope Ξ
+(define-metafunction tt-ctxtL
+  Δ-ref-parameter-Ξ : Δ x -> Ξ
+  [(Δ-ref-parameter-Ξ Δ x_D)
+   Ξ
+   (where (in-hole Ξ U) (Δ-ref-type Δ x_D))])
+
+;; 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 (equivalent t (Ξ-apply Ξ t))?
+ | Maybe not. t is a lambda whose type is equivalent to (Ξ-apply Ξ t)? Yes.
+ |#
+(define-metafunction tt-ctxtL
+  Ξ-apply : Ξ t -> t
+  [(Ξ-apply hole t) t]
+  [(Ξ-apply (Π (x : t) Ξ) t_0) (Ξ-apply Ξ (t_0 x))])
+
+;; Compose multiple telescopes into a single telescope:
+(define-metafunction tt-ctxtL
+  Ξ-compose : Ξ Ξ ... -> Ξ
+  [(Ξ-compose Ξ) Ξ]
+  [(Ξ-compose Ξ_0 Ξ_1 Ξ_rest ...)
+   (Ξ-compose (in-hole Ξ_0 Ξ_1) Ξ_rest ...)])
+
+;; Compute the number of arguments in a Ξ
+(define-metafunction tt-ctxtL
+  Ξ-length : Ξ -> natural
+  [(Ξ-length hole) 0]
+  [(Ξ-length (Π (x : t) Ξ)) ,(add1 (term (Ξ-length Ξ)))])
+
+;; Compute the number of applications in a Θ
+(define-metafunction tt-ctxtL
+  Θ-length : Θ -> natural
+  [(Θ-length hole) 0]
+  [(Θ-length (Θ e)) ,(add1 (term (Θ-length Θ)))])
+
+;; 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
+
+;; 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)
+   Ξ
+   (where (in-hole Ξ (in-hole Θ x_D))
+     (Δ-ref-constructor-type Δ x_D x_ci))])
+
+;; 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-parameters : Δ x x -> Θ
+  [(Δ-constructor-parameters Δ x_D x_ci)
+   Θ
+   (where (in-hole Ξ (in-hole Θ x_D))
+     (Δ-ref-constructor-type Δ x_D x_ci))])
+
+;; Inner loop for Δ-constructor-noninductive-telescope
+(define-metafunction tt-ctxtL
+  noninductive-loop : x Φ -> Φ
+  [(noninductive-loop x_D hole) hole]
+  [(noninductive-loop x_D (Π (x : (in-hole Φ (in-hole Θ x_D))) Φ_1))
+   (noninductive-loop x_D Φ_1)]
+  [(noninductive-loop x_D (Π (x : t) Φ_1))
+   (Π (x : t) (noninductive-loop x_D Φ_1))])
+
+;; Returns the noninductive arguments to the constructor x_ci of the inductively defined type x_D
+(define-metafunction tt-ctxtL
+  Δ-constructor-noninductive-telescope : Δ x x -> Ξ
+  [(Δ-constructor-noninductive-telescope Δ x_D x_ci)
+   (noninductive-loop x_D (Δ-constructor-telescope Δ x_D x_ci))])
+
+;; Inner loop for Δ-constructor-inductive-telescope
+;; 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)])
+
+;; Returns the inductive arguments to the constructor x_ci of the inducitvely defined type x_D
+(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))])
+
+;; 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 : 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 x_D t_P Φ_1))
+   (where x_h ,(variable-not-in (term (x_D t_P any_0)) 'x-ih))])
+
+;; Returns the inductive hypotheses required for the elimination method of constructor x_ci for
+;; inductive type x_D, when eliminating with motive t_P.
+(define-metafunction tt-ctxtL
+  Δ-constructor-inductive-hypotheses : Δ x x t -> Ξ
+  [(Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P)
+   (hypotheses-loop x_D t_P (Δ-constructor-inductive-telescope Δ x_D x_ci))])
+
+(define-metafunction tt-ctxtL
+  Δ-constructor-method-telescope : Δ x x t -> Ξ
+  [(Δ-constructor-method-telescope Δ x_D x_ci t_P)
+   (Π (x_mi : (in-hole Ξ_a (in-hole Ξ_h ((in-hole Θ_p t_P) (Ξ-apply Ξ_a x_ci)))))
+      hole)
+   (where Θ_p (Δ-constructor-parameters Δ x_D x_ci))
+   (where Ξ_a (Δ-constructor-telescope Δ x_D x_ci))
+   (where Ξ_h (Δ-constructor-inductive-hypotheses Δ x_D x_ci t_P))
+   (where x_mi ,(variable-not-in (term (t_P Δ)) 'x-mi))])
+
+;; fold Ξ-compose over map Δ-constructor-method-telescope over the list of constructors
+(define-metafunction tt-ctxtL
+  method-loop : Δ x t (x ...) -> Ξ
+  [(method-loop Δ x_D t_P ()) hole]
+  [(method-loop Δ x_D t_P (x_0 x_rest ...))
+   (Ξ-compose (Δ-constructor-method-telescope Δ x_D x_0 t_P) (method-loop Δ x_D t_P (x_rest ...)))])
+
+;; Returns the telescope of all methods required to eliminate the type x_D with motive t_P
+(define-metafunction tt-ctxtL
+  Δ-methods-telescope : Δ x t -> Ξ
+  [(Δ-methods-telescope Δ x_D t_P)
+   (method-loop Δ x_D t_P (Δ-ref-constructors Δ x_D))])
+
+;; Computes the type of the eliminator for the inductively defined type x_D with a motive whose result
+;; is in universe U.
+;;
+;; The type of (elim x_D U) is something like:
+;;  (∀ (P : (∀ a -> ... -> (D a ...) -> U))
+;;     (method_ci ...) -> ... ->
+;;     (a -> ... -> (D a ...) ->
+;;       (P a ... (D a ...))))
+;;
+;; x_D   is an inductively defined type
+;; U     is the sort the motive
+;; x_P   is the name of the motive
+;; Ξ_P*D is the telescope of the parameters of x_D and
+;;       the witness of type x_D (applied to the parameters)
+;; Ξ_m   is the telescope of the methods for x_D
+(define-metafunction tt-ctxtL
+  Δ-elim-type : Δ x U -> t
+  [(Δ-elim-type Δ x_D U)
+   (Π (x_P : (in-hole Ξ_P*D U))
+      ;; The methods Ξ_m for each constructor of type x_D
+      (in-hole Ξ_m
+        ;; And finally, the parameters and discriminant
+        (in-hole Ξ_P*D
+          ;; The result is (P a ... (x_D a ...)), i.e., the motive
+          ;; applied to the paramters and discriminant
+          (Ξ-apply Ξ_P*D x_P))))
+   ;; Get the parameters of x_D
+   (where Ξ (Δ-ref-parameter-Ξ Δ x_D))
+   ;; A fresh name to bind the discriminant
+   (where x ,(variable-not-in (term (Δ Γ x_D Ξ)) 'x-D))
+   ;; The telescope (∀ a -> ... -> (D a ...) hole), i.e.,
+   ;; of the parameters and the inductive type applied to the
+   ;; parameters
+   (where Ξ_P*D (in-hole Ξ (Π (x : (Ξ-apply Ξ x_D)) hole)))
+   ;; A fresh name for the motive
+   (where x_P ,(variable-not-in (term (Δ Γ x_D Ξ Ξ_P*D x)) 'x-P))
+   ;; The types of the methods for this inductive.
+   (where Ξ_m (Δ-methods-telescope Δ x_D x_P))])
+
+;; TODO: This might belong in the next section, since it's related to evaluation
+;; Generate recursive applications of the eliminator for each inductive argument of type x_D.
+;; In more detaill, 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)
+(define-metafunction tt-ctxtL
+  Δ-inductive-elim : Δ x U t Θ Θ Θ -> Θ
+  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m (in-hole Θ_i (hole (name t_i (in-hole Θ_r x_ci)))))
+   ((Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_i)
+    (in-hole ((in-hole Θ_p Θ_m) t_i) ((elim x_D U) t_P)))
+   (side-condition (memq (term x_ci) (term (Δ-ref-constructors Δ x_D))))]
+  [(Δ-inductive-elim Δ x_D U t_P Θ_p Θ_m Θ_nr) hole])
+
+;;; ------------------------------------------------------------------------
+;;; Dynamic semantics
+;;; The majority of this section is dedicated to evaluation of (elim x U), the eliminator for the
+;;; inductively defined type x with a motive whose result is in universe U
+
+(define-extended-language tt-redL tt-ctxtL
+  ;; NB: (in-hole Θv (elim x U)) is only a value when it's a partially applied elim. However,
+  ;; determining whether or not it is partially applied cannot be done with the grammar alone.
+  (v   ::= x U (Π (x : t) t) (λ (x : t) t) (elim x U) (in-hole Θv x) (in-hole Θv (elim x U)))
+  (Θv  ::= hole (Θv v))
+  ;; call-by-value, plus reduce under Π (helps with typing checking)
+  (E   ::= hole (E e) (v E) (Π (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))
+
+(define current-Δ (make-parameter (make-empty-Δ)))
+(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 (in-hole Θv ((elim x_D U) v_P)))
+         (in-hole E (in-hole Θ_r (in-hole Θv_i v_mi)))
+         #|
+          | The elim form must appear applied like so:
+          | (elim x_D U v_P m_0 ... m_i m_j ... m_n p ... (c_i a ...))
+          |
+          | Where:
+          |   x_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
+          | Unfortunately, Θ contexts turn all this inside out:
+          | TODO: Write better abstractions for this notation
+          |#
+         (where Δ ,(current-Δ))
+         ;; Split Θv into its components: the paramters Θv_P for x_D, the methods Θv_m for x_D, and
+         ;; the discriminant: the constructor x_ci applied to its argument Θv_i
+         (where (in-hole (Θv_p (in-hole Θv_i x_ci)) Θv_m) Θv)
+         ;; Check that Θ_p actually matches the parameters of x_D, to ensure it doesn't capture other
+         ;; arguments.
+         (side-condition (equal? (term (Θ-length Θv_p)) (term (Ξ-length (Δ-ref-parameter-Ξ Δ x_D)))))
+         ;; Ensure x_ci is actually a constructor for x_D
+         (where (x_c* ...) (Δ-ref-constructors Δ x_D))
+         (side-condition (memq (term x_ci) (term (x_c* ...))))
+         ;; There should be a number of methods equal to the number of constructors; to ensure E
+         ;; doesn't capture methods and Θv_m doesn't capture other arguments
+         (side-condition (equal? (length (term (x_c* ...)))  (term (Θ-length Θv_m))))
+         ;; Find the method for constructor x_ci, relying on the order of the arguments.
+         (where v_mi (Θ-ref Θv_m (Δ-constructor-index Δ x_D x_ci)))
+         ;; Generate the inductive recursion
+         (where Θ_r (Δ-inductive-elim Δ x_D U v_P Θv_p Θv_m Θv_i))
+         -->elim)))
+
+(define reduce-memoize (make-hash))
+(define-metafunction tt-redL
+  step : Δ e -> e
+  [(step Δ e)
+   e_r
+   (where e_r ,(dict-ref reduce-memoize (term e)
+                         (thunk
+                          (parameterize ([current-Δ (term Δ)])
+                            (let ([x (car (apply-reduction-relation tt--> (term e)))])
+                              (dict-set! reduce-memoize (term e_r) x)
+                              x)))))])
+
+(define-metafunction tt-redL
+  reduce : Δ e -> e
+  [(reduce Δ e)
+   e_r
+   (where e_r ,(dict-ref reduce-memoize (term e)
+                         (thunk
+                          (parameterize ([current-Δ (term Δ)])
+                            (let ([x (car (apply-reduction-relation* tt--> (term e) #:cache-all? #t))])
+                              (dict-set! reduce-memoize (term e_r) x)
+                              x)))))])
+
+(define-judgment-form tt-redL
+  #:mode (equivalent I I I)
+  #:contract (equivalent Δ t t)
+
+  [(where t_2 (reduce Δ t_0))
+   (where t_3 (reduce Δ t_1))
+   (side-condition (α-equivalent? t_2 t_3))
+   ----------------- "≡-αβ"
+   (equivalent Δ t_0 t_1)])
+
+;;; ------------------------------------------------------------------------
+;;; Type checking and synthesis
+
+(define-extended-language tt-typingL tt-redL
+  ;; NB: There may be a bijection between Γ and Ξ. That's interesting.
+  ;; NB: Also a bijection between Γ and a list of maps from x to t.
+  (Γ   ::= ∅ (Γ x : t)))
+(define Γ? (redex-match? tt-typingL Γ))
+
+(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
+  Γ-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
+  [(nonpositive x (in-hole Θ x))
+   #t]
+  [(nonpositive x (Π (x_0 : (in-hole Θ x)) t))
+   #f]
+  [(nonpositive x (Π (x_0 : t_0) t))
+   ,(and (term (positive x t_0)) (term (nonpositive x t)))]
+  [(nonpositive x t) #t])
+
+(define-metafunction tt-typingL
+  positive : x t -> #t or #f
+  [(positive x (in-hole Θ x))
+   #f]
+  [(positive x (Π (x_0 : (in-hole Θ x)) t))
+   (positive x t)]
+  [(positive x (Π (x_0 : t_0) t))
+   ,(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 signature Δ and typing context Γ are well-formed.
+(define-judgment-form tt-typingL
+  #:mode (wf I I)
+  #:contract (wf Δ Γ)
+
+  [(side-condition ,(empty-Δ? (term Δ)))
+   ----------------- "WF-Empty"
+   (wf Δ ∅)]
+
+  [(type-infer Δ Γ t t_0)
+   (wf Δ Γ)
+   ----------------- "WF-Var"
+   (wf Δ (Γ x : t))]
+
+  [(side-condition ,(not (empty-Δ? (term Δ_1))))
+   ;; TODO: Depends on order, but "first" here is nondeterministic/unspecified
+   (where x_D ,(dict-iterate-key (term Δ_1) (dict-iterate-first (term Δ_1))))
+   (where t_D (Δ-ref-type Δ_1 x_D))
+   (where (x_c ...) (Δ-ref-constructors Δ_1 x_D))
+   (where ((name t_c (in-hole Ξ (in-hole Θ x_D*))) ...)
+          ((Δ-ref-type Δ_1 x_c) ...))
+   (where Δ ,(dict-remove (term Δ_1) (term x_D)))
+   (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 Δ_1 ∅)])
+
+;; TODO: Bi-directional and inference?
+;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
+
+;; Holds when e has type t under signature Δ and typing context Γ
+(define-judgment-form tt-typingL
+  #:mode (type-infer I I I O)
+  #:contract (type-infer Δ Γ e t)
+
+  [(wf Δ Γ)
+   (unv-type U_0 U_1)
+   ----------------- "DTR-Unv"
+   (type-infer Δ Γ U_0 U_1)]
+
+  [(wf Δ Γ)
+   (where t (Δ-ref-type Δ x))
+   ----------------- "DTR-Inductive"
+   (type-infer Δ Γ x t)]
+
+  [(wf Δ Γ)
+   (where t (Γ-ref Γ x))
+   ----------------- "DTR-Start"
+   (type-infer Δ Γ x t)]
+
+  [(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 Δ Γ 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 Δ Γ 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"
+   (type-infer Δ Γ (e_0 e_1) t_3)]
+
+  [(where t (Δ-elim-type Δ D U))
+   (type-infer Δ Γ t U_e)
+   ----------------- "DTR-Elim_D"
+   (type-infer Δ Γ (elim D U) t)])
+
+(define-judgment-form tt-typingL
+  #:mode (type-check I I I I)
+  #:contract (type-check Δ Γ e t)
+
+  [(type-infer Δ Γ e t_0)
+   (equivalent Δ t t_0)
+   ----------------- "DTR-Check"
+   (type-check Δ Γ e t)])
+
+
+(module+ test
+  (require rackunit)
+  (define-term Δt (Δ-set ,(make-empty-Δ) True (Unv 0) ((T : True))))
+  (check-false
+   (judgment-holds (type-check ,(make-empty-Δ) ∅ T True)))
+  (check-true
+   (judgment-holds (type-check Δt ∅ T True)))
+  (check-true
+   (judgment-holds (type-check Δt ∅ True (Unv 0))))
+  (check-true
+   (judgment-holds (wf Δt ∅)))
+  (check-true
+   (judgment-holds (wf Δt (∅ P : (Unv 0)))))
+  (check-true
+   (judgment-holds (type-infer Δt ∅ (Π (P : (Unv 0)) True) t))))

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

@@ -0,0 +1,493 @@
+#lang racket/base
+;; This module just provide module language sugar over the redex model.
+
+(require
+  "hybrid-core.rkt"
+  redex/reduction-semantics
+  racket/provide-syntax
+  (for-syntax
+    (except-in racket import)
+    syntax/parse
+    racket/syntax
+    (except-in racket/provide-transform export)
+    racket/require-transform
+    "hybrid-core.rkt"
+    redex/reduction-semantics))
+(provide
+  ;; Basic syntax
+  for-syntax
+  only-in
+  except-in
+  all-defined-out
+  rename-in
+  rename-out
+  prefix-out
+  prefix-in
+  submod
+  #%module-begin
+  (rename-out
+    [dep-module+ module+]
+    [dep-provide provide]
+    [dep-require require]
+
+    [dep-lambda lambda]
+    [dep-lambda λ]
+    [dep-app #%app]
+
+    [dep-forall forall]
+    [dep-forall ∀]
+
+    [dep-inductive data]
+
+    [dep-elim elim]
+
+    [dep-top #%top]
+    [dep-top-interaction #%top-interaction]
+
+    ;      [dep-datum #%datum]
+    [dep-define define]
+    [dep-void void])
+  begin
+  Type
+  ;; DYI syntax extension
+  define-syntax
+  begin-for-syntax
+  define-for-syntax
+  syntax-case
+  syntax-rules
+  define-syntax-rule
+  (for-syntax
+   (all-from-out syntax/parse)
+   (all-from-out racket)
+   (all-from-out racket/syntax)
+    cur->datum
+    cur-expand
+    type-infer/syn
+    type-check/syn?
+    normalize/syn
+    step/syn
+    cur-equal?))
+
+(begin-for-syntax
+  ;; TODO: Gamma and Delta seem to get reset inside a module+
+  (define gamma
+    (make-parameter
+      (term ∅)
+      (lambda (x)
+        (unless (Γ? x)
+          (error 'core-error "We built a bad term environment ~s" x))
+        x)))
+
+  (define delta
+    (make-parameter
+      (make-empty-Δ)
+      (lambda (x)
+        (unless (Δ? x)
+          (error 'core-error "We built a bad inductive declaration ~s" x))
+        x)))
+
+  ;; These should be provided by core, so details of envs can be hidden.
+  (define (extend-Γ/term env x t)
+    (term (Γ-set ,(env) ,x ,t)))
+
+  (define (extend-Γ/term! env x t) (env (extend-Γ/term env x t)))
+
+  (define (extend-Γ/syn env x t)
+    (extend-Γ/term env (syntax->datum x) (cur->datum t)))
+
+  (define (extend-Γ/syn! env x t) (env (extend-Γ/syn env x t)))
+
+  (define (extend-Δ/term env x t c*)
+    (term (Δ-set ,(env) ,x ,t (,@c*))))
+
+  (define (extend-Δ/term! env x t c*)
+    (env (extend-Δ/term env x t c*)))
+
+  (define (extend-Δ/syn env x t c*)
+    (extend-Δ/term env (syntax->datum x) (cur->datum t)
+                   (for/list ([c (syntax->list c*)])
+                     (syntax-case c ()
+                       [(c : ct)
+                        (parameterize ([gamma (extend-Γ/syn gamma x t)])
+                          (term (,(syntax->datum #'c) : ,(cur->datum #'ct))))]))))
+
+  (define (extend-Δ/syn! env x t c*)
+    (env (extend-Δ/syn env x t c*)))
+
+  (define subst? (list/c (listof x?)  (listof e?)))
+  (define bind-subst
+    (make-parameter
+     (list null null)
+     (lambda (x)
+       (unless (subst? x)
+           (error 'core-error "We build a bad subst ~s" x))
+       x)))
+
+  (define (add-binding/term! x t)
+    (let ([vars (first (bind-subst))]
+          [exprs (second (bind-subst))])
+      (bind-subst (list (cons x vars) (cons t exprs)))))
+
+  (define (subst-bindings t)
+    (term (subst-all ,t ,(first (bind-subst)) ,(second (bind-subst)))))
+
+  (define (type-infer/term t)
+    (let ([t (judgment-holds (type-infer ,(delta) ,(gamma) ,(subst-bindings t) t_0) t_0)])
+      (and (pair? t) (car t))))
+
+  (define (type-check/term? e t)
+    (and (judgment-holds (type-check ,(delta) ,(gamma) ,(subst-bindings e) ,(subst-bindings t))) #t))
+
+  ;; TODO: Blanket disarming is probably a bad idea.
+  (define orig-insp (variable-reference->module-declaration-inspector (#%variable-reference)))
+  (define (disarm syn) (syntax-disarm syn orig-insp))
+
+  ;; Locally expand everything down to core forms.
+  (define (core-expand syn)
+    (disarm
+      (local-expand
+        syn
+        'expression
+        (append (syntax-e #'(term reduce subst-all dep-top #%app λ Π elim Unv #%datum void))))))
+
+  ;; Only type-check at the top-level, to prevent exponential
+  ;; type-checking. Redex is expensive enough.
+  (define inner-expand? (make-parameter #f))
+
+  ;; Reifiy cur syntax into curnel datum
+  (define (cur->datum syn)
+    ;; Main loop; avoid type
+    (define reified-term
+      ;; TODO: This results in less good error messages. Add an
+      ;; algorithm to find the smallest ill-typed term.
+      (parameterize ([inner-expand? #t])
+        (let cur->datum ([syn syn])
+          (syntax-parse (core-expand syn)
+            #:literals (term reduce #%app subst-all)
+            #:datum-literals (elim Π λ : Unv)
+            [x:id (syntax->datum #'x)]
+            [(subst-all e _ _) (syntax->datum #'e)]
+            [(reduce Δ e) (cur->datum #'e)]
+            [(term e) (cur->datum #'e)]
+            [(Unv i) (term (Unv ,(syntax->datum #'i)))]
+            ;; TODO: should really check that b is one of the binders
+            ;; Maybe make a syntax class for the binders, core forms,
+            ;; etc.
+            [(b:id (x:id : t) e)
+             (let* ([x (syntax->datum #'x)]
+                    [t (cur->datum #'t)]
+                    [e (parameterize ([gamma (extend-Γ/term gamma x t)])
+                         (cur->datum #'e))])
+               (term (,(syntax->datum #'b) (,x : ,t) ,e)))]
+            [(elim t1 t2)
+             (let* ([t1 (cur->datum #'t1)]
+                    [t2 (cur->datum #'t2)])
+               (term (elim ,t1 ,t2)))]
+            [(#%app e1 e2)
+             (term (,(cur->datum #'e1) ,(cur->datum #'e2)))]))))
+    (unless (or (inner-expand?) (type-infer/term reified-term))
+      (printf "Delta: ~s~nGamma: ~s~n" (delta) (gamma))
+      (raise-syntax-error 'cur "term is ill-typed:" reified-term syn))
+    reified-term)
+
+  (define (datum->cur syn t)
+    (match t
+      [(list (quote term) e)
+       (quasisyntax/loc
+         syn
+         (datum->cur syn e))]
+      [(list (quote Unv) i)
+       (quasisyntax/loc
+         syn
+         (Type #,i))]
+      [(list (quote Π) (list x (quote :) t) body)
+       (quasisyntax/loc
+         syn
+         (dep-forall (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
+      [(list (quote λ) (list x (quote :) t) body)
+       (quasisyntax/loc
+         syn
+         (dep-lambda (#,(datum->syntax syn x) : #,(datum->cur syn t)) #,(datum->cur syn body)))]
+      [(list (list (quote elim) t1) t2)
+       (quasisyntax/loc
+         syn
+         (dep-elim #,(datum->cur syn t1) #,(datum->cur syn t2)))]
+      [(list e1 e2)
+       (quasisyntax/loc
+         syn
+         (dep-app #,(datum->cur syn e1) #,(datum->cur syn e2)))]
+      [_
+       (quasisyntax/loc
+         syn
+         #,(datum->syntax syn t))]))
+
+  (define (eval-cur syn)
+    (term (reduce ,(delta) ,(subst-bindings (cur->datum syn)))))
+
+  (define (syntax->curnel-syntax syn)
+    (quasisyntax/loc
+      syn
+      ;; TODO: this subst-all should be #,(subst-bindings (cur->datum syn)), but doesn't work
+      (term (reduce #,(delta) (subst-all #,(cur->datum syn) #,(first (bind-subst)) #,(second (bind-subst)))))))
+
+  ;; Reflection tools
+
+  (define (normalize/syn syn)
+    (datum->cur
+      syn
+      (eval-cur syn)))
+
+  (define (step/syn syn)
+    (datum->cur
+      syn
+      (term (step ,(delta) ,(subst-bindings (cur->datum syn))))))
+
+  ;; Are these two terms equivalent in type-systems internal equational reasoning?
+  (define (cur-equal? e1 e2)
+    (and (judgment-holds (equivalent ,(delta) ,(eval-cur e1) ,(eval-cur e2))) #t))
+
+  ;; TODO: Document local-env
+  (define (type-infer/syn syn #:local-env [env '()])
+    (parameterize ([gamma (for/fold ([gamma (gamma)])
+                                    ([(x t) (in-dict env)])
+                            (extend-Γ/syn (thunk gamma) x t))])
+      (let ([t (type-infer/term (eval-cur syn))])
+        (and t (datum->cur syn t)))))
+
+  (define (type-check/syn? syn type)
+    (type-check/term? (eval-cur syn) (eval-cur type)))
+
+  ;; Takes a Cur term syn and an arbitrary number of identifiers ls. The cur term is
+  ;; expanded until expansion reaches a Curnel form, or one of the
+  ;; identifiers in ls.
+  (define (cur-expand syn . ls)
+    (disarm
+      (local-expand
+        syn
+        'expression
+        (append (syntax-e #'(Type dep-inductive dep-lambda dep-app dep-elim dep-forall dep-top))
+                ls)))))
+
+;; -----------------------------------------------------------------
+;; Require/provide macros
+
+#| TODO NB XXX
+ | This is code some of the most hacky awful code I've ever written. But it works. ish
+ |#
+(begin-for-syntax
+  (define envs (list #'(void)))
+
+  (define (cur-identifier-bound? id)
+    (let ([x (syntax->datum id)])
+      (and (x? x)
+        (or (term (Γ-ref ,(gamma) ,x))
+          (term (Δ-ref-type ,(delta) ,x))))))
+
+  (define (filter-cur-exports syn modes)
+    (partition (compose cur-identifier-bound? export-local-id)
+               (apply append (map (lambda (e) (expand-export e modes))
+                                  (syntax->list syn))))))
+(define-syntax extend-env-and-provide
+  (make-provide-transformer
+    (lambda (syn modes)
+      (syntax-case syn ()
+        [(_ e ...)
+         (let-values ([(cur ~cur) (filter-cur-exports #'(e ...) modes)])
+           #| TODO: Ignoring the built envs for now
+           (set! envs (for/list ([e cur])
+           (let* ([x (syntax->datum (export-local-id e))]
+                  [t (type-infer/term x)]
+                  [env (if (term (lookup ,(gamma) ,x)) #'gamma #'delta)])
+             #`(extend-env/term! #,env #,(export-out-sym e) #,t))))
+           |#
+        ~cur)]))))
+
+(define-syntax (export-envs syn)
+  (syntax-case syn ()
+    [(_ gamma-out delta-out bind-out)
+     (begin
+       #`(begin-for-syntax
+          (define gamma-out (term #,(gamma)))
+          (define delta-out (term #,(delta)))
+          (define bind-out '#,(bind-subst))))]))
+
+;; TODO: This can only handle a single provide form, otherwise generates multiple *-out
+(define-syntax (dep-provide syn)
+  (syntax-case syn ()
+    [(_ e ...)
+     (begin
+       #| TODO NB:
+        | Ignoring the built envs above, for now.  The local-lift export seems to get executed before
+        | the filtered environment is built.
+        |#
+       ;; TODO: rename out will need to rename variables in gamma and ; delta.
+       (syntax-local-lift-module-end-declaration
+         #`(export-envs gamma-out delta-out bind-out))
+       #`(provide (extend-env-and-provide e ...)
+                  (for-syntax gamma-out delta-out bind-out)))]))
+(begin-for-syntax
+  (define out-gammas #`())
+  (define out-deltas #`())
+  (define out-binds #`())
+  (define gn 0)
+  (define sn 0)
+  (define bn 0)
+  (define (filter-cur-imports syn)
+    (for/fold ([imports '()]
+               [sources '()])
+              ([req-spec (syntax->list syn)])
+      (let-values ([(more-imports more-sources) (expand-import req-spec)])
+        (values (for/fold ([imports imports])
+                          ([imp more-imports])
+                  (cond
+                    [(equal? (import-src-sym imp) 'gamma-out)
+                     (let ([new-id (format-id (import-orig-stx imp)
+                                              "gamma-out~a" gn)])
+                       ;; TODO: Fewer set!s
+                       ;; TODO: Do not DIY gensym
+                       (set! gn (add1 gn))
+                       (set! out-gammas
+                             #`(#,@out-gammas (gamma (term (Γ-union
+                                                             ,(gamma)
+                                                             ,#,new-id)))))
+                       (cons (struct-copy import imp [local-id new-id])
+                             imports))]
+                    ;; TODO: Many shared code between these two clauses
+                    [(equal? (import-src-sym imp) 'delta-out)
+                     (let ([new-id (format-id (import-orig-stx imp)
+                                              "delta-out~a" sn)])
+                       ;; TODO: Fewer set!s
+                       ;; TODO: Do not DIY gensym
+                       (set! sn (add1 sn))
+                       (set! out-deltas
+                             #`(#,@out-deltas (delta (term (Δ-union
+                                                             ,(delta)
+                                                             ,#,new-id)))))
+                       (cons (struct-copy import imp [local-id new-id])
+                             imports))]
+                    ;; TODO: Many shared code between these two clauses
+                    [(equal? (import-src-sym imp) 'bind-out)
+                     (let ([new-id (format-id (import-orig-stx imp)
+                                              "bind-out~a" bn)])
+                       ;; TODO: Fewer set!s
+                       ;; TODO: Do not DIY gensym
+                       (set! bn (add1 bn))
+                       (set! out-binds
+                             #`(#,@out-binds (bind-subst (list (append
+                                                                 (first #,new-id)
+                                                                 (first (bind-subst)))
+                                                               (append
+                                                                 (second #,new-id)
+                                                                 (second (bind-subst)))))))
+                       (cons (struct-copy import imp [local-id new-id])
+                             imports))]
+                    [else (cons imp imports)]))
+                (append sources more-sources))))))
+
+(define-syntax extend-env-and-require
+  (make-require-transformer
+    (lambda (syn)
+      (syntax-case syn ()
+        [(_ e ...) (filter-cur-imports #'(e ...))]))))
+
+;; TODO: rename in will need to rename variables in gamma and delta.
+(define-syntax (import-envs syn)
+  (syntax-case syn ()
+    [(_) #`(begin-for-syntax #,@out-gammas #,@out-deltas
+                             #,@out-binds)]))
+
+(define-syntax (dep-require syn)
+  (syntax-case syn ()
+    [(_ e ...)
+     #`(begin
+         (require (extend-env-and-require e ...))
+         (import-envs))]))
+
+(define-syntax (dep-module+ syn)
+  (syntax-case syn ()
+    [(_ name body ...)
+     #`(module+ name
+         (begin-for-syntax
+           (gamma (term #,(gamma)))
+           (delta (term #,(delta)))
+           (bind-subst '#,(bind-subst)))
+         body ...)]))
+
+;; -----------------------------------------------------------------
+;; Core wrapper macros
+;;
+;; TODO: Can these be simplified further?
+(define-syntax (dep-lambda syn)
+  (syntax-case syn (:)
+    [(_ (x : t) e)
+     (syntax->curnel-syntax
+       (quasisyntax/loc syn (λ (x : t) e)))]))
+
+(define-syntax (dep-app syn)
+  (syntax-case syn ()
+    [(_ e1 e2)
+     (syntax->curnel-syntax
+       (quasisyntax/loc syn (#%app e1 e2)))]))
+
+(define-syntax (dep-forall syn)
+  (syntax-case syn (:)
+    [(_ (x : t) e)
+     (syntax->curnel-syntax
+       (quasisyntax/loc syn (Π (x : t) e)))]))
+
+(define-syntax (Type syn)
+  (syntax-case syn ()
+    [(_ i)
+     (syntax->curnel-syntax
+       (quasisyntax/loc syn (Unv i)))]
+    [_ (quasisyntax/loc syn (Type 0))]))
+
+(define-syntax (dep-inductive syn)
+  (syntax-case syn (:)
+    [(_ i : ti (x1 : t1) ...)
+     (begin
+       (extend-Δ/syn! delta #'i #'ti #'((x1 : t1) ...))
+       #'(void))]))
+
+(define-syntax (dep-elim syn)
+  (syntax-case syn ()
+    [(_ D T)
+     (syntax->curnel-syntax
+       (quasisyntax/loc syn (elim D T)))]))
+
+(define-syntax-rule (dep-void) (void))
+
+;; TODO: Not sure if this is the correct behavior for #%top
+(define-syntax (dep-top syn)
+  (syntax-case syn ()
+    [(_ . id)
+     ;; TODO NB FIXME: HACKS HACKS HACKS
+     (let ([t (core-expand #'id)])
+       (if (equal? (syntax->datum t) '(void))
+           #'(void)
+           (syntax->curnel-syntax t)))]))
+
+(define-syntax (dep-top-interaction syn)
+  (syntax-case syn ()
+    [(_ . form)
+     (begin
+       ;; TODO NB FIXME: HACKS
+       #`(begin
+           (export-envs gamma-out delta-out bind-out)
+           (begin-for-syntax
+             (define nm (map (lambda (x) (namespace-variable-value x #f (lambda x #t))) (namespace-mapped-symbols)))
+             (bind-subst (first (memf subst? nm)))
+             (gamma (first (memf Γ? nm)))
+             (delta (first (memf Δ? nm))))
+          form))]))
+
+(define-syntax (dep-define syn)
+  (syntax-parse syn
+    [(_ id:id e)
+     (let ([e (cur->datum #'e)]
+           [id (syntax->datum #'id)])
+       ;; NB: Have to roll our own namespace rather than use built-in define so id is resolved at
+       ;; compile time in redex, and at runtime in racket.
+       (extend-Γ/term! gamma id (type-infer/term e))
+       (add-binding/term! id e)
+       #'(void))]))

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

@@ -0,0 +1,665 @@
+#lang racket/base
+;; TODO: Copy-paste of redex-core
+(require
+ redex/reduction-semantics
+ cur/curnel/hybrid-core
+ rackunit
+ racket/function
+ (only-in racket/set set=?))
+(define-syntax-rule (check-holds (e ...))
+  (check-true
+   (judgment-holds (e ...))))
+(define-syntax-rule (check-not-holds (e ...))
+  (check-false
+   (judgment-holds (e ...))))
+(define-syntax-rule (check-equiv? e1 e2)
+  (check (default-equiv) e1 e2))
+(define-syntax-rule (check-not-equiv? e1 e2)
+  (check (compose not (default-equiv)) e1 e2))
+
+(default-equiv (lambda (x y) (term (α-equivalent? ,x ,y))))
+
+;; Syntax tests
+;; ------------------------------------------------------------------------
+
+(define-term Type (Unv 0))
+(check-true (x? (term T)))
+(check-true (x? (term A)))
+(check-true (x? (term truth)))
+(check-true (x? (term zero)))
+(check-true (x? (term s)))
+(check-true (t? (term zero)))
+(check-true (t? (term s)))
+(check-true (x? (term nat)))
+(check-true (t? (term nat)))
+(check-true (t? (term A)))
+(check-true (t? (term S)))
+(check-true (U? (term (Unv 0))))
+(check-true (U? (term Type)))
+(check-true (e? (term (λ (x_0 : (Unv 0)) x_0))))
+(check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
+(check-true (t? (term (λ (x_0 : (Unv 0)) x_0))))
+
+;; TODO: Rename these signatures, and use them in all future tests.
+(define Δ (term (Δ-set* ,(make-empty-Δ)
+                 (nat (Unv 0) ((zero : nat) (s : (Π (x : nat) nat))))
+                 (bool (Unv 0) ((true : bool) (false : bool))))))
+(define Δ0 (make-empty-Δ))
+(define Δ3 (term (Δ-set ,(make-empty-Δ) and (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0))) ())))
+(define Δ4 (term (Δ-set ,(make-empty-Δ) and (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                         ((conj : (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B))))))))))
+(check-true (Δ? Δ0))
+(check-true (Δ? Δ))
+(check-true (Δ? Δ4))
+(check-true (Δ? Δ3))
+(check-true (Δ? Δ4))
+(define sigma (term (Δ-set* ,(make-empty-Δ)
+                            (true (Unv 0) ((T : true)))
+                            (false (Unv 0) ())
+                            (equal (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                                   ())
+                            (nat (Unv 0) ())
+                            (heap (Unv 0) ())
+                            (pre (Π (temp808 : heap) (Unv 0)) ()))))
+(displayln sigma)
+(check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (true (Unv 0) ((T : true)))))))
+(check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (false (Unv 0) ())))))
+(check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (equal (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                                ())))))
+(check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (nat (Unv 0) ())))))
+(check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (pre (Π (temp808 : heap) (Unv 0)) ())))))
+
+(check-true (Δ? (term (Δ-set* ,(make-empty-Δ) (true (Unv 0) ((T : true))) (false (Unv 0) ())))))
+(check-true (Δ? (term (Δ-set* ,(make-empty-Δ)
+                              (true (Unv 0) ((T : true)))
+                              (false (Unv 0) ())
+                              (equal (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Unv 0)))
+                                     ())))))
+(check-true (Δ? sigma))
+(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))))
+
+;; Various accessor tests
+;; ------------------------------------------------------------------------
+
+(check-equal?
+ (term (Δ-key-by-constructor ,Δ zero))
+ (term nat))
+(check-equal?
+ (term (Δ-key-by-constructor ,Δ s))
+ (term nat))
+
+(check-equal?
+ (term (Δ-ref-constructor-map ,Δ nat))
+ (term ((zero : nat) (s : (Π (x : nat) nat)))))
+(check-equal?
+ (term (Δ-ref-constructor-map ,sigma false))
+ (term ()))
+
+;; Telescope tests
+;; ------------------------------------------------------------------------
+;; Are these telescopes the same when filled with alpha-equivalent, and equivalently renamed, termed
+(define (telescope-equiv x y)
+  (alpha-equivalent? ttL (term (in-hole ,x (Unv 0))) (term (in-hole ,y (Unv 0)))))
+(define-syntax-rule (check-telescope-equiv? e1 e2)
+  (check telescope-equiv e1 e2))
+(define-syntax-rule (check-telescope-not-equiv? e1 e2)
+  (check (compose not telescope-equiv) e1 e2))
+
+(check-telescope-equiv?
+ (term (Δ-ref-parameter-Ξ ,Δ nat))
+ (term hole))
+(check-telescope-equiv?
+ (term (Δ-ref-parameter-Ξ ,Δ4 and))
+ (term (Π (A : Type) (Π (B : Type) hole))))
+
+(check-telescope-equiv?
+ (term (Ξ-compose
+        (Π (x : t_0) (Π (y : t_1) hole))
+        (Π (z : t_2) (Π (a : t_3) hole))))
+ (term (Π (x : t_0) (Π (y : t_1) (Π (z : t_2) (Π (a : t_3) hole))))))
+
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ nat (λ (x : nat) nat)))
+ (term (Π (m-zero : ((λ (x : nat) nat) zero))
+          (Π (m-s : (Π (x : nat) (Π (x-ih : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x))))) hole))))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ nat P))
+ (term (Π (m-zero : (P zero))
+          (Π (m-s : (Π (x : nat) (Π (ih-x : (P x)) (P (s x)))))
+             hole))))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ  nat (λ (x : nat) nat)))
+ (term (Π (m-zero :  ((λ (x : nat) nat) zero))
+          (Π (m-s : (Π (x : nat) (Π (ih-x : ((λ (x : nat) nat) x)) ((λ (x : nat) nat) (s x)))))
+             hole))))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δ4 and (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))))
+ (term (Π (m-conj : (Π (A : Type) (Π (B : Type) (Π (a : A) (Π (b : B)
+                                                              ((((λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
+                                                                 A)
+                                                                B)
+                                                               ((((conj A) B) a) b)))))))
+          hole)))
+(check-true (x? (term false)))
+(check-true (Ξ? (term hole)))
+(check-true (t? (term (λ (y : false) (Π (x : Type) x)))))
+(check-true (redex-match? ttL ((x : t) ...) (term ())))
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,sigma false (λ (y : false) (Π (x : Type) x))))
+ (term hole))
+
+;; Tests for inductive elimination
+;; ------------------------------------------------------------------------
+;; 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?
+ (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
+                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                         (hole zero)))
+ (term (hole (((((elim nat Type) (λ (x : nat) nat))
+                (s zero))
+               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              zero))))
+(check-telescope-equiv?
+ (term (Δ-inductive-elim ,Δ nat Type (λ (x : nat) nat) hole
+                         ((hole (s zero)) (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                         (hole (s zero))))
+ (term (hole (((((elim nat Type) (λ (x : nat) nat))
+                (s zero))
+               (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+              (s zero)))))
+
+;; Tests for dynamic semantics
+;; ------------------------------------------------------------------------
+
+(check-true (v? (term (λ (x_0 : (Unv 0)) x_0))))
+(check-true (v? (term (refl Nat))))
+(check-true (v? (term ((refl Nat) z))))
+
+;; TODO: Move equivalence up here, and use in these tests.
+(check-equiv? (term (reduce ∅ (Unv 0))) (term (Unv 0)))
+(check-equiv? (term (reduce ∅ ((λ (x : t) x) (Unv 0)))) (term (Unv 0)))
+(check-not-equiv? (term (reduce ∅ ((Π (x : t) x) (Unv 0)))) (term (Unv 0)))
+(check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) x_0) (Unv 0)))))
+                  (term (Π (x : t) (Unv 0))))
+(check-not-equiv? (term (reduce ∅ (Π (x : t) ((Π (x_0 : t) (x_0 x)) x))))
+                  (term (Π (x : t) (x x))))
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+                                  (s zero))
+                                 (λ (x : nat) (λ (ih-x : nat)
+                                                (s (s x)))))
+                                zero)))
+              (term (s zero)))
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+                                  (s zero))
+                                 (λ (x : nat) (λ (ih-x : nat)
+                                                (s (s x)))))
+                                (s zero))))
+              (term (s (s zero))))
+(check-equiv? (term (reduce ,Δ (((((elim nat Type) (λ (x : nat) nat))
+                                  (s zero))
+                                 (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+                                (s (s (s zero))))))
+              (term (s (s (s (s zero))))))
+
+(check-equiv?
+ (term (reduce ,Δ
+               (((((elim nat Type) (λ (x : nat) nat))
+                  (s (s zero)))
+                 (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                (s (s zero)))))
+ (term (s (s (s (s zero))))))
+(check-equiv?
+ (term (step ,Δ
+             (((((elim nat Type) (λ (x : nat) nat))
+                (s (s zero)))
+               (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+              (s (s zero)))))
+ (term
+  (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+    (s zero))
+   (((((elim nat Type) (λ (x : nat) nat))
+      (s (s zero)))
+     (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+    (s zero)))))
+(check-equiv?
+ (term (step ,Δ (step ,Δ
+                      (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+                        (s zero))
+                       (((((elim nat Type) (λ (x : nat) nat))
+                          (s (s zero)))
+                         (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+                        (s zero))))))
+ (term
+  ((λ (ih-x1 : nat) (s ih-x1))
+   (((λ (x : nat) (λ (ih-x : nat) (s ih-x)))
+     zero)
+    (((((elim nat Type) (λ (x : nat) nat))
+       (s (s zero)))
+      (λ (x : nat) (λ (ih-x : nat) (s ih-x))))
+     zero)))))
+
+(define-syntax-rule (check-equivalent e1 e2)
+  (check-holds (equivalent ∅ e1 e2)))
+(check-equivalent
+ (λ (x : Type) x) (λ (y : Type) y))
+(check-equivalent
+ (Π (x : Type) x) (Π (y : Type) y))
+
+;; 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)))))
+;; (nat -> nat) -> nat
+;; Not sure if this is actually supposed to pass
+(check-false (term (positive* nat ((Π (x : (Π (y : nat) nat)) nat)))))
+;; ((Unv 0) -> nat) -> nat
+(check-true (term (positive* 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)))))
+;; 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-true (judgment-holds (wf ,Δ0 ∅)))
+(check-true (redex-match? tt-redL (in-hole Ξ (Unv 0)) (term (Unv 0))))
+(check-true (redex-match? tt-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
+                          (term (Π (x : nat) nat))))
+(define (bindings-equal? l1 l2)
+  (map set=? l1 l2))
+(check-pred
+ (curry bindings-equal?
+        (list (list
+               (make-bind 'Ξ (term (Π (x : nat) hole)))
+               (make-bind 'Φ (term hole))
+               (make-bind 'Θ (term hole)))
+              (list
+               (make-bind 'Ξ (term hole))
+               (make-bind 'Φ (term (Π (x : nat) hole)))
+               (make-bind 'Θ (term hole)))))
+ (map match-bindings (redex-match tt-redL (in-hole Ξ (in-hole Φ (in-hole Θ nat)))
+                                  (term (Π (x : nat) nat)))))
+(check-pred
+ (curry bindings-equal?
+        (list
+         (list
+          (make-bind 'Φ (term (Π (x : nat) hole)))
+          (make-bind 'Θ (term hole)))))
+ (map match-bindings (redex-match tt-redL (in-hole hole (in-hole Φ (in-hole Θ nat)))
+                                  (term (Π (x : nat) nat)))))
+
+(check-true
+ (redex-match? tt-redL
+               (in-hole hole (in-hole hole (in-hole hole nat)))
+               (term nat)))
+(check-true
+ (redex-match? tt-redL
+               (in-hole hole (in-hole (Π (x : nat) hole) (in-hole hole nat)))
+               (term (Π (x : nat) nat))))
+(check-holds (wf (Δ-set ,(make-empty-Δ) nat (Unv 0) ()) ∅))
+
+(check-holds (wf ,Δ0 ∅))
+(check-holds (type-infer ,(make-empty-Δ) ∅ (Unv 0) U))
+(check-holds (type-infer ,(make-empty-Δ) (∅ nat : (Unv 0)) nat U))
+(check-holds (type-infer ,(make-empty-Δ) (∅ nat : (Unv 0)) (Π (x : nat) nat) U))
+(check-true (term (positive* nat (nat (Π (x : nat) nat)))))
+(check-holds
+ (wf (Δ-set ,(make-empty-Δ) nat (Unv 0) ((zero : nat))) ∅))
+(check-holds
+ (wf (Δ-set ,(make-empty-Δ) nat (Unv 0) ((s : (Π (x : nat) nat)))) ∅))
+(check-holds (wf ,Δ ∅))
+
+;; TODO: Poor abstraction w.r.t. Δ
+(check-holds (wf ,Δ3 ∅))
+(check-holds (wf ,Δ4 ∅))
+(check-holds (wf (Δ-set ,(make-empty-Δ) truth (Unv 0) ()) ∅))
+(check-holds (wf ,(make-empty-Δ) (∅ x : (Unv 0))))
+(check-holds (wf (Δ-set ,(make-empty-Δ) nat (Unv 0) ()) (∅ x : nat)))
+(check-holds (wf (Δ-set ,(make-empty-Δ) nat (Unv 0) ()) (∅ x : (Π (x : nat) nat))))
+
+(check-holds (type-infer ,(make-empty-Δ) ∅ (Unv 0) (Unv 1)))
+(check-holds (type-infer ,(make-empty-Δ) (∅ x : (Unv 0)) (Unv 0) (Unv 1)))
+(check-holds (type-infer ,(make-empty-Δ) (∅ x : (Unv 0)) x (Unv 0)))
+(check-holds (type-infer ,(make-empty-Δ) ((∅ x_0 : (Unv 0)) x_1 : (Unv 0))
+                           (Π (x_3 : x_0) x_1) (Unv 0)))
+(check-holds (type-infer ,(make-empty-Δ) (∅ x_0 : (Unv 0)) x_0 U_1))
+(check-holds (type-infer ,(make-empty-Δ) ((∅ x_0 : (Unv 0)) x_2 : x_0) (Unv 0) U_2))
+(check-holds (unv-pred (Unv 0) (Unv 0) (Unv 0)))
+(check-holds (type-infer ,(make-empty-Δ) (∅ x_0 : (Unv 0)) (Π (x_2 : x_0) (Unv 0)) t))
+
+(check-holds (type-check ,(make-empty-Δ) ∅ (λ (x : (Unv 0)) x) (Π (x : (Unv 0)) (Unv 0))))
+(check-holds (type-check ,(make-empty-Δ) ∅ (λ (y : (Unv 0)) (λ (x : y) x))
+                             (Π (y : (Unv 0)) (Π (x : y) y))))
+
+(check-equal? (list (term (Unv 1)))
+              (judgment-holds
+               (type-infer ,(make-empty-Δ) ((∅ x1 : (Unv 0)) x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0)))
+                             U)
+               U))
+;; ---- Elim
+;; TODO: Clean up/Reorganize these tests
+(check-true
+ (redex-match? tt-typingL
+               (in-hole Θ_m (((elim x_D U) e_D) e_P))
+               (term ((((elim truth Type) T) (Π (x : truth) (Unv 1))) (Unv 0)))))
+(define Δtruth (term (Δ-set ,(make-empty-Δ) truth (Unv 0) ((T : truth)))))
+(check-holds (type-infer ,Δtruth ∅ truth (in-hole Ξ U)))
+(check-holds (type-infer ,Δtruth ∅ T (in-hole Θ_ai truth)))
+(check-holds (type-infer ,Δtruth ∅ (λ (x : truth) (Unv 1))
+                         (in-hole Ξ (Π (x : (in-hole Θ truth)) U))))
+
+(check-telescope-equiv?
+ (term (Δ-methods-telescope ,Δtruth truth (λ (x : truth) (Unv 1))))
+ (term (Π (m-T : ((λ (x : truth) (Unv 1)) T)) hole)))
+(check-holds (type-infer ,Δtruth ∅ (elim truth Type) t))
+(check-holds (type-check (Δ-set ,(make-empty-Δ) truth (Unv 0) ((T : truth)))
+                         ∅
+                         ((((elim truth (Unv 2)) (λ (x : truth) (Unv 1))) (Unv 0))
+                          T)
+                         (Unv 1)))
+(check-not-holds (type-check (Δ-set ,(make-empty-Δ) truth (Unv 0) ((T : truth)))
+                             ∅
+                             ((((elim truth (Unv 1)) Type) Type) T)
+                             (Unv 1)))
+(check-holds
+ (type-infer ,(make-empty-Δ) ∅ (Π (x2 : (Unv 0)) (Unv 0)) U))
+(check-holds
+ (type-infer ,(make-empty-Δ) (∅ x1 : (Unv 0)) (λ (x2 : (Unv 0)) (Π (t6 : x1) (Π (t2 : x2) (Unv 0))))
+               t))
+(check-holds
+ (type-infer ,Δ ∅ nat (in-hole Ξ U)))
+(check-holds
+ (type-infer ,Δ ∅ zero (in-hole Θ_ai nat)))
+(check-holds
+ (type-infer ,Δ ∅ (λ (x : nat) nat)
+             (in-hole Ξ (Π (x : (in-hole Θ nat)) U))))
+(define-syntax-rule (nat-test syn ...)
+  (check-holds (type-check ,Δ syn ...)))
+(nat-test ∅ (Π (x : nat) nat) (Unv 0))
+(nat-test ∅ (λ (x : nat) x) (Π (x : nat) nat))
+(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat)) zero)
+              (λ (x : nat) (λ (ih-x : nat) x))) zero)
+            nat)
+(nat-test ∅ nat (Unv 0))
+(nat-test ∅ zero nat)
+(nat-test ∅ s (Π (x : nat) nat))
+(nat-test ∅ (s zero) nat)
+;; TODO: Meta-function auto-currying and such
+(check-holds
+ (type-infer ,Δ ∅ ((((elim nat (Unv 0)) (λ (x : nat) nat))
+                    zero)
+                   (λ (x : nat) (λ (ih-x : nat) x)))
+             t))
+(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
+               zero)
+              (λ (x : nat) (λ (ih-x : nat) x)))
+             zero)
+            nat)
+(nat-test ∅ (((((elim nat (Unv 0)) (λ (x : nat) nat))
+               (s zero))
+              (λ (x : nat) (λ (ih-x : nat) (s (s x)))))
+             zero)
+            nat)
+(nat-test ∅ (((((elim nat Type) (λ (x : nat) nat))
+               (s zero))
+              (λ (x : nat) (λ (ih-x : nat) (s (s x))))) zero)
+            nat)
+(nat-test (∅ n : nat)
+          (((((elim nat (Unv 0)) (λ (x : nat) nat)) zero) (λ (x : nat) (λ (ih-x : nat) x))) n)
+          nat)
+(check-holds
+ (type-check (Δ-set ,Δ bool (Unv 0) ((btrue : bool) (bfalse : bool)))
+             (∅ n2 : nat)
+             (((((elim nat (Unv 0)) (λ (x : nat) bool))
+                btrue)
+               (λ (x : nat) (λ (ih-x : bool) bfalse)))
+              n2)
+             bool))
+(check-not-holds
+ (type-check ,Δ ∅
+             ((((elim nat (Unv 0)) nat) (s zero)) zero)
+             nat))
+(define lam (term (λ (nat : (Unv 0)) nat)))
+(check-equivalent
+ (Π (nat : (Unv 0)) (Unv 0))
+ ,(car (judgment-holds (type-infer ,Δ0 ∅ ,lam t) t)))
+(check-equivalent
+ (Π (nat : (Unv 0)) (Unv 0))
+ ,(car (judgment-holds (type-infer ,Δ ∅ ,lam t) t)))
+(check-equivalent
+ (Π (x : (Π (y : (Unv 0)) y)) nat)
+ ,(car (judgment-holds (type-infer (Δ-set ,(make-empty-Δ) nat (Unv 0) ()) ∅ (λ (x : (Π (y : (Unv 0)) y)) (x nat))
+                                   t) t)))
+(check-equivalent
+ (Π (y : (Unv 0)) (Unv 0))
+ ,(car (judgment-holds (type-infer (Δ-set ,(make-empty-Δ) nat (Unv 0) ()) ∅ (λ (y : (Unv 0)) y) t) t)))
+(check-equivalent
+ (Unv 0)
+ ,(car (judgment-holds (type-infer (Δ-set ,(make-empty-Δ) nat (Unv 0) ()) ∅
+                                   ((λ (x : (Π (y : (Unv 0)) (Unv 0))) (x nat))
+                                    (λ (y : (Unv 0)) y))
+                                   t) t)))
+(check-equal?
+ (list (term (Unv 0)) (term (Unv 1)))
+ (judgment-holds
+  (type-infer ,Δ4 ∅ (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))
+              U) U))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) conj (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (a : A) (Π (b : B) ((and A) B)))))))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0))
+             conj (Π (P : (Unv 0)) (Π (Q : (Unv 0)) (Π (x : P) (Π (y : Q) ((and P) Q)))))))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) S (Unv 0)))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) (conj S)
+             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
+(check-holds
+ (type-check ,Δ4 (∅ S : (Unv 0)) (conj S)
+             (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B))))))
+(check-holds
+ (type-check ,Δ4 ∅ (λ (S : (Unv 0)) (conj S))
+             (Π (S : (Unv 0)) (Π (B : (Unv 0)) (Π (a : S) (Π (b : B) ((and S) B)))))))
+(check-holds
+ (type-check (Δ-set ,Δ4 true (Unv 0) ((tt : true))) ∅
+             ((((conj true) true) tt) tt)
+             ((and true) true)))
+(check-holds
+ (type-infer ,Δ4 ∅ and (in-hole Ξ U_D)))
+(check-holds
+ (type-infer (Δ-set ,Δ4 true (Unv 0) ((tt : true))) ∅
+             ((((conj true) true) tt) tt)
+             (in-hole Θ and)))
+(check-holds
+ (type-infer (Δ-set ,Δ4 true (Unv 0) ((tt : true))) ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) true)))
+             (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
+(check-holds
+ (type-check (Δ-set ,Δ4 true (Unv 0) ((tt : true))) ∅
+             ((((((elim and (Unv 0))
+                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                true))))
+                 (λ (A : (Unv 0))
+                   (λ (B : (Unv 0))
+                     (λ (a : A)
+                       (λ (b : B) tt)))))
+                true) true)
+              ((((conj true) true) tt) tt))
+             true))
+(check-true (Γ? (term (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q)))))
+(check-holds
+ (type-infer ,Δ4 ∅ and (in-hole Ξ U)))
+(check-holds
+ (type-infer ,Δ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
+             ab (in-hole Θ and)))
+(check-true
+ (redex-match? tt-redL
+               (in-hole Ξ (Π (x : (in-hole Θ and)) U))
+               (term (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0)))))))
+(check-holds
+ (type-infer ,Δ4 (((∅ P : Type) Q : Type) ab : ((and P) Q))
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                           ((and B) A))))
+             (in-hole Ξ (Π (x : (in-hole Θ and)) U))))
+(check-holds
+ (equivalent ,Δ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
+ (type-infer ,Δ4 ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                           ((and B) A))))
+             (in-hole Ξ (Π (x : (in-hole Θ_Ξ and)) U_P))))
+(check-holds
+ (type-check ,Δ4
+             (((∅ P : (Unv 0)) Q : (Unv 0)) ab : ((and P) Q))
+             ((((((elim and (Unv 0))
+                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                ((and B) A)))))
+                 (λ (A : (Unv 0))
+                   (λ (B : (Unv 0))
+                     (λ (a : A)
+                       (λ (b : B) ((((conj B) A) b) a))))))
+                P) Q) ab)
+             ((and Q) P)))
+(check-holds
+ (type-check (Δ-set ,Δ4 true (Unv 0) ((tt : true))) ∅
+             (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B)) ((and B) A))))
+             (Π (A : (Unv 0)) (Π (B : (Unv 0)) (Π (x : ((and A) B)) (Unv 0))))))
+(check-holds
+ (type-infer (Δ-set ,Δ4 true (Unv 0) ((tt : true)))
+             ((∅ A : Type) B : Type)
+             (conj B)
+             t))
+(check-holds
+ (type-check (Δ-set ,Δ4 true (Unv 0) ((tt : true))) ∅
+             ((((((elim and (Unv 0))
+                  (λ (A : Type) (λ (B : Type) (λ (x : ((and A) B))
+                                                ((and B) A)))))
+                 (λ (A : (Unv 0))
+                   (λ (B : (Unv 0))
+                     (λ (a : A)
+                       (λ (b : B) ((((conj B) A) b) a))))))
+                true) true)
+              ((((conj true) true) tt) tt))
+             ((and true) true)))
+(define gamma (term (∅ temp863 : pre)))
+(check-holds (wf ,sigma ∅))
+(check-holds (wf ,sigma ,gamma))
+(check-holds
+ (type-infer ,sigma ,gamma (Unv 0) t))
+(check-holds
+ (type-infer ,sigma ,gamma pre t))
+(check-holds
+ (type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
+(check-holds
+ (type-infer ,sigma ,gamma pre t))
+(check-holds
+ (type-check ,sigma (,gamma tmp863 : pre) (Unv 0) (Unv 1)))
+(check-holds
+ (type-infer ,sigma (,gamma x : false) false (in-hole Ξ U_D)))
+(check-holds
+ (type-infer ,sigma (,gamma x : false) x (in-hole Θ false)))
+(check-holds
+ (type-infer ,sigma (,gamma x : false) (λ (y : false) (Π (x : Type) x))
+             (in-hole Ξ (Π (x : (in-hole Θ false)) U))))
+(check-true
+ (redex-match? tt-typingL
+               ((in-hole Θ_m ((elim x_D U) e_P)) e_D)
+               (term (((elim false (Unv 1)) (λ (y : false) (Π (x : Type) x)))
+                      x))))
+(check-holds
+ (type-check ,sigma (,gamma x : false)
+             (((elim false (Unv 0)) (λ (y : false) (Π (x : Type) x))) x)
+             (Π (x : (Unv 0)) x)))
+
+;; nat-equal? tests
+(define zero?
+  (term ((((elim nat Type) (λ (x : nat) bool))
+          true)
+         (λ (x : nat) (λ (x_ih : bool) false)))))
+(check-holds
+ (type-check ,Δ ∅ ,zero? (Π (x : nat) bool)))
+(check-equal?
+ (term (reduce ,Δ (,zero? zero)))
+ (term true))
+(check-equal?
+ (term (reduce ,Δ (,zero? (s zero))))
+ (term false))
+(define ih-equal?
+  (term ((((elim nat Type) (λ (x : nat) bool))
+          false)
+         (λ (x : nat) (λ (y : bool) (x_ih x))))))
+(check-holds
+ (type-check ,Δ (∅ x_ih : (Π (x : nat) bool))
+             ,ih-equal?
+             (Π (x : nat) bool)))
+(check-holds
+ (type-infer ,Δ ∅ nat (Unv 0)))
+(check-holds
+ (type-infer ,Δ ∅ bool (Unv 0)))
+(check-holds
+ (type-infer ,Δ ∅ (λ (x : nat) (Π (x : nat) bool)) (Π (x : nat) (Unv 0))))
+(define nat-equal?
+  (term ((((elim nat Type) (λ (x : nat) (Π (x : nat) bool)))
+          ,zero?)
+         (λ (x : nat) (λ (x_ih : (Π (x : nat) bool))
+                        ,ih-equal?)))))
+(check-holds
+ (type-check ,Δ (∅ nat-equal? : (Π (x-D«4158» : nat) ((λ (x«4159» : nat) (Π (x«4160» : nat) bool)) x-D«4158»)))
+             ((nat-equal? zero) zero)
+             bool))
+(check-holds
+ (type-check ,Δ ∅
+             ,nat-equal?
+             (Π (x : nat) (Π (y : nat) bool))))
+(check-equal?
+ (term (reduce ,Δ ((,nat-equal? zero) (s zero))))
+ (term false))
+(check-equal?
+ (term (reduce ,Δ ((,nat-equal? (s zero)) zero)))
+ (term false))
+
+;; == tests
+(define Δ= (term (Δ-set ,Δ == (Π (A : (Unv 0)) (Π (a : A) (Π (b : A) (Unv 0))))
+                         ((refl : (Π (A : (Unv 0)) (Π (a : A) (((== A) a) a))))))))
+(check-true (Δ? Δ=))
+
+(define refl-elim
+  (term (((((((elim == (Unv 0)) (λ (A1 : (Unv 0)) (λ (x1 : A1) (λ (y1 : A1) (λ (p2 : (((==
+                                                                                        A1)
+                                                                                       x1)
+                                                                                      y1))
+                                                                              nat)))))
+             (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true))))
+(check-holds
+ (type-check ,Δ= ∅ ,refl-elim nat))
+(check-true
+ (redex-match?
+  tt-redL
+  (Δ (in-hole E (in-hole Θ ((elim x_D U) e_P))))
+  (term (,Δ= ,refl-elim))))
+(check-true
+ (redex-match?
+  tt-redL
+  (in-hole (Θ_p (in-hole Θ_i x_ci)) Θ_m)
+  (term (((((hole
+             (λ (A1 : (Unv 0)) (λ (x1 : A1) zero))) bool) true) true) ((refl bool) true)))))
+(check-telescope-equiv?
+ (term (Δ-ref-parameter-Ξ ,Δ= ==))
+ (term (Π (A : Type) (Π (a : A) (Π (b : A) hole)))))
+(check-equal?
+ (term (reduce ,Δ= ,refl-elim))
+ (term zero))