(**
AST aexp, bexp and winstr for the WHILE language.
*)

(* ------------------------------------------------------------ *)
(** * Small imperative languages *)

(** ** Abstract Syntax *)
Inductive aexp :=
| Aco : nat -> aexp (* constants *)
| Ava : nat -> aexp (* variables *)
| Apl : aexp -> aexp -> aexp
| Amu : aexp -> aexp -> aexp
| Asu : aexp -> aexp -> aexp
.

Inductive bexp :=
| Btrue : bexp
| Bfalse : bexp
| Bnot : bexp -> bexp
| Band : bexp -> bexp -> bexp
| Bor : bexp -> bexp -> bexp
| Beq : bexp -> bexp -> bexp    (* equality test between Boolean expressions *)
| Beqnat : aexp -> aexp -> bexp (* equality test between arithmetic expressions *)
.

Inductive winstr :=
| Skip   : winstr
| Assign : nat -> aexp -> winstr
| Seq    : winstr -> winstr -> winstr
| If     : bexp -> winstr -> winstr -> winstr
| While  : bexp -> winstr -> winstr
.

(** The IMP language: same as WHILE but without the While loop. *)
Inductive instr :=
| ISkip   : instr
| IAssign : nat -> aexp -> instr
| ISeq    : instr -> instr -> instr
| IIf     : bexp -> instr -> instr -> instr
.

(** Define ASTs for the following programs *)
(** x3 := 5 * x2 *)
Example P1 : instr. Admitted.
(** x2 := x2 + 1 *)
Example P2 : instr. Admitted.
(** if x1 = x3 then (x2 := x2 + 1; x2 := x2 + 1) else x3 := 5 * x2 *)
Example P3 := IIf (Beqnat (Ava 1) (Ava 3)) (ISeq P2 P2) P1.

(** ** Functional semantics *)

Require Import List.
Import ListNotations.

Definition state := list nat.

(** Calling [get i s] returns the value associated to xi in state [s] *)
Fixpoint get (i: nat) (s: state) : nat :=
  match s with
  | []     => 0
  | v :: s' =>
    match i with
    | O => v
    | S i' => get i' s'
    end
  end.

(** A shorter and equivalent definition *)

Reset get.

Fixpoint get (i:nat) (s:state) : nat :=
  match i,s with
  | 0   ,  v :: _   => v
  | S i',  _ :: s'  => get i' s'
  | _   ,  _        => 0
  end.

(** *** Functional semantics of [aexp] *)
Fixpoint evalA (a: aexp) (s: state) : nat :=
  match a with
  | Aco n => n
  | Ava x => get x s
  | Apl a1 a2 =>  evalA a1 s + evalA a2 s
  | Amu a1 a2 =>  evalA a1 s * evalA a2 s
  | Asu a1 a2 =>  evalA a1 s - evalA a2 s
  end.


(** *** Functional semantics of [bexp] *)
Definition eqboolb b1 b2 : bool :=
  match b1, b2  with
  | true, true   => true
  | false, false => true
  | _ , _        => false
  end.

Fixpoint eqnatb n1 n2 : bool :=
   match n1, n2 with
  | O, O         => true
  | S n1', S n2' => eqnatb n1' n2'
  | _, _         => false
  end.

 Fixpoint evalB (b : bexp) (s : state) : bool :=
  match b with
  | Btrue => true
  | Bfalse => false
  | Bnot b => negb (evalB b s)
  | Band e1 e2 => (evalB e1 s) && (evalB e2 s)
  | Bor e1 e2 => (evalB e1 s) || (evalB e2 s)
  | Beq e1 e2 => eqboolb (evalB e1 s) (evalB e2 s)
  | Beqnat n1 n2 => eqnatb (evalA n1 s) (evalA n2 s)
  end.


(** *** Functional semantics of IMP *)

(** [update s i v] returns the state where xi is mapped to [v],
    and the other variables are mapped to the same value as in [s].
    This function never fails, even when variable xi is not
    explicitly given in state [s].
    Take care at managing all cases, including when the state is
    represented by an empty list: everything happens as if we
    instead had a list with enough 0s (the default value).
 *)
Fixpoint update (s:state) (i:nat) (v:nat) : state.
Admitted.

(** Some states for testing *)
(** [S1] is a state etat where variable "x0" is mapped to 1, variable "x1"
    is mapped to 2 and all other variable are mapped to 0 (defaut value) *)

Example S1 := [1; 2].
Example S2 := [0; 3].
Example S3 := [0; 7; 5; 41].

Example S4 :=
  let s1 := update S1 4 1 in
  let s2 := update s1 3 2 in
  let s3 := update s2 2 3 in
  let s4 := update s3 2 3 in
  update s4 0 5.
Example test_S4 : S4 = 5 :: 2 :: 3 :: 2 :: 1 :: [].
Proof. Admitted. (* reflexivity. Qed. *)

(** We can write a functional semantics for IMP. *)
Fixpoint evalI (i : instr) (s : state) : state :=
  match i with
  | ISkip       => s
     (** COMPLETE HERE and remove the fake wildcard case *)
  | _ => s (* fake *)
  end.

Compute evalI P3 S3.
Compute evalI P3 S4.


(** However the extension to WHILE is expected to fail:
    a success would mean that the semantics given does not
    correspond to the expected behavior. *)
(** In order to get the right feedback from Coq, is is important to
    make it clear that the expected structurally decreasiing argument
    should be [i], as for [evalI]. This is the rôle of [{struct i}].
    This infromation could also be added in the definition of [evalI]
    but Coq was able to infer it from the body of the function.
*)
Fail Fixpoint evalW (i : winstr) (s : state) {struct i} : state :=
  (** COMPLETE AND EXPLAIN the error message returned by Coq. *)
  match i with
  | Skip       => s
     (** COMPLETE HERE and remove the fake wildcard case *)
  | _ => evalW i s (* fake *)
  end.

(** ** Tests for [evalI] (should not fail) *)

Example test1 : evalI P1 S1 = 1 :: 2 :: 0 :: 0 :: [].
Proof. Admitted. (* reflexivity. Qed. *)

Example test2 : evalI P1 S4 = 5 :: 2 :: 3 :: 15 :: 1 :: [].
Proof. Admitted. (* reflexivity. Qed. *)

Example test3 : evalI P3 S1 = 1 :: 2 :: 0 :: 0 :: [].
Proof. Admitted. (* reflexivity. Qed. *)

Example test4 : evalI P3 S4 = 5 :: 2 :: 5 :: 2 :: 1 :: [].
Proof. Admitted. (* reflexivity. Qed. *)