Add FMapContext, PositiveContext

Also copy some definitions from Syntax out of it, in prep for removing
them

4 files changed, 150 insertions, 0 deletions

diff --git a/src/Reflection/Named/FMapContext.v b/src/Reflection/Named/FMapContext.v
new file mode 100644
index 000000000..3ef3946ca
--- /dev/null
+++ b/src/Reflection/Named/FMapContext.v
@@ -0,0 +1,57 @@
+Require Import Coq.Bool.Sumbool.
+Require Import Coq.FSets.FMapInterface.
+Require Import Coq.FSets.FMapFacts.
+Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Reflection.Named.Wf.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Equality.
+
+Module FMapContextFun (E : DecidableType) (W : WSfun E).
+  Module Import Properties := WProperties_fun E W.
+  Import F.
+  Section ctx.
+    Context (E_eq_l : forall x y, E.eq x y -> x = y)
+            base_type_code (var : base_type_code -> Type)
+            (base_type_code_beq : base_type_code -> base_type_code -> bool)
+            (base_type_code_bl_transparent : forall x y, base_type_code_beq x y = true -> x = y)
+            (base_type_code_lb : forall x y, x = y -> base_type_code_beq x y = true).
+
+    Definition var_cast {a b} (x : var a) : option (var b)
+      := match Sumbool.sumbool_of_bool (base_type_code_beq a b), Sumbool.sumbool_of_bool (base_type_code_beq b b) with
+         | left pf, left pf' => match eq_trans (base_type_code_bl_transparent _ _ pf) (eq_sym (base_type_code_bl_transparent _ _ pf')) with
+                                | eq_refl => Some x
+                                end
+         | right _, _ | _, right _ => None
+         end.
+    Definition FMapContext : @Context base_type_code W.key var
+      := {| ContextT := W.t { t : _ & var t };
+            lookupb ctx n t
+            := match W.find n ctx with
+               | Some (existT t' v)
+                 => var_cast v
+               | None => None
+               end;
+            extendb ctx n t v
+            := W.add n (existT _ t v) ctx;
+            removeb ctx n t
+            := W.remove n ctx;
+            empty := W.empty _ |}.
+    Lemma FMapContextOk : @ContextOk base_type_code W.key var FMapContext.
+    Proof.
+      split;
+        repeat first [ reflexivity
+                     | progress simpl in *
+                     | progress intros
+                     | rewrite add_eq_o by reflexivity
+                     | progress rewrite ?add_neq_o, ?remove_neq_o in * by intuition
+                     | progress rewrite empty_o in *
+                     | progress unfold var_cast
+                     | progress break_innermost_match_step
+                     | rewrite concat_pV
+                     | congruence
+                     | rewrite base_type_code_lb in * by reflexivity ].
+    Qed.
+  End ctx.
+End FMapContextFun.
+
+Module FMapContext (W : WS) := FMapContextFun W.E W.
diff --git a/src/Reflection/Named/PositiveContext.v b/src/Reflection/Named/PositiveContext.v
new file mode 100644
index 000000000..6cf81cba6
--- /dev/null
+++ b/src/Reflection/Named/PositiveContext.v
@@ -0,0 +1,8 @@
+Require Import Coq.FSets.FMapPositive.
+Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Reflection.Named.FMapContext.
+
+Module PositiveContext := FMapContext PositiveMap.
+Notation PositiveContext := PositiveContext.FMapContext.
+Definition PositiveContextOk := PositiveContext.FMapContextOk (fun x y pf => pf).
+Global Existing Instance PositiveContextOk.
diff --git a/src/Reflection/Named/SmartMap.v b/src/Reflection/Named/SmartMap.v
new file mode 100644
index 000000000..3cacf7a1b
--- /dev/null
+++ b/src/Reflection/Named/SmartMap.v
@@ -0,0 +1,20 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Reflection.Named.Syntax.
+
+Module Export Named.
+  Section language.
+    Context {base_type_code : Type}
+            {interp_base_type : base_type_code -> Type}
+            {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+            {Name : Type}.
+
+    (** [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 (fun _ => Name) t -> @exprf base_type_code op Name t
+      := smart_interp_flat_map (f:=fun _ => Name) (g:=@exprf _ _ _) (fun t => Var) TT (fun A B x y => Pair x y).
+  End language.
+End Named.
+
+Global Arguments SmartVar {_ _ _ _} _.
diff --git a/src/Reflection/Named/Wf.v b/src/Reflection/Named/Wf.v
new file mode 100644
index 000000000..87d84a07f
--- /dev/null
+++ b/src/Reflection/Named/Wf.v
@@ -0,0 +1,65 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Named.Syntax.
+Require Import Crypto.Util.PointedProp.
+
+Section with_context.
+  Context {base_type_code Name var} (Context : @Context base_type_code Name var).
+
+  Class ContextOk :=
+    { lookupb_extendb_same
+      : forall (ctx : Context) n t v, lookupb (extendb ctx n (t:=t) v) n t = Some v;
+      lookupb_extendb_different
+      : forall (ctx : Context) n n' t t' v, n <> n' -> lookupb (extendb ctx n (t:=t) v) n' t'
+                                                                                 = lookupb ctx n' t';
+      lookupb_extendb_wrong_type
+      : forall (ctx : Context) n t t' v, t <> t' -> lookupb (extendb ctx n (t:=t) v) n t' = None;
+      lookupb_removeb
+      : forall (ctx : Context) n n' t t', n <> n' -> lookupb (removeb ctx n t) n' t'
+                                                                     = lookupb ctx n' t';
+      lookupb_empty
+      : forall n t, lookupb (@empty _ _ _ Context) n t = None }.
+
+  Context (ContextOk : ContextOk).
+
+  Lemma lookupb_eq_cast
+    : forall (ctx : Context) n t t' (pf : t = t'),
+      lookupb ctx n t' = option_map (fun v => eq_rect _ var v _ pf) (lookupb ctx n t).
+  Proof.
+    intros; subst; edestruct lookupb; reflexivity.
+  Defined.
+  Lemma lookupb_extendb_eq
+    : forall (ctx : Context) n t t' (pf : t = t') v,
+      lookupb (extendb ctx n (t:=t) v) n t' = Some (eq_rect _ var v _ pf).
+  Proof.
+    intros; subst; apply lookupb_extendb_same; assumption.
+  Defined.
+End with_context.
+
+Module Export Named.
+  Section language.
+    Context {base_type_code Name var}
+            {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+            (Context : @Context base_type_code Name var)
+            (ContextOk : @ContextOk base_type_code Name var Context).
+
+    Fixpoint wff (ctx : Context) {t} (e : @exprf base_type_code op Name 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 base_type_code op Name t) : Prop
+      := match e with
+         | Abs src _ n f => forall v, prop_of_option (@wff (extend ctx (t:=src) n v) _ f)
+         end.
+  End language.
+End Named.
+
+Global Arguments wff {_ _ _ _ _} ctx {t} _.
+Global Arguments wf {_ _ _ _ _} ctx {t} _.