Section BoolExpExample.

(* Les booléens *)

Inductive Bool : Set := true : Bool | false : Bool.

Check true.

(* Le complément *)

Definition neg (a : Bool) := 
  match a with true => false | false => true end.

(* La conjuction *)

Definition andb (a b : Bool) :=
  match a with
  | true => match b with true => true | false => false end
  | false => false
  end.

Parameter vName : Set.
Variables x y z : vName.

(* Les expressions booléennes (langage source) *)

Inductive bExp : Set :=
  bCst (b : Bool) | bVar (v : vName) | bNeg (e : bExp) | bAnd (e1 e2 : bExp).

Check (bAnd (bNeg (bVar x)) (bCst true)).

(* Fonction qui évalue les expressions booléennes (sémantique) *)

Fixpoint bEval (env : vName -> Bool) (e : bExp) {struct e} : Bool :=
  match e with
  | bCst b => b
  | bVar v => env v
  | bNeg e1 => neg (bEval env e1)
  | bAnd e1 e2 => andb (bEval env e1) (bEval env e2)
  end.

Eval compute in
  (bEval (fun x : vName => true) (bAnd (bNeg (bVar x)) (bCst true))).

(* Les expressions conditionnelles (langage objet) *)

Inductive iExp : Set :=
   iCst (b : Bool) | iVar (v : vName) | iCond (test e1 e2 : iExp).

Check (iCond (iVar x) (iCst false) (iCst true)).

(* Fonction qui évalue les expressions conditionelles (sémantique) *)

Fixpoint iEval (env : vName -> Bool) (e : iExp) {struct e} : Bool :=
  match e with
  | iCst b => b
  | iVar v => env v
  | iCond test e1 e2 =>
      match iEval env test with
      | true => iEval env e1
      | false => iEval env e2
      end
  end.

Eval compute in
  (iEval (fun x : vName => true) (iCond (iVar x) (iCst false) (iCst true))).

(* Fonction qui transforme les bExp en iExp (compilation) *)

Fixpoint b2i (e : bExp) : iExp :=
  match e with
  | bCst b => iCst b
  | bVar v => iVar v
  | bNeg e1 => iCond (b2i e1) (iCst false) (iCst true)
  | bAnd e1 e2 => iCond (b2i e1) (b2i e2) (iCst false)
  end.

Theorem b2ifKeepsValue :
 forall (env : vName -> Bool) (e : bExp), bEval env e = iEval env (b2i e).

(* Normal Form pour expressions conditionnelles *)

Inductive Normal : iExp -> Prop :=
  | NormalCst : forall b : Bool, Normal (iCst b)
  | NormalVif : forall v : vName, Normal (iVar v)
  | NormalIfCif :
      forall (b : Bool) (e1 e2 : iExp),
      Normal e1 -> Normal e2 -> Normal (iCond (iCst b) e1 e2)
  | NormalIfVif :
      forall (n : vName) (e1 e2 : iExp),
      Normal e1 -> Normal e2 -> Normal (iCond (iVar n) e1 e2).

(* Fonction qui s'occupe des conditionnelles *)

Fixpoint normCond (thenPart elsePart e : iExp) {struct e} : iExp :=
  match e with
  | iCst b => iCond (iCst b) thenPart elsePart
  | iVar v => iCond (iVar v) thenPart elsePart
  | iCond test then1 else1 =>
      normCond (normCond thenPart elsePart then1) 
               (normCond thenPart elsePart else1) test
  end.

(* Fonction qui normalise (optimisation) *)

Fixpoint norm (e : iExp) : iExp :=
  match e with
  | iCst b => iCst b
  | iVar v => iVar v
  | iCond test thenPart elsePart => 
       normCond (norm thenPart) (norm elsePart) test
  end.

Theorem normCondKeepsEval :
 forall (env : vName -> Bool) (e thenPart elsePart : iExp),
   iEval env (normCond thenPart elsePart e) = 
   iEval env (iCond e thenPart elsePart).

Theorem normKeepsEval :
 forall (env : vName -> Bool) (e : iExp), iEval env (norm e) = iEval env e.

Theorem normCondIsNormal :
 forall e thenPart elsePart : iExp,
 Normal thenPart -> Normal elsePart -> Normal (normCond thenPart elsePart e).

Theorem normIsNormal : forall e : iExp, Normal (norm e).

End BoolExpExample.