From f8692dd801c5d0eaa94f48acbfaeb4f466e81705 Mon Sep 17 00:00:00 2001 From: bu Date: Thu, 5 Apr 2018 12:09:58 +0200 Subject: [PATCH] =?UTF-8?q?Renamed=20LNCS=5Fonto=20into=20=E2=80=9Cscholar?= =?UTF-8?q?ly=5Fpaper=E2=80=9D.=20Decided=20for=20the=20trace=20variant=20?= =?UTF-8?q?semantics=20of=20monitors.=20(more=20power,=20easier=20to=20imp?= =?UTF-8?q?lement)?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Isa_DOF.thy | 48 ++++++++-------- .../{LNCS_onto.thy => scholarly_paper.thy} | 56 +++++++------------ 2 files changed, 43 insertions(+), 61 deletions(-) rename ontologies/{LNCS_onto.thy => scholarly_paper.thy} (59%) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 641c696..9b71fae 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -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 _ = diff --git a/ontologies/LNCS_onto.thy b/ontologies/scholarly_paper.thy similarity index 59% rename from ontologies/LNCS_onto.thy rename to ontologies/scholarly_paper.thy index 898a0c0..28f0e05 100644 --- a/ontologies/LNCS_onto.thy +++ b/ontologies/scholarly_paper.thy @@ -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 -- \adding a contribution list and checking that it is cited as well in tech as in conclusion. ? \ @@ -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)" - --- \other idea: capture the essence of a monitor class as trace. +-- \underlying idea: capture the essence of a monitor class as trace. trace would be `predefined id` like `main` in C. \ 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)"