blob: d82740cb4eadd559e5a4190a565b373a6d33cceb (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
|
Require Import Coq.Lists.List.
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Named.Context.
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.
|
