# HG changeset patch # User wenzelm # Date 1248360795 -7200 # Node ID 8228f67bfe182b72c1c77c815e2272b47876c6d6 # Parent 0ddf61f96b2af9204e6ea63de150696f83b6b003# Parent 4937d98368247edbfb6805aefab071352d854a40 merged diff -r 0ddf61f96b2a -r 8228f67bfe18 Admin/isatest/settings/mac-poly-M4 --- a/Admin/isatest/settings/mac-poly-M4 Thu Jul 23 15:59:14 2009 +0200 +++ b/Admin/isatest/settings/mac-poly-M4 Thu Jul 23 16:53:15 2009 +0200 @@ -4,7 +4,7 @@ ML_SYSTEM="polyml-experimental" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="--mutable 600 --immutable 1800" + ML_OPTIONS="--mutable 800 --immutable 2000" ISABELLE_HOME_USER=~/isabelle-mac-poly-M4 diff -r 0ddf61f96b2a -r 8228f67bfe18 Admin/isatest/settings/mac-poly-M8 --- a/Admin/isatest/settings/mac-poly-M8 Thu Jul 23 15:59:14 2009 +0200 +++ b/Admin/isatest/settings/mac-poly-M8 Thu Jul 23 16:53:15 2009 +0200 @@ -4,7 +4,7 @@ ML_SYSTEM="polyml-experimental" ML_PLATFORM="x86-darwin" ML_HOME="$POLYML_HOME/$ML_PLATFORM" - ML_OPTIONS="--mutable 600 --immutable 1800" + ML_OPTIONS="--mutable 800 --immutable 2000" ISABELLE_HOME_USER=~/isabelle-mac-poly-M8 diff -r 0ddf61f96b2a -r 8228f67bfe18 src/HOL/Tools/Function/lexicographic_order.ML --- a/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/HOL/Tools/Function/lexicographic_order.ML Thu Jul 23 16:53:15 2009 +0200 @@ -140,7 +140,7 @@ fun pr_table table = writeln (cat_lines (map (fn r => concat (map pr_cell r)) table)) fun pr_goals ctxt st = - Display_Goal.pretty_goals_aux (Syntax.pp ctxt) Markup.none (true, false) (Thm.nprems_of st) st + Display_Goal.pretty_goals ctxt Markup.none (true, false) (Thm.nprems_of st) st |> Pretty.chunks |> Pretty.string_of diff -r 0ddf61f96b2a -r 8228f67bfe18 src/Pure/Isar/proof.ML --- a/src/Pure/Isar/proof.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/Pure/Isar/proof.ML Thu Jul 23 16:53:15 2009 +0200 @@ -318,8 +318,6 @@ val show_main_goal = ref false; val verbose = ProofContext.verbose; -val pretty_goals_local = Display_Goal.pretty_goals_aux o Syntax.pp; - fun pretty_facts _ _ NONE = [] | pretty_facts s ctxt (SOME ths) = [Pretty.big_list (s ^ "this:") (map (Display.pretty_thm ctxt) ths), Pretty.str ""]; @@ -346,7 +344,7 @@ (if mode <> Backward orelse null using then NONE else SOME using) @ [Pretty.str ("goal" ^ description [levels_up (i div 2), subgoals (Thm.nprems_of goal)] ^ ":")] @ - pretty_goals_local ctxt Markup.subgoal + Display_Goal.pretty_goals ctxt Markup.subgoal (true, ! show_main_goal) (! Display.goals_limit) goal @ (map (fn msg => Position.setmp_thread_data pos msg ()) (rev messages)) | prt_goal NONE = []; @@ -368,7 +366,7 @@ fun pretty_goals main state = let val (ctxt, (_, goal)) = get_goal state - in pretty_goals_local ctxt Markup.none (false, main) (! Display.goals_limit) goal end; + in Display_Goal.pretty_goals ctxt Markup.none (false, main) (! Display.goals_limit) goal end; @@ -474,7 +472,8 @@ val ngoals = Thm.nprems_of goal; val _ = ngoals = 0 orelse error (Pretty.string_of (Pretty.chunks - (pretty_goals_local ctxt Markup.none (true, ! show_main_goal) (! Display.goals_limit) goal @ + (Display_Goal.pretty_goals ctxt Markup.none + (true, ! show_main_goal) (! Display.goals_limit) goal @ [Pretty.str (string_of_int ngoals ^ " unsolved goal(s)!")]))); val extra_hyps = Assumption.extra_hyps ctxt goal; diff -r 0ddf61f96b2a -r 8228f67bfe18 src/Pure/Isar/proof_display.ML --- a/src/Pure/Isar/proof_display.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/Pure/Isar/proof_display.ML Thu Jul 23 16:53:15 2009 +0200 @@ -35,7 +35,7 @@ let val thy = Thm.theory_of_thm th; val flags = {quote = true, show_hyps = false, show_status = true}; - in Display.pretty_thm_raw (Syntax.pp_global thy) flags [] th end; + in Display.pretty_thm_raw (Syntax.init_pretty_global thy) flags th end; val pp_typ = Pretty.quote oo Syntax.pretty_typ_global; val pp_term = Pretty.quote oo Syntax.pretty_term_global; diff -r 0ddf61f96b2a -r 8228f67bfe18 src/Pure/Proof/reconstruct.ML --- a/src/Pure/Proof/reconstruct.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/Pure/Proof/reconstruct.ML Thu Jul 23 16:53:15 2009 +0200 @@ -255,7 +255,7 @@ let fun search env [] = error ("Unsolvable constraints:\n" ^ Pretty.string_of (Pretty.chunks (map (fn (_, p, _) => - Display_Goal.pretty_flexpair (Syntax.pp_global thy) (pairself + Display_Goal.pretty_flexpair (Syntax.init_pretty_global thy) (pairself (Envir.norm_term bigenv) p)) cs))) | search env ((u, p as (t1, t2), vs)::ps) = if u then diff -r 0ddf61f96b2a -r 8228f67bfe18 src/Pure/ProofGeneral/proof_general_pgip.ML --- a/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/Pure/ProofGeneral/proof_general_pgip.ML Thu Jul 23 16:53:15 2009 +0200 @@ -655,11 +655,8 @@ text=[XML.Elem("pgml",[], maps YXML.parse_body strings)] }) - fun string_of_thm th = Pretty.string_of (Display.pretty_thm_raw - (Syntax.pp_global (Thm.theory_of_thm th)) - {quote = false, show_hyps = false, show_status = true} [] th) - - fun strings_of_thm (thy, name) = map string_of_thm (PureThy.get_thms thy name) + fun strings_of_thm (thy, name) = + map (Display.string_of_thm_global thy) (PureThy.get_thms thy name) val string_of_thy = Pretty.string_of o ProofDisplay.pretty_full_theory false in diff -r 0ddf61f96b2a -r 8228f67bfe18 src/Pure/display.ML --- a/src/Pure/display.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/Pure/display.ML Thu Jul 23 16:53:15 2009 +0200 @@ -16,8 +16,8 @@ signature DISPLAY = sig include BASIC_DISPLAY - val pretty_thm_raw: Pretty.pp -> {quote: bool, show_hyps: bool, show_status: bool} -> - term list -> thm -> Pretty.T + val pretty_thm_raw: Proof.context -> {quote: bool, show_hyps: bool, show_status: bool} -> + thm -> Pretty.T val pretty_thm_aux: Proof.context -> bool -> thm -> Pretty.T val pretty_thm: Proof.context -> thm -> Pretty.T val pretty_thm_global: theory -> thm -> Pretty.T @@ -68,7 +68,7 @@ else "" end; -fun pretty_thm_raw pp {quote, show_hyps = show_hyps', show_status} asms raw_th = +fun pretty_thm_raw ctxt {quote, show_hyps = show_hyps', show_status} raw_th = let val th = Thm.strip_shyps raw_th; val {hyps, tpairs, prop, ...} = Thm.rep_thm th; @@ -76,8 +76,9 @@ val tags = Thm.get_tags th; val q = if quote then Pretty.quote else I; - val prt_term = q o Pretty.term pp; + val prt_term = q o Syntax.pretty_term ctxt; + val asms = map Thm.term_of (Assumption.all_assms_of ctxt); val hyps' = if ! show_hyps then hyps else subtract (op aconv) asms hyps; val status = display_status show_status th; @@ -86,8 +87,8 @@ if hlen = 0 andalso status = "" then [] else if ! show_hyps orelse show_hyps' then [Pretty.brk 2, Pretty.list "[" "]" - (map (q o Display_Goal.pretty_flexpair pp) tpairs @ map prt_term hyps' @ - map (Pretty.sort pp) xshyps @ + (map (q o Display_Goal.pretty_flexpair ctxt) tpairs @ map prt_term hyps' @ + map (Syntax.pretty_sort ctxt) xshyps @ (if status = "" then [] else [Pretty.str status]))] else [Pretty.brk 2, Pretty.str ("[" ^ implode (replicate hlen ".") ^ status ^ "]")]; val tsymbs = @@ -95,18 +96,14 @@ else [Pretty.brk 1, pretty_tags tags]; in Pretty.block (prt_term prop :: (hsymbs @ tsymbs)) end; -fun pretty_thm_aux ctxt show_status th = - let - val flags = {quote = false, show_hyps = true, show_status = show_status}; - val asms = map Thm.term_of (Assumption.all_assms_of ctxt); - in pretty_thm_raw (Syntax.pp ctxt) flags asms th end; - +fun pretty_thm_aux ctxt show_status = + pretty_thm_raw ctxt {quote = false, show_hyps = true, show_status = show_status}; fun pretty_thm ctxt = pretty_thm_aux ctxt true; -fun pretty_thm_global thy th = - pretty_thm_raw (Syntax.pp_global thy) - {quote = false, show_hyps = false, show_status = true} [] th; +fun pretty_thm_global thy = + pretty_thm_raw (Syntax.init_pretty_global thy) + {quote = false, show_hyps = false, show_status = true}; fun pretty_thm_without_context th = pretty_thm_global (Thm.theory_of_thm th) th; diff -r 0ddf61f96b2a -r 8228f67bfe18 src/Pure/display_goal.ML --- a/src/Pure/display_goal.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/Pure/display_goal.ML Thu Jul 23 16:53:15 2009 +0200 @@ -9,10 +9,10 @@ sig val goals_limit: int ref val show_consts: bool ref - val pretty_flexpair: Pretty.pp -> term * term -> Pretty.T - val pretty_goals_aux: Pretty.pp -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list - val pretty_goals: int -> thm -> Pretty.T list - val print_goals: int -> thm -> unit + val pretty_flexpair: Proof.context -> term * term -> Pretty.T + val pretty_goals: Proof.context -> Markup.T -> bool * bool -> int -> thm -> Pretty.T list + val pretty_goals_without_context: int -> thm -> Pretty.T list + val print_goals_without_context: int -> thm -> unit end; structure Display_Goal: DISPLAY_GOAL = @@ -21,8 +21,8 @@ val goals_limit = ref 10; (*max number of goals to print*) val show_consts = ref false; (*true: show consts with types in proof state output*) -fun pretty_flexpair pp (t, u) = Pretty.block - [Pretty.term pp t, Pretty.str " =?=", Pretty.brk 1, Pretty.term pp u]; +fun pretty_flexpair ctxt (t, u) = Pretty.block + [Syntax.pretty_term ctxt t, Pretty.str " =?=", Pretty.brk 1, Syntax.pretty_term ctxt u]; (*print thm A1,...,An/B in "goal style" -- premises as numbered subgoals*) @@ -56,31 +56,35 @@ in -fun pretty_goals_aux pp markup (msg, main) maxgoals state = +fun pretty_goals ctxt markup (msg, main) maxgoals state = let + val prt_sort = Syntax.pretty_sort ctxt; + val prt_typ = Syntax.pretty_typ ctxt; + val prt_term = Syntax.pretty_term ctxt; + fun prt_atoms prt prtT (X, xs) = Pretty.block [Pretty.block (Pretty.commas (map prt xs)), Pretty.str " ::", Pretty.brk 1, prtT X]; - fun prt_var (x, ~1) = Pretty.term pp (Syntax.free x) - | prt_var xi = Pretty.term pp (Syntax.var xi); + fun prt_var (x, ~1) = prt_term (Syntax.free x) + | prt_var xi = prt_term (Syntax.var xi); - fun prt_varT (x, ~1) = Pretty.typ pp (TFree (x, [])) - | prt_varT xi = Pretty.typ pp (TVar (xi, [])); + fun prt_varT (x, ~1) = prt_typ (TFree (x, [])) + | prt_varT xi = prt_typ (TVar (xi, [])); - val prt_consts = prt_atoms (Pretty.term pp o Const) (Pretty.typ pp); - val prt_vars = prt_atoms prt_var (Pretty.typ pp); - val prt_varsT = prt_atoms prt_varT (Pretty.sort pp); + val prt_consts = prt_atoms (prt_term o Const) prt_typ; + val prt_vars = prt_atoms prt_var prt_typ; + val prt_varsT = prt_atoms prt_varT prt_sort; fun pretty_list _ _ [] = [] | pretty_list name prt lst = [Pretty.big_list name (map prt lst)]; fun pretty_subgoal (n, A) = Pretty.markup markup - [Pretty.str (" " ^ string_of_int n ^ ". "), Pretty.term pp A]; + [Pretty.str (" " ^ string_of_int n ^ ". "), prt_term A]; fun pretty_subgoals As = map pretty_subgoal (1 upto length As ~~ As); - val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair pp); + val pretty_ffpairs = pretty_list "flex-flex pairs:" (pretty_flexpair ctxt); val pretty_consts = pretty_list "constants:" prt_consts o consts_of; val pretty_vars = pretty_list "variables:" prt_vars o vars_of; @@ -92,7 +96,7 @@ val ngoals = length As; fun pretty_gs (types, sorts) = - (if main then [Pretty.term pp B] else []) @ + (if main then [prt_term B] else []) @ (if ngoals = 0 then [Pretty.str "No subgoals!"] else if ngoals > maxgoals then pretty_subgoals (Library.take (maxgoals, As)) @ @@ -110,10 +114,11 @@ (! show_types orelse ! show_sorts orelse ! show_all_types, ! show_sorts) end; -fun pretty_goals n th = - pretty_goals_aux (Syntax.pp_global (Thm.theory_of_thm th)) Markup.none (true, true) n th; +fun pretty_goals_without_context n th = + pretty_goals (Syntax.init_pretty_global (Thm.theory_of_thm th)) Markup.none (true, true) n th; -val print_goals = (Pretty.writeln o Pretty.chunks) oo pretty_goals; +val print_goals_without_context = + (Pretty.writeln o Pretty.chunks) oo pretty_goals_without_context; end; diff -r 0ddf61f96b2a -r 8228f67bfe18 src/Pure/goal.ML --- a/src/Pure/goal.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/Pure/goal.ML Thu Jul 23 16:53:15 2009 +0200 @@ -78,7 +78,7 @@ (case Thm.nprems_of th of 0 => conclude th | n => raise THM ("Proof failed.\n" ^ - Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals n th)) ^ + Pretty.string_of (Pretty.chunks (Display_Goal.pretty_goals_without_context n th)) ^ ("\n" ^ string_of_int n ^ " unsolved goal(s)!"), 0, [th])); diff -r 0ddf61f96b2a -r 8228f67bfe18 src/Pure/old_goals.ML --- a/src/Pure/old_goals.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/Pure/old_goals.ML Thu Jul 23 16:53:15 2009 +0200 @@ -135,7 +135,8 @@ (*Default action is to print an error message; could be suppressed for special applications.*) fun result_error_default state msg : thm = - Pretty.str "Bad final proof state:" :: Display_Goal.pretty_goals (!goals_limit) state @ + Pretty.str "Bad final proof state:" :: + Display_Goal.pretty_goals_without_context (!goals_limit) state @ [Pretty.str msg, Pretty.str "Proof failed!"] |> Pretty.chunks |> Pretty.string_of |> error; val result_error_fn = ref result_error_default; @@ -277,7 +278,7 @@ (if ngoals > 0 then " (" ^ string_of_int ngoals ^ " subgoal" ^ (if ngoals <> 1 then "s" else "") ^ ")" else ""))] @ - Display_Goal.pretty_goals m th + Display_Goal.pretty_goals_without_context m th end |> Pretty.chunks |> Pretty.writeln; (*Printing can raise exceptions, so the assignment occurs last. diff -r 0ddf61f96b2a -r 8228f67bfe18 src/Pure/tctical.ML --- a/src/Pure/tctical.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/Pure/tctical.ML Thu Jul 23 16:53:15 2009 +0200 @@ -191,12 +191,11 @@ (*** Tracing tactics ***) (*Print the current proof state and pass it on.*) -fun print_tac msg = - (fn st => - (tracing msg; - tracing ((Pretty.string_of o Pretty.chunks o - Display_Goal.pretty_goals (! Display_Goal.goals_limit)) st); - Seq.single st)); +fun print_tac msg st = + (tracing (msg ^ "\n" ^ + Pretty.string_of (Pretty.chunks + (Display_Goal.pretty_goals_without_context (! Display_Goal.goals_limit) st))); + Seq.single st); (*Pause until a line is typed -- if non-empty then fail. *) fun pause_tac st = @@ -232,10 +231,10 @@ (*Extract from a tactic, a thm->thm seq function that handles tracing*) fun tracify flag tac st = - if !flag andalso not (!suppress_tracing) - then (Display_Goal.print_goals (! Display_Goal.goals_limit) st; - tracing "** Press RETURN to continue:"; - exec_trace_command flag (tac,st)) + if !flag andalso not (!suppress_tracing) then + (Display_Goal.print_goals_without_context (! Display_Goal.goals_limit) st; + tracing "** Press RETURN to continue:"; + exec_trace_command flag (tac, st)) else tac st; (*Create a tactic whose outcome is given by seqf, handling TRACE_EXIT*) diff -r 0ddf61f96b2a -r 8228f67bfe18 src/Pure/type_infer.ML --- a/src/Pure/type_infer.ML Thu Jul 23 15:59:14 2009 +0200 +++ b/src/Pure/type_infer.ML Thu Jul 23 16:53:15 2009 +0200 @@ -40,7 +40,9 @@ fun param i (x, S) = TVar (("?" ^ x, i), S); val paramify_vars = - perhaps (Term_Subst.map_atypsT_option (fn TVar ((x, i), S) => SOME (param i (x, S)) | _ => NONE)); + Same.commit + (Term_Subst.map_atypsT_same + (fn TVar ((x, i), S) => (param i (x, S)) | _ => raise Same.SAME)); val paramify_dummies = let @@ -90,9 +92,10 @@ (* utils *) -fun deref tye (T as Param (i, S)) = (case Inttab.lookup tye i of - NONE => T - | SOME U => deref tye U) +fun deref tye (T as Param (i, S)) = + (case Inttab.lookup tye i of + NONE => T + | SOME U => deref tye U) | deref tye T = T; fun fold_pretyps f (PConst (_, T)) x = f T x @@ -194,32 +197,35 @@ (* add_parms *) -fun add_parmsT tye T = case deref tye T of +fun add_parmsT tye T = + (case deref tye T of PType (_, Ts) => fold (add_parmsT tye) Ts | Param (i, _) => insert (op =) i - | _ => I; + | _ => I); fun add_parms tye = fold_pretyps (add_parmsT tye); (* add_names *) -fun add_namesT tye T = case deref tye T of +fun add_namesT tye T = + (case deref tye T of PType (_, Ts) => fold (add_namesT tye) Ts | PTFree (x, _) => Name.declare x | PTVar ((x, _), _) => Name.declare x - | Param _ => I; + | Param _ => I); fun add_names tye = fold_pretyps (add_namesT tye); (* simple_typ/term_of *) -fun simple_typ_of tye f T = case deref tye T of +fun simple_typ_of tye f T = + (case deref tye T of PType (a, Ts) => Type (a, map (simple_typ_of tye f) Ts) | PTFree v => TFree v | PTVar v => TVar v - | Param (i, S) => TVar (f i, S); + | Param (i, S) => TVar (f i, S)); (*convert types, drop constraints*) fun simple_term_of tye f (PConst (c, T)) = Const (c, simple_typ_of tye f T) @@ -282,7 +288,8 @@ fun occurs_check tye i (Param (i', S)) = if i = i' then raise NO_UNIFIER ("Occurs check!", tye) - else (case Inttab.lookup tye i' of + else + (case Inttab.lookup tye i' of NONE => () | SOME T => occurs_check tye i T) | occurs_check tye i (PType (_, Ts)) = List.app (occurs_check tye i) Ts @@ -297,14 +304,15 @@ (* unification *) - fun unif (T1, T2) (tye_idx as (tye, idx)) = case (deref tye T1, deref tye T2) of + fun unif (T1, T2) (tye_idx as (tye, idx)) = + (case (deref tye T1, deref tye T2) of (Param (i, S), T) => assign i T S tye_idx | (T, Param (i, S)) => assign i T S tye_idx | (PType (a, Ts), PType (b, Us)) => if a <> b then raise NO_UNIFIER ("Clash of types " ^ quote a ^ " and " ^ quote b, tye) else fold unif (Ts ~~ Us) tye_idx - | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye); + | (T, U) => if T = U then tye_idx else raise NO_UNIFIER ("", tye)); in unif end; @@ -396,7 +404,7 @@ let val (T, tye_idx') = inf bs t tye_idx in (T, unif (T, U) tye_idx' - handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U) + handle NO_UNIFIER (msg, tye) => err_constraint msg tye bs t T U) end; in inf [] end;