blob: d2fbad987d9ca4e1e4fa4331db2bfafd9e3c44d6 (
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
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.InSet.Syntax.
Section language.
Context {base_type_code : Set}
{op : flat_type base_type_code -> flat_type base_type_code -> Set}
{var : base_type_code -> Set}.
Fixpoint typeify_interp_flat_type {t}
: InSet.Syntax.interp_flat_type var t -> Compilers.Syntax.interp_flat_type var t
:= match t with
| Tbase T => fun v => v
| Unit => fun v => v
| Prod A B => fun ab : InSet.Syntax.interp_flat_type _ A * InSet.Syntax.interp_flat_type _ B
=> (@typeify_interp_flat_type _ (fst ab),
@typeify_interp_flat_type _ (snd ab))
end.
Fixpoint untypeify_interp_flat_type {t}
: Compilers.Syntax.interp_flat_type var t -> InSet.Syntax.interp_flat_type var t
:= match t with
| Tbase T => fun v => v
| Unit => fun v => v
| Prod A B => fun ab : Compilers.Syntax.interp_flat_type _ A * Compilers.Syntax.interp_flat_type _ B
=> (@untypeify_interp_flat_type _ (fst ab),
@untypeify_interp_flat_type _ (snd ab))
end.
Fixpoint typeify {t} (e : @InSet.Syntax.exprf base_type_code op var t)
: @Compilers.Syntax.exprf base_type_code op var t
:= match e with
| TT => Compilers.Syntax.TT
| Var t v => Compilers.Syntax.Var v
| Op t1 tR opc args => Compilers.Syntax.Op opc (@typeify _ args)
| LetIn tx ex tC eC
=> Compilers.Syntax.LetIn
(@typeify _ ex)
(fun x => @typeify _ (eC (untypeify_interp_flat_type x)))
| Pair tx ex ty ey => Compilers.Syntax.Pair
(@typeify _ ex)
(@typeify _ ey)
end.
Fixpoint untypeify {t} (e : @Compilers.Syntax.exprf base_type_code op var t)
: @InSet.Syntax.exprf base_type_code op var t
:= match e with
| Compilers.Syntax.TT => TT
| Compilers.Syntax.Var t v => Var v
| Compilers.Syntax.Op t1 tR opc args => Op opc (@untypeify _ args)
| Compilers.Syntax.LetIn tx ex tC eC
=> LetIn
(@untypeify _ ex)
(fun x => @untypeify _ (eC (typeify_interp_flat_type x)))
| Compilers.Syntax.Pair tx ex ty ey
=> Pair
(@untypeify _ ex)
(@untypeify _ ey)
end.
End language.
|
