(** 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