Merge branch 'main' of git.logicalhacking.com:Isabelle_DOF/Isabelle_DOF
ci/woodpecker/push/build Pipeline was successful
Details
ci/woodpecker/push/build Pipeline was successful
Details
This commit is contained in:
commit
ecb1e88b78
|
|
@ -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>
|
||||
|
||||
|
||||
|
|
|
|||
|
|
@ -11,9 +11,9 @@
|
|||
* SPDX-License-Identifier: BSD-2-Clause
|
||||
*************************************************************************)
|
||||
|
||||
chapter\<open>High level syntax Invariants\<close>
|
||||
chapter\<open>High-level Class Invariants\<close>
|
||||
|
||||
theory High_Level_Syntax_Invariants
|
||||
theory Concept_High_Level_Invariants
|
||||
imports "Isabelle_DOF.Isa_DOF"
|
||||
"Isabelle_DOF-Unit-Tests_document"
|
||||
TestKit
|
||||
|
|
@ -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,45 +18,69 @@ 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 ''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>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>
|
||||
|
||||
|
||||
lemma*[l2::E] local_sample_lemma2 :
|
||||
"@{thm ''local_sample_lemma''} = @{thm ''local_sample_lemma''}" by simp
|
||||
|
||||
|
||||
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>
|
||||
|
||||
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\<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*[xcv1::A, x=5]\<open>Lorem ipsum ...\<close>
|
||||
text*[xcv3::A, x=7]\<open>Lorem ipsum ...\<close>
|
||||
|
|
@ -74,10 +98,26 @@ 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>
|
||||
|
||||
value-assert-error\<open>@{file \<open>non-existing.thy\<close>}\<close>\<open>No such file: \<close>
|
||||
value*\<open>@{file \<open>TestKit.thy\<close>}\<close>
|
||||
|
||||
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*)
|
||||
|
|
@ -5,9 +5,9 @@ text\<open>Term Annotation Antiquotations (TA) can be evaluated with the help of
|
|||
theory
|
||||
Evaluation
|
||||
imports
|
||||
"Isabelle_DOF-Unit-Tests.TermAntiquotations"
|
||||
"Isabelle_DOF-Unit-Tests.High_Level_Syntax_Invariants"
|
||||
|
||||
"Isabelle_DOF-Unit-Tests.Concept_TermAntiquotations"
|
||||
"Isabelle_DOF-Unit-Tests.Concept_High_Level_Invariants"
|
||||
TestKit
|
||||
begin
|
||||
|
||||
(*
|
||||
|
|
@ -187,7 +187,7 @@ text\<open>The \<^emph>\<open>assert*\<close>-command allows for logical stateme
|
|||
It uses the same implementation as the \<^emph>\<open>value*\<close>-command and has the same limitations.
|
||||
\<close>
|
||||
|
||||
text\<open>Using the ontology defined in \<^theory>\<open>Isabelle_DOF-Unit-Tests.High_Level_Syntax_Invariants\<close>
|
||||
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>
|
||||
|
|
|
|||
|
|
@ -5,12 +5,12 @@ session "Isabelle_DOF-Unit-Tests" = "Isabelle_DOF-Ontologies" +
|
|||
"Latex_Tests"
|
||||
"Concept_OntoReferencing"
|
||||
"Concept_Example_Low_Level_Invariant"
|
||||
"Concept_High_Level_Invariants"
|
||||
"Concept_MonitorTest1"
|
||||
"TermAntiquotations"
|
||||
"Concept_TermAntiquotations"
|
||||
"Attributes"
|
||||
"Evaluation"
|
||||
"AssnsLemmaThmEtc"
|
||||
"High_Level_Syntax_Invariants"
|
||||
"Ontology_Matching_Example"
|
||||
"Cenelec_Test"
|
||||
"OutOfOrderPresntn"
|
||||
|
|
|
|||
|
|
@ -20,6 +20,7 @@ keywords "text-" "text-latex" :: document_body
|
|||
and "text-assert-error" :: document_body
|
||||
and "update_instance-assert-error" :: document_body
|
||||
and "declare_reference-assert-error" :: document_body
|
||||
and "value-assert-error" :: document_body
|
||||
|
||||
begin
|
||||
|
||||
|
|
@ -114,7 +115,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."
|
||||
|
|
@ -123,10 +124,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
|
||||
|
|
@ -140,7 +139,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)
|
||||
|
|
@ -154,11 +153,36 @@ 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});
|
||||
|
||||
|
||||
|
||||
|
||||
\<close>
|
||||
|
||||
(* auto-tests *)
|
||||
|
|
|
|||
|
|
@ -487,8 +487,8 @@ struct
|
|||
|
||||
|
||||
datatype monitor_info = Monitor_Info of
|
||||
{accepted_cids : string list,
|
||||
rejected_cids : string list,
|
||||
{accepted_cids : RegExpInterface.env,
|
||||
rejected_cids : RegExpInterface.env,
|
||||
automatas : RegExpInterface.automaton list}
|
||||
|
||||
|
||||
|
|
@ -753,14 +753,11 @@ fun check_invs get_ml_invs cid_long oid is_monitor thy =
|
|||
|> map (fn check => check oid is_monitor ctxt)
|
||||
in (fold_and checks) end)
|
||||
|
||||
fun check_ml_invs cid_long oid is_monitor thy =
|
||||
check_invs get_ml_invariants cid_long oid is_monitor thy
|
||||
val check_ml_invs = check_invs get_ml_invariants
|
||||
|
||||
fun check_opening_ml_invs cid_long oid is_monitor thy =
|
||||
check_invs get_opening_ml_invariants cid_long oid is_monitor thy
|
||||
val check_opening_ml_invs = check_invs get_opening_ml_invariants
|
||||
|
||||
fun check_closing_ml_invs cid_long oid is_monitor thy =
|
||||
check_invs get_closing_ml_invariants cid_long oid is_monitor thy
|
||||
val check_closing_ml_invs = check_invs get_closing_ml_invariants
|
||||
|
||||
val ISA_prefix = "Isabelle_DOF_"
|
||||
|
||||
|
|
@ -1028,18 +1025,13 @@ fun ML_isa_check_term thy (term, _, pos) _ =
|
|||
|
||||
|
||||
fun ML_isa_check_thm thy (term, _, pos) _ =
|
||||
(* this works for long-names only *)
|
||||
let fun check thy (name, _) = case Proof_Context.lookup_fact (Proof_Context.init_global thy) name of
|
||||
NONE => err ("No Theorem:" ^name) pos
|
||||
| SOME X => X
|
||||
let fun check thy (name, _) = Global_Theory.check_fact thy (name, Position.none)
|
||||
in ML_isa_check_generic check thy (term, pos) end
|
||||
|
||||
|
||||
fun ML_isa_check_file thy (term, _, pos) _ =
|
||||
let fun check thy (name, pos) = check_path (SOME File.check_file)
|
||||
(Proof_Context.init_global thy)
|
||||
(Path.current)
|
||||
(name, pos);
|
||||
let fun check thy (name, pos) = name |> Syntax.read_input
|
||||
|> Resources.check_file (Proof_Context.init_global thy) NONE
|
||||
in ML_isa_check_generic check thy (term, pos) end;
|
||||
|
||||
fun check_instance thy (term, _, pos) s =
|
||||
|
|
@ -1788,19 +1780,24 @@ fun create_and_check_docitem is_monitor {is_inline=is_inline} {define=define} oi
|
|||
|> value (Proof_Context.init_global thy),
|
||||
is_inline, cid_long, vcid))
|
||||
|> register_oid_cid_in_open_monitors oid pos cid_pos'
|
||||
|> tap (DOF_core.check_opening_ml_invs cid_long oid is_monitor)
|
||||
|> tap (DOF_core.check_ml_invs cid_long oid is_monitor)
|
||||
(* Bypass checking of high-level invariants when the class default_cid = "text",
|
||||
the top (default) document class.
|
||||
We want the class default_cid to stay abstract
|
||||
and not have the capability to be defined with attribute, invariants, etc.
|
||||
Hence this bypass handles docitem without a class associated,
|
||||
for example when you just want a document element to be referenceable
|
||||
without using the burden of ontology classes.
|
||||
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> *)
|
||||
|> (fn thy => if default_cid then thy
|
||||
else if Config.get_global thy DOF_core.invariants_checking
|
||||
then check_invariants thy (oid, pos) else thy)
|
||||
|> (fn thy =>
|
||||
if (* declare_reference* without arguments is not checked against invariants *)
|
||||
thy |> DOF_core.get_defined_global oid |> not
|
||||
andalso null doc_attrs
|
||||
then thy
|
||||
else thy |> tap (DOF_core.check_opening_ml_invs cid_long oid is_monitor)
|
||||
|> tap (DOF_core.check_ml_invs cid_long oid is_monitor)
|
||||
(* Bypass checking of high-level invariants when the class default_cid = "text",
|
||||
the top (default) document class.
|
||||
We want the class default_cid to stay abstract
|
||||
and not have the capability to be defined with attribute, invariants, etc.
|
||||
Hence this bypass handles docitem without a class associated,
|
||||
for example when you just want a document element to be referenceable
|
||||
without using the burden of ontology classes.
|
||||
ex: text*[sdf]\<open> Lorem ipsum @{thm refl}\<close> *)
|
||||
|> (fn thy => if default_cid then thy
|
||||
else if Config.get_global thy DOF_core.invariants_checking
|
||||
then check_invariants thy (oid, pos) else thy))
|
||||
end
|
||||
|
||||
end (* structure Docitem_Parser *)
|
||||
|
|
@ -1904,18 +1901,18 @@ val _ = Toplevel.theory_toplevel
|
|||
(* setup ontology aware commands *)
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>term*\<close> "read and print term"
|
||||
(ODL_Meta_Args_Parser.opt_attributes -- (opt_modes -- Parse.term)
|
||||
>> (fn (meta_args_opt, eval_args ) => print_term meta_args_opt eval_args));
|
||||
(ODL_Meta_Args_Parser.opt_attributes -- (opt_modes -- Parse.term)
|
||||
>> (uncurry print_term));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>value*\<close> "evaluate and print term"
|
||||
(ODL_Meta_Args_Parser.opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term)
|
||||
>> (fn (meta_args_opt, eval_args ) => pass_trans_to_value_cmd meta_args_opt eval_args));
|
||||
>> (uncurry pass_trans_to_value_cmd));
|
||||
|
||||
val _ =
|
||||
Outer_Syntax.command \<^command_keyword>\<open>assert*\<close> "evaluate and assert term"
|
||||
(ODL_Meta_Args_Parser.opt_attributes -- (opt_evaluator -- opt_modes -- Parse.term)
|
||||
>> (fn (meta_args_opt, eval_args ) => pass_trans_to_assert_value_cmd meta_args_opt eval_args));
|
||||
>> (uncurry pass_trans_to_assert_value_cmd));
|
||||
|
||||
|
||||
(* setup ontology - aware text and ML antiquotations. Due to lexical restrictions, we can not
|
||||
|
|
@ -1944,7 +1941,7 @@ end
|
|||
(* setup evaluators *)
|
||||
val _ = Theory.setup(
|
||||
add_evaluator (\<^binding>\<open>simp\<close>, Code_Simp.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>nbe\<close>, Nbe.dynamic_value) #> snd
|
||||
#> add_evaluator (\<^binding>\<open>code\<close>, Code_Evaluation.dynamic_value_strict) #> snd);
|
||||
|
||||
|
||||
|
|
@ -2015,8 +2012,8 @@ fun open_monitor_command ((((oid, pos),cid_pos), doc_attrs) : ODL_Meta_Args_Par
|
|||
NONE => ISA_core.err ("You must specified a monitor class.") pos
|
||||
| SOME (cid, _) => cid
|
||||
val (accS, rejectS, aS) = compute_enabled_set cid thy
|
||||
val info = {accepted_cids = accS, rejected_cids = rejectS, automatas = aS }
|
||||
in DOF_core.add_monitor_info (Binding.make (oid, pos)) (DOF_core.Monitor_Info info) thy
|
||||
in DOF_core.add_monitor_info (Binding.make (oid, pos))
|
||||
(DOF_core.make_monitor_info (accS, rejectS, aS)) thy
|
||||
end
|
||||
in
|
||||
o_m_c oid pos cid_pos doc_attrs #> create_monitor_entry oid
|
||||
|
|
|
|||
Loading…
Reference in New Issue