src/Pure/unify.ML
changeset 52127 a40dfe02dd83
parent 52126 5386150ed067
child 52128 7f3549a316f4
equal deleted inserted replaced
52126:5386150ed067 52127:a40dfe02dd83
   205 
   205 
   206 exception CANTUNIFY;  (*Signals non-unifiability.  Does not signal errors!*)
   206 exception CANTUNIFY;  (*Signals non-unifiability.  Does not signal errors!*)
   207 exception ASSIGN;  (*Raised if not an assignment*)
   207 exception ASSIGN;  (*Raised if not an assignment*)
   208 
   208 
   209 
   209 
   210 fun unify_types thy (T, U) env =
   210 fun unify_types thy TU env =
   211   if T = U then env
   211   Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY;
   212   else
       
   213     let
       
   214       val Envir.Envir {maxidx, tenv, tyenv} = env;
       
   215       val (tyenv', maxidx') = Sign.typ_unify thy (U, T) (tyenv, maxidx);
       
   216     in Envir.Envir {maxidx = maxidx', tenv = tenv, tyenv = tyenv'} end
       
   217     handle Type.TUNIFY => raise CANTUNIFY;
       
   218 
   212 
   219 fun test_unify_types thy (T, U) env =
   213 fun test_unify_types thy (T, U) env =
   220   let
   214   let
   221     val str_of = Syntax.string_of_typ_global thy;
   215     val str_of = Syntax.string_of_typ_global thy;
   222     fun warn () = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);
   216     fun warn () = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T);