blob: 2288b3a10a1e819ca674ed1dc9c9981c0e756736 (
plain) (
blame)
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
|
Require Import Omega Wellfounded Coq.Lists.List.
Import ListNotations.
Inductive Exp (v : Type) :=
| elit : nat -> Exp v
| evar : v -> Exp v
| eadd : Exp v -> Exp v -> Exp v.
Fixpoint eval (v : Type) (env : v -> nat) (e : Exp v) : nat :=
match e with
| elit _ n => n
| evar _ n => env n
| eadd _ a b => eval v env a + eval v env b
end.
Inductive RPNOp (v : Type) :=
| rpnlit : nat -> RPNOp v
| rpnvar : v -> RPNOp v
| rpnadd : RPNOp v.
Fixpoint rpn (v : Type) (e : Exp v) : list (RPNOp v) :=
match e with
| elit _ n => [rpnlit v n]
| evar _ n => [rpnvar v n]
| eadd _ a b => rpn v b ++ rpn v a ++ [rpnadd v]
end.
Definition fmap (a : Type) (b : Type) (f : a -> b) (o : option a) : option b :=
match o with
| Some x => Some (f x)
| None => None
end.
Notation "x <$> y" := (fmap _ _ x y) (at level 65, left associativity).
Definition bind (a : Type) (b : Type) (f : a -> option b) (o : option a) : option b :=
match o with
| Some x => f x
| None => None
end.
Notation "x >>= f" := (bind _ _ f x) (at level 55, left associativity).
Fixpoint pn_eval (v : Type) (env : v -> nat) (rpn : list (RPNOp v)) : option (list nat) :=
match rpn with
| [] => Some []
| rpnlit _ n :: a => cons n <$> pn_eval v env a
| rpnvar _ n :: a => cons (env n) <$> pn_eval v env a
| rpnadd _ :: a => pn_eval v env a >>= fun stack => match stack with
| x :: y :: stack => Some (x+y :: stack)
| _ => None
end
end.
Function rpn_eval (v : Type) (env : v -> nat) (rpn : list (RPNOp v)) : option nat :=
match pn_eval v env (rev rpn) with
| Some [x] => Some x
| _ => None
end.
Lemma correctness_partial_compilation (v : Type) (e : Exp v) :
forall (env : v -> nat) (rest : list (RPNOp v)) (results : list nat),
Some results = pn_eval v env rest ->
Some (eval v env e :: results) = pn_eval v env (rev (rpn v e) ++ rest).
Proof.
Fixpoint exprsize (v : Type) (e : Exp v) : nat :=
match e with
| elit _ _ => 1
| evar _ _ => 1
| eadd _ a b => 1 + exprsize v a + exprsize v b
end.
induction e using (well_founded_induction
(wf_inverse_image _ nat _ (exprsize v) PeanoNat.Nat.lt_wf_0)).
intros.
destruct e; simpl; try rewrite <- H0; try reflexivity.
rewrite (rev_app_distr (rpn v e2)).
rewrite (rev_app_distr (rpn v e1)).
simpl.
rewrite (app_assoc_reverse (rev (rpn v e1)) (rev (rpn v e2)) rest).
assert (Some (eval v env e1 :: eval v env e2 :: results)
= pn_eval v env (rev (rpn v e1) ++ rev (rpn v e2) ++ rest)) as recstep.
apply H; try apply H; simpl; try assumption; omega.
rewrite <- recstep.
reflexivity.
Qed.
Theorem correctness (v : Type) (e : Exp v) (env : v -> nat) :
Some (eval v env e) = rpn_eval v env (rpn v e).
Proof.
assert (Some [eval v env e] = pn_eval v env (rev (rpn v e))) as outsourcing.
rewrite <- (app_nil_r (rev (rpn v e))).
apply correctness_partial_compilation.
simpl. reflexivity.
unfold rpn_eval.
rewrite <- outsourcing.
reflexivity.
Qed.
|
