# HG changeset patch # User wenzelm # Date 1426846148 -3600 # Node ID cb1966f3a92b4088237496f40a32b5240ecef35b # Parent 96abba46955f65a5fd1d6ff656a46b0a43f6e8b7 tuned -- prepare instantiation more uniformly; diff -r 96abba46955f -r cb1966f3a92b src/Pure/Tools/rule_insts.ML --- a/src/Pure/Tools/rule_insts.ML Thu Mar 19 22:31:23 2015 +0100 +++ b/src/Pure/Tools/rule_insts.ML Fri Mar 20 11:09:08 2015 +0100 @@ -48,8 +48,6 @@ fun error_var msg (xi, pos) = error (msg ^ quote (Term.string_of_vname xi) ^ Position.here pos); -local - fun the_sort tvars (xi, pos) : sort = (case AList.lookup (op =) tvars xi of SOME S => S @@ -60,6 +58,8 @@ SOME T => T | NONE => error_var "No such variable in theorem: " (xi, pos)); +local + fun instantiate inst = Term_Subst.instantiate ([], map (fn (xi, t) => ((xi, Term.fastype_of t), t)) inst) #> Envir.beta_norm; @@ -78,6 +78,15 @@ in +fun readT ctxt tvars ((xi, pos), s) = + let + val S = the_sort tvars (xi, pos); + val T = Syntax.read_typ ctxt s; + in + if Sign.of_sort (Proof_Context.theory_of ctxt) (T, S) then ((xi, S), T) + else error_var "Incompatible sort for typ instantiation of " (xi, pos) + end; + fun read_termTs ctxt ss Ts = let fun parse T = if T = propT then Syntax.parse_prop ctxt else Syntax.parse_term ctxt; @@ -88,27 +97,17 @@ |> Variable.polymorphic ctxt; val Ts' = map Term.fastype_of ts'; val tyenv = fold Type.raw_match (Ts ~~ Ts') Vartab.empty; - in (ts', map (apsnd snd) (Vartab.dest tyenv)) end; + val tyenv' = Vartab.fold (fn (xi, (S, T)) => cons ((xi, S), T)) tyenv []; + in (ts', tyenv') end; -fun read_insts ctxt mixed_insts (tvars, vars) = +fun read_insts ctxt (tvars, vars) mixed_insts = let - val thy = Proof_Context.theory_of ctxt; - val (type_insts, term_insts) = partition_insts mixed_insts; (* type instantiations *) - fun readT ((xi, pos), s) = - let - val S = the_sort tvars (xi, pos); - val T = Syntax.read_typ ctxt s; - in - if Sign.of_sort thy (T, S) then ((xi, S), T) - else error_var "Incompatible sort for typ instantiation of " (xi, pos) - end; - - val instT1 = Term_Subst.instantiateT (map readT type_insts); + val instT1 = Term_Subst.instantiateT (map (readT ctxt tvars) type_insts); val vars1 = map (apsnd instT1) vars; @@ -118,7 +117,7 @@ val Ts = map (the_type vars1) xs; val (ts, inferred) = read_termTs ctxt ss Ts; - val instT2 = Term.typ_subst_TVars inferred; + val instT2 = Term_Subst.instantiateT inferred; val vars2 = map (apsnd instT2) vars1; val inst2 = instantiate (map #1 xs ~~ ts); @@ -139,7 +138,7 @@ |> Variable.declare_thm thm; val tvars = Thm.fold_terms Term.add_tvars thm []; val vars = Thm.fold_terms Term.add_vars thm []; - val insts = read_insts ctxt' mixed_insts (tvars, vars); + val insts = read_insts ctxt' (tvars, vars) mixed_insts; in Drule.instantiate_normalize insts thm |> singleton (Proof_Context.export ctxt' ctxt) @@ -212,11 +211,12 @@ fun bires_inst_tac bires_flag ctxt mixed_insts thm i st = CSUBGOAL (fn (cgoal, _) => let - val thy = Proof_Context.theory_of ctxt; + val (Tinsts, tinsts) = partition_insts mixed_insts; + - val (Tinsts, tinsts) = partition_insts mixed_insts; + (* goal context *) + val goal = Thm.term_of cgoal; - val params = Logic.strip_params goal (*as they are printed: bound variables with the same name are renamed*) @@ -228,37 +228,18 @@ |> Proof_Context.add_fixes (map (fn (x, T) => (Binding.name x, SOME T, NoSyn)) params); - (* process type insts: Tinsts_env *) + (* preprocess rule *) - val (rtypes, rsorts) = Drule.types_sorts thm; - fun readT ((xi, pos), s) = - let - val S = - (case rsorts xi of - SOME S => S - | NONE => error_var "No such type variable in theorem: " (xi, pos)); - val T = Syntax.read_typ ctxt' s; - val U = TVar (xi, S); - in - if Sign.typ_instance thy (T, U) then (U, T) - else error_var "Cannot instantiate: " (xi, pos) - end; - val Tinsts_env = map readT Tinsts; + val tvars = Thm.fold_terms Term.add_tvars thm []; + val vars = Thm.fold_terms Term.add_vars thm []; - - (* preprocess rule: extract vars and their types, apply Tinsts *) - - fun get_typ (xi, pos) = - (case rtypes xi of - SOME T => typ_subst_atomic Tinsts_env T - | NONE => error_var "No such variable in theorem: " (xi, pos) xi); + val Tinsts_env = map (readT ctxt' tvars) Tinsts; val (xis, ss) = split_list tinsts; - val Ts = map get_typ xis; + val Ts = map (Term_Subst.instantiateT Tinsts_env o the_type vars) xis; val (ts, envT) = read_termTs (Proof_Context.set_mode Proof_Context.mode_schematic ctxt') ss Ts; - val envT' = - map (fn (xi, T) => (TVar (xi, the (rsorts xi)), T)) envT @ Tinsts_env; + val envT' = map (fn (v, T) => (TVar v, T)) (envT @ Tinsts_env); val cenv = map (fn ((xi, _), t) => apply2 (Thm.cterm_of ctxt') (Var (xi, fastype_of t), t)) (distinct diff -r 96abba46955f -r cb1966f3a92b src/Pure/drule.ML --- a/src/Pure/drule.ML Thu Mar 19 22:31:23 2015 +0100 +++ b/src/Pure/drule.ML Fri Mar 20 11:09:08 2015 +0100 @@ -58,7 +58,6 @@ val strip_comb: cterm -> cterm * cterm list val strip_type: ctyp -> ctyp list * ctyp val beta_conv: cterm -> cterm -> cterm - val types_sorts: thm -> (indexname-> typ option) * (indexname-> sort option) val flexflex_unique: Proof.context option -> thm -> thm val export_without_context: thm -> thm val export_without_context_open: thm -> thm @@ -172,27 +171,6 @@ -(*** Find the type (sort) associated with a (T)Var or (T)Free in a term - Used for establishing default types (of variables) and sorts (of - type variables) when reading another term. - Index -1 indicates that a (T)Free rather than a (T)Var is wanted. -***) - -fun types_sorts thm = - let - val vars = Thm.fold_terms Term.add_vars thm []; - val frees = Thm.fold_terms Term.add_frees thm []; - val tvars = Thm.fold_terms Term.add_tvars thm []; - val tfrees = Thm.fold_terms Term.add_tfrees thm []; - fun types (a, i) = - if i < 0 then AList.lookup (op =) frees a else AList.lookup (op =) vars (a, i); - fun sorts (a, i) = - if i < 0 then AList.lookup (op =) tfrees a else AList.lookup (op =) tvars (a, i); - in (types, sorts) end; - - - - (** Standardization of rules **) (*Generalization over a list of variables*)