Add GetNames

2 files changed, 39 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 1a88c6e89..2422bb9f1 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -84,6 +84,7 @@ src/Compilers/Named/CountLets.v
 src/Compilers/Named/DeadCodeElimination.v
 src/Compilers/Named/EstablishLiveness.v
 src/Compilers/Named/FMapContext.v
+src/Compilers/Named/GetNames.v
 src/Compilers/Named/IdContext.v
 src/Compilers/Named/InterpretToPHOAS.v
 src/Compilers/Named/InterpretToPHOASInterp.v
diff --git a/src/Compilers/Named/GetNames.v b/src/Compilers/Named/GetNames.v
new file mode 100644
index 000000000..ce26b1bca
--- /dev/null
+++ b/src/Compilers/Named/GetNames.v
@@ -0,0 +1,38 @@
+Require Import Coq.Lists.List.
+Require Import Crypto.Compilers.Syntax.
+Require Import Crypto.Compilers.Named.Syntax.
+
+Local Open Scope list_scope.
+
+Section language.
+  Context {base_type_code}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {Name : Type}.
+
+  Local Notation exprf := (@exprf base_type_code op Name).
+  Local Notation expr := (@expr base_type_code op Name).
+
+  Fixpoint get_names_of_type {t} : interp_flat_type (fun _ : base_type_code => Name) t -> list Name
+    := match t with
+       | Tbase T => fun n => n::nil
+       | Unit => fun _ => nil
+       | Prod A B => fun ab : interp_flat_type _ A * interp_flat_type _ B
+                     => @get_names_of_type _ (fst ab) ++ @get_names_of_type _ (snd ab)
+       end.
+
+  Fixpoint get_namesf {t} (e : exprf t) : list Name
+    := match e with
+       | TT => nil
+       | Var _ x => x::nil
+       | Op _ _ opc args => @get_namesf _ args
+       | LetIn tx nx ex tC eC
+         => get_names_of_type nx ++ (* @get_namesf _ ex ++ *) @get_namesf _ eC
+       | Pair _ ex _ ey
+         => @get_namesf _ ex ++ @get_namesf _ ey
+       end.
+
+  Fixpoint get_names {t} (e : expr t) : list Name
+    := match e with
+       | Abs _ _ n f => get_names_of_type n ++ get_namesf f
+       end.
+End language.