--- a/src/HOL/Tools/inductive_codegen.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Wed Aug 11 18:17:53 2010 +0200
@@ -830,10 +830,10 @@
str "case Seq.pull (testf p) of", Pretty.brk 1,
str "SOME ", mk_tuple [mk_tuple (map (str o fst) args'), str "_"],
str " =>", Pretty.brk 1, str "SOME ",
- Pretty.block (str "[" ::
- Pretty.commas (map (fn (s, T) => Pretty.block
- [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args') @
- [str "]"]), Pretty.brk 1,
+ Pretty.enum "," "[" "]"
+ (map (fn (s, T) => Pretty.block
+ [mk_term_of gr "Generated" false T, Pretty.brk 1, str s]) args'),
+ Pretty.brk 1,
str "| NONE => NONE);"]) ^
"\n\nend;\n";
val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;
--- a/src/Pure/Isar/attrib.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/Pure/Isar/attrib.ML Wed Aug 11 18:17:53 2010 +0200
@@ -16,7 +16,6 @@
val defined: theory -> string -> bool
val attribute: theory -> src -> attribute
val attribute_i: theory -> src -> attribute
- val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
val map_specs: ('a -> 'att) ->
(('c * 'a list) * 'b) list -> (('c * 'att list) * 'b) list
val map_facts: ('a -> 'att) ->
@@ -25,6 +24,7 @@
val map_facts_refs: ('a -> 'att) -> ('b -> 'fact) ->
(('c * 'a list) * ('b * 'a list) list) list ->
(('c * 'att list) * ('fact * 'att list) list) list
+ val eval_thms: Proof.context -> (Facts.ref * src list) list -> thm list
val crude_closure: Proof.context -> src -> src
val setup: Binding.binding -> attribute context_parser -> string -> theory -> theory
val attribute_setup: bstring * Position.T -> Symbol_Pos.text * Position.T -> string ->
@@ -94,8 +94,7 @@
fun pretty_attribs _ [] = []
| pretty_attribs ctxt srcs =
- [Pretty.enclose "[" "]"
- (Pretty.commas (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs))];
+ [Pretty.enum "," "[" "]" (map (Args.pretty_src ctxt o Args.map_name (extern ctxt)) srcs)];
(* get attributes *)
@@ -115,11 +114,6 @@
fun attribute thy = attribute_i thy o intern_src thy;
-fun eval_thms ctxt args = ProofContext.note_thmss ""
- [(Thm.empty_binding, args |> map (fn (a, atts) =>
- (ProofContext.get_fact ctxt a, map (attribute (ProofContext.theory_of ctxt)) atts)))] ctxt
- |> fst |> maps snd;
-
(* attributed declarations *)
@@ -129,6 +123,15 @@
fun map_facts_refs f g = map_facts f #> map (apsnd (map (apfst g)));
+(* fact expressions *)
+
+fun eval_thms ctxt srcs = ctxt
+ |> ProofContext.note_thmss ""
+ (map_facts_refs (attribute (ProofContext.theory_of ctxt)) (ProofContext.get_fact ctxt)
+ [((Binding.empty, []), srcs)])
+ |> fst |> maps snd;
+
+
(* crude_closure *)
(*Produce closure without knowing facts in advance! The following
--- a/src/Pure/Isar/calculation.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/Pure/Isar/calculation.ML Wed Aug 11 18:17:53 2010 +0200
@@ -37,8 +37,10 @@
((Item_Net.merge (trans1, trans2), Thm.merge_thms (sym1, sym2)), NONE);
);
+val get_rules = #1 o Data.get o Context.Proof;
+
fun print_rules ctxt =
- let val ((trans, sym), _) = Data.get (Context.Proof ctxt) in
+ let val (trans, sym) = get_rules ctxt in
[Pretty.big_list "transitivity rules:"
(map (Display.pretty_thm ctxt) (Item_Net.content trans)),
Pretty.big_list "symmetry rules:" (map (Display.pretty_thm ctxt) sym)]
@@ -122,21 +124,21 @@
(* also and finally *)
-val get_rules = #1 o Data.get o Context.Proof o Proof.context_of;
-
fun calculate prep_rules final raw_rules int state =
let
+ val ctxt = Proof.context_of state;
+
val strip_assums_concl = Logic.strip_assums_concl o Thm.prop_of;
val eq_prop = op aconv o pairself (Envir.beta_eta_contract o strip_assums_concl);
fun projection ths th = exists (curry eq_prop th) ths;
- val opt_rules = Option.map (prep_rules state) raw_rules;
+ val opt_rules = Option.map (prep_rules ctxt) raw_rules;
fun combine ths =
(case opt_rules of SOME rules => rules
| NONE =>
(case ths of
- [] => Item_Net.content (#1 (get_rules state))
- | th :: _ => Item_Net.retrieve (#1 (get_rules state)) (strip_assums_concl th)))
+ [] => Item_Net.content (#1 (get_rules ctxt))
+ | th :: _ => Item_Net.retrieve (#1 (get_rules ctxt)) (strip_assums_concl th)))
|> Seq.of_list |> Seq.maps (Drule.multi_resolve ths)
|> Seq.filter (not o projection ths);
@@ -154,9 +156,9 @@
end;
val also = calculate (K I) false;
-val also_cmd = calculate Proof.get_thmss_cmd false;
+val also_cmd = calculate Attrib.eval_thms false;
val finally = calculate (K I) true;
-val finally_cmd = calculate Proof.get_thmss_cmd true;
+val finally_cmd = calculate Attrib.eval_thms true;
(* moreover and ultimately *)
--- a/src/Pure/Isar/isar_cmd.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/Pure/Isar/isar_cmd.ML Wed Aug 11 18:17:53 2010 +0200
@@ -416,7 +416,7 @@
fun thm_deps args = Toplevel.unknown_theory o Toplevel.keep (fn state =>
Thm_Deps.thm_deps (Toplevel.theory_of state)
- (Proof.get_thmss_cmd (Toplevel.enter_proof_body state) args));
+ (Attrib.eval_thms (Toplevel.context_of state) args));
(* find unused theorems *)
@@ -450,20 +450,20 @@
local
-fun string_of_stmts state args =
- Proof.get_thmss_cmd state args
- |> map (Element.pretty_statement (Proof.context_of state) Thm.theoremK)
+fun string_of_stmts ctxt args =
+ Attrib.eval_thms ctxt args
+ |> map (Element.pretty_statement ctxt Thm.theoremK)
|> Pretty.chunks2 |> Pretty.string_of;
-fun string_of_thms state args =
- Pretty.string_of (Display.pretty_thms (Proof.context_of state) (Proof.get_thmss_cmd state args));
+fun string_of_thms ctxt args =
+ Pretty.string_of (Display.pretty_thms ctxt (Attrib.eval_thms ctxt args));
fun string_of_prfs full state arg =
Pretty.string_of
(case arg of
NONE =>
let
- val {context = ctxt, goal = thm} = Proof.simple_goal state;
+ val {context = ctxt, goal = thm} = Proof.simple_goal (Toplevel.proof_of state);
val thy = ProofContext.theory_of ctxt;
val prf = Thm.proof_of thm;
val prop = Thm.full_prop_of thm;
@@ -472,20 +472,19 @@
Proof_Syntax.pretty_proof ctxt
(if full then Reconstruct.reconstruct_proof thy prop prf' else prf')
end
- | SOME args => Pretty.chunks
- (map (Proof_Syntax.pretty_proof_of (Proof.context_of state) full)
- (Proof.get_thmss_cmd state args)));
+ | SOME srcs =>
+ let val ctxt = Toplevel.context_of state
+ in map (Proof_Syntax.pretty_proof_of ctxt full) (Attrib.eval_thms ctxt srcs) end
+ |> Pretty.chunks);
-fun string_of_prop state s =
+fun string_of_prop ctxt s =
let
- val ctxt = Proof.context_of state;
val prop = Syntax.read_prop ctxt s;
val ctxt' = Variable.auto_fixes prop ctxt;
in Pretty.string_of (Pretty.quote (Syntax.pretty_term ctxt' prop)) end;
-fun string_of_term state s =
+fun string_of_term ctxt s =
let
- val ctxt = Proof.context_of state;
val t = Syntax.read_term ctxt s;
val T = Term.type_of t;
val ctxt' = Variable.auto_fixes t ctxt;
@@ -495,24 +494,21 @@
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 = Syntax.read_typ ctxt s;
+fun string_of_type ctxt s =
+ let val T = Syntax.read_typ ctxt s
in Pretty.string_of (Pretty.quote (Syntax.pretty_typ ctxt T)) end;
fun print_item string_of (modes, arg) = Toplevel.keep (fn state =>
- Print_Mode.with_modes modes (fn () =>
- writeln (string_of (Toplevel.enter_proof_body state) arg)) ());
+ Print_Mode.with_modes modes (fn () => writeln (string_of state arg)) ());
in
-val print_stmts = print_item string_of_stmts;
-val print_thms = print_item string_of_thms;
+val print_stmts = print_item (string_of_stmts o Toplevel.context_of);
+val print_thms = print_item (string_of_thms o Toplevel.context_of);
val print_prfs = print_item o string_of_prfs;
-val print_prop = print_item string_of_prop;
-val print_term = print_item string_of_term;
-val print_type = print_item string_of_type;
+val print_prop = print_item (string_of_prop o Toplevel.context_of);
+val print_term = print_item (string_of_term o Toplevel.context_of);
+val print_type = print_item (string_of_type o Toplevel.context_of);
end;
--- a/src/Pure/Isar/proof.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/Pure/Isar/proof.ML Wed Aug 11 18:17:53 2010 +0200
@@ -60,7 +60,6 @@
val def_cmd: (Attrib.binding * ((binding * mixfix) * (string * string list))) list -> state -> state
val chain: state -> state
val chain_facts: thm list -> state -> state
- val get_thmss_cmd: state -> (Facts.ref * Attrib.src list) list -> thm list
val note_thmss: (Thm.binding * (thm list * attribute list) list) list -> state -> state
val note_thmss_cmd: (Attrib.binding * (Facts.ref * Attrib.src list) list) list -> state -> state
val from_thmss: ((thm list * attribute list) list) list -> state -> state
@@ -679,8 +678,6 @@
val local_results = gen_thmss (K []) I I (K I) (K I) o map (apsnd Thm.simple_fact);
-fun get_thmss_cmd state srcs = the_facts (note_thmss_cmd [((Binding.empty, []), srcs)] state);
-
end;
--- a/src/Pure/Isar/proof_context.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/Pure/Isar/proof_context.ML Wed Aug 11 18:17:53 2010 +0200
@@ -1123,7 +1123,7 @@
val type_notation = gen_notation (K type_syntax);
val notation = gen_notation const_syntax;
-fun target_type_notation add mode args phi =
+fun target_type_notation add mode args phi =
let
val args' = args |> map_filter (fn (T, mx) =>
let
--- a/src/Pure/Isar/toplevel.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/Pure/Isar/toplevel.ML Wed Aug 11 18:17:53 2010 +0200
@@ -20,7 +20,6 @@
val theory_of: state -> theory
val proof_of: state -> Proof.state
val proof_position_of: state -> int
- val enter_proof_body: state -> Proof.state
val end_theory: Position.T -> state -> theory
val print_state_context: state -> unit
val print_state: bool -> state -> unit
@@ -186,8 +185,6 @@
Proof (prf, _) => Proof_Node.position prf
| _ => raise UNDEF);
-val enter_proof_body = node_case (Proof.init o Context.proof_of) Proof.enter_forward;
-
fun end_theory _ (State (NONE, SOME (Theory (Context.Theory thy, _)))) = Theory.end_theory thy
| end_theory pos _ = error ("Unfinished theory at end of input" ^ Position.str_of pos);
--- a/src/Pure/Syntax/ast.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/Pure/Syntax/ast.ML Wed Aug 11 18:17:53 2010 +0200
@@ -75,8 +75,7 @@
fun pretty_ast (Constant a) = Pretty.quote (Pretty.str a)
| pretty_ast (Variable x) = Pretty.str x
- | pretty_ast (Appl asts) =
- Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
+ | pretty_ast (Appl asts) = Pretty.enclose "(" ")" (Pretty.breaks (map pretty_ast asts));
fun pretty_rule (lhs, rhs) =
Pretty.block [pretty_ast lhs, Pretty.str " ->", Pretty.brk 2, pretty_ast rhs];
--- a/src/Pure/Tools/find_consts.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/Pure/Tools/find_consts.ML Wed Aug 11 18:17:53 2010 +0200
@@ -28,24 +28,13 @@
(* matching types/consts *)
fun matches_subtype thy typat =
- let
- val p = can (fn ty => Sign.typ_match thy (typat, ty) Vartab.empty);
-
- fun fs [] = false
- | fs (t :: ts) = f t orelse fs ts
+ Term.exists_subtype (fn ty => Sign.typ_instance thy (ty, typat));
- and f (t as Type (_, ars)) = p t orelse fs ars
- | f t = p t;
- in f end;
-
-fun check_const p (nm, (ty, _)) =
- if p (nm, ty)
- then SOME (Term.size_of_typ ty)
- else NONE;
+fun check_const pred (nm, (ty, _)) =
+ if pred (nm, ty) then SOME (Term.size_of_typ ty) else NONE;
fun opt_not f (c as (_, (ty, _))) =
- if is_some (f c)
- then NONE else SOME (Term.size_of_typ ty);
+ if is_some (f c) then NONE else SOME (Term.size_of_typ ty);
fun filter_const _ NONE = NONE
| filter_const f (SOME (c, r)) =
@@ -71,8 +60,7 @@
val ty' = Logic.unvarifyT_global ty;
in
Pretty.block
- [Pretty.quote (Pretty.str nm), Pretty.fbrk,
- Pretty.str "::", Pretty.brk 1,
+ [Pretty.str nm, Pretty.str " ::", Pretty.brk 1,
Pretty.quote (Syntax.pretty_typ ctxt ty')]
end;
@@ -128,35 +116,35 @@
val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
in
- Pretty.big_list "searched for:" (map pretty_criterion raw_criteria)
- :: Pretty.str ""
- :: (Pretty.str o implode)
- (if null matches
- then ["nothing found", end_msg]
- else ["found ", (string_of_int o length) matches,
- " constants", end_msg, ":"])
- :: Pretty.str ""
- :: map (pretty_const ctxt) matches
- |> Pretty.chunks
- |> Pretty.writeln
- end;
+ Pretty.big_list "searched for:" (map pretty_criterion raw_criteria) ::
+ Pretty.str "" ::
+ Pretty.str
+ (if null matches
+ then "nothing found" ^ end_msg
+ else "found " ^ string_of_int (length matches) ^ " constant(s)" ^ end_msg ^ ":") ::
+ Pretty.str "" ::
+ map (pretty_const ctxt) matches
+ end |> Pretty.chunks |> Pretty.writeln;
(* command syntax *)
-fun find_consts_cmd spec =
- Toplevel.unknown_theory o Toplevel.keep (fn state =>
- find_consts (Proof.context_of (Toplevel.enter_proof_body state)) spec);
+local
val criterion =
Parse.reserved "strict" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Strict ||
Parse.reserved "name" |-- Parse.!!! (Parse.$$$ ":" |-- Parse.xname) >> Name ||
Parse.xname >> Loose;
+in
+
val _ =
Outer_Syntax.improper_command "find_consts" "search constants by type pattern" Keyword.diag
(Scan.repeat ((Scan.option Parse.minus >> is_none) -- criterion)
- >> (Toplevel.no_timing oo find_consts_cmd));
+ >> (fn spec => Toplevel.no_timing o
+ Toplevel.keep (fn state => find_consts (Toplevel.context_of state) spec)));
end;
+end;
+
--- a/src/Pure/Tools/find_theorems.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/Pure/Tools/find_theorems.ML Wed Aug 11 18:17:53 2010 +0200
@@ -433,36 +433,27 @@
val tally_msg =
(case foundo of
- NONE => "displaying " ^ string_of_int returned ^ " theorems"
+ NONE => "displaying " ^ string_of_int returned ^ " theorem(s)"
| SOME found =>
- "found " ^ string_of_int found ^ " theorems" ^
+ "found " ^ string_of_int found ^ " theorem(s)" ^
(if returned < found
then " (" ^ string_of_int returned ^ " displayed)"
else ""));
val end_msg = " in " ^ Time.toString (#cpu (end_timing start)) ^ " secs";
in
- Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria)
- :: Pretty.str "" ::
- (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
- else
- [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
+ Pretty.big_list "searched for:" (map (pretty_criterion ctxt) criteria) ::
+ Pretty.str "" ::
+ (if null thms then [Pretty.str ("nothing found" ^ end_msg)]
+ else
+ [Pretty.str (tally_msg ^ end_msg ^ ":"), Pretty.str ""] @
map (pretty_thm ctxt) thms)
- |> Pretty.chunks |> Pretty.writeln
- end;
+ end |> Pretty.chunks |> Pretty.writeln;
(** command syntax **)
-fun find_theorems_cmd ((opt_lim, rem_dups), spec) =
- Toplevel.unknown_theory o Toplevel.keep (fn state =>
- let
- val proof_state = Toplevel.enter_proof_body state;
- val ctxt = Proof.context_of proof_state;
- val opt_goal = try Proof.simple_goal proof_state |> Option.map #goal;
- in print_theorems ctxt opt_goal opt_lim rem_dups spec end);
-
local
val criterion =
@@ -486,7 +477,13 @@
Outer_Syntax.improper_command "find_theorems" "print theorems meeting specified criteria"
Keyword.diag
(options -- Scan.repeat (((Scan.option Parse.minus >> is_none) -- criterion))
- >> (Toplevel.no_timing oo find_theorems_cmd));
+ >> (fn ((opt_lim, rem_dups), spec) =>
+ Toplevel.no_timing o
+ Toplevel.keep (fn state =>
+ let
+ val ctxt = Toplevel.context_of state;
+ val opt_goal = try (Proof.simple_goal o Toplevel.proof_of) state |> Option.map #goal;
+ in print_theorems ctxt opt_goal opt_lim rem_dups spec end)));
end;
--- a/src/Pure/codegen.ML Wed Aug 11 14:45:38 2010 +0200
+++ b/src/Pure/codegen.ML Wed Aug 11 18:17:53 2010 +0200
@@ -889,9 +889,8 @@
mk_app false (str "testf") (map (str o fst) args),
Pretty.brk 1, str "then NONE",
Pretty.brk 1, str "else ",
- Pretty.block [str "SOME ", Pretty.block (str "[" ::
- Pretty.commas (map (fn (s, _) => str (s ^ "_t ()")) args) @
- [str "]"])]]),
+ Pretty.block [str "SOME ",
+ Pretty.enum "," "[" "]" (map (fn (s, _) => str (s ^ "_t ()")) args)]]),
str ");"]) ^
"\n\nend;\n";
val _ = ML_Context.eval_text_in (SOME ctxt) false Position.none s;