187 Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY; |
187 Pattern.unify_types thy TU env handle Pattern.Unif => raise CANTUNIFY; |
188 |
188 |
189 fun test_unify_types thy (T, U) env = |
189 fun test_unify_types thy (T, U) env = |
190 let |
190 let |
191 val str_of = Syntax.string_of_typ_global thy; |
191 val str_of = Syntax.string_of_typ_global thy; |
192 fun warn () = tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T); |
192 fun warn () = |
|
193 if Context_Position.is_visible_global thy then |
|
194 tracing ("Potential loss of completeness: " ^ str_of U ^ " = " ^ str_of T) |
|
195 else (); |
193 val env' = unify_types thy (T, U) env; |
196 val env' = unify_types thy (T, U) env; |
194 in if is_TVar T orelse is_TVar U then warn () else (); env' end; |
197 in if is_TVar T orelse is_TVar U then warn () else (); env' end; |
195 |
198 |
196 (*Is the term eta-convertible to a single variable with the given rbinder? |
199 (*Is the term eta-convertible to a single variable with the given rbinder? |
197 Examples: ?a ?f(B.0) ?g(B.1,B.0) |
200 Examples: ?a ?f(B.0) ?g(B.1,B.0) |
570 |
573 |
571 (*Print a tracing message + list of dpairs. |
574 (*Print a tracing message + list of dpairs. |
572 In t==u print u first because it may be rigid or flexible -- |
575 In t==u print u first because it may be rigid or flexible -- |
573 t is always flexible.*) |
576 t is always flexible.*) |
574 fun print_dpairs thy msg (env, dpairs) = |
577 fun print_dpairs thy msg (env, dpairs) = |
575 let |
578 if Context_Position.is_visible_global thy then |
576 fun pdp (rbinder, t, u) = |
579 let |
577 let |
580 fun pdp (rbinder, t, u) = |
578 fun termT t = |
581 let |
579 Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t))); |
582 fun termT t = |
580 val bsymbs = [termT u, Pretty.str " =?=", Pretty.brk 1, termT t]; |
583 Syntax.pretty_term_global thy (Envir.norm_term env (Logic.rlist_abs (rbinder, t))); |
581 in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end; |
584 val bsymbs = [termT u, Pretty.str " =?=", Pretty.brk 1, termT t]; |
582 in tracing msg; List.app pdp dpairs end; |
585 in tracing (Pretty.string_of (Pretty.blk (0, bsymbs))) end; |
|
586 in tracing msg; List.app pdp dpairs end |
|
587 else (); |
583 |
588 |
584 |
589 |
585 (*Unify the dpairs in the environment. |
590 (*Unify the dpairs in the environment. |
586 Returns flex-flex disagreement pairs NOT IN normal form. |
591 Returns flex-flex disagreement pairs NOT IN normal form. |
587 SIMPL may raise exception CANTUNIFY. *) |
592 SIMPL may raise exception CANTUNIFY. *) |
600 in |
605 in |
601 (case flexrigid of |
606 (case flexrigid of |
602 [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq) |
607 [] => SOME (fold_rev (add_ffpair thy) flexflex (env', []), reseq) |
603 | dp :: frigid' => |
608 | dp :: frigid' => |
604 if tdepth > search_bound then |
609 if tdepth > search_bound then |
605 (warning "Unification bound exceeded"; Seq.pull reseq) |
610 (Context_Position.if_visible_global thy warning "Unification bound exceeded"; |
|
611 Seq.pull reseq) |
606 else |
612 else |
607 (if tdepth > trace_bound then |
613 (if tdepth > trace_bound then |
608 print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) |
614 print_dpairs thy "Enter MATCH" (env',flexrigid@flexflex) |
609 else (); |
615 else (); |
610 Seq.pull (Seq.it_right |
616 Seq.pull (Seq.it_right |
611 (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq)))) |
617 (add_unify (tdepth + 1)) (MATCH thy (env',dp, frigid'@flexflex), reseq)))) |
612 end |
618 end |
613 handle CANTUNIFY => |
619 handle CANTUNIFY => |
614 (if tdepth > trace_bound then tracing "Failure node" else (); |
620 (if tdepth > trace_bound then Context_Position.if_visible_global thy tracing "Failure node" |
615 Seq.pull reseq)); |
621 else (); Seq.pull reseq)); |
616 val dps = map (fn (t, u) => ([], t, u)) tus; |
622 val dps = map (fn (t, u) => ([], t, u)) tus; |
617 in add_unify 1 ((env, dps), Seq.empty) end; |
623 in add_unify 1 ((env, dps), Seq.empty) end; |
618 |
624 |
619 fun unifiers (params as (thy, env, tus)) = |
625 fun unifiers (params as (thy, env, tus)) = |
620 Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty |
626 Seq.cons (fold (Pattern.unify thy) tus env, []) Seq.empty |