blob: 4e74fc59a3ec04b16caf1ede1d0a30980f077146 (
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
59
60
61
62
63
64
65
|
Require Import Crypto.Compilers.Named.Context.
Require Import Crypto.Compilers.Named.Syntax.
Require Import Crypto.Compilers.Named.Wf.
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Util.PointedProp.
Local Notation eta_and x := (conj (let (a, b) := x in a) (let (a, b) := x in b)).
Module Export Named.
Section language.
Context {base_type_code : Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
{Name : Type}.
Section with_var.
Context {var : base_type_code -> Type}
{Context : Context Name var}
(failb : forall t, @Syntax.exprf base_type_code op var (Tbase t)).
Local Notation failf t (* : @Syntax.exprf base_type_code op var t*)
:= (SmartPairf (SmartValf _ failb t)).
Fixpoint interpf_to_phoas
(ctx : Context)
{t} (e : @Named.exprf base_type_code op Name t)
{struct e}
: @Syntax.exprf base_type_code op var t
:= match e in Named.exprf _ _ _ t return @Syntax.exprf base_type_code op var t with
| Named.Var t' x
=> match lookupb t' ctx x with
| Some v => Var v
| None => failf _
end
| Named.TT => TT
| Named.Pair tx ex ty ey
=> Pair (@interpf_to_phoas ctx tx ex) (@interpf_to_phoas ctx ty ey)
| Named.Op _ _ opc args
=> Op opc (@interpf_to_phoas ctx _ args)
| Named.LetIn _ n ex _ eC
=> LetIn (@interpf_to_phoas ctx _ ex)
(fun v
=> @interpf_to_phoas (extend ctx n v) _ eC)
end.
Definition interp_to_phoas
(ctx : Context)
{t} (e : @Named.expr base_type_code op Name t)
: @Syntax.expr base_type_code op var (domain t -> codomain t)
:= Abs (fun v => interpf_to_phoas (extend ctx (Abs_name e) v) (invert_Abs e)).
End with_var.
Section all.
Context {Context : forall var, @Context base_type_code Name var}
(failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t)).
Definition InterpToPHOAS_gen
(ctx : forall var, Context var)
{t} (e : @Named.expr base_type_code op Name t)
: @Syntax.Expr base_type_code op (domain t -> codomain t)
:= fun var => interp_to_phoas (failb var) (ctx var) e.
Definition InterpToPHOAS {t} e
:= @InterpToPHOAS_gen (fun var => empty) t e.
End all.
End language.
End Named.
|
