(* Type d'une fonction abstraite : bool vect -> bool *)

(* J'identifie ici 1 à true et 0 à false *)

(* La fonctionnelle abstraite prend donc une (string*((bool vect -> bool)*int)) list *)
(* et une function_declaration list et rend une (string*(bool vect -> bool)*int) list *)

#open "print";;
#open "aintv";;

exception Analyse;;

let fonctionnelle_abstraite lfoncconc lfoncabs =
  let rec applique_equations_de_Mycroft larg =
    let numero s l =
      let n=list_length l in
      let rec num i = function
	| [] -> raise Analyse
	| t::q -> if t=s then i else num (i+1) q
      in num 0 l
    in function
    | CST _ -> (function v -> true)
    | VAR s -> (function v -> v.(numero s larg))
    | ADD (e1,e2) ->
	(function v ->
	  (applique_equations_de_Mycroft larg e1 v) && 
	  (applique_equations_de_Mycroft larg e2 v))
    | SUB (e1,e2) ->
	(function v ->
	  (applique_equations_de_Mycroft larg e1 v) && 
	  (applique_equations_de_Mycroft larg e2 v))
    | MULT (e1,e2) ->
	(function v ->
	  (applique_equations_de_Mycroft larg e1 v) && 
	  (applique_equations_de_Mycroft larg e2 v))
    | DIV (e1,e2) ->
	(function v ->
	  (applique_equations_de_Mycroft larg e1 v) && 
	  (applique_equations_de_Mycroft larg e2 v))
    | LESS (e1,e2) ->
	(function v ->
	  (applique_equations_de_Mycroft larg e1 v) && 
	  (applique_equations_de_Mycroft larg e2 v))
    | EQUAL (e1,e2) ->
	(function v ->
	  (applique_equations_de_Mycroft larg e1 v) && 
	  (applique_equations_de_Mycroft larg e2 v))
    | NOT e ->
	applique_equations_de_Mycroft larg e
    | AND (e1,e2) ->
	(function v ->
	  (applique_equations_de_Mycroft larg e1 v) && 
	  (applique_equations_de_Mycroft larg e2 v))
    | IF (e1,(e2,e3)) ->
	(function v ->
	  (applique_equations_de_Mycroft larg e1 v) &&
	  ((applique_equations_de_Mycroft larg e2 v) ||
	  (applique_equations_de_Mycroft larg e3 v)))
    | CALL (f,lexpr) ->
	try 
	  (function v -> 
	    assoc f lfoncabs (vect_of_list (map (function e->applique_equations_de_Mycroft larg e v) lexpr)))
	with
	    Not_found -> raise Analyse
  in map (function (f,(lpar,expr))->(f,applique_equations_de_Mycroft lpar expr)) lfoncconc;;

let egale f g n =
  let suivant v =
    let i=ref 0 in 
    while (!i<n && (v.(!i)=true)) do
      v.(!i)<-false;
      i:=!i+1
    done;
    if !i=n then failwith "suivant" else v.(!i)<-true;v
  in
  try 
    let rec eg t =
      if f t = g t then eg (suivant t) else false
    in eg (make_vect n false)
  with
    | exc__Failure "suivant" -> true;;

let recherche_points_fixes lfoncconc =
  let rec rpf anciennes_fonctions_abstraites =
    let nouvelles_fonctions_abstraites = fonctionnelle_abstraite lfoncconc
      anciennes_fonctions_abstraites in
    if (it_list (prefix &&) true (map (function (nom,fonc)-> egale fonc (assoc nom anciennes_fonctions_abstraites) (list_length (fst (assoc nom lfoncconc)))) nouvelles_fonctions_abstraites)) then
      nouvelles_fonctions_abstraites
    else
      rpf nouvelles_fonctions_abstraites
  in rpf (map (function (f,_)->(f,function v->true)) lfoncconc);;

let analyse_de_necessite = function (lf,e) ->
  let enleve_type_par = function 
    | FPNSTAT v -> v
    | FPNDYN v -> v
    | FPVAL v -> v
  in let a=recherche_points_fixes (map (function (s,(lp,e)) -> (s,(map enleve_type_par lp,e))) lf) in
  let transforme_fonction = function (s,(lp,e)) ->
    let n=list_length lp in
    let v=make_vect n true in
    let rec construit_nouvelle_lpar i = function 
      | [] -> []
      | t::q ->
	  v.(i)<-false;
	  if (assoc s a) v then
	    begin
	      v.(i)<-true;
	      t::(construit_nouvelle_lpar (i+1) q)
	    end
	  else
	    begin
	      v.(i)<-true;
	      (match t with 
		| FPNSTAT v -> FPVAL v
		| _ -> t
	      )::(construit_nouvelle_lpar (i+1) q)
	    end
    in (s,(construit_nouvelle_lpar 0 lp,e))
  in (map transforme_fonction lf,e);;