blob: 57b3e23653a30d7a8a4d0cf5073e81b0e49b1553 (
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
28
29
30
31
32
33
34
35
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.SmartMap.
Section language.
Context {base_type_code : Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}.
Local Notation Expr := (@Expr base_type_code op).
Local Notation expr := (@expr base_type_code op).
Local Notation exprf := (@exprf base_type_code op).
Section with_var.
Context {var : base_type_code -> Type}.
Fixpoint strip_exprf {T} (e : @exprf (fun t => @exprf var (Tbase t)) T)
: @exprf var T
:= match e with
| TT => TT
| Var t v
=> v
| Op src dst opv args
=> Op opv (strip_exprf args)
| LetIn tx ex tC eC
=> LetIn (strip_exprf ex)
(fun v => strip_exprf (eC (SmartVarVarf v)))
| Pair tx ex ty ey
=> Pair (strip_exprf ex) (strip_exprf ey)
end.
Definition strip_expr {T} (e : @expr (fun t => @exprf var (Tbase t)) T)
: @expr var T
:= match e with
| Abs src dst f => Abs (fun x => strip_exprf (f (SmartVarVarf x)))
end.
End with_var.
End language.
|
