From bf4c3d618e5c0b75ff17de32e4bb4c96ada1f59b Mon Sep 17 00:00:00 2001 From: Burkhart Wolff Date: Wed, 1 Mar 2023 20:47:28 +0100 Subject: [PATCH] ground for revision of tests: TestKit, Conceptual, Latex-tests --- .../Conceptual/Conceptual.thy | 82 +++- Isabelle_DOF-Unit-Tests/Attributes.thy | 12 +- Isabelle_DOF-Unit-Tests/Evaluation.thy | 6 +- Isabelle_DOF-Unit-Tests/Latex_Tests.thy | 435 ++++++++++++++++++ Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy | 136 +----- Isabelle_DOF-Unit-Tests/ROOT | 2 + Isabelle_DOF-Unit-Tests/TestKit.thy | 163 +++++++ 7 files changed, 692 insertions(+), 144 deletions(-) create mode 100644 Isabelle_DOF-Unit-Tests/Latex_Tests.thy create mode 100644 Isabelle_DOF-Unit-Tests/TestKit.thy diff --git a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy index bc2b81a8..87661a62 100644 --- a/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy +++ b/Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy @@ -20,12 +20,14 @@ imports "Isabelle_DOF.Isa_COL" begin +section\Excursion: On the semantic consequences of this definition: \ + +text\Consider the following document class definition and its consequences:\ doc_class A = level :: "int option" x :: int -section\Excursion: On the semantic consequences of this definition: \ text\This class definition leads an implicit Isabelle/HOL \<^theory_text>\record\ definition (cf. \<^url>\https://isabelle.in.tum.de/doc/isar-ref.pdf\, chapter 11.6.). @@ -49,23 +51,61 @@ Consequently, \<^theory_text>\doc_class\'es inherit the entire theo \<^enum> @{thm [display] A.simps(6)} \<^enum> ... \ -(* the generated theory of the \<^theory_text>\doc_class\ A can be inspected, of course, by *) + +text\The generated theory of the \<^theory_text>\doc_class\ A can be inspected, of course, by:\ find_theorems (60) name:Conceptual name:A +text\A more abstract view on the state of the DOF machine can be found here:\ + +print_doc_classes + +print_doc_items + +text\... and an ML-level output:\ + +ML\ +val docitem_tab = DOF_core.get_instances \<^context>; +val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>; +val docclass_tab = DOF_core.get_onto_classes \<^context>; + +\ + +ML\ +Name_Space.dest_table docitem_tab; +Name_Space.dest_table isa_transformer_tab; +Name_Space.dest_table docclass_tab; +\ +text\... or as ML assertion: \ +ML\ +@{assert} (Name_Space.dest_table docitem_tab = []); +fun match ("Conceptual.A", (* the long-name *) + DOF_core.Onto_Class {params, name, virtual,inherits_from=NONE, + attribute_decl, rejectS=[],rex=[], invs=[]}) + = (Binding.name_of name = "A") + | match _ = false; + +@{assert} (exists match (Name_Space.dest_table docclass_tab)) +\ text\As a consequence of the theory of the \<^theory_text>\doc_class\ \A\, the code-generator setup lets us evaluate statements such as: \ value\ the(A.level (A.make 3 (Some 4) 5)) = 4\ -text\And finally, as a consequence of the above semantic construction of \<^theory_text>\doc_class\'es, the internal +text\And further, as a consequence of the above semantic construction of \<^theory_text>\doc_class\'es, the internal \\\-calculus representation of class instances looks as follows:\ ML\ -val tt = @{term \the(A.level (A.make 3 (Some 4) 5))\} +@{term \the(A.level (A.make 3 (Some 4) 5))\}; +fun match (Const("Option.option.the",_) $ + (Const ("Conceptual.A.level",_) $ + (Const ("Conceptual.A.make", _) $ u $ v $ w))) = true + |match _ = false; +@{assert} (match @{term \the(A.level (A.make 3 (Some 4) 5))\}) \ -text\For the code-generation, we have the following access to values representing class instances:\ +text\And finally, via the code-generation, we have the following programmable + access to values representing class instances:\ ML\ val A_make = @{code A.make}; val zero = @{code "0::int"}; @@ -75,9 +115,9 @@ val add = @{code "(+) :: int \ int \ int"}; A_make zero (SOME one) (add one one) \ +section\Building up a conceptual class hierarchy:\ -section\An independent class-tree root: \ - +text\An independent class-tree root: \ doc_class B = level :: "int option" @@ -125,7 +165,7 @@ doc_class F = and br':: "r \ \ [] \ length(b' \) \ 3" and cr :: "properties \ \ []" -text\The effect of the invariant declaration is to provide intern definitions for validation +text\The effect of the invariant declaration is to provide intern HOL definitions for validation functions of this invariant. They can be referenced as follows:\ thm br_inv_def thm br'_inv_def @@ -133,7 +173,7 @@ thm cr_inv_def term "\F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\" -term "br' (\F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\) " +term "br'_inv (\F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\) " text\Now, we can use these definitions in order to generate code for these validation functions. Note, however, that not everything that we can write in an invariant (basically: HOL) is executable, @@ -141,7 +181,7 @@ or even compilable by the code generator setup:\ ML\ val cr_inv_code = @{code "cr_inv"} \ \ \works albeit thm is abstract ...\ text\while in :\ -(* ML\ val br_inv_code = @{code "br_inv"} \ \\this does not work ...\ *) +ML\ val br_inv_code = @{code "br_inv"} \ \\this does not work ...\ text\... the compilation fails due to the fact that nothing prevents the user to define an infinite relation between \<^typ>\A\ and \<^typ>\C\. However, the alternative @@ -151,21 +191,27 @@ ML\ val br'_inv_code = @{code "br'_inv"} \ \ \does w text\... is compilable ...\ - - doc_class G = C + - g :: "thm" <= "@{thm \HOL.refl\}" + g :: "thm" <= "@{thm \HOL.refl\}" (* warning overriding attribute expected*) doc_class M = ok :: "unit" accepts "A ~~ \C || D\\<^sup>* ~~ \F\" +text\The final class and item tables look like this:\ +print_doc_classes +print_doc_items + +ML\ +let val class_ids_so_far = ["Conceptual.A", "Conceptual.B", "Conceptual.C", "Conceptual.D", + "Conceptual.E", "Conceptual.F", "Conceptual.G", "Conceptual.M", + "Isa_COL.figure", "Isa_COL.chapter", "Isa_COL.figure2", "Isa_COL.section", + "Isa_COL.subsection", "Isa_COL.figure_group", "Isa_COL.text_element", + "Isa_COL.subsubsection", "Isa_COL.side_by_side_figure"] + val docclass_tab = map fst (Name_Space.dest_table (DOF_core.get_onto_classes \<^context>)); +in @{assert} (class_ids_so_far = docclass_tab) end\ + -(* -ML\ Document.state();\ -ML\ Outer_Syntax.command; \ -ML\ Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \ -*) open_monitor*[aaa::M] section*[test::A]\Test and Validation\ diff --git a/Isabelle_DOF-Unit-Tests/Attributes.thy b/Isabelle_DOF-Unit-Tests/Attributes.thy index 15275b3f..875f1a3f 100644 --- a/Isabelle_DOF-Unit-Tests/Attributes.thy +++ b/Isabelle_DOF-Unit-Tests/Attributes.thy @@ -17,8 +17,8 @@ theory "Isabelle_DOF-Unit-Tests_document" "Isabelle_DOF-Ontologies.Conceptual" begin - -section\Elementary Creation of Doc-items and Access of their Attibutes\ +ML\@{assert} (1 = 1)\ +section\Elementar Creation of Doc-items and Access of their Attibutes\ text\Current status:\ print_doc_classes @@ -29,9 +29,13 @@ ML\ val docitem_tab = DOF_core.get_instances \<^context> val isa_transformer_tab = DOF_core.get_isa_transformers \<^context> val docclass_tab = DOF_core.get_onto_classes @{context}; -Name_Space.dest_table docitem_tab; -Name_Space.dest_table docclass_tab; \ +ML\ +map fst (Name_Space.dest_table docitem_tab); +Name_Space.dest_table docclass_tab; + +\ + ML\ val (oid, DOF_core.Instance {value, ...}) = Name_Space.check (Context.Proof \<^context>) (DOF_core.get_instances \<^context>) ("aaa", Position.none) diff --git a/Isabelle_DOF-Unit-Tests/Evaluation.thy b/Isabelle_DOF-Unit-Tests/Evaluation.thy index b6742bc4..85421b6c 100644 --- a/Isabelle_DOF-Unit-Tests/Evaluation.thy +++ b/Isabelle_DOF-Unit-Tests/Evaluation.thy @@ -81,9 +81,9 @@ term*\@{A \xcv1\}\ text\The instance class @{docitem \xcv1\} is not an instance of the class @{doc_class B}: \ -(* Error: -term*\@{B \xcv1\}\*) - +(* Error: +term*\@{B \xcv1\}\ +*) text\We can evaluate the instance class. The current implementation returns the value of the instance, i.e. a collection of every attribute of the instance: \ diff --git a/Isabelle_DOF-Unit-Tests/Latex_Tests.thy b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy new file mode 100644 index 00000000..b83db275 --- /dev/null +++ b/Isabelle_DOF-Unit-Tests/Latex_Tests.thy @@ -0,0 +1,435 @@ +(************************************************************************* + * Copyright (C) + * 2019-2023 The University of Exeter + * 2018-2023 The University of Paris-Saclay + * 2018 The University of Sheffield + * + * License: + * This program can be redistributed and/or modified under the terms + * of the 2-clause BSD-style license. + * + * SPDX-License-Identifier: BSD-2-Clause + *************************************************************************) + +theory + Latex_Tests +imports + "Isabelle_DOF-Unit-Tests_document" + "TestKit" +keywords "Figure*" :: document_body (* still experimental feature *) + +begin + +section\Elementary Creation of Doc-items and Access of their Attibutes\ + + +text\Output status:\ +print_doc_classes +print_doc_items + + +text\And here a tex - text macro.\ +text\Pythons ReStructuredText (RST). + @{url \https://de.wikipedia.org/wiki/ReStructuredText\}. Tool: Sphinx. + \ + +text*[aaaa::B]\dfg @{thm [display] refl}\ + +text-[dfgdfg::B] +\ Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ + +text-latex\ Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ + +text-[asd::B] +\... and here is its application macro expansion: + @{B [display] "dfgdfg"} + \textbf{TEST} + @{cartouche [display] + \text*[dfgdfg::B] + \ Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ + \} +\ + +text-latex\... and here is its application macro expansion: + @{B [display] "dfgdfg"} + \textbf{TEST} + @{cartouche [display] + \text*[dfgdfg::B] + \ Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ + \}\ + +(*<*) +text-latex\ \<^theory_text>\definition df = ... + \ + @{ML [display] \ let val x = 3 + 4 in true end + \} + + @{ML_text [display] \ val x = ... + \} + + @{verbatim [display] \ Lorem ipsum ... @{thm refl} + Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \} + @{theory_text [display] \definition df = ... \x. + \} + @{cartouche [display] \ @{figure "cfgdfg"}\} \ + +(*>*) +text\Final Status:\ +print_doc_items +print_doc_classes + +section\Experiments on Inline-Textelements\ +text\Std Abbreviations. Inspired by the block *\control spacing\ + in @{file \$ISABELLE_HOME/src/Pure/Thy/document_antiquotations.ML\}. + We mechanize the table-construction and even attach the LaTeX + quirks to be dumped into the prelude. \ + +ML\ +val _ = + Theory.setup + ( Document_Output.antiquotation_raw \<^binding>\doof\ (Scan.succeed ()) + (fn _ => fn () => Latex.string "\\emph{doof}") + #> Document_Output.antiquotation_raw \<^binding>\LATEX\ (Scan.succeed ()) + (fn _ => fn () => Latex.string "\\textbf{LaTeX}") + ) +\ + +text-latex\ \<^doof> \<^LATEX> \ + +(* the same effect is achieved with : *) +setup \DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\ +(* Note that this assumes that the generated LaTeX macro call "\blabla" is defined somewhere in the + target document, for example, in the tex prelude. Note that the "Binding.make" can be avoided + using the alternative \<^binding> notation (see above).*) + + +setup\DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" (K(K()))\ + +(*<*) +text-latex\ \<^blong>\asd\ outer \<^blong>\syntax| ! see {syntax, outer}\ \ +(*>*) + +ML\ + +fun report_text ctxt text = + let val pos = Input.pos_of text in + Context_Position.reports ctxt + [(pos, Markup.language_text (Input.is_delimited text)), + (pos, Markup.raw_text)] + end; + +fun report_theory_text ctxt text = + let val keywords = Thy_Header.get_keywords' ctxt; + val _ = report_text ctxt text; + val _ = + Input.source_explode text + |> Token.tokenize keywords {strict = true} + |> maps (Token.reports keywords) + |> Context_Position.reports_text ctxt; + in () end + +fun prepare_text ctxt = + Input.source_content #> #1 #> Document_Antiquotation.prepare_lines ctxt; +(* This also produces indent-expansion and changes space to "\_" and the introduction of "\newline", + I believe. Otherwise its in Thy_Output.output_source, the compiler from string to LaTeX.text. *) + +fun string_2_text_antiquotation ctxt text = + prepare_text ctxt text + |> Document_Output.output_source ctxt + |> Document_Output.isabelle ctxt + +fun string_2_theory_text_antiquotation ctxt text = + let + val keywords = Thy_Header.get_keywords' ctxt; + in + prepare_text ctxt text + |> Token.explode0 keywords + |> maps (Document_Output.output_token ctxt) + |> Document_Output.isabelle ctxt + end + +fun gen_text_antiquotation name reportNcheck compile = + Document_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) + (fn ctxt => fn text:Input.source => + let + val _ = reportNcheck ctxt text; + in + compile ctxt text + end); + +fun std_text_antiquotation name (* redefined in these more abstract terms *) = + gen_text_antiquotation name report_text string_2_text_antiquotation + +(* should be the same as (2020): +fun text_antiquotation name = + Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) + (fn ctxt => fn text => + let + val _ = report_text ctxt text; + in + prepare_text ctxt text + |> Thy_Output.output_source ctxt + |> Thy_Output.isabelle ctxt + end); +*) + +fun std_theory_text_antiquotation name (* redefined in these more abstract terms *) = + gen_text_antiquotation name report_theory_text string_2_theory_text_antiquotation + +(* should be the same as (2020): +fun theory_text_antiquotation name = + Thy_Output.antiquotation_raw_embedded name (Scan.lift Parse.embedded_input) + (fn ctxt => fn text => + let + val keywords = Thy_Header.get_keywords' ctxt; + + val _ = report_text ctxt text; + val _ = + Input.source_explode text + |> Token.tokenize keywords {strict = true} + |> maps (Token.reports keywords) + |> Context_Position.reports_text ctxt; + in + prepare_text ctxt text + |> Token.explode0 keywords + |> maps (Thy_Output.output_token ctxt) + |> Thy_Output.isabelle ctxt + |> enclose_env ctxt "isarbox" + end); +*) + + + +fun enclose_env ctxt block_env body = + if Config.get ctxt Document_Antiquotation.thy_output_display + then Latex.environment block_env body + else body; + + +fun boxed_text_antiquotation name (* redefined in these more abstract terms *) = + gen_text_antiquotation name report_text + (fn ctxt => string_2_text_antiquotation ctxt + #> enclose_env ctxt "isarbox") + + +fun boxed_theory_text_antiquotation name (* redefined in these more abstract terms *) = + gen_text_antiquotation name report_theory_text + (fn ctxt => string_2_theory_text_antiquotation ctxt + #> enclose_env ctxt "isarbox") + + +(* #> enclose_env ctxt "isarbox" *) + +val _ = Theory.setup + (std_text_antiquotation \<^binding>\my_text\ #> + boxed_text_antiquotation \<^binding>\boxed_text\ #> + std_text_antiquotation \<^binding>\my_cartouche\ #> + boxed_text_antiquotation \<^binding>\boxed_cartouche\ #> + std_theory_text_antiquotation \<^binding>\my_theory_text\#> + boxed_theory_text_antiquotation \<^binding>\boxed_theory_text\); (* is overriding possible ?*) + +\ +(*<*) +text-latex\ + @{boxed_cartouche [display] \definition dfg = \x. x\} + @{boxed_theory_text [display] \doc_class dfg = \x... \\} \ +(*>*) + + + +section\Section Experiments of picture-content\ + + +ML\ + +val thy_output_display = Attrib.setup_option_bool ("thy_output_display", \<^here>); + +val caption_param = Config.declare_string ("caption", \<^here>) (K ""); +val width_param = Config.declare_int ("width", \<^here>) (K 80); \ \char per line\ +val scale_param = Config.declare_int ("scale", \<^here>) (K 100); \ \in percent\ + +Config.put caption_param; +Config.put_global; +Config.get ; + +(* + Latex.string (enclose "[" "]" (String.concat [ label_and_type, ", args={", (commas str_args), "}"])) +*) + +(* +\begin{figure}[h] + \centering + + \includegraphics[scale=0.5]{graph_a} + \caption{An example graph} + + \label{fig:x cubed graph} +\end{figure} + + +\begin{figure} + \centering + + \begin{subfigure}[b]{0.3\textwidth} + + \centering + \includegraphics[width=\textwidth]{graph1} + \caption{$y=x$} + + \label{fig:y equals x} (* PROBLEM *) + \end{subfigure} + + \hfill + + \begin{subfigure}[b]{0.3\textwidth} + + \centering + \includegraphics[width=\textwidth]{graph2} + \caption{$y=3sinx$} + + \label{fig:three sin x} (* PROBLEM *) + \end{subfigure} + + \hfill + + \begin{subfigure}[b]{0.3\textwidth} + + \centering + \includegraphics[width=\textwidth]{graph3} + \caption{$y=5/x$} + + \label{fig:five over x} (* PROBLEM *) + \end{subfigure} + + \caption{Three simple graphs} + \label{fig:three graphs} +\end{figure} + + +\begin{wrapfigure}{l}{0.5\textwidth} + + \centering + \includegraphics[width=1.5cm]{logo.png} + \caption{$y=5/x$} + +\end{wrapfigure} + +*) + +datatype figure_type = single | subfigure | float_embedded + +(* to check if this can be done more properly: user-state or attributes ??? *) +val figure_mode = Unsynchronized.ref(float_embedded) +val figure_label = Unsynchronized.ref(NONE:string option) +val figure_proportions = Unsynchronized.ref([]:int list) +(* invariant : !figure_mode = subfigure_embedded ==> length(!figure_proportions) > 1 *) + +fun figure_antiq (check: Proof.context -> Path.T option -> Input.source -> Path.T) = + Args.context -- Scan.lift Parse.path_input >> (fn (ctxt, source) => + (check ctxt NONE source; + let val cap = Config.get ctxt caption_param + val cap_txt = if cap = "" then "" else (Library.enclose "\n\\caption{" "}\n" cap) + \ \this is naive. one should add an evaluation of doc antiquotations here\ + val wdth= Config.get ctxt width_param + val wdth_ltx = (if wdth = 100 then "" + else if 10<=wdth andalso wdth<=99 + then "width=0."^(Int.toString wdth) + else if 1<=wdth then "width=0.0"^(Int.toString wdth) + else error "width out of range (must be between 1 and 100" + )^"\\textwidth" + val scl = Config.get ctxt scale_param + val scl_ltx = if scl = 100 then "" + else if 10<=scl andalso scl<=99 then "scale=0."^(Int.toString scl) + else if 1<=scl then "scale=0.0"^(Int.toString scl) + else error "scale out of range (must be between 1 and 100" + val fig_args = Library.enclose "[" "]" (commas [wdth_ltx,scl_ltx]) + val _ = writeln cap + fun proportion () = "0."^ (Int.toString (100 div List.length(!figure_proportions))) + \ \naive: assumes equal proportions\ + fun core arg = "\n\\centering\n" + ^"\\includegraphics" + ^fig_args^(Library.enclose "{" "}" arg) + ^cap_txt + \ \add internal labels here\ + fun pat arg = case !figure_mode of + single => core arg + |subfigure => "\n\\begin{subfigure}[b]{"^proportion ()^"\\textwidth}" + ^ core arg + ^"\n\\end{subfigure}\n" + |float_embedded => "\n\\begin{wrapfigure}{r}{"^wdth_ltx^"}" + ^ core arg + ^"\n\\end{wrapfigure}\n" + + in (Latex.output_ascii_breakable "/" (Input.string_of source)) + |> pat + |> Latex.string + end)); + +val _ = Theory.setup + (Document_Antiquotation.setup_option \<^binding>\width\ + (Config.put width_param o Document_Antiquotation.integer) #> + Document_Antiquotation.setup_option \<^binding>\scale\ + (Config.put scale_param o Document_Antiquotation.integer) #> + Document_Antiquotation.setup_option \<^binding>\caption\ + (Config.put caption_param) #> + Document_Output.antiquotation_raw_embedded \<^binding>\figure_content\ + (figure_antiq Resources.check_file) (K I) + + ); +\ + +(*<*) +text-latex\ +@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"} +\ +(*>*) +ML\ + +fun gen_enriched_document_command3 name {body} cid_transform attr_transform markdown + (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, + xstring_opt:(xstring * Position.T) option), + toks:Input.source list) += gen_enriched_document_command2 name {body=body} cid_transform attr_transform markdown + (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, + xstring_opt:(xstring * Position.T) option), + toks) \ \Hack : drop second and thrd args.\ + +val _ = + Outer_Syntax.command ("Figure*", @{here}) "multiple figure" + (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source + >> (Toplevel.theory o (gen_enriched_document_command2 "TTT" {body=true} I I {markdown = true} ))); + + +\ +(* +Figure*[fff::figure,src="\this is a side-by-side\"] + \@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}\ + \ \<^doof> \<^LATEX> \ + \ \<^theory_text>\definition df = ... \ + @{ML [display] \ let val x = 3 + 4 in true end\} + @{cartouche [display] \ @{figure "cfgdfg"}\} + \ +*) + +(*<*) +Figure*[ffff::figure2, caption="\this is another 2 side-by-side\"] + \@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\ + \@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\ + +(* proposed syntax for sub-figure labels : text\ @{figure "ffff(2)"}\ *) + +Figure*[figxxx::figure2,caption="\Proofs establishing an Invariant Preservation.\"] +\@{boxed_theory_text [display] +\lemma inv_c2_preserved : "c2_inv \ \ c1_inv (\ \Hardware\\<^sub>C\<^sub>o\<^sub>m\<^sub>p\<^sub>u\<^sub>t\<^sub>e\<^sub>r\<^sub>H\<^sub>a\<^sub>r\<^sub>d\<^sub>w\<^sub>a\<^sub>r\<^sub>e)" + unfolding c1_inv_def c2_inv_def + Computer_Hardware_to_Hardware_morphism_def + Product_to_Component_morphism_def + by (auto simp: comp_def) + +lemma Computer_Hardware_to_Hardware_total : + "Computer_Hardware_to_Hardware_morphism ` ({X. c2_inv X}) + \ ({X::Hardware. c1_inv X})" + using inv_c2_preserved by auto\}\ + +end +(*>*) diff --git a/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy b/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy index 5fa3d6cc..84e33d40 100644 --- a/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy +++ b/Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy @@ -15,133 +15,29 @@ theory OutOfOrderPresntn imports "Isabelle_DOF-Unit-Tests_document" + "TestKit" "Isabelle_DOF-Ontologies.Conceptual" -keywords "text-" "textN" :: document_body - and "Figure*" :: document_body +keywords "Figure*" :: document_body begin section\Elementary Creation of Doc-items and Access of their Attibutes\ -text\Current status:\ -print_doc_classes -print_doc_items -(* this corresponds to low-level accesses : *) -ML\ -val docitem_tab = DOF_core.get_instances \<^context>; -val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>; -val docclass_tab = DOF_core.get_onto_classes \<^context>; - -Name_Space.dest_table docitem_tab; -Name_Space.dest_table isa_transformer_tab; -Name_Space.dest_table docclass_tab; -app; -\ - - -ML\ - -val _ = Document_Output.document_output - -fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown - (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, - xstring_opt:(xstring * Position.T) option), - toks_list:Input.source list) - : theory -> theory = - let val toplvl = Toplevel.theory_toplevel - - (* as side-effect, generates markup *) - fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (toplvl thy); - val pos = Input.pos_of toks; - val _ = Context_Position.reports ctxt - [(pos, Markup.language_document (Input.is_delimited toks)), - (pos, Markup.plain_text)]; - fun markup xml = let val m = if body then Markup.latex_body - else Markup.latex_heading - in [XML.Elem (m (Latex.output_name name), - xml)] end; - - val text = Document_Output.output_document - (Proof_Context.init_global thy) - markdown toks -(* type file = {path: Path.T, pos: Position.T, content: string} *) - - val strg = XML.string_of (hd (Latex.output text)) - val file = {path = Path.make [oid ^ "_snippet.tex"], - pos = @{here}, - content = Bytes.string strg} - - val _ = Generated_Files.write_file (Path.make ["latex_test"]) - file - val _ = writeln (strg) - in () end \ \important observation: thy is not modified. - This implies that several text block can be - processed in parallel in a future, as long - as they are associated to one meta arg.\ - - (* ... generating the level-attribute syntax *) - in - ( Value_Command.Docitem_Parser.create_and_check_docitem - {is_monitor = false} {is_inline = false} {define = true} - oid pos (cid_transform cid_pos) (attr_transform doc_attrs) - #> (fn thy => (app (check_n_tex_text thy) toks_list; thy))) - end; - -val _ = - Outer_Syntax.command ("text-", @{here}) "formal comment macro" - (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source - >> (Toplevel.theory o (gen_enriched_document_command2 "TTT" {body=true} I I {markdown = true} ))); - -(* copied from Pure_syn for experiments *) - -fun output_document2 state markdown txt = - let - val ctxt = Toplevel.presentation_context state; - val pos = Input.pos_of txt; - val _ = - Context_Position.reports ctxt - [(pos, Markup.language_document (Input.is_delimited txt)), - (pos, Markup.plain_text)]; - val txt' = Document_Output.output_document ctxt markdown txt - val strg = XML.string_of (hd (Latex.output txt')) - - val _ = writeln (strg) - in Document_Output.output_document ctxt markdown txt end; - -fun document_command2 markdown (loc, txt) = - Toplevel.keep (fn state => - (case loc of - NONE => ignore (output_document2 state markdown txt) - | SOME (_, pos) => - error ("Illegal target specification -- not a theory context" - ^ Position.here pos))) - o - Toplevel.present_local_theory loc - (fn state => (output_document2 state markdown txt)); - - -val _ = - Outer_Syntax.command ("textN", \<^here>) "formal comment (primary style)" - (Parse.opt_target -- Parse.document_source >> document_command2 {markdown = true}); - - -\ - -ML\open Bytes\ -(* text\And here a tex - text macro.\ text\Pythons ReStructuredText (RST). @{url \https://de.wikipedia.org/wiki/ReStructuredText\}. Tool: Sphinx. \ text*[aaaa::B]\dfg @{thm [display] refl}\ + +(*<*) text-[dfgdfg::B] \ Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ -textN\ Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ +text-latex\ Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ text-[asd::B] \... and here is its application macro expansion: @@ -153,7 +49,7 @@ text-[asd::B] \} \ -textN\... and here is its application macro expansion: +text-latex\... and here is its application macro expansion: @{B [display] "dfgdfg"} \textbf{TEST} @{cartouche [display] @@ -161,7 +57,7 @@ textN\... and here is its application macro expansion: \ Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \dfgdfg\ \ \}\ -textN\ \<^theory_text>\definition df = ... +text-latex\ \<^theory_text>\definition df = ... \ @{ML [display] \ let val x = 3 + 4 in true end \} @@ -174,8 +70,8 @@ textN\ \<^theory_text>\definition df = ... @{theory_text [display] \definition df = ... \x. \} @{cartouche [display] \ @{figure "cfgdfg"}\} \ -*) -(*<*) + + text\Final Status:\ print_doc_items print_doc_classes @@ -196,7 +92,7 @@ val _ = ) \ -textN\ \<^doof> \<^LATEX> \ +text-latex\ \<^doof> \<^LATEX> \ (* the same effect is achieved with : *) setup \DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\ @@ -204,10 +100,10 @@ setup \DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\< target document, for example, in the tex prelude. Note that the "Binding.make" can be avoided using the alternative \<^binding> notation (see above).*) - setup\DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" (K(K()))\ -textN\ \<^blong>\asd\ outer \<^blong>\syntax| ! see {syntax, outer}\ \ +text-latex\ \<^blong>\asd\ outer \<^blong>\syntax| ! see {syntax, outer}\ \ +(*>*) ML\ @@ -330,14 +226,16 @@ val _ = Theory.setup \ -textN\ +(*<*) +text-latex\ @{boxed_cartouche [display] \definition dfg = \x. x\} @{boxed_theory_text [display] \doc_class dfg = \x... \\} \ - +(*>*) section\Section Experiments of picture-content\ +(*<*) ML\ @@ -477,7 +375,7 @@ val _ = Theory.setup ); \ -textN\ +text-latex\ @{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"} \ diff --git a/Isabelle_DOF-Unit-Tests/ROOT b/Isabelle_DOF-Unit-Tests/ROOT index 9b1e1106..a51fa5f4 100644 --- a/Isabelle_DOF-Unit-Tests/ROOT +++ b/Isabelle_DOF-Unit-Tests/ROOT @@ -1,6 +1,8 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" + options [document = pdf, document_output = "output", document_build = dof] theories + "TestKit" + "Latex_Tests" "AssnsLemmaThmEtc" "Concept_Example_Low_Level_Invariant" "Concept_Example" diff --git a/Isabelle_DOF-Unit-Tests/TestKit.thy b/Isabelle_DOF-Unit-Tests/TestKit.thy new file mode 100644 index 00000000..bf068918 --- /dev/null +++ b/Isabelle_DOF-Unit-Tests/TestKit.thy @@ -0,0 +1,163 @@ +(************************************************************************* + * Copyright (C) + * 2019-2023 The University of Exeter + * 2018-2023 The University of Paris-Saclay + * 2018 The University of Sheffield + * + * License: + * This program can be redistributed and/or modified under the terms + * of the 2-clause BSD-style license. + * + * SPDX-License-Identifier: BSD-2-Clause + *************************************************************************) + +theory + TestKit +imports + "Isabelle_DOF-Unit-Tests_document" + "Isabelle_DOF-Ontologies.Conceptual" +keywords "text-" "text-latex" :: document_body + and "text-assert-error":: document_body + +begin + +section\Elementary Creation of Doc-items and Access of their Attibutes\ + + +text\Current status:\ +print_doc_classes +print_doc_items + +(* this corresponds to low-level accesses : *) +ML\ +val docitem_tab = DOF_core.get_instances \<^context>; +val isa_transformer_tab = DOF_core.get_isa_transformers \<^context>; +val docclass_tab = DOF_core.get_onto_classes \<^context>; + +Name_Space.dest_table docitem_tab; +Name_Space.dest_table isa_transformer_tab; +Name_Space.dest_table docclass_tab; +app; +\ + + +ML\ + +val _ = Document_Output.document_output + +fun gen_enriched_document_command2 name {body} cid_transform attr_transform markdown + (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, + xstring_opt:(xstring * Position.T) option), + toks_list:Input.source list) + : theory -> theory = + let val toplvl = Toplevel.theory_toplevel + + (* as side-effect, generates markup *) + fun check_n_tex_text thy toks = let val ctxt = Toplevel.presentation_context (toplvl thy); + val pos = Input.pos_of toks; + val _ = Context_Position.reports ctxt + [(pos, Markup.language_document (Input.is_delimited toks)), + (pos, Markup.plain_text)]; + fun markup xml = let val m = if body then Markup.latex_body + else Markup.latex_heading + in [XML.Elem (m (Latex.output_name name), + xml)] end; + + val text = Document_Output.output_document + (Proof_Context.init_global thy) + markdown toks +(* type file = {path: Path.T, pos: Position.T, content: string} *) + + val strg = XML.string_of (hd (Latex.output text)) + val file = {path = Path.make [oid ^ "_snippet.tex"], + pos = @{here}, + content = Bytes.string strg} + + val _ = Generated_Files.write_file (Path.make ["latex_test"]) + file + val _ = writeln (strg) + in () end \ \important observation: thy is not modified. + This implies that several text block can be + processed in parallel in a future, as long + as they are associated to one meta arg.\ + + (* ... generating the level-attribute syntax *) + in + ( Value_Command.Docitem_Parser.create_and_check_docitem + {is_monitor = false} {is_inline = false} {define = true} + oid pos (cid_transform cid_pos) (attr_transform doc_attrs) + #> (fn thy => (app (check_n_tex_text thy) toks_list; thy))) + end; + +val _ = + Outer_Syntax.command ("text-", @{here}) "formal comment macro" + (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source + >> (Toplevel.theory o (gen_enriched_document_command2 "TTT" {body=true} I I {markdown = true} ))); + +(* copied from Pure_syn for experiments *) + +fun output_document2 state markdown txt = + let + val ctxt = Toplevel.presentation_context state; + val pos = Input.pos_of txt; + val _ = + Context_Position.reports ctxt + [(pos, Markup.language_document (Input.is_delimited txt)), + (pos, Markup.plain_text)]; + val txt' = Document_Output.output_document ctxt markdown txt + val strg = XML.string_of (hd (Latex.output txt')) + + val _ = writeln (strg) + in Document_Output.output_document ctxt markdown txt end; + +fun document_command2 markdown (loc, txt) = + Toplevel.keep (fn state => + (case loc of + NONE => ignore (output_document2 state markdown txt) + | SOME (_, pos) =>(ISA_core.err + "Illegal target specification -- not a theory context" + pos))) + o + Toplevel.present_local_theory loc + (fn state => (output_document2 state markdown txt)); + +fun document_command3 markdown (loc, txt) trns = (document_command2 markdown (loc, txt) trns + handle exn => ((writeln "AAA"); trns)) + +fun gen_enriched_document_command3 assert name body cid_transform attr_transform markdown + (((((oid,pos),cid_pos), doc_attrs) : ODL_Meta_Args_Parser.meta_args_t, + xstring_opt:(xstring * Position.T) option), + src_list:Input.source list) thy + = (gen_enriched_document_command2 name body cid_transform attr_transform markdown + (((((oid,pos),cid_pos), doc_attrs), xstring_opt), src_list) + thy) + handle ERROR str => (if assert src_list str then (writeln ("Correct error:"^str^":reported.");thy) + else error"Wrong error reported") + +fun error_match [_, src] str = (String.isPrefix (Input.string_of src) str) + | error_match _ _ = error "Wrong assertion format: required" + + +val _ = + Outer_Syntax.command ("text-assert-error", @{here}) "formal comment macro" + (ODL_Meta_Args_Parser.attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source + >> (Toplevel.theory o (gen_enriched_document_command3 error_match "TTT" {body=true} + I I {markdown = true}) + )); + + +val _ = + Outer_Syntax.command ("text-latex", \<^here>) "formal comment (primary style)" + (Parse.opt_target -- Parse.document_source >> document_command2 {markdown = true}); + + +\ + +(* auto-tests *) +text-latex\ dfg\ + +text-assert-error[aaaa::A]\ @{A \sdf\}\\reference ontologically inconsistent\ + + +end +(*>*)