blob: 68eb06a54918ab9052b241348ed7bc482e08164b (
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
|
Require Import Crypto.Reflection.SmartMap.
Require Import Crypto.Reflection.Named.Syntax.
Require Import Crypto.Reflection.Named.MapCast.
Require Import Crypto.Reflection.Named.InterpretToPHOAS.
Require Import Crypto.Reflection.Named.Compile.
Require Import Crypto.Reflection.Named.PositiveContext.
Require Import Crypto.Reflection.Named.PositiveContext.Defaults.
Require Import Crypto.Reflection.Syntax.
(** N.B. This procedure only works when there are no nested lets,
i.e., nothing like [let x := let y := z in w] in the PHOAS syntax
tree. This is a limitation of [compile]. *)
Section language.
Context {base_type_code : Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
(base_type_code_beq : base_type_code -> base_type_code -> bool)
(base_type_code_bl_transparent : forall x y, base_type_code_beq x y = true -> x = y)
(failb : forall var t, @Syntax.exprf base_type_code op var (Tbase t))
{interp_base_type_bounds : base_type_code -> Type}
(interp_op_bounds : forall src dst, op src dst -> interp_flat_type interp_base_type_bounds src -> interp_flat_type interp_base_type_bounds dst)
(pick_typeb : forall t, interp_base_type_bounds t -> base_type_code).
Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v).
Context (cast_op : forall t tR (opc : op t tR) args_bs,
op (pick_type args_bs) (pick_type (interp_op_bounds t tR opc args_bs))).
Local Notation PContext var := (PositiveContext _ var _ base_type_code_bl_transparent).
Section MapCast.
Context {t} (e : Expr base_type_code op t)
(input_bounds : interp_flat_type interp_base_type_bounds (domain t)).
Definition MapCastCompile
:= compile (e _) (DefaultNamesFor e).
Definition MapCastDoCast (e' : option (Named.expr base_type_code op BinNums.positive t))
:= option_map
(fun e'' => map_cast
interp_op_bounds pick_typeb cast_op
(BoundsContext:=PContext _)
empty
e''
input_bounds)
e'.
Definition MapCastDoInterp
(e' : option
(option
{ output_bounds : interp_flat_type interp_base_type_bounds (codomain t) &
Named.expr _ _ _ (Arrow (pick_type input_bounds) (pick_type output_bounds)) }))
: option { output_bounds : interp_flat_type interp_base_type_bounds (codomain t)
& Expr base_type_code op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }
:= match e' with
| Some (Some (existT output_bounds e''))
=> Some (existT _ output_bounds (InterpToPHOAS (Context:=fun var => PContext var) failb e''))
| Some None | None => None
end.
Definition MapCast
: option { output_bounds : interp_flat_type interp_base_type_bounds (codomain t)
& Expr base_type_code op (Arrow (pick_type input_bounds) (pick_type output_bounds)) }
:= MapCastDoInterp (MapCastDoCast MapCastCompile).
End MapCast.
End language.
|
