- New checks for reject sets
- basic infrastructure for class invariants
This commit is contained in:
parent
d406b3daeb
commit
90f6c2d4ab
52
Isa_DOF.thy
52
Isa_DOF.thy
|
|
@ -4,7 +4,7 @@ text\<open> 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. \<close>
|
||||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -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
|
||||
|
|
|
|||
|
|
@ -721,8 +721,7 @@ text\<open> \isadof in its present form has a number of technical short-comings
|
|||
|
||||
paragraph\<open> Availability. \<close>
|
||||
text\<open> The implementation of the framework, the discussed ontology definitions,
|
||||
and examples are available at
|
||||
\url{https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF/}.\<close>
|
||||
and examples are available at \url{https://git.logicalhacking.com/HOL-OCL/Isabelle_DOF/}.\<close>
|
||||
paragraph\<open> Acknowledgement. \<close>
|
||||
text\<open> 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''.\<close>
|
||||
|
|
|
|||
Loading…
Reference in New Issue