syntax and 1st level type-checking of invariants
This commit is contained in:
parent
cc98979f43
commit
9035c46023
|
@ -34,7 +34,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
|
||||||
RegExpInterface (* Interface to functional regular automata for monitoring *)
|
RegExpInterface (* Interface to functional regular automata for monitoring *)
|
||||||
Assert
|
Assert
|
||||||
|
|
||||||
keywords "+=" ":=" "accepts" "rejects"
|
keywords "+=" ":=" "accepts" "rejects" "invs"
|
||||||
|
|
||||||
and "title*" "subtitle*"
|
and "title*" "subtitle*"
|
||||||
"chapter*" "section*" "subsection*" "subsubsection*"
|
"chapter*" "section*" "subsection*" "subsubsection*"
|
||||||
|
@ -140,7 +140,8 @@ struct
|
||||||
inherits_from : (typ list * string) option, (* imports *)
|
inherits_from : (typ list * string) option, (* imports *)
|
||||||
attribute_decl : (binding*typ*term option)list, (* class local *)
|
attribute_decl : (binding*typ*term option)list, (* class local *)
|
||||||
rejectS : term list,
|
rejectS : term list,
|
||||||
rex : term list } (* monitoring regexps --- product semantics*)
|
rex : term list,
|
||||||
|
invs : ((string * Position.T) * term) list } (* monitoring regexps --- product semantics*)
|
||||||
|
|
||||||
|
|
||||||
type docclass_tab = docclass_struct Symtab.table
|
type docclass_tab = docclass_struct Symtab.table
|
||||||
|
@ -410,7 +411,7 @@ fun check_reject_atom cid_long term =
|
||||||
in term end
|
in term end
|
||||||
|
|
||||||
|
|
||||||
fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms thy =
|
fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms invs thy =
|
||||||
(* This operation is executed in a context where the record has amready been defined, but
|
(* This operation is executed in a context where the record has amready been defined, but
|
||||||
its conversion into a class is not yet done. *)
|
its conversion into a class is not yet done. *)
|
||||||
let val nn = Context.theory_name thy (* in case that we need the thy-name to identify
|
let val nn = Context.theory_name thy (* in case that we need the thy-name to identify
|
||||||
|
@ -439,7 +440,11 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms t
|
||||||
val reg_exps = map (Syntax.read_term_global thy) rexp;
|
val reg_exps = map (Syntax.read_term_global thy) rexp;
|
||||||
val _ = map check_regexps reg_exps
|
val _ = map check_regexps reg_exps
|
||||||
val _ = if not(null rejectS) andalso (null reg_exps)
|
val _ = if not(null rejectS) andalso (null reg_exps)
|
||||||
then error ("reject clause requires accept clause ! ") else ();
|
then error ("reject clause requires accept clause ! " ) else ();
|
||||||
|
val _ = if has_duplicates (op =) (map (fst o fst) invs)
|
||||||
|
then error("invariant labels must be unique"^ Position.here (snd(fst(hd invs))))
|
||||||
|
else ()
|
||||||
|
val invs' = map (map_snd(Syntax.read_term_global thy)) invs
|
||||||
val info = {params=params',
|
val info = {params=params',
|
||||||
name = binding,
|
name = binding,
|
||||||
thy_name = nn,
|
thy_name = nn,
|
||||||
|
@ -449,7 +454,8 @@ fun define_doc_class_global (params', binding) parent fields rexp reject_Atoms t
|
||||||
inherits_from = parent',
|
inherits_from = parent',
|
||||||
attribute_decl = fields ,
|
attribute_decl = fields ,
|
||||||
rejectS = rejectS,
|
rejectS = rejectS,
|
||||||
rex = reg_exps }
|
rex = reg_exps,
|
||||||
|
invs = invs'}
|
||||||
|
|
||||||
in map_data_global(upd_docclass_tab(Symtab.update(cid_long,info)))(thy)
|
in map_data_global(upd_docclass_tab(Symtab.update(cid_long,info)))(thy)
|
||||||
end
|
end
|
||||||
|
@ -638,14 +644,16 @@ fun print_doc_classes b ctxt =
|
||||||
let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt;
|
let val {docobj_tab={tab = x, ...},docclass_tab, ...} = get_data ctxt;
|
||||||
val _ = writeln "=====================================";
|
val _ = writeln "=====================================";
|
||||||
fun print_attr (n, ty, NONE) = (Binding.print n)
|
fun print_attr (n, ty, NONE) = (Binding.print n)
|
||||||
| print_attr (n, ty, SOME t) = (Binding.print n^"("^Syntax.string_of_term ctxt t^")")
|
| print_attr (n, ty, SOME t)= (Binding.print n^"("^Syntax.string_of_term ctxt t^")")
|
||||||
fun print_class (n, {attribute_decl, id, inherits_from, name, params, thy_name, rejectS, rex}) =
|
fun print_inv ((lab,pos),trm) = (lab ^"::"^Syntax.string_of_term ctxt trm)
|
||||||
|
fun print_class (n, {attribute_decl, id, inherits_from, name, params, thy_name, rejectS, rex,invs}) =
|
||||||
(case inherits_from of
|
(case inherits_from of
|
||||||
NONE => writeln ("docclass: "^n)
|
NONE => writeln ("docclass: "^n)
|
||||||
| SOME(_,nn) => writeln ("docclass: "^n^" = "^nn^" + ");
|
| SOME(_,nn) => writeln ("docclass: "^n^" = "^nn^" + ");
|
||||||
writeln (" name: "^(Binding.print name));
|
writeln (" name: "^(Binding.print name));
|
||||||
writeln (" origin: "^thy_name);
|
writeln (" origin: "^thy_name);
|
||||||
writeln (" attrs: "^commas (map print_attr attribute_decl))
|
writeln (" attrs: "^commas (map print_attr attribute_decl));
|
||||||
|
writeln (" invs: "^commas (map print_inv invs))
|
||||||
);
|
);
|
||||||
in map print_class (Symtab.dest docclass_tab);
|
in map print_class (Symtab.dest docclass_tab);
|
||||||
writeln "=====================================\n\n\n"
|
writeln "=====================================\n\n\n"
|
||||||
|
@ -1805,7 +1813,7 @@ val trace_attr = ((Binding.make("trace",@{here}), "(doc_class rexp \<times> stri
|
||||||
SOME "[]"): ((binding * string * mixfix) * string option)
|
SOME "[]"): ((binding * string * mixfix) * string option)
|
||||||
|
|
||||||
fun add_doc_class_cmd overloaded (raw_params, binding)
|
fun add_doc_class_cmd overloaded (raw_params, binding)
|
||||||
raw_parent raw_fieldsNdefaults reject_Atoms regexps thy =
|
raw_parent raw_fieldsNdefaults reject_Atoms regexps invariants thy =
|
||||||
let
|
let
|
||||||
val ctxt = Proof_Context.init_global thy;
|
val ctxt = Proof_Context.init_global thy;
|
||||||
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
|
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
|
||||||
|
@ -1841,14 +1849,14 @@ fun add_doc_class_cmd overloaded (raw_params, binding)
|
||||||
|
|
||||||
in thy |> Record.add_record overloaded (params', binding) parent' (tag_attr::fields)
|
in thy |> Record.add_record overloaded (params', binding) parent' (tag_attr::fields)
|
||||||
|> (Sign.add_consts_cmd [(binding, "doc_class Regular_Exp.rexp", Mixfix.NoSyn)])
|
|> (Sign.add_consts_cmd [(binding, "doc_class Regular_Exp.rexp", Mixfix.NoSyn)])
|
||||||
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps reject_Atoms
|
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' regexps
|
||||||
|
reject_Atoms invariants
|
||||||
(* adding const symbol representing doc-class for Monitor-RegExps.*)
|
(* adding const symbol representing doc-class for Monitor-RegExps.*)
|
||||||
|> (fn thy => OntoLinkParser.docitem_antiquotation binding (cid thy) thy)
|
|> (fn thy => OntoLinkParser.docitem_antiquotation binding (cid thy) thy)
|
||||||
(* defines the ontology-checked text antiquotation to this document class *)
|
(* defines the ontology-checked text antiquotation to this document class *)
|
||||||
|
|
||||||
end;
|
end;
|
||||||
|
|
||||||
|
|
||||||
val _ =
|
val _ =
|
||||||
Outer_Syntax.command \<^command_keyword>\<open>doc_class\<close> "define document class"
|
Outer_Syntax.command \<^command_keyword>\<open>doc_class\<close> "define document class"
|
||||||
((Parse_Spec.overloaded
|
((Parse_Spec.overloaded
|
||||||
|
@ -1858,10 +1866,12 @@ val _ =
|
||||||
-- Scan.repeat1 (Parse.const_binding -- Scan.option (\<^keyword>\<open><=\<close> |-- Parse.term))
|
-- Scan.repeat1 (Parse.const_binding -- Scan.option (\<^keyword>\<open><=\<close> |-- Parse.term))
|
||||||
)
|
)
|
||||||
-- ( Scan.optional (\<^keyword>\<open>rejects\<close> |-- Parse.enum1 "," Parse.term) []
|
-- ( Scan.optional (\<^keyword>\<open>rejects\<close> |-- Parse.enum1 "," Parse.term) []
|
||||||
-- Scan.repeat (\<^keyword>\<open>accepts\<close> |-- Parse.term))
|
-- Scan.repeat (\<^keyword>\<open>accepts\<close> |-- Parse.term)
|
||||||
|
-- Scan.repeats ((\<^keyword>\<open>invs\<close>) |--
|
||||||
|
Parse.and_list (Args.name_position --| Parse.$$$ "::" -- Parse.term)))
|
||||||
)
|
)
|
||||||
>> (fn (((overloaded, x), (y, z)),(rejectS,accept_rex)) =>
|
>> (fn (((overloaded, x), (y, z)),((rejectS,accept_rex),invs)) =>
|
||||||
Toplevel.theory (add_doc_class_cmd {overloaded = overloaded} x y z rejectS accept_rex)));
|
Toplevel.theory (add_doc_class_cmd {overloaded = overloaded} x y z rejectS accept_rex invs)));
|
||||||
|
|
||||||
end (* struct *)
|
end (* struct *)
|
||||||
\<close>
|
\<close>
|
||||||
|
|
|
@ -55,8 +55,12 @@ doc_class F =
|
||||||
u :: "file"
|
u :: "file"
|
||||||
s :: "typ list"
|
s :: "typ list"
|
||||||
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
|
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
|
||||||
to an association class. It can be used to track
|
to an association class. It can be used to track
|
||||||
claims to result - relations, for example.*)
|
claims to result - relations, for example.*)
|
||||||
|
invs bxxx :: "\<lambda>\<sigma>. r \<sigma> \<noteq> [] \<and> card(b \<sigma>) \<ge> 3"
|
||||||
|
and xxx :: "\<lambda>\<sigma>. properties \<sigma> \<noteq> []"
|
||||||
|
|
||||||
|
|
||||||
doc_class G = C +
|
doc_class G = C +
|
||||||
g :: "thm" <= "@{thm ''HOL.refl''}"
|
g :: "thm" <= "@{thm ''HOL.refl''}"
|
||||||
|
|
||||||
|
@ -65,7 +69,6 @@ doc_class M =
|
||||||
accepts "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
|
accepts "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
|
||||||
|
|
||||||
|
|
||||||
|
|
||||||
(*
|
(*
|
||||||
ML\<open> Document.state();\<close>
|
ML\<open> Document.state();\<close>
|
||||||
ML\<open> Session.get_keywords(); (* this looks to be really session global. *)
|
ML\<open> Session.get_keywords(); (* this looks to be really session global. *)
|
||||||
|
|
|
@ -82,20 +82,20 @@ type_synonym tc = technical
|
||||||
|
|
||||||
text\<open>A rough structuring is modeled as follows:\<close>
|
text\<open>A rough structuring is modeled as follows:\<close>
|
||||||
|
|
||||||
doc_class "definition" = technical +
|
doc_class "definition" = tc +
|
||||||
referentiable :: bool <= "True"
|
referentiable :: bool <= "True"
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
doc_class "theorem" = technical +
|
doc_class "theorem" = tc +
|
||||||
referentiable :: bool <= "True"
|
referentiable :: bool <= "True"
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
|
text\<open>Note that the following two text-elements are currently set to no-keyword in LNCS style.\<close>
|
||||||
doc_class "lemma" = technical +
|
doc_class "lemma" = tc +
|
||||||
referentiable :: bool <= "True"
|
referentiable :: bool <= "True"
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
doc_class "corollary" = technical +
|
doc_class "corollary" = tc +
|
||||||
referentiable :: bool <= "True"
|
referentiable :: bool <= "True"
|
||||||
tag :: "string" <= "''''"
|
tag :: "string" <= "''''"
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue