Require Arith.
Require PolyList.
Require Zerob.
 
Set Implicit Arguments.

(* I- De'finition de la syntaxe des programmes : un ensemble de clauses   *)
(* garde'es forme'es d'une garde et d'une suite d'affectations de termes a` *)
(* des variables *)
(**)

(* Les variables, constantes et symboles de fonctions binaires sont *)
(* des parame`tres abstraits *) 

Section Abstract.

Variables var, cte, fun : Set.

(* De'finition inductive des termes *)

Inductive term : Set :=  ...

(* 
Une affectation multiple de termes a` des variables, se repre'sente 
comme une liste de couples forme's d'une variable et d'un terme appele'e
une substitution 
*)

Definition substitution := ...

(* Une clause est forme'e d'une terme repre'sentant la garde (vraie si *)
(* elle ne s'e'value pas en 0) et d'une substitution *)

Definition clause := ...

Definition programme := ...

(* II - Se'mantique les programmes sont interpre'te'e comme des *)
(* transformations sur les valuations qui repre'sentent l'e'tat de la *)
(* me'moire *)

(* Une valuation est une interpre'tation des variables par des entiers *)

Definition valuation := var -> nat.

(* On se donne une interpre'tation des constantes et symboles de *)
(* fonctions *)

Variable cte_sem : cte -> nat.
Variable fun_sem : fun -> nat -> nat -> nat.

(* Chaque expression represente un entier *)

Fixpoint term_sem [val:valuation;t:term] : nat
  :=  ...

(* Une substitution definit une transformation sur les valuations  *)
(* La se'mantique d'une substitution est de'finie par re'currence sur *)
(* la longueur de la substitution.                                 *)
(* Pour la construire il faut supposer que l'e'galite' est de'cidable *)
(* sur les variables *)

Variable eq_var_dec : (v,v':var){v=v'}+{~v=v'}.

(* Cette proprie'te' permet de definir des fonctions par cas sur *)
(* l'e'galite' de deux variables : 
	if (eq_var_dec v v') then [_]a else [_]b 
*)

Fixpoint aff_sem [val:valuation;aff:substitution] : valuation :=
 ...

(* Se'mantique des clauses *)

Definition clause_sem : valuation -> clause -> valuation := ...


(* La se'mantique d'un programme est non de'terministe par rapport a` la *)
(* clause qui sera exe'cute'e et doit e^tre repre'sente'e par une relation *)
(* sur les valuations *)

(* Transition associe'e a` une clause : la garde soit e^tre vraie *)
Definition evolve : clause -> valuation -> valuation -> Prop 
   := ...

Definition trans_prog : programme -> valuation -> valuation -> Prop
   := ...

End Abstract.