# HG changeset patch # User wenzelm # Date 1138384995 -3600 # Node ID 95b4a51781aa94d2c715bf9557152a03b2e01f1c # Parent 838fb803636e6c16e64522793903158f519fca66 added invent_fixes; added debug flag, pprint_context; diff -r 838fb803636e -r 95b4a51781aa src/Pure/Isar/proof_context.ML --- a/src/Pure/Isar/proof_context.ML Fri Jan 27 19:03:14 2006 +0100 +++ b/src/Pure/Isar/proof_context.ML Fri Jan 27 19:03:15 2006 +0100 @@ -127,6 +127,7 @@ val add_fixes: (string * string option * mixfix) list -> context -> string list * context val add_fixes_i: (string * typ option * mixfix) list -> context -> string list * context val add_fixes_legacy: (string * typ option * mixfix) list -> context -> string list * context + val invent_fixes: string list -> context -> string list * context val fix_frees: term -> context -> context val auto_fixes: context * (term list list * 'a) -> context * (term list list * 'a) val bind_fixes: string list -> context -> (term -> term) * context @@ -157,6 +158,8 @@ val prems_limit: int ref val pretty_ctxt: context -> Pretty.T list val pretty_context: context -> Pretty.T list + val debug: bool ref + val pprint_context: context -> pprint_args -> unit end; structure ProofContext: PROOF_CONTEXT = @@ -1110,7 +1113,7 @@ fun no_dups _ [] = () | no_dups ctxt dups = error ("Duplicate variable(s): " ^ commas_quote dups); -fun gen_fixes prep raw_vars ctxt = +fun gen_fixes prep invent raw_vars ctxt = let val (ys, zs) = split_list (fixes_of ctxt); val (vars, ctxt') = prep raw_vars ctxt; @@ -1118,6 +1121,7 @@ val _ = no_dups ctxt (duplicates xs); val xs' = if is_body ctxt then Term.variantlist (map Syntax.skolem xs, zs) + else if invent then Term.variantlist (xs, zs) else (no_dups ctxt (xs inter_string ys); no_dups ctxt (xs inter_string zs); xs); val vars' = map2 (fn x' => fn (_, T, mx) => (x', T, mx)) xs' vars; in @@ -1130,9 +1134,10 @@ in -val add_fixes = gen_fixes read_vars; -val add_fixes_i = gen_fixes cert_vars; -val add_fixes_legacy = gen_fixes cert_vars_legacy; +val add_fixes = gen_fixes read_vars false; +val add_fixes_i = gen_fixes cert_vars false; +val add_fixes_legacy = gen_fixes cert_vars_legacy false; +fun invent_fixes xs = gen_fixes cert_vars true (map (fn x => (x, NONE, NoSyn)) xs); end; @@ -1144,7 +1149,13 @@ fun add (Free (x, T)) = if is_fixed ctxt x then I else insert (op =) (x, SOME T, NoSyn) | add _ = I; val fixes = rev (fold_aterms add t []); - in ctxt |> set_body false |> add_fixes_i fixes |> snd |> restore_body ctxt end; + in + ctxt + |> declare_term t + |> set_body false + |> (snd o add_fixes_i fixes) + |> restore_body ctxt + end; fun auto_fixes (arg as (ctxt, (propss, x))) = if is_body ctxt then arg @@ -1189,8 +1200,10 @@ val new_asms = List.concat (map #1 results); val new_prems = map #2 results; - val ctxt3 = ctxt2 |> map_assms (fn (asms, prems) => (asms @ [(new_asms, exp)], prems @ new_prems)) - val ctxt4 = ctxt3 |> put_thms ("prems", SOME (prems_of ctxt3)); + val ctxt3 = ctxt2 + |> map_assms (fn (asms, prems) => (asms @ [(new_asms, exp)], prems @ new_prems)) + val ctxt4 = ctxt3 + |> put_thms ("prems", SOME (prems_of ctxt3)); in (map #3 results, warn_extra_tfrees ctxt ctxt4) end; in @@ -1495,7 +1508,16 @@ verb pretty_cases (K ctxt) @ verb single (fn () => Pretty.big_list "type constraints:" (map prt_defT (Vartab.dest types))) @ verb single (fn () => Pretty.big_list "default sorts:" (map prt_defS (Vartab.dest sorts))) @ - verb single (fn () => Pretty.strs ("used type variable names:" :: used)) + verb single (fn () => Pretty.strs ("used type variable names:" :: rev used)) end; + +(* toplevel pretty printing *) + +val debug = ref false; + +fun pprint_context ctxt = Pretty.pprint + (if ! debug then Pretty.quote (Pretty.big_list "proof context:" (pretty_context ctxt)) + else Pretty.str ""); + end;