# HG changeset patch # User berghofe # Date 1114103583 -7200 # Node ID 016f3be5a5ec98ebe632be7fd6270b363662576c # Parent a6360558257318e8beb7c055f1d59ff24cc72a2c Adapted to new interface of instantiation and unification / matching functions. diff -r a63605582573 -r 016f3be5a5ec TFL/casesplit.ML --- a/TFL/casesplit.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/TFL/casesplit.ML Thu Apr 21 19:13:03 2005 +0200 @@ -162,11 +162,12 @@ case (Thm.concl_of case_thm) of (_ $ ((Pv as Var(P,Pty)) $ (Dv as Var(D, Dty)))) => (Pv, Dv, - Vartab.dest (Type.typ_match tsig (Vartab.empty, (Dty, ty)))) + Type.typ_match tsig (Vartab.empty, (Dty, ty))) | _ => raise ERROR_MESSAGE ("not a valid case thm"); - val type_cinsts = map (apsnd ctypify) type_insts; - val cPv = ctermify (Sign.inst_term_tvars sgn type_insts Pv); - val cDv = ctermify (Sign.inst_term_tvars sgn type_insts Dv); + val type_cinsts = map (fn (ixn, (S, T)) => (ctypify (TVar (ixn, S)), ctypify T)) + (Vartab.dest type_insts); + val cPv = ctermify (Envir.subst_TVars type_insts Pv); + val cDv = ctermify (Envir.subst_TVars type_insts Dv); in (beta_eta_contract (case_thm diff -r a63605582573 -r 016f3be5a5ec TFL/rules.ML --- a/TFL/rules.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/TFL/rules.ML Thu Apr 21 19:13:03 2005 +0200 @@ -276,12 +276,12 @@ local (* this is fragile *) val {prop,sign,...} = rep_thm spec val x = hd (tl (term_vars prop)) - val (TVar (indx,_)) = type_of x + val cTV = ctyp_of sign (type_of x) val gspec = forall_intr (cterm_of sign x) spec in fun SPEC tm thm = let val {sign,T,...} = rep_cterm tm - val gspec' = instantiate([(indx,ctyp_of sign T)],[]) gspec + val gspec' = instantiate ([(cTV, ctyp_of sign T)], []) gspec in thm RS (forall_elim tm gspec') end @@ -295,13 +295,14 @@ (* Not optimized! Too complicated. *) local val {prop,sign,...} = rep_thm allI val [P] = add_term_vars (prop, []) - fun cty_theta s = map (fn (i,ty) => (i, ctyp_of s ty)) - fun ctm_theta s = map (fn (i,tm2) => + fun cty_theta s = map (fn (i, (S, ty)) => (ctyp_of s (TVar (i, S)), ctyp_of s ty)) + fun ctm_theta s = map (fn (i, (_, tm2)) => let val ctm2 = cterm_of s tm2 in (cterm_of s (Var(i,#T(rep_cterm ctm2))), ctm2) end) - fun certify s (ty_theta,tm_theta) = (cty_theta s ty_theta, - ctm_theta s tm_theta) + fun certify s (ty_theta,tm_theta) = + (cty_theta s (Vartab.dest ty_theta), + ctm_theta s (Vartab.dest tm_theta)) in fun GEN v th = let val gth = forall_intr v th diff -r a63605582573 -r 016f3be5a5ec TFL/thry.ML --- a/TFL/thry.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/TFL/thry.ML Thu Apr 21 19:13:03 2005 +0200 @@ -26,17 +26,23 @@ * Matching *---------------------------------------------------------------------------*) -local fun tybind (x,y) = (TVar (x, HOLogic.typeS) , y) - fun tmbind (x,y) = (Var (x, Term.type_of y), y) +local + +fun tybind (ixn, (S, T)) = (TVar (ixn, S), T); + in - fun match_term thry pat ob = - let val tsig = Sign.tsig_of (Theory.sign_of thry) - val (ty_theta,tm_theta) = Pattern.match tsig (pat,ob) - in (map tmbind tm_theta, map tybind ty_theta) - end - fun match_type thry pat ob = map tybind (Vartab.dest - (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat,ob)))) +fun match_term thry pat ob = + let + val tsig = Sign.tsig_of (Theory.sign_of thry) + val (ty_theta, tm_theta) = Pattern.match tsig (pat,ob) + fun tmbind (ixn, (T, t)) = (Var (ixn, Envir.typ_subst_TVars ty_theta T), t) + in (map tmbind (Vartab.dest tm_theta), map tybind (Vartab.dest ty_theta)) + end; + +fun match_type thry pat ob = map tybind (Vartab.dest + (Type.typ_match (Sign.tsig_of (Theory.sign_of thry)) (Vartab.empty, (pat, ob)))); + end; diff -r a63605582573 -r 016f3be5a5ec src/Pure/IsaPlanner/rw_inst.ML --- a/src/Pure/IsaPlanner/rw_inst.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/src/Pure/IsaPlanner/rw_inst.ML Thu Apr 21 19:13:03 2005 +0200 @@ -33,7 +33,7 @@ (string * Term.typ) list -> Thm.thm -> Thm.cterm list * Thm.thm val mk_fixtvar_tyinsts : Term.indexname list -> - Term.term list -> ((string * int) * Term.typ) list * string list + Term.term list -> ((string * int) * Term.typ) list * (string * sort) list val mk_renamings : Term.term -> Thm.thm -> (((string * int) * Term.typ) * Term.term) list val new_tfree : @@ -151,14 +151,14 @@ (* make instantiations to fix type variables that are not already instantiated (in ignore_ixs) from the list of terms. *) fun mk_fixtvar_tyinsts ignore_ixs ts = - let val (tvars, tfreenames) = - foldr (fn (t, (varixs, tfreenames)) => + let val (tvars, tfrees) = + foldr (fn (t, (varixs, tfrees)) => (Term.add_term_tvars (t,varixs), - Term.add_term_tfree_names (t,tfreenames))) + Term.add_term_tfrees (t,tfrees))) ([],[]) ts; val unfixed_tvars = List.filter (fn (ix,s) => not (ix mem ignore_ixs)) tvars; - val (fixtyinsts, _) = foldr new_tfree ([], tfreenames) unfixed_tvars - in (fixtyinsts, tfreenames) end; + val (fixtyinsts, _) = foldr new_tfree ([], map fst tfrees) unfixed_tvars + in (fixtyinsts, tfrees) end; (* cross-instantiate the instantiations - ie for each instantiation @@ -212,10 +212,13 @@ val ctyp_insts = map (apsnd ctypeify) typinsts; (* type instantiated versions *) - val tgt_th_tyinst = - Thm.instantiate (ctyp_insts, []) target_thm; - val rule_tyinst = - Thm.instantiate (ctyp_insts, []) rule; + fun tyinst insts rule = + let val (_, rsorts) = types_sorts rule + in Thm.instantiate (List.mapPartial (fn (ixn, cT) => Option.map + (fn S => (ctypeify (TVar (ixn, S)), cT)) (rsorts ixn)) insts, []) rule + end; + val tgt_th_tyinst = tyinst ctyp_insts target_thm; + val rule_tyinst = tyinst ctyp_insts rule; (* type instanitated outer term *) val outerterm_tyinst = diff -r a63605582573 -r 016f3be5a5ec src/Pure/IsaPlanner/term_lib.ML --- a/src/Pure/IsaPlanner/term_lib.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/src/Pure/IsaPlanner/term_lib.ML Thu Apr 21 19:13:03 2005 +0200 @@ -143,7 +143,10 @@ (* Higher order matching with exception handled *) (* returns optional instantiation *) fun clean_match tsig (a as (pat, t)) = - SOME (Pattern.match tsig a) handle Pattern.MATCH => NONE; + let val (tyenv, tenv) = Pattern.match tsig a + in SOME (map (apsnd snd) (Vartab.dest tyenv), + map (apsnd snd) (Vartab.dest tenv)) + end handle Pattern.MATCH => NONE; (* Higher order unification with exception handled, return the instantiations *) (* given Signature, max var index, pat, tgt *) (* returns Seq of instantiations *) @@ -166,7 +169,8 @@ (* is it right to throw away the flexes? or should I be using them somehow? *) fun mk_insts (env,flexflexes) = - (Vartab.dest (Envir.type_env env), Envir.alist_of env); + (map (apsnd snd) (Vartab.dest (Envir.type_env env)), + map (apsnd snd) (Envir.alist_of env)); val initenv = Envir.Envir {asol = Vartab.empty, iTs = typinsttab, maxidx = ix2}; val useq = (Unify.unifiers (sgn,initenv,[a])) diff -r a63605582573 -r 016f3be5a5ec src/Pure/Isar/attrib.ML --- a/src/Pure/Isar/attrib.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/src/Pure/Isar/attrib.ML Thu Apr 21 19:13:03 2005 +0200 @@ -260,13 +260,14 @@ fun typ_subst env = apsnd (Term.typ_subst_TVars env); fun subst env = apsnd (Term.subst_TVars env); -fun instantiate sign envT env = +fun instantiate sign envT env thm = let - fun prepT (a, T) = (a, Thm.ctyp_of sign T); + val (_, sorts) = Drule.types_sorts thm; + fun prepT (a, T) = (Thm.ctyp_of sign (TVar (a, the_sort sorts a)), Thm.ctyp_of sign T); fun prep (xi, t) = pairself (Thm.cterm_of sign) (Var (xi, Term.fastype_of t), t); in Drule.instantiate (map prepT (distinct envT), - map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) + map prep (gen_distinct (fn ((xi, t), (yj, u)) => xi = yj andalso t aconv u) env)) thm end; in @@ -309,8 +310,8 @@ (* internal term instantiations *) val types' = #1 (Drule.types_sorts thm'); - val unifier = Vartab.dest (#1 - (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts))); + val unifier = map (apsnd snd) (Vartab.dest (#1 + (Library.foldl (unify_types sign types') ((Vartab.empty, 0), internal_insts)))); val type_insts'' = map (typ_subst unifier) type_insts'; val internal_insts'' = map (subst unifier) internal_insts; diff -r a63605582573 -r 016f3be5a5ec src/Pure/Isar/locale.ML --- a/src/Pure/Isar/locale.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/src/Pure/Isar/locale.ML Thu Apr 21 19:13:03 2005 +0200 @@ -499,7 +499,8 @@ |> Drule.implies_intr_list (map cert hyps) |> Drule.tvars_intr_list (map (#1 o #1) env') |> (fn (th', al) => th' |> - Thm.instantiate ((map (fn ((a, _), T) => (valOf (assoc (al, a)), certT T)) env'), [])) + Thm.instantiate ((map (fn ((a, _), T) => + (certT (TVar (valOf (assoc (al, a)))), certT T)) env'), [])) |> (fn th'' => Drule.implies_elim_list th'' (map (Thm.assume o cert o inst_term env') hyps)) end; @@ -535,7 +536,7 @@ else thm |> Drule.implies_intr_list (map cert hyps) |> Drule.tvars_intr_list (map #1 tinst') |> (fn (th, al) => th |> Thm.instantiate - ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'), + ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'), [])) |> (fn th => Drule.implies_elim_list th (map (Thm.assume o cert o tinst_tab_term tinst) hyps)) @@ -584,7 +585,7 @@ else thm |> Drule.implies_intr_list (map cert hyps) |> Drule.tvars_intr_list (map #1 tinst') |> (fn (th, al) => th |> Thm.instantiate - ((map (fn (a, T) => (valOf (assoc (al, a)), certT T)) tinst'), + ((map (fn (a, T) => (certT (TVar (valOf (assoc (al, a)))), certT T)) tinst'), [])) |> Drule.forall_intr_list (map (cert o #1) inst') |> Drule.forall_elim_list (map (cert o #2) inst') @@ -604,14 +605,14 @@ (* parameter types *) (* CB: frozen_tvars has the following type: - ProofContext.context -> Term.typ list -> (Term.indexname * Term.typ) list *) + ProofContext.context -> Term.typ list -> (Term.indexname * (sort * Term.typ)) list *) fun frozen_tvars ctxt Ts = let val tvars = rev (Library.foldl Term.add_tvarsT ([], Ts)); val tfrees = map TFree (Term.invent_names (ProofContext.used_types ctxt) "'a" (length tvars) ~~ map #2 tvars); - in map #1 tvars ~~ tfrees end; + in map (fn ((x, S), y) => (x, (S, y))) (tvars ~~ tfrees) end; fun unify_frozen ctxt maxidx Ts Us = let @@ -1382,7 +1383,7 @@ (* get their sorts *) val tfrees = foldr Term.add_typ_tfrees [] param_types val Tenv' = map - (fn ((a, i), T) => ((a, valOf (assoc_string (tfrees, a))), T)) + (fn ((a, i), (S, T)) => ((a, S), T)) (Vartab.dest Tenv); (* process (internal) elements *) @@ -1417,7 +1418,7 @@ |> Drule.tvars_intr_list (map (#1 o #1) Tenv') |> (fn (th', al) => th' |> Thm.instantiate ((map (fn ((a, _), T) => - (valOf (assoc (al, a)), certT T)) Tenv'), [])) + (certT (TVar (valOf (assoc (al, a)))), certT T)) Tenv'), [])) |> (fn th'' => Drule.implies_elim_list th'' (map (Thm.assume o cert o inst_term Tenv') hyps)) end; @@ -1623,7 +1624,7 @@ (* type instantiation *) val vtinst = Library.foldl (Type.typ_match (Sign.tsig_of sign)) (Vartab.empty, (parmvTs ~~ map Term.fastype_of ts)); - val tinst = Vartab.dest vtinst |> map (fn ((x, 0), T) => (x, T)) + val tinst = Vartab.dest vtinst |> map (fn ((x, 0), (_, T)) => (x, T)) |> Symtab.make; (* replace parameter names in ids by instantiations *) val vinst = Symtab.make (parms ~~ vts); diff -r a63605582573 -r 016f3be5a5ec src/Pure/Isar/method.ML --- a/src/Pure/Isar/method.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/src/Pure/Isar/method.ML Thu Apr 21 19:13:03 2005 +0200 @@ -354,7 +354,8 @@ fun readT (xi, s) = let val S = case rsorts xi of SOME S => S | NONE => absent xi; val T = Sign.read_typ (sign, sorts) s; - in if Sign.typ_instance sign (T, TVar (xi, S)) then (xi, T) + val U = TVar (xi, S); + in if Sign.typ_instance sign (T, U) then (U, T) else error ("Instantiation of " ^ Syntax.string_of_vname xi ^ " fails") end; @@ -362,7 +363,7 @@ (* Preprocess rule: extract vars and their types, apply Tinsts *) fun get_typ xi = (case rtypes xi of - SOME T => typ_subst_TVars Tinsts_env T + SOME T => typ_subst_atomic Tinsts_env T | NONE => absent xi); val (xis, ss) = Library.split_list tinsts; val Ts = map get_typ xis; @@ -380,7 +381,8 @@ val used = Drule.add_used thm (Drule.add_used st []); val (ts, envT) = ProofContext.read_termTs_schematic ctxt internal types' sorts used (ss ~~ Ts); - val cenvT = map (apsnd (Thm.ctyp_of sign)) (envT @ Tinsts_env); + val envT' = map (fn (ixn, T) => + (TVar (ixn, valOf (rsorts ixn)), T)) envT @ Tinsts_env; val cenv = map (fn (xi, t) => @@ -399,11 +401,9 @@ (params, Logic.incr_indexes(paramTs,inc) t) fun liftpair (cv,ct) = (cterm_fun liftvar cv, cterm_fun liftterm ct) - fun lifttvar((a,i),ctyp) = - let val {T,sign} = rep_ctyp ctyp - in ((a,i+inc), ctyp_of sign (incr_tvar inc T)) end + val lifttvar = pairself (ctyp_of sign o incr_tvar inc); val rule = Drule.instantiate - (map lifttvar cenvT, map liftpair cenv) + (map lifttvar envT', map liftpair cenv) (lift_rule (st, i) thm) in if i > nprems_of st then no_tac st diff -r a63605582573 -r 016f3be5a5ec src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/src/Pure/Isar/proof_context.ML Thu Apr 21 19:13:03 2005 +0200 @@ -562,7 +562,7 @@ let val env = unifyT ctxt (T, U) handle Type.TUNIFY => raise TYPE ("norm_term: ill-typed variable assignment", [T, U], [t, u]); - val u' = Term.subst_TVars_Vartab env u; + val u' = Envir.subst_TVars env u; in norm u' handle SAME => u' end | NONE => if schematic then raise SAME @@ -877,7 +877,7 @@ val _ = (*may not assign variables from text*) if null (map #1 (Envir.alist_of env) inter (map #1 (Drule.vars_of_terms (map #2 pairs)))) then () else fail (); - fun norm_bind (xi, t) = if xi mem domain then SOME (xi, Envir.norm_term env t) else NONE; + fun norm_bind (xi, (_, t)) = if xi mem domain then SOME (xi, Envir.norm_term env t) else NONE; in List.mapPartial norm_bind (Envir.alist_of env) end; diff -r a63605582573 -r 016f3be5a5ec src/Pure/Proof/extraction.ML --- a/src/Pure/Proof/extraction.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/src/Pure/Proof/extraction.ML Thu Apr 21 19:13:03 2005 +0200 @@ -108,11 +108,11 @@ fun ren t = getOpt (Term.rename_abs tm1 tm t, t); val inc = Logic.incr_indexes ([], maxidx_of_term tm + 1); val env as (Tenv, tenv) = Pattern.match tsig (inc tm1, tm); - val prems' = map (pairself (subst_vars env o inc o ren)) prems; + val prems' = map (pairself (Envir.subst_vars env o inc o ren)) prems; val env' = Envir.Envir {maxidx = Library.foldl Int.max (~1, map (Int.max o pairself maxidx_of_term) prems'), - iTs = Vartab.make Tenv, asol = Vartab.make tenv}; + iTs = Tenv, asol = tenv}; val env'' = Library.foldl (fn (env, p) => Pattern.unify (sign, env, [pairself (lookup rew) p])) (env', prems') in SOME (Envir.norm_term env'' (inc (ren tm2))) diff -r a63605582573 -r 016f3be5a5ec src/Pure/Proof/proofchecker.ML --- a/src/Pure/Proof/proofchecker.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/src/Pure/Proof/proofchecker.ML Thu Apr 21 19:13:03 2005 +0200 @@ -40,7 +40,8 @@ let val tvars = term_tvars (prop_of thm); val (thm', fmap) = Thm.varifyT' [] thm; - val ctye = map fst tvars @ map snd fmap ~~ map (Thm.ctyp_of sg) Ts + val ctye = map (pairself (Thm.ctyp_of sg)) + (map TVar tvars @ map (fn ((_, S), ixn) => TVar (ixn, S)) fmap ~~ Ts) in Thm.instantiate (ctye, []) (forall_intr_vars (forall_intr_frees thm')) end; diff -r a63605582573 -r 016f3be5a5ec src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Thu Apr 21 19:12:03 2005 +0200 +++ b/src/Pure/Proof/reconstruct.ML Thu Apr 21 19:13:03 2005 +0200 @@ -42,7 +42,7 @@ fun merge_envs (Envir.Envir {asol=asol1, iTs=iTs1, maxidx=maxidx1}) (Envir.Envir {asol=asol2, iTs=iTs2, maxidx=maxidx2}) = - Envir.Envir {asol=Vartab.merge (op aconv) (asol1, asol2), + Envir.Envir {asol=Vartab.merge (op =) (asol1, asol2), iTs=Vartab.merge (op =) (iTs1, iTs2), maxidx=Int.max (maxidx1, maxidx2)}; @@ -67,8 +67,8 @@ handle Type.TUNIFY => error ("Non-unifiable types:\n" ^ Sign.string_of_typ sg T ^ "\n\n" ^ Sign.string_of_typ sg U); -fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar (ixn, _)) = - (case Vartab.lookup (iTs, ixn) of NONE => T | SOME T' => chaseT env T') +fun chaseT (env as Envir.Envir {iTs, ...}) (T as TVar ixnS) = + (case Type.lookup (iTs, ixnS) of NONE => T | SOME T' => chaseT env T') | chaseT _ T = T; fun infer_type sg (env as Envir.Envir {maxidx, asol, iTs}) Ts vTs @@ -247,8 +247,8 @@ val Envir.Envir {asol, iTs, ...} = env; val dom = Vartab.foldl (uncurry (cons o fst) o Library.swap) (Vartab.foldl (uncurry (cons o fst) o Library.swap) ([], asol), iTs); - val vran = Vartab.foldl (add_typ_ixns o apsnd snd) - (Vartab.foldl (add_term_ixns o apsnd snd) ([], asol), iTs); + val vran = Vartab.foldl (add_typ_ixns o apsnd (snd o snd)) + (Vartab.foldl (add_term_ixns o apsnd (snd o snd)) ([], asol), iTs); fun check_cs [] = [] | check_cs ((u, p, vs)::ps) = let val vs' = vs \\ dom;