--- a/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Jul 01 17:44:04 2011 +0200
+++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Jul 01 18:11:17 2011 +0200
@@ -179,6 +179,7 @@
antiquotations are checked within the current theory or proof
context.
+ %% FIXME less monolithic presentation, move to individual sections!?
@{rail "
'@{' antiquotation '}'
;
@@ -188,7 +189,7 @@
@@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
@@{antiquotation prop} options styles @{syntax prop} |
@@{antiquotation term} options styles @{syntax term} |
- @@{antiquotation value} options styles @{syntax term} |
+ @@{antiquotation (HOL) value} options styles @{syntax term} |
@@{antiquotation term_type} options styles @{syntax term} |
@@{antiquotation typeof} options styles @{syntax term} |
@@{antiquotation const} options @{syntax term} |
@@ -238,7 +239,8 @@
\item @{text "@{term t}"} prints a well-typed term @{text "t"}.
- \item @{text "@{value t}"} evaluates a term @{text "t"} and prints its result.
+ \item @{text "@{value t}"} evaluates a term @{text "t"} and prints
+ its result, see also @{command_ref (HOL) value}.
\item @{text "@{term_type t}"} prints a well-typed term @{text "t"}
annotated with its type.
--- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Jul 01 17:44:04 2011 +0200
+++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Jul 01 18:11:17 2011 +0200
@@ -229,6 +229,7 @@
antiquotations are checked within the current theory or proof
context.
+ %% FIXME less monolithic presentation, move to individual sections!?
\begin{railoutput}
\rail@begin{1}{}
\rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[]
@@ -266,7 +267,7 @@
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
\rail@nextbar{6}
-\rail@term{\hyperlink{antiquotation.value}{\mbox{\isa{value}}}}[]
+\rail@term{\hyperlink{antiquotation.HOL.value}{\mbox{\isa{value}}}}[]
\rail@nont{\isa{options}}[]
\rail@nont{\isa{styles}}[]
\rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
@@ -396,7 +397,8 @@
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a well-typed term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}}.
- \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}value\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} evaluates a term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} and prints its result.
+ \item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}value\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} evaluates a term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}} and prints
+ its result, see also \indexref{HOL}{command}{value}\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}.
\item \isa{{\isaliteral{22}{\isachardoublequote}}{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}term{\isaliteral{5F}{\isacharunderscore}}type\ t{\isaliteral{7D}{\isacharbraceright}}{\isaliteral{22}{\isachardoublequote}}} prints a well-typed term \isa{{\isaliteral{22}{\isachardoublequote}}t{\isaliteral{22}{\isachardoublequote}}}
annotated with its type.
--- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Jul 01 17:44:04 2011 +0200
+++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Jul 01 18:11:17 2011 +0200
@@ -1902,7 +1902,7 @@
val setT = HOLogic.mk_setT T
val elems = HOLogic.mk_set T ts
val ([dots], ctxt') =
- Proof_Context.add_fixes [(Binding.name "dots", SOME setT, Mixfix ("...", [], 1000))] ctxt
+ Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt
(* check expected values *)
val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
val () =
--- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jul 01 17:44:04 2011 +0200
+++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jul 01 18:11:17 2011 +0200
@@ -408,8 +408,10 @@
val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t
- val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
- ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
+ (* FIXME proper naming convention for local_theory *)
+ val ((prop_def, _), ctxt') =
+ Local_Theory.define ((Binding.conceal @{binding test_property}, NoSyn),
+ ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt')
val (counterexample, result) = dynamic_value_strict (true, opts)
(Existential_Counterexample.get, Existential_Counterexample.put,
--- a/src/HOL/Tools/inductive_codegen.ML Fri Jul 01 17:44:04 2011 +0200
+++ b/src/HOL/Tools/inductive_codegen.ML Fri Jul 01 18:11:17 2011 +0200
@@ -884,7 +884,7 @@
val (_, thy') = Inductive.add_inductive_global
{quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false,
no_elim=true, no_ind=false, skip_mono=false, fork_mono=false}
- [((Binding.name "quickcheckp", T), NoSyn)] []
+ [((@{binding quickcheckp}, T), NoSyn)] []
[(Attrib.empty_binding, rl)] [] (Theory.copy thy);
val pred = HOLogic.mk_Trueprop (list_comb
(Const (Sign.intern_const thy' "quickcheckp", T),
--- a/src/Pure/Isar/outer_syntax.ML Fri Jul 01 17:44:04 2011 +0200
+++ b/src/Pure/Isar/outer_syntax.ML Fri Jul 01 18:11:17 2011 +0200
@@ -249,13 +249,13 @@
handle ERROR msg => (Toplevel.malformed range_pos msg, true)
end;
-fun prepare_atom commands init (cmd, proof, proper_proof) =
+fun prepare_element commands init {head, proof, proper_proof} =
let
- val (tr, proper_cmd) = prepare_span commands cmd |>> Toplevel.modify_init init;
+ val (tr, proper_head) = prepare_span commands head |>> Toplevel.modify_init init;
val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
in
- if proper_cmd andalso proper_proof then [(tr, proof_trs)]
- else map (rpair []) (if proper_cmd then tr :: proof_trs else proof_trs)
+ if proper_head andalso proper_proof then [(tr, proof_trs)]
+ else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
end;
fun prepare_command pos str =
@@ -278,14 +278,14 @@
val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
val spans = Source.exhaust (Thy_Syntax.span_source toks);
val _ = List.app Thy_Syntax.report_span spans; (* FIXME ?? *)
- val atoms = Source.exhaust (Thy_Syntax.atom_source (Source.of_list spans))
- |> Par_List.map_name "Outer_Syntax.prepare_atom" (prepare_atom commands init) |> flat;
+ val elements = Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
+ |> Par_List.map_name "Outer_Syntax.prepare_element" (prepare_element commands init) |> flat;
val _ = Present.theory_source name
(fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
- val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion atoms);
+ val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
val present =
--- a/src/Pure/Thy/thy_syntax.ML Fri Jul 01 17:44:04 2011 +0200
+++ b/src/Pure/Thy/thy_syntax.ML Fri Jul 01 18:11:17 2011 +0200
@@ -21,8 +21,9 @@
val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
val present_span: span -> Output.output
val report_span: span -> unit
- val atom_source: (span, 'a) Source.source ->
- (span * span list * bool, (span, 'a) Source.source) Source.source
+ type element = {head: span, proof: span list, proper_proof: bool}
+ val element_source: (span, 'a) Source.source ->
+ (element, (span, 'a) Source.source) Source.source
end;
structure Thy_Syntax: THY_SYNTAX =
@@ -159,7 +160,13 @@
-(** specification atoms: commands with optional proof **)
+(** specification elements: commands with optional proof **)
+
+type element = {head: span, proof: span list, proper_proof: bool};
+
+fun make_element head proof proper_proof =
+ {head = head, proof = proof, proper_proof = proper_proof};
+
(* scanning spans *)
@@ -173,7 +180,7 @@
val stopper = Scan.stopper (K eof) is_eof;
-(* atom_source *)
+(* element_source *)
local
@@ -187,13 +194,14 @@
(if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
-val atom =
- command_with Keyword.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
- Scan.one not_eof >> (fn a => (a, [], true));
+val element =
+ command_with Keyword.is_theory_goal -- proof
+ >> (fn (a, (bs, d)) => make_element a bs (d >= 0)) ||
+ Scan.one not_eof >> (fn a => make_element a [] true);
in
-fun atom_source src = Source.source stopper (Scan.bulk atom) NONE src;
+fun element_source src = Source.source stopper (Scan.bulk element) NONE src;
end;
--- a/src/Pure/Tools/find_theorems.ML Fri Jul 01 17:44:04 2011 +0200
+++ b/src/Pure/Tools/find_theorems.ML Fri Jul 01 18:11:17 2011 +0200
@@ -101,6 +101,7 @@
end;
+
(** queries **)
type 'term query = {
@@ -154,6 +155,8 @@
end
| query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
+
+
(** theorems, either internal or external (without proof) **)
datatype theorem =
@@ -164,21 +167,21 @@
Position.markup pos o Markup.properties [("name", name), ("index", Markup.print_int i)]
| fact_ref_markup (Facts.Named ((name, pos), NONE)) =
Position.markup pos o Markup.properties [("name", name)]
- | fact_ref_markup fact_ref = raise Fail "bad fact ref"
+ | fact_ref_markup fact_ref = raise Fail "bad fact ref";
fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
| xml_of_theorem (External (fact_ref, prop)) =
- XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop])
+ XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop]);
fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
- let
- val name = the (Properties.get properties "name");
- val pos = Position.of_properties properties;
- val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
- (Properties.get properties "index");
- in
- External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
- end
+ let
+ val name = the (Properties.get properties "name");
+ val pos = Position.of_properties properties;
+ val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
+ (Properties.get properties "index");
+ in
+ External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
+ end
| theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
fun xml_of_result (opt_found, theorems) =
@@ -207,6 +210,8 @@
fun fact_ref_of (Internal (fact_ref, _)) = fact_ref
| fact_ref_of (External (fact_ref, _)) = fact_ref;
+
+
(** search criterion filters **)
(*generated filters are to be of the form
@@ -228,7 +233,7 @@
fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
-(*educated guesses on HOL*) (* FIXME broken *)
+(*educated guesses on HOL*) (* FIXME utterly broken *)
val boolT = Type ("bool", []);
val iff_const = Const ("op =", boolT --> boolT --> boolT);
@@ -339,8 +344,8 @@
else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
in
fn Internal (_, thm) =>
- if is_some (Seq.pull (try_thm thm))
- then SOME (Thm.nprems_of thm, 0) else NONE
+ if is_some (Seq.pull (try_thm thm))
+ then SOME (Thm.nprems_of thm, 0) else NONE
| External _ => NONE
end;
@@ -423,7 +428,6 @@
in app (opt_add r r', consts', fs) end;
in app end;
-
in
fun filter_criterion ctxt opt_goal (b, c) =
@@ -520,8 +524,6 @@
in
maps Facts.selections
(visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)) @
-
-
visible_facts (Proof_Context.facts_of ctxt))
end;
--- a/src/Tools/Code/code_runtime.ML Fri Jul 01 17:44:04 2011 +0200
+++ b/src/Tools/Code/code_runtime.ML Fri Jul 01 18:11:17 2011 +0200
@@ -163,7 +163,7 @@
end;
val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "holds_by_evaluation",
+ (Thm.add_oracle (@{binding holds_by_evaluation},
fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
@@ -338,7 +338,7 @@
val _ =
Context.>> (Context.map_theory
- (ML_Context.add_antiq (Binding.name "code") (fn _ => Args.term >> ml_code_antiq)));
+ (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq)));
local
--- a/src/Tools/Code/code_simp.ML Fri Jul 01 17:44:04 2011 +0200
+++ b/src/Tools/Code/code_simp.ML Fri Jul 01 18:11:17 2011 +0200
@@ -58,9 +58,10 @@
fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
-val setup = Method.setup (Binding.name "code_simp")
- (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
- "simplification with code equations"
+val setup =
+ Method.setup @{binding code_simp}
+ (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
+ "simplification with code equations"
#> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of);
--- a/src/Tools/nbe.ML Fri Jul 01 17:44:04 2011 +0200
+++ b/src/Tools/nbe.ML Fri Jul 01 18:11:17 2011 +0200
@@ -78,7 +78,7 @@
val get_triv_classes = map fst o Triv_Class_Data.get;
val (_, triv_of_class) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "triv_of_class", fn (thy, T, class) =>
+ (Thm.add_oracle (@{binding triv_of_class}, fn (thy, T, class) =>
Thm.cterm_of thy (Logic.mk_of_class (T, class)))));
in
@@ -589,7 +589,7 @@
in Thm.mk_binop eq lhs rhs end;
val (_, raw_oracle) = Context.>>> (Context.map_theory_result
- (Thm.add_oracle (Binding.name "normalization_by_evaluation",
+ (Thm.add_oracle (@{binding normalization_by_evaluation},
fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
--- a/src/Tools/value.ML Fri Jul 01 17:44:04 2011 +0200
+++ b/src/Tools/value.ML Fri Jul 01 18:11:17 2011 +0200
@@ -69,7 +69,7 @@
(value_cmd some_name modes t)));
val antiq_setup =
- Thy_Output.antiquotation (Binding.name "value")
+ Thy_Output.antiquotation @{binding value}
(Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
(fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
(Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source