From 23bc75d08d695ab57fe84f34b874c485f68dbb15 Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Dec 2018 13:19:31 +0100 Subject: [PATCH] Corrections in ontologies (revealed by examples) - identified problem: accept/reject conflicts were only detected at application time, not at declaration time :-( (leaved as "known problem" for the moment) - new functionality for declaring doc class invariants --- Isa_COL.thy | 2 +- Isa_DOF.thy | 52 ++++++++++++++++++++--------- examples/cenelec/Example.thy | 3 -- examples/conceptual/Attributes.thy | 2 +- examples/simple/Concept_Example.thy | 8 +++++ ontologies/Conceptual.thy | 11 +++++- ontologies/technical_report.thy | 3 ++ 7 files changed, 60 insertions(+), 21 deletions(-) diff --git a/Isa_COL.thy b/Isa_COL.thy index 90892ac1..fb0b4bda 100644 --- a/Isa_COL.thy +++ b/Isa_COL.thy @@ -34,7 +34,7 @@ doc_class figure_group = (* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *) anchor :: "string" caption :: "string" - rejects figure, figure_group (* this forbids recursive figure-groups *) + rejects figure_group (* this forbids recursive figure-groups *) accepts "\figure\\<^sup>+" ML\@{term "side_by_side_figure"}; diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 0e91ef06..3ccad46d 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -66,8 +66,9 @@ section\ A HomeGrown Document Type Management (the ''Model'') \ ML\ structure DOF_core = struct - type docclass_struct = {params : (string * sort) list, (*currently not used *) - name : binding, thy_name : string, id : serial, (* for pide *) + type docclass_struct = {params : (string * sort) list, (*currently not used *) + name : binding, + thy_name : string, id : serial, (* for pide *) inherits_from : (typ list * string) option, (* imports *) attribute_decl : (binding * typ * term option) list, (* class local *) rejectS : term list, @@ -188,7 +189,7 @@ fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab fun upd_docclass_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab, docclass_inv_tab} = {docobj_tab = docobj_tab,docclass_tab = docclass_tab, ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab, - docclass_inv_tab= f docclass_inv_tab}; + docclass_inv_tab = f docclass_inv_tab}; fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids @@ -232,12 +233,19 @@ fun is_defined_cid_global cid thy = let val t = #docclass_tab(get_data_global th Symtab.defined t (name2doc_class_name thy cid) end +fun is_defined_cid_global' cid_long thy = let val t = #docclass_tab(get_data_global thy) + in cid_long=default_cid orelse Symtab.defined t cid_long end + + fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt) in cid=default_cid orelse Symtab.defined t (name2doc_class_name_local ctxt cid) end +fun is_defined_cid_local' cid_long ctxt = let val t = #docclass_tab(get_data ctxt) + in cid_long=default_cid orelse Symtab.defined t cid_long end + fun is_declared_oid_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy) in Symtab.defined tab oid end @@ -272,6 +280,24 @@ fun declare_object_local oid ctxt = handle Symtab.DUP _ => error("multiple declaration of document reference")) end + +fun update_class_invariant cid_long f thy = + let val _ = if is_defined_cid_global' cid_long thy then () + else error("undefined class id : " ^cid_long) + in map_data_global (upd_docclass_inv_tab (Symtab.update (cid_long, + (fn ctxt => ((writeln("Inv check of :" ^cid_long); f ctxt )))))) + thy + end + +fun get_class_invariant cid_long thy = + let val _ = if is_defined_cid_global' cid_long thy then () + else error("undefined class id : " ^cid_long) + val {docclass_inv_tab, ...} = get_data_global thy + in case Symtab.lookup docclass_inv_tab cid_long of + NONE => K true + | SOME f => f + end + val SPY = Unsynchronized.ref(Bound 0) fun check_regexps term = @@ -464,9 +490,10 @@ fun update_value_global oid upd thy = val ISA_prefix = "Isa_DOF.ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *) -fun get_isa_global isa thy = case Symtab.lookup (#ISA_transformer_tab(get_data_global thy)) (ISA_prefix^isa) of - NONE => error("undefined inner syntax antiquotation: "^isa) - |SOME(bbb) => bbb +fun get_isa_global isa thy = + case Symtab.lookup (#ISA_transformer_tab(get_data_global thy)) (ISA_prefix^isa) of + NONE => error("undefined inner syntax antiquotation: "^isa) + | SOME(bbb) => bbb fun get_isa_local isa ctxt = case Symtab.lookup (#ISA_transformer_tab(get_data ctxt)) (ISA_prefix^isa) of @@ -894,13 +921,13 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list) val _ = if Long_Name.base_name lhs = lhs orelse ln = lhs then () else error("illegal notation for attribute of "^cid_long) fun join (ttt as @{typ "int"}) - = Const (@{const_name "plus"}, ttt --> ttt --> ttt) + = Const (@{const_name "Groups.plus"}, ttt --> ttt --> ttt) |join (ttt as @{typ "string"}) - = Const (@{const_name "append"}, ttt --> ttt --> ttt) + = Const (@{const_name "List.append"}, ttt --> ttt --> ttt) |join (ttt as Type(@{type_name "set"},_)) - = Const (@{const_name "sup"}, ttt --> ttt --> ttt) + = Const (@{const_name "Lattices.sup"}, ttt --> ttt --> ttt) |join (ttt as Type(@{type_name "list"},_)) - = Const (@{const_name "append"}, ttt --> ttt --> ttt) + = Const (@{const_name "List.append"}, ttt --> ttt --> ttt) |join _ = error("implicit fusion operation not defined for attribute: "^ lhs) (* could be extended to bool, map, multisets, ... *) val rhs' = instantiate_term tyenv' (generalize_term rhs) @@ -1491,11 +1518,6 @@ ML\ section\ Testing and Validation \ -text*[sdf] {* f @{thm refl}*} -text*[sdfg] {* fg @{thm refl}*} - -text*[xxxy] {* dd @{docitem \sdfg\} @{thm refl}*} - (* the following test crashes the LaTeX generation - however, without the latter this output is instructive ML\ diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy index 34bcaeb3..830eb3bb 100644 --- a/examples/cenelec/Example.thy +++ b/examples/cenelec/Example.thy @@ -70,9 +70,6 @@ paragraph* [sdfk] \ just a paragraph - lexical variant \ section\ Some global inspection commands for the status of docitem and doc-class tables ... \ -print_doc_classes -print_doc_items - section\ Text Antiquotation Infrastructure ... \ diff --git a/examples/conceptual/Attributes.thy b/examples/conceptual/Attributes.thy index fe7abe69..6a6e5a9d 100644 --- a/examples/conceptual/Attributes.thy +++ b/examples/conceptual/Attributes.thy @@ -10,7 +10,7 @@ print_doc_items (* this corresponds to low-level accesses : *) ML\ -val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab} +val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...} = DOF_core.get_data @{context}; Symtab.dest docitem_tab; diff --git a/examples/simple/Concept_Example.thy b/examples/simple/Concept_Example.thy index 385f0af5..476a1bee 100644 --- a/examples/simple/Concept_Example.thy +++ b/examples/simple/Concept_Example.thy @@ -41,6 +41,14 @@ close_monitor*[struct] text\And the trace of the monitor is:\ ML\@{trace_attribute struct}\ +print_doc_classes +print_doc_items + +ML\ + +\ + +setup\DOF_core.update_class_invariant "Conceptual.A" (K true)\ end \ No newline at end of file diff --git a/ontologies/Conceptual.thy b/ontologies/Conceptual.thy index 9182c84e..32c3a163 100644 --- a/ontologies/Conceptual.thy +++ b/ontologies/Conceptual.thy @@ -41,5 +41,14 @@ doc_class G = C + doc_class M = trace :: "(A + C + D + F) list" accepts "A ~~ \C || D\\<^sup>* ~~ \F\" - + + +section*[test::A]\ Test and Validation\ +text\Defining some document elements to be referenced in another theory: \ +text*[sdf] {* f @{thm refl}*} +text*[sdfg] {* fg @{thm refl}*} + +text*[xxxy] {* dd @{docitem \sdfg\} @{thm refl}*} + + end \ No newline at end of file diff --git a/ontologies/technical_report.thy b/ontologies/technical_report.thy index e287593a..51db48bd 100644 --- a/ontologies/technical_report.thy +++ b/ontologies/technical_report.thy @@ -32,5 +32,8 @@ doc_class report = \index\\<^sup>+ ~~ bibliography)" +ML\ +\ + end