Remove stuff from Reflection/Named/Syntax

5 files changed, 145 insertions, 173 deletions

diff --git a/src/Reflection/Named/DeadCodeElimination.v b/src/Reflection/Named/DeadCodeElimination.v
index d48c0bbbe..d97c36742 100644
--- a/src/Reflection/Named/DeadCodeElimination.v
+++ b/src/Reflection/Named/DeadCodeElimination.v
@@ -3,6 +3,7 @@ Require Import Coq.PArith.BinPos Coq.Lists.List.
 Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Reflection.Named.Compile.
 Require Import Crypto.Reflection.Named.RegisterAssign.
+Require Import Crypto.Reflection.Named.PositiveContext.
 Require Import Crypto.Reflection.Named.EstablishLiveness.
 Require Import Crypto.Reflection.CountLets.
 Require Import Crypto.Reflection.Syntax.
@@ -56,8 +57,8 @@ Section language.
     : option (nexpr t)
     := let e := compile (Name:=positive) (e _) (List.map Pos.of_nat (seq 1 (CountBinders e))) in
        match e with
-       | Some e => Let_In (insert_dead_names None e ls) (* help vm_compute by factoring this out *)
-                          (fun names => register_reassign Pos.eqb empty empty e names)
+       | Some e => Let_In (insert_dead_names (Context:=PositiveContext_nd) None e ls) (* help vm_compute by factoring this out *)
+                          (fun names => register_reassign (InContext:=PositiveContext_nd) (ReverseContext:=Context) Pos.eqb empty empty e names)
        | None => None
        end.
 End language.
diff --git a/src/Reflection/Named/FMapContext.v b/src/Reflection/Named/FMapContext.v
index 3ef3946ca..d3d94235d 100644
--- a/src/Reflection/Named/FMapContext.v
+++ b/src/Reflection/Named/FMapContext.v
@@ -52,6 +52,17 @@ Module FMapContextFun (E : DecidableType) (W : WSfun E).
                      | rewrite base_type_code_lb in * by reflexivity ].
     Qed.
   End ctx.
+
+  Section ctx_nd.
+    Context {base_type_code var : Type}.
+
+    Definition FMapContext_nd : @Context base_type_code W.key (fun _ => var)
+      := {| ContextT := W.t var;
+            lookupb ctx n t := W.find n ctx;
+            extendb ctx n t v := W.add n v ctx;
+            removeb ctx n t := W.remove n ctx;
+            empty := W.empty _ |}.
+  End ctx_nd.
 End FMapContextFun.
 
 Module FMapContext (W : WS) := FMapContextFun W.E W.
diff --git a/src/Reflection/Named/PositiveContext.v b/src/Reflection/Named/PositiveContext.v
index 6cf81cba6..4356a174a 100644
--- a/src/Reflection/Named/PositiveContext.v
+++ b/src/Reflection/Named/PositiveContext.v
@@ -4,5 +4,6 @@ Require Import Crypto.Reflection.Named.FMapContext.
 
 Module PositiveContext := FMapContext PositiveMap.
 Notation PositiveContext := PositiveContext.FMapContext.
+Notation PositiveContext_nd := PositiveContext.FMapContext_nd.
 Definition PositiveContextOk := PositiveContext.FMapContextOk (fun x y pf => pf).
 Global Existing Instance PositiveContextOk.
diff --git a/src/Reflection/Named/RegisterAssign.v b/src/Reflection/Named/RegisterAssign.v
index 70ee5a203..18e15519a 100644
--- a/src/Reflection/Named/RegisterAssign.v
+++ b/src/Reflection/Named/RegisterAssign.v
@@ -1,6 +1,6 @@
 (** * Reassign registers *)
-Require Import Coq.FSets.FMapPositive Coq.PArith.BinPos.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Named.PositiveContext.
 Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Reflection.Named.NameUtil.
 Require Import Crypto.Util.Decidable.
@@ -82,37 +82,7 @@ Section language.
               end
          end.
   End internal.
-
-  Section context_pos.
-    Global Instance pos_context {decR : DecidableRel (@eq base_type_code)}
-           (var : base_type_code -> Type) : Context positive var
-      := { ContextT := PositiveMap.t { t : _ & var t };
-           lookupb ctx key t := match PositiveMap.find key ctx with
-                                | Some v => match dec (projT1 v = t) with
-                                            | left pf => Some match pf in (_ = t) return var t with
-                                                              | eq_refl => projT2 v
-                                                              end
-                                            | right _ => None
-                                            end
-                                | None => None
-                                end;
-           extendb ctx key t v := PositiveMap.add key (existT _ t v) ctx;
-           removeb ctx key t := if dec (option_map (@projT1 _ _) (PositiveMap.find key ctx) = Some t)
-                                then PositiveMap.remove key ctx
-                                else ctx;
-           empty := PositiveMap.empty _ }.
-    Global Instance pos_context_nd
-           (var : Type)
-      : Context positive (fun _ : base_type_code => var)
-      := { ContextT := PositiveMap.t var;
-           lookupb ctx key t := PositiveMap.find key ctx;
-           extendb ctx key t v := PositiveMap.add key v ctx;
-           removeb ctx key t := PositiveMap.remove key ctx;
-           empty := PositiveMap.empty _ }.
-  End context_pos.
 End language.
 
-Global Arguments pos_context {_ _} var.
-Global Arguments pos_context_nd : clear implicits.
 Global Arguments register_reassign {_ _ _ _ _ _} _ ctxi ctxr {t} e _.
 Global Arguments register_reassignf {_ _ _ _ _ _} _ ctxi ctxr {t} e _.
diff --git a/src/Reflection/Named/Syntax.v b/src/Reflection/Named/Syntax.v
index 1f171e9af..ff1710aae 100644
--- a/src/Reflection/Named/Syntax.v
+++ b/src/Reflection/Named/Syntax.v
@@ -6,8 +6,9 @@ Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
+Require Import Crypto.Util.LetIn.
 
-Class Context {base_type_code} (Name : Type) (var : base_type_code -> Type) :=
+Record Context {base_type_code} (Name : Type) (var : base_type_code -> Type) :=
   { ContextT : Type;
     lookupb : ContextT -> Name -> forall {t : base_type_code}, option (var t);
     extendb : ContextT -> Name -> forall {t : base_type_code}, var t -> ContextT;
@@ -36,146 +37,136 @@ Module Export Named.
     Local Notation interp_flat_type_gen := interp_flat_type.
     Local Notation interp_flat_type := (interp_flat_type interp_base_type).
 
-
-    Section expr_param.
-      Section expr.
-        Inductive exprf : flat_type -> Type :=
-        | TT : exprf Unit
-        | Var {t : base_type_code} : Name -> exprf (Tbase t)
-        | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR
-        | LetIn : forall {tx}, interp_flat_type_gen (fun _ => Name) tx -> exprf tx -> forall {tC}, exprf tC -> exprf tC
-        | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2).
-        Bind Scope nexpr_scope with exprf.
-        Inductive expr : type -> Type :=
-        | Abs {src dst} : interp_flat_type_gen (fun _ => Name) src -> exprf dst -> expr (Arrow src dst).
-        Bind Scope nexpr_scope with expr.
-        (** [SmartVar] is like [Var], except that it inserts
-          pair-projections and [Pair] as necessary to handle
-          [flat_type], and not just [base_type_code] *)
-        Definition SmartVar {t} : interp_flat_type_gen (fun _ => Name) t -> exprf t
-          := smart_interp_flat_map (f:=fun _ => Name) (g:=exprf) (fun t => Var) TT (fun A B x y => Pair x y).
-      End expr.
-
-      Section with_context.
-        Context {var : base_type_code -> Type}
-                {Context : Context Name var}.
-
-        Fixpoint extend (ctx : Context) {t : flat_type}
-                 (n : interp_flat_type_gen (fun _ => Name) t) (v : interp_flat_type_gen var t)
-          : Context
-          := match t return interp_flat_type_gen (fun _ => Name) t -> interp_flat_type_gen var t -> Context with
-             | Tbase t => fun n v => extendb ctx n v
-             | Unit => fun _ _ => ctx
-             | Prod A B => fun n v
-                           => let ctx := @extend ctx A (fst n) (fst v) in
-                              let ctx := @extend ctx B (snd n) (snd v) in
-                              ctx
-             end n v.
-
-        Fixpoint remove (ctx : Context) {t : flat_type}
-                 (n : interp_flat_type_gen (fun _ => Name) t)
-          : Context
-          := match t return interp_flat_type_gen (fun _ => Name) t -> Context with
-             | Tbase t => fun n => removeb ctx n t
-             | Unit => fun _ => ctx
-             | Prod A B => fun n
-                           => let ctx := @remove ctx A (fst n) in
-                              let ctx := @remove ctx B (snd n) in
-                              ctx
-             end n.
-
-        Definition lookup (ctx : Context) {t}
-          : interp_flat_type_gen (fun _ => Name) t -> option (interp_flat_type_gen var t)
-          := smart_interp_flat_map
-               (g := fun t => option (interp_flat_type_gen var t))
-               (fun t v => lookupb ctx v)
-               (Some tt)
-               (fun A B x y => match x, y with
-                               | Some x', Some y' => Some (x', y')%core
-                               | _, _ => None
-                               end).
-
-        Section wf.
-          Fixpoint wff (ctx : Context) {t} (e : exprf t) : option pointed_Prop
-            := match e with
-               | TT => Some trivial
-               | Var t n => match lookupb ctx n t return bool with
-                            | Some _ => true
-                            | None => false
-                            end
-               | Op _ _ op args => @wff ctx _ args
-               | LetIn _ n ex _ eC => @wff ctx _ ex /\ inject (forall v, prop_of_option (@wff (extend ctx n v) _ eC))
-               | Pair _ ex _ ey => @wff ctx _ ex /\ @wff ctx _ ey
-               end%option_pointed_prop.
-
-          Definition wf (ctx : Context) {t} (e : expr t) : Prop
-            := match e with
-               | Abs src _ n f => forall v, prop_of_option (@wff (extend ctx (t:=src) n v) _ f)
-               end.
-        End wf.
-
-        Section interp_gen.
-          Context (output_interp_flat_type : flat_type -> Type)
-                  (interp_tt : output_interp_flat_type Unit)
-                  (interp_var : forall t, var t -> output_interp_flat_type (Tbase t))
-                  (interp_op : forall src dst, op src dst -> output_interp_flat_type src -> output_interp_flat_type dst)
-                  (interp_let : forall (tx : flat_type) (ex : output_interp_flat_type tx)
-                                       tC (eC : interp_flat_type_gen var tx -> output_interp_flat_type tC),
-                      output_interp_flat_type tC)
-                  (interp_pair : forall (tx : flat_type) (ex : output_interp_flat_type tx)
-                                        (ty : flat_type) (ey : output_interp_flat_type ty),
-                      output_interp_flat_type (Prod tx ty)).
-
-          Fixpoint interp_genf (ctx : Context) {t} (e : exprf t)
-            : prop_of_option (wff ctx e) -> output_interp_flat_type t
-            := match e in exprf t return prop_of_option (wff ctx e) -> output_interp_flat_type t with
-               | TT => fun _ => interp_tt
-               | Var t' x => match lookupb ctx x t' as v
-                                   return prop_of_option (match v return bool with
-                                                          | Some _ => true
-                                                          | None => false
-                                                          end)
-                                          -> output_interp_flat_type (Tbase t')
-                             with
-                             | Some v => fun _ => interp_var _ v
-                             | None => fun bad => match bad : False with end
-                             end
-               | Op _ _ op args => fun good => @interp_op _ _ op (@interp_genf ctx _ args good)
-               | LetIn _ n ex _ eC => fun good => let goodxC := proj1 (@prop_of_option_and _ _) good in
-                                                  let x := @interp_genf ctx _ ex (proj1 goodxC) in
-                                                  interp_let _ x _ (fun x => @interp_genf (extend ctx n x) _ eC (proj2 goodxC x))
-               | Pair _ ex _ ey => fun good => let goodxy := proj1 (@prop_of_option_and _ _) good in
-                                               let x := @interp_genf ctx _ ex (proj1 goodxy) in
-                                               let y := @interp_genf ctx _ ey (proj2 goodxy) in
-                                               interp_pair _ x _ y
-               end.
-        End interp_gen.
-      End with_context.
-
-      Section with_val_context.
-        Context (Context : Context Name interp_base_type)
-                (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
-        Definition interpf
-          : forall (ctx : Context) {t} (e : exprf t),
-            prop_of_option (wff ctx e) -> interp_flat_type t
-          := @interp_genf
-               interp_base_type Context interp_flat_type
-               tt (fun _ x => x) interp_op (fun _ y _ f => let x := y in f x)
-               (fun _ x _ y => (x, y)%core).
-
-        Definition interp (ctx : Context) {t} (e : expr t)
-          : wf ctx e -> interp_type t
-          := match e in expr t return wf ctx e -> interp_type t with
-             | Abs _ _ n f => fun good v => @interpf _ _ f (good v)
+    Inductive exprf : flat_type -> Type :=
+    | TT : exprf Unit
+    | Var {t : base_type_code} : Name -> exprf (Tbase t)
+    | Op {t1 tR} : op t1 tR -> exprf t1 -> exprf tR
+    | LetIn : forall {tx}, interp_flat_type_gen (fun _ => Name) tx -> exprf tx -> forall {tC}, exprf tC -> exprf tC
+    | Pair : forall {t1}, exprf t1 -> forall {t2}, exprf t2 -> exprf (Prod t1 t2).
+    Bind Scope nexpr_scope with exprf.
+    Inductive expr : type -> Type :=
+    | Abs {src dst} : interp_flat_type_gen (fun _ => Name) src -> exprf dst -> expr (Arrow src dst).
+    Bind Scope nexpr_scope with expr.
+    Definition Abs_name {t} (e : expr t) : interp_flat_type_gen (fun _ => Name) (domain t)
+      := match e with Abs _ _ n f => n end.
+    Definition invert_Abs {t} (e : expr t) : exprf (codomain t)
+      := match e with Abs _ _ n f => f end.
+
+    Section with_context.
+      Context {var : base_type_code -> Type}
+              {Context : Context Name var}.
+
+      Fixpoint extend (ctx : Context) {t : flat_type}
+               (n : interp_flat_type_gen (fun _ => Name) t) (v : interp_flat_type_gen var t)
+        : Context
+        := match t return interp_flat_type_gen (fun _ => Name) t -> interp_flat_type_gen var t -> Context with
+           | Tbase t => fun n v => extendb ctx n v
+           | Unit => fun _ _ => ctx
+           | Prod A B => fun n v
+                         => let ctx := @extend ctx A (fst n) (fst v) in
+                            let ctx := @extend ctx B (snd n) (snd v) in
+                            ctx
+           end n v.
+
+      Fixpoint remove (ctx : Context) {t : flat_type}
+               (n : interp_flat_type_gen (fun _ => Name) t)
+        : Context
+        := match t return interp_flat_type_gen (fun _ => Name) t -> Context with
+           | Tbase t => fun n => removeb ctx n t
+           | Unit => fun _ => ctx
+           | Prod A B => fun n
+                         => let ctx := @remove ctx A (fst n) in
+                            let ctx := @remove ctx B (snd n) in
+                            ctx
+           end n.
+
+      Definition lookup (ctx : Context) {t}
+        : interp_flat_type_gen (fun _ => Name) t -> option (interp_flat_type_gen var t)
+        := smart_interp_flat_map
+             (g := fun t => option (interp_flat_type_gen var t))
+             (fun t v => lookupb ctx v)
+             (Some tt)
+             (fun A B x y => match x, y with
+                             | Some x', Some y' => Some (x', y')%core
+                             | _, _ => None
+                             end).
+    End with_context.
+
+    Section with_val_context.
+      Context (Context : Context Name interp_base_type)
+              (interp_op : forall src dst, op src dst -> interp_flat_type src -> interp_flat_type dst).
+
+      Fixpoint interpf
+               (ctx : Context) {t} (e : exprf t)
+        : option (interp_flat_type t)
+        := match e in exprf t return option (interp_flat_type t) with
+           | Var t' x => lookupb ctx x t'
+           | TT => Some tt
+           | Pair _ ex _ ey
+             => match @interpf ctx _ ex, @interpf ctx _ ey with
+                | Some xv, Some yv => Some (xv, yv)%core
+                | None, _ | _, None => None
+                end
+           | Op _ _ opc args
+             => option_map (@interp_op _ _ opc) (@interpf ctx _ args)
+           | LetIn _ n ex _ eC
+             => match @interpf ctx _ ex with
+                | Some xv
+                  => dlet x := xv in
+                     @interpf (extend ctx n x) _ eC
+                | None => None
+                end
+           end.
+
+      Definition interp (ctx : Context) {t} (e : expr t)
+        : interp_flat_type (domain t) -> option (interp_flat_type (codomain t))
+        := fun v => @interpf (extend ctx (Abs_name e) v) _ (invert_Abs e).
+    End with_val_context.
+(*
+      Section interp_gen.
+        Context (output_interp_flat_type : flat_type -> Type)
+                (interp_tt : output_interp_flat_type Unit)
+                (interp_var : forall t, var t -> output_interp_flat_type (Tbase t))
+                (interp_op : forall src dst, op src dst -> output_interp_flat_type src -> output_interp_flat_type dst)
+                (interp_let : forall (tx : flat_type) (ex : output_interp_flat_type tx)
+                                     tC (eC : interp_flat_type_gen var tx -> output_interp_flat_type tC),
+                    output_interp_flat_type tC)
+                (interp_pair : forall (tx : flat_type) (ex : output_interp_flat_type tx)
+                                      (ty : flat_type) (ey : output_interp_flat_type ty),
+                    output_interp_flat_type (Prod tx ty)).
+
+        Fixpoint interp_genf (ctx : Context) {t} (e : exprf t)
+          : prop_of_option (wff ctx e) -> output_interp_flat_type t
+          := match e in exprf t return prop_of_option (wff ctx e) -> output_interp_flat_type t with
+             | TT => fun _ => interp_tt
+             | Var t' x => match lookupb ctx x t' as v
+                                 return prop_of_option (match v return bool with
+                                                        | Some _ => true
+                                                        | None => false
+                                                        end)
+                                        -> output_interp_flat_type (Tbase t')
+                           with
+                           | Some v => fun _ => interp_var _ v
+                           | None => fun bad => match bad : False with end
+                           end
+             | Op _ _ op args => fun good => @interp_op _ _ op (@interp_genf ctx _ args good)
+             | LetIn _ n ex _ eC => fun good => let goodxC := proj1 (@prop_of_option_and _ _) good in
+                                                let x := @interp_genf ctx _ ex (proj1 goodxC) in
+                                                interp_let _ x _ (fun x => @interp_genf (extend ctx n x) _ eC (proj2 goodxC x))
+             | Pair _ ex _ ey => fun good => let goodxy := proj1 (@prop_of_option_and _ _) good in
+                                             let x := @interp_genf ctx _ ex (proj1 goodxy) in
+                                             let y := @interp_genf ctx _ ey (proj2 goodxy) in
+                                             interp_pair _ x _ y
              end.
-      End with_val_context.
-    End expr_param.
+      End interp_gen.
+    End with_context.
+
+    End expr_param.*)
   End language.
 End Named.
 
 Global Arguments TT {_ _ _}.
 Global Arguments Var {_ _ _ _} _.
-Global Arguments SmartVar {_ _ _ _} _.
 Global Arguments Op {_ _ _ _ _} _ _.
 Global Arguments LetIn {_ _ _} _ _ _ {_} _.
 Global Arguments Pair {_ _ _ _} _ {_} _.
@@ -183,11 +174,9 @@ Global Arguments Abs {_ _ _ _ _} _ _.
 Global Arguments extend {_ _ _ _} ctx {_} _ _.
 Global Arguments remove {_ _ _ _} ctx {_} _.
 Global Arguments lookup {_ _ _ _} ctx {_} _, {_ _ _ _} ctx _ _.
-Global Arguments wff {_ _ _ _ _} ctx {t} _.
-Global Arguments wf {_ _ _ _ _} ctx {t} _.
-Global Arguments interp_genf {_ _ _ var _} _ _ _ _ _ _ {ctx t} _ _.
-Global Arguments interpf {_ _ _ _ _ interp_op ctx t} _ _.
-Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _ _.
+(*Global Arguments interp_genf {_ _ _ var _} _ _ _ _ _ _ {ctx t} _ _.*)
+Global Arguments interpf {_ _ _ _ _ interp_op ctx t} _.
+Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _.
 
 Notation "'slet' x := A 'in' b" := (LetIn _ x A%nexpr b%nexpr) : nexpr_scope.
 Notation "'λn'  x .. y , t" := (Abs x .. (Abs y t%nexpr) .. ) : nexpr_scope.