(* unification for types *) (* $Id: unifier.ml,v 1.27 2000/07/10 18:51:20 alamstei Exp $ *) open Library open Lambda open Types type substitution = (tvar * typeexp) list (* returns true if the tvar alpha occurs in a typeexp b and false otherwise *) let rec occurs alpha b = match b with TVar(beta) -> if (alpha=beta) then true else false | Arrow(c,d) -> ((occurs alpha c) || (occurs alpha d)) | Int -> false | Bool -> false | Sum(tlist) -> List.exists (occurs alpha) tlist | Prod(tlist) -> List.exists (occurs alpha) tlist (* apply the substituion sigma to the type variable alpha *) (* sig: tvar->typeexp *) let apply (sigma:substitution) alpha = try List.assoc alpha sigma with Not_found -> TVar(alpha) (* apply the substitution sigma to the typeexp alpha *) let rec apply_bar sigma alpha = match alpha with TVar(beta) -> apply sigma beta | Arrow(beta, gamma) -> Arrow(apply_bar sigma beta, apply_bar sigma gamma) | Int -> alpha | Bool -> alpha | Sum(tlist) -> Sum(List.map (apply_bar sigma) tlist) | Prod(tlist) -> Prod(List.map (apply_bar sigma) tlist) (* apply the substitution sigma to the type schema schema *) let apply_schema sigma schema = (* renames those bound variables that occurs in newtvars *) let avoid_name_clash newtvars (boundvars,tterm) = let newtvars' = Library.set_intersection newtvars boundvars in let freshtvars = List.map (fun x->(rename_tvar x)) newtvars' in let boundvars' = Library.set_difference boundvars newtvars' in let boundvars'' = Library.set_union boundvars' freshtvars in let freshtvars' = List.map (fun x->TVar(x)) freshtvars in let sigma' = List.combine newtvars' freshtvars' in (boundvars'',apply_bar sigma' tterm) in let domain = Types.free_tvars_of_schema schema in let sigma' = Library.restrict_domain sigma domain in let newtvars = List.map (fun (x,sx) -> Types.free_tvars_of_typeexp sx) sigma in let newtvars' = Library.set_flatten newtvars in let (boundvars',tterm') = avoid_name_clash newtvars' schema in (boundvars', apply_bar sigma' tterm') (* apply a substitution to a list of assumptions *) let rec apply_ctxt sigma l = match l with [] -> [] | (var,s)::t -> (var,apply_schema sigma s)::(apply_ctxt sigma t) (* retuns the composition of two functions. for all variables x, return tau(sigma(x)) *) let compose tau sigma = let domain = (Library.set_union (Library.get_domain tau) (Library.get_domain sigma)) in let f = fun alpha -> (alpha, (apply_bar tau (apply sigma alpha))) in List.map f domain (* attempt to unify typeexps a and b. return the most general unification if one exists otherwise raise exception Exn.Can't_unify. *) let rec unify a b = let rec unify_tlists tlist tlist' = match (tlist,tlist') with (hd::tl,h::t) -> let sigma = unify_tlists tl t in let tau = unify (apply_bar sigma hd) (apply_bar sigma h) in compose tau sigma | ([],[]) -> [] | _ -> raise (Exn.Compiler_exception "Unifier.unify_tlists") in match (a,b) with | (TVar(alpha), TVar(beta)) -> [(alpha, TVar(beta))] | (TVar(alpha),b) -> if (occurs (alpha) b) then raise (Exn.Can't_unify(a,b)) else [(alpha,b)] | (a,TVar(beta)) -> if (occurs beta a) then raise (Exn.Can't_unify(a,b)) else [(beta,a)] | (Arrow(a',a''),Arrow(b',b'')) -> let sigma = unify a' b' in let sigma_a'' = apply_bar sigma a'' and sigma_b'' = apply_bar sigma b'' in let tau = unify sigma_a'' sigma_b'' in compose tau sigma | (Int,Int) -> [] | (Bool,Bool) -> [] | (Prod(tlist),Prod(tlist')) -> if (List.length tlist <> List.length tlist') then raise (Exn.Can't_unify(a,b)) else unify_tlists tlist tlist' | (Sum(tlist),Sum(tlist')) -> if (List.length tlist <> List.length tlist') then raise (Exn.Can't_unify(a,b)) else unify_tlists tlist tlist' | _ -> raise (Exn.Can't_unify(a,b))