From 98565b837c56aefd30c2e80d1421928bb894a509 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 11 Dec 2018 16:03:01 +0100 Subject: [PATCH] Worked on assert*. Still needs debugging. Regression tests of some examples; necessary revisions due to stronger checks at close_monitor. --- Assert.thy | 67 ++++--- Isa_COL.thy | 19 +- Isa_DOF.thy | 57 +++--- examples/conceptual/Attributes.thy | 8 +- .../conceptual/Concept_ExampleInvariant.thy | 4 +- .../2018_cicm/IsaDofApplications.thy | 6 +- .../IsaDof_Manual/IsaDofManual.thy | 2 + .../MyCommentedIsabelle.thy | 188 +++++++++--------- ontologies/scholarly_paper.thy | 8 +- ontologies/technical_report.thy | 2 +- test/simple/Example.thy | 97 ++++----- 11 files changed, 256 insertions(+), 202 deletions(-) diff --git a/Assert.thy b/Assert.thy index b4e9953..93b7df0 100644 --- a/Assert.thy +++ b/Assert.thy @@ -1,4 +1,6 @@ -(* Little theory implementing the an assertion command in Isabelle/HOL. *) +section \ Little theory implementing the an assertion command in Isabelle/HOL. \ +text\This command is useful for certification documents allowing to validate + corner-cases of (executable) definitions. \ theory Assert imports Main @@ -6,34 +8,16 @@ theory Assert begin +subsection\Core\ -ML{* - +ML\ +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 +\ - -(* Test: - + + +subsection\ Test: \ +(* assert "" assert "3 = 4" assert "False" - assert "5 * 5 = 25 " - + assert "5 * 5 = 25" *) - + +subsection\Example\ + assert "True \ True " assert "(5::int) * 5 = 25 " - end \ No newline at end of file diff --git a/Isa_COL.thy b/Isa_COL.thy index ef7a2a8..65b813a 100644 --- a/Isa_COL.thy +++ b/Isa_COL.thy @@ -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 "\figure\\<^sup>+" @@ -46,6 +46,23 @@ doc_class figure_group = +section\Some attempt to model standardized links to Standard Isabelle Formal Content\ + +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 "\formal_item\\<^sup>+" + + + section\Tests\ diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 6c69655..3c10d63 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -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 \ 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 *) \ - +ML\find_index\ section\ Testing and Validation \ -(* 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\ writeln (DOF_core.toStringDocItemCommand "section" "scholarly_paper.introduction" []); diff --git a/examples/conceptual/Attributes.thy b/examples/conceptual/Attributes.thy index 2864471..e0d5629 100644 --- a/examples/conceptual/Attributes.thy +++ b/examples/conceptual/Attributes.thy @@ -122,13 +122,17 @@ figure*[fig_B::figure, close_monitor*[figs1] text\Resulting trace of figs1 as ML antiquotation: \ -ML\@{trace_attribute figs1}\ -text\ Resulting trace of figs as text antiquotation:\ +ML \@{trace_attribute figs1}\ +text\Resulting trace of figs as text antiquotation:\ text\@{trace_attribute figs1}\ text\Final Status:\ print_doc_items print_doc_classes +(*quatsch so far *) +text*[aa::figure]\dfg\ +assert*[aa] "True" + end \ No newline at end of file diff --git a/examples/conceptual/Concept_ExampleInvariant.thy b/examples/conceptual/Concept_ExampleInvariant.thy index 59980f9..c58a1db 100644 --- a/examples/conceptual/Concept_ExampleInvariant.thy +++ b/examples/conceptual/Concept_ExampleInvariant.thy @@ -29,7 +29,7 @@ subsection*[b::A, x = "5"] \ Lorem ipsum dolor sit amet, ... \ text\Setting a sample invariant, referring to attribute value "x":\ ML\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 \ @@ -62,7 +62,7 @@ to take sub-classing into account: \ ML\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 diff --git a/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy b/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy index 8424264..e3f80a0 100644 --- a/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy +++ b/examples/scholarly_paper/2018_cicm/IsaDofApplications.thy @@ -735,12 +735,10 @@ text\ 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 d’Avenir''.\ (*<*) +section*[bib::bibliography]\References\ + close_monitor*[this] -text\Resulting trace in doc\_item ''this'': \ -ML\@{trace_attribute this}\ - - end (*>*) diff --git a/examples/technical_report/IsaDof_Manual/IsaDofManual.thy b/examples/technical_report/IsaDof_Manual/IsaDofManual.thy index d6e82c7..4faaec9 100644 --- a/examples/technical_report/IsaDof_Manual/IsaDofManual.thy +++ b/examples/technical_report/IsaDof_Manual/IsaDofManual.thy @@ -4,6 +4,8 @@ theory IsaDofManual begin (*<*) +text*[bib::bibliography]\TODO\ + close_monitor*[this] text\Resulting trace in doc\_item ''this'': \ diff --git a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy index cbe7d76..626b74d 100644 --- a/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy +++ b/examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy @@ -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. \ +chapter*[intro::introduction]\ Introduction \ -chapter{* SML and Fundamental SML libraries *} +chapter*[t1::technical]\ SML and Fundamental SML libraries \ -section "ML, Text and Antiquotations" +section*[t11::technical] "ML, Text and Antiquotations" text\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). \ -section "Elements of the SML library"; +section*[t12::technical] "Elements of the SML library"; text\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 \ text\... where \<^verbatim>\key\ is usually just a synonym for string.\ -chapter {* Prover Architecture *} +chapter*[t2::technical] \ Prover Architecture \ -section {* The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts *} +section*[t21::technical] \ The Nano-Kernel: Contexts, (Theory)-Contexts, (Proof)-Contexts \ text\ 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. \ -subsection\ Mechanism 1 : Core Interface. \ +subsection*[t212::technical]\ Mechanism 1 : Core Interface. \ text\To be found in @{file "$ISABELLE_HOME/src/Pure/context.ML"}:\ -ML{* +ML\ 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; -*} +\ text\ML structure @{ML_structure Proof_Context}:\ @@ -281,9 +282,9 @@ ML\ \ -subsection\Mechanism 2 : global arbitrary data structure that is attached to the global and +subsection*[t213::example]\Mechanism 2 : global arbitrary data structure that is attached to the global and local Isabelle context $\theta$ \ -ML {* +ML \ 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 ... *) -*} +\ section\ The LCF-Kernel: terms, types, theories, proof\_contexts, thms \ @@ -318,9 +319,9 @@ text\The classical LCF-style \<^emph>\kernel\ is about \ -subsection{* Terms and Types *} +subsection\ Terms and Types \ text \A basic data-structure of the kernel is @{file "$ISABELLE_HOME/src/Pure/term.ML"} \ -ML{* open Term; +ML\ open Term; signature TERM' = sig (* ... *) type indexname = string * int @@ -342,7 +343,7 @@ signature TERM' = sig exception TERM of string * term list (* ... *) end -*} +\ text\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\ Type-Certification (=checking that a type annotation is consistent) \ -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\ 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{* Term.dummyT : typ *} +ML\ Term.dummyT : typ \ -ML{* +ML\ 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{* +\ +text\ @{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. \ text\Note that @{emph \polymorphic variables\} 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; \ -text{* Type generalization --- the conversion between free type variables and schematic +text\ 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:\ ML\ 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) \ -subsection{* Type-Inference (= inferring consistent type information if possible) *} +subsection\ Type-Inference (= inferring consistent type information if possible) \ -text{* Type inference eliminates also joker-types such as @{ML dummyT} and produces +text\ 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. \ +ML\ Type_Infer_Context.infer_types: Proof.context -> term list -> term list -*} +\ -subsection{* thy and the signature interface*} +subsection\ thy and the signature interface\ ML\ Sign.tsig_of: theory -> Type.tsig; Sign.syn_of : theory -> Syntax.syntax; Sign.of_sort : theory -> typ * sort -> bool ; \ -subsection{* Thm's and the LCF-Style, "Mikro"-Kernel *} +subsection\ Thm's and the LCF-Style, "Mikro"-Kernel \ text\ 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\ \ -subsection{* Theories *} +subsection\ Theories \ text \ 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. \ -ML{* +ML\ (* 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; -*} +\ section\Backward Proofs: Tactics, Tacticals and Goal-States\ @@ -801,7 +802,7 @@ Goal.prove_global : theory -> string list -> term list -> term -> section\The Isar Engine\ -ML{* +ML\ 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 #> *) -*} +\ -ML{* +ML\ 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; *) -*} +\ -ML{* Thy_Output.document_command {markdown = true} *} +ML\ Thy_Output.document_command {markdown = true} \ (* Structures related to LaTeX Generation *) -ML{* Latex.output_ascii; +ML\ Latex.output_ascii; Latex.output_token (* Hm, generierter output for @@ -867,9 +868,9 @@ Generierter output for: text\\label{sec:Shaft-Encoder-characteristics}\ -ML{* +ML\ 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 *} +\ +ML\ Type_Infer_Context.infer_types \ +ML\ Type_Infer_Context.prepare_positions \ -subsection {*Transaction Management in the Isar-Engine : The Toplevel *} +subsection \Transaction Management in the Isar-Engine : The Toplevel \ -ML{* +ML\ 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 *) -*} +\ -ML{* +ML\ (* 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 *) -*} +\ subsection\ Configuration flags of fixed type in the Isar-engine. \ -ML{* +ML\ 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{" "}"); *) -*} +\ chapter\Front End \ text\Introduction ... TODO\ @@ -1087,15 +1088,15 @@ ML\ fun dark_matter x = XML.content_of (YXML.parse_body x)\ (* MORE TO COME *) -section{* Parsing issues *} +section\ Parsing issues \ text\ 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+. \ -ML{* open Token*} +ML\ open Token\ -ML{* +ML\ (* 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. *) -*} +\ -text{* Tokens and Bindings *} +text\ Tokens and Bindings \ -ML{* +ML\ val H = @{binding here}; (* There are "bindings" consisting of a text-span and a position, where \positions\ are absolute references to a file *) @@ -1130,10 +1131,10 @@ Position.here: Position.T -> string; (* Bindings *) ML\val X = @{here};\ -*} +\ -subsection {*Input streams. *} -ML{* +subsection \Input streams. \ +ML\ 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})] - *)*} + *)\ -subsection {*Scanning and combinator parsing. *} +subsection \Scanning and combinator parsing. \ text\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); \ -text{* "parsers" are actually interpreters; an 'a parser is a function that parses +text\ "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. -*} +\ -text{* Syntax operations : Interface for parsing, type-checking, "reading" +text\ 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}. -*} +\ ML\ Parse.nat: int parser; @@ -1198,7 +1199,7 @@ Parse.position: 'a parser -> ('a * Position.T) parser; Parse.position Args.cartouche_input; \ -text{* Inner Syntax Parsing combinators for elementary Isabelle Lexems*} +text\ Inner Syntax Parsing combinators for elementary Isabelle Lexems\ ML\ 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; \ -ML{* +ML\ fun read_terms ctxt = grouped 10 Par_List.map_independent (Syntax.parse_term ctxt) #> Syntax.check_terms ctxt; -*} +\ ML\ (* More High-level, more Isar-specific Parsers *) @@ -1263,11 +1264,11 @@ ML\Sign.add_trrules\ section\ The PIDE Framework \ subsection\ Markup \ -text{* Markup Operations, and reporting. Diag in Isa\_DOF Foundations TR. +text\ 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, ... \ +ML\ (* 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) = *) -*} +\ -section {* Output: Very Low Level *} +section \ Output: Very Low Level \ ML\ Output.output; (* output is the structure for the "hooks" with the target devices. *) Output.output "bla_1:"; \ -section {* Output: LaTeX *} +section \ Output: LaTeX \ ML\ Thy_Output.verbatim_text; @@ -1396,14 +1397,14 @@ Thy_Output.output : Proof.context -> Pretty.T list -> string; -ML{* +ML\ Syntax_Phases.reports_of_scope; -*} +\ (* Pretty.T, pretty-operations. *) -ML{* +ML\ (* interesting piece for LaTeX Generation: fun verbatim_text ctxt = @@ -1456,9 +1457,9 @@ fun pretty_command (cmd as (name, Command {comment, ...})) = *) -*} +\ -ML{* +ML\ Thy_Output.output_text; (* is: fun output_text state {markdown} source = @@ -1505,10 +1506,10 @@ fun output_text state {markdown} source = end; *) -*} +\ -ML{* +ML\ 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; -*} +\ -text{* Even the parsers and type checkers stemming from the theory-structure are registered via +text\ 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: -*} +\ (* @@ -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\ Thus, Syntax\_Phases does the actual work, including + markup generation and generation of reports. Look at: \ (* fun check_typs ctxt raw_tys = let @@ -1600,4 +1600,12 @@ As one can see, check-routines internally generate the markup. *) +section*[c::conclusion]\Conclusion\ +text\More to come\ +section*[bib::bibliography]\Bibliography\ + +(*<*) +close_monitor*[this] +check_doc_global +(*>*) end diff --git a/ontologies/scholarly_paper.thy b/ontologies/scholarly_paper.thy index ed95253..e634dca 100644 --- a/ontologies/scholarly_paper.thy +++ b/ontologies/scholarly_paper.thy @@ -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\ Besides subtyping, there is another relation between doc_classes: a class can be a \<^emph>\monitor\ to other ones, diff --git a/ontologies/technical_report.thy b/ontologies/technical_report.thy index 51db48b..25256f3 100644 --- a/ontologies/technical_report.thy +++ b/ontologies/technical_report.thy @@ -29,7 +29,7 @@ doc_class report = \introduction\\<^sup>+ ~~ \technical || example\\<^sup>+ ~~ \conclusion\\<^sup>+ ~~ - \index\\<^sup>+ ~~ + \index\\<^sup>* ~~ bibliography)" ML\ diff --git a/test/simple/Example.thy b/test/simple/Example.thy index 583bb5e..47106ee 100644 --- a/test/simple/Example.thy +++ b/test/simple/Example.thy @@ -3,14 +3,14 @@ theory Example keywords "Term" :: diag begin -section{* Some show-off's of general antiquotations. *} +section\ Some show-off's of general antiquotations : for demos. \ (* some show-off of standard anti-quotations: *) print_attributes print_antiquotations -text{* @{thm refl} of name @{thm [source] refl} +text\ @{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"} \ -section{* Example *} +section\ Example \ -text*[ass1::assumption] {* Brexit means Brexit *} +text*[ass1::assumption] \ Brexit means Brexit \ -text*[hyp1::hypothesis] {* P means not P *} +text*[hyp1::hypothesis] \ P means not P \ -text*[ass122::srac] {* The overall sampling frequence of the odometer +text*[ass122::srac] \ The overall sampling frequence of the odometer subsystem is therefore 14 khz, which includes sampling, computing and -result communication times... *} +result communication times... \ -text*[t10::test_result] {* This is a meta-test. This could be an ML-command +text*[t10::test_result] \ 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 \ text \ As established by @{docref (unchecked) \t10\}, @@ -46,73 +46,74 @@ text \ safety related applicability condition @{srac \ass122\ exported constraint @{ec \ass122\}. \ -text{* +text\ And some ontologically inconsistent reference: @{hypothesis \ass1\} as well as -*} +\ -- "very wrong" -text{* +text\ And some ontologically inconsistent reference: @{assumption \hyp1\} as well as -*} +\ -- "very wrong" -text{* +text\ And some ontologically inconsistent reference: @{test_result \ass122\} as well as -*} +\ -- wrong -text{* +text\ And some other ontologically inconsistent reference: @{ec \t10\} as well as -*} +\ -- wrong -section{* Some Tests for Ontology Framework and its CENELEC Instance *} +section\ Some Tests for Ontology Framework and its CENELEC Instance \ 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]\ just a paragraph \ paragraph* [sdfk] \ just a paragraph - lexical variant \ -subsection*[sdf]{* shouldn't work, multiple ref. *} +subsection*[sdf]\ shouldn't work, multiple ref. \ +-- wrong section*[sedf::requirement, long_name = "None::string option"] - {* works again. One can hover over the class constraint and - jump to its definition. *} -text\\label{sedf}\ (* Hack to make the LaTeX-ing running. Should disappear. *) + \ works again. One can hover over the class constraint and jump to its definition. \ -section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with undefined attributes. *} +section*[seedf::test_case, dfg=34,fgdfg=zf]\ and another example with undefined attributes. \ +-- wrong -section{* Text Antiquotation Infrastructure ... *} +section\ Text Antiquotation Infrastructure ... \ -text{* @{docref \lalala\} -- produces warning. *} -text{* @{docref (unchecked) \lalala\} -- produces no warning. *} +text\ @{docref \lalala\} -- produces warning. \ +text\ @{docref (unchecked) \lalala\} -- produces no warning. \ -text{* @{docref \ass122\} -- global reference to a text-item in another file. *} +text\ @{docref \ass122\} -- global reference to a text-item in another file. \ -text{* @{ec \ass122\} -- global reference to a exported constraint in another file. +text\ @{ec \ass122\} -- 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". \ -text{* @{test_specification \ass122\} -- wrong: "reference ontologically inconsistent". *} +text\ @{test_specification \ass122\} -- wrong: "reference ontologically inconsistent". \ -text{* Here is a reference to @{docref \sedf\} *} +text\ Here is a reference to @{docref \sedf\} \ (* 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 \sedf\} *} -section{* A Small Example for a Command Definition --- just to see how this works in principle. *} +section\ A Small Example for Isar-support of a Command Definition --- for demos. \ -ML{* -val opt_modes = - Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []; +ML\ -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 +\ 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)\ sdfsdf \ (* undocumented trouvaille when analysing the code *) end