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
|
Require Import Crypto.Reflection.Syntax.
Require Export Crypto.Reflection.Reify.
Require Import Crypto.Reflection.InputSyntax.
Require Crypto.Reflection.Linearize.
Require Import Crypto.Reflection.WfReflective.
Import ReifyDebugNotations.
Inductive base_type := Tnat.
Definition interp_base_type (v : base_type) : Type :=
match v with
| Tnat => nat
end.
Local Notation tnat := (Tbase Tnat).
Inductive op : flat_type base_type -> flat_type base_type -> Type :=
| Add : op (Prod tnat tnat) tnat
| Mul : op (Prod tnat tnat) tnat.
Definition interp_op src dst (f : op src dst) : interp_flat_type_gen interp_base_type src -> interp_flat_type_gen interp_base_type dst
:= match f with
| Add => fun xy => fst xy + snd xy
| Mul => fun xy => fst xy * snd xy
end%nat.
Global Instance: forall x y, reify_op op (x + y)%nat 2 Add := fun _ _ => I.
Global Instance: forall x y, reify_op op (x * y)%nat 2 Mul := fun _ _ => I.
Global Instance: reify type nat := Tnat.
Ltac Reify' e := Reify.Reify' base_type interp_base_type op e.
Ltac Reify e := Reify.Reify base_type interp_base_type op e.
Ltac Reify_rhs := Reify.Reify_rhs base_type interp_base_type op interp_op.
(*Ltac reify_debug_level ::= constr:(2).*)
Goal (flat_type base_type -> Type) -> False.
intro var.
let x := reifyf base_type interp_base_type op var 1%nat in pose x.
let x := Reify' 1%nat in unify x (fun var => Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1).
let x := reifyf base_type interp_base_type op var (1 + 1)%nat in pose x.
let x := Reify' (1 + 1)%nat in unify x (fun var => Op Add (Pair (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1))).
let x := reify_abs base_type interp_base_type op var (fun x => x + 1)%nat in pose x.
let x := Reify' (fun x => x + 1)%nat in unify x (fun var => Abs (fun y => Op Add (Pair (Var y) (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1)))).
let x := reifyf base_type interp_base_type op var (let '(a, b) := (1, 1) in a + b)%nat in pose x.
let x := reifyf base_type interp_base_type op var (let '(a, b, c) := (1, 1, 1) in a + b + c)%nat in pose x.
let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in let x := (eval vm_compute in x) in pose x.
let x := Reify' (fun x => let '(a, b) := (1, 1) in a + x)%nat in
unify x (fun var => Abs (fun x' =>
let c1 := (Const (interp_base_type:=interp_base_type) (var:=var) (t:=Tbase Tnat) (op:=op) 1) in
MatchPair (tC:=tnat) (Pair c1 c1)
(fun x0 _ : var tnat => Op Add (Pair (Var x0) (Var x'))))).
let x := reifyf base_type interp_base_type op var (let x := 5 in let y := 6 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x.
let x := Reify' (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in pose x.
Abort.
Goal (0 = let x := 1+2 in x*3)%nat.
Reify_rhs.
Abort.
Goal (0 = let x := 1 in let y := 2 in x * y)%nat.
Reify_rhs.
Abort.
Import Linearize.
Goal True.
let x := Reify (fun x y => (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in
pose (InlineConst (Linearize x)) as e.
vm_compute in e.
Abort.
Definition example_expr : Syntax.Expr base_type interp_base_type op (Tbase Tnat).
Proof.
let x := Reify (let x := 1 in let y := 1 in (let a := 1 in let '(c, d) := (2, 3) in a + x + c + d) + y)%nat in
exact x.
Defined.
Definition base_type_eq_semidec_transparent : forall t1 t2, option (t1 = t2)
:= fun t1 t2 => match t1, t2 with
| Tnat, Tnat => Some eq_refl
end.
Lemma base_type_eq_semidec_is_dec : forall t1 t2,
base_type_eq_semidec_transparent t1 t2 = None -> t1 <> t2.
Proof.
intros t1 t2; destruct t1, t2; simpl; intros; congruence.
Qed.
Definition op_beq t1 tR : op t1 tR -> op t1 tR -> option pointed_Prop
:= fun x y => match x, y with
| Add, Add => Some trivial
| Add, _ => None
| Mul, Mul => Some trivial
| Mul, _ => None
end.
Lemma op_beq_bl t1 tR (x y : op t1 tR)
: match op_beq t1 tR x y with
| Some p => to_prop p
| None => False
end -> x = y.
Proof.
destruct x; simpl.
{ refine match y with Add => _ | _ => _ end; tauto. }
{ refine match y with Add => _ | _ => _ end; tauto. }
Qed.
Ltac reflect_Wf := WfReflective.reflect_Wf base_type_eq_semidec_is_dec op_beq_bl.
Lemma example_expr_wf_slow : Wf example_expr.
Proof.
Time (vm_compute; intros;
repeat match goal with
| [ |- wf _ _ _ ] => constructor; intros
| [ |- wff _ _ _ ] => constructor; intros
| [ |- List.In _ _ ] => vm_compute
| [ |- ?x = ?x \/ _ ] => left; reflexivity
| [ |- ?x = ?y \/ _ ] => right
end). (* 0.036 s *)
Qed.
Lemma example_expr_wf : Wf example_expr.
Proof. Time reflect_Wf. (* 0.008 s *) Qed.
|
