Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Merge.
ci/woodpecker/push/build Pipeline was successful Details

This commit is contained in:
Achim D. Brucker 2023-03-02 08:06:21 +00:00
parent daea6333f1 0f5e7f582b
commit 113b3e79bf
10 changed files with 860 additions and 238 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

82
Isabelle_DOF-Ontologies/Conceptual/Conceptual.thy
View File

@ -20,12 +20,14 @@ imports
"Isabelle_DOF.Isa_COL"
begin
section\<open>Excursion: On the semantic consequences of this definition: \<close>
text\<open>Consider the following document class definition and its consequences:\<close>
doc_class A =
level :: "int option"
x :: int
section\<open>Excursion: On the semantic consequences of this definition: \<close>
text\<open>This class definition leads an implicit Isabelle/HOL \<^theory_text>\<open>record\<close> definition
(cf. \<^url>\<open>https://isabelle.in.tum.de/doc/isar-ref.pdf\<close>, chapter 11.6.).
@ -49,23 +51,61 @@ Consequently, \<^theory_text>\<open>doc_class\<close>'es inherit the entire theo
\<^enum> @{thm [display] A.simps(6)}
\<^enum> ...
\<close>
(* the generated theory of the \<^theory_text>\<open>doc_class\<close> A can be inspected, of course, by *)
text\<open>The generated theory of the \<^theory_text>\<open>doc_class\<close> A can be inspected, of course, by:\<close>
find_theorems (60) name:Conceptual name:A
text\<open>A more abstract view on the state of the DOF machine can be found here:\<close>
print_doc_classes
print_doc_items
text\<open>... and an ML-level output:\<close>
ML\<open>
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>;
\<close>
ML\<open>
Name_Space.dest_table docitem_tab;
Name_Space.dest_table isa_transformer_tab;
Name_Space.dest_table docclass_tab;
\<close>
text\<open>... or as ML assertion: \<close>
ML\<open>
@{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))
\<close>
text\<open>As a consequence of the theory of the \<^theory_text>\<open>doc_class\<close> \<open>A\<close>, the code-generator setup lets us
evaluate statements such as: \<close>
value\<open> the(A.level (A.make 3 (Some 4) 5)) = 4\<close>
text\<open>And finally, as a consequence of the above semantic construction of \<^theory_text>\<open>doc_class\<close>'es, the internal
text\<open>And further, as a consequence of the above semantic construction of \<^theory_text>\<open>doc_class\<close>'es, the internal
\<open>\<lambda>\<close>-calculus representation of class instances looks as follows:\<close>
ML\<open>
val tt = @{term \<open>the(A.level (A.make 3 (Some 4) 5))\<close>}
@{term \<open>the(A.level (A.make 3 (Some 4) 5))\<close>};
fun match (Const("Option.option.the",_) $
(Const ("Conceptual.A.level",_) $
(Const ("Conceptual.A.make", _) $ u $ v $ w))) = true
|match _ = false;
@{assert} (match @{term \<open>the(A.level (A.make 3 (Some 4) 5))\<close>})
\<close>
text\<open>For the code-generation, we have the following access to values representing class instances:\<close>
text\<open>And finally, via the code-generation, we have the following programmable
access to values representing class instances:\<close>
ML\<open>
val A_make = @{code A.make};
val zero = @{code "0::int"};
@ -75,9 +115,9 @@ val add = @{code "(+) :: int \<Rightarrow> int \<Rightarrow> int"};
A_make zero (SOME one) (add one one)
\<close>
section\<open>Building up a conceptual class hierarchy:\<close>
section\<open>An independent class-tree root: \<close>
text\<open>An independent class-tree root: \<close>
doc_class B =
level :: "int option"
@ -125,7 +165,7 @@ doc_class F =
and br':: "r \<sigma> \<noteq> [] \<and> length(b' \<sigma>) \<ge> 3"
and cr :: "properties \<sigma> \<noteq> []"
text\<open>The effect of the invariant declaration is to provide intern definitions for validation
text\<open>The effect of the invariant declaration is to provide intern HOL definitions for validation
functions of this invariant. They can be referenced as follows:\<close>
thm br_inv_def
thm br'_inv_def
@ -133,7 +173,7 @@ thm cr_inv_def
term "\<lparr>F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\<rparr>"
term "br' (\<lparr>F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\<rparr>) "
term "br'_inv (\<lparr>F.tag_attribute = 5, properties = [], r = [], u = undefined, s = [], b = {}, b' = []\<rparr>) "
text\<open>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:\<close>
ML\<open> val cr_inv_code = @{code "cr_inv"} \<close> \<comment> \<open>works albeit thm is abstract ...\<close>
text\<open>while in :\<close>
(* ML\<open> val br_inv_code = @{code "br_inv"} \<close> \<comment>\<open>this does not work ...\<close> *)
ML\<open> val br_inv_code = @{code "br_inv"} \<close> \<comment>\<open>this does not work ...\<close>
text\<open>... the compilation fails due to the fact that nothing prevents the user
to define an infinite relation between \<^typ>\<open>A\<close> and \<^typ>\<open>C\<close>. However, the alternative
@ -151,21 +191,27 @@ ML\<open> val br'_inv_code = @{code "br'_inv"} \<close> \<comment> \<open>does w
text\<open>... is compilable ...\<close>
doc_class G = C +
g :: "thm" <= "@{thm \<open>HOL.refl\<close>}"
g :: "thm" <= "@{thm \<open>HOL.refl\<close>}" (* warning overriding attribute expected*)
doc_class M =
ok :: "unit"
accepts "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
text\<open>The final class and item tables look like this:\<close>
print_doc_classes
print_doc_items
ML\<open>
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\<close>
(*
ML\<open> Document.state();\<close>
ML\<open> Outer_Syntax.command; \<close>
ML\<open> Thy_Header.get_keywords @{theory};(* this looks to be really theory global. *) \<close>
*)
open_monitor*[aaa::M]
section*[test::A]\<open>Test and Validation\<close>

12
Isabelle_DOF-Unit-Tests/Attributes.thy
View File

@ -17,8 +17,8 @@ theory
"Isabelle_DOF-Unit-Tests_document"
"Isabelle_DOF-Ontologies.Conceptual"
begin
section\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
ML\<open>@{assert} (1 = 1)\<close>
section\<open>Elementar Creation of Doc-items and Access of their Attibutes\<close>
text\<open>Current status:\<close>
print_doc_classes
@ -29,9 +29,13 @@ ML\<open>
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;
\<close>
ML\<open>
map fst (Name_Space.dest_table docitem_tab);
Name_Space.dest_table docclass_tab;
\<close>
ML\<open>
val (oid, DOF_core.Instance {value, ...}) =
Name_Space.check (Context.Proof \<^context>) (DOF_core.get_instances \<^context>) ("aaa", Position.none)

71
Isabelle_DOF-Unit-Tests/Concept_Example.thy
View File

@ -1,71 +0,0 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 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
*************************************************************************)
chapter\<open>Setting and modifying attributes of doc-items\<close>
theory
Concept_Example
imports
"Isabelle_DOF-Unit-Tests_document"
"Isabelle_DOF-Ontologies.Conceptual" (* we use the generic "Conceptual" ontology *)
begin
text\<open>@{theory "Isabelle_DOF-Ontologies.Conceptual"} provides a monitor @{typ M} enforcing a particular document structure.
Here, we say: From now on, this structural rules are respected wrt. all doc\_classes M is
enabled for.\<close>
open_monitor*[struct::M]
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
... @{C "c1"} @{thm "refl"} \<close>
update_instance*[d::D, a1 := X2]
text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>}\<close>
text*[c2::C, x = "\<open>delta\<close>"] \<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>
text\<open>Note that both the notations @{term "''beta''"} and @{term "\<open>beta\<close>"} are possible;
the former is a more ancient format only supporting pure ascii, while the latter also supports
fancy unicode such as: @{term "\<open>\<beta>\<^sub>i''\<close>"} \<close>
text*[f::F] \<open> Lectus accumsan velit ultrices, ... \<close>
theorem some_proof : "True" by simp
text\<open>This is an example where we add a theorem into a kind of "result-list" of the doc-item f.\<close>
update_instance*[f::F,r:="[@{thm ''Concept_Example.some_proof''}]"]
text\<open> ..., mauris amet, id elit aliquam aptent id, ... @{docitem \<open>a\<close>} \<close>
text\<open>Here we add and maintain a link that is actually modeled as m-to-n relation ...\<close>
update_instance*[f::F,b:="{(@{docitem \<open>a\<close>}::A,@{docitem \<open>c1\<close>}::C),
(@{docitem \<open>a\<close>}, @{docitem \<open>c2\<close>})}"]
close_monitor*[struct]
text\<open>And the trace of the monitor is:\<close>
ML\<open>@{trace_attribute struct}\<close>
print_doc_classes
print_doc_items
end

142
Isabelle_DOF-Unit-Tests/Concept_OntoReferencing.thy Normal file
View File

@ -0,0 +1,142 @@
(*************************************************************************
* Copyright (C)
* 2019 The University of Exeter
* 2018-2019 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
*************************************************************************)
chapter\<open>Setting and modifying attributes of doc-items\<close>
theory
Concept_OntoReferencing
imports
"Isabelle_DOF-Unit-Tests_document"
"Isabelle_DOF-Ontologies.Conceptual"
"TestKit"
begin
section\<open>Setting up a monitor.\<close>
text\<open>\<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> provides a monitor \<^typ>\<open>M\<close> enforcing a
particular document structure. Here, we say: From now on, this structural rules are
respected wrt. all \<^theory_text>\<open>doc_classes M\<close> is enabled for.\<close>
open_monitor*[struct::M]
section\<open>Defining Text Elements and Referring to them... \<close>
text\<open> This uses elements of two ontologies, notably
\<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> and \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>.\<close>
(*<*)
title*[abbb::title, short_title="Some\<open>ooups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
subtitle*[abbbb::subtitle, abbrev = "Some\<open>ooups-oups.\<close>"]\<open>Lorem ipsum dolor sit amet ...\<close>
chapter*[abbbbbb::A, x = "3"] \<open> Lorem ipsum dolor sit amet ... \<close>
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
subsection*[ab::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ...
As mentioned in the @{title \<open>abbb\<close>}... \<close> \<comment> \<open>old-style and ...\<close>
subsubsection*[abb::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ...
As mentioned in the \<^title>\<open>abbb\<close>\<close> \<comment> \<open>new-style references to
ontological instances
assigned to text
elements ...\<close>
(*>*)
text\<open>Meta-Objects are typed, and references have to respect this : \<close>
(*<*)
text-assert-error[ac]\<open> \<^title>\<open>a\<close> \<close> \<open>reference ontologically inconsistent\<close>
text-assert-error[ad]\<open> \<^title>\<open>abbbb\<close> \<close>\<open>reference ontologically inconsistent\<close>
\<comment> \<open>erroneous reference: please consider class hierarchy!\<close>
(*>*)
text\<open>References to Meta-Objects can be forward-declared:\<close>
text-assert-error[ae1]\<open>@{C \<open>c1\<close>} \<close>\<open>Undefined instance:\<close>
declare_reference*[c1::C] \<comment> \<open>forward declaration\<close>
text\<open>@{C \<open>c1\<close>} \<close> \<comment> \<open>THIS IS A BUG !!! OVERLY SIMPLISTIC BEHAVIOUR. THIS SHOULD FAIL! \<close>
text\<open>@{C (unchecked) \<open>c1\<close>} \<close> \<comment> \<open>THIS SHOULD BE THE CORRECT BEHAVIOUR! \<close>
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
text-assert-error[c1::C, x = "''gamma''"]
\<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
\<open>Duplicate instance declaration\<close>
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
... @{C "c1"} or @{C \<open>c1\<close>} or \<^C>\<open>c1\<close>
similar to @{thm "refl"} and \<^thm>"refl"\<close> \<comment> \<open>ontological and built-in
references\<close>
text\<open>Not only text-elements are "ontology-aware", proofs and code can this be too !\<close>
ML*[ddddd2::E]\<open>fun fac x = if x = 0 then 1 else x * (fac(x-1))\<close> (* TODO : BUG *)
(* TODO BUG : lemma*[ddddd3::E] asd: "True" *)
text\<open>Ontological information ("class instances") is mutable: \<close>
update_instance*[d::D, a1 := X2]
text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>} ... \<close> \<comment> \<open>untyped or typed referencing \<close>
(* THIS IS A BUG \<And>\<And>! *)
text-assert-error[ae::text_element]\<open>the function @{E "ddddd2"} \<close>\<open>referred text-element is macro!\<close>
text*[c2::C, x = "\<open>delta\<close>"] \<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>
text\<open>Note that both the notations @{term "''beta''"} and @{term "\<open>beta\<close>"} are possible;
the former is a more ancient format only supporting pure ascii, while the latter also supports
fancy unicode such as: @{term "\<open>\<beta>\<^sub>i''\<close>"} \<close>
text*[f::F] \<open> Lectus accumsan velit ultrices, ... \<close>
theorem some_proof : "True" by simp
text\<open>This is an example where we add a theorem into a kind of "result-list" of the doc-item f.\<close>
update_instance*[f::F,r:="[@{thm ''Concept_OntoReferencing.some_proof''}]"]
text\<open> ..., mauris amet, id elit aliquam aptent id, ... @{docitem \<open>a\<close>} \<close>
text\<open>Here we add and maintain a link that is actually modeled as m-to-n relation ...\<close>
update_instance*[f::F,b:="{(@{docitem \<open>a\<close>}::A,@{docitem \<open>c1\<close>}::C),
(@{docitem \<open>a\<close>}, @{docitem \<open>c2\<close>})}"]
close_monitor*[struct]
text\<open>And the trace of the monitor is:\<close>
ML\<open>val trace = @{trace_attribute struct}\<close>
ML\<open>@{assert} (trace = [("Conceptual.A", "abbbbbb"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"),
("Conceptual.A", "abb"),("Conceptual.C", "c1"),("Conceptual.C", "c1"), ("Conceptual.D", "d"),
("Conceptual.E", "ddddd2"), ("Conceptual.C", "c2"), ("Conceptual.F", "f")]) \<close>
(* SHOULD BE:
ML\<open>@{assert} (trace = [("Conceptual.A", "abbbbbb"), ("Conceptual.A", "a"), ("Conceptual.A", "ab"),
("Conceptual.A", "abb"),("Conceptual.C", "c1"), ("Conceptual.D", "d"),
("Conceptual.E", "ddddd2"), ("Conceptual.C", "c2"), ("Conceptual.F", "f")]) \<close>
FAILURE DUE TO DUPLICATE DEFINITION BUG
*)
text\<open>Note that the monitor \<^typ>\<open>M\<close> of the ontology \<^theory>\<open>Isabelle_DOF-Ontologies.Conceptual\<close> does
not observe the common entities of \<^theory>\<open>Isabelle_DOF.Isa_COL\<close>, but just those defined in the
accept- clause of \<^typ>\<open>M\<close>.\<close>
text\<open>One final check of the status DOF core: observe that no new classes have been defined,
just a couple of new document elements have been introduced.\<close>
print_doc_classes
print_doc_items
end

6
Isabelle_DOF-Unit-Tests/Evaluation.thy
View File

@ -81,9 +81,9 @@ term*\<open>@{A \<open>xcv1\<close>}\<close>
text\<open>The instance class @{docitem \<open>xcv1\<close>} is not an instance of the class @{doc_class B}:
\<close>
(* Error:
term*\<open>@{B \<open>xcv1\<close>}\<close>*)
(* Error:
term*\<open>@{B \<open>xcv1\<close>}\<close>
*)
text\<open>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:
\<close>

43
Isabelle_DOF-Unit-Tests/High_Level_Syntax_Invariants.thy
View File

@ -90,7 +90,7 @@ text\<open>Now assume the following ontology:\<close>
doc_class title =
short_title :: "string option" <= "None"
doc_class author =
doc_class Author =
email :: "string" <= "''''"
datatype classification = SIL0 | SIL1 | SIL2 | SIL3 | SIL4
@ -100,18 +100,18 @@ doc_class abstract =
safety_level :: "classification" <= "SIL3"
doc_class text_section =
authored_by :: "author set" <= "{}"
authored_by :: "Author set" <= "{}"
level :: "int option" <= "None"
type_synonym notion = string
doc_class introduction = text_section +
authored_by :: "author set" <= "UNIV"
doc_class Introduction = text_section +
authored_by :: "Author set" <= "UNIV"
uses :: "notion set"
invariant author_finite :: "finite (authored_by \<sigma>)"
and force_level :: "the (level \<sigma>) > 1"
and force_level :: "(level \<sigma>) \<noteq> None \<and> the (level \<sigma>) > 1"
doc_class claim = introduction +
doc_class claim = Introduction +
based_on :: "notion list"
doc_class technical = text_section +
@ -140,7 +140,7 @@ text\<open>Next we define some instances (docitems): \<close>
declare[[invariants_checking_with_tactics = true]]
text*[church::author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
text*[church::Author, email="\<open>church@lambda.org\<close>"]\<open>\<close>
text*[resultProof::result, evidence = "proof", property="[@{thm \<open>HOL.refl\<close>}]"]\<open>\<close>
text*[resultArgument::result, evidence = "argument"]\<open>\<close>
@ -151,29 +151,30 @@ text\<open>The invariants \<^theory_text>\<open>author_finite\<close> and \<^the
It will enable a basic tactic, using unfold and auto:\<close>
declare[[invariants_checking_with_tactics = true]]
(*
text*[curry::author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
text*[introduction2::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
When not commented, should violated the invariant:
update_instance*[introduction2::introduction
, authored_by := "{@{author \<open>church\<close>}}"
text*[curry::Author, email="\<open>curry@lambda.org\<close>"]\<open>\<close>
text*[introduction2::Introduction, authored_by = "{@{Author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
(* When not commented, should violated the invariant:
update_instance*[introduction2::Introduction
, authored_by := "{@{Author \<open>church\<close>}}"
, level := "Some 1"]
*)
text*[introduction3::introduction, authored_by = "{@{author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
text*[introduction4::introduction, authored_by = "{@{author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
text*[introduction3::Introduction, authored_by = "{@{Author \<open>church\<close>}}", level = "Some 2"]\<open>\<close>
text*[introduction4::Introduction, authored_by = "{@{Author \<open>curry\<close>}}", level = "Some 4"]\<open>\<close>
text*[resultProof2::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"]\<open>\<close>
text\<open>Then we can evaluate expressions with instances:\<close>
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
value*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction4\<close>}\<close>
term*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
value*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
value*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction4\<close>}\<close>
value*\<open>@{introduction \<open>introduction2\<close>}\<close>
value*\<open>@{Introduction \<open>introduction2\<close>}\<close>
value*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>
value*\<open>{@{Author \<open>curry\<close>}} = {@{Author \<open>church\<close>}}\<close>
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
value*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
@ -183,5 +184,5 @@ value*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \
declare[[invariants_checking_with_tactics = false]]
declare[[invariants_strict_checking = false]]
*)
end

435
Isabelle_DOF-Unit-Tests/Latex_Tests.thy Normal file
View File

@ -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\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
text\<open>Output status:\<close>
print_doc_classes
print_doc_items
text\<open>And here a tex - text macro.\<close>
text\<open>Pythons ReStructuredText (RST).
@{url \<open>https://de.wikipedia.org/wiki/ReStructuredText\<close>}. Tool: Sphinx.
\<close>
text*[aaaa::B]\<open>dfg @{thm [display] refl}\<close>
text-[dfgdfg::B]
\<open> Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
text-latex\<open> Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
text-[asd::B]
\<open>... and here is its application macro expansion:
@{B [display] "dfgdfg"}
\textbf{TEST}
@{cartouche [display]
\<open>text*[dfgdfg::B]
\<open> Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
\<close>}
\<close>
text-latex\<open>... and here is its application macro expansion:
@{B [display] "dfgdfg"}
\textbf{TEST}
@{cartouche [display]
\<open>text*[dfgdfg::B]
\<open> Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
\<close>}\<close>
(*<*)
text-latex\<open> \<^theory_text>\<open>definition df = ...
\<close>
@{ML [display] \<open> let val x = 3 + 4 in true end
\<close>}
@{ML_text [display] \<open> val x = ...
\<close>}
@{verbatim [display] \<open> Lorem ipsum ... @{thm refl}
Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>}
@{theory_text [display] \<open>definition df = ... \<lambda>x.
\<close>}
@{cartouche [display] \<open> @{figure "cfgdfg"}\<close>} \<close>
(*>*)
text\<open>Final Status:\<close>
print_doc_items
print_doc_classes
section\<open>Experiments on Inline-Textelements\<close>
text\<open>Std Abbreviations. Inspired by the block *\<open>control spacing\<close>
in @{file \<open>$ISABELLE_HOME/src/Pure/Thy/document_antiquotations.ML\<close>}.
We mechanize the table-construction and even attach the LaTeX
quirks to be dumped into the prelude. \<close>
ML\<open>
val _ =
Theory.setup
( Document_Output.antiquotation_raw \<^binding>\<open>doof\<close> (Scan.succeed ())
(fn _ => fn () => Latex.string "\\emph{doof}")
#> Document_Output.antiquotation_raw \<^binding>\<open>LATEX\<close> (Scan.succeed ())
(fn _ => fn () => Latex.string "\\textbf{LaTeX}")
)
\<close>
text-latex\<open> \<^doof> \<^LATEX> \<close>
(* the same effect is achieved with : *)
setup \<open>DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\<close>
(* 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\<open>DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" (K(K()))\<close>
(*<*)
text-latex\<open> \<^blong>\<open>asd\<close> outer \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
(*>*)
ML\<open>
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>\<open>my_text\<close> #>
boxed_text_antiquotation \<^binding>\<open>boxed_text\<close> #>
std_text_antiquotation \<^binding>\<open>my_cartouche\<close> #>
boxed_text_antiquotation \<^binding>\<open>boxed_cartouche\<close> #>
std_theory_text_antiquotation \<^binding>\<open>my_theory_text\<close>#>
boxed_theory_text_antiquotation \<^binding>\<open>boxed_theory_text\<close>); (* is overriding possible ?*)
\<close>
(*<*)
text-latex\<open>
@{boxed_cartouche [display] \<open>definition dfg = \<lambda>x. x\<close>}
@{boxed_theory_text [display] \<open>doc_class dfg = \<lambda>x... \<Gamma>\<close>} \<close>
(*>*)
section\<open>Section Experiments of picture-content\<close>
ML\<open>
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); \<comment> \<open>char per line\<close>
val scale_param = Config.declare_int ("scale", \<^here>) (K 100); \<comment> \<open>in percent\<close>
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)
\<comment> \<open>this is naive. one should add an evaluation of doc antiquotations here\<close>
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)))
\<comment> \<open>naive: assumes equal proportions\<close>
fun core arg = "\n\\centering\n"
^"\\includegraphics"
^fig_args^(Library.enclose "{" "}" arg)
^cap_txt
\<comment> \<open>add internal labels here\<close>
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>\<open>width\<close>
(Config.put width_param o Document_Antiquotation.integer) #>
Document_Antiquotation.setup_option \<^binding>\<open>scale\<close>
(Config.put scale_param o Document_Antiquotation.integer) #>
Document_Antiquotation.setup_option \<^binding>\<open>caption\<close>
(Config.put caption_param) #>
Document_Output.antiquotation_raw_embedded \<^binding>\<open>figure_content\<close>
(figure_antiq Resources.check_file) (K I)
);
\<close>
(*<*)
text-latex\<open>
@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}
\<close>
(*>*)
ML\<open>
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) \<comment> \<open>Hack : drop second and thrd args.\<close>
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} )));
\<close>
(*
Figure*[fff::figure,src="\<open>this is a side-by-side\<close>"]
\<open>@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}\<close>
\<open> \<^doof> \<^LATEX> \<close>
\<open> \<^theory_text>\<open>definition df = ... \<close>
@{ML [display] \<open> let val x = 3 + 4 in true end\<close>}
@{cartouche [display] \<open> @{figure "cfgdfg"}\<close>}
\<close>
*)
(*<*)
Figure*[ffff::figure2, caption="\<open>this is another 2 side-by-side\<close>"]
\<open>@{figure_content [width=40, scale=35, caption="This is a left test"] "ROOT"}\<close>
\<open>@{figure_content [width=40, scale=35, caption="This is a right test"] "ROOT"}\<close>
(* proposed syntax for sub-figure labels : text\<open> @{figure "ffff(2)"}\<close> *)
Figure*[figxxx::figure2,caption="\<open>Proofs establishing an Invariant Preservation.\<close>"]
\<open>@{boxed_theory_text [display]
\<open>lemma inv_c2_preserved : "c2_inv \<sigma> \<Longrightarrow> c1_inv (\<sigma> \<langle>Hardware\<rangle>\<^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})
\<subseteq> ({X::Hardware. c1_inv X})"
using inv_c2_preserved by auto\<close>}\<close>
end
(*>*)

136
Isabelle_DOF-Unit-Tests/OutOfOrderPresntn.thy
View File

@ -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\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
text\<open>Current status:\<close>
print_doc_classes
print_doc_items
(* this corresponds to low-level accesses : *)
ML\<open>
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;
\<close>
ML\<open>
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 \<comment> \<open>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.\<close>
(* ... 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});
\<close>
ML\<open>open Bytes\<close>
(*
text\<open>And here a tex - text macro.\<close>
text\<open>Pythons ReStructuredText (RST).
@{url \<open>https://de.wikipedia.org/wiki/ReStructuredText\<close>}. Tool: Sphinx.
\<close>
text*[aaaa::B]\<open>dfg @{thm [display] refl}\<close>
(*<*)
text-[dfgdfg::B]
\<open> Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
textN\<open> Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
text-latex\<open> Lorem ipsum ... @{thm [display] refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
text-[asd::B]
\<open>... and here is its application macro expansion:
@ -153,7 +49,7 @@ text-[asd::B]
\<close>}
\<close>
textN\<open>... and here is its application macro expansion:
text-latex\<open>... and here is its application macro expansion:
@{B [display] "dfgdfg"}
\textbf{TEST}
@{cartouche [display]
@ -161,7 +57,7 @@ textN\<open>... and here is its application macro expansion:
\<open> Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
\<close>}\<close>
textN\<open> \<^theory_text>\<open>definition df = ...
text-latex\<open> \<^theory_text>\<open>definition df = ...
\<close>
@{ML [display] \<open> let val x = 3 + 4 in true end
\<close>}
@ -174,8 +70,8 @@ textN\<open> \<^theory_text>\<open>definition df = ...
@{theory_text [display] \<open>definition df = ... \<lambda>x.
\<close>}
@{cartouche [display] \<open> @{figure "cfgdfg"}\<close>} \<close>
*)
(*<*)
text\<open>Final Status:\<close>
print_doc_items
print_doc_classes
@ -196,7 +92,7 @@ val _ =
)
\<close>
textN\<open> \<^doof> \<^LATEX> \<close>
text-latex\<open> \<^doof> \<^LATEX> \<close>
(* the same effect is achieved with : *)
setup \<open>DOF_lib.define_shortcut (Binding.make("bla",\<^here>)) "\\blabla"\<close>
@ -204,10 +100,10 @@ setup \<open>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\<open>DOF_lib.define_macro (Binding.make("blong",\<^here>)) "\\blong{" "}" (K(K()))\<close>
textN\<open> \<^blong>\<open>asd\<close> outer \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
text-latex\<open> \<^blong>\<open>asd\<close> outer \<^blong>\<open>syntax| ! see {syntax, outer}\<close> \<close>
(*>*)
ML\<open>
@ -330,14 +226,16 @@ val _ = Theory.setup
\<close>
textN\<open>
(*<*)
text-latex\<open>
@{boxed_cartouche [display] \<open>definition dfg = \<lambda>x. x\<close>}
@{boxed_theory_text [display] \<open>doc_class dfg = \<lambda>x... \<Gamma>\<close>} \<close>
(*>*)
section\<open>Section Experiments of picture-content\<close>
(*<*)
ML\<open>
@ -477,7 +375,7 @@ val _ = Theory.setup
);
\<close>
textN\<open>
text-latex\<open>
@{figure_content [width=40, scale=35, caption="This is a test"] "ROOT"}
\<close>

6
Isabelle_DOF-Unit-Tests/ROOT
View File

@ -1,12 +1,14 @@
session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
options [document = pdf, document_output = "output", document_build = dof]
theories
"AssnsLemmaThmEtc"
"TestKit"
"Latex_Tests"
"Concept_OntoReferencing"
"Concept_Example_Low_Level_Invariant"
"Concept_Example"
"TermAntiquotations"
"Attributes"
"Evaluation"
"AssnsLemmaThmEtc"
"High_Level_Syntax_Invariants"
"Ontology_Matching_Example"
"Cenelec_Test"

165
Isabelle_DOF-Unit-Tests/TestKit.thy Normal file
View File

@ -0,0 +1,165 @@
(*************************************************************************
* 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\<open>Elementary Creation of Doc-items and Access of their Attibutes\<close>
text\<open>Current status:\<close>
print_doc_classes
print_doc_items
(* this corresponds to low-level accesses : *)
ML\<open>
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;
\<close>
ML\<open>
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 \<comment> \<open>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.\<close>
(* ... 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 msg => (if assert src_list msg then (writeln ("Correct error:"^msg^":reported.");thy)
else error"Wrong error reported")
fun error_match [_, src] msg = (writeln((Input.string_of src));
String.isPrefix (Input.string_of src) msg )
| error_match _ _ = error "Wrong text-assertion-error. Argument format <arg><match> 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});
\<close>
(* auto-tests *)
text-latex\<open>dfg\<close>
text-assert-error[aaaa::A]\<open> @{A \<open>sdf\<close>}\<close>\<open>reference ontologically inconsistent\<close>
ML\<open>String.isPrefix "ab" "abc"\<close>
end
(*>*)