Add IdContext

1 files changed, 25 insertions, 0 deletions

diff --git a/src/Reflection/Named/IdContext.v b/src/Reflection/Named/IdContext.v
new file mode 100644
index 000000000..c2a6936f8
--- /dev/null
+++ b/src/Reflection/Named/IdContext.v
@@ -0,0 +1,25 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Named.Syntax.
+
+Section language.
+  Context {base_type_code Name}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          (Context : @Context base_type_code Name (fun _ => Name)).
+
+  Fixpoint collect_binders {t} (e : Named.exprf base_type_code op Name t)
+    : list { t : flat_type base_type_code & interp_flat_type (fun _ => Name) t }
+    := match e with
+       | TT => nil
+       | Var t n => (existT _ (Tbase t) n) :: nil
+       | Op t1 tR opc args => @collect_binders _ args
+       | LetIn tx n ex tC eC
+         => (existT _ tx n) :: @collect_binders tx ex ++ @collect_binders tC eC
+       | Pair tx ex ty ey
+         => @collect_binders tx ex ++ @collect_binders ty ey
+       end%list.
+  Definition idcontext {t} (e : Named.exprf base_type_code op Name t) : Context
+    := List.fold_right
+         (fun v ctx => extend ctx (projT2 v) (projT2 v))
+         empty
+         (collect_binders e).
+End language.