From d7794e06aca2161be151096c017213ec9181c542 Mon Sep 17 00:00:00 2001 From: bu Date: Mon, 3 Sep 2018 20:56:08 +0200 Subject: [PATCH] Added ISA_tables (inner syntax antiquotations) - Kleinkram. --- Isa_DOF.thy | 75 +++++++++++++---------- examples/conceptual/Attributes.thy | 2 +- examples/scholarly/IsaDofApplications.thy | 34 +++++----- 3 files changed, 62 insertions(+), 49 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 2fb2f447..a8c7b67f 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -43,12 +43,13 @@ typedecl "thy" -- \ and others in the future : file, http, thy, ... \ -consts mk_typ :: "string \ typ" ("@{typ _}") -consts mk_term :: "string \ term" ("@{term _}") -consts mk_thm :: "string \ thm" ("@{thm _}") -consts mk_file :: "string \ file" ("@{file _}") -consts mk_thy :: "string \ thy" ("@{thy _}") -consts mk_docitem :: "string \ 'a" ("@{docitem _}") +consts ISA_typ :: "string \ typ" ("@{typ _}") +consts ISA_term :: "string \ term" ("@{term _}") +consts ISA_thm :: "string \ thm" ("@{thm _}") +consts ISA_file :: "string \ file" ("@{file _}") +consts ISA_thy :: "string \ thy" ("@{thy _}") +consts ISA_docitem :: "string \ 'a" ("@{docitem _}") +consts ISA_docitem_attr :: "string \ string \ 'a" ("@{docitemattr (_) :: (_)}") term "@{typ ''int => int''}" @@ -114,10 +115,10 @@ struct father_is_sub s end - type docobj = {pos : Position.T, - thy_name : string, - value : term, - id : serial, cid : string} + type docobj = {pos : Position.T, + thy_name : string, + value : term, + id : serial, cid : string} type docobj_tab ={tab : (docobj option) Symtab.table, maxano : int @@ -133,20 +134,32 @@ struct in {tab=Symtab.merge X (otab,otab'),maxano=Int.max(m,m')} end) + type ISA_transformer_tab = (term -> term option) Symtab.table + + val initial_ISA_tab:ISA_transformer_tab = Symtab.empty + + (* registrating data of the Isa_DOF component *) structure Data = Generic_Data ( - type T = docobj_tab * docclass_tab - val empty = (initial_docobj_tab, initial_docclass_tab) + type T = docobj_tab * docclass_tab * ISA_transformer_tab + val empty = (initial_docobj_tab, initial_docclass_tab, initial_ISA_tab) val extend = I - fun merge((d1,c1),(d2,c2)) = (merge_docobj_tab (d1, d2), merge_docclass_tab(c1,c2)) + fun merge((d1,c1,e1),(d2,c2,e2)) = (merge_docobj_tab (d1,d2), + merge_docclass_tab (c1,c2), + Symtab.merge (fn (_ , _) => false)(e1,e2) + ) ); + val get_data = Data.get o Context.Proof; val map_data = Data.map; val get_data_global = Data.get o Context.Theory; val map_data_global = Context.theory_map o map_data; +fun apfst f (x, y, z) = (f x, y, z); +fun apsnd f (x, y, z) = (x, f y, z); +fun apthrd f (x, y, z) = (x, y, f z); (* doc-class-name management: We still use the record-package for internally representing doc-classes. The main motivation is that "links" to entities are @@ -157,7 +170,7 @@ val map_data_global = Context.theory_map o map_data; of type names must be reduced to qualifier names only. The used Syntax.parse_typ handling the identification does that already. *) -fun is_subclass (ctxt) s t = is_subclass0(snd(get_data ctxt)) s t +fun is_subclass (ctxt) s t = is_subclass0(#2(get_data ctxt)) s t fun type_name2doc_class_name thy str = (* Long_Name.qualifier *) str @@ -175,32 +188,32 @@ fun name2doc_class_name_local ctxt str = -fun is_defined_cid_global cid thy = let val t = snd(get_data_global thy) +fun is_defined_cid_global cid thy = let val t = #2(get_data_global thy) in cid=default_cid orelse Symtab.defined t (name2doc_class_name thy cid) end -fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt) +fun is_defined_cid_local cid ctxt = let val t = #2(get_data ctxt) in cid=default_cid orelse Symtab.defined t (name2doc_class_name_local ctxt cid) end -fun is_declared_oid_global oid thy = let val {tab,...} = fst(get_data_global thy) +fun is_declared_oid_global oid thy = let val {tab,...} = #1(get_data_global thy) in Symtab.defined tab oid end -fun is_declared_oid_local oid thy = let val {tab,...} = fst(get_data thy) +fun is_declared_oid_local oid thy = let val {tab,...} = #1(get_data thy) in Symtab.defined tab oid end -fun is_defined_oid_global oid thy = let val {tab,...} = fst(get_data_global thy) +fun is_defined_oid_global oid thy = let val {tab,...} = #1(get_data_global thy) in case Symtab.lookup tab oid of NONE => false |SOME(NONE) => false |SOME _ => true end -fun is_defined_oid_local oid thy = let val {tab,...} = fst(get_data thy) +fun is_defined_oid_local oid thy = let val {tab,...} = #1(get_data thy) in case Symtab.lookup tab oid of NONE => false |SOME(NONE) => false @@ -288,13 +301,13 @@ fun declare_anoobject_local ctxt cid = end -fun get_object_global oid thy = let val {tab,...} = fst(get_data_global thy) +fun get_object_global oid thy = let val {tab,...} = #1(get_data_global thy) in case Symtab.lookup tab oid of NONE => error("undefined reference: "^oid) |SOME(bbb) => bbb end -fun get_object_local oid ctxt = let val {tab,...} = fst(get_data ctxt) +fun get_object_local oid ctxt = let val {tab,...} = #1(get_data ctxt) in case Symtab.lookup tab oid of NONE => error("undefined reference: "^oid) |SOME(bbb) => bbb @@ -302,17 +315,17 @@ fun get_object_local oid ctxt = let val {tab,...} = fst(get_data ctxt) fun get_doc_class_global cid thy = if cid = default_cid then error("default doc class acces") (* TODO *) - else let val t = snd(get_data_global thy) + else let val t = #2(get_data_global thy) in (Symtab.lookup t cid) end fun get_doc_class_local cid ctxt = if cid = default_cid then error("default doc class acces") (* TODO *) - else let val t = snd(get_data ctxt) + else let val t = #2(get_data ctxt) in (Symtab.lookup t cid) end -fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt) +fun is_defined_cid_local cid ctxt = let val t = #2(get_data ctxt) in cid=default_cid orelse Symtab.defined t (name2doc_class_name_local ctxt cid) end @@ -320,7 +333,7 @@ fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt) fun get_attributes_local cid ctxt = if cid = default_cid then [] - else let val t = snd(get_data ctxt) + else let val t = #2(get_data ctxt) val cid_long = name2doc_class_name_local ctxt cid in case Symtab.lookup t cid_long of NONE => error("undefined doc class id :"^cid) @@ -378,15 +391,15 @@ fun update_value_global oid upd thy = | NONE => error("undefined doc object: "^oid) -fun writeln_classrefs ctxt = let val tab = snd(get_data ctxt) +fun writeln_classrefs ctxt = let val tab = #2(get_data ctxt) in writeln (String.concatWith "," (Symtab.keys tab)) end -fun writeln_docrefs ctxt = let val {tab,...} = fst(get_data ctxt) +fun writeln_docrefs ctxt = let val {tab,...} = #1(get_data ctxt) in writeln (String.concatWith "," (Symtab.keys tab)) end fun print_doc_items b ctxt = - let val ({tab = x, ...},_)= get_data ctxt; + let val ({tab = x, ...},_,_)= get_data ctxt; val _ = writeln "====================================="; fun print_item (n, SOME({cid,id,pos,thy_name,value})) = (writeln ("docitem: "^n); @@ -400,7 +413,7 @@ fun print_doc_items b ctxt = writeln "=====================================\n\n\n" end; fun print_doc_classes b ctxt = - let val ({tab = _, ...},y)= get_data ctxt; + let val ({tab = _, ...},y,_)= get_data ctxt; val _ = writeln "====================================="; fun print_attr (n, ty, NONE) = (Binding.print n) | print_attr (n, ty, SOME t) = (Binding.print n^"("^Syntax.string_of_term ctxt t^")") @@ -489,7 +502,7 @@ val attributes_upd = fun cid_2_cidType cid_long thy = if cid_long = DOF_core.default_cid then @{typ "unit"} - else let val t = snd(DOF_core.get_data_global thy) + else let val t = #2(DOF_core.get_data_global thy) fun ty_name cid = cid^"."^ Long_Name.base_name cid^"_ext" fun fathers cid_long = case Symtab.lookup t cid_long of NONE => error("undefined doc class id :"^cid_long) diff --git a/examples/conceptual/Attributes.thy b/examples/conceptual/Attributes.thy index a956209b..f27f8670 100644 --- a/examples/conceptual/Attributes.thy +++ b/examples/conceptual/Attributes.thy @@ -75,7 +75,7 @@ ML\ val Const("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attr a2 update_instance*[omega::E, a2+="1"] -ML\ val Const("Groups.one_class.one", @{typ "int"})= @{docitem_attr a2 :: omega} \ +ML\ val (s as Const("Groups.one_class.one", @{typ "int"}))= @{docitem_attr a2 :: omega} \ update_instance*[omega::E, a2+="6"] diff --git a/examples/scholarly/IsaDofApplications.thy b/examples/scholarly/IsaDofApplications.thy index 660a19bb..63a22767 100644 --- a/examples/scholarly/IsaDofApplications.thy +++ b/examples/scholarly/IsaDofApplications.thy @@ -31,46 +31,46 @@ mechanism for linking informal and formal parts of a document. In this paper, we present \isadof, a novel Document Ontology Framework on top of Isabelle. \isadof allows for conventional typesetting -\emph{as well} as formal development. We show how to model document +\<^emph>\as well\ as formal development. We show how to model document ontologies inside \isadof, how to use the resulting meta-information for enforcing a certain document structure, and discuss ontology-specific IDE support. \ section*[intro::introduction]\ Introduction \ text*[introtext::introduction]\ -The linking of the \emph{formal} to the \emph{informal} is perhaps the +The linking of the \<^emph>\formal\ to the \<^emph>\informal\ is perhaps the most pervasive challenge in the digitization of knowledge and its propagation. This challenge incites numerous research efforts summarized under the labels ``semantic web'', ``data mining'', or any form of advanced ``semantic'' text processing. A key role in -structuring this linking play \emph{document ontologies} (also called -\emph{vocabulary} in the semantic web -community~\cite{w3c:ontologies:2015}), \ie, a machine-readable form of -the structure of documents as well as the document discourse. +structuring this linking play \<^emph>\document ontologies\ (also called +\<^emph>\vocabulary\ in the semantic web community~\cite{w3c:ontologies:2015}), +\ie, a machine-readable form of the structure of documents as well as +the document discourse. + Such ontologies can be used for the scientific discourse within scholarly articles, mathematical libraries, and in the engineering discourse of standardized software certification documents~\cite{boulanger:cenelec-50128:2015,cc:cc-part3:2006}. Further applications are the domain-specific discourse in juridical texts or medical reports. -In general, an ontology is a formal explicit description of \emph{concepts} -in a domain of discourse (called \emph{classes}), properties of each concept -describing \emph{attributes} of the concept, as well as \emph{links} between -them. A particular link between concepts is the \emph{is-a} relation declaring +In general, an ontology is a formal explicit description of \<^emph>\concepts\ +in a domain of discourse (called \<^emph>\classes\), properties of each concept +describing \<^emph>\attributes\ of the concept, as well as \<^emph>\links\ between +them. A particular link between concepts is the \<^emph>\is-a\ relation declaring the instances of a subclass to be instances of the super-class. The main objective of this paper is to present \isadof, a novel -framework to \emph{model} typed ontologies and to \emph{enforce} them during +framework to \<^emph>\model\ typed ontologies and to \<^emph>\enforce\ them during document evolution. Based on Isabelle infrastructures, ontologies may refer to types, terms, proven theorems, code, or established assertions. Based on a novel adaption of the Isabelle IDE, a document is checked to be -\emph{conform} to a particular ontology---\isadof is -designed to give fast user-feedback \emph{during the capture of -content}. This is particularly valuable in case of document changes, -where the \emph{coherence} between the formal and the informal parts of the +\<^emph>\conform\ to a particular ontology---\isadof is designed to give fast user-feedback +\<^emph>\during the capture of content\. This is particularly valuable in case of document +changes, where the \<^emph>\coherence\ between the formal and the informal parts of the content can be mechanically checked. -To avoid any misunderstanding: \isadof is \emph{not a theory in HOL} +To avoid any misunderstanding: \isadof is \<^emph>\not a theory in HOL\ on ontologies and operations to track and trace links in texts, -it is an \emph{environment to write structured text} which \emph{may contain} +it is an \<^emph>\environment to write structured text\ which \<^emph>\may contain\ Isabelle/HOL definitions and proofs like mathematical articles, tech-reports and scientific papers---as the present one, which is written in \isadof itself. \isadof is a plugin into the Isabelle/Isar