added value-assert to TestKit, improved Concept_TermAntiquotations. Still TODO's.
This commit is contained in:
Burkhart Wolff
parent
af096e56fc
commit
94543a86e4
|
|
@ -143,10 +143,15 @@ ML\<open>val ctxt = @{context}
|
|||
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
|
||||
fun conv' (\<^Const>\<open>Pair \<^typ>\<open>doc_class rexp\<close> \<^typ>\<open>string\<close>\<close>
|
||||
$ (\<^Const>\<open>Atom \<^typ>\<open>doc_class\<close>\<close> $ (\<^Const>\<open>mk\<close> $ s)) $ S) =
|
||||
let val s' = DOF_core.get_onto_class_name_global' (HOLogic.dest_string s)
|
||||
(Proof_Context.theory_of ctxt)
|
||||
let val s' = DOF_core.get_onto_class_name_global'
|
||||
(HOLogic.dest_string s)
|
||||
(Proof_Context.theory_of ctxt)
|
||||
in (s', HOLogic.dest_string S) end
|
||||
val string_pair_list = map conv' (HOLogic.dest_list term)
|
||||
val string_pair_list = map conv' (HOLogic.dest_list term);
|
||||
@{assert} (string_pair_list =
|
||||
[("Conceptual.A", "a"), ("Conceptual.C", "c1"),
|
||||
("Conceptual.E", "d1"), ("Conceptual.C", "c2"),
|
||||
("Conceptual.E", "f")])
|
||||
\<close>
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -1,7 +1,7 @@
|
|||
(*************************************************************************
|
||||
* Copyright (C)
|
||||
* 2019 The University of Exeter
|
||||
* 2018-2019 The University of Paris-Saclay
|
||||
* 2019-2023 The University of Exeter
|
||||
* 2018-2023 The University of Paris-Saclay
|
||||
* 2018 The University of Sheffield
|
||||
*
|
||||
* License:
|
||||
|
|
@ -18,47 +18,72 @@ For historical reasons, \<^emph>\<open>term antiquotations\<close> are called th
|
|||
"Inner Syntax Antiquotations". \<close>
|
||||
|
||||
theory
|
||||
TermAntiquotations
|
||||
Concept_TermAntiquotations
|
||||
imports
|
||||
"Isabelle_DOF-Unit-Tests_document"
|
||||
"Isabelle_DOF-Ontologies.Conceptual"
|
||||
TestKit
|
||||
begin
|
||||
|
||||
section\<open>Context\<close>
|
||||
|
||||
text\<open>Since the syntax chosen for values of doc-class attributes is HOL-syntax --- requiring
|
||||
a fast read on the ``What's in Main''-documentation, but not additional knowledge on, say, SML ---
|
||||
an own syntax for references to types, terms, theorems, etc. are necessary. These are the
|
||||
``Inner Syntax Antiquotations'' since they make only sense \emph{inside} the Inner-Syntax
|
||||
of Isabelle/Isar, so inside the \verb+" ... "+ parenthesis.
|
||||
a fast read on the ``What's in Main''-documentation, but not additional knowledge on, say,
|
||||
SML --- an own syntax for references to types, terms, theorems, etc. are necessary. These are
|
||||
the ``Term Antiquotations'' (in earlier papers also called: ``Inner Syntax Antiquotations'').
|
||||
|
||||
They are the key-mechanism to denote
|
||||
\<^item> Ontological Links, i.e. attributes refering to document classes defined by the ontology
|
||||
\<^item> Ontological F-Links, i.e. attributes referring to formal entities inside Isabelle (such as thm's)
|
||||
|
||||
This file contains a number of examples resulting from the
|
||||
% @ {theory "Isabelle_DOF-Unit-Tests.Conceptual"} does not work here --- why ?
|
||||
\<^theory_text>\<open>Conceptual\<close> - ontology; the emphasis of this presentation is to present the expressivity of
|
||||
ODL on a paradigmatical example.
|
||||
@{theory "Isabelle_DOF-Ontologies.Conceptual"} - ontology; the emphasis of this presentation is to
|
||||
present the expressivity of ODL on a paradigmatical example.
|
||||
\<close>
|
||||
|
||||
|
||||
text\<open>Voila the content of the Isabelle/DOF environment so far:\<close>
|
||||
ML\<open>
|
||||
val x = 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 isa_transformer_tab;
|
||||
\<close>
|
||||
section\<open>Test Purpose.\<close>
|
||||
|
||||
text\<open>Testing Standard Term-Antiquotations and Code-Term-Antiquotations. \<close>
|
||||
|
||||
text\<open>Just a check of the status DOF core: observe that no new classes have been defined.\<close>
|
||||
|
||||
print_doc_classes
|
||||
print_doc_items
|
||||
|
||||
|
||||
section\<open>Term-Antiquotations Referring to \<^verbatim>\<open>thm\<close>‘s\<close>
|
||||
|
||||
text\<open>Some sample lemma:\<close>
|
||||
lemma murks : "Example=Example" by simp
|
||||
lemma*[l::E] murks : "Example = @{thm ''HOL.refl''}" oops
|
||||
|
||||
text\<open>Example for a meta-attribute of ODL-type @{typ "file"} with an appropriate ISA for the
|
||||
file @{file "TermAntiquotations.thy"}\<close>
|
||||
(* not working:
|
||||
text*[xcv::F, u="@{file ''InnerSyntaxAntiquotations.thy''}"]\<open>Lorem ipsum ...\<close>
|
||||
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
|
||||
\<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 :
|
||||
"@{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>
|
||||
|
||||
section\<open>Testing the Standard ("Built-in") Term-Antiquotations\<close>
|
||||
|
||||
text\<open>Example for a meta-attribute of ODL-type @{typ "file"} with an
|
||||
appropriate ISA for the file @{file "Concept_TermAntiquotations.thy"}\<close>
|
||||
|
||||
|
||||
|
||||
text*[xcv1::A, x=5]\<open>Lorem ipsum ...\<close>
|
||||
text*[xcv3::A, x=7]\<open>Lorem ipsum ...\<close>
|
||||
|
||||
|
|
@ -75,10 +100,28 @@ But it may give rise to unwanted behaviors, due to its polymorphic type.
|
|||
It must not be used for certification.
|
||||
\<close>
|
||||
|
||||
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>
|
||||
|
||||
(* 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>
|
||||
|
||||
|
||||
section\<open>Putting everything together\<close>
|
||||
|
||||
text\<open>Major sample: test-item of doc-class \<open>F\<close> with a relational link between class instances,
|
||||
and links to formal Isabelle items like \<open>typ\<close>, \<open>term\<close> and \<open>thm\<close>. \<close>
|
||||
text*[xcv4::F, r="[@{thm ''HOL.refl''},
|
||||
@{thm \<open>TermAntiquotations.murks\<close>}]", (* long names required *)
|
||||
@{thm \<open>Concept_TermAntiquotations.local_sample_lemma\<close>}]", (* long names required *)
|
||||
b="{(@{docitem ''xcv1''},@{docitem \<open>xcv2\<close>})}", (* notations \<open>...\<close> vs. ''...'' *)
|
||||
s="[@{typ \<open>int list\<close>}]",
|
||||
properties = "[@{term \<open>H \<longrightarrow> H\<close>}]" (* notation \<open>...\<close> required for UTF8*)
|
||||
|
|
|
|||
|
|
@ -7,7 +7,7 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
|
|||
"Concept_Example_Low_Level_Invariant"
|
||||
"Concept_High_Level_Invariants"
|
||||
"Concept_MonitorTest1"
|
||||
"TermAntiquotations"
|
||||
"Concept_TermAntiquotations"
|
||||
"Attributes"
|
||||
"Evaluation"
|
||||
"AssnsLemmaThmEtc"
|
||||
|
|
|
|||
|
|
@ -116,7 +116,7 @@ fun gen_enriched_document_command3 assert name body trans at md (margs, src_list
|
|||
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)
|
||||
fun error_match src msg = (String.isPrefix (Input.string_of src) msg)
|
||||
|
||||
fun error_match2 [_, src] msg = error_match src msg
|
||||
| error_match2 _ _ = error "Wrong text-assertion-error. Argument format <arg><match> required."
|
||||
|
|
@ -142,7 +142,7 @@ val _ =
|
|||
>> (Toplevel.theory o update_instance_command));
|
||||
|
||||
val _ =
|
||||
let fun create_and_check_docitem ((((oid, pos),cid_pos),doc_attrs),src) thy=
|
||||
let fun create_and_check_docitem ((((oid, pos),cid_pos),doc_attrs),src) thy =
|
||||
(Value_Command.Docitem_Parser.create_and_check_docitem
|
||||
{is_monitor = false} {is_inline=true}
|
||||
{define = false} oid pos (cid_pos) (doc_attrs) thy)
|
||||
|
|
@ -156,23 +156,34 @@ val _ =
|
|||
end;
|
||||
|
||||
|
||||
(* fun pass_trans_to_value_cmd args ((name, modes), t) trans =
|
||||
let val pos = Toplevel.pos_of trans
|
||||
in
|
||||
trans |> Toplevel.theory (value_cmd {assert=false} args name modes t @{here})
|
||||
end
|
||||
*)
|
||||
|
||||
val _ =
|
||||
let fun pass_trans_to_value_cmd (args, (((name, modes), t),src)) trans =
|
||||
(Value_Command.value_cmd {assert=false} args name modes t @{here} trans
|
||||
handle ERROR msg => (if error_match src msg
|
||||
then (writeln ("Correct error: "^msg^": reported.");trans)
|
||||
else error"Wrong error reported"))
|
||||
in Outer_Syntax.command \<^command_keyword>\<open>value-assert-error\<close> "evaluate and print term"
|
||||
(ODL_Meta_Args_Parser.opt_attributes --
|
||||
(Value_Command.opt_evaluator
|
||||
-- Value_Command.opt_modes
|
||||
-- Parse.term
|
||||
-- Parse.document_source)
|
||||
>> (Toplevel.theory o pass_trans_to_value_cmd))
|
||||
end;
|
||||
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command ("text-latex", \<^here>) "formal comment (primary style)"
|
||||
(Parse.opt_target -- Parse.document_source >> document_command2 {markdown = true});
|
||||
|
||||
|
||||
val _ =
|
||||
let fun pass_trans_to_value_cmd(args, (parms, src)) state =
|
||||
(Value_Command.pass_trans_to_value_cmd args parms state
|
||||
handle ERROR msg => (if error_match src msg
|
||||
then (writeln ("Correct error: "^msg^": reported.");state)
|
||||
else error"Wrong error reported"))
|
||||
in Outer_Syntax.command \<^command_keyword>\<open>value-assert-error\<close> "evaluate and print term"
|
||||
(ODL_Meta_Args_Parser.opt_attributes --
|
||||
(Value_Command.opt_evaluator -- Value_Command.opt_modes -- Parse.term -- Parse.document_source)
|
||||
>> (pass_trans_to_value_cmd))
|
||||
end;
|
||||
|
||||
|
||||
\<close>
|
||||
|
|
|
|||
Loading…
Reference in New Issue