Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Renamed LNCS_onto into “scholarly_paper”. 

Decided for the trace variant semantics of monitors.
(more power, easier to implement)
This commit is contained in:
Burkhart Wolff 2018-04-05 12:09:58 +02:00
parent 5e48dcffdf
commit f8692dd801
2 changed files with 43 additions and 61 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

48
Isa_DOF.thy
View File

@ -482,32 +482,32 @@ fun map_option _ NONE = NONE
|map_option f (SOME x) = SOME (f x)
fun read_fields raw_fields ctxt =
let
val Ts = Syntax.read_typs ctxt (map (fn ((_, raw_T, _),_) => raw_T) raw_fields);
val terms = map ((map_option (Syntax.read_term ctxt)) o snd) raw_fields
val fields = map2 (fn ((x, _, mx),_) => fn T => (x, T, mx)) raw_fields Ts;
val ctxt' = fold Variable.declare_typ Ts ctxt;
in (fields, terms, ctxt') end;
let
val Ts = Syntax.read_typs ctxt (map (fn ((_, raw_T, _),_) => raw_T) raw_fields);
val terms = map ((map_option (Syntax.read_term ctxt)) o snd) raw_fields
val fields = map2 (fn ((x, _, mx),_) => fn T => (x, T, mx)) raw_fields Ts;
val ctxt' = fold Variable.declare_typ Ts ctxt;
in (fields, terms, ctxt') end;
fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaults _ thy =
let
val ctxt = Proof_Context.init_global thy;
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
val (parent, ctxt2) = read_parent raw_parent ctxt1;
val (fields, terms, ctxt3) = read_fields raw_fieldsNdefaults ctxt2;
val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ terms
val fieldsNterms' = map (fn ((x,y),z) => (x,y,z)) fieldsNterms
val params' = map (Proof_Context.check_tfree ctxt3) params;
fun cid thy = DOF_core.name2doc_class_name thy (Binding.name_of binding)
val gen_antiquotation = OntoLinkParser.doc_class_ref_antiquotation
in thy |> Record.add_record overloaded (params', binding) parent fields
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms'
|> (fn thy => gen_antiquotation binding (cid thy) thy)
(* defines the ontology-checked text antiquotation to this document class *)
end;
let
val ctxt = Proof_Context.init_global thy;
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
val (parent, ctxt2) = read_parent raw_parent ctxt1;
val (fields, terms, ctxt3) = read_fields raw_fieldsNdefaults ctxt2;
val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ terms
val fieldsNterms' = map (fn ((x,y),z) => (x,y,z)) fieldsNterms
val params' = map (Proof_Context.check_tfree ctxt3) params;
fun cid thy = DOF_core.name2doc_class_name thy (Binding.name_of binding)
val gen_antiquotation = OntoLinkParser.doc_class_ref_antiquotation
in thy |> Record.add_record overloaded (params', binding) parent fields
|> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms'
|> (fn thy => gen_antiquotation binding (cid thy) thy)
(* defines the ontology-checked text antiquotation to this document class *)
end;
val _ =

56
ontologies/LNCS_onto.thy → ontologies/scholarly_paper.thy
View File

@ -1,14 +1,14 @@
text{* dfgdfg n*}
section{* An example ontology for a scholarly paper*}
theory LNCS_onto
theory scholarly_paper
imports "../Isa_DOF"
begin
doc_class title =
short_title :: "string option" -- None
short_title :: "string option" <= None
doc_class subtitle =
abbrev :: "string option" -- None
abbrev :: "string option" <= None
-- \<open>adding a contribution list and checking that it is cited as well in tech as in conclusion. ? \<close>
@ -16,28 +16,28 @@ doc_class author =
affiliation :: "string"
doc_class abstract =
keyword_list :: "string list" -- None
keyword_list :: "string list" <= None
doc_class text_section =
main_author :: "author option" -- None
main_author :: "author option" <= None
doc_class introduction = text_section +
comment :: string
doc_class technical = text_section +
definition_list :: "string list" -- "[]"
definition_list :: "string list" <= "[]"
doc_class example = text_section +
comment :: string
doc_class conclusion = text_section +
main_author :: "author option" -- None
main_author :: "author option" <= None
doc_class related_work = conclusion +
main_author :: "author option" -- None
main_author :: "author option" <= None
doc_class bibliography =
style :: "string option" -- "''LNCS''"
style :: "string option" <= "''LNCS''"
text{* Besides subtyping, there is another relation between
doc_classes: a class can be a \emph{monitor} to other ones,
@ -60,39 +60,21 @@ text{* Besides subtyping, there is another relation between
*}
doc_class article =
T :: "title option" -- None
ST :: "subtitle option" -- None
AS :: "author list"
ABS :: "abstract option"
INTRO :: "introduction option"
TS :: "technical list"
EXS :: "example list"
CON :: "conclusion"
where "(title .
[subtitle] .
(author)+ .
abstract .
introduction .
(technical | example)+ .
conclusion .
bibliography)"
-- \<open>other idea: capture the essence of a monitor class as trace.
-- \<open>underlying idea: capture the essence of a monitor class as trace.
trace would be `predefined id` like `main` in C. \<close>
text{* @{cite bla} *}
doc_class article' =
doc_class article =
trace :: "(title + subtitle + author+ abstract +
introduction + technical + example +
conclusion + bibliography) list"
where "(title .
[subtitle] .
(author)+ .
abstract .
introduction .
(technical | example)+ .
conclusion .
where "(title ~
[subtitle] ~
(author)+ ~
abstract ~
introduction ~
(technical || example)+ .
conclusion ~
bibliography)"