# HG changeset patch # User wenzelm # Date 1273478081 -7200 # Node ID 7bf87d844f28c4290ad2c024d5ed49e01ceed026 # Parent 0713931bd76961a53e7a679a9524e51fbe02a165# Parent c3a04614c710829de6cdfd8838173c5c1c8a719a merged diff -r 0713931bd769 -r 7bf87d844f28 src/HOL/HOL.thy --- a/src/HOL/HOL.thy Sun May 09 23:57:56 2010 -0700 +++ b/src/HOL/HOL.thy Mon May 10 09:54:41 2010 +0200 @@ -1869,7 +1869,7 @@ proof assume "PROP ?ofclass" show "PROP ?eq" - by (tactic {* ALLGOALS (rtac (Thm.unconstrain_allTs @{thm equals_eq})) *}) + by (tactic {* ALLGOALS (rtac (Thm.unconstrainT @{thm equals_eq})) *}) (fact `PROP ?ofclass`) next assume "PROP ?eq" diff -r 0713931bd769 -r 7bf87d844f28 src/Pure/General/pretty.scala --- a/src/Pure/General/pretty.scala Sun May 09 23:57:56 2010 -0700 +++ b/src/Pure/General/pretty.scala Mon May 10 09:54:41 2010 +0200 @@ -30,7 +30,8 @@ object Break { def apply(width: Int): XML.Tree = - XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)), List(XML.Text(" " * width))) + XML.Elem(Markup.BREAK, List((Markup.WIDTH, width.toString)), + List(XML.Text(Symbol.spaces(width)))) def unapply(tree: XML.Tree): Option[Int] = tree match { @@ -48,7 +49,7 @@ { def newline: Text = copy(tx = FBreak :: tx, pos = 0, nl = nl + 1) def string(s: String): Text = copy(tx = XML.Text(s) :: tx, pos = pos + s.length) - def blanks(wd: Int): Text = string(" " * wd) + def blanks(wd: Int): Text = string(Symbol.spaces(wd)) def content: List[XML.Tree] = tx.reverse } @@ -126,7 +127,7 @@ def fmt(tree: XML.Tree): List[XML.Tree] = tree match { case Block(_, body) => body.flatMap(fmt) - case Break(wd) => List(XML.Text(" " * wd)) + case Break(wd) => List(XML.Text(Symbol.spaces(wd))) case FBreak => List(XML.Text(" ")) case XML.Elem(name, atts, body) => List(XML.Elem(name, atts, body.flatMap(fmt))) case XML.Text(_) => List(tree) diff -r 0713931bd769 -r 7bf87d844f28 src/Pure/General/symbol.scala --- a/src/Pure/General/symbol.scala Sun May 09 23:57:56 2010 -0700 +++ b/src/Pure/General/symbol.scala Mon May 10 09:54:41 2010 +0200 @@ -13,6 +13,18 @@ object Symbol { + /* spaces */ + + private val static_spaces = " " * 4000 + + def spaces(k: Int): String = + { + require(k >= 0) + if (k < static_spaces.length) static_spaces.substring(0, k) + else " " * k + } + + /* Symbol regexps */ private val plain = new Regex("""(?xs) diff -r 0713931bd769 -r 7bf87d844f28 src/Pure/axclass.ML --- a/src/Pure/axclass.ML Sun May 09 23:57:56 2010 -0700 +++ b/src/Pure/axclass.ML Mon May 10 09:54:41 2010 +0200 @@ -423,7 +423,7 @@ val (c1, c2) = cert_classrel thy rel handle TYPE _ => err (); val th' = th |> Drule.instantiate' [SOME (ctyp_of thy (TVar ((Name.aT, 0), [c1])))] [] - |> Thm.unconstrain_allTs; + |> Thm.unconstrainT; val _ = shyps_topped th' orelse raise Fail "add_classrel: nontop shyps after unconstrain"; in thy @@ -449,7 +449,7 @@ |> (map o apsnd o map_atyps) (K T); val th' = th |> Drule.instantiate' std_vars [] - |> Thm.unconstrain_allTs; + |> Thm.unconstrainT; val _ = shyps_topped th' orelse raise Fail "add_arity: nontop shyps after unconstrain"; in thy diff -r 0713931bd769 -r 7bf87d844f28 src/Pure/logic.ML --- a/src/Pure/logic.ML Sun May 09 23:57:56 2010 -0700 +++ b/src/Pure/logic.ML Mon May 10 09:54:41 2010 +0200 @@ -46,6 +46,7 @@ val name_arity: string * sort list * class -> string val mk_arities: arity -> term list val dest_arity: term -> string * sort list * class + val unconstrainT: sort list -> term -> ((typ -> typ) * ((typ * class) * term) list) * term val protectC: term val protect: term -> term val unprotect: term -> term @@ -269,6 +270,42 @@ in (t, Ss, c) end; +(* internalized sort constraints *) + +fun unconstrainT shyps prop = + let + val present = rev ((fold_types o fold_atyps_sorts) (insert (eq_fst op =)) prop []); + val extra = fold (Sorts.remove_sort o #2) present shyps; + + val n = length present; + val (names1, names2) = Name.invents Name.context Name.aT (n + length extra) |> chop n; + + val present_map = + map2 (fn (T, S) => fn a => (T, TVar ((a, 0), S))) present names1; + val constraints_map = + map2 (fn (_, S) => fn a => (S, TVar ((a, 0), S))) present names1 @ + map2 (fn S => fn a => (S, TVar ((a, 0), S))) extra names2; + + fun atyp_map T = + (case AList.lookup (op =) present_map T of + SOME U => U + | NONE => + (case AList.lookup (op =) constraints_map (Type.sort_of_atyp T) of + SOME U => U + | NONE => raise TYPE ("Dangling type variable", [T], []))); + + val constraints = + maps (fn (_, T as TVar (ai, S)) => + map (fn c => ((T, c), mk_of_class (TVar (ai, []), c))) S) + constraints_map; + + val prop' = + prop + |> (Term.map_types o Term.map_atyps) (Type.strip_sorts o atyp_map) + |> curry list_implies (map snd constraints); + in ((atyp_map, constraints), prop') end; + + (** protected propositions and embedded terms **) diff -r 0713931bd769 -r 7bf87d844f28 src/Pure/term_subst.ML --- a/src/Pure/term_subst.ML Sun May 09 23:57:56 2010 -0700 +++ b/src/Pure/term_subst.ML Mon May 10 09:54:41 2010 +0200 @@ -9,26 +9,20 @@ val map_atypsT_same: typ Same.operation -> typ Same.operation val map_types_same: typ Same.operation -> term Same.operation val map_aterms_same: term Same.operation -> term Same.operation - val map_atypsT_option: (typ -> typ option) -> typ -> typ option - val map_atyps_option: (typ -> typ option) -> term -> term option - val map_types_option: (typ -> typ option) -> term -> term option - val map_aterms_option: (term -> term option) -> term -> term option val generalizeT_same: string list -> int -> typ Same.operation val generalize_same: string list * string list -> int -> term Same.operation + val generalizeT: string list -> int -> typ -> typ val generalize: string list * string list -> int -> term -> term - val generalizeT: string list -> int -> typ -> typ - val generalize_option: string list * string list -> int -> term -> term option - val generalizeT_option: string list -> int -> typ -> typ option val instantiateT_maxidx: ((indexname * sort) * (typ * int)) list -> typ -> int -> typ * int val instantiate_maxidx: ((indexname * sort) * (typ * int)) list * ((indexname * typ) * (term * int)) list -> term -> int -> term * int + val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation + val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> + term Same.operation val instantiateT: ((indexname * sort) * typ) list -> typ -> typ val instantiate: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> term -> term - val instantiateT_same: ((indexname * sort) * typ) list -> typ Same.operation - val instantiate_same: ((indexname * sort) * typ) list * ((indexname * typ) * term) list -> - term Same.operation val zero_var_indexes: term -> term val zero_var_indexes_inst: term list -> ((indexname * sort) * typ) list * ((indexname * typ) * term) list @@ -64,11 +58,6 @@ | term a = f a; in term end; -val map_atypsT_option = Same.capture o map_atypsT_same o Same.function; -val map_atyps_option = Same.capture o map_types_same o map_atypsT_same o Same.function; -val map_types_option = Same.capture o map_types_same o Same.function; -val map_aterms_option = Same.capture o map_aterms_same o Same.function; - (* generalization of fixed variables *) @@ -99,11 +88,8 @@ | gen (t $ u) = (gen t $ Same.commit gen u handle Same.SAME => t $ gen u); in gen tm end; +fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty; fun generalize names i tm = Same.commit (generalize_same names i) tm; -fun generalizeT names i ty = Same.commit (generalizeT_same names i) ty; - -fun generalize_option names i tm = SOME (generalize_same names i tm) handle Same.SAME => NONE; -fun generalizeT_option names i ty = SOME (generalizeT_same names i ty) handle Same.SAME => NONE; (* instantiation of schematic variables (types before terms) -- recomputes maxidx *) @@ -160,18 +146,15 @@ let val maxidx = Unsynchronized.ref i in (Same.commit (inst_same maxidx insts) tm, ! maxidx) end; -fun instantiateT [] ty = ty - | instantiateT instT ty = Same.commit (instT_same (Unsynchronized.ref ~1) (no_indexes1 instT)) ty; - -fun instantiate ([], []) tm = tm - | instantiate insts tm = Same.commit (inst_same (Unsynchronized.ref ~1) (no_indexes2 insts)) tm; - fun instantiateT_same [] _ = raise Same.SAME | instantiateT_same instT ty = instT_same (Unsynchronized.ref ~1) (no_indexes1 instT) ty; fun instantiate_same ([], []) _ = raise Same.SAME | instantiate_same insts tm = inst_same (Unsynchronized.ref ~1) (no_indexes2 insts) tm; +fun instantiateT instT ty = Same.commit (instantiateT_same instT) ty; +fun instantiate inst tm = Same.commit (instantiate_same inst) tm; + end; diff -r 0713931bd769 -r 7bf87d844f28 src/Pure/thm.ML --- a/src/Pure/thm.ML Sun May 09 23:57:56 2010 -0700 +++ b/src/Pure/thm.ML Mon May 10 09:54:41 2010 +0200 @@ -138,8 +138,8 @@ val varifyT_global': (string * sort) list -> thm -> ((string * sort) * indexname) list * thm val of_class: ctyp * class -> thm val strip_shyps: thm -> thm - val unconstrainT: ctyp -> thm -> thm - val unconstrain_allTs: thm -> thm + val unconstrainT: thm -> thm + val legacy_unconstrainT: ctyp -> thm -> thm val legacy_freezeT: thm -> thm val assumption: int -> thm -> thm Seq.seq val eq_assumption: int -> thm -> thm @@ -1221,8 +1221,29 @@ shyps = shyps', hyps = hyps, tpairs = tpairs, prop = prop}) end; -(*Internalize sort constraints of type variable*) -fun unconstrainT +(*Internalize sort constraints of type variables*) +fun unconstrainT (thm as Thm (_, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = + let + fun err msg = raise THM ("unconstrainT: " ^ msg, 0, [thm]); + + val _ = null hyps orelse err "illegal hyps"; + val _ = null tpairs orelse err "unsolved flex-flex constraints"; + val tfrees = rev (Term.add_tfree_names prop []); + val _ = null tfrees orelse err ("illegal free type variables " ^ commas_quote tfrees); + + val (_, prop') = Logic.unconstrainT shyps prop; + in + Thm (deriv_rule0 (Pt.PAxm ("Pure.unconstrainT", prop, SOME [])), + {thy_ref = thy_ref, + tags = [], + maxidx = maxidx_of_term prop', + shyps = [[]], (*potentially redundant*) + hyps = hyps, + tpairs = tpairs, + prop = prop'}) + end; + +fun legacy_unconstrainT (Ctyp {thy_ref = thy_ref1, T, ...}) (th as Thm (_, {thy_ref = thy_ref2, maxidx, shyps, hyps, tpairs, prop, ...})) = let @@ -1242,10 +1263,6 @@ prop = Logic.list_implies (constraints, unconstrain prop)}) end; -fun unconstrain_allTs th = - fold (unconstrainT o ctyp_of (theory_of_thm th) o TVar) - (fold_terms Term.add_tvars th []) th; - (* Replace all TFrees not fixed or in the hyps by new TVars *) fun varifyT_global' fixed (Thm (der, {thy_ref, maxidx, shyps, hyps, tpairs, prop, ...})) = diff -r 0713931bd769 -r 7bf87d844f28 src/Tools/jEdit/src/jedit/isabelle_sidekick.scala --- a/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Sun May 09 23:57:56 2010 -0700 +++ b/src/Tools/jEdit/src/jedit/isabelle_sidekick.scala Mon May 10 09:54:41 2010 +0200 @@ -132,7 +132,7 @@ for ((command, command_start) <- document.command_range(0) if !stopped) { root.add(document.current_state(command).get.markup_root.swing_tree((node: Markup_Node) => { - val content = Pretty.str_of(List(XML.Text(command.source(node.start, node.stop)))) + val content = command.source(node.start, node.stop).replace('\n', ' ') val id = command.id new DefaultMutableTreeNode(new IAsset { diff -r 0713931bd769 -r 7bf87d844f28 src/Tools/nbe.ML --- a/src/Tools/nbe.ML Sun May 09 23:57:56 2010 -0700 +++ b/src/Tools/nbe.ML Mon May 10 09:54:41 2010 +0200 @@ -101,14 +101,16 @@ val prem_thms = map (the o AList.lookup (op =) of_classes o apfst (fst o fst o dest_TVar) o Logic.dest_of_class) prem_props; in Drule.implies_elim_list thm prem_thms end; - in ct + in + (* FIXME avoid legacy operations *) + ct |> Drule.cterm_rule Thm.varifyT_global |> Thm.instantiate_cterm (Thm.certify_inst thy (map (fn (v, ((sort, _), sort')) => (((v, 0), sort), TFree (v, sort'))) vs, [])) |> Drule.cterm_rule Thm.legacy_freezeT |> conv |> Thm.varifyT_global - |> fold (fn (v, (_, sort')) => Thm.unconstrainT (certT (TVar ((v, 0), sort')))) vs + |> fold (fn (v, (_, sort')) => Thm.legacy_unconstrainT (certT (TVar ((v, 0), sort')))) vs |> Thm.certify_instantiate (map (fn (v, ((sort, _), _)) => (((v, 0), []), TVar ((v, 0), sort))) vs, []) |> strip_of_class