From b318617f0ec68e6697a267ecd67bb46b2629e68c Mon Sep 17 00:00:00 2001
From: "William J. Bowman" <wjb@williamjbowman.com>
Date: Mon, 11 Jan 2016 04:28:58 -0500
Subject: [PATCH] =?UTF-8?q?Set=20hybrid-core=20to=20default;=20converted?=
 =?UTF-8?q?=20=CE=94=20to=20dict?=
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

* Hybrid core now used by default in this branch.
* Converted Δ to a Racket dictionary, started converting Δ abstractions
  to use dictionary.
---
 cur-lib/cur/cur.rkt                |   6 +-
 cur-lib/cur/curnel/hybrid-core.rkt | 159 ++++++----
 cur-lib/cur/curnel/hybrid-lang.rkt | 493 +++++++++++++++++++++++++++++
 3 files changed, 586 insertions(+), 72 deletions(-)
 create mode 100644 cur-lib/cur/curnel/hybrid-lang.rkt

diff --git a/cur-lib/cur/cur.rkt b/cur-lib/cur/cur.rkt
index dd74a9e..5c7d4f0 100644
--- a/cur-lib/cur/cur.rkt
+++ b/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))
diff --git a/cur-lib/cur/curnel/hybrid-core.rkt b/cur-lib/cur/curnel/hybrid-core.rkt
index a93ce98..b1bbf4f 100644
--- a/cur-lib/cur/curnel/hybrid-core.rkt
+++ b/cur-lib/cur/curnel/hybrid-core.rkt
@@ -1,11 +1,11 @@
 #lang racket/base
 
 ;; A mostly Redex core, with parts written in Racket for performance reasons
-;; TODO: Move tests into common place to use in both Redex cores.
 
 (require
   racket/dict
   racket/function
+  racket/list
   redex/reduction-semantics)
 
 (provide
@@ -13,33 +13,21 @@
 
 (set-cache-size! 10000)
 
-;; Test suite setup.
-(module+ test
-  (require
-    rackunit
-    (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)))
+(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-language ttL
+(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))
-  ;; Δ (signature). (inductive-name : type ((constructor : type) ...))
-  ;; NB: Δ is a map from a name x to a pair of it's type and a map of constructor names to their types
-  (Δ   ::= ∅ (Δ (D : t ((c : t) ...))))
+  (Δ   ::= dict)
   (D x c ::= variable-not-otherwise-mentioned)
   #:binding-forms
   (λ (x : t) e #:refers-to x)
@@ -49,7 +37,17 @@
 (define t? (redex-match? ttL t))
 (define e? (redex-match? ttL e))
 (define U? (redex-match? ttL U))
-(define Δ? (redex-match? ttL Δ))
+
+;; 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?)
+(define-struct inductive-decl (type constr-dict))
+
+;; A Δ is a dict mapping names x? to inductive-decl?
+(define Δ? dict?)
+(define make-empty-Δ make-dict)
+(define empty-Δ? dict-empty?)
 
 ;;; ------------------------------------------------------------------------
 ;;; Universe typing
@@ -94,61 +92,73 @@
 ;;; ------------------------------------------------------------------------
 ;;; Primitive Operations on signatures Δ (those operations that do not require contexts)
 
-;;; 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
+;; 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) #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 Δ 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 any) (Δ (x : t any))])
+  [(Δ-set Δ x t any)
+   ,(dict-set
+     (term Δ)
+     (term x)
+     (inductive-decl
+      (term t)
+      (for/fold ([d (make-dict)])
+                ([constr-decl (term any)])
+        (dict-set d (first constr-decl) (third constr-decl)))))])
 
+;; Merge two inductive declarations
 (define-metafunction ttL
   Δ-union : Δ Δ -> Δ
-  [(Δ-union Δ ∅) Δ]
-  [(Δ-union Δ_2 (Δ_1 (x : t any)))
-   ((Δ-union Δ_2 Δ_1) (x : t any))])
+  [(Δ-union Δ_1 Δ_2)
+   ,(for/fold ([d (term Δ_1)])
+              ([(k v) (in-dict (term Δ_2))])
+      (dict-set d k v (thunk (error 'curnel "~a is already declared in ~a" k d))))])
 
 ;; Returns the inductively defined type that x constructs
-;; NB: Depends on clause order
 (define-metafunction ttL
   Δ-key-by-constructor : Δ x -> x
-  [(Δ-key-by-constructor (Δ (x : t ((x_0 : t_0) ... (x_c : t_c) (x_1 : t_1) ...))) x_c)
-   x]
-  [(Δ-key-by-constructor (Δ (x_1 : t_1 any)) x)
-   (Δ-key-by-constructor Δ x)])
+  [(Δ-key-by-constructor Δ x_c)
+   ,(for/or ([(k v) (in-dict (term Δ))])
+      (and (dict-has-key? (inductive-decl-constr-dict v)) 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
-  ;; NB: Depends on clause order
-  [(Δ-ref-constructor-map ∅ x_D) #f]
-  [(Δ-ref-constructor-map (Δ (x_D : t_D any)) x_D)
-   any]
-  [(Δ-ref-constructor-map (Δ (x_1 : t_1 any)) x_D)
-   (Δ-ref-constructor-map Δ x_D)])
-
-;; 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)])
+  [(Δ-ref-constructor-map Δ x_D)
+   ,(cond
+      [(dict-ref (term Δ) (term x_D) (thunk #f)) =>
+       (lambda (x)
+         (for/list ([(k v) (inductive-decl-constr-dict x)])
+           `(,k : ,v)))]
+      [else #f])])
 
 ;; 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 Δ x_D)
+   ,(dict-keys (inductive-decl-constr-dict (dict-ref (term Δ) (term x_D))))])
 
 ;; NB: Depends on clause order
 (define-metafunction ttL
@@ -182,13 +192,11 @@
 ;; TODO: Might be worth it to actually maintain the above bijections, for performance reasons.
 
 ;; Return the parameters of x_D as a telescope Ξ
-;; TODO: Define generic traversals of Δ and Γ ?
 (define-metafunction tt-ctxtL
   Δ-ref-parameter-Ξ : Δ x -> Ξ
-  [(Δ-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_D)
+   Ξ
+   (where (in-hole Ξ U) (Δ-ref-type Δ x_D))])
 
 ;; Applies the term t to the telescope Ξ.
 ;; TODO: Test
@@ -390,7 +398,7 @@
 (define E? (redex-match? tt-redL E))
 (define v? (redex-match? tt-redL v))
 
-(define current-Δ (make-parameter (term ∅)))
+(define current-Δ (make-parameter (make-empty-Δ)))
 (define tt-->
   (reduction-relation tt-redL
     (--> (in-hole E ((λ (x : t_0) t_1) t_2))
@@ -532,25 +540,29 @@
   #:mode (wf I I)
   #:contract (wf Δ Γ)
 
-  [----------------- "WF-Empty"
-   (wf ∅ ∅)]
+  [(side-condition ,(empty-Δ? (term Δ)))
+   ----------------- "WF-Empty"
+   (wf Δ ∅)]
 
   [(type-infer Δ Γ t t_0)
    (wf Δ Γ)
    ----------------- "WF-Var"
    (wf Δ (Γ x : t))]
 
-  [(wf Δ ∅)
+  [(where x_D ,(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 (Δ (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 Δ_1 ∅)])
 
 ;; TODO: Bi-directional and inference?
 ;; TODO: http://www.cs.ox.ac.uk/ralf.hinze/WG2.8/31/slides/stephanie.pdf
@@ -605,3 +617,12 @@
    (equivalent Δ t t_0)
    ----------------- "DTR-Check"
    (type-check Δ Γ e t)])
+
+
+(module+ test
+  (require rackunit)
+  (define-term Δt (Δ-set ,(make-empty-Δ) True Type ((T : True))))
+  (check-false
+   (judgment-holds (type-check ,(make-empty-Δ) ∅ T True)))
+  (check-true
+   (judgment-holds (type-check Δt ∅ T True))))
diff --git a/cur-lib/cur/curnel/hybrid-lang.rkt b/cur-lib/cur/curnel/hybrid-lang.rkt
new file mode 100644
index 0000000..2bc4bc7
--- /dev/null
+++ b/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))]))