(* TD - Compilation certifiée des expressions arithmétiques  *)
(* Pierre Corbineau,Jean-Francois Monin                      *)
(*            UGA Polytech RICM4  2021                       *)

Require Import Bool Arith List.
Import List.ListNotations.

(** * Syntaxe des expressions arithétiques *)

Inductive aexp :=
| Aco : nat -> aexp (** constantes *)
| Ava : nat -> aexp (** variables *)
| Apl : aexp -> aexp -> aexp
| Amu : aexp -> aexp -> aexp
| Amo : aexp -> aexp -> aexp
.

Definition state := list nat.

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

(** * Sémantique fonctionnelle pour 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
  | Amo a1 a2 =>  evalA a1 s - evalA a2 s
  end.

(** * Un état pour faire des tests *)

Definition S2 := [0; 3].

(** * Un exemple d'expression pour faire des tests *)

Definition X := Ava 1.