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

let liste_appels p =
  let cree_liste =
    function (s,l) -> 
      let rec sub = function
	| CST _ -> []
        | VAR _ -> []
        | ADD (e1,e2) -> (sub e1)@(sub e2)
        | SUB (e1,e2) -> (sub e1)@(sub e2)
        | MULT (e1,e2) -> (sub e1)@(sub e2)
        | DIV (e1,e2) -> (sub e1)@(sub e2)
        | LESS (e1,e2) -> (sub e1)@(sub e2)
        | EQUAL (e1,e2) -> (sub e1)@(sub e2)
        | NOT e -> sub e
        | AND (e1,e2) -> (sub e1)@(sub e2)
        | IF (e1,(e2,e3)) -> (sub e1)@(sub e2)@(sub e3)
        | CALL (s,l) -> s::(flat_map sub l)
      in (s,sub (snd l))
  in map cree_liste (fst p);;

let cree_num l =
  let i = ref 0 in
  let rec sub = function
      [] -> []
    | t::q->let a=((fst t), !i) in i:=!i+1;a::(sub q)
  in sub l;;

let la_to_graphe la =
  let ln=cree_num la in
  let n=list_length ln in
  let g=matrice false n n in
  let l=ref la in
  for i = 0 to n-1 do
    let rec parcoure_liste = function
      | [] -> ()
      | t::q ->
	  g.(i).(assoc t ln)<- true;
	  parcoure_liste q
    in parcoure_liste (snd (hd !l));
    l:=tl !l
  done;
  ((g:graphe),ln);;

let cree_graphe (p:prog) =
  la_to_graphe (liste_appels p);;

let tri_typage p =
  if fst p=[] then [] else 
    let (g,ln)=cree_graphe p in
    let rec associnv x = function
	[] -> raise Not_found
      | (a,y)::q -> if y=x then a else associnv x q
    in map (map (fun t->associnv t ln)) (tri_topologique g);;

let instancie n =
  let rec construit_instanciation n pile = function
      [] -> (n,[],pile)
    | t::q -> 
	let (n',q',pile')=construit_instanciation n pile q in
	match t with 
	  | Var i ->
	      if mem_assoc i pile' then
		(n',(Var (assoc i pile'))::q',pile')
	      else
		(n'+1,(Var n')::q',(i,n')::pile')
	  | _ -> 
	      (n',t::q',pile')
  in function (tpar,tres) ->
    let (n',l',_)=construit_instanciation n [] (tres::tpar)
    in (tl l',hd l',n');;

let ajoute_equation equ t1 t2 = match (t1,t2) with
  | (Entier,Entier) | (Bool,Bool) -> equ
  | (Bool,Entier) | (Entier,Bool) -> raise Erreur_typage
  | (Var i,Var j) when i=j -> equ
  | _ -> (t1,t2)::equ;;

let type_expr env mcc acc equ n e =
    let rec t_e equ n = function
      | CST "true" | CST "false" -> (n,Bool,equ)
      | CST i ->
	  let is_integer s =
	    try
	      (fun x -> ()) (int_of_string s);
	      true
	    with
		Failure "int_of_string" -> false
	  in if is_integer i then (n,Entier,equ) else raise Erreur_typage
      | VAR x -> (n,assoc x env,equ)
      | ADD (e1,e2) ->
	  let (n',typ1,equ1)=t_e equ n e1 in
	  let (n'',typ2,equ2)=t_e equ1 n' e2 in
	  (n'',Entier,ajoute_equation (ajoute_equation equ2 typ1 Entier) typ2 Entier)
      | SUB (e1,e2) -> 
	  let (n',typ1,equ1)=t_e equ n e1 in
	  let (n'',typ2,equ2)=t_e equ1 n' e2 in
	  (n'',Entier,ajoute_equation (ajoute_equation equ2 typ1 Entier) typ2 Entier)
      | MULT (e1,e2) ->
	  let (n',typ1,equ1)=t_e equ n e1 in
	  let (n'',typ2,equ2)=t_e equ1 n' e2 in
	  (n'',Entier,ajoute_equation (ajoute_equation equ2 typ1 Entier) typ2 Entier)
      | DIV (e1,e2) ->
	  let (n',typ1,equ1)=t_e equ n e1 in
	  let (n'',typ2,equ2)=t_e equ1 n' e2 in
	  (n'',Entier,ajoute_equation (ajoute_equation equ2 typ1 Entier) typ2 Entier)
      | LESS (e1,e2) ->
	  let (n',typ1,equ1)=t_e equ n e1 in
	  let (n'',typ2,equ2)=t_e equ1 n' e2 in
	  (n'',Bool,ajoute_equation (ajoute_equation equ2 typ1 Entier) typ2 Entier)
      | EQUAL (e1,e2) ->
	  let (n',typ1,equ1)=t_e equ n e1 in
	  let (n'',typ2,equ2)=t_e equ1 n' e2 in
	  (n'',Bool,ajoute_equation equ2 typ1 typ2)
      | NOT e ->
	  let (n',typ0,equ0)=t_e equ n e in
	  (n',Bool,ajoute_equation equ0 typ0 Bool)
      | AND (e1,e2) ->
	  let (n',typ1,equ1)=t_e equ n e1 in
	  let (n'',typ2,equ2)=t_e equ1 n' e2 in
	  (n'',Bool,ajoute_equation (ajoute_equation equ2 typ1 Bool) typ2 Bool)
      | IF (t,(e1,e2)) ->
	  let (n',typ0,equ0)=t_e equ n t in
	  let (n'',typ1,equ1)=t_e equ0 n' e1 in
	  let (n''',typ2,equ2)=t_e equ1 n'' e2 in
	  (n''',typ1,ajoute_equation (ajoute_equation equ2 typ1 typ2) typ0 Bool)
      | CALL (f,l) ->
	  let rec type_appel_fonction equ n = function
	      ([],[]) -> (n,equ)
	    | ([],_) -> raise Erreur_typage
	    | (_,[]) -> raise Erreur_typage
	    | (e::q1,t::q2) ->
		let (n',typ0,equ0)=t_e equ n e in
		let (n'',equ1)=type_appel_fonction equ0 n' (q1,q2) in
		(n'',ajoute_equation equ1 typ0 t)
	  in if mem_assoc f acc then
	    let tf=assoc f acc in
	    let (tpar,tres,n')=instancie n tf in
	    let (n'',equ')=type_appel_fonction equ n' (l,tpar) in
	    (n'',tres,equ')
	  else if mem_assoc f mcc then
	    let (tpar,tres)=assoc f mcc in
	    let (n',equ')=type_appel_fonction equ n (l,tpar) in
	    (n',tres,equ')
	  else
	    raise Erreur_typage
    in t_e equ n e;;

let rec print_equations =
  let print_type = function
    | Entier -> print_string "Entier"
    | Bool -> print_string "Booléen"
    | Var i -> print_string ("'"^(string_of_int i))
  in function
      [] -> ()
    | (x,y)::q -> print_type x;print_string " = ";print_type y;print_newline ();print_equations q;;

let simplifie_equations equ =
  let rec s_e deb = function
      [] -> deb
    | (x,y)::q ->
	match (x,y) with
	  | (Entier,Entier) -> s_e deb q
	  | (Entier,Bool) -> raise Erreur_typage
	  | (Bool,Bool) -> s_e deb q
	  | (Bool,Entier) -> raise Erreur_typage
	  | (Var i,Var j) when j=i -> s_e deb q
	  | (Entier,Var i) -> s_e deb ((Var i,Entier)::q)
	  | (Bool,Var i) -> s_e deb ((Var i,Bool)::q)
	  | (Var i,t) ->
	      let rec remplace i t = function
		  [] -> []
		| (Var j,Var k)::q when j=k -> (remplace i t q)
		| (Var j,a)::q when j=i -> (t,a)::(remplace i t q)
		| (a,Var j)::q when j=i -> (a,t)::(remplace i t q)
		| x::q -> x::(remplace i t q)
	      in s_e ((Var i,t)::(remplace i t deb)) (remplace i t q)
  in s_e [] equ;;
  
let rec utilise_equations_simplifiees equ = function
  | [] -> []
  | (f,(tpar,tres))::q ->
      let trouve_type = function x -> try assoc x equ with Not_found -> x in
      (f,((map trouve_type tpar),trouve_type tres))::(utilise_equations_simplifiees equ q);;

let type_composante_connexe acc n l =
  let construit_mcc ll =
    let rec c_mcc n = function
      | [] -> (n,[])
      | (f,(l,_))::q ->
	  let rec construit_liste_types n = function
	      [] -> (n,[])
	    | _::q -> let (n',a)=construit_liste_types (n+1) q in
		(n',(Var n)::a)
	  in
	  let (n',l')=construit_liste_types n l in
	  (n'+1,(f,(l',Var n'))::(snd (c_mcc (n'+1) q)))
    in c_mcc n ll;
  in let (n',mcc)=construit_mcc l in
  let rec type_mcc equ n = function
    | ([],[]) -> (n,equ)
    | ([],_) | (_,[]) -> raise Erreur_typage
    | ((_,(listpar,e))::q1,(_,(tpar,tres))::q2) ->
	let rec construit_env = function
	  | ([],[]) -> []
	  | ([],_) | (_,[]) -> raise Erreur_typage
	  | (par::q1,tpar::q2) ->
	      let extrait_nom = function
		| FPVAL s -> s
		| FPNDYN s -> s
		| FPNSTAT s -> s
	      in (extrait_nom par,tpar)::(construit_env (q1,q2))
	in let (n',tres',equ')=type_expr (construit_env (listpar,tpar)) mcc acc equ n e in
	type_mcc ((tres,tres')::equ') n' (q1,q2)
  in let (n'',e) = type_mcc [] n' (l,mcc) in
  (n'',utilise_equations_simplifiees (simplifie_equations e) mcc);;

let type_programme (p:prog) tri_cc =
  let (l,e)=p in
  let rec type_composantes n cc_precedentes = function
    | [] -> (n,cc_precedentes)
    | t::q ->
	let (n',t)=type_composante_connexe cc_precedentes n t in
	type_composantes n' (t@cc_precedentes) q
  in 
  let (k,equations)=type_composantes 0 [] (map (map (function t->(t,assoc t l))) tri_cc) in
  let (_,t,equ)=type_expr [] [] equations [] k e in
  let t'=snd (snd (hd (utilise_equations_simplifiees (simplifie_equations equ) [("",([],t))]))) in
  (equations,t');;