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
|
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.Named.Syntax.
Require Import Crypto.Compilers.Named.Context.
Require Import Crypto.Util.PointedProp.
Require Import Crypto.Util.Notations.
Module Export Named.
Section language.
Context {base_type_code : Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
{Name : Type}
{interp_base_type : base_type_code -> Type}
{Context : Context Name interp_base_type}
(interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d)
(interped_op_side_conditions : forall s d, op s d -> interp_flat_type interp_base_type s -> pointed_Prop).
Local Notation exprf := (@exprf base_type_code op Name).
Local Notation expr := (@expr base_type_code op Name).
Fixpoint interpf_side_conditions_gen {t} (ctx : Context) (e : exprf t)
: option (pointed_Prop * interp_flat_type interp_base_type t)
:= match e with
| TT => Some (trivial, tt)
| Var t' x => option_map (fun v => (trivial, v)) (lookupb t' ctx x)
| Op t1 tR opc args
=> match @interpf_side_conditions_gen _ ctx args with
| Some (args_cond, argsv)
=> Some (args_cond /\ interped_op_side_conditions _ _ opc argsv, interp_op _ _ opc argsv)
| None => None
end
| LetIn _ n ex _ eC
=> match @interpf_side_conditions_gen _ ctx ex with
| Some (x_cond, x)
=> match @interpf_side_conditions_gen _ (extend ctx n x) eC with
| Some (c_cond, cv)
=> Some (x_cond /\ c_cond, cv)
| None => None
end
| None => None
end
| Pair _ ex _ ey
=> match @interpf_side_conditions_gen _ ctx ex, @interpf_side_conditions_gen _ ctx ey with
| Some (x_cond, xv), Some (y_cond, yv) => Some (x_cond /\ y_cond, (xv, yv))
| None, _ | _, None => None
end
end%pointed_prop.
Definition interpf_side_conditions {t} ctx e : option pointed_Prop
:= option_map (@fst _ _) (@interpf_side_conditions_gen t ctx e).
Definition interp_side_conditions {t} ctx (e : expr t) : interp_flat_type interp_base_type (domain t) -> option pointed_Prop
:= fun x => interpf_side_conditions (extend ctx (Abs_name e) x) (invert_Abs e).
Definition InterpSideConditions {t} (e : expr t) : interp_flat_type interp_base_type (domain t) -> option pointed_Prop
:= interp_side_conditions empty e.
End language.
End Named.
|
