Ontology checking bug for unrelated direct sub_classes fixed.
Enfin !
This commit is contained in:
parent
027361fb03
commit
5e48dcffdf
20
Isa_DOF.thy
20
Isa_DOF.thy
|
@ -63,11 +63,11 @@ struct
|
||||||
fun is_subclass0 (tab:docclass_tab) s t =
|
fun is_subclass0 (tab:docclass_tab) s t =
|
||||||
let val _ = case Symtab.lookup tab t of
|
let val _ = case Symtab.lookup tab t of
|
||||||
NONE => if t <> default_cid
|
NONE => if t <> default_cid
|
||||||
then error "document superclass not defined"
|
then error ("document superclass not defined: "^t)
|
||||||
else default_cid
|
else default_cid
|
||||||
| SOME _ => ""
|
| SOME _ => ""
|
||||||
fun father_is_sub s = case Symtab.lookup tab s of
|
fun father_is_sub s = case Symtab.lookup tab s of
|
||||||
NONE => error "document subclass not defined"
|
NONE => error ("document subclass not defined: "^s)
|
||||||
| SOME ({inherits_from=NONE, ...}) => s = t
|
| SOME ({inherits_from=NONE, ...}) => s = t
|
||||||
| SOME ({inherits_from=SOME (_,s'), ...}) =>
|
| SOME ({inherits_from=SOME (_,s'), ...}) =>
|
||||||
s' = t orelse father_is_sub s'
|
s' = t orelse father_is_sub s'
|
||||||
|
@ -446,19 +446,12 @@ fun doc_class_ref_antiquotation name cid_decl =
|
||||||
let fun open_par x = if x then "\\label{"
|
let fun open_par x = if x then "\\label{"
|
||||||
else "\\autoref{"
|
else "\\autoref{"
|
||||||
val close = "}"
|
val close = "}"
|
||||||
val _ = writeln ("XXX" ^ cid_decl)
|
|
||||||
fun cid_decl' ctxt = let val thy = (Proof_Context.theory_of ctxt)
|
|
||||||
val str = (Binding.name_of name)
|
|
||||||
val name = DOF_core.name2doc_class_name thy str
|
|
||||||
val _ = writeln ("YYY" ^ name)
|
|
||||||
in str end
|
|
||||||
in
|
in
|
||||||
Thy_Output.antiquotation name (Scan.lift (doc_ref_modes -- Args.cartouche_input))
|
Thy_Output.antiquotation name (Scan.lift (doc_ref_modes -- Args.cartouche_input))
|
||||||
(fn {context = ctxt, source = src:Token.src, state} =>
|
(fn {context = ctxt, source = src:Token.src, state} =>
|
||||||
fn ({unchecked = x, define= y}, source:Input.source) =>
|
fn ({unchecked = x, define= y}, source:Input.source) =>
|
||||||
(Thy_Output.output_text state {markdown=false} #>
|
(Thy_Output.output_text state {markdown=false} #>
|
||||||
check_and_mark ctxt
|
check_and_mark ctxt
|
||||||
(* (cid_decl' ctxt) *)
|
|
||||||
cid_decl
|
cid_decl
|
||||||
({strict_checking = not x})
|
({strict_checking = not x})
|
||||||
(Input.pos_of source) #>
|
(Input.pos_of source) #>
|
||||||
|
@ -506,15 +499,14 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdef
|
||||||
val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ terms
|
val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ terms
|
||||||
val fieldsNterms' = map (fn ((x,y),z) => (x,y,z)) fieldsNterms
|
val fieldsNterms' = map (fn ((x,y),z) => (x,y,z)) fieldsNterms
|
||||||
val params' = map (Proof_Context.check_tfree ctxt3) params;
|
val params' = map (Proof_Context.check_tfree ctxt3) params;
|
||||||
val cid = case raw_parent of (* why the parent ? ? ? *)
|
|
||||||
NONE => DOF_core.default_cid
|
fun cid thy = DOF_core.name2doc_class_name thy (Binding.name_of binding)
|
||||||
| SOME X => DOF_core.name2doc_class_name thy X
|
|
||||||
val gen_antiquotation = OntoLinkParser.doc_class_ref_antiquotation
|
val gen_antiquotation = OntoLinkParser.doc_class_ref_antiquotation
|
||||||
|
|
||||||
in thy |> Record.add_record overloaded (params', binding) parent fields
|
in thy |> Record.add_record overloaded (params', binding) parent fields
|
||||||
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms'
|
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms'
|
||||||
|> gen_antiquotation binding cid (* defines the ontology-checked
|
|> (fn thy => gen_antiquotation binding (cid thy) thy)
|
||||||
text antiquotation to this document class *)
|
(* defines the ontology-checked text antiquotation to this document class *)
|
||||||
end;
|
end;
|
||||||
|
|
||||||
|
|
||||||
|
|
|
@ -1,6 +1,5 @@
|
||||||
theory Example
|
theory Example
|
||||||
imports "../../ontologies/CENELEC_50126"
|
imports "../../ontologies/CENELEC_50126"
|
||||||
keywords "Term" :: diag
|
|
||||||
begin
|
begin
|
||||||
|
|
||||||
section{* Some show-off's of general antiquotations. *}
|
section{* Some show-off's of general antiquotations. *}
|
||||||
|
@ -19,10 +18,11 @@ text{* @{thm refl} of name @{thm [source] refl}
|
||||||
@{term "3"}
|
@{term "3"}
|
||||||
@{type bool}
|
@{type bool}
|
||||||
@{term [show_types] "f x = a + x"} *}
|
@{term [show_types] "f x = a + x"} *}
|
||||||
|
|
||||||
|
|
||||||
section{* Example *}
|
section{* Example *}
|
||||||
|
|
||||||
|
text*[tralala] {* Brexit means Brexit *}
|
||||||
|
|
||||||
text*[ass1::assumption] {* Brexit means Brexit *}
|
text*[ass1::assumption] {* Brexit means Brexit *}
|
||||||
|
|
||||||
text*[hyp1::hypothesis] {* P means not P *}
|
text*[hyp1::hypothesis] {* P means not P *}
|
||||||
|
@ -38,52 +38,38 @@ to a test-environment or test-engine *}
|
||||||
|
|
||||||
|
|
||||||
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
|
text \<open> As established by @{docref (unchecked) \<open>t10\<close>},
|
||||||
@{docref (define) \<open>t10\<close>}
|
@{docref (define) \<open>t10\<close>} \<close>
|
||||||
the @{docref \<open>t10\<close>}
|
text \<open> the @{docref \<open>t10\<close>}
|
||||||
the @{docref \<open>ass122\<close>}
|
the @{docref \<open>ass122\<close>}
|
||||||
\<close>
|
\<close>
|
||||||
text \<open> safety related applicability condition @{srac \<open>ass122\<close>}.
|
text \<open> safety related applicability condition @{srac \<open>ass122\<close>}. \<close>
|
||||||
exported constraint @{ec \<open>ass122\<close>}.
|
text \<open> exported constraint @{ec \<open>ass122\<close>}.
|
||||||
\<close>
|
\<close>
|
||||||
|
|
||||||
text{*
|
text{* And some ontologically inconsistent reference: @{hypothesis \<open>ass1\<close>} as well as *}
|
||||||
And some ontologically inconsistent reference:
|
-- wrong
|
||||||
@{hypothesis \<open>ass1\<close>} as well as
|
|
||||||
|
|
||||||
*}
|
|
||||||
-- "very wrong"
|
|
||||||
|
|
||||||
text{*
|
text{* ... some more ontologically inconsistent reference: @{assumption \<open>hyp1\<close>} as well as *}
|
||||||
And some ontologically inconsistent reference:
|
-- wrong
|
||||||
@{assumption \<open>hyp1\<close>} as well as
|
|
||||||
|
|
||||||
*}
|
|
||||||
-- "very wrong"
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
text{*
|
text{* And a further ontologically totally inconsistent reference:
|
||||||
And some ontologically inconsistent reference:
|
@{test_result \<open>ass122\<close>} as well as ... *}
|
||||||
@{test_result \<open>ass122\<close>} as well as
|
|
||||||
|
|
||||||
*}
|
|
||||||
-- wrong
|
-- wrong
|
||||||
|
|
||||||
text{*
|
text{* the ontologically inconsistent reference: @{ec \<open>t10\<close>} *}
|
||||||
And some other ontologically inconsistent reference:
|
|
||||||
@{ec \<open>t10\<close>} as well as
|
|
||||||
*}
|
|
||||||
-- wrong
|
-- wrong
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
section{* Some Tests for Ontology Framework and its CENELEC Instance *}
|
section{* Some Tests for Ontology Framework and its CENELEC Instance *}
|
||||||
|
|
||||||
declare_reference [lalala::requirement, alpha="main", beta=42]
|
declare_reference* [lalala::requirement, alpha="main", beta=42]
|
||||||
|
|
||||||
declare_reference [lalala::quod] (* shouldn't work *)
|
declare_reference* [lalala::quod] (* shouldn't work *)
|
||||||
|
|
||||||
declare_reference [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1]
|
||||||
|
|
||||||
paragraph*[sdf]{* just a paragraph *}
|
paragraph*[sdf]{* just a paragraph *}
|
||||||
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
|
paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
|
||||||
|
@ -117,34 +103,7 @@ text{* Here is a reference to @{docref \<open>sedf\<close>} *}
|
||||||
Try to hover over the sedf - link and activate it !!! *)
|
Try to hover over the sedf - link and activate it !!! *)
|
||||||
|
|
||||||
|
|
||||||
|
section{* Miscellaneous ...*}
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
section{* A Small Example for a Command Definition --- just to see how this works in principle. *}
|
|
||||||
|
|
||||||
ML{*
|
|
||||||
val opt_modes =
|
|
||||||
Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) [];
|
|
||||||
|
|
||||||
val _ =
|
|
||||||
Outer_Syntax.command @{command_keyword Term} "read and print term"
|
|
||||||
(opt_modes -- Parse.term >> Isar_Cmd.print_term);
|
|
||||||
|
|
||||||
*}
|
|
||||||
|
|
||||||
lemma "True" by simp
|
|
||||||
|
|
||||||
Term "a + b = b + a"
|
|
||||||
|
|
||||||
term "a + b = b + a"
|
|
||||||
|
|
||||||
section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *)
|
section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *)
|
||||||
|
|
||||||
|
|
|
@ -153,15 +153,15 @@ DOF_core.name2doc_class_name @{theory} "requirement";
|
||||||
DOF_core.name2doc_class_name @{theory} "srac";
|
DOF_core.name2doc_class_name @{theory} "srac";
|
||||||
DOF_core.is_defined_cid_global "srac" @{theory};
|
DOF_core.is_defined_cid_global "srac" @{theory};
|
||||||
DOF_core.is_defined_cid_global "ec" @{theory};
|
DOF_core.is_defined_cid_global "ec" @{theory};
|
||||||
"hallo";
|
"XXXXXXXXXXXXXXXXX";
|
||||||
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.ec";
|
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.ec";
|
||||||
DOF_core.is_subclass @{context} "CENELEC_50126.srac" "CENELEC_50126.ec";
|
DOF_core.is_subclass @{context} "CENELEC_50126.srac" "CENELEC_50126.ec";
|
||||||
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.srac";
|
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.srac";
|
||||||
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.test_requirement";
|
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.test_requirement";
|
||||||
|
"XXXXXXXXXXXXXXXXX";
|
||||||
val ({maxano, tab},tab2) = DOF_core.get_data @{context};
|
val ({maxano, tab=ref_tab},class_tab) = DOF_core.get_data @{context};
|
||||||
Symtab.dest tab;
|
Symtab.dest ref_tab;
|
||||||
Symtab.dest tab2;
|
Symtab.dest class_tab;
|
||||||
|
|
||||||
|
|
||||||
*}
|
*}
|
||||||
|
|
Loading…
Reference in New Issue