(* Projet IPR 2009-2010 *)
(* Verificateur d'assertions à Runtime *)

(* Pierre Guilbault - Louis Volant *)


(* Syntaxe PL *)

type expr =
Const of int
| Var of string
| Booleen of bool
| Plus of expr * expr
| Moins of expr * expr;;

type cond =
Booleen of bool
| Inf of expr * expr
| InfEgal of expr * expr
| Sup of expr * expr
| SupEgal of expr * expr
| Egal of expr * expr
| NonEgal of expr * expr;;

type instr =
| Seq of instr list
| IfThenElse of cond * instr list * instr list
| While of cond * instr list
| Abort of string
| Assign of string * expr
| Call of fonction

and fonction = F of string * (string * int) list * instr list;;

type env = (string * int) list;;

type prog = P of env * instr list;;


(* Récupère dans l'environnement la valeur associée à une variable *)

let rec valeur s var = match s with
(x,v)::r -> if (var=x) then v else valeur r var
| [] -> raise Not_found;;


(* Met à jour la variable x de l'environnement s *)

let rec maj_env s x v = match s with
[] -> [(x,v)]
| (a,b)::r -> if a=x then (x,v)::r else (a,b)::(maj_env r x v);;

(* Met à jour l'environnement s avec la liste l composée de couples (variable,valeur) *)

let rec maj_env_list s l = match l with
(a,b)::r -> maj_env_list (maj_env s a b) r
| [] -> s ;;


let rec eval_expr env e = match e with
| Const(i) -> i
| Var(i) -> valeur env i
| Plus(e1,e2) -> (eval_expr env e1) + (eval_expr env e2)
| Moins(e1,e2) -> (eval_expr env e1) - (eval_expr env e2);;

let eval_bool env b = match b with
| Booleen(e) -> e
| Inf(e1,e2) -> ((eval_expr env e1) < (eval_expr env e2))
| InfEgal(e1,e2) -> ((eval_expr env e1) <= (eval_expr env e2))
| Sup(e1,e2) -> ((eval_expr env e1) > (eval_expr env e2))
| SupEgal(e1,e2) -> ((eval_expr env e1) >= (eval_expr env e2))
| Egal(e1,e2) -> ((eval_expr env e1) = (eval_expr env e2))
| NonEgal(e1,e2) -> ((eval_expr env e1) <> (eval_expr env e2));;



(*(* Récupère la fonction f depuis l'environnement env *)

let rec fonction env nom_fonction = match env with
(V(a,b))::q -> (fonction q nom_fonction)
| (F(nom,args,corps))::r -> if (nom=nom_fonction) then F(nom,args,corps) else (fonction r nom_fonction)
| [] -> raise Not_found;;



(* Met à jour la fonction f portant le nom x de l'environnement env *)

let rec maj_env_fonction env f x = match env with
[] -> [f]
| ((F(a,b,c))::r) -> if a=x then (F(x,b,c))::r else (F(a,b,c))::(maj_env_fonction r f x)
| ((V(a,b))::q) -> maj_env_fonction q f x ;;


(* Crée une liste de couple (x,v) à partir d'une liste de x et d'une liste de v (ordonnées) *)

let rec fusion_var_val l1 l2 = match (l1,l2) with
([],[]) -> []
| (a::b,c::d) -> (a,c)::(fusion_var_val b d);;*)



(* Interprête PL *)
(* s est l'environnement, i l'instruction *)
let rec interprete s i = match i with
| Assign(x,e1) -> maj_env s x (eval_expr s e1)
| Call(F(a,b,c)) -> let s2 = (maj_env_list s b) in (instr_list s2 c)
			
| Seq(i) -> instr_list s i     
        
| IfThenElse(cond,listInstr1,listInstr2) -> if (eval_bool s cond) then (match listInstr1 with
    | (x::r) -> (interprete (interprete s x) (IfThenElse (Booleen(true),r,[])))
    | [] -> s
    )
    else (match listInstr2 with
    | (x::r) -> (interprete (interprete s x) (IfThenElse (Booleen(true),r,[])))
    | [] -> s
    )
| Abort mess -> failwith mess  

| While(cond,listInstr) -> if (eval_bool s cond) then let l = listInstr@[While(cond,listInstr)] 
							in (interprete s (IfThenElse (Booleen(true),l,[]))) else s

and instr_list env list = match list with
  | [] -> env
  | i::rem -> instr_list (interprete env i) rem        
;;


(* Fonctions de test *)

(* 	env_depart : []
	x = 1;
	y = 2;
	z = x + y;
*)	

(*let env_depart1 = [];;
let i1 = Assign("x",Const(1));;
let i2 = Assign("y",Const(2));;
let i3 = Assign("z",Plus(Var("x"),Var("y")));;
let liste1 = [i1;i2;i3];;
let env_arrivee = interprete env_depart1 (Seq(liste1));;*)

(* 	env_depart : [(x,1)]
	if (x>2){
		z=1;
		}
	else{
		z=2;
		}
*)


(*let env_depart1 = [("x",1)];;
let condition = Sup(Var("x"),Const(2));;
let i1 = IfThenElse((condition),[(Assign("z",Const(1)))],[(Assign("z",Const(2)))]);;	
let liste1 = [i1];;
interprete env_depart1 (Seq(liste1));;*)


(*	env_depart : []
	int f (int a, int b){

		z = a + b;
		return z;
	}
	t = f(a,b) + 2;
*)	


let s =[("t",1)];;
let e1 = Var("t");;
let e2 = Const(1)
let e3 = Egal(e1,e2);;

let i = IfThenElse((e3),[(Assign("z",Const(1)))],[(Assign("z",Const(2)))]);;

let ii = interprete s i;;


(* Syntaxe PLML *)

type exprML =
ConstML of int
| VarML of string
| OldML of string
| PlusML of exprML * exprML
| MoinsML of exprML * exprML;;

type condML =
SupML of exprML * exprML
| InfML of exprML * exprML
| SupEgalML of exprML * exprML
| InfEgalML of exprML * exprML
| EgalML of exprML * exprML;;

type invariants = Invariants of condML;; (* Preconditions *)
type requires = Requires of condML;; (* Preconditions *)
type ensures = Ensures of condML;;(* Postconditions *)

type ligneML = L of string * invariants list * requires list * ensures list;;

(* Passage des types PLML aux types PL *)
let rec pLMLtoML a = match a with
ConstML b -> Const b
| VarML b -> Var (b)
| PlusML (b,c) -> Plus ((pLMLtoML b),(pLMLtoML c))
| MoinsML (b,c) -> Moins ((pLMLtoML b),(pLMLtoML c));;

(* Fonction auxiliaire de transformation pour les invariants *)
let rec transformI3 listInstrI = match listInstrI with
(Invariants a)::b -> (match a with
	SupML(c2,d2) -> let e2=(IfThenElse ((Sup(pLMLtoML c2,pLMLtoML d2)),[],[Abort("Invariants Sup")])) in e2::(transformI3 b)
    | InfML(c3,d3) -> let e3=(IfThenElse ((Inf(pLMLtoML c3,pLMLtoML d3)),[],[Abort("Invariants Inf")])) in e3::(transformI3 b)
    | SupEgalML(c4,d4) -> let e4=(IfThenElse ((SupEgal(pLMLtoML c4,pLMLtoML d4)),[],[Abort("Invariants SupEgal")])) in e4::(transformI3 b)
    | InfEgalML(c5,d5) -> let e5=(IfThenElse ((InfEgal(pLMLtoML c5,pLMLtoML d5)),[],[Abort("Invariants InfEgal")])) in e5::(transformI3 b)
    | EgalML(c6,d6) -> let e6=(IfThenElse ((Egal(pLMLtoML c6,pLMLtoML d6)),[],[Abort("Invariants Egal")])) in e6::(transformI3 b))
| [] -> [];;

(* Fonction de transformation pour les invariants *)
let rec transformI2 listInstrI listInstr = match listInstr with
debutListInstr::resteListInstr -> (transformI3 listInstrI)@[debutListInstr]@(transformI2 listInstrI resteListInstr)
| [] -> (transformI3 listInstrI);;

(* Fonction de transformation pour les préconditions *)
let rec transformR2 listInstrR = match listInstrR with
(Requires a)::b -> (match a with
	SupML(c2,d2) -> let e2=(IfThenElse ((Sup(pLMLtoML c2,pLMLtoML d2)),[],[Abort("PredCondition Sup")])) in e2::(transformR2 b)
    | InfML(c3,d3) -> let e3=(IfThenElse ((Inf(pLMLtoML c3,pLMLtoML d3)),[],[Abort("PredCondition Inf")])) in e3::(transformR2 b)
    | SupEgalML(c4,d4) -> let e4=(IfThenElse ((SupEgal(pLMLtoML c4,pLMLtoML d4)),[],[Abort("PredCondition SupEgal")])) in e4::(transformR2 b)
    | InfEgalML(c5,d5) -> let e5=(IfThenElse ((InfEgal(pLMLtoML c5,pLMLtoML d5)),[],[Abort("PredCondition InfEgal")])) in e5::(transformR2 b)
    | EgalML(c6,d6) -> let e6=(IfThenElse ((Egal(pLMLtoML c6,pLMLtoML d6)),[],[Abort("PredCondition Egal")])) in e6::(transformR2 b))
| [] -> [];;

(* Fonction de transformation pour les postconditions *)
let rec transformE2 listInstrR = match listInstrR with
(Ensures a)::b -> (match a with
	SupML(c2,d2) -> let e2=(IfThenElse ((Sup(pLMLtoML c2,pLMLtoML d2)),[],[Abort("PostCondition Sup")])) in e2::(transformE2 b)
    | InfML(c3,d3) -> let e3=(IfThenElse ((Inf(pLMLtoML c3,pLMLtoML d3)),[],[Abort("PostCondition Inf")])) in e3::(transformE2 b)
    | SupEgalML(c4,d4) -> let e4=(IfThenElse ((SupEgal(pLMLtoML c4,pLMLtoML d4)),[],[Abort("PostCondition SupEgal")])) in e4::(transformE2 b)
    | InfEgalML(c5,d5) -> let e5=(IfThenElse ((InfEgal(pLMLtoML c5,pLMLtoML d5)),[],[Abort("PostCondition InfEgal")])) in e5::(transformE2 b)
    | EgalML(c6,d6) -> let e6=(IfThenElse ((Egal(pLMLtoML c6,pLMLtoML d6)),[],[Abort("PostCondition Egal")])) in e6::(transformE2 b))
| [] -> [];;

(* Fonction principale de transformation *)
let rec transform1 (L (nom,listInstrInvariants,listInstrRequires,listInstrEnsures)) (F (a,b,c)) = 
	((transformR2 listInstrRequires)@(transformI2 listInstrInvariants c)@(transformE2 listInstrEnsures));; 


(* Tests *)
let s = [("x",4);("y",2)];;
(*let i = IfThenElse((e3),[(Assign("z",Const(1)))],[(Assign("z",Const(2)))]);; *)
(*let i21 = Assign("a",Const(12));;
let i22 = Assign("b",Const(24));; *)
let i23 = Assign("z",Plus(Var ("x"),Var ("y")));;
let l2ii = [(*i21;i22;*)i23];;
let f = F("f1",([("z",1);("t",6)]),l2ii);;

let env_depart1 = [("x",1);("y",1)];;
let env_depart2 = [("x",4);("y",1)];;
let i1 = Assign("x",Const(1));;
let i2 = Assign("y",Const(2));;
let i3 = Assign("z",Plus(Var("x"),Var("y")));;
let liste1 = [i1;i2;i3];;
let env_arrivee = interprete env_depart1 (Seq(liste1));;

(* Tests *)
let s = [("x",4);("y",2)];;
(*let i = IfThenElse((e3),[(Assign("z",Const(1)))],[(Assign("z",Const(2)))]);; *)
(*let i21 = Assign("a",Const(12));;=
let i22 = Assign("b",Const(24));; *)
let i23 = Assign("z",Plus(Var ("x"),Var ("y")));;
let l2ii = [(*i21;i22;*)i23];;
let f = F("f1",([("z",1);("t",6)]),l2ii);;

let env_depart1 = [("x",1);("y",1)];;
let env_depart2 = [("x",4);("y",1)];;
let i1 = Assign("x",Const(1));;
let i2 = Assign("y",Const(2));;
let i3 = Assign("z",Plus(Var("x"),Var("y")));;
let liste1 = [i1;i2;i3];;
let env_arrivee = interprete env_depart1 (Seq(liste1));;

(* Tests PLML *)
let f = F("f1",
	([("z",1);("t",6)]),
	(	[Assign("x",Plus(Var ("x"),Const(1))); (* x:=x+1 *)
		Assign("z",Plus(Var ("x"),Var ("y"))); (* z:=x+y *)
		Assign("y",Plus(Var ("x"),Const(2))); (* y:=x+2 *)
		While((Inf(Var "y",Const (9))),[Assign("y",Plus(Var "y",Const (1)))]) 
		(* While (y < 9) do y:=y+1 done *)
		]
	))
let env_departpositif = [("x",1);("y",1)];;
let env_departnegatif = [("x",4);("y",1)];;

let ii2 = interprete s (Call(f));;

let l11 = L("PLML Positif",[],[],[]);;

let l1 =  transform1 l11 f;; 

let l12 = L("PLML",
			[Invariants(InfEgalML(VarML("x"),ConstML(10)));Invariants(InfEgalML(VarML("y"),ConstML(10)))],
			[Requires(SupEgalML(VarML("x"),ConstML(1)));Requires(SupEgalML(VarML("y"),ConstML(1)))],
			[Ensures(InfEgalML(VarML ("z"),ConstML (4)));Ensures(SupML(VarML ("y"),ConstML(2)))]);;

(* On annote f en l2 *)
let l2 =  transform1 l12 f;;   

(* test positif *)
let l3 = interprete env_departpositif (Seq(l2));;

(* test negatif *)
let l4 = interprete env_departnegatif (Seq(l2));;