unifyType.ml

(** Time-stamp: <modified the 28/08/2008 (at 17:26) 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_eff

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
    | 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 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
      print_string (
	" ==> try UnifyType.proposition1 with lists " ^ 
	  (LicDump.type_eff_list_to_string tl1) ^ " and " ^ 
	  (LicDump.type_eff_list_to_string tl2) ^ "\n");
      assert (proposition1 tl1 tl2)
  done