From 90f6c2d4ab0c30d9806dbe7d72430785640e66c2 Mon Sep 17 00:00:00 2001 From: bu Date: Tue, 20 Nov 2018 10:11:11 +0100 Subject: [PATCH] - New checks for reject sets - basic infrastructure for class invariants --- Isa_DOF.thy | 52 ++++++++++++------- RegExpInterface.thy | 7 ++- .../technical_report/IsaDofApplications.thy | 3 +- 3 files changed, 41 insertions(+), 21 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 52e42ba..99dbdda 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -4,7 +4,7 @@ text\ Offering \<^item> text-elements that can be annotated with meta-information \<^item> typed links to text-elements via specifically generated anti-quotations \<^item> typed structure of this meta-information specifiable in an Ontology-Language ODL -\<^item> inner-syntax-antiquotations allowing to reference Isabelle-entities such as +\<^item> inner-syntax-antiquotations (ISA's) allowing to reference Isabelle-entities such as types, terms, theorems inside the meta-information \<^item> monitors allowing to enforce a specific textual structure of an Isabelle Document \<^item> LaTeX support. \ @@ -116,15 +116,16 @@ struct end) type ISA_transformer_tab = (theory -> term * typ * Position.T -> term option) Symtab.table - val initial_ISA_tab:ISA_transformer_tab = Symtab.empty + type docclass_inv_tab = (theory -> bool) Symtab.table + val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty + type open_monitor_info = {accepted_cids : string list, rejected_cids : string list, automatas : RegExpInterface.automaton list } type monitor_tab = open_monitor_info Symtab.table - val initial_monitor_tab:monitor_tab = Symtab.empty fun override(t1,t2) = fold(Symtab.update)(Symtab.dest t2)(t1) @@ -135,20 +136,27 @@ structure Data = Generic_Data type T = {docobj_tab : docobj_tab, docclass_tab : docclass_tab, ISA_transformer_tab : ISA_transformer_tab, - monitor_tab : monitor_tab} - val empty = {docobj_tab = initial_docobj_tab, - docclass_tab = initial_docclass_tab, + monitor_tab : monitor_tab, + docclass_inv_tab : docclass_inv_tab} + val empty = {docobj_tab = initial_docobj_tab, + docclass_tab = initial_docclass_tab, ISA_transformer_tab = initial_ISA_tab, - monitor_tab = initial_monitor_tab + monitor_tab = initial_monitor_tab, + docclass_inv_tab = initial_docclass_inv_tab } val extend = I - fun merge( {docobj_tab=d1,docclass_tab = c1,ISA_transformer_tab = e1, monitor_tab=m1}, - {docobj_tab=d2,docclass_tab = c2,ISA_transformer_tab = e2, monitor_tab=m2}) = + fun merge( {docobj_tab=d1,docclass_tab = c1, + ISA_transformer_tab = e1, monitor_tab=m1, + docclass_inv_tab = n1}, + {docobj_tab=d2,docclass_tab = c2, + ISA_transformer_tab = e2, monitor_tab=m2, + docclass_inv_tab = n2}) = {docobj_tab=merge_docobj_tab (d1,d2), docclass_tab = merge_docclass_tab (c1,c2), ISA_transformer_tab = Symtab.merge (fn (_ , _) => false)(e1,e2), - monitor_tab = override(m1,m2) + monitor_tab = override(m1,m2), (* PROVISORY ... ITS A REAL QUESTION HOW TO DO THIS!*) + docclass_inv_tab = override(n1,n2) } ); @@ -159,16 +167,24 @@ val get_data_global = Data.get o Context.Theory; val map_data_global = Context.theory_map o map_data; -fun upd_docobj_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab} = +fun upd_docobj_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab,docclass_inv_tab} = {docobj_tab = f docobj_tab, docclass_tab=docclass_tab, - ISA_transformer_tab=ISA_transformer_tab, monitor_tab=monitor_tab}; -fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab} = - {docobj_tab=x,docclass_tab = f y,ISA_transformer_tab = z, monitor_tab=monitor_tab}; -fun upd_ISA_transformers f{docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab} = - {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = f z, monitor_tab=monitor_tab}; -fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab} = + ISA_transformer_tab=ISA_transformer_tab, monitor_tab=monitor_tab, + docclass_inv_tab=docclass_inv_tab}; +fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab, docclass_inv_tab} = + {docobj_tab=x,docclass_tab = f y,ISA_transformer_tab = z, monitor_tab=monitor_tab, + docclass_inv_tab=docclass_inv_tab}; +fun upd_ISA_transformers f{docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab, docclass_inv_tab} = + {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = f z, monitor_tab=monitor_tab, + docclass_inv_tab=docclass_inv_tab}; +fun upd_monitor_tabs 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 = f monitor_tab}; + ISA_transformer_tab = ISA_transformer_tab, monitor_tab = f monitor_tab, + docclass_inv_tab=docclass_inv_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}; fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids diff --git a/RegExpInterface.thy b/RegExpInterface.thy index 0a4be51..a2f719e 100644 --- a/RegExpInterface.thy +++ b/RegExpInterface.thy @@ -135,7 +135,12 @@ local open RegExpChecker in val add_atom = fold_aterms (fn Const(c as(_,Type(@{type_name "rexp"},_)))=> insert (op=) c |_=>I); fun alphabet termS = rev(map fst (fold add_atom termS [])); - fun ext_alphabet env termS = rev(map fst (fold add_atom termS [])) @ env; + fun ext_alphabet env termS = + let val res = rev(map fst (fold add_atom termS [])) @ env; + val _ = if has_duplicates (op=) res + then error("reject and accept alphabets must be disjoint!") + else () + in res end; fun conv (Const(@{const_name "Regular_Exp.rexp.Zero"},_)) _ = Zero |conv (Const(@{const_name "Regular_Exp.rexp.One"},_)) _ = Onea diff --git a/examples/technical_report/IsaDofApplications.thy b/examples/technical_report/IsaDofApplications.thy index 45f21f0..a62e153 100644 --- a/examples/technical_report/IsaDofApplications.thy +++ b/examples/technical_report/IsaDofApplications.thy @@ -721,8 +721,7 @@ text\ \isadof in its present form has a number of technical short-comings paragraph\ Availability. \ text\ The implementation of the framework, the discussed ontology definitions, - and examples are available at - \url{https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF/}.\ + and examples are available at \url{https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF/}.\ paragraph\ Acknowledgement. \ text\ This work was partly supported by the framework of IRT SystemX, Paris-Saclay, France, and therefore granted with public funds within the scope of the Program ``Investissements d’Avenir''.\