--- a/NEWS Mon Oct 08 22:06:32 2007 +0200
+++ b/NEWS Tue Oct 09 00:20:13 2007 +0200
@@ -1307,6 +1307,13 @@
(Syntax.read_term etc.). These supersede former Sign.read_term etc.
which are considered legacy and await removal.
+* Pure/Syntax: generic interfaces for type unchecking
+(Syntax.uncheck_terms etc.) and unparsing (Syntax.unparse_term etc.),
+with common combinations (Syntax.pretty_term, Syntax.string_of_term
+etc.). Former Sign.pretty_term, Sign.string_of_term etc. are still
+available for convenience, but refer to the very same operations
+(using a mere theory instead of a full context).
+
* Isar: simplified treatment of user-level errors, using exception
ERROR of string uniformly. Function error now merely raises ERROR,
without any side effect on output channels. The Isar toplevel takes
--- a/doc-src/antiquote_setup.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/doc-src/antiquote_setup.ML Tue Oct 09 00:20:13 2007 +0200
@@ -76,7 +76,7 @@
#> space_implode "\\par\\smallskip%\n"
#> enclose "\\isa{" "}");
-fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
+fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
fun pretty_thm ctxt = pretty_term ctxt o Thm.full_prop_of;
in
--- a/src/HOL/Algebra/ringsimp.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Algebra/ringsimp.ML Tue Oct 09 00:20:13 2007 +0200
@@ -34,7 +34,7 @@
fun print_structures ctxt =
let
val structs = Data.get (Context.Proof ctxt);
- val pretty_term = Pretty.quote o ProofContext.pretty_term ctxt;
+ val pretty_term = Pretty.quote o Syntax.pretty_term ctxt;
fun pretty_struct ((s, ts), _) = Pretty.block
[Pretty.str s, Pretty.str ":", Pretty.brk 1,
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
--- a/src/HOL/Library/Eval.thy Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Library/Eval.thy Tue Oct 09 00:20:13 2007 +0200
@@ -190,9 +190,9 @@
of SOME t' => t'
| NONE => evl thy t;
val ty' = Term.type_of t';
- val p = Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'),
+ val p = Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'),
Pretty.fbrk, Pretty.str "::", Pretty.brk 1,
- Pretty.quote (ProofContext.pretty_typ ctxt ty')];
+ Pretty.quote (Syntax.pretty_typ ctxt ty')];
in Pretty.writeln p end;
val evaluate = gen_evaluate (map snd evaluators);
--- a/src/HOL/Nominal/nominal_induct.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Nominal/nominal_induct.ML Tue Oct 09 00:20:13 2007 +0200
@@ -134,7 +134,7 @@
inst >> Option.map (pair NONE);
val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (ctxt, t) =>
- error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of ctxt) t));
+ error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of ctxt) t));
fun unless_more_args scan = Scan.unless (Scan.lift
((Args.$$$ avoidingN || Args.$$$ fixingN || Args.$$$ ruleN) -- Args.colon)) scan;
--- a/src/HOL/Orderings.thy Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Orderings.thy Tue Oct 09 00:20:13 2007 +0200
@@ -275,9 +275,9 @@
let
val structs = Data.get (Context.Proof ctxt);
fun pretty_term t = Pretty.block
- [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.brk 1,
+ [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.brk 1,
Pretty.str "::", Pretty.brk 1,
- Pretty.quote (ProofContext.pretty_typ ctxt (type_of t))];
+ Pretty.quote (Syntax.pretty_typ ctxt (type_of t))];
fun pretty_struct ((s, ts), _) = Pretty.block
[Pretty.str s, Pretty.str ":", Pretty.brk 1,
Pretty.enclose "(" ")" (Pretty.breaks (map pretty_term ts))];
--- a/src/HOL/Tools/datatype_case.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/datatype_case.ML Tue Oct 09 00:20:13 2007 +0200
@@ -247,7 +247,7 @@
in (pat_rect1, tree)
end)
| SOME (t, i) => raise CASE_ERROR ("Not a datatype constructor: " ^
- ProofContext.string_of_term ctxt t, i)
+ Syntax.string_of_term ctxt t, i)
end
| mk _ = raise CASE_ERROR ("Malformed row matrix", ~1)
in mk
@@ -260,13 +260,13 @@
(fn x as Free (s, _) => (fn xs =>
if member op aconv xs x then
case_error (quote s ^ " occurs repeatedly in the pattern " ^
- quote (ProofContext.string_of_term ctxt pat))
+ quote (Syntax.string_of_term ctxt pat))
else x :: xs)
| _ => I) pat [];
fun gen_make_case ty_match ty_inst type_of tab ctxt err used x clauses =
let
- fun string_of_clause (pat, rhs) = ProofContext.string_of_term ctxt
+ fun string_of_clause (pat, rhs) = Syntax.string_of_term ctxt
(Syntax.const "_case1" $ pat $ rhs);
val _ = map (no_repeat_vars ctxt o fst) clauses;
val rows = map_index (fn (i, (pat, rhs)) =>
@@ -333,8 +333,7 @@
in
(t' $ u', used'')
end
- | prep_pat t used = case_error ("Bad pattern: " ^
- ProofContext.string_of_term ctxt t);
+ | prep_pat t used = case_error ("Bad pattern: " ^ Syntax.string_of_term ctxt t);
fun dest_case1 (t as Const ("_case1", _) $ l $ r) =
let val (l', cnstrts) = strip_constraints l
in ((fst (prep_pat l' (add_term_free_names (t, []))), r), cnstrts)
--- a/src/HOL/Tools/function_package/fundef_common.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_common.ML Tue Oct 09 00:20:13 2007 +0200
@@ -175,7 +175,7 @@
fun split_def ctxt geq =
let
- fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
+ fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
val (qs, imp) = open_all_all geq
val gs = Logic.strip_imp_prems imp
@@ -214,7 +214,7 @@
fun check geq =
let
- fun input_error msg = cat_lines [msg, ProofContext.string_of_term ctxt geq]
+ fun input_error msg = cat_lines [msg, Syntax.string_of_term ctxt geq]
val fqgar as (fname, qs, gs, args, rhs) = split_def ctxt geq
--- a/src/HOL/Tools/function_package/fundef_datatype.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/function_package/fundef_datatype.ML Tue Oct 09 00:20:13 2007 +0200
@@ -25,7 +25,7 @@
let
fun err str = error (cat_lines ["Malformed definition:",
str ^ " not allowed in sequential mode.",
- ProofContext.string_of_term ctxt geq])
+ Syntax.string_of_term ctxt geq])
val thy = ProofContext.theory_of ctxt
fun check_constr_pattern (Bound _) = ()
@@ -235,7 +235,7 @@
fun warn_if_redundant ctxt origs tss =
let
- fun msg t = "Ignoring redundant equation: " ^ quote (ProofContext.string_of_term ctxt t)
+ fun msg t = "Ignoring redundant equation: " ^ quote (Syntax.string_of_term ctxt t)
val (tss', _) = chop (length origs) tss
fun check ((_, t), []) = (Output.warning (msg t); [])
--- a/src/HOL/Tools/function_package/lexicographic_order.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/function_package/lexicographic_order.ML Tue Oct 09 00:20:13 2007 +0200
@@ -252,7 +252,7 @@
fun no_order_msg ctxt table tl measure_funs =
let
- val prterm = ProofContext.string_of_term ctxt
+ val prterm = Syntax.string_of_term ctxt
fun pr_fun t i = string_of_int i ^ ") " ^ prterm t
fun pr_goal t i =
@@ -292,7 +292,7 @@
val clean_table = map (fn x => map (nth x) order) table
val relation = mk_measures domT (map (nth measure_funs) order)
- val _ = writeln ("Found termination order: " ^ quote (ProofContext.string_of_term ctxt relation))
+ val _ = writeln ("Found termination order: " ^ quote (Syntax.string_of_term ctxt relation))
in (* 4: proof reconstruction *)
st |> (PRIMITIVE (cterm_instantiate [(cterm_of thy rel, cterm_of thy relation)])
--- a/src/HOL/Tools/inductive_package.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/inductive_package.ML Tue Oct 09 00:20:13 2007 +0200
@@ -247,11 +247,11 @@
fun err_in_rule ctxt name t msg =
error (cat_lines ["Ill-formed introduction rule " ^ quote name,
- ProofContext.string_of_term ctxt t, msg]);
+ Syntax.string_of_term ctxt t, msg]);
fun err_in_prem ctxt name t p msg =
- error (cat_lines ["Ill-formed premise", ProofContext.string_of_term ctxt p,
- "in introduction rule " ^ quote name, ProofContext.string_of_term ctxt t, msg]);
+ error (cat_lines ["Ill-formed premise", Syntax.string_of_term ctxt p,
+ "in introduction rule " ^ quote name, Syntax.string_of_term ctxt t, msg]);
val bad_concl = "Conclusion of introduction rule must be an inductive predicate";
@@ -275,7 +275,7 @@
fun check_ind err t = case dest_predicate cs params t of
NONE => err (bad_app ^
- commas (map (ProofContext.string_of_term ctxt) params))
+ commas (map (Syntax.string_of_term ctxt) params))
| SOME (_, _, ys, _) =>
if exists (fn c => exists (fn t => Logic.occs (c, t)) ys) cs
then err bad_ind_occ else ();
@@ -431,7 +431,7 @@
fun err msg =
error (Pretty.string_of (Pretty.block
- [Pretty.str msg, Pretty.fbrk, ProofContext.pretty_term ctxt prop]));
+ [Pretty.str msg, Pretty.fbrk, Syntax.pretty_term ctxt prop]));
val elims = Induct.find_casesP ctxt prop;
--- a/src/HOL/Tools/lin_arith.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/lin_arith.ML Tue Oct 09 00:20:13 2007 +0200
@@ -656,7 +656,7 @@
(* implemented above, or 'is_split_thm' should be modified to filter it *)
(* out *)
| (t, ts) => (
- warning ("Lin. Arith.: split rule for " ^ ProofContext.string_of_term ctxt t ^
+ warning ("Lin. Arith.: split rule for " ^ Syntax.string_of_term ctxt t ^
" (with " ^ string_of_int (length ts) ^
" argument(s)) not implemented; proof reconstruction is likely to fail");
NONE
--- a/src/HOL/Tools/metis_tools.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/metis_tools.ML Tue Oct 09 00:20:13 2007 +0200
@@ -215,9 +215,9 @@
else error ("Constant " ^ c ^ " expects " ^ Int.toString ntyargs ^
" but gets " ^ Int.toString (length tys) ^
" type arguments\n" ^
- space_implode "\n" (map (ProofContext.string_of_typ ctxt) tys) ^
+ space_implode "\n" (map (Syntax.string_of_typ ctxt) tys) ^
" the terms are \n" ^
- space_implode "\n" (map (ProofContext.string_of_term ctxt) (terms_of tts)))
+ space_implode "\n" (map (Syntax.string_of_term ctxt) (terms_of tts)))
end
| NONE => (*Not a constant. Is it a type constructor?*)
case Recon.strip_prefix ResClause.tconst_prefix a of
@@ -236,11 +236,11 @@
fun fol_terms_to_hol ctxt fol_tms =
let val ts = map (fol_term_to_hol_RAW ctxt) fol_tms
val _ = Output.debug (fn () => " calling type inference:")
- val _ = app (fn t => Output.debug (fn () => ProofContext.string_of_term ctxt t)) ts
+ val _ = app (fn t => Output.debug (fn () => Syntax.string_of_term ctxt t)) ts
val ts' = infer_types ctxt ts;
val _ = app (fn t => Output.debug
- (fn () => " final term: " ^ ProofContext.string_of_term ctxt t ^
- " of type " ^ ProofContext.string_of_typ ctxt (type_of t)))
+ (fn () => " final term: " ^ Syntax.string_of_term ctxt t ^
+ " of type " ^ Syntax.string_of_typ ctxt (type_of t)))
ts'
in ts' end;
@@ -338,7 +338,7 @@
else
let
val i_atm = singleton (fol_terms_to_hol ctxt) (Metis.Term.Fn atm)
- val _ = Output.debug (fn () => " atom: " ^ ProofContext.string_of_term ctxt i_atm)
+ val _ = Output.debug (fn () => " atom: " ^ Syntax.string_of_term ctxt i_atm)
val prems_th1 = prems_of i_th1
val prems_th2 = prems_of i_th2
val index_th1 = get_index (mk_not i_atm) prems_th1
@@ -373,10 +373,11 @@
val adjustment = get_ty_arg_size thy tm1
val p' = if adjustment > p then p else p-adjustment
val tm_p = List.nth(args,p')
- handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^ Int.toString adjustment ^ " term " ^ ProofContext.string_of_term ctxt tm)
+ handle Subscript => error ("equality_inf: " ^ Int.toString p ^ " adj " ^
+ Int.toString adjustment ^ " term " ^ Syntax.string_of_term ctxt tm)
in
Output.debug (fn () => "path_finder: " ^ Int.toString p ^
- " " ^ ProofContext.string_of_term ctxt tm_p);
+ " " ^ Syntax.string_of_term ctxt tm_p);
if null ps (*FIXME: why not use pattern-matching and avoid repetition*)
then (tm_p, list_comb (tm1, replace_item_list (Term.Bound 0) p' args))
else let val (r,t) = path_finder_FO tm_p ps
@@ -398,9 +399,9 @@
| path_finder_lit tm_a idx = path_finder isFO tm_a idx
val (tm_subst, body) = path_finder_lit i_atm fp
val tm_abs = Term.Abs("x", Term.type_of tm_subst, body)
- val _ = Output.debug (fn () => "abstraction: " ^ ProofContext.string_of_term ctxt tm_abs)
- val _ = Output.debug (fn () => "i_tm: " ^ ProofContext.string_of_term ctxt i_tm)
- val _ = Output.debug (fn () => "located term: " ^ ProofContext.string_of_term ctxt tm_subst)
+ val _ = Output.debug (fn () => "abstraction: " ^ Syntax.string_of_term ctxt tm_abs)
+ val _ = Output.debug (fn () => "i_tm: " ^ Syntax.string_of_term ctxt i_tm)
+ val _ = Output.debug (fn () => "located term: " ^ Syntax.string_of_term ctxt tm_subst)
val imax = maxidx_of_term (i_tm $ tm_abs $ tm_subst) (*ill typed but gives right max*)
val subst' = incr_indexes (imax+1) (if pos then subst_em else ssubst_em)
val _ = Output.debug (fn () => "subst' " ^ string_of_thm subst')
--- a/src/HOL/Tools/res_atp.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/res_atp.ML Tue Oct 09 00:20:13 2007 +0200
@@ -960,8 +960,7 @@
val thy = ProofContext.theory_of ctxt;
in
Output.debug (fn () => "subgoals in isar_atp:\n" ^
- Pretty.string_of (ProofContext.pretty_term ctxt
- (Logic.mk_conjunction_list (Thm.prems_of goal))));
+ Syntax.string_of_term ctxt (Logic.mk_conjunction_list (Thm.prems_of goal)));
Output.debug (fn () => "current theory: " ^ Context.theory_name thy);
app (fn th => Output.debug (fn _ => "chained: " ^ string_of_thm th)) chain_ths;
if !time_limit > 0 then isar_atp (ctxt, chain_ths, goal)
--- a/src/HOL/Tools/res_reconstruct.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/res_reconstruct.ML Tue Oct 09 00:20:13 2007 +0200
@@ -352,7 +352,7 @@
(*ctms is a list of conjecture clauses as yielded by Isabelle. Those returned by the
ATP may have their literals reordered.*)
fun isar_lines ctxt ctms =
- let val string_of = ProofContext.string_of_term ctxt
+ let val string_of = Syntax.string_of_term ctxt
fun doline have (lname, t, []) = (*No deps: it's a conjecture clause, with no proof.*)
(case permuted_clause t ctms of
SOME u => "assume " ^ lname ^ ": \"" ^ string_of u ^ "\"\n"
--- a/src/HOL/Tools/typedef_package.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOL/Tools/typedef_package.ML Tue Oct 09 00:20:13 2007 +0200
@@ -108,7 +108,7 @@
val rhs_tfrees = Term.add_tfrees set [];
val rhs_tfreesT = Term.add_tfreesT setT [];
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT));
+ error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
fun mk_nonempty A =
HOLogic.mk_Trueprop (HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A)));
val goal = mk_nonempty set;
@@ -232,7 +232,7 @@
fun gen_typedef prep_term def opt_name typ set opt_morphs tac thy =
let
- val string_of_term = ProofContext.string_of_term (ProofContext.init thy);
+ val string_of_term = Sign.string_of_term thy;
val name = the_default (#1 typ) opt_name;
val (set, goal, _, typedef_result) =
prepare_typedef prep_term def name typ set opt_morphs thy;
--- a/src/HOLCF/Tools/pcpodef_package.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/HOLCF/Tools/pcpodef_package.ML Tue Oct 09 00:20:13 2007 +0200
@@ -67,7 +67,7 @@
val setT = Term.fastype_of set;
val rhs_tfrees = term_tfrees set;
val oldT = HOLogic.dest_setT setT handle TYPE _ =>
- error ("Not a set type: " ^ quote (ProofContext.string_of_typ ctxt setT));
+ error ("Not a set type: " ^ quote (Syntax.string_of_typ ctxt setT));
fun mk_nonempty A =
HOLogic.mk_exists ("x", oldT, HOLogic.mk_mem (Free ("x", oldT), A));
fun mk_admissible A =
--- a/src/Provers/Arith/fast_lin_arith.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Provers/Arith/fast_lin_arith.ML Tue Oct 09 00:20:13 2007 +0200
@@ -416,7 +416,7 @@
(if !trace then (tracing msg; tracing (Display.string_of_thm th)) else (); th);
fun trace_term ctxt msg t =
- (if !trace then tracing (cat_lines [msg, ProofContext.string_of_term ctxt t]) else (); t)
+ (if !trace then tracing (cat_lines [msg, Syntax.string_of_term ctxt t]) else (); t)
fun trace_msg msg =
if !trace then tracing msg else ();
@@ -562,7 +562,7 @@
| (v, lineqs) :: hist' =>
let
val frees = map Free params
- fun show_term t = ProofContext.string_of_term ctxt (subst_bounds (frees, t))
+ fun show_term t = Syntax.string_of_term ctxt (subst_bounds (frees, t))
val start =
if v = ~1 then (hist', findex0 discr n lineqs)
else (hist, replicate n Rat.zero)
--- a/src/Pure/Isar/args.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/args.ML Tue Oct 09 00:20:13 2007 +0200
@@ -170,8 +170,8 @@
let
val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
fun prt (Arg (_, Value (SOME (Text s)))) = Pretty.str (quote s)
- | prt (Arg (_, Value (SOME (Typ T)))) = ProofContext.pretty_typ ctxt T
- | prt (Arg (_, Value (SOME (Term t)))) = ProofContext.pretty_term ctxt t
+ | prt (Arg (_, Value (SOME (Typ T)))) = Syntax.pretty_typ ctxt T
+ | prt (Arg (_, Value (SOME (Term t)))) = Syntax.pretty_term ctxt t
| prt (Arg (_, Value (SOME (Fact ths)))) =
Pretty.enclose "(" ")" (Pretty.breaks (map prt_thm ths))
| prt arg = Pretty.str (string_of arg);
--- a/src/Pure/Isar/class.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/class.ML Tue Oct 09 00:20:13 2007 +0200
@@ -413,6 +413,8 @@
fun print_classes thy =
let
+ val ctxt = ProofContext.init thy;
+
val algebra = Sign.classes_of thy;
val arities =
Symtab.empty
@@ -423,13 +425,13 @@
fun mk_arity class tyco =
let
val Ss = Sorts.mg_domain algebra tyco [class];
- in Sign.pretty_arity thy (tyco, Ss, [class]) end;
+ in Syntax.pretty_arity ctxt (tyco, Ss, [class]) end;
fun mk_param (c, ty) = Pretty.str (Sign.extern_const thy c ^ " :: "
- ^ setmp show_sorts false (Sign.string_of_typ thy o Type.strip_sorts) ty);
+ ^ setmp show_sorts false (Syntax.string_of_typ ctxt o Type.strip_sorts) ty);
fun mk_entry class = (Pretty.block o Pretty.fbreaks o map_filter I) [
(SOME o Pretty.str) ("class " ^ class ^ ":"),
(SOME o Pretty.block) [Pretty.str "supersort: ",
- (Sign.pretty_sort thy o Sign.minimize_sort thy o Sign.super_classes thy) class],
+ (Syntax.pretty_sort ctxt o Sign.minimize_sort thy o Sign.super_classes thy) class],
Option.map (Pretty.str o prefix "locale: " o #locale) (lookup_class_data thy class),
((fn [] => NONE | ps => (SOME o Pretty.block o Pretty.fbreaks) (Pretty.str "parameters:" :: ps)) o map mk_param
o these o Option.map #params o try (AxClass.get_definition thy)) class,
--- a/src/Pure/Isar/element.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/element.ML Tue Oct 09 00:20:13 2007 +0200
@@ -164,8 +164,8 @@
fun pretty_stmt ctxt =
let
- val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
- val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
+ val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
+ val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
val prt_terms = separate (Pretty.keyword "and") o map prt_term;
val prt_name_atts = pretty_name_atts ctxt;
@@ -189,8 +189,8 @@
fun pretty_ctxt ctxt =
let
- val prt_typ = Pretty.quote o ProofContext.pretty_typ ctxt;
- val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
+ val prt_typ = Pretty.quote o Syntax.pretty_typ ctxt;
+ val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
val prt_thm = Pretty.backquote o ProofContext.pretty_thm ctxt;
val prt_name_atts = pretty_name_atts ctxt;
@@ -310,7 +310,7 @@
(CONJUNCTS (TRYALL (Tactic.rtac Drule.protectI)))))))), Position.none));
fun pretty_witness ctxt witn =
- let val prt_term = Pretty.quote o ProofContext.pretty_term ctxt in
+ let val prt_term = Pretty.quote o Syntax.pretty_term ctxt in
Pretty.block (prt_term (witness_prop witn) ::
(if ! show_hyps then [Pretty.brk 2, Pretty.list "[" "]"
(map prt_term (witness_hyps witn))] else []))
--- a/src/Pure/Isar/find_theorems.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/find_theorems.ML Tue Oct 09 00:20:13 2007 +0200
@@ -40,9 +40,9 @@
| Elim => Pretty.str (prfx "elim")
| Dest => Pretty.str (prfx "dest")
| Simp pat => Pretty.block [Pretty.str (prfx "simp:"), Pretty.brk 1,
- Pretty.quote (ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat))]
+ Pretty.quote (Syntax.pretty_term ctxt (Term.show_dummy_patterns pat))]
| Pattern pat => Pretty.enclose (prfx " \"") "\""
- [ProofContext.pretty_term ctxt (Term.show_dummy_patterns pat)])
+ [Syntax.pretty_term ctxt (Term.show_dummy_patterns pat)])
end;
--- a/src/Pure/Isar/isar_cmd.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Tue Oct 09 00:20:13 2007 +0200
@@ -562,7 +562,7 @@
let
val ctxt = Proof.context_of state;
val prop = Syntax.read_prop ctxt s;
- in Pretty.string_of (Pretty.quote (ProofContext.pretty_term ctxt prop)) end;
+ in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt prop)) end;
fun string_of_term state s =
let
@@ -571,15 +571,15 @@
val T = Term.type_of t;
in
Pretty.string_of
- (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
+ (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
end;
fun string_of_type state s =
let
val ctxt = Proof.context_of state;
val T = ProofContext.read_typ ctxt s;
- in Pretty.string_of (Pretty.quote (ProofContext.pretty_typ ctxt T)) end;
+ in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
PrintMode.with_modes modes (fn () =>
--- a/src/Pure/Isar/locale.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/locale.ML Tue Oct 09 00:20:13 2007 +0200
@@ -472,7 +472,7 @@
fun print_registrations show_wits loc ctxt =
let
val thy = ProofContext.theory_of ctxt;
- val prt_term = Pretty.quote o ProofContext.pretty_term ctxt;
+ val prt_term = Pretty.quote o Syntax.pretty_term ctxt;
val prt_thm = prt_term o prop_of;
fun prt_inst ts =
Pretty.enclose "(" ")" (Pretty.breaks (map prt_term ts));
@@ -1545,7 +1545,7 @@
| SOME (_, _, eqns') => Termtab.join (fn t => fn (_, e) => e) (eqns, eqns')
handle Termtab.DUP t =>
error ("Conflicting interpreting equations for term " ^
- quote (ProofContext.string_of_term ctxt t))
+ quote (Syntax.string_of_term ctxt t))
in ((id', eqns'), eqns') end;
--- a/src/Pure/Isar/obtain.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/obtain.ML Tue Oct 09 00:20:13 2007 +0200
@@ -71,7 +71,7 @@
if member (op =) vs v then insert (op aconv) t else I | _ => I) tm [];
val _ = null bads orelse
error ("Result contains obtained parameters: " ^
- space_implode " " (map (ProofContext.string_of_term ctxt) bads));
+ space_implode " " (map (Syntax.string_of_term ctxt) bads));
in tm end;
fun eliminate fix_ctxt rule xs As thm =
@@ -217,8 +217,8 @@
val thy = ProofContext.theory_of ctxt;
val certT = Thm.ctyp_of thy;
val cert = Thm.cterm_of thy;
- val string_of_typ = ProofContext.string_of_typ ctxt;
- val string_of_term = setmp show_types true (ProofContext.string_of_term ctxt);
+ val string_of_typ = Syntax.string_of_typ ctxt;
+ val string_of_term = setmp show_types true (Syntax.string_of_term ctxt);
fun err msg th = error (msg ^ ":\n" ^ ProofContext.string_of_thm ctxt th);
--- a/src/Pure/Isar/proof.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/proof.ML Tue Oct 09 00:20:13 2007 +0200
@@ -465,7 +465,7 @@
let
val thy = theory_of state;
val ctxt = context_of state;
- val string_of_term = ProofContext.string_of_term ctxt;
+ val string_of_term = Syntax.string_of_term ctxt;
val string_of_thm = ProofContext.string_of_thm ctxt;
val ngoals = Thm.nprems_of goal;
--- a/src/Pure/Isar/proof_display.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/proof_display.ML Tue Oct 09 00:20:13 2007 +0200
@@ -43,8 +43,8 @@
fun pprint pretty thy = Pretty.pprint o Pretty.quote o pretty (ProofContext.init thy);
-val pprint_typ = pprint ProofContext.pretty_typ;
-val pprint_term = pprint ProofContext.pretty_term;
+val pprint_typ = pprint Syntax.pretty_typ;
+val pprint_term = pprint Syntax.pretty_term;
fun pprint_ctyp cT = pprint_typ (Thm.theory_of_ctyp cT) (Thm.typ_of cT);
fun pprint_cterm ct = pprint_term (Thm.theory_of_cterm ct) (Thm.term_of ct);
val pprint_thm = Pretty.pprint o ProofContext.pretty_thm_legacy;
@@ -136,7 +136,7 @@
fun pretty_var ctxt (x, T) =
Pretty.block [Pretty.str x, Pretty.str " ::", Pretty.brk 1,
- Pretty.quote (ProofContext.pretty_typ ctxt T)];
+ Pretty.quote (Syntax.pretty_typ ctxt T)];
fun pretty_vars ctxt kind vs = Pretty.big_list kind (map (pretty_var ctxt) vs);
--- a/src/Pure/Isar/toplevel.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Isar/toplevel.ML Tue Oct 09 00:20:13 2007 +0200
@@ -273,10 +273,10 @@
raised "AST" (msg :: map (Pretty.string_of o Syntax.pretty_ast) asts)
| exn_msg false (TYPE (msg, _, _)) = raised "TYPE" [msg]
| exn_msg true (TYPE (msg, Ts, ts)) = raised "TYPE" (msg ::
- with_context ProofContext.string_of_typ Ts @ with_context ProofContext.string_of_term ts)
+ with_context Syntax.string_of_typ Ts @ with_context Syntax.string_of_term ts)
| exn_msg false (TERM (msg, _)) = raised "TERM" [msg]
| exn_msg true (TERM (msg, ts)) =
- raised "TERM" (msg :: with_context ProofContext.string_of_term ts)
+ raised "TERM" (msg :: with_context Syntax.string_of_term ts)
| exn_msg false (THM (msg, _, _)) = raised "THM" [msg]
| exn_msg true (THM (msg, i, thms)) =
raised ("THM " ^ string_of_int i) (msg :: with_context ProofContext.string_of_thm thms)
--- a/src/Pure/Thy/term_style.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Thy/term_style.ML Tue Oct 09 00:20:13 2007 +0200
@@ -55,14 +55,14 @@
(Logic.strip_imp_concl t)
in
case concl of (_ $ l $ r) => (l, r)
- | _ => error ("Binary operator expected in term: " ^ ProofContext.string_of_term ctxt concl)
+ | _ => error ("Binary operator expected in term: " ^ Syntax.string_of_term ctxt concl)
end;
fun style_parm_premise i ctxt t =
let val prems = Logic.strip_imp_prems t in
if i <= length prems then nth prems (i - 1)
else error ("Not enough premises for prem" ^ string_of_int i ^
- " in propositon: " ^ ProofContext.string_of_term ctxt t)
+ " in propositon: " ^ Syntax.string_of_term ctxt t)
end;
val _ = Context.add_setup
--- a/src/Pure/Thy/thy_output.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/Thy/thy_output.ML Tue Oct 09 00:20:13 2007 +0200
@@ -429,22 +429,23 @@
val pretty_text = Pretty.chunks o map Pretty.str o map tweak_line o Library.split_lines;
-fun pretty_term ctxt = ProofContext.pretty_term ctxt o ProofContext.revert_skolems ctxt;
+fun pretty_term ctxt = Syntax.pretty_term ctxt o ProofContext.revert_skolems ctxt;
+
fun pretty_term_abbrev ctxt =
ProofContext.pretty_term_abbrev ctxt o ProofContext.revert_skolems ctxt;
fun pretty_term_typ ctxt t =
- ProofContext.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
+ Syntax.pretty_term ctxt (TypeInfer.constrain (Term.fastype_of t) t);
-fun pretty_term_typeof ctxt = ProofContext.pretty_typ ctxt o Term.fastype_of;
+fun pretty_term_typeof ctxt = Syntax.pretty_typ ctxt o Term.fastype_of;
fun pretty_term_const ctxt t =
if Term.is_Const t then pretty_term ctxt t
- else error ("Logical constant expected: " ^ ProofContext.string_of_term ctxt t);
+ else error ("Logical constant expected: " ^ Syntax.string_of_term ctxt t);
fun pretty_abbrev ctxt t =
let
- fun err () = error ("Abbreviated constant expected: " ^ ProofContext.string_of_term ctxt t);
+ fun err () = error ("Abbreviated constant expected: " ^ Syntax.string_of_term ctxt t);
val (head, args) = Term.strip_comb t;
val (c, T) = Term.dest_Const head handle TERM _ => err ();
val (U, (u, _)) = Consts.the_abbreviation (ProofContext.consts_of ctxt) c
@@ -519,7 +520,7 @@
("typeof", args Args.term (output pretty_term_typeof)),
("const", args Args.term (output pretty_term_const)),
("abbrev", args Args.term_abbrev (output pretty_abbrev)),
- ("typ", args Args.typ_abbrev (output ProofContext.pretty_typ)),
+ ("typ", args Args.typ_abbrev (output Syntax.pretty_typ)),
("text", args (Scan.lift Args.name) (output (K pretty_text))),
("goals", output_goals true),
("subgoals", output_goals false),
--- a/src/Pure/axclass.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/axclass.ML Tue Oct 09 00:20:13 2007 +0200
@@ -148,7 +148,8 @@
fun the_classrel thy (c1, c2) =
(case AList.lookup (op =) (#1 (get_instances thy)) (c1, c2) of
SOME th => Thm.transfer thy th
- | NONE => error ("Unproven class relation " ^ Sign.string_of_classrel thy [c1, c2]));
+ | NONE => error ("Unproven class relation " ^
+ Syntax.string_of_classrel (ProofContext.init thy) [c1, c2]));
fun put_classrel arg = map_instances (fn (classrel, arities) =>
(insert (eq_fst op =) arg classrel, arities));
@@ -157,7 +158,8 @@
fun the_arity thy a (c, Ss) =
(case AList.lookup (op =) (Symtab.lookup_list (#2 (get_instances thy)) a) (c, Ss) of
SOME th => Thm.transfer thy th
- | NONE => error ("Unproven type arity " ^ Sign.string_of_arity thy (a, Ss, [c])));
+ | NONE => error ("Unproven type arity " ^
+ Syntax.string_of_arity (ProofContext.init thy) (a, Ss, [c])));
fun put_arity ((t, Ss, c), th) = map_instances (fn (classrel, arities) =>
(classrel, arities |> Symtab.insert_list (eq_fst op =) (t, ((c, Ss), th))));
@@ -173,7 +175,7 @@
fun pretty_axclass (class, AxClass {def, intro, axioms, params}) =
Pretty.block (Pretty.fbreaks
[Pretty.block
- [Pretty.str "class ", ProofContext.pretty_sort ctxt [class], Pretty.str ":"],
+ [Pretty.str "class ", Syntax.pretty_sort ctxt [class], Pretty.str ":"],
Pretty.strs ("parameters:" :: params_of thy class),
ProofContext.pretty_fact ctxt ("def", [def]),
ProofContext.pretty_fact ctxt (introN, [intro]),
@@ -233,11 +235,12 @@
fun prove_classrel raw_rel tac thy =
let
+ val ctxt = ProofContext.init thy;
val (c1, c2) = cert_classrel thy raw_rel;
- val th = Goal.prove (ProofContext.init thy) [] []
+ val th = Goal.prove ctxt [] []
(Logic.mk_classrel (c1, c2)) (fn _ => tac) handle ERROR msg =>
cat_error msg ("The error(s) above occurred while trying to prove class relation " ^
- quote (Sign.string_of_classrel thy [c1, c2]));
+ quote (Syntax.string_of_classrel ctxt [c1, c2]));
in
thy
|> PureThy.add_thms [((prefix classrel_prefix (Logic.name_classrel (c1, c2)), th), [])]
@@ -246,13 +249,14 @@
fun prove_arity raw_arity tac thy =
let
+ val ctxt = ProofContext.init thy;
val arity = Sign.cert_arity thy raw_arity;
val names = map (prefix arity_prefix) (Logic.name_arities arity);
val props = Logic.mk_arities arity;
- val ths = Goal.prove_multi (ProofContext.init thy) [] [] props
+ val ths = Goal.prove_multi ctxt [] [] props
(fn _ => Goal.precise_conjunction_tac (length props) 1 THEN tac) handle ERROR msg =>
cat_error msg ("The error(s) above occurred while trying to prove type arity " ^
- quote (Sign.string_of_arity thy arity));
+ quote (Syntax.string_of_arity ctxt arity));
in
thy
|> PureThy.add_thms (map (rpair []) (names ~~ ths))
--- a/src/Pure/codegen.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/codegen.ML Tue Oct 09 00:20:13 2007 +0200
@@ -982,8 +982,7 @@
| pretty_counterex ctxt (SOME cex) =
Pretty.chunks (Pretty.str "Counterexample found:\n" ::
map (fn (s, t) =>
- Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1,
- ProofContext.pretty_term ctxt t]) cex);
+ Pretty.block [Pretty.str (s ^ " ="), Pretty.brk 1, Syntax.pretty_term ctxt t]) cex);
val auto_quickcheck = ref true;
val auto_quickcheck_time_limit = ref 5000;
@@ -1043,8 +1042,8 @@
val T = Term.type_of t;
in
Pretty.writeln
- (Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt T)])
+ (Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt T)])
end);
exception Evaluation of term;
--- a/src/Pure/display.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Pure/display.ML Tue Oct 09 00:20:13 2007 +0200
@@ -146,12 +146,14 @@
fun pretty_full_theory verbose thy =
let
- fun prt_cls c = Sign.pretty_sort thy [c];
- fun prt_sort S = Sign.pretty_sort thy S;
- fun prt_arity t (c, (_, Ss)) = Sign.pretty_arity thy (t, Ss, [c]);
- fun prt_typ ty = Pretty.quote (Sign.pretty_typ thy ty);
+ val ctxt = ProofContext.init thy;
+
+ fun prt_cls c = Syntax.pretty_sort ctxt [c];
+ fun prt_sort S = Syntax.pretty_sort ctxt S;
+ fun prt_arity t (c, (_, Ss)) = Syntax.pretty_arity ctxt (t, Ss, [c]);
+ fun prt_typ ty = Pretty.quote (Syntax.pretty_typ ctxt ty);
val prt_typ_no_tvars = prt_typ o Logic.unvarifyT;
- fun prt_term t = Pretty.quote (Sign.pretty_term thy t);
+ fun prt_term t = Pretty.quote (Syntax.pretty_term ctxt t);
val prt_term_no_vars = prt_term o Logic.unvarify;
fun prt_const (c, ty) = [Pretty.str c, Pretty.str " ::", Pretty.brk 1, prt_typ_no_tvars ty];
val prt_const' = Defs.pretty_const (Sign.pp thy);
--- a/src/Tools/induct.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Tools/induct.ML Tue Oct 09 00:20:13 2007 +0200
@@ -718,7 +718,7 @@
inst >> Option.map (pair NONE);
val free = Scan.state -- Args.term >> (fn (_, Free v) => v | (context, t) =>
- error ("Bad free variable: " ^ ProofContext.string_of_term (Context.proof_of context) t));
+ error ("Bad free variable: " ^ Syntax.string_of_term (Context.proof_of context) t));
fun unless_more_args scan = Scan.unless (Scan.lift
((Args.$$$ arbitraryN || Args.$$$ takingN || Args.$$$ typeN ||
--- a/src/Tools/nbe.ML Mon Oct 08 22:06:32 2007 +0200
+++ b/src/Tools/nbe.ML Tue Oct 09 00:20:13 2007 +0200
@@ -393,8 +393,8 @@
val t' = norm_term thy t;
val ty' = Term.type_of t';
val p = PrintMode.with_modes modes (fn () =>
- Pretty.block [Pretty.quote (ProofContext.pretty_term ctxt t'), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1, Pretty.quote (ProofContext.pretty_typ ctxt ty')]) ();
+ Pretty.block [Pretty.quote (Syntax.pretty_term ctxt t'), Pretty.fbrk,
+ Pretty.str "::", Pretty.brk 1, Pretty.quote (Syntax.pretty_typ ctxt ty')]) ();
in Pretty.writeln p end;