#open "expr";;
#open "types";;
#open "divers";;
#open "global";;

exception MembreDroitLetRec;;
exception ConstructeurAttendu;;

let type_cst = function
  | CstEntier _  -> base_int
  | CstBooleen _ -> base_bool
  | CstUnit      -> base_unit
  | CstCar _     -> base_car
  | CstChaine _  -> base_chaine
  | CstListeVide -> Type_liste (fraiche_alpha ());;

let type_op = function
  | OpAdd|OpMoins|OpMult|OpDiv ->
        Type_fonct(Type_prod(base_int, base_int), base_int)
  | OpEt|OpOu ->
        Type_fonct(Type_prod(base_bool, base_bool), base_bool)
  | OpNot  -> Type_fonct(base_bool, base_bool)
  | OpNeg  -> Type_fonct(base_int, base_int)
  | OpEgal ->
        let a=fraiche_alpha () in Type_fonct(Type_prod(a,a), base_bool)
  | OpInfEgal|OpInf ->
        Type_fonct(Type_prod(base_int,base_int), base_bool)
  | OpFirst  ->
        let a=fraiche_alpha () and b=fraiche_alpha () in
        Type_fonct(Type_prod(a,b),a)
  | OpSecond ->
        let a=fraiche_alpha () and b=fraiche_alpha () in
        Type_fonct(Type_prod(a,b),b)
  | OpITH  ->
        let a=fraiche_alpha () in
        Type_fonct(Type_prod(Type_base Base_Bool, Type_prod(a,a)), a)
  | OpCons ->
        let a=fraiche_alpha () in
        Type_fonct(Type_prod(a, Type_liste a), Type_liste a)
  | OpHead ->
        let a=fraiche_alpha () in
        Type_fonct(Type_liste a, a)
  | OpTail ->
        let a=fraiche_alpha () in
        Type_fonct(Type_liste a, Type_liste a)
  | OpRef ->
        let a=fraiche_alpha () in
        Type_fonct(a, Type_ref a)
  | OpAffect ->
        let a=fraiche_alpha () in
        Type_fonct(Type_prod (Type_ref a, a), type_cst CstUnit)
  | OpIndirect ->
        let a=fraiche_alpha () in
        Type_fonct(Type_ref a,a)
  | OpSeq ->
        let a=fraiche_alpha () and b=fraiche_alpha () in
        Type_fonct(Type_prod (a,b), b);;

let op_sur = function
 OpRef -> false
| _ -> true;;

(* Si une expression est sure, elle ne risque pas de creer de nouveaux objets mutables *)
let rec expr_sure expr =
match expr.e_desc with
  ExprCst _ | ExprIdent _ | ExprFunc _ -> true
| ExprOp (op,a) -> op_sur op && (expr_sure a)
| ExprAppl _ -> false
| ExprLet (_,decl,corps) -> expr_sure corps && (for_all (fun (id,e)->expr_sure e)) decl
| ExprPaire (a,b) -> expr_sure a && expr_sure b
| ExprMatch (x,a) -> expr_sure x && (for_all (fun (_,e) -> expr_sure e)) a;;

let get_id env x =
  try assoc x env with
  Not_found ->
  try (global_ids.find x).typ with
  Not_found -> failwith ("Identificateur non lié :"^x);;




let rec inferer env expr =
(* pr "debut inferer "; affiche_expr expr; pr "\n";  *)
 let t=type_expr env (expr.e_desc) in
 expr.e_type<-t;
(* pr "fin inferer "; affiche_expr expr; pr "\n"; pr "===>"; afficher_typeexpr t; *)
 t
and
 type_expr env = function
  ExprCst c   -> type_cst c
| ExprIdent i -> instancier (get_id env i)
| ExprOp (op,ex) ->
        let t1=inferer env ex
        and t2=type_op op
        and a =fraiche_alpha () in
        unifier (Type_fonct(t1,a)) t2;
        a
| ExprFunc (x,ex) ->
        let a=fraiche_alpha() and b=fraiche_alpha() in
        let ab=Type_fonct(a,b) in
        let nenv=(x,a)::env in
        let t1=inferer nenv ex in
        unifier b t1;
        ab
| ExprAppl (fonc,arg) ->
        let t1=inferer env fonc
        and t2=inferer env arg
        and a =fraiche_alpha () in
        unifier t1 (Type_fonct(t2,a));
        a
| ExprPaire (a,b) -> Type_prod(inferer env a, inferer env b)
| ExprLet (recurs,decl,corps) -> inferer (typer_let env (recurs,decl)) corps
| ExprMatch (e,act) ->
        let t1=inferer env e
        and a =fraiche_alpha () in
        do_list (typer_action env t1 a) act;
        a

and typer_pat env tpat = function
|PatId x  -> (x,tpat)::env
|PatConstr (constr,x) -> 
  match constr with
   | CBloc (_,a,b) -> 
      let (a,b)=instancier2 a b  in 
      unifier b tpat; (x,a)::env
   | CCst  (_,a) -> unifier (instancier a) tpat; env

(*
|PatCst c -> unifier (type_cst c) tpat; env
|PatId x  -> (x,tpat)::env
|PatCouple (a,b) ->
        let ta=fraiche_alpha() and tb=fraiche_alpha() in
        unifier (Type_prod (ta,tb)) tpat;
        typer_pat (typer_pat env ta a) tb b
|PatConstr (x,p) -> env
*)

and typer_action env tpat tex (pat,ex) =
        let nenv=typer_pat env tpat pat in
        unifier tex (inferer nenv ex)

and typer_let env (recurs,decl) =
   incr niveau_courant;
   if recurs then do_list (fun (_,{e_desc=(ExprFunc _)}) -> () | _ -> raise MembreDroitLetRec) decl;
   let ts,nenv=
    if recurs then
    begin
     let alphas=map (fun x->fraiche_alpha()) decl in
     let nenv=it_list2 (fun e (x,def) a -> (x,a)::e) env decl alphas in
     let ts=map (fun (x,def) -> inferer nenv def) decl in
     do_list2 (fun t a -> unifier t a) ts alphas;
     ts, nenv
    end else
     let ts=map (fun (x,def) -> inferer env def) decl in
     let nenv=it_list2 (fun e (x,def) t -> (x,t)::e) env decl ts in
     ts, nenv
   in
   decr niveau_courant;
   let gens=map (fun (x,def) -> expr_sure def) decl in
   do_list2 (fun t gen -> if not gen then abaisse_niveau t) ts gens;
   do_list2 (fun t gen -> if gen then generalise t) ts gens;
   nenv;;