1.1 --- a/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Jul 01 17:44:04 2011 +0200
1.2 +++ b/doc-src/IsarRef/Thy/Document_Preparation.thy Fri Jul 01 18:11:17 2011 +0200
1.3 @@ -179,6 +179,7 @@
1.4 antiquotations are checked within the current theory or proof
1.5 context.
1.6
1.7 + %% FIXME less monolithic presentation, move to individual sections!?
1.8 @{rail "
1.9 '@{' antiquotation '}'
1.10 ;
1.11 @@ -188,7 +189,7 @@
1.12 @@{antiquotation lemma} options @{syntax prop} @'by' @{syntax method} @{syntax method}? |
1.13 @@{antiquotation prop} options styles @{syntax prop} |
1.14 @@{antiquotation term} options styles @{syntax term} |
1.15 - @@{antiquotation value} options styles @{syntax term} |
1.16 + @@{antiquotation (HOL) value} options styles @{syntax term} |
1.17 @@{antiquotation term_type} options styles @{syntax term} |
1.18 @@{antiquotation typeof} options styles @{syntax term} |
1.19 @@{antiquotation const} options @{syntax term} |
1.20 @@ -238,7 +239,8 @@
1.21
1.22 \item @{text "@{term t}"} prints a well-typed term @{text "t"}.
1.23
1.24 - \item @{text "@{value t}"} evaluates a term @{text "t"} and prints its result.
1.25 + \item @{text "@{value t}"} evaluates a term @{text "t"} and prints
1.26 + its result, see also @{command_ref (HOL) value}.
1.27
1.28 \item @{text "@{term_type t}"} prints a well-typed term @{text "t"}
1.29 annotated with its type.
2.1 --- a/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Jul 01 17:44:04 2011 +0200
2.2 +++ b/doc-src/IsarRef/Thy/document/Document_Preparation.tex Fri Jul 01 18:11:17 2011 +0200
2.3 @@ -229,6 +229,7 @@
2.4 antiquotations are checked within the current theory or proof
2.5 context.
2.6
2.7 + %% FIXME less monolithic presentation, move to individual sections!?
2.8 \begin{railoutput}
2.9 \rail@begin{1}{}
2.10 \rail@term{\isa{{\isaliteral{40}{\isacharat}}{\isaliteral{7B}{\isacharbraceleft}}}}[]
2.11 @@ -266,7 +267,7 @@
2.12 \rail@nont{\isa{styles}}[]
2.13 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2.14 \rail@nextbar{6}
2.15 -\rail@term{\hyperlink{antiquotation.value}{\mbox{\isa{value}}}}[]
2.16 +\rail@term{\hyperlink{antiquotation.HOL.value}{\mbox{\isa{value}}}}[]
2.17 \rail@nont{\isa{options}}[]
2.18 \rail@nont{\isa{styles}}[]
2.19 \rail@nont{\hyperlink{syntax.term}{\mbox{\isa{term}}}}[]
2.20 @@ -396,7 +397,8 @@
2.21
2.22 \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}}}.
2.23
2.24 - \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.
2.25 + \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
2.26 + its result, see also \indexref{HOL}{command}{value}\hyperlink{command.HOL.value}{\mbox{\isa{\isacommand{value}}}}.
2.27
2.28 \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}}}
2.29 annotated with its type.
3.1 --- a/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Jul 01 17:44:04 2011 +0200
3.2 +++ b/src/HOL/Tools/Predicate_Compile/predicate_compile_core.ML Fri Jul 01 18:11:17 2011 +0200
3.3 @@ -1902,7 +1902,7 @@
3.4 val setT = HOLogic.mk_setT T
3.5 val elems = HOLogic.mk_set T ts
3.6 val ([dots], ctxt') =
3.7 - Proof_Context.add_fixes [(Binding.name "dots", SOME setT, Mixfix ("...", [], 1000))] ctxt
3.8 + Proof_Context.add_fixes [(@{binding dots}, SOME setT, Mixfix ("...", [], 1000))] ctxt
3.9 (* check expected values *)
3.10 val union = Const (@{const_abbrev Set.union}, setT --> setT --> setT)
3.11 val () =
4.1 --- a/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jul 01 17:44:04 2011 +0200
4.2 +++ b/src/HOL/Tools/Quickcheck/narrowing_generators.ML Fri Jul 01 18:11:17 2011 +0200
4.3 @@ -408,8 +408,10 @@
4.4 val finitize = if Config.get ctxt finite_functions then wrap finitize_functions else I
4.5 val (qs, prop_t) = finitize (strip_quantifiers pnf_t)
4.6 val prop_term = fold_rev (fn (_, (x, T)) => fn t => Abs (x, T, t)) qs prop_t
4.7 - val ((prop_def, _), ctxt') = Local_Theory.define ((Binding.conceal (Binding.name "test_property"), NoSyn),
4.8 - ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
4.9 + (* FIXME proper naming convention for local_theory *)
4.10 + val ((prop_def, _), ctxt') =
4.11 + Local_Theory.define ((Binding.conceal @{binding test_property}, NoSyn),
4.12 + ((Binding.conceal Binding.empty, [Code.add_default_eqn_attrib]), prop_term)) ctxt
4.13 val (prop_def', thy') = Local_Theory.exit_result_global Morphism.term (prop_def, ctxt')
4.14 val (counterexample, result) = dynamic_value_strict (true, opts)
4.15 (Existential_Counterexample.get, Existential_Counterexample.put,
5.1 --- a/src/HOL/Tools/inductive_codegen.ML Fri Jul 01 17:44:04 2011 +0200
5.2 +++ b/src/HOL/Tools/inductive_codegen.ML Fri Jul 01 18:11:17 2011 +0200
5.3 @@ -884,7 +884,7 @@
5.4 val (_, thy') = Inductive.add_inductive_global
5.5 {quiet_mode=true, verbose=false, alt_name=Binding.empty, coind=false,
5.6 no_elim=true, no_ind=false, skip_mono=false, fork_mono=false}
5.7 - [((Binding.name "quickcheckp", T), NoSyn)] []
5.8 + [((@{binding quickcheckp}, T), NoSyn)] []
5.9 [(Attrib.empty_binding, rl)] [] (Theory.copy thy);
5.10 val pred = HOLogic.mk_Trueprop (list_comb
5.11 (Const (Sign.intern_const thy' "quickcheckp", T),
6.1 --- a/src/Pure/Isar/outer_syntax.ML Fri Jul 01 17:44:04 2011 +0200
6.2 +++ b/src/Pure/Isar/outer_syntax.ML Fri Jul 01 18:11:17 2011 +0200
6.3 @@ -249,13 +249,13 @@
6.4 handle ERROR msg => (Toplevel.malformed range_pos msg, true)
6.5 end;
6.6
6.7 -fun prepare_atom commands init (cmd, proof, proper_proof) =
6.8 +fun prepare_element commands init {head, proof, proper_proof} =
6.9 let
6.10 - val (tr, proper_cmd) = prepare_span commands cmd |>> Toplevel.modify_init init;
6.11 + val (tr, proper_head) = prepare_span commands head |>> Toplevel.modify_init init;
6.12 val proof_trs = map (prepare_span commands) proof |> filter #2 |> map #1;
6.13 in
6.14 - if proper_cmd andalso proper_proof then [(tr, proof_trs)]
6.15 - else map (rpair []) (if proper_cmd then tr :: proof_trs else proof_trs)
6.16 + if proper_head andalso proper_proof then [(tr, proof_trs)]
6.17 + else map (rpair []) (if proper_head then tr :: proof_trs else proof_trs)
6.18 end;
6.19
6.20 fun prepare_command pos str =
6.21 @@ -278,14 +278,14 @@
6.22 val toks = Source.exhausted (Thy_Syntax.token_source lexs pos (Source.of_string text));
6.23 val spans = Source.exhaust (Thy_Syntax.span_source toks);
6.24 val _ = List.app Thy_Syntax.report_span spans; (* FIXME ?? *)
6.25 - val atoms = Source.exhaust (Thy_Syntax.atom_source (Source.of_list spans))
6.26 - |> Par_List.map_name "Outer_Syntax.prepare_atom" (prepare_atom commands init) |> flat;
6.27 + val elements = Source.exhaust (Thy_Syntax.element_source (Source.of_list spans))
6.28 + |> Par_List.map_name "Outer_Syntax.prepare_element" (prepare_element commands init) |> flat;
6.29
6.30 val _ = Present.theory_source name
6.31 (fn () => HTML.html_mode (implode o map Thy_Syntax.present_span) spans);
6.32
6.33 val _ = if time then writeln ("\n**** Starting theory " ^ quote name ^ " ****") else ();
6.34 - val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion atoms);
6.35 + val (results, thy) = cond_timeit time "" (fn () => Toplevel.excursion elements);
6.36 val _ = if time then writeln ("**** Finished theory " ^ quote name ^ " ****\n") else ();
6.37
6.38 val present =
7.1 --- a/src/Pure/Thy/thy_syntax.ML Fri Jul 01 17:44:04 2011 +0200
7.2 +++ b/src/Pure/Thy/thy_syntax.ML Fri Jul 01 18:11:17 2011 +0200
7.3 @@ -21,8 +21,9 @@
7.4 val parse_spans: Scan.lexicon * Scan.lexicon -> Position.T -> string -> span list
7.5 val present_span: span -> Output.output
7.6 val report_span: span -> unit
7.7 - val atom_source: (span, 'a) Source.source ->
7.8 - (span * span list * bool, (span, 'a) Source.source) Source.source
7.9 + type element = {head: span, proof: span list, proper_proof: bool}
7.10 + val element_source: (span, 'a) Source.source ->
7.11 + (element, (span, 'a) Source.source) Source.source
7.12 end;
7.13
7.14 structure Thy_Syntax: THY_SYNTAX =
7.15 @@ -159,7 +160,13 @@
7.16
7.17
7.18
7.19 -(** specification atoms: commands with optional proof **)
7.20 +(** specification elements: commands with optional proof **)
7.21 +
7.22 +type element = {head: span, proof: span list, proper_proof: bool};
7.23 +
7.24 +fun make_element head proof proper_proof =
7.25 + {head = head, proof = proof, proper_proof = proper_proof};
7.26 +
7.27
7.28 (* scanning spans *)
7.29
7.30 @@ -173,7 +180,7 @@
7.31 val stopper = Scan.stopper (K eof) is_eof;
7.32
7.33
7.34 -(* atom_source *)
7.35 +(* element_source *)
7.36
7.37 local
7.38
7.39 @@ -187,13 +194,14 @@
7.40 (if d = 0 then Scan.fail else command_with Keyword.is_qed >> pair (d - 1)) ||
7.41 Scan.unless (command_with Keyword.is_theory) (Scan.one not_eof) >> pair d)) -- Scan.state);
7.42
7.43 -val atom =
7.44 - command_with Keyword.is_theory_goal -- proof >> (fn (a, (bs, d)) => (a, bs, d >= 0)) ||
7.45 - Scan.one not_eof >> (fn a => (a, [], true));
7.46 +val element =
7.47 + command_with Keyword.is_theory_goal -- proof
7.48 + >> (fn (a, (bs, d)) => make_element a bs (d >= 0)) ||
7.49 + Scan.one not_eof >> (fn a => make_element a [] true);
7.50
7.51 in
7.52
7.53 -fun atom_source src = Source.source stopper (Scan.bulk atom) NONE src;
7.54 +fun element_source src = Source.source stopper (Scan.bulk element) NONE src;
7.55
7.56 end;
7.57
8.1 --- a/src/Pure/Tools/find_theorems.ML Fri Jul 01 17:44:04 2011 +0200
8.2 +++ b/src/Pure/Tools/find_theorems.ML Fri Jul 01 18:11:17 2011 +0200
8.3 @@ -101,6 +101,7 @@
8.4 end;
8.5
8.6
8.7 +
8.8 (** queries **)
8.9
8.10 type 'term query = {
8.11 @@ -154,6 +155,8 @@
8.12 end
8.13 | query_of_xml tree = raise XML_Syntax.XML ("query_of_xml: bad tree", tree);
8.14
8.15 +
8.16 +
8.17 (** theorems, either internal or external (without proof) **)
8.18
8.19 datatype theorem =
8.20 @@ -164,21 +167,21 @@
8.21 Position.markup pos o Markup.properties [("name", name), ("index", Markup.print_int i)]
8.22 | fact_ref_markup (Facts.Named ((name, pos), NONE)) =
8.23 Position.markup pos o Markup.properties [("name", name)]
8.24 - | fact_ref_markup fact_ref = raise Fail "bad fact ref"
8.25 + | fact_ref_markup fact_ref = raise Fail "bad fact ref";
8.26
8.27 fun xml_of_theorem (Internal _) = raise Fail "xml_of_theorem: Internal"
8.28 | xml_of_theorem (External (fact_ref, prop)) =
8.29 - XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop])
8.30 + XML.Elem (fact_ref_markup fact_ref ("External", []), [XML_Syntax.xml_of_term prop]);
8.31
8.32 fun theorem_of_xml (XML.Elem (("External", properties), [tree])) =
8.33 - let
8.34 - val name = the (Properties.get properties "name");
8.35 - val pos = Position.of_properties properties;
8.36 - val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
8.37 - (Properties.get properties "index");
8.38 - in
8.39 - External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
8.40 - end
8.41 + let
8.42 + val name = the (Properties.get properties "name");
8.43 + val pos = Position.of_properties properties;
8.44 + val intvs_opt = Option.map (single o Facts.Single o Markup.parse_int)
8.45 + (Properties.get properties "index");
8.46 + in
8.47 + External (Facts.Named ((name, pos), intvs_opt), XML_Syntax.term_of_xml tree)
8.48 + end
8.49 | theorem_of_xml tree = raise XML_Syntax.XML ("theorem_of_xml: bad tree", tree);
8.50
8.51 fun xml_of_result (opt_found, theorems) =
8.52 @@ -207,6 +210,8 @@
8.53 fun fact_ref_of (Internal (fact_ref, _)) = fact_ref
8.54 | fact_ref_of (External (fact_ref, _)) = fact_ref;
8.55
8.56 +
8.57 +
8.58 (** search criterion filters **)
8.59
8.60 (*generated filters are to be of the form
8.61 @@ -228,7 +233,7 @@
8.62
8.63 fun is_nontrivial thy = Term.is_Const o Term.head_of o Object_Logic.drop_judgment thy;
8.64
8.65 -(*educated guesses on HOL*) (* FIXME broken *)
8.66 +(*educated guesses on HOL*) (* FIXME utterly broken *)
8.67 val boolT = Type ("bool", []);
8.68 val iff_const = Const ("op =", boolT --> boolT --> boolT);
8.69
8.70 @@ -339,8 +344,8 @@
8.71 else (etacn thm THEN_ALL_NEW (Goal.norm_hhf_tac THEN' Method.assm_tac ctxt)) 1 goal;
8.72 in
8.73 fn Internal (_, thm) =>
8.74 - if is_some (Seq.pull (try_thm thm))
8.75 - then SOME (Thm.nprems_of thm, 0) else NONE
8.76 + if is_some (Seq.pull (try_thm thm))
8.77 + then SOME (Thm.nprems_of thm, 0) else NONE
8.78 | External _ => NONE
8.79 end;
8.80
8.81 @@ -423,7 +428,6 @@
8.82 in app (opt_add r r', consts', fs) end;
8.83 in app end;
8.84
8.85 -
8.86 in
8.87
8.88 fun filter_criterion ctxt opt_goal (b, c) =
8.89 @@ -520,8 +524,6 @@
8.90 in
8.91 maps Facts.selections
8.92 (visible_facts (Global_Theory.facts_of (Proof_Context.theory_of ctxt)) @
8.93 -
8.94 -
8.95 visible_facts (Proof_Context.facts_of ctxt))
8.96 end;
8.97
9.1 --- a/src/Tools/Code/code_runtime.ML Fri Jul 01 17:44:04 2011 +0200
9.2 +++ b/src/Tools/Code/code_runtime.ML Fri Jul 01 18:11:17 2011 +0200
9.3 @@ -163,7 +163,7 @@
9.4 end;
9.5
9.6 val (_, raw_check_holds_oracle) = Context.>>> (Context.map_theory_result
9.7 - (Thm.add_oracle (Binding.name "holds_by_evaluation",
9.8 + (Thm.add_oracle (@{binding holds_by_evaluation},
9.9 fn (thy, evaluator, vs_t, deps, ct) => check_holds thy evaluator vs_t deps ct)));
9.10
9.11 fun check_holds_oracle thy evaluator ((_, vs_ty), t) deps ct =
9.12 @@ -338,7 +338,7 @@
9.13
9.14 val _ =
9.15 Context.>> (Context.map_theory
9.16 - (ML_Context.add_antiq (Binding.name "code") (fn _ => Args.term >> ml_code_antiq)));
9.17 + (ML_Context.add_antiq @{binding code} (fn _ => Args.term >> ml_code_antiq)));
9.18
9.19 local
9.20
10.1 --- a/src/Tools/Code/code_simp.ML Fri Jul 01 17:44:04 2011 +0200
10.2 +++ b/src/Tools/Code/code_simp.ML Fri Jul 01 18:11:17 2011 +0200
10.3 @@ -58,9 +58,10 @@
10.4
10.5 fun dynamic_value thy = snd o Logic.dest_equals o Thm.prop_of o dynamic_conv thy o Thm.cterm_of thy;
10.6
10.7 -val setup = Method.setup (Binding.name "code_simp")
10.8 - (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
10.9 - "simplification with code equations"
10.10 +val setup =
10.11 + Method.setup @{binding code_simp}
10.12 + (Scan.succeed (SIMPLE_METHOD' o (CHANGED_PROP oo dynamic_tac o Proof_Context.theory_of)))
10.13 + "simplification with code equations"
10.14 #> Value.add_evaluator ("simp", dynamic_value o Proof_Context.theory_of);
10.15
10.16
11.1 --- a/src/Tools/nbe.ML Fri Jul 01 17:44:04 2011 +0200
11.2 +++ b/src/Tools/nbe.ML Fri Jul 01 18:11:17 2011 +0200
11.3 @@ -78,7 +78,7 @@
11.4 val get_triv_classes = map fst o Triv_Class_Data.get;
11.5
11.6 val (_, triv_of_class) = Context.>>> (Context.map_theory_result
11.7 - (Thm.add_oracle (Binding.name "triv_of_class", fn (thy, T, class) =>
11.8 + (Thm.add_oracle (@{binding triv_of_class}, fn (thy, T, class) =>
11.9 Thm.cterm_of thy (Logic.mk_of_class (T, class)))));
11.10
11.11 in
11.12 @@ -589,7 +589,7 @@
11.13 in Thm.mk_binop eq lhs rhs end;
11.14
11.15 val (_, raw_oracle) = Context.>>> (Context.map_theory_result
11.16 - (Thm.add_oracle (Binding.name "normalization_by_evaluation",
11.17 + (Thm.add_oracle (@{binding normalization_by_evaluation},
11.18 fn (thy, program, nbe_program_idx_tab, vsp_ty_t, deps, ct) =>
11.19 mk_equals thy ct (eval_term thy program nbe_program_idx_tab vsp_ty_t deps))));
11.20
12.1 --- a/src/Tools/value.ML Fri Jul 01 17:44:04 2011 +0200
12.2 +++ b/src/Tools/value.ML Fri Jul 01 18:11:17 2011 +0200
12.3 @@ -69,7 +69,7 @@
12.4 (value_cmd some_name modes t)));
12.5
12.6 val antiq_setup =
12.7 - Thy_Output.antiquotation (Binding.name "value")
12.8 + Thy_Output.antiquotation @{binding value}
12.9 (Scan.lift opt_evaluator -- Term_Style.parse -- Args.term)
12.10 (fn {source, context, ...} => fn ((some_name, style), t) => Thy_Output.output context
12.11 (Thy_Output.maybe_pretty_source Thy_Output.pretty_term context source