Cleanup expression compiler; write basic report

1 files changed, 59 insertions, 51 deletions

diff --git a/expr.v b/expr.v
index 8530764..2288b3a 100644
--- a/expr.v
+++ b/expr.v
@@ -1,86 +1,94 @@
-Require Import Omega.
-Require Import Wellfounded.
+Require Import Omega Wellfounded Coq.Lists.List.
+Import ListNotations.
 
-Inductive Exp : Set :=
-  | elit : nat -> Exp
-  | evar : nat -> Exp
-  | eadd : Exp -> Exp -> Exp.
+Inductive Exp (v : Type) :=
+  | elit : nat -> Exp v
+  | evar : v   -> Exp v
+  | eadd : Exp v -> Exp v -> Exp v.
 
-Fixpoint eval (env : nat -> nat) (e : Exp) :=
+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 env a + eval env b
+  | elit _ n   => n
+  | evar _ n   => env n
+  | eadd _ a b => eval v env a + eval v env b
   end.
 
-Inductive RPNOp :=
-  | rpnlit : nat -> RPNOp
-  | rpnvar : nat -> RPNOp
-  | rpnadd : RPNOp.
+Inductive RPNOp (v : Type) :=
+  | rpnlit : nat -> RPNOp v
+  | rpnvar : v   -> RPNOp v
+  | rpnadd : RPNOp v.
 
-Fixpoint rpn (e : Exp) :=
+Fixpoint rpn (v : Type) (e : Exp v) : list (RPNOp v) :=
   match e with
-  | elit n => cons (rpnlit n) nil
-  | evar n => cons (rpnvar n) nil
-  | eadd a b => app (rpn b) (app (rpn a) (cons rpnadd nil))
+  | 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 B (f : A -> B) (o : option A) :=
+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 fmap := (_fmap _ _).
+Notation "x <$> y" := (fmap _ _ x y) (at level 65, left associativity).
 
-Fixpoint rpn_eval' (env : nat -> nat) (rpn : list RPNOp) :=
+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
-  | nil => Some nil
-  | cons (rpnlit n) a => fmap (cons n) (rpn_eval' env a)
-  | cons (rpnvar n) a => fmap (cons (env n)) (rpn_eval' env a)
-  | cons (rpnadd) a => match rpn_eval' env a with
-    | Some (cons x (cons y stack)) => Some (cons (x+y) stack)
-    | _                            => None
+  | []              => 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 (env : nat -> nat) (rpn : list RPNOp) :=
-  match rpn_eval' env (List.rev rpn) with
-  | Some (cons x nil) => Some x
-  | _                 => None
+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.
 
-Fixpoint exprsize e :=
+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 a + exprsize b
+  | elit _ _ => 1
+  | evar _ _ => 1
+  | eadd _ a b => 1 + exprsize v a + exprsize v b
   end.
-
-Lemma correctness_partial_compilation e :
-  forall env rest results,
-  Some results = rpn_eval' env rest ->
-  Some (eval env e :: results)%list = rpn_eval' env (app (List.rev (rpn e)) rest).
-Proof.
 induction e using (well_founded_induction
-  (wf_inverse_image _ nat _ exprsize PeanoNat.Nat.lt_wf_0)).
+  (wf_inverse_image _ nat _ (exprsize v) PeanoNat.Nat.lt_wf_0)).
+
 intros.
 destruct e; simpl; try rewrite <- H0; try reflexivity.
-rewrite (List.rev_app_distr (rpn e2)).
-rewrite (List.rev_app_distr (rpn e1)).
+rewrite (rev_app_distr (rpn v e2)).
+rewrite (rev_app_distr (rpn v e1)).
 simpl.
-(* Only eadd is left now *)
-rewrite (List.app_assoc_reverse (List.rev (rpn e1)) (List.rev (rpn e2)) rest).
-assert (Some (eval env e1 :: eval env e2 :: results)%list
-    = rpn_eval' env (app (List.rev (rpn e1)) (app (List.rev (rpn e2)) rest))) as recstep.
+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 e env : Some (eval env e) = rpn_eval env (rpn e).
+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 env e :: nil)%list = rpn_eval' env (List.rev (rpn e))) as outsourcing.
-rewrite <- (List.app_nil_r (List.rev (rpn e))).
+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.