diff options
Diffstat (limited to 'src/Compilers/Named/IdContext.v')
-rw-r--r-- | src/Compilers/Named/IdContext.v | 25 |
1 files changed, 25 insertions, 0 deletions
diff --git a/src/Compilers/Named/IdContext.v b/src/Compilers/Named/IdContext.v new file mode 100644 index 000000000..5ed1e7cf2 --- /dev/null +++ b/src/Compilers/Named/IdContext.v @@ -0,0 +1,25 @@ +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.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. |