--- 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"
--- 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)
--- 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)
--- 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
--- 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 **)
--- 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;
--- 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, ...})) =
--- 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 {
--- 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