Worked on assert*.

Still needs debugging.
Regression tests of some examples;
necessary revisions due to stronger
checks at close_monitor.
This commit is contained in:
Burkhart Wolff 2018-12-11 16:03:01 +01:00
parent 40c12801c6
commit 98565b837c
11 changed files with 256 additions and 202 deletions

View File

@ -1,4 +1,6 @@
(* Little theory implementing the an assertion command in Isabelle/HOL. *)
section \<open> Little theory implementing the an assertion command in Isabelle/HOL. \<close>
text\<open>This command is useful for certification documents allowing to validate
corner-cases of (executable) definitions. \<close>
theory Assert
imports Main
@ -6,34 +8,16 @@ theory Assert
begin
subsection\<open>Core\<close>
ML{*
ML\<open>
local
(* Reimplementation needed because not exported from ML structure Value_Command *)
fun value_maybe_select some_name =
case some_name
of NONE => Value_Command.value
| SOME name => Value_Command.value_select name;
(* Reimplementation structure Value_Command due to tiny modification of value_cmd. *)
fun assert_cmd some_name modes raw_t state =
let
val ctxt = Toplevel.context_of state;
val t = Syntax.read_term ctxt raw_t;
val t' = value_maybe_select some_name ctxt t;
val ty' = Term.type_of t';
val ty' = case ty' of @{typ "bool"} => ty' | _ => error "Assertion expressions must be boolean.";
val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed.";
val ctxt' = Variable.auto_fixes t' ctxt;
val p = Print_Mode.with_modes modes (fn () =>
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;
*}
ML{*
in
(* Reimplementation needed because not exported from ML structure Value_Command *)
val opt_modes =
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
@ -42,27 +26,44 @@ val opt_modes =
val opt_evaluator =
Scan.option (@{keyword "["} |-- Parse.name --| @{keyword "]"})
(* NEW *)
(* Reimplementation structure Value_Command due to tiny modification of value_cmd. *)
fun assert_cmd some_name modes raw_t ctxt (* state*) =
let
(* val ctxt = Toplevel.context_of state; *)
val t = Syntax.read_term ctxt raw_t;
val t' = value_maybe_select some_name ctxt t;
val ty' = Term.type_of t';
val ty' = case ty' of @{typ "bool"} => ty' | _ => error "Assertion expressions must be boolean.";
val t' = case t' of @{term "True"} => t' | _ => error "Assertion failed.";
val ctxt' = Variable.auto_fixes t' ctxt;
val p = Print_Mode.with_modes modes (fn () =>
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;
val _ =
Outer_Syntax.command @{command_keyword assert} "evaluate and print term"
(opt_evaluator -- opt_modes -- Parse.term
>> (fn ((some_name, modes), t) => Toplevel.keep (assert_cmd some_name modes t) ));
*}
>> (fn ((some_name, modes), t) =>
Toplevel.keep ( (assert_cmd some_name modes t) o Toplevel.context_of) ));
end
\<close>
(* Test:
subsection\<open> Test: \<close>
(*
assert ""
assert "3 = 4"
assert "False"
assert "5 * 5 = 25 "
assert "5 * 5 = 25"
*)
subsection\<open>Example\<close>
assert "True \<and> True "
assert "(5::int) * 5 = 25 "
end

View File

@ -34,7 +34,7 @@ doc_class side_by_side_figure = figure +
doc_class figure_group =
(* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *)
caption :: "string"
rejects figure_group (* this forbids recursive figure-groups not supported
rejects figure_group (* this forbids recursive figure-groups not supported
by the current LaTeX style-file. *)
accepts "\<lbrace>figure\<rbrace>\<^sup>+"
@ -46,6 +46,23 @@ doc_class figure_group =
section\<open>Some attempt to model standardized links to Standard Isabelle Formal Content\<close>
doc_class assertions =
properties :: "term list"
doc_class "thms" =
properties :: "thm list"
doc_class formal_item =
item :: "(assertions + thms)"
doc_class formal_content =
style :: "string option"
accepts "\<lbrace>formal_item\<rbrace>\<^sup>+"
section\<open>Tests\<close>

View File

@ -1077,7 +1077,7 @@ fun update_instance_command (((oid:string,pos),cid_pos),
fun enriched_document_command markdown level (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
xstring_opt:(xstring * Position.T) option),
toks:Input.source)
: Toplevel.transition -> Toplevel.transition =
: theory -> theory =
let
(* as side-effect, generates markup *)
fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy)
@ -1087,7 +1087,7 @@ fun enriched_document_command markdown level (((((oid,pos),cid_pos), doc_attrs)
| SOME(NONE) => (("level",@{here}),"None")::doc_attrs
| SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::doc_attrs
in
Toplevel.theory(create_and_check_docitem false oid pos cid_pos doc_attrs #> check_text)
(create_and_check_docitem false oid pos cid_pos doc_attrs #> check_text)
(* Thanks Frederic Tuong! ! ! *)
end;
@ -1110,7 +1110,7 @@ fun open_monitor_command ((((oid,pos),cid_pos), doc_attrs) : meta_args_t) =
in DOF_core.map_data_global(DOF_core.upd_monitor_tabs(Symtab.update(oid, info )))(thy)
end
in
Toplevel.theory(o_m_c oid pos cid_pos doc_attrs #> create_monitor_entry )
o_m_c oid pos cid_pos doc_attrs #> create_monitor_entry
end;
@ -1119,14 +1119,16 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
let val {monitor_tab,...} = DOF_core.get_data_global thy
fun check_if_final aS = let val i = find_index (not o RegExpInterface.final) aS
in if i >= 0
then error("monitor number "^ Int.toString i^" not in final state.")
then error("monitor number "^Int.toString i^" not in final state.")
else ()
end
val _ = case Symtab.lookup monitor_tab oid of
SOME {automatas,...} => check_if_final automatas
| NONE => error ("Not belonging to a monitor class: "^oid)
val delete_monitor_entry = DOF_core.map_data_global (DOF_core.upd_monitor_tabs (Symtab.delete oid))
val {cid=cid_long, ...} = the(DOF_core.get_object_global oid thy)
val {cid=cid_long, id, ...} = the(DOF_core.get_object_global oid thy)
val markup = docref_markup false oid id pos;
val _ = Context_Position.report (Proof_Context.init_global thy) pos markup;
val check_inv = (DOF_core.get_class_invariant cid_long thy oid) {is_monitor=true}
o Context.Theory
in thy |> update_instance_command args
@ -1138,59 +1140,59 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
val _ =
Outer_Syntax.command ("title*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false} NONE) ;
>> (Toplevel.theory o (enriched_document_command {markdown = false} NONE))) ;
val _ =
Outer_Syntax.command ("subtitle*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false} NONE);
>> (Toplevel.theory o (enriched_document_command {markdown = false} NONE)));
val _ =
Outer_Syntax.command ("chapter*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false} (SOME(SOME 0)));
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 0)))));
val _ =
Outer_Syntax.command ("section*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false} (SOME(SOME 1)));
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 1)))));
val _ =
Outer_Syntax.command ("subsection*", @{here}) "subsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false} (SOME(SOME 2)));
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 2)))));
val _ =
Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false} (SOME(SOME 3)));
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 3)))));
val _ =
Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false} (SOME(SOME 4)));
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 4)))));
val _ =
Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false} (SOME(SOME 5)));
>> (Toplevel.theory o (enriched_document_command {markdown = false} (SOME(SOME 5)))));
val _ =
Outer_Syntax.command ("figure*", @{here}) "figure"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false} NONE);
>> (Toplevel.theory o (enriched_document_command {markdown = false} NONE)));
val _ =
Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false} NONE);
>> (Toplevel.theory o (enriched_document_command {markdown = false} NONE)));
val _ =
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
(attributes -- Parse.opt_target -- Parse.document_source
>> enriched_document_command {markdown = true} (SOME NONE));
>> (Toplevel.theory o (enriched_document_command {markdown = true} (SOME NONE))));
val _ =
Outer_Syntax.command @{command_keyword "declare_reference*"}
@ -1201,7 +1203,7 @@ val _ =
val _ =
Outer_Syntax.command @{command_keyword "open_monitor*"}
"open a document reference monitor"
(attributes >> open_monitor_command);
(attributes >> (Toplevel.theory o open_monitor_command));
val _ =
Outer_Syntax.command @{command_keyword "close_monitor*"}
@ -1221,9 +1223,19 @@ val _ =
Outer_Syntax.command @{command_keyword "lemma*"}
"lemma" (attributes >> update_lemma_cmd);
(* dummy/fake so far: *)
fun assert_cmd' ((((((oid,pos),cid),doc_attrs),some_name:string option),modes : string list),t:string) =
(Toplevel.keep (assert_cmd some_name modes t))
fun assert_cmd'((((((oid,pos),cid_pos),doc_attrs),some_name:string option),modes : string list),
prop:string) =
let val doc_attrs' = map (fn ((lhs,pos),rhs) => (((lhs,pos),"="),rhs)) doc_attrs
(* missing : registrating t as property *)
fun mks thy = case DOF_core.get_object_global oid thy of
SOME _ => update_instance_command (((oid,pos),cid_pos),doc_attrs') thy
| NONE => create_and_check_docitem false oid pos cid_pos doc_attrs thy
val check = (assert_cmd some_name modes prop) o Proof_Context.init_global
in
(* Toplevel.keep (check o Toplevel.context_of) *)
Toplevel.theory (fn thy => (check thy; mks thy))
end
val _ =
Outer_Syntax.command @{command_keyword "assert*"}
"evaluate and print term"
@ -1514,7 +1526,6 @@ val tag_attr = (Binding.make("tag_attribute",@{here}), @{typ "int"},Mixfix.NoSyn
val trace_attr = ((Binding.make("trace",@{here}), "(doc_class rexp \<times> string) list",Mixfix.NoSyn),
SOME "[]"): ((binding * string * mixfix) * string option)
fun add_doc_class_cmd overloaded (raw_params, binding)
raw_parent raw_fieldsNdefaults reject_Atoms regexps thy =
let
@ -1577,11 +1588,11 @@ val _ =
end (* struct *)
\<close>
ML\<open>find_index\<close>
section\<open> Testing and Validation \<close>
(* the following test crashes the LaTeX generation - however, without the latter this output is
(* the f ollowing test crashes the LaTeX generation - however, without the latter this output is
instructive
ML\<open>
writeln (DOF_core.toStringDocItemCommand "section" "scholarly_paper.introduction" []);

View File

@ -122,13 +122,17 @@ figure*[fig_B::figure,
close_monitor*[figs1]
text\<open>Resulting trace of figs1 as ML antiquotation: \<close>
ML\<open>@{trace_attribute figs1}\<close>
text\<open> Resulting trace of figs as text antiquotation:\<close>
ML \<open>@{trace_attribute figs1}\<close>
text\<open>Resulting trace of figs as text antiquotation:\<close>
text\<open>@{trace_attribute figs1}\<close>
text\<open>Final Status:\<close>
print_doc_items
print_doc_classes
(*quatsch so far *)
text*[aa::figure]\<open>dfg\<close>
assert*[aa] "True"
end

View File

@ -29,7 +29,7 @@ subsection*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
ML\<open>fun check_A_invariant oid {is_monitor:bool} ctxt =
let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here} @{here}
let val term = AttributeAccess.compute_attr_access ctxt "x" oid @{here} @{here}
val (@{typ "int"},x_value) = HOLogic.dest_number term
in if x_value > 5 then error("class A invariant violation") else true end
\<close>
@ -62,7 +62,7 @@ to take sub-classing into account:
\<close>
ML\<open>fun check_M_invariant oid {is_monitor} ctxt =
let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here} @{here}
let val term = AttributeAccess.compute_attr_access ctxt "trace" oid @{here} @{here}
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
val string_pair_list = map conv (HOLogic.dest_list term)
val cid_list = map fst string_pair_list

View File

@ -735,12 +735,10 @@ text\<open> This work was partly supported by the framework of IRT SystemX, Par
and therefore granted with public funds within the scope of the Program ``Investissements dAvenir''.\<close>
(*<*)
section*[bib::bibliography]\<open>References\<close>
close_monitor*[this]
text\<open>Resulting trace in doc\_item ''this'': \<close>
ML\<open>@{trace_attribute this}\<close>
end
(*>*)

View File

@ -4,6 +4,8 @@ theory IsaDofManual
begin
(*<*)
text*[bib::bibliography]\<open>TODO\<close>
close_monitor*[this]
text\<open>Resulting trace in doc\_item ''this'': \<close>

View File

@ -36,11 +36,12 @@ Moreover, the textual parts have been enriched with a maximum of formal content
which makes this text re-checkable at each load and easier maintainable.
\<close>
chapter*[intro::introduction]\<open> Introduction \<close>
chapter{* SML and Fundamental SML libraries *}
chapter*[t1::technical]\<open> SML and Fundamental SML libraries \<close>
section "ML, Text and Antiquotations"
section*[t11::technical] "ML, Text and Antiquotations"
text\<open>Isabelle is written in SML, the "Standard Meta-Language", which is
is an impure functional programming language allowing, in principle, mutable variables and side-effects.
@ -146,7 +147,7 @@ figure*[architecture::figure,relative_width="100",src="''figures/isabelle-archit
the IDE (right-hand side). \<close>
section "Elements of the SML library";
section*[t12::technical] "Elements of the SML library";
text\<open>Elements of the @{file "$ISABELLE_HOME/src/Pure/General/basics.ML"} SML library
are basic exceptions. Note that exceptions should be catched individually, uncatched exceptions
except those generated by the specific "error" function are discouraged in Isabelle
@ -212,9 +213,9 @@ end
\<close>
text\<open>... where \<^verbatim>\<open>key\<close> is usually just a synonym for string.\<close>
chapter {* Prover Architecture *}
chapter*[t2::technical] \<open> Prover Architecture \<close>
section {* The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts *}
section*[t21::technical] \<open> The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts \<close>
text\<open> What I call the 'Nano-Kernel' in Isabelle can also be seen as an acyclic theory graph.
The meat of it can be found in the file @{file "$ISABELLE_HOME/src/Pure/context.ML"}.
@ -258,10 +259,10 @@ Contexts come with type user-defined data which is mutable through the entire li
a context.
\<close>
subsection\<open> Mechanism 1 : Core Interface. \<close>
subsection*[t212::technical]\<open> Mechanism 1 : Core Interface. \<close>
text\<open>To be found in @{file "$ISABELLE_HOME/src/Pure/context.ML"}:\<close>
ML{*
ML\<open>
Context.parents_of: theory -> theory list;
Context.ancestors_of: theory -> theory list;
Context.proper_subthy : theory * theory -> bool;
@ -270,7 +271,7 @@ Context.proof_of : Context.generic -> Proof.context;
Context.certificate_theory_id : Context.certificate -> Context.theory_id;
Context.theory_name : theory -> string;
Context.map_theory: (theory -> theory) -> Context.generic -> Context.generic;
*}
\<close>
text\<open>ML structure @{ML_structure Proof_Context}:\<close>
@ -281,9 +282,9 @@ ML\<open>
\<close>
subsection\<open>Mechanism 2 : global arbitrary data structure that is attached to the global and
subsection*[t213::example]\<open>Mechanism 2 : global arbitrary data structure that is attached to the global and
local Isabelle context $\theta$ \<close>
ML {*
ML \<open>
datatype X = mt
val init = mt;
@ -303,7 +304,7 @@ structure Data = Generic_Data
Data.put : Data.T -> Context.generic -> Context.generic;
Data.map : (Data.T -> Data.T) -> Context.generic -> Context.generic;
(* there are variants to do this on theories ... *)
*}
\<close>
section\<open> The LCF-Kernel: terms, types, theories, proof\_contexts, thms \<close>
@ -318,9 +319,9 @@ text\<open>The classical LCF-style \<^emph>\<open>kernel\<close> is about
\<close>
subsection{* Terms and Types *}
subsection\<open> Terms and Types \<close>
text \<open>A basic data-structure of the kernel is @{file "$ISABELLE_HOME/src/Pure/term.ML"} \<close>
ML{* open Term;
ML\<open> open Term;
signature TERM' = sig
(* ... *)
type indexname = string * int
@ -342,7 +343,7 @@ signature TERM' = sig
exception TERM of string * term list
(* ... *)
end
*}
\<close>
text\<open>This core-data structure of the Isabelle Kernel is accessible in the Isabelle/ML environment
and serves as basis for programmed extensions concerning syntax, type-checking, and advanced
@ -404,15 +405,15 @@ HOLogic.conjuncts: term -> term list;
subsection{* Type-Certification (=checking that a type annotation is consistent) *}
subsection\<open> Type-Certification (=checking that a type annotation is consistent) \<close>
ML{* Type.typ_instance: Type.tsig -> typ * typ -> bool (* raises TYPE_MATCH *) *}
text{* there is a joker type that can be added as place-holder during term construction.
Jokers can be eliminated by the type inference. *}
ML\<open> Type.typ_instance: Type.tsig -> typ * typ -> bool (* raises TYPE_MATCH *) \<close>
text\<open> there is a joker type that can be added as place-holder during term construction.
Jokers can be eliminated by the type inference. \<close>
ML{* Term.dummyT : typ *}
ML\<open> Term.dummyT : typ \<close>
ML{*
ML\<open>
Sign.typ_instance: theory -> typ * typ -> bool;
Sign.typ_match: theory -> typ * typ -> Type.tyenv -> Type.tyenv;
Sign.typ_unify: theory -> typ * typ -> Type.tyenv * int -> Type.tyenv * int;
@ -420,15 +421,15 @@ Sign.const_type: theory -> string -> typ option;
Sign.certify_term: theory -> term -> term * typ * int; (* core routine for CERTIFICATION of types*)
Sign.cert_term: theory -> term -> term; (* short-cut for the latter *)
Sign.tsig_of: theory -> Type.tsig (* projects the type signature *)
*}
text{*
\<close>
text\<open>
@{ML "Sign.typ_match"} etc. is actually an abstract wrapper on the structure
@{ML_structure "Type"}
which contains the heart of the type inference.
It also contains the type substitution type @{ML_type "Type.tyenv"} which is
is actually a type synonym for @{ML_type "(sort * typ) Vartab.table"}
which in itself is a synonym for @{ML_type "'a Symtab.table"}, so
possesses the usual @{ML "Symtab.empty"} and @{ML "Symtab.dest"} operations. *}
possesses the usual @{ML "Symtab.empty"} and @{ML "Symtab.dest"} operations. \<close>
text\<open>Note that @{emph \<open>polymorphic variables\<close>} are treated like constant symbols
in the type inference; thus, the following test, that one type is an instance of the
@ -458,10 +459,10 @@ val tyenv = Sign.typ_match ( @{theory})
val [(("'a", 0), (["HOL.type"], @{typ "int"}))] = Vartab.dest tyenv;
\<close>
text{* Type generalization --- the conversion between free type variables and schematic
text\<open> Type generalization --- the conversion between free type variables and schematic
type variables --- is apparently no longer part of the standard API (there is a slightly
more general replacement in @{ML "Term_Subst.generalizeT_same"}, however). Here is a way to
overcome this by a self-baked generalization function:*}
overcome this by a self-baked generalization function:\<close>
ML\<open>
val generalize_typ = Term.map_type_tfree (fn (str,sort)=> Term.TVar((str,0),sort));
@ -510,23 +511,23 @@ val t' = Term_Subst.map_types_same (Term_Subst.instantiateT S') (t)
val t'' = Term.map_types (Term_Subst.instantiateT S') (t)
\<close>
subsection{* Type-Inference (= inferring consistent type information if possible) *}
subsection\<open> Type-Inference (= inferring consistent type information if possible) \<close>
text{* Type inference eliminates also joker-types such as @{ML dummyT} and produces
text\<open> Type inference eliminates also joker-types such as @{ML dummyT} and produces
instances for schematic type variables where necessary. In the case of success,
it produces a certifiable term. *}
ML{*
it produces a certifiable term. \<close>
ML\<open>
Type_Infer_Context.infer_types: Proof.context -> term list -> term list
*}
\<close>
subsection{* thy and the signature interface*}
subsection\<open> thy and the signature interface\<close>
ML\<open>
Sign.tsig_of: theory -> Type.tsig;
Sign.syn_of : theory -> Syntax.syntax;
Sign.of_sort : theory -> typ * sort -> bool ;
\<close>
subsection{* Thm's and the LCF-Style, "Mikro"-Kernel *}
subsection\<open> Thm's and the LCF-Style, "Mikro"-Kernel \<close>
text\<open>
The basic constructors and operations on theorems@{file "$ISABELLE_HOME/src/Pure/thm.ML"},
a set of derived (Pure) inferences can be found in @{file "$ISABELLE_HOME/src/Pure/drule.ML"}.
@ -643,12 +644,12 @@ ML\<open>
\<close>
subsection{* Theories *}
subsection\<open> Theories \<close>
text \<open> This structure yields the datatype \verb*thy* which becomes the content of
\verb*Context.theory*. In a way, the LCF-Kernel registers itself into the Nano-Kernel,
which inspired me (bu) to this naming. \<close>
ML{*
ML\<open>
(* intern Theory.Thy;
@ -676,7 +677,7 @@ Theory.at_end: (theory -> theory option) -> theory -> theory;
Theory.begin_theory: string * Position.T -> theory list -> theory;
Theory.end_theory: theory -> theory;
*}
\<close>
section\<open>Backward Proofs: Tactics, Tacticals and Goal-States\<close>
@ -801,7 +802,7 @@ Goal.prove_global : theory -> string list -> term list -> term ->
section\<open>The Isar Engine\<close>
ML{*
ML\<open>
Toplevel.theory;
Toplevel.presentation_context_of; (* Toplevel is a kind of table with call-back functions *)
@ -821,9 +822,9 @@ Input.source_content;
(*
basic_entity @{binding const} (Args.const {proper = true, strict = false}) pretty_const #>
*)
*}
\<close>
ML{*
ML\<open>
Config.get @{context} Thy_Output.display;
Config.get @{context} Thy_Output.source;
Config.get @{context} Thy_Output.modes;
@ -840,12 +841,12 @@ fun document_command markdown (loc, txt) =
end;
*)
*}
\<close>
ML{* Thy_Output.document_command {markdown = true} *}
ML\<open> Thy_Output.document_command {markdown = true} \<close>
(* Structures related to LaTeX Generation *)
ML{* Latex.output_ascii;
ML\<open> Latex.output_ascii;
Latex.output_token
(* Hm, generierter output for
@ -867,9 +868,9 @@ Generierter output for: text\<open>\label{sec:Shaft-Encoder-characteristics}\<cl
*)
*}
\<close>
ML{*
ML\<open>
Thy_Output.maybe_pretty_source :
(Proof.context -> 'a -> Pretty.T) -> Proof.context -> Token.src -> 'a list -> Pretty.T list;
@ -888,15 +889,15 @@ fun document_antiq check_file ctxt (name, pos) =
|> enclose "\\isatt{" "}"
end;
*}
ML{* Type_Infer_Context.infer_types *}
ML{* Type_Infer_Context.prepare_positions *}
\<close>
ML\<open> Type_Infer_Context.infer_types \<close>
ML\<open> Type_Infer_Context.prepare_positions \<close>
subsection {*Transaction Management in the Isar-Engine : The Toplevel *}
subsection \<open>Transaction Management in the Isar-Engine : The Toplevel \<close>
ML{*
ML\<open>
Thy_Output.output_text: Toplevel.state -> {markdown: bool} -> Input.source -> string;
Thy_Output.document_command;
@ -970,10 +971,10 @@ Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> s
(* this is where antiquotation expansion happens : uses eval_antiquote *)
*}
\<close>
ML{*
ML\<open>
(* Isar Toplevel Steuerung *)
@ -1022,12 +1023,12 @@ Thy_Output.output_text : Toplevel.state -> {markdown: bool} -> Input.source -> s
(* this is where antiquotation expansion happens : uses eval_antiquote *)
*}
\<close>
subsection\<open> Configuration flags of fixed type in the Isar-engine. \<close>
ML{*
ML\<open>
Config.get @{context} Thy_Output.quotes;
Config.get @{context} Thy_Output.display;
@ -1050,7 +1051,7 @@ fun output ctxt prts =
613 #> space_implode "\\isasep\\isanewline%\n"
614 #> enclose "\\isa{" "}");
*)
*}
\<close>
chapter\<open>Front End \<close>
text\<open>Introduction ... TODO\<close>
@ -1087,15 +1088,15 @@ ML\<open> fun dark_matter x = XML.content_of (YXML.parse_body x)\<close>
(* MORE TO COME *)
section{* Parsing issues *}
section\<open> Parsing issues \<close>
text\<open> Parsing combinators represent the ground building blocks of both generic input engines
as well as the specific Isar framework. They are implemented in the structure \verb+Token+
providing core type \verb+Token.T+.
\<close>
ML{* open Token*}
ML\<open> open Token\<close>
ML{*
ML\<open>
(* Provided types : *)
(*
@ -1115,12 +1116,12 @@ val _ = Scan.lift Args.cartouche_input : Input.source context_parser;
Token.is_command;
Token.content_of; (* textueller kern eines Tokens. *)
*}
\<close>
text{* Tokens and Bindings *}
text\<open> Tokens and Bindings \<close>
ML{*
ML\<open>
val H = @{binding here}; (* There are "bindings" consisting of a text-span and a position,
where \<dieresis>positions\<dieresis> are absolute references to a file *)
@ -1130,10 +1131,10 @@ Position.here: Position.T -> string;
(* Bindings *)
ML\<open>val X = @{here};\<close>
*}
\<close>
subsection {*Input streams. *}
ML{*
subsection \<open>Input streams. \<close>
ML\<open>
Input.source_explode : Input.source -> Symbol_Pos.T list;
(* conclusion: Input.source_explode converts " f @{thm refl}"
into:
@ -1142,9 +1143,9 @@ ML{*
("h", {offset=20, id=-2769}), ("m", {offset=21, id=-2769}), (" ", {offset=22, id=-2769}),
("r", {offset=23, id=-2769}), ("e", {offset=24, id=-2769}), ("f", {offset=25, id=-2769}),
("l", {offset=26, id=-2769}), ("}", {offset=27, id=-2769})]
*)*}
*)\<close>
subsection {*Scanning and combinator parsing. *}
subsection \<open>Scanning and combinator parsing. \<close>
text\<open>Is used on two levels:
\<^enum> outer syntax, that is the syntax in which Isar-commands are written, and
\<^enum> inner-syntax, that is the syntax in which lambda-terms, and in particular HOL-terms were written.
@ -1163,7 +1164,7 @@ Scan.lift : ('a -> 'b * 'c) -> 'd * 'a -> 'b * ('d * 'c);
Scan.lift (Parse.position Args.cartouche_input);
\<close>
text{* "parsers" are actually interpreters; an 'a parser is a function that parses
text\<open> "parsers" are actually interpreters; an 'a parser is a function that parses
an input stream and computes(=evaluates, computes) it into 'a.
Since the semantics of an Isabelle command is a transition => transition
or theory $\Rightarrow$ theory function, i.e. a global system transition.
@ -1171,9 +1172,9 @@ text{* "parsers" are actually interpreters; an 'a parser is a function that par
to a table in the Toplevel-structure of Isar.
The type 'a parser is already defined in the structure Token.
*}
\<close>
text{* Syntax operations : Interface for parsing, type-checking, "reading"
text\<open> Syntax operations : Interface for parsing, type-checking, "reading"
(both) and pretty-printing.
Note that this is a late-binding interface, i.e. a collection of "hooks".
The real work is done ... see below.
@ -1181,7 +1182,7 @@ text{* Syntax operations : Interface for parsing, type-checking, "reading"
Encapsulates the data structure "syntax" --- the table with const symbols,
print and ast translations, ... The latter is accessible, e.g. from a Proof
context via @{ML Proof_Context.syn_of}.
*}
\<close>
ML\<open>
Parse.nat: int parser;
@ -1198,7 +1199,7 @@ Parse.position: 'a parser -> ('a * Position.T) parser;
Parse.position Args.cartouche_input;
\<close>
text{* Inner Syntax Parsing combinators for elementary Isabelle Lexems*}
text\<open> Inner Syntax Parsing combinators for elementary Isabelle Lexems\<close>
ML\<open>
Syntax.parse_sort : Proof.context -> string -> sort;
Syntax.parse_typ : Proof.context -> string -> typ;
@ -1239,10 +1240,10 @@ Syntax.string_of_typ: Proof.context -> typ -> string;
Syntax.lookup_const : Syntax.syntax -> string -> string option;
\<close>
ML{*
ML\<open>
fun read_terms ctxt =
grouped 10 Par_List.map_independent (Syntax.parse_term ctxt) #> Syntax.check_terms ctxt;
*}
\<close>
ML\<open>
(* More High-level, more Isar-specific Parsers *)
@ -1263,11 +1264,11 @@ ML\<open>Sign.add_trrules\<close>
section\<open> The PIDE Framework \<close>
subsection\<open> Markup \<close>
text{* Markup Operations, and reporting. Diag in Isa\_DOF Foundations TR.
text\<open> Markup Operations, and reporting. Diag in Isa\_DOF Foundations TR.
Markup operation send via side-effect annotations to the GUI (precisely:
to the PIDE Framework) that were used for hyperlinking applicating to binding
occurrences, info for hovering, ... *}
ML{*
occurrences, info for hovering, ... \<close>
ML\<open>
(* Position.report is also a type consisting of a pair of a position and markup. *)
(* It would solve all my problems if I find a way to infer the defining Position.report
@ -1368,17 +1369,17 @@ fun check ctxt (name, pos) =
*)
*}
\<close>
section {* Output: Very Low Level *}
section \<open> Output: Very Low Level \<close>
ML\<open>
Output.output; (* output is the structure for the "hooks" with the target devices. *)
Output.output "bla_1:";
\<close>
section {* Output: LaTeX *}
section \<open> Output: LaTeX \<close>
ML\<open>
Thy_Output.verbatim_text;
@ -1396,14 +1397,14 @@ Thy_Output.output : Proof.context -> Pretty.T list -> string;
ML{*
ML\<open>
Syntax_Phases.reports_of_scope;
*}
\<close>
(* Pretty.T, pretty-operations. *)
ML{*
ML\<open>
(* interesting piece for LaTeX Generation:
fun verbatim_text ctxt =
@ -1456,9 +1457,9 @@ fun pretty_command (cmd as (name, Command {comment, ...})) =
*)
*}
\<close>
ML{*
ML\<open>
Thy_Output.output_text;
(* is:
fun output_text state {markdown} source =
@ -1505,10 +1506,10 @@ fun output_text state {markdown} source =
end;
*)
*}
\<close>
ML{*
ML\<open>
Outer_Syntax.print_commands @{theory};
Outer_Syntax.command : Outer_Syntax.command_keyword -> string ->
@ -1527,14 +1528,14 @@ val _ =
(* not exported: Thy_Output.output_token; Ich glaub, da passierts ... *)
Thy_Output.present_thy;
*}
\<close>
text{* Even the parsers and type checkers stemming from the theory-structure are registered via
text\<open> Even the parsers and type checkers stemming from the theory-structure are registered via
hooks (this can be confusing at times). Main phases of inner syntax processing, with standard
implementations of parse/unparse operations were treated this way.
At the very very end in @{file "~~/src/Pure/Syntax/syntax_phases.ML"}, it sets up the entire syntax engine
(the hooks) via:
*}
\<close>
(*
@ -1555,9 +1556,8 @@ val _ =
uncheck_terms = uncheck_terms});
*)
text{* Thus, Syntax\_Phases does the actual work, including
markup generation and generation of reports.
Look at: *}
text\<open> Thus, Syntax\_Phases does the actual work, including
markup generation and generation of reports. Look at: \<close>
(*
fun check_typs ctxt raw_tys =
let
@ -1600,4 +1600,12 @@ As one can see, check-routines internally generate the markup.
*)
section*[c::conclusion]\<open>Conclusion\<close>
text\<open>More to come\<close>
section*[bib::bibliography]\<open>Bibliography\<close>
(*<*)
close_monitor*[this]
check_doc_global
(*>*)
end

View File

@ -55,8 +55,14 @@ doc_class "conclusion" = text_section +
doc_class related_work = "conclusion" +
main_author :: "author option" <= None
(* There is no consensus if this is a good classification *)
datatype formal_content_kind = "definition" | "axiom" | aux_lemma | "lemma" | "corrollary" | "theorem"
doc_class "thm_elements" = "thms" +
kind :: "formal_content_kind option"
doc_class bibliography =
style :: "string option" <= "Some ''LNCS''"
style :: "string option" <= "Some ''LNCS''"
text\<open> Besides subtyping, there is another relation between
doc_classes: a class can be a \<^emph>\<open>monitor\<close> to other ones,

View File

@ -29,7 +29,7 @@ doc_class report =
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
\<lbrace>index\<rbrace>\<^sup>+ ~~
\<lbrace>index\<rbrace>\<^sup>* ~~
bibliography)"
ML\<open>

View File

@ -3,14 +3,14 @@ theory Example
keywords "Term" :: diag
begin
section{* Some show-off's of general antiquotations. *}
section\<open> Some show-off's of general antiquotations : for demos. \<close>
(* some show-off of standard anti-quotations: *)
print_attributes
print_antiquotations
text{* @{thm refl} of name @{thm [source] refl}
text\<open> @{thm refl} of name @{thm [source] refl}
@{thm[mode=Rule] conjI}
@{file "../../Isa_DOF.thy"}
@{value "3+4::int"}
@ -18,23 +18,23 @@ text{* @{thm refl} of name @{thm [source] refl}
@{theory List}}
@{term "3"}
@{type bool}
@{term [show_types] "f x = a + x"} *}
@{term [show_types] "f x = a + x"} \<close>
section{* Example *}
section\<open> Example \<close>
text*[ass1::assumption] {* Brexit means Brexit *}
text*[ass1::assumption] \<open> Brexit means Brexit \<close>
text*[hyp1::hypothesis] {* P means not P *}
text*[hyp1::hypothesis] \<open> P means not P \<close>
text*[ass122::srac] {* The overall sampling frequence of the odometer
text*[ass122::srac] \<open> The overall sampling frequence of the odometer
subsystem is therefore 14 khz, which includes sampling, computing and
result communication times... *}
result communication times... \<close>
text*[t10::test_result] {* This is a meta-test. This could be an ML-command
text*[t10::test_result] \<open> This is a meta-test. This could be an ML-command
that governs the external test-execution via, eg., a makefile or specific calls
to a test-environment or test-engine *}
to a test-environment or test-engine \<close>
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
@ -46,73 +46,74 @@ text \<open> safety related applicability condition @{srac \<open>ass122\<close>
exported constraint @{ec \<open>ass122\<close>}.
\<close>
text{*
text\<open>
And some ontologically inconsistent reference:
@{hypothesis \<open>ass1\<close>} as well as
*}
\<close>
-- "very wrong"
text{*
text\<open>
And some ontologically inconsistent reference:
@{assumption \<open>hyp1\<close>} as well as
*}
\<close>
-- "very wrong"
text{*
text\<open>
And some ontologically inconsistent reference:
@{test_result \<open>ass122\<close>} as well as
*}
\<close>
-- wrong
text{*
text\<open>
And some other ontologically inconsistent reference:
@{ec \<open>t10\<close>} as well as
*}
\<close>
-- wrong
section{* Some Tests for Ontology Framework and its CENELEC Instance *}
section\<open> Some Tests for Ontology Framework and its CENELEC Instance \<close>
declare_reference* [lalala::requirement, alpha="main", beta=42]
declare_reference* [lalala::quod] (* shouldn't work *)
declare_reference* [lalala::quod] (* multiple declaration*)
-- wrong
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
paragraph*[sdf]{* just a paragraph *}
paragraph*[sdf]\<open> just a paragraph \<close>
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
subsection*[sdf]{* shouldn't work, multiple ref. *}
subsection*[sdf]\<open> shouldn't work, multiple ref. \<close>
-- wrong
section*[sedf::requirement, long_name = "None::string option"]
{* works again. One can hover over the class constraint and
jump to its definition. *}
text\<open>\label{sedf}\<close> (* Hack to make the LaTeX-ing running. Should disappear. *)
\<open> works again. One can hover over the class constraint and jump to its definition. \<close>
section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with undefined attributes. *}
section*[seedf::test_case, dfg=34,fgdfg=zf]\<open> and another example with undefined attributes. \<close>
-- wrong
section{* Text Antiquotation Infrastructure ... *}
section\<open> Text Antiquotation Infrastructure ... \<close>
text{* @{docref \<open>lalala\<close>} -- produces warning. *}
text{* @{docref (unchecked) \<open>lalala\<close>} -- produces no warning. *}
text\<open> @{docref \<open>lalala\<close>} -- produces warning. \<close>
text\<open> @{docref (unchecked) \<open>lalala\<close>} -- produces no warning. \<close>
text{* @{docref \<open>ass122\<close>} -- global reference to a text-item in another file. *}
text\<open> @{docref \<open>ass122\<close>} -- global reference to a text-item in another file. \<close>
text{* @{ec \<open>ass122\<close>} -- global reference to a exported constraint in another file.
text\<open> @{ec \<open>ass122\<close>} -- global reference to a exported constraint in another file.
Note that the link is actually a srac, which, according to
the ontology, happens to be an "ec". *}
the ontology, happens to be an "ec". \<close>
text{* @{test_specification \<open>ass122\<close>} -- wrong: "reference ontologically inconsistent". *}
text\<open> @{test_specification \<open>ass122\<close>} -- wrong: "reference ontologically inconsistent". \<close>
text{* Here is a reference to @{docref \<open>sedf\<close>} *}
text\<open> Here is a reference to @{docref \<open>sedf\<close>} \<close>
(* works currently only in connection with the above label-hack.
Try to hover over the sedf - link and activate it !!! *)
@ -128,25 +129,31 @@ text{* Here is a reference to @{docref \<open>sedf\<close>} *}
section{* A Small Example for a Command Definition --- just to see how this works in principle. *}
section\<open> A Small Example for Isar-support of a Command Definition --- for demos. \<close>
ML{*
val opt_modes =
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
ML\<open>
val _ =
Outer_Syntax.command @{command_keyword Term} "read and print term"
(opt_modes -- Parse.term >> Isar_Cmd.print_term);
*}
local
val opt_modes = Scan.optional (@{keyword "("}
|-- Parse.!!! (Scan.repeat1 Parse.name
--| @{keyword ")"})) [];
in
val _ =
Outer_Syntax.command @{command_keyword Term} "read and print term"
(opt_modes -- Parse.term >> Isar_Cmd.print_term);
end
\<close>
lemma "True" by simp
Term "a + b = b + a"
term "a + b = b + a"
section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *)
section(in order)\<open> sdfsdf \<close> (* undocumented trouvaille when analysing the code *)
end