# HG changeset patch # User wenzelm # Date 1369836725 -7200 # Node ID 0fa3b456a2679374457b212cff23471baa8267f8 # Parent 4ffe819a9b115d7c4ee7c127ffa6ad2990c5512b unify types of schematic variables in non-lifted case (i.e. "compose variants") -- allow schematic polymorphism, without revisiting HO-unification; diff -r 4ffe819a9b11 -r 0fa3b456a267 src/Pure/thm.ML --- a/src/Pure/thm.ML Wed May 29 12:03:58 2013 +0200 +++ b/src/Pure/thm.ML Wed May 29 16:12:05 2013 +0200 @@ -1593,6 +1593,18 @@ | norm_term_skip _ _ _ = error "norm_term_skip: too few assumptions??"; +(*unify types of schematic variables (non-lifted case)*) +fun unify_var_types thy (th1, th2) env = + let + fun unify_vars (T :: Us) = fold (fn U => Pattern.unify_types thy (T, U)) Us + | unify_vars _ = I; + val add_vars = + full_prop_of #> + fold_aterms (fn Var v => Vartab.insert_list (op =) v | _ => I); + val vars = Vartab.empty |> add_vars th1 |> add_vars th2; + in SOME (Vartab.fold (unify_vars o #2) vars env) end + handle Pattern.Unif => NONE; + (*Composition of object rule r=(A1...Am/B) with proof state s=(B1...Bn/C) Unifies B with Bi, replacing subgoal i (1 <= i <= n) If match then forbid instantiations in proof state @@ -1659,13 +1671,12 @@ handle TERM _ => raise THM("bicompose: 1st premise", 0, [orule]) end; - val env = Envir.empty(Int.max(rmax,smax)); val BBi = if lifted then strip_assums2(B,Bi) else (B,Bi); val dpairs = BBi :: (rtpairs@stpairs); (*elim-resolution: try each assumption in turn*) - fun eres [] = raise THM ("bicompose: no premises", 0, [orule, state]) - | eres (A1 :: As) = + fun eres _ [] = raise THM ("bicompose: no premises", 0, [orule, state]) + | eres env (A1 :: As) = let val A = SOME A1; val (close, asms, concl) = Logic.assum_problems (nlift + 1, A1); @@ -1685,14 +1696,18 @@ in tryasms asms 1 end; (*ordinary resolution*) - fun res () = + fun res env = (case Seq.pull (Unify.unifiers (thy, env, dpairs)) of NONE => Seq.empty | cell as SOME ((_, tpairs), _) => Seq.it_right (addth NONE (newAs (rev rAs, 0, [BBi], tpairs))) (Seq.make (fn () => cell), Seq.empty)); + + val env0 = Envir.empty (Int.max (rmax, smax)); in - if eres_flg then eres (rev rAs) else res () + (case if lifted then SOME env0 else unify_var_types thy (state, orule) env0 of + NONE => Seq.empty + | SOME env => if eres_flg then eres env (rev rAs) else res env) end; end;