(** Introduction to Formal Reasoning (G52IFR)
    Nicolai Kraus and Nuo Li
    Tutorial 7 : compilers and trees **)

Section Tutorial7.


Require Import Coq.Bool.Bool.
Require Import Coq.Lists.List.
Load Arith.



(** very restricted expressions
    why are they restricted? *)
Inductive Expr : Set :=
| Const : bool -> Expr
| Xor   : Expr -> Expr -> Expr
| Id    : Expr -> Expr.

(* And an evaluator which evaluates these
   boolean expressions. *)
Fixpoint eval (e : Expr) : bool :=
  match e with
  | Const b => b
  | Xor e1 e2 => xorb (eval e1) (eval e2)
  | Id e => eval e
  end.

(* Machine code for Boolean expressions. It is for stack *)
Inductive Op : Set :=
  | Push : bool -> Op
  | XorC : Op
  | IdC : Op.

Definition Code : Set := list Op.

Definition Stack : Set := list bool.

(* and a function which executes the machine code. 
The machine returns false as default
*)

Fixpoint run (st : Stack)(p : Code) : bool :=
  match p with
  | nil => match st with
           | nil => false
           | b :: st => b
           end
  | op :: p' => match op with
                | Push b => run (b :: st) p'
                | XorC => match st with 
                           | nil => false
                           | _ :: nil => false
                           | b2 :: b1 :: st' => 
                                run ((xorb b1 b2) ::st') p'
                           end
                | IdC => run st p'
                end
  end.

(* We want to implement
   
   compile : Expr -> Code

   and prove it correct. *)

Fixpoint compile_naive (e : Expr) : Code :=
  match e with
    | Const b   => (Push b) :: nil
    | Xor b1 b2 => (compile_naive b1) ++ (compile_naive b2) ++ XorC :: nil
    | Id b      => (compile_naive b) ++ IdC :: nil
  end.


Lemma compile_lemma : forall e:Expr, forall st: Stack, 
  forall code: Code,
  run st ((compile_naive e) ++ code) = run ((eval e) :: st) code.
intro e.
induction e; simpl.
reflexivity.

intros.
rewrite (app_ass (compile_naive e1) (compile_naive e2 ++ XorC :: nil) code).
rewrite IHe1.
rewrite app_ass.
rewrite IHe2.
simpl.
reflexivity.

intros; simpl.
rewrite app_ass.
rewrite IHe.
simpl.
reflexivity.
Qed.


Theorem compileOk : forall e:Expr, 
  run nil (compile_naive e) = eval e.
intros.
pattern (compile_naive e).
rewrite <- app_nil_r.
rewrite compile_lemma.
simpl.
reflexivity.
Qed.




(** General exercises with trees *)

Set Implicit Arguments.

(* Binary trees with leaves labelled
   with elements of a given set A. *)

Inductive BinTree (A : Set) : Set :=
  | leaf : A -> BinTree A
  | node : BinTree A -> BinTree A -> BinTree A.



(** count the number of elements in a tree *)
Fixpoint count (A : Set) (t : BinTree A) : nat := 
  match t with
    | (leaf _)     => 1
    | (node t1 t2) => (count t1) + (count t2)
  end.



list - non-deterministic

monadplus

for maybe : simple try and catch

Either e a

for either e we can define a monad which does for each exception e we return something

(** we want to flatten the tree, i.e. we want
    to make a list of all elements in the tree *)

Fixpoint flatten (A : Set) (t : BinTree A) : list A :=
  match t with
    | leaf a     => a :: nil
    | node t1 t2 => (flatten t1) ++ (flatten t2)
  end.



(** We want to prove that the length of (flatten t) 
    is equal to the number of elements in t *)

Theorem flattenCount : forall (A: Set) (t: BinTree A),
  (length (flatten t)) = count t.
intros.
induction t; simpl.

reflexivity.

(** check the Coq library *)
rewrite app_length.

rewrite IHt1.
rewrite IHt2.
reflexivity.
Qed.



End Tutorial7.