forked from Isabelle_DOF/Isabelle_DOF
Merge branch 'main' of https://git.logicalhacking.com/Isabelle_DOF/Isabelle_DOF
This commit is contained in:
Burkhart Wolff
commit
3b446c874d
|
|
@ -21,7 +21,6 @@ no_notation "Isabelle_DOF_trace_attribute" ("@{trace-attribute _}")
|
|||
|
||||
consts Isabelle_DOF_typ :: "string \<Rightarrow> typ" ("@{typ _}")
|
||||
consts Isabelle_DOF_term :: "string \<Rightarrow> term" ("@{term _}")
|
||||
consts Isabelle_DOF_term_repr :: "string \<Rightarrow> term" ("@{termrepr _}")
|
||||
datatype "thm" = Isabelle_DOF_thm string ("@{thm _}") | Thm_content ("proof":proofterm)
|
||||
datatype "thms_of" = Isabelle_DOF_thms_of string ("@{thms-of _}")
|
||||
datatype "file" = Isabelle_DOF_file string ("@{file _}")
|
||||
|
|
@ -269,13 +268,6 @@ case term_option of
|
|||
val traces' = map conv (HOLogic.dest_list traces)
|
||||
in HOLogic.mk_list \<^Type>\<open>prod \<^typ>\<open>string\<close> \<^typ>\<open>string\<close>\<close> traces' end
|
||||
|
||||
(* utilities *)
|
||||
|
||||
fun property_list_dest ctxt X =
|
||||
map (fn \<^Const_>\<open>Isabelle_DOF_term for s\<close> => HOLogic.dest_string s
|
||||
|\<^Const_>\<open>Isabelle_DOF_term_repr for s\<close> => holstring_to_bstring ctxt (HOLogic.dest_string s))
|
||||
(HOLogic.dest_list X)
|
||||
|
||||
end; (* struct *)
|
||||
|
||||
\<close>
|
||||
|
|
@ -314,7 +306,6 @@ end)
|
|||
#>
|
||||
([(\<^const_name>\<open>Isabelle_DOF_typ\<close>, ISA_core.ML_isa_check_typ, ISA_core.ML_isa_elaborate_typ)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_term\<close>, ISA_core.ML_isa_check_term, ISA_core.ML_isa_elaborate_term)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_term_repr\<close>, ISA_core.check_identity, ISA_core.ML_isa_elaborate_generic)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_docitem\<close>,
|
||||
ISA_core.ML_isa_check_docitem, ISA_core.ML_isa_elaborate_generic)
|
||||
,(\<^const_name>\<open>Isabelle_DOF_trace_attribute\<close>,
|
||||
|
|
|
|||
|
|
@ -39,39 +39,17 @@ text\<open>For now, as the term annotation is not bound to a meta logic which wi
|
|||
in the assertion.
|
||||
\<close>
|
||||
|
||||
(* does not work in batch mode ...
|
||||
(* sample for accessing a property filled with previous assert's of "aa" *)
|
||||
ML\<open> ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa};\<close>
|
||||
|
||||
|
||||
|
||||
assert*[aa::F] " X \<and> Y \<longrightarrow> True" (*example with uni-code *)
|
||||
ML\<open> ISA_core.property_list_dest @{context} @{docitem_attribute property :: aa};
|
||||
app writeln (tl (rev it));\<close>
|
||||
|
||||
|
||||
|
||||
assert*[aa::F] "\<forall>x::bool. X \<and> Y \<longrightarrow> True" (*problem with uni-code *)
|
||||
*)
|
||||
ML\<open>
|
||||
Syntax.read_term_global @{theory} "[@{termrepr ''True @<longrightarrow> True''}]";
|
||||
(* this only works because the isa check is not activated in "term" !!! *)
|
||||
@{term "[@{term '' True @<longrightarrow> True ''}]"}; (* with isa-check *)
|
||||
@{term "[@{termrepr '' True @<longrightarrow> True ''}]"}; (* without isa check *)
|
||||
\<close>
|
||||
(*
|
||||
ML\<open>val [_,_,Const _ $ s,_] = (HOLogic.dest_list @{docitem_attribute property :: aa});
|
||||
val t = HOLogic.dest_string s;
|
||||
holstring_to_bstring @{context} t
|
||||
\<close>
|
||||
*)
|
||||
|
||||
lemma "All (\<lambda>x. X \<and> Y \<longrightarrow> True)" oops
|
||||
|
||||
|
||||
text\<open>An example for the ontology specification character of the short-cuts such as
|
||||
@{command "assert*"}: in the following, we use the same notation referring to a completely
|
||||
different class. "F" and "assertion" have only in common that they posses the attribute
|
||||
\<^verbatim>\<open>property\<close>: \<close>
|
||||
@{const [names_short] \<open>properties\<close>}: \<close>
|
||||
|
||||
text\<open>Creation just like that: \<close>
|
||||
assert*[ababa::assertion] "3 < (4::int)"
|
||||
|
|
|
|||
|
|
@ -128,10 +128,10 @@ DOF_core.get_attribute_info "Conceptual.C" "z" @{theory};
|
|||
|
||||
|
||||
ML\<open>
|
||||
DOF_core.get_value_local "sdf" @{context};
|
||||
DOF_core.get_value_local "sdfg" @{context};
|
||||
DOF_core.get_value_local "dfgdfg" @{context};
|
||||
DOF_core.get_value_local "omega" @{context};
|
||||
DOF_core.value_of "sdf" \<^theory>;
|
||||
DOF_core.value_of "sdfg" \<^theory>;
|
||||
DOF_core.value_of "dfgdfg" \<^theory>;
|
||||
DOF_core.value_of "omega" \<^theory>;
|
||||
\<close>
|
||||
|
||||
text\<open>A not too trivial test: default y -> [].
|
||||
|
|
|
|||
|
|
@ -77,8 +77,10 @@ text-assert-error[test_monitor_A1::test_monitor_A]\<open>\<close>
|
|||
\<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M rejected\<close>
|
||||
declare[[strict_monitor_checking=false]]
|
||||
text*[test_monitor_A1::test_monitor_A]\<open>\<close> \<comment> \<open>the same in non-strict monitor checking.\<close>
|
||||
|
||||
text*[testFree2::test_monitor_free]\<open>\<close>
|
||||
declare[[free_class_in_monitor_strict_checking]]
|
||||
text-assert-error[testFree2::test_monitor_free]\<open>\<close>
|
||||
\<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M not enabled\<close>
|
||||
declare[[free_class_in_monitor_strict_checking=false]]
|
||||
text*[test_monitor_head1::test_monitor_head]\<open>\<close>
|
||||
text*[testFree3::test_monitor_free]\<open>\<close>
|
||||
text*[test_monitor_B1::test_monitor_B]\<open>\<close>
|
||||
|
|
@ -107,5 +109,19 @@ value*\<open>map fst @{trace-attribute \<open>test_monitor_M\<close>}\<close>
|
|||
|
||||
ML\<open>@{assert} ([("Conceptual.A", "test"), ("Conceptual.F", "sdfg")] = @{trace_attribute aaa}) \<close>
|
||||
|
||||
|
||||
open_monitor*[test_monitor_M3::monitor_M]
|
||||
|
||||
declare[[strict_monitor_checking]]
|
||||
text-assert-error[test_monitor_A2::test_monitor_A]\<open>\<close>
|
||||
\<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M3 rejected\<close>
|
||||
declare[[strict_monitor_checking=false]]
|
||||
text*[test_monitor_A3::test_monitor_A]\<open>\<close> \<comment> \<open>the same in non-strict monitor checking.\<close>
|
||||
declare[[free_class_in_monitor_strict_checking]]
|
||||
text-assert-error[testFree7::test_monitor_free]\<open>\<close>
|
||||
\<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M3 not enabled\<close>
|
||||
declare[[free_class_in_monitor_strict_checking=false]]
|
||||
|
||||
|
||||
end
|
||||
|
||||
|
|
|
|||
|
|
@ -0,0 +1,65 @@
|
|||
(*************************************************************************
|
||||
* 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
|
||||
*************************************************************************)
|
||||
|
||||
chapter\<open>Testing Nested Monitors\<close>
|
||||
|
||||
theory
|
||||
Concept_MonitorTest2
|
||||
imports
|
||||
Concept_MonitorTest1
|
||||
begin
|
||||
|
||||
section\<open>Test Purpose.\<close>
|
||||
text\<open> Creation of document parts that are controlled by (nested, locally defined) monitors. \<close>
|
||||
|
||||
doc_class monitor_M =
|
||||
tmM :: int
|
||||
rejects "test_monitor_B"
|
||||
accepts "test_monitor_E ~~ test_monitor_C"
|
||||
|
||||
doc_class test_monitor_head =
|
||||
tmhd :: int
|
||||
|
||||
declare[[free_class_in_monitor_checking]]
|
||||
|
||||
declare[[free_class_in_monitor_strict_checking]]
|
||||
text-assert-error[test_monitor_head1::test_monitor_head]\<open>\<close>
|
||||
\<open>accepts clause 1 of monitor Concept_MonitorTest1.test_monitor_M3 not enabled\<close>
|
||||
declare[[free_class_in_monitor_strict_checking=false]]
|
||||
text*[test_monitor_head2::Concept_MonitorTest1.test_monitor_head]\<open>\<close>
|
||||
|
||||
open_monitor*[test_monitor_M3::monitor_M]
|
||||
|
||||
text*[test_monitor_head3::Concept_MonitorTest1.test_monitor_head]\<open>\<close>
|
||||
text*[testFree3::test_monitor_free]\<open>\<close>
|
||||
declare[[strict_monitor_checking]]
|
||||
text-assert-error[test_monitor_B1::test_monitor_B]\<open>\<close>
|
||||
\<open>accepts clause 1 of monitor Concept_MonitorTest2.test_monitor_M3 rejected\<close>
|
||||
declare[[strict_monitor_checking=false]]
|
||||
text*[testFree4::test_monitor_free]\<open>\<close>
|
||||
declare[[strict_monitor_checking]]
|
||||
text-assert-error[test_monitor_D1::test_monitor_D]\<open>\<close>
|
||||
\<open>accepts clause 1 of monitor Concept_MonitorTest2.test_monitor_M3 rejected\<close>
|
||||
declare[[strict_monitor_checking=false]]
|
||||
text*[testFree5::test_monitor_free]\<open>\<close>
|
||||
text*[test_monitor_E1::test_monitor_E]\<open>\<close>
|
||||
text*[test_monitor_C1::test_monitor_C]\<open>\<close>
|
||||
text*[testFree6::test_monitor_free]\<open>\<close>
|
||||
|
||||
close_monitor*[Concept_MonitorTest1.test_monitor_M3]
|
||||
|
||||
close_monitor*[test_monitor_M3]
|
||||
|
||||
declare[[free_class_in_monitor_checking = false]]
|
||||
|
||||
end
|
||||
|
|
@ -55,27 +55,25 @@ print_doc_items
|
|||
section\<open>Term-Antiquotations Referring to \<^verbatim>\<open>thm\<close>‘s\<close>
|
||||
|
||||
text\<open>Some sample lemma:\<close>
|
||||
lemma*[l::E] murks : "Example = @{thm ''HOL.refl''}" oops
|
||||
lemma*[l::E] murks : "Example = @{thm ''refl''}" oops
|
||||
|
||||
text-assert-error\<open>... @{E "l"}\<close>\<open>Undefined instance:\<close> \<comment> \<open>oops retracts the ENTIRE system state,
|
||||
thus also the creation of an instance of E\<close>
|
||||
|
||||
lemma*[l::E] local_sample_lemma :
|
||||
"@{thm \<open>HOL.refl\<close>} = @{thm ''HOL.refl''}" by simp
|
||||
"@{thm \<open>refl\<close>} = @{thm ''refl''}" by simp
|
||||
\<comment> \<open>un-evaluated references are similar to
|
||||
uninterpreted constants. Not much is known
|
||||
about them, but that doesn't mean that we
|
||||
can't prove some basics over them...\<close>
|
||||
|
||||
|
||||
(* BUG: Why does this not work ? Shortnames are apparently not recognized !*)
|
||||
(* SHOULD WORK :
|
||||
lemma*[l2::E] local_sample_lemma :
|
||||
lemma*[l2::E] local_sample_lemma2 :
|
||||
"@{thm ''local_sample_lemma''} = @{thm ''local_sample_lemma''}" by simp
|
||||
*)
|
||||
|
||||
value*\<open>@{thm ''Concept_TermAntiquotations.local_sample_lemma''}\<close>
|
||||
value-assert-error\<open> @{thm ''Conept_TermAntiquotations.local_sample_lemma''}\<close>\<open>No Theorem\<close>
|
||||
|
||||
value*\<open>@{thm ''local_sample_lemma''}\<close>
|
||||
value-assert-error\<open> @{thm \<open>Conxept_TermAntiquotations.local_sample_lemma\<close>}\<close>\<open>Undefined fact\<close>
|
||||
|
||||
section\<open>Testing the Standard ("Built-in") Term-Antiquotations\<close>
|
||||
|
||||
|
|
@ -104,13 +102,11 @@ section\<open>Other Built-In Term Antiquotations\<close>
|
|||
text-assert-error[ae::text_element]\<open>@{file "non-existing.thy"}\<close>\<open>No such file: \<close>
|
||||
text\<open>A text-antiquotation from Main: @{file "TestKit.thy"}\<close>
|
||||
|
||||
(* BUG : This shoulöd work rather than throw an exception *)
|
||||
value-assert-error\<open>@{file \<open>TestKit.thy\<close>}\<close>\<open>No such file: \<close>
|
||||
text-assert-error\<open>A text-antiquotation from Main: @{file "TestKit.thy"}\<close>
|
||||
value-assert-error\<open>@{file \<open>non-existing.thy\<close>}\<close>\<open>No such file: \<close>
|
||||
value*\<open>@{file \<open>TestKit.thy\<close>}\<close>
|
||||
|
||||
(* BUG. Again: Long-name Short Name on Files ?
|
||||
text*[xcv::F, u="@{file ''TestKit.thy''}"]\<open>Lorem ipsum ...\<close>
|
||||
*)
|
||||
|
||||
|
||||
value*\<open>@{term \<open>aa + bb\<close>}\<close>
|
||||
value*\<open>@{typ \<open>'a list\<close>}\<close>
|
||||
|
|
|
|||
|
|
@ -26,18 +26,18 @@ text\<open> Creation of ontological instances along the \<^theory>\<open>Isabell
|
|||
Ontology. Emphasis is put on type-safe (ontologically consistent) referencing of text, code and
|
||||
proof elements. Some tests cover also the critical cases concerning name spaces of oid's. \<close>
|
||||
|
||||
(*
|
||||
|
||||
section\<open>\<^theory_text>\<open>ML*\<close>-Annotated SML-commands\<close>
|
||||
|
||||
ML*[thefunction::B,x=\<open>\<open>dfg\<close>\<close>]\<open>fun fac x = if x = 0 then 1 else x * fac(x-1);
|
||||
val t = \<^value_>\<open>x @{B \<open>thefunction\<close>}\<close>\<close>
|
||||
ML\<open>fac 5; t\<close> \<comment> \<open>this is a test that ML* is actually evaluated and the
|
||||
resulting toplevel state is preserved.\<close>
|
||||
text-macro*[the::C]\<open> @{B [display] "thefunction"} \<close>
|
||||
text*[the::C]\<open> @{B "thefunction"} \<close>
|
||||
|
||||
text\<open>... and here we reference @{B \<open>thefunction\<close>}.\<close>
|
||||
|
||||
text\<open>... and here we reference @{B [display] \<open>thefunction\<close>}.\<close>
|
||||
|
||||
*)
|
||||
|
||||
section\<open>\<^theory_text>\<open>value*\<close>-Annotated evaluation-commands\<close>
|
||||
|
||||
|
|
@ -54,13 +54,6 @@ Some built-ins remain as unspecified constants:
|
|||
\<^item> the docitem TA offers a way to check the reference of class instances
|
||||
without checking the instances type.
|
||||
It must be avoided for certification
|
||||
\<^item> the termrepr TA is left as unspecified constant for now.
|
||||
A major refactoring of code should be done to enable
|
||||
referential equivalence for termrepr, by changing the dependency
|
||||
between the Isa-DOF theory and the Assert theory.
|
||||
The assert-cmd function in Assert should use the value* command
|
||||
functions, which make the elaboration of the term
|
||||
referenced by the TA before passing it to the evaluator
|
||||
|
||||
We also have the possibility to make some requests on classes instances, i.e. on docitems
|
||||
by specifying the doc class.
|
||||
|
|
@ -134,13 +127,13 @@ used in the \<open>b\<close> attribute will be checked, and the type of these cl
|
|||
\<close>
|
||||
value* \<open>@{F \<open>xcv4\<close>}\<close>
|
||||
|
||||
(*
|
||||
|
||||
text\<open>If we want the classes to be checked,
|
||||
we can use the TA which will also check the type of the instances.
|
||||
The instance @{A \<open>xcv3\<close>} is of type @{typ "A"} and the instance @{C \<open>xcv2\<close>} is of type @{typ "C"}:
|
||||
\<close>
|
||||
update_instance*[xcv4::F, b+="{(@{A ''xcv3''},@{C ''xcv2''})}"]
|
||||
*)
|
||||
|
||||
text\<open>Using a TA in terms is possible, and the term is evaluated:\<close>
|
||||
value*\<open>[@{thm \<open>HOL.refl\<close>}, @{thm \<open>HOL.refl\<close>}]\<close>
|
||||
value*\<open>@{thm ''HOL.refl''} = @{thm (''HOL.refl'')}\<close>
|
||||
|
|
@ -207,12 +200,12 @@ It uses the same implementation as the \<^emph>\<open>value*\<close>-command and
|
|||
|
||||
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants\<close>
|
||||
we can check logical statements:\<close>
|
||||
(*
|
||||
term*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>authored_by @{introduction \<open>introduction2\<close>} = authored_by @{introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>\<not>(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>
|
||||
assert*\<open>authored_by @{Introduction \<open>introduction2\<close>} = authored_by @{Introduction \<open>introduction3\<close>}\<close>
|
||||
assert*\<open>\<not>(authored_by @{Introduction \<open>introduction2\<close>}
|
||||
= authored_by @{Introduction \<open>introduction4\<close>})\<close>
|
||||
|
||||
text\<open>Assertions must be boolean expressions, so the following assertion triggers an error:\<close>
|
||||
(* Error:
|
||||
assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
|
||||
|
|
@ -220,19 +213,19 @@ assert*\<open>@{introduction \<open>introduction2\<close>}\<close>*)
|
|||
text\<open>Assertions must be true, hence the error:\<close>
|
||||
(* Error:
|
||||
assert*\<open>{@{author \<open>curry\<close>}} = {@{author \<open>church\<close>}}\<close>*)
|
||||
(*
|
||||
|
||||
term*\<open>property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
assert*[assertionA::A]\<open>\<not> property @{result \<open>resultProof\<close>} = property @{result \<open>resultProof2\<close>}\<close>
|
||||
|
||||
text-macro*[assertionAA::A]\<open>@{A [display] "assertionA"}\<close>
|
||||
text\<open>... and here we reference @{A [display] \<open>assertionA\<close>}.\<close>
|
||||
text*[assertionAA::A]\<open>@{A "assertionA"}\<close>
|
||||
text\<open>... and here we reference @{A \<open>assertionA\<close>}.\<close>
|
||||
|
||||
assert*\<open>evidence @{result \<open>resultProof\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||
*)
|
||||
|
||||
text\<open>The optional evaluator of \<open>value*\<close> and \<open>assert*\<close> must be specified after the meta arguments:\<close>
|
||||
value* [optional_test_A::A, x=6] [nbe] \<open>filter (\<lambda>\<sigma>. A.x \<sigma> > 5) @{A-instances}\<close>
|
||||
(*
|
||||
|
||||
assert* [resultProof3::result, evidence = "proof", property="[@{thm \<open>HOL.sym\<close>}]"] [nbe]
|
||||
\<open>evidence @{result \<open>resultProof3\<close>} = evidence @{result \<open>resultProof2\<close>}\<close>
|
||||
*)
|
||||
|
||||
end
|
||||
|
|
|
|||
|
|
@ -51,7 +51,7 @@ text-[asd::B]
|
|||
\textbf{TEST}
|
||||
@{cartouche [display]
|
||||
\<open>text*[dfgdfg::B]
|
||||
\<open> Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
|
||||
\<open> Lorem ipsum ... @{thm refl} Frederic \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
|
||||
\<close>}
|
||||
\<close>
|
||||
|
||||
|
|
@ -60,10 +60,9 @@ text-latex\<open>... and here is its application macro expansion:
|
|||
\textbf{TEST}
|
||||
@{cartouche [display]
|
||||
\<open>text*[dfgdfg::B]
|
||||
\<open> Lorem ipsum ... @{thm refl} Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>
|
||||
\<open> Lorem ipsum ... @{thm refl} Fr\'ed\'eric \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
|
||||
|
|
@ -73,12 +72,11 @@ text-latex\<open> \<^theory_text>\<open>definition df = ...
|
|||
\<close>}
|
||||
|
||||
@{verbatim [display] \<open> Lorem ipsum ... @{thm refl}
|
||||
Frédéric \textbf{TEST} \verb+sdf+ \<open>dfgdfg\<close> \<close>}
|
||||
Fr\'ed\'eric \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
|
||||
|
|
|
|||
|
|
@ -7,6 +7,7 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
|
|||
"Concept_Example_Low_Level_Invariant"
|
||||
"Concept_High_Level_Invariants"
|
||||
"Concept_MonitorTest1"
|
||||
"Concept_MonitorTest2"
|
||||
"Concept_TermAntiquotations"
|
||||
"Attributes"
|
||||
"Evaluation"
|
||||
|
|
|
|||
|
|
@ -126,10 +126,8 @@ fun error_match2 [_, src] msg = error_match src msg
|
|||
val _ =
|
||||
Outer_Syntax.command ("text-assert-error", @{here}) "formal comment macro"
|
||||
(ODL_Meta_Args_Parser.opt_attributes -- Parse.opt_target -- Scan.repeat1 Parse.document_source
|
||||
>> (Toplevel.theory o
|
||||
(fn ((meta_args, xstring_opt), source) =>
|
||||
(gen_enriched_document_command3 error_match2 "TTT" {body=true}
|
||||
I I {markdown = true} ((meta_args, xstring_opt), source)))));
|
||||
>> (Toplevel.theory o (gen_enriched_document_command3 error_match2 "TTT" {body=true}
|
||||
I I {markdown = true} )));
|
||||
|
||||
fun update_instance_command (args,src) thy =
|
||||
(Monitor_Command_Parser.update_instance_command args thy
|
||||
|
|
@ -195,4 +193,3 @@ text-latex\<open>dfg\<close>
|
|||
text-assert-error[aaaa::A]\<open> @{A \<open>sdf\<close>}\<close>\<open>reference ontologically inconsistent\<close>
|
||||
|
||||
end
|
||||
(*>*)
|
||||
|
|
|
|||
File diff suppressed because it is too large
Load Diff
|
|
@ -87,9 +87,10 @@ not make use of a file called \<^verbatim>\<open>document/root.tex\<close>. Inst
|
|||
ontology represenations is done within theory files. To make use of this feature, one needs
|
||||
to add the option \<^verbatim>\<open>document_build = dof\<close> to the \<^verbatim>\<open>ROOT\<close> file.
|
||||
An example \<^verbatim>\<open>ROOT\<close> file looks as follows:
|
||||
|
||||
\<close>
|
||||
text\<open>
|
||||
\begin{config}{ROOT}
|
||||
session example = HOL +
|
||||
session example = Isabelle_DOF +
|
||||
options [document = pdf, document_output = "output", document_build = dof]
|
||||
(*theories [document = false]
|
||||
A
|
||||
|
|
@ -102,8 +103,19 @@ session example = HOL +
|
|||
The document template and ontology can be selected as follows:
|
||||
@{boxed_theory_text [display]
|
||||
\<open>
|
||||
use_template "scrreprt-modern"
|
||||
theory
|
||||
C
|
||||
imports
|
||||
Isabelle_DOF.technical_report
|
||||
Isabelle_DOF.scholarly_paper
|
||||
begin
|
||||
|
||||
list_templates
|
||||
use_template "scrreprt-modern"
|
||||
list_ontologies
|
||||
use_ontology "technical_report" and "scholarly_paper"
|
||||
|
||||
end
|
||||
\<close>}
|
||||
|
||||
The commands @{boxed_theory_text
|
||||
|
|
@ -120,8 +132,37 @@ can be used for inspecting (and selecting) the available ontologies and template
|
|||
list_templates
|
||||
list_ontologies
|
||||
\<close>}
|
||||
|
||||
Note that you need to import the theories that define the ontologies that you
|
||||
want to use. Otherwise, they will not be available.
|
||||
\<close>
|
||||
|
||||
paragraph\<open>Warning.\<close>
|
||||
text\<open>
|
||||
Note that the session @{session "Isabelle_DOF"} needs to be part of the ``main'' session
|
||||
hierarchy. Loading the Isabelle/DOF theories as part of a session section, e.g.,
|
||||
\<close>
|
||||
text\<open>
|
||||
\begin{config}{ROOT}
|
||||
session example = HOL +
|
||||
options [document = pdf, document_output = "output", document_build = dof]
|
||||
session
|
||||
Isabelle_DOF.scholarly_paper
|
||||
Isabelle_DOF.technical_report
|
||||
theories
|
||||
C
|
||||
\end{config}
|
||||
\<close>
|
||||
text\<open>
|
||||
will not work. Trying to build a document using such a setup will result in the
|
||||
following error message:
|
||||
|
||||
@{boxed_bash [display]\<open>ë\prompt{}ë
|
||||
isabelle build -D .
|
||||
Running example ...
|
||||
Bad document_build engine "dof"
|
||||
example FAILED\<close>}
|
||||
\<close>
|
||||
|
||||
subsection*[naming::example]\<open>Name-Spaces, Long- and Short-Names\<close>
|
||||
text\<open>\<^isadof> is built upon the name space and lexical conventions of Isabelle. Long-names were
|
||||
|
|
|
|||
|
|
@ -72,7 +72,7 @@ foo@bar:~$ isabelle build -d . -o 'timeout_scale=2' Isabelle_DOF-Proofs
|
|||
## Usage
|
||||
|
||||
In the following, we assume that you installed Isabelle/DOF either from the AFP
|
||||
(adding the AFP as a component to your Isabelle system) or from the GIT
|
||||
(adding the AFP as a component to your Isabelle system) or from the Git
|
||||
repository of Isabelle/DOF (installing Isabelle/DOF as a component to your
|
||||
Isabelle system).
|
||||
|
||||
|
|
|
|||
|
|
@ -5,7 +5,9 @@ requirements = \
|
|||
env:ISABELLE_SCALA_JAR
|
||||
sources = \
|
||||
Isabelle_DOF/scala/dof.scala \
|
||||
Isabelle_DOF/scala/dof_document_build.scala \
|
||||
scala/dof_mkroot.scala \
|
||||
scala/dof_tools.scala
|
||||
services = \
|
||||
isabelle.dof.DOF_Tools
|
||||
isabelle.dof.DOF_Tools \
|
||||
isabelle.dof.DOF_Document_Build$Engine
|
||||
|
|
|
|||
Loading…
Reference in New Issue