# HG changeset patch # User wenzelm # Date 1309536677 -7200 # Node ID 37d52be4d8db3116729b1d80d90e3c4cfdf6e981 # Parent 4144d7b4ec77c1ce51e1058794263ab794dbdfe2# Parent e8858190cccdbd97b24f276cab595dfcb0d4c154 merged; diff -r 4144d7b4ec77 -r 37d52be4d8db doc-src/IsarRef/Thy/Document_Preparation.thy --- 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. diff -r 4144d7b4ec77 -r 37d52be4d8db doc-src/IsarRef/Thy/document/Document_Preparation.tex --- 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. diff -r 4144d7b4ec77 -r 37d52be4d8db src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML --- 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 () = diff -r 4144d7b4ec77 -r 37d52be4d8db src/HOL/Tools/Quickcheck/narrowing_generators.ML --- 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, diff -r 4144d7b4ec77 -r 37d52be4d8db src/HOL/Tools/inductive_codegen.ML --- 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), diff -r 4144d7b4ec77 -r 37d52be4d8db src/Pure/Isar/outer_syntax.ML --- 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 = diff -r 4144d7b4ec77 -r 37d52be4d8db src/Pure/Thy/thy_syntax.ML --- 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; diff -r 4144d7b4ec77 -r 37d52be4d8db src/Pure/Tools/find_theorems.ML --- 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; diff -r 4144d7b4ec77 -r 37d52be4d8db src/Tools/Code/code_runtime.ML --- 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 diff -r 4144d7b4ec77 -r 37d52be4d8db src/Tools/Code/code_simp.ML --- 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); diff -r 4144d7b4ec77 -r 37d52be4d8db src/Tools/nbe.ML --- 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)))); diff -r 4144d7b4ec77 -r 37d52be4d8db src/Tools/value.ML --- 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