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
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
|
(** * Common Subexpression Elimination for PHOAS Syntax *)
Require Import Coq.Lists.List.
Require Import Crypto.Compilers.Named.Context.
Require Import Crypto.Compilers.Named.AListContext.
Require Import Crypto.Compilers.Syntax.
Require Import Crypto.Compilers.ExprInversion.
Require Import Crypto.Compilers.Equality.
Require Import Crypto.Compilers.SmartMap.
Require Import Crypto.Compilers.CommonSubexpressionElimination.
Section symbolic.
Context (base_type_code : Type)
(op_code : Type)
(base_type_code_beq : base_type_code -> base_type_code -> bool)
(op_code_beq : op_code -> op_code -> bool)
(base_type_code_bl : forall x y, base_type_code_beq x y = true -> x = y)
(base_type_code_lb : forall x y, x = y -> base_type_code_beq x y = true)
(op_code_bl : forall x y, op_code_beq x y = true -> x = y)
(op_code_lb : forall x y, x = y -> op_code_beq x y = true)
(op : flat_type base_type_code -> flat_type base_type_code -> Type)
(symbolize_op : forall s d, op s d -> op_code)
(denote_op : forall s d, op_code -> option (op s d))
(denote_symbolize_op : forall s d opc, denote_op s d (symbolize_op s d opc) = Some opc).
Local Notation symbolic_expr := (symbolic_expr base_type_code op_code).
Local Notation symbolic_expr_beq := (@symbolic_expr_beq base_type_code op_code base_type_code_beq op_code_beq).
Local Notation symbolic_expr_lb := (@internal_symbolic_expr_dec_lb base_type_code op_code base_type_code_beq op_code_beq base_type_code_lb op_code_lb).
Local Notation symbolic_expr_bl := (@internal_symbolic_expr_dec_bl base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op_code_bl).
Local Notation flat_type := (flat_type base_type_code).
Local Notation type := (type base_type_code).
Local Notation exprf := (@exprf base_type_code op).
Local Notation expr := (@expr base_type_code op).
Local Notation Expr := (@Expr base_type_code op).
Local Notation flat_type_beq := (@flat_type_beq base_type_code base_type_code_beq).
Local Notation flat_type_dec_bl := (@flat_type_dec_bl base_type_code base_type_code_beq base_type_code_bl).
Local Notation symbolicify_smart_var := (@symbolicify_smart_var base_type_code op_code).
Local Notation symbolize_exprf := (@symbolize_exprf base_type_code op_code op symbolize_op).
Local Notation csef := (@csef base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
Local Notation cse := (@cse base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
Local Notation CSE := (@CSE base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl op symbolize_op).
Local Notation SymbolicExprContext := (@SymbolicExprContext base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl).
Local Notation SymbolicExprContextOk := (@SymbolicExprContextOk base_type_code op_code base_type_code_beq op_code_beq base_type_code_bl base_type_code_lb op_code_bl op_code_lb).
Local Notation prepend_prefix := (@prepend_prefix base_type_code op).
Section with_var.
Context {interp_base_type : base_type_code -> Type}
{interp_op : forall s d, op s d -> interp_flat_type interp_base_type s -> interp_flat_type interp_base_type d}
(m : @SymbolicExprContext (interp_flat_type interp_base_type)).
Local Notation var_cast := (@var_cast _ (interp_flat_type interp_base_type) flat_type_beq flat_type_dec_bl).
Fixpoint denote_symbolic_expr
(t : flat_type)
(se : symbolic_expr)
: option (interp_flat_type interp_base_type t)
:= match se, t with
| STT, Unit => Some tt
| SVar n, t
=> match List.nth_error m (length m - S n) with
| Some e => @var_cast _ t (projT2 (snd e))
| None => None
end
| SOp argsT op args, _
=> match denote_op argsT t op, @denote_symbolic_expr argsT args with
| Some opc, Some eargs => Some (interp_op _ _ opc eargs)
| Some _, None | None, Some _ | None, None => None
end
| SPair x y, Prod A B
=> match @denote_symbolic_expr A x, @denote_symbolic_expr B y with
| Some ex, Some ey => Some (ex, ey)
| Some _, None | None, Some _ | None, None => None
end
| SFst A B x, A'
=> if flat_type_beq A A'
then option_map (@fst _ _) (@denote_symbolic_expr (Prod A' B) x)
else None
| SSnd A B x, B'
=> if flat_type_beq B B'
then option_map (@snd _ _) (@denote_symbolic_expr (Prod A B') x)
else None
| SInvalid, _
| STT, _
| SPair _ _, _
=> None
end.
Fail Lemma denote_symbolize_exprf
(*(Hm : forall n v, List.nth_error m n = Some v -> denote_symbolic_expr *)
t e se e'
: @symbolize_exprf var t e = Some se
-> denote_symbolic_expr t se = Some e'
-> e' = e. (* The command has indeed failed with message:
In environment
base_type_code : Type
op_code : Type
base_type_code_beq : base_type_code -> base_type_code -> bool
op_code_beq : op_code -> op_code -> bool
base_type_code_bl : forall x y : base_type_code, base_type_code_beq x y = true -> x = y
base_type_code_lb : forall x y : base_type_code, x = y -> base_type_code_beq x y = true
op_code_bl : forall x y : op_code, op_code_beq x y = true -> x = y
op_code_lb : forall x y : op_code, x = y -> op_code_beq x y = true
op : flat_type -> flat_type -> Type
symbolize_op : forall s d : flat_type, op s d -> op_code
denote_op : forall s d : flat_type, op_code -> option (op s d)
denote_symbolize_op : forall (s d : flat_type) (opc : op s d), denote_op s d (symbolize_op s d opc) = Some opc
var : base_type_code -> Type
m : SymbolicExprContext
t : flat_type
e : exprf t
se : symbolic_expr
e' : exprf t
The term "e" has type
"@Syntax.exprf base_type_code op
(fun t : base_type_code => prod (var t) (CommonSubexpressionElimination.symbolic_expr base_type_code op_code)) t"
while it is expected to have type "@Syntax.exprf base_type_code op var t".
*)
End with_var.
End symbolic.
|
