blob: ee3712954c62900cee44fca995e26177d53aec09 (
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
|
Require Import Coq.Bool.Sumbool.
Require Import Crypto.Reflection.Syntax.
Require Import Crypto.Reflection.TypeUtil.
Require Import Crypto.Util.Notations.
Local Open Scope expr_scope.
Local Open Scope ctype_scope.
Section language.
Context {base_type_code : Type}
{op : flat_type base_type_code -> flat_type base_type_code -> Type}
(base_type_beq : base_type_code -> base_type_code -> bool)
(base_type_bl_transparent : forall x y, base_type_beq x y = true -> x = y)
(Cast : forall var A A', exprf base_type_code op (var:=var) (Tbase A) -> exprf base_type_code op (var:=var) (Tbase A')).
Local Notation exprf := (@exprf base_type_code op).
Definition SmartCast_base {var A A'} (x : exprf (var:=var) (Tbase A))
: exprf (var:=var) (Tbase A')
:= match sumbool_of_bool (base_type_beq A A') with
| left pf => match base_type_bl_transparent _ _ pf with
| eq_refl => x
end
| right _ => Cast _ _ A' x
end.
Fixpoint SmartCast {var} A B
: option (interp_flat_type var A -> exprf (var:=var) B)
:= match A, B return option (interp_flat_type var A -> exprf (var:=var) B) with
| Tbase A, Tbase B => Some (fun v => SmartCast_base (Var (var:=var) v))
| Prod A0 A1, Prod B0 B1
=> match @SmartCast _ A0 B0, @SmartCast _ A1 B1 with
| Some f, Some g => Some (fun xy => Pair (f (fst xy)) (g (snd xy)))
| _, _ => None
end
| Unit, Unit => Some (fun _ => TT)
| Tbase _, _
| Prod _ _, _
| Unit, _
=> None
end.
End language.
|
