Split off Compilers.Named.Context

28 files changed, 93 insertions, 66 deletions

diff --git a/_CoqProject b/_CoqProject
index e0e88e441..d266f8fcf 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -86,6 +86,7 @@ src/Compilers/Named/Compile.v
 src/Compilers/Named/CompileInterp.v
 src/Compilers/Named/CompileProperties.v
 src/Compilers/Named/CompileWf.v
+src/Compilers/Named/Context.v
 src/Compilers/Named/ContextDefinitions.v
 src/Compilers/Named/ContextOn.v
 src/Compilers/Named/ContextProperties.v
diff --git a/src/Compilers/MapCastByDeBruijn.v b/src/Compilers/MapCastByDeBruijn.v
index 0964847a6..0eb137a06 100644
--- a/src/Compilers/MapCastByDeBruijn.v
+++ b/src/Compilers/MapCastByDeBruijn.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.MapCast.
 Require Import Crypto.Compilers.Named.InterpretToPHOAS.
diff --git a/src/Compilers/MapCastByDeBruijnInterp.v b/src/Compilers/MapCastByDeBruijnInterp.v
index 5d8156f09..10e09242a 100644
--- a/src/Compilers/MapCastByDeBruijnInterp.v
+++ b/src/Compilers/MapCastByDeBruijnInterp.v
@@ -1,6 +1,7 @@
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Wf.
 Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Compilers.Named.MapCastInterp.
diff --git a/src/Compilers/MapCastByDeBruijnWf.v b/src/Compilers/MapCastByDeBruijnWf.v
index 7bc58042f..7c1e386b5 100644
--- a/src/Compilers/MapCastByDeBruijnWf.v
+++ b/src/Compilers/MapCastByDeBruijnWf.v
@@ -1,6 +1,7 @@
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Wf.
 Require Import Crypto.Compilers.Relations.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Compilers.Named.MapCastWf.
diff --git a/src/Compilers/Named/CompileInterp.v b/src/Compilers/Named/CompileInterp.v
index 1c7e42258..9368900e4 100644
--- a/src/Compilers/Named/CompileInterp.v
+++ b/src/Compilers/Named/CompileInterp.v
@@ -1,4 +1,5 @@
 (** * PHOAS → Named Representation of Gallina *)
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.NameUtil.
 Require Import Crypto.Compilers.Named.NameUtilProperties.
diff --git a/src/Compilers/Named/CompileWf.v b/src/Compilers/Named/CompileWf.v
index aea8cb2b1..b04c207d2 100644
--- a/src/Compilers/Named/CompileWf.v
+++ b/src/Compilers/Named/CompileWf.v
@@ -1,4 +1,5 @@
 (** * PHOAS → Named Representation of Gallina *)
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.Wf.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
diff --git a/src/Compilers/Named/Context.v b/src/Compilers/Named/Context.v
new file mode 100644
index 000000000..ba0ad6feb
--- /dev/null
+++ b/src/Compilers/Named/Context.v
@@ -0,0 +1,65 @@
+(** * Contexts for Named Representation of Gallina *)
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Util.Notations.
+
+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;
+    removeb : ContextT -> Name -> base_type_code -> ContextT;
+    empty : ContextT }.
+Coercion ContextT : Context >-> Sortclass.
+Arguments ContextT {_ _ _ _}, {_ _ _} _.
+Arguments lookupb {_ _ _ _} _ _ {_}, {_ _ _ _} _ _ _.
+Arguments extendb {_ _ _ _} _ _ [_] _.
+Arguments removeb {_ _ _ _} _ _ _.
+Arguments empty {_ _ _ _}.
+
+Section language.
+  Context {base_type_code : Type}
+          {Name : Type}
+          {var : base_type_code -> Type}
+          {Context : Context Name var}.
+
+  Local Notation flat_type := (flat_type base_type_code).
+
+  Fixpoint extend (ctx : Context) {t : flat_type}
+           (n : interp_flat_type (fun _ => Name) t) (v : interp_flat_type var t)
+    : Context
+    := match t return interp_flat_type (fun _ => Name) t -> interp_flat_type 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 (fun _ => Name) t)
+    : Context
+    := match t return interp_flat_type (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 (fun _ => Name) t -> option (interp_flat_type var t)
+    := smart_interp_flat_map
+         (g := fun t => option (interp_flat_type 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 language.
+
+Global Arguments extend {_ _ _ _} ctx {_} _ _.
+Global Arguments remove {_ _ _ _} ctx {_} _.
+Global Arguments lookup {_ _ _ _} ctx {_} _, {_ _ _ _} ctx _ _.
diff --git a/src/Compilers/Named/ContextDefinitions.v b/src/Compilers/Named/ContextDefinitions.v
index 6e1a3e64a..386a1a363 100644
--- a/src/Compilers/Named/ContextDefinitions.v
+++ b/src/Compilers/Named/ContextDefinitions.v
@@ -1,5 +1,5 @@
 Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Decidable.
 
diff --git a/src/Compilers/Named/ContextOn.v b/src/Compilers/Named/ContextOn.v
index 6c06d3fbe..5e51f7585 100644
--- a/src/Compilers/Named/ContextOn.v
+++ b/src/Compilers/Named/ContextOn.v
@@ -1,5 +1,5 @@
 (** * Transfer [Context] across an injection *)
-Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 
 Section language.
   Context {base_type_code Name1 Name2 : Type}
diff --git a/src/Compilers/Named/ContextProperties.v b/src/Compilers/Named/ContextProperties.v
index c2a9ca828..2f6b8d209 100644
--- a/src/Compilers/Named/ContextProperties.v
+++ b/src/Compilers/Named/ContextProperties.v
@@ -1,5 +1,5 @@
 Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Compilers.Named.ContextProperties.Tactics.
 Require Import Crypto.Util.Decidable.
diff --git a/src/Compilers/Named/ContextProperties/NameUtil.v b/src/Compilers/Named/ContextProperties/NameUtil.v
index 96653ac99..95edcff8f 100644
--- a/src/Compilers/Named/ContextProperties/NameUtil.v
+++ b/src/Compilers/Named/ContextProperties/NameUtil.v
@@ -2,7 +2,7 @@ Require Import Coq.omega.Omega.
 Require Import Crypto.Util.FixCoqMistakes.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Wf.
-Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Compilers.Named.NameUtil.
 Require Import Crypto.Compilers.Named.NameUtilProperties.
diff --git a/src/Compilers/Named/ContextProperties/SmartMap.v b/src/Compilers/Named/ContextProperties/SmartMap.v
index 7cf761a34..9018bce76 100644
--- a/src/Compilers/Named/ContextProperties/SmartMap.v
+++ b/src/Compilers/Named/ContextProperties/SmartMap.v
@@ -1,7 +1,7 @@
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.Relations.
 Require Import Crypto.Compilers.SmartMap.
-Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Compilers.Named.ContextProperties.
 Require Import Crypto.Compilers.Named.ContextProperties.Tactics.
diff --git a/src/Compilers/Named/DeadCodeElimination.v b/src/Compilers/Named/DeadCodeElimination.v
index 312370834..c2e1e8a7d 100644
--- a/src/Compilers/Named/DeadCodeElimination.v
+++ b/src/Compilers/Named/DeadCodeElimination.v
@@ -1,5 +1,6 @@
 (** * PHOAS → Named Representation of Gallina *)
 Require Import Coq.PArith.BinPos Coq.Lists.List.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.Compile.
 Require Import Crypto.Compilers.Named.RegisterAssign.
diff --git a/src/Compilers/Named/EstablishLiveness.v b/src/Compilers/Named/EstablishLiveness.v
index 5d1255af3..c2d6c273a 100644
--- a/src/Compilers/Named/EstablishLiveness.v
+++ b/src/Compilers/Named/EstablishLiveness.v
@@ -2,6 +2,7 @@
 Require Import Coq.Lists.List.
 Require Import Crypto.Compilers.Syntax.
 Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.CountLets.
 Require Import Crypto.Util.ListUtil.
diff --git a/src/Compilers/Named/FMapContext.v b/src/Compilers/Named/FMapContext.v
index 1ea45cbbe..5519881c8 100644
--- a/src/Compilers/Named/FMapContext.v
+++ b/src/Compilers/Named/FMapContext.v
@@ -1,7 +1,7 @@
 Require Import Coq.Bool.Sumbool.
 Require Import Coq.FSets.FMapInterface.
 Require Import Coq.FSets.FMapFacts.
-Require Import Crypto.Compilers.Named.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Equality.
diff --git a/src/Compilers/Named/IdContext.v b/src/Compilers/Named/IdContext.v
index 5ed1e7cf2..d82740cb4 100644
--- a/src/Compilers/Named/IdContext.v
+++ b/src/Compilers/Named/IdContext.v
@@ -1,4 +1,6 @@
+Require Import Coq.Lists.List.
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 
 Section language.
diff --git a/src/Compilers/Named/InterpretToPHOAS.v b/src/Compilers/Named/InterpretToPHOAS.v
index dc737a38d..1ccad6cad 100644
--- a/src/Compilers/Named/InterpretToPHOAS.v
+++ b/src/Compilers/Named/InterpretToPHOAS.v
@@ -1,3 +1,4 @@
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.Wf.
 Require Import Crypto.Compilers.SmartMap.
diff --git a/src/Compilers/Named/InterpretToPHOASInterp.v b/src/Compilers/Named/InterpretToPHOASInterp.v
index 0772721f6..88fb2d8a0 100644
--- a/src/Compilers/Named/InterpretToPHOASInterp.v
+++ b/src/Compilers/Named/InterpretToPHOASInterp.v
@@ -1,3 +1,4 @@
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.Wf.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
diff --git a/src/Compilers/Named/InterpretToPHOASWf.v b/src/Compilers/Named/InterpretToPHOASWf.v
index c0e59d10e..fd35ab12c 100644
--- a/src/Compilers/Named/InterpretToPHOASWf.v
+++ b/src/Compilers/Named/InterpretToPHOASWf.v
@@ -1,3 +1,4 @@
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.Wf.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
diff --git a/src/Compilers/Named/MapCast.v b/src/Compilers/Named/MapCast.v
index 83c477765..fddee84fa 100644
--- a/src/Compilers/Named/MapCast.v
+++ b/src/Compilers/Named/MapCast.v
@@ -1,6 +1,7 @@
 Require Import Coq.Bool.Sumbool.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 
 Local Open Scope nexpr_scope.
diff --git a/src/Compilers/Named/MapCastInterp.v b/src/Compilers/Named/MapCastInterp.v
index f3842e691..cb4d3062c 100644
--- a/src/Compilers/Named/MapCastInterp.v
+++ b/src/Compilers/Named/MapCastInterp.v
@@ -3,6 +3,7 @@ Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Relations.
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Compilers.Named.ContextProperties.
diff --git a/src/Compilers/Named/MapCastWf.v b/src/Compilers/Named/MapCastWf.v
index cd8a2e720..9f82004bc 100644
--- a/src/Compilers/Named/MapCastWf.v
+++ b/src/Compilers/Named/MapCastWf.v
@@ -3,6 +3,7 @@ Require Import Coq.Logic.Eqdep_dec.
 Require Import Crypto.Compilers.SmartMap.
 Require Import Crypto.Compilers.Relations.
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.ContextDefinitions.
 Require Import Crypto.Compilers.Named.ContextProperties.
diff --git a/src/Compilers/Named/RegisterAssign.v b/src/Compilers/Named/RegisterAssign.v
index d1e871fd0..869d959ec 100644
--- a/src/Compilers/Named/RegisterAssign.v
+++ b/src/Compilers/Named/RegisterAssign.v
@@ -1,5 +1,6 @@
 (** * Reassign registers *)
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.PositiveContext.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.NameUtil.
diff --git a/src/Compilers/Named/Syntax.v b/src/Compilers/Named/Syntax.v
index c58fcc9d1..0af2bb33e 100644
--- a/src/Compilers/Named/Syntax.v
+++ b/src/Compilers/Named/Syntax.v
@@ -1,26 +1,10 @@
 (** * Named Representation of Gallina *)
-Require Import Coq.Classes.RelationClasses.
 Require Import Crypto.Compilers.Syntax.
-Require Import Crypto.Compilers.SmartMap.
+Require Import Crypto.Compilers.Named.Context.
 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.
 
-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;
-    removeb : ContextT -> Name -> base_type_code -> ContextT;
-    empty : ContextT }.
-Coercion ContextT : Context >-> Sortclass.
-Arguments ContextT {_ _ _ _}, {_ _ _} _.
-Arguments lookupb {_ _ _ _} _ _ {_}, {_ _ _ _} _ _ _.
-Arguments extendb {_ _ _ _} _ _ [_] _.
-Arguments removeb {_ _ _ _} _ _ _.
-Arguments empty {_ _ _ _}.
-
 Local Open Scope ctype_scope.
 Local Open Scope expr_scope.
 Delimit Scope nexpr_scope with nexpr.
@@ -52,46 +36,6 @@ Module Export Named.
     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).
@@ -133,9 +77,6 @@ Global Arguments Pair {_ _ _ _} _ {_} _.
 Global Arguments Abs {_ _ _ _ _} _ _.
 Global Arguments invert_Abs {_ _ _ _} _.
 Global Arguments Abs_name {_ _ _ _} _.
-Global Arguments extend {_ _ _ _} ctx {_} _ _.
-Global Arguments remove {_ _ _ _} ctx {_} _.
-Global Arguments lookup {_ _ _ _} ctx {_} _, {_ _ _ _} ctx _ _.
 Global Arguments interpf {_ _ _ _ _ interp_op ctx t} _.
 Global Arguments interp {_ _ _ _ _ interp_op ctx t} _ _.
 
diff --git a/src/Compilers/Named/Wf.v b/src/Compilers/Named/Wf.v
index df2213b21..fec1de5ed 100644
--- a/src/Compilers/Named/Wf.v
+++ b/src/Compilers/Named/Wf.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Util.PointedProp.
 
diff --git a/src/Compilers/Named/WfInterp.v b/src/Compilers/Named/WfInterp.v
index b44811b06..580dcb438 100644
--- a/src/Compilers/Named/WfInterp.v
+++ b/src/Compilers/Named/WfInterp.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.Wf.
 Require Import Crypto.Util.PointedProp.
diff --git a/src/Compilers/TestCase.v b/src/Compilers/TestCase.v
index 0db93721e..229e5f869 100644
--- a/src/Compilers/TestCase.v
+++ b/src/Compilers/TestCase.v
@@ -1,5 +1,6 @@
 Require Import Coq.omega.Omega Coq.micromega.Psatz.
 Require Import Coq.PArith.BinPos Coq.Lists.List.
+Require Import Crypto.Compilers.Named.Context.
 Require Import Crypto.Compilers.Named.Syntax.
 Require Import Crypto.Compilers.Named.Compile.
 Require Import Crypto.Compilers.Named.RegisterAssign.
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index 900ac92a9..adb29e81f 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -8,6 +8,7 @@ Require Export Crypto.LegacyArithmetic.ArchitectureToZLike.
 Require Export Crypto.LegacyArithmetic.ArchitectureToZLikeProofs.
 Require Export Crypto.Util.Tuple.
 Require Import Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod.
+Require Import Crypto.Compilers.Named.Context.
 Require Export Crypto.Compilers.Named.Syntax.
 Require Export Crypto.Compilers.Named.PositiveContext.
 Require Import Crypto.Compilers.Named.DeadCodeElimination.