unifyType.ml

(** Time-stamp: <modified the 03/03/2009 (at 18:00) by Erwan Jahier> *)

open Eff

(* exported *)
type t = 
  | Equal
  | Unif of Eff.type_
  | Ko of string (* a msg explaining why the unification failed *)

let teff2str = LicDump.string_of_type_eff4msg

let (is_overloadable : Eff.type_ -> bool) = function
  | Int_type_eff -> true
  | Real_type_eff -> true
  | _ -> false
  

(* [contains t1 t2] is true iff t2 appears in t1 *)
let rec (contains : Eff.type_ -> Eff.type_ -> bool) =
  fun t1 t2 -> 
    if t1 = t2 then true else
    match t1 with
    | Any 
    | Overload
    | Bool_type_eff 
    | Int_type_eff 
    | Real_type_eff 
    | Enum_type_eff(_,_) 
    | External_type_eff _ -> false
    | Abstract_type_eff (_, teff) -> false
    | Array_type_eff(teff,i) -> contains teff t2
    | Struct_type_eff(l, fl) -> 
	List.exists (fun (_,(teff,_)) -> contains teff t2) fl
    

(* exported *)
let (f : Eff.type_ list -> Eff.type_ list -> t) = fun l1 l2 -> 
  let rec (unify_type_eff : Eff.type_ -> Eff.type_ -> t) =
    fun t1 t2 -> 
      if t1 = t2 then Equal else  
	match (t1,t2) with
	  | Array_type_eff(teff_ext1,i1), Array_type_eff(teff_ext2,i2) -> 
	      if i1 <> i2 then Ko "\n*** incompatible array size" else
		unify_type_eff teff_ext1 teff_ext2
		  
	  | Struct_type_eff(l1, fl1), Struct_type_eff(l2, fl2) -> 
	      if l1 <> l2 then Ko "\n*** incompatible structure" else
		let fl1 = List.map (fun (_,(te,_)) -> te) fl1
		and fl2 = List.map (fun (_,(te,_)) -> te) fl2 in
		  List.fold_left2 unify_do_acc Equal fl1 fl2
		    
	  | Overload, Any
	  | Any, Overload -> Unif Overload

	  | t, Any 
	  | Any, t -> 
	      if contains t Any || contains t Overload then 
		Ko(("\n*** " ^ teff2str t1) ^ " and " ^ (teff2str t2) ^ 
		     " are not unifiable (there is a cycle)") 
	      else 
		Unif t

	  | t, Overload 
	  | Overload, t -> 
	      if contains t Any || contains t Overload then 
		Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^ 
		     " are not unifiable (there is a cycle)") 
	      else if is_overloadable t then 
		Unif t 
	      else 
		Ko("\n*** " ^ (teff2str t) ^ " should be an integer or a real")
		  
	  | _ -> 
	      Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^
		   " are not unifiable")

  and (unify_do_acc: t -> Eff.type_ -> Eff.type_ -> t) =
    fun acc te1 te2 -> 
      match acc, unify_type_eff te1 te2 with
	| Equal, Equal -> Equal
	| Ko msg, _ 
	| _, Ko msg -> Ko msg
	| Unif t, Equal
	| Equal, Unif t -> Unif t
	| Unif t1, Unif t2 -> if t1 = t2 then acc else 
	    Ko("\n*** " ^ (teff2str t1) ^ " and " ^ (teff2str t2) ^
		 " are not unifiable")
  in
    assert (List.length l1 = List.length l2);
    List.fold_left2 unify_do_acc Equal l1 l2


(************************************************************************************)
(* Some unit tests *)
let i = Int_type_eff
let r = Real_type_eff
let b = Bool_type_eff
let e = External_type_eff (Ident.long_of_string "Toto::t")
let o = Overload
let a = Any
let array t c = Array_type_eff(t,c)
let struc t = Struct_type_eff ((Ident.long_of_string "T::t"), 
				   [(Ident.of_string "x"),(t,None)])

let unify_failed = function Ko(_) -> true | _  -> false
let to_string = function 
  | Ko(msg) -> msg
  | Equal -> "types are equals\n"
  | Unif t -> "types are unifiable via " ^ (teff2str t) ^ "\n"

  

let proposition1 t1 t2 =
  (* two lists of type are unifiable iff there exists a substitution
     that makes them equal. Hence, if [f] and [subst_type] are
     correct, the following function should always return true *)
  match f t1 t2 with
    | Unif t -> List.map (subst_type t) t1 = List.map (subst_type t) t2
    | _ -> true

(* Since i don't know how to prove proposition1, I generate some random tests *)
let rec gen_random_type_eff () = 
  match Random.int 8 with
    | 0 -> b
    | 1 -> i
    | 2 -> r
    | 3 -> e
    | 4 -> array (gen_random_type_eff ()) 42
    | 5 -> struc (gen_random_type_eff ())
    | 6 -> Any
    | _ -> Overload 

let gen_unifiable_typeff_of_size size =
  let rec aux tl1 tl2 =
    let ntl1 = (gen_random_type_eff ())::tl1 
    and ntl2 = (gen_random_type_eff ())::tl2 in
      if unify_failed (f ntl1 ntl2) then
	aux tl1 tl2
      else
	if List.length ntl1 = size then (ntl1,ntl2) else aux ntl1 ntl2
  in
    aux [] []


let (type_eff_list_to_string : Eff.type_ list -> string) =
  fun tel -> 
    let str_l = List.map LicDump.string_of_type_eff4msg tel in
      String.concat "*" str_l    


let unit_test () = 
  assert( f [i;r;b] [i;r;b] = Equal  );
  assert( f [i;r;b] [i;r;a] = Unif b );
  assert( f [i;r;a] [i;r;a] = Equal  );
  assert( f [i;a;b] [i;b;a] = Unif b );
  assert( f [a] [o]         = Unif o );
  assert( unify_failed(f [a] [ array o 3]) );
  assert( unify_failed(f [a] [ array a 3]) );
  assert( unify_failed(f [o] [ array o 3]) );
  assert( unify_failed(f [array i 4] [array o 3]));
  assert( unify_failed(f [a;a] [r;b]));

  Random.self_init ();
  for i = 1 to 1000 do
    let (tl1, tl2) = gen_unifiable_typeff_of_size (1+ Random.int 10) in
      Verbose.print_string ~level:3 (
	" ==> try UnifyType.proposition1 with lists " ^ 
	  (type_eff_list_to_string tl1) ^ " and " ^ 
	  (type_eff_list_to_string tl2) ^ "\n");
      assert (proposition1 tl1 tl2)
  done

(*****************************************)
(* Check that the interface and the implementation types profile
   declarations are compatible.

   The idea is to consider abstract types as alpha types. The problem
   is that my unification algo works for one type variable only.
   However, it is a very simple [*] case of unification with several
   alpha var, that does not require the general unification
   algorithm. By considering variables one by one, I can use [UnifyType.f].

   [*] it is simpler than the general case because we can have alpha
   var in the provide part.

*)
let (profile_is_compatible: node_key -> Lxm.t -> Eff.type_ list * Eff.type_ list -> 
      Eff.type_ list * Eff.type_ list -> Eff.type_ option) =
  fun nk lxm (ins1, ins2) (outs1, outs2) -> 
    let to_any t = match t with (* consider abstract types as alpha types *)
      | Abstract_type_eff(name, _) -> Any
      | t -> t
    in
    let sot = LicDump.string_of_type_eff4msg in
    let msg_prefix = ("provided node for " ^ (Ident.string_of_long (fst nk)) ^ 
                        " is not compatible with its implementation: ")
    in
    let apply_subst s t = try List.assoc t s with Not_found -> t in
    let unif_types (subst,topt) t_prov t_body = 
      if t_body = Any || t_body = Overload then
        (* Migth occur when a model is instanciated with a polymorphic operator,
           such as Lustre::eq. In such a case, we obtain an Any or an Overload 
           from the implementation part ; the solution then is to replace that Any
           type by the type of the provided part.
        *)
        ( 
          assert (t_prov <> Any); 
          assert (t_prov <> Overload); 
          assert (topt = None || topt = Some t_prov); (* at most one type var per op *)
          (subst, Some t_prov) 
        )
      else
        let t_prov = apply_subst subst t_prov and t_body = apply_subst subst t_body in
        let nt_prov = to_any t_prov in
          match f [nt_prov] [t_body] with
            | Equal -> subst, topt
            | Unif t -> 
                (match t_prov with
                   | Abstract_type_eff(_, tbody) -> 
                       if tbody <> t && t_prov <> t_body then
                         let msg = msg_prefix ^ "\n*** "^(sot tbody)^" <> "^(sot t) in
                           raise(Errors.Compile_error (lxm, msg))
                   | _ -> ()
                );
                (t_prov,t)::subst, topt
            | Ko(msg) -> raise(Errors.Compile_error (lxm, msg_prefix ^ msg))
    in

    let acc = [], None in
    let _ = 
      if List.length ins1 <> List.length ins2 then 
        raise(Errors.Compile_error (lxm, msg_prefix ^ " wrong number of inputs"));
      if List.length outs1 <> List.length outs2 then 
        raise(Errors.Compile_error (lxm, msg_prefix ^ " wrong number of outputs"))
    in
    let acc = List.fold_left2 unif_types acc ins1 ins2 in
    let acc = List.fold_left2 unif_types acc outs1 outs2 in
      snd acc