diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 16f9435a..efdf90b6 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -11,25 +11,18 @@ that provide direct support in the PIDE framework. *} theory Isa_DOF (* Isabelle Document Ontology Framework *) imports Main (* Isa_MOF *) keywords "section*" "subsection*" "subsubsection*" - "paragraph*" "subparagraph*" "text*" "declare_reference"::thy_decl + "paragraph*" "subparagraph*" "text*" + "open_monitor*" "close_monitor*" "declare_reference*" + "update_instance*" ::thy_decl and "doc_class" :: thy_decl begin + -text{* - @{thm [names_long] refl} - -*} -section{* A HomeGrown Document Type Management (the ''Model'') *} - +section{*Primitive Markup Generators*} ML{* -curry; -op |>; -op #>; -op |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c; -op ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b; val docrefN = "docref"; val docclassN = "doc_class"; @@ -47,9 +40,9 @@ val docclass_markup = docref_markup_gen docclassN *} +section{* A HomeGrown Document Type Management (the ''Model'') *} ML{* - structure DOF_core = struct type docclass_struct = {params : (string * sort) list, (*currently not used *) @@ -71,11 +64,11 @@ struct fun is_subclass0 (tab:docclass_tab) s t = let val _ = case Symtab.lookup tab t of NONE => if t <> default_cid - then error "document superclass not defined" + then error ("document superclass not defined: "^t) else default_cid | SOME _ => "" fun father_is_sub s = case Symtab.lookup tab s of - NONE => error "document subclass not defined" + NONE => error ("document subclass not defined: "^s) | SOME ({inherits_from=NONE, ...}) => s = t | SOME ({inherits_from=SOME (_,s'), ...}) => s' = t orelse father_is_sub s' @@ -100,7 +93,7 @@ struct in {tab=Symtab.merge X (otab,otab'),maxano=Int.max(m,m')} end) - +(* registrating data of the Isa_DOF component *) structure Data = Generic_Data ( type T = docobj_tab * docclass_tab @@ -154,137 +147,130 @@ fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt) end -fun is_declared_oid_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy) - in Symtab.defined t oid end +fun is_declared_oid_global oid thy = let val {tab,...} = fst(get_data_global thy) + in Symtab.defined tab oid end -fun is_declared_oid_local oid thy = let val {tab=t,maxano=_} = fst(get_data thy) - in Symtab.defined t oid end +fun is_declared_oid_local oid thy = let val {tab,...} = fst(get_data thy) + in Symtab.defined tab oid end -fun is_defined_oid_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy) - in case Symtab.lookup t oid of +fun is_defined_oid_global oid thy = let val {tab,...} = fst(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=t,maxano=_} = fst(get_data thy) - in case Symtab.lookup t oid of +fun is_defined_oid_local oid thy = let val {tab,...} = fst(get_data thy) + in case Symtab.lookup tab oid of NONE => false |SOME(NONE) => false |SOME _ => true end -fun declare_object_global oid thy = (map_data_global - (apfst(fn {tab=t,maxano=x} => - {tab=Symtab.update_new(oid,NONE)t, - maxano=x})) - (thy) - handle Symtab.DUP _ => - error("multiple declaration of document reference")) +fun declare_object_global oid thy = + let fun decl {tab=t,maxano=x} = {tab=Symtab.update_new(oid,NONE)t, maxano=x} -fun declare_object_local oid ctxt = (map_data (apfst(fn {tab=t,maxano=x} => - {tab=Symtab.update_new(oid,NONE) t, - maxano=x})) - (ctxt) - handle Symtab.DUP _ => - error("multiple declaration of document reference")) + in (map_data_global (apfst(decl)) (thy) + handle Symtab.DUP _ => error("multiple declaration of document reference")) + end + +fun declare_object_local oid ctxt = + let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab, maxano=maxano} + in (map_data(apfst decl)(ctxt) + handle Symtab.DUP _ => error("multiple declaration of document reference")) + end fun define_doc_class_global (params', binding) parent fields thy = - let val nn = Context.theory_name thy (* in case that we need the thy-name to identify - the space where it is ... *) - val cid = (Binding.name_of binding) - val pos = (Binding.pos_of binding) - - val _ = if is_defined_cid_global cid thy - then error("redefinition of document class") - else () - - val _ = case parent of (* the doc_class may be root, but must refer - to another doc_class and not just an - arbitrary type *) - NONE => () - | SOME(_,cid_parent) => - if not (is_defined_cid_global cid_parent thy) - then error("document class undefined : " ^ cid_parent) - else () - val cid_long = name2doc_class_name thy cid - val id = serial (); - val _ = Position.report pos (docclass_markup true cid id pos); - - val info = {params=params', - name = binding, - thy_name = nn, - id = id, (* for pide --- really fresh or better reconstruct - from prior record definition ? *) - inherits_from = parent, - attribute_decl = fields (* currently unchecked *) - (*, rex : term list -- not yet used *)} - val _ = () (* XXX *) - - in map_data_global(apsnd(Symtab.update(cid_long,info)))(thy) - end + let val nn = Context.theory_name thy (* in case that we need the thy-name to identify + the space where it is ... *) + val cid = (Binding.name_of binding) + val pos = (Binding.pos_of binding) + + val _ = if is_defined_cid_global cid thy + then error("redefinition of document class") + else () + + val _ = case parent of (* the doc_class may be root, but must refer + to another doc_class and not just an + arbitrary type *) + NONE => () + | SOME(_,cid_parent) => + if not (is_defined_cid_global cid_parent thy) + then error("document class undefined : " ^ cid_parent) + else () + val cid_long = name2doc_class_name thy cid + val id = serial (); + val _ = Position.report pos (docclass_markup true cid id pos); + + val info = {params=params', + name = binding, + thy_name = nn, + id = id, (* for pide --- really fresh or better reconstruct + from prior record definition ? For the moment: own + generation of serials ... *) + inherits_from = parent, + attribute_decl = fields (* currently unchecked *) + (*, rex : term list -- not yet used *)} + + in map_data_global(apsnd(Symtab.update(cid_long,info)))(thy) + end fun define_object_global (oid, bbb) thy = - let val nn = Context.theory_name thy (* in case that we need the thy-name to identify - the space where it is ... *) - in if is_defined_oid_global oid thy - then error("multiple definition of document reference") - else map_data_global (apfst(fn {tab=t,maxano=x} => - {tab=Symtab.update(oid,SOME bbb) t, - maxano=x})) - (thy) - end + let val nn = Context.theory_name thy (* in case that we need the thy-name to identify + the space where it is ... *) + in if is_defined_oid_global oid thy + then error("multiple definition of document reference") + else map_data_global (apfst(fn {tab=t,maxano=x} => + {tab=Symtab.update(oid,SOME bbb) t, + maxano=x})) + (thy) + end fun define_object_local (oid, bbb) ctxt = - map_data (apfst(fn {tab=t,maxano=x} => - {tab=Symtab.update(oid,SOME bbb) t,maxano=x})) ctxt + map_data (apfst(fn{tab,maxano}=>{tab=Symtab.update(oid,SOME bbb)tab,maxano=maxano})) ctxt (* declares an anonyme label of a given type and generates a unique reference ... *) -fun declare_anoobject_global thy cid = map_data_global - (apfst(fn {tab=t,maxano=x} => - let val str = cid^":"^Int.toString(x+1) - val _ = writeln("Anonymous doc-ref declared: " - ^str) - in {tab=Symtab.update(str,NONE)t,maxano=x+1} - end)) - (thy) +fun declare_anoobject_global thy cid = + let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1) + val _ = writeln("Anonymous doc-ref declared: " ^ str) + in {tab=Symtab.update(str,NONE)tab,maxano= maxano+1} end + in map_data_global (apfst declare) (thy) + end -fun declare_anoobject_local ctxt cid = map_data - (apfst(fn {tab=t,maxano=x} => - let val str = cid^":"^Int.toString(x+1) - val _ = writeln("Anonymous doc-ref declared: " - ^str) - in {tab=Symtab.update(str,NONE)t, maxano=x+1} - end)) - (ctxt) +fun declare_anoobject_local ctxt cid = + let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1) + val _ = writeln("Anonymous doc-ref declared: " ^str) + in {tab=Symtab.update(str,NONE)tab, maxano=maxano+1} end + in map_data (apfst declare) (ctxt) + end -fun get_object_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy) - in case Symtab.lookup t oid of - NONE => error"undefined reference" - |SOME(bbb) => bbb - end +fun get_object_global oid thy = let val {tab,...} = fst(get_data_global thy) + in case Symtab.lookup tab oid of + NONE => error"undefined reference" + |SOME(bbb) => bbb + end -fun get_object_local oid ctxt = let val {tab=t,maxano=_} = fst(get_data ctxt) - in case Symtab.lookup t oid of - NONE => error"undefined reference" - |SOME(bbb) => bbb - end +fun get_object_local oid ctxt = let val {tab,...} = fst(get_data ctxt) + in case Symtab.lookup tab oid of + NONE => error"undefined reference" + |SOME(bbb) => bbb + end 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) - in (Symtab.lookup t cid) end - + if cid = default_cid then error("default doc class acces") (* TODO *) + else let val t = snd(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) - in (Symtab.lookup t cid) end + if cid = default_cid then error("default doc class acces") (* TODO *) + else let val t = snd(get_data ctxt) + in (Symtab.lookup t cid) end fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt) @@ -292,38 +278,52 @@ fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt) Symtab.defined t (name2doc_class_name_local ctxt cid) end -fun writeln_classrefs ctxt = let val t = snd(get_data ctxt) - in writeln (String.concatWith "," (Symtab.keys t)) end +fun writeln_classrefs ctxt = let val tab = snd(get_data ctxt) + in writeln (String.concatWith "," (Symtab.keys tab)) end -fun writeln_docrefs ctxt = let val {tab=t,maxano=_} = fst(get_data ctxt) - in writeln (String.concatWith "," (Symtab.keys t)) end +fun writeln_docrefs ctxt = let val {tab,...} = fst(get_data ctxt) + in writeln (String.concatWith "," (Symtab.keys tab)) end end (* struct *) *} -section{* Syntax for Annotated Documentation Commands (the '' View'') *} - +section{* Syntax for Annotated Documentation Commands (the '' View'' Part I) *} ML{* -structure DocAttrParser = +structure AnnoTextelemParser = struct val semi = Scan.option (Parse.$$$ ";"); val attribute = - Parse.position Parse.name - -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) ""; + Parse.position Parse.name + -- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) ""; +val attribute_upd = + Parse.position Parse.name + -- (Parse.$$$ "+=" || Parse.$$$ "=") + -- Parse.!!! Parse.name; +(* +Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ uncheckedN) +*) val reference = - Parse.position Parse.name - -- Scan.option (Parse.$$$ "::" |-- Parse.!!! (Parse.position Parse.name)); + Parse.position Parse.name + -- Scan.option (Parse.$$$ "::" |-- Parse.!!! (Parse.position Parse.name)); -val attributes = (Parse.$$$ "[" |-- (reference -- - (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) [])) - --| Parse.$$$ "]" +val attributes = + (Parse.$$$ "[" + |-- (reference -- + (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) [])) + --| Parse.$$$ "]" + +val attributes_upd = + (Parse.$$$ "[" + |-- (reference -- + (Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute_upd))) [])) + --| Parse.$$$ "]" fun enriched_document_command markdown (((((oid,pos),cid_pos),doc_attrs), @@ -341,18 +341,8 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos),doc_attrs), then error("document class undefined") else () val cid_long = DOF_core.name2doc_class_name thy cid - val _ = writeln cid_long - -(* - val {pos=pos_decl,id,cid,...} = the(DOF_core.get_object_global name thy) - val markup = docref_markup false name id pos_decl; - val _ = Context_Position.report ctxt pos markup; -Context.Theory; -Context_Position.report_generic; - -*) val {id, name=bind_target,...} = - the(DOF_core.get_doc_class_global cid_long thy) + the(DOF_core.get_doc_class_global cid_long thy) val markup = docclass_markup false cid id (Binding.pos_of bind_target); val ctxt = Context.Theory thy val _ = Context_Position.report_generic ctxt pos' markup; @@ -366,7 +356,7 @@ Context_Position.report_generic; let val name = Context.theory_name thy in DOF_core.define_object_global (oid, {pos=pos, thy_name=name, - id=id , cid=DOF_core.default_cid}) + id=id, cid=DOF_core.default_cid}) (thy) end fun MMM(SOME(s,p)) = SOME(s^"XXX",p) @@ -410,11 +400,38 @@ val _ = >> enriched_document_command {markdown = false}); val _ = - Outer_Syntax.command @{command_keyword "declare_reference"} "declare document reference" - (attributes >> (fn (((oid,pos),cid),doc_attrs) => - (Toplevel.theory (DOF_core.declare_object_global oid)))); + Outer_Syntax.command @{command_keyword "declare_reference*"} + "declare document reference" + (attributes >> (fn (((oid,pos),cid),doc_attrs) => + (Toplevel.theory (DOF_core.declare_object_global oid)))); +val _ = + Outer_Syntax.command @{command_keyword "open_monitor*"} + "open a document reference monitor" + (attributes >> (fn (((oid,pos),cid),doc_attrs) => + (Toplevel.theory (DOF_core.declare_object_global oid)))); +val _ = + Outer_Syntax.command @{command_keyword "close_monitor*"} + "close a document reference monitor" + (attributes >> (fn (((oid,pos),cid),doc_attrs) => + (Toplevel.theory (I)))); (* dummy so far *) + +val _ = + Outer_Syntax.command @{command_keyword "update_instance*"} + "update meta-attributes of an instance of a document class" + (attributes_upd >> (fn (((oid,pos),cid),doc_attrs) => + (Toplevel.theory (I)))); (* dummy so far *) + +end (* struct *) + +*} + +section{* Syntax for Ontological Antiquotations (the '' View'' Part II) *} + +ML{* +structure OntoLinkParser = +struct fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name = @@ -432,11 +449,13 @@ fun check_and_mark ctxt cid_decl (str:{strict_checking: bool}) pos name = else () in name end else if DOF_core.is_declared_oid_global name thy - then (if #strict_checking str then warning("declared but undefined document reference:"^name) + then (if #strict_checking str + then warning("declared but undefined document reference:"^name) else (); name) else error("undefined document reference:"^name) end + (* generic syntax for doc_class links. *) val defineN = "define" @@ -446,36 +465,37 @@ val doc_ref_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc >> (fn str => if str = defineN then {unchecked = false, define= true} else {unchecked = true, define= false})) - {unchecked = false, define= false}; + {unchecked = false, define= false} (* default *); fun doc_class_ref_antiquotation name cid_decl = - let fun open_par x = if x then (writeln "ctr_anti true"; "\\label{" ) - else (writeln "ctr_anti false"; "\\autoref{" ) + let fun open_par x = if x then "\\label{" + else "\\autoref{" val close = "}" in -(* Thy_Output.antiquotation name (Scan.lift (args_alt -- Args.cartouche_input)) *) Thy_Output.antiquotation name (Scan.lift (doc_ref_modes -- Args.cartouche_input)) - (fn {context =ctxt, source = src:Token.src, state} => + (fn {context = ctxt, source = src:Token.src, state} => fn ({unchecked = x, define= y}, source:Input.source) => (Thy_Output.output_text state {markdown=false} #> - check_and_mark ctxt cid_decl ({strict_checking = not x})(Input.pos_of source) #> + check_and_mark ctxt + cid_decl + ({strict_checking = not x}) + (Input.pos_of source) #> enclose (open_par y) close) source) end (* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*) -val _ = Theory.setup - ((doc_class_ref_antiquotation @{binding docref} DOF_core.default_cid ) -(* #> - (doc_class_antiquotation @{binding docref_unchecked} DOF_core.default_cid )#> - (doc_class_antiquotation @{binding docref_define} DOF_core.default_cid )) -*) ) +val _ = Theory.setup (doc_class_ref_antiquotation @{binding docref} DOF_core.default_cid) end (* struct *) *} +section{* Syntax for Ontologies (the '' View'' Part III) *} + ML{* +structure OntoParser = +struct fun read_parent NONE ctxt = (NONE, ctxt) | read_parent (SOME raw_T) ctxt = @@ -488,70 +508,91 @@ 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_record_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; - in thy |> Record.add_record overloaded (params', binding) parent fields - |> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' - 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; val _ = Outer_Syntax.command @{command_keyword doc_class} "define document class" - (Parse_Spec.overloaded - -- (Parse.type_args_constrained -- Parse.binding) - -- (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) - -- Scan.repeat1 (Parse.const_binding -- Scan.option (@{keyword "<="} |-- Parse.term))) - -- Scan.repeat (@{keyword "where"} |-- Parse.term) + ((Parse_Spec.overloaded + -- (Parse.type_args_constrained -- Parse.binding) + -- (@{keyword "="} + |-- Scan.option (Parse.typ --| @{keyword "+"}) + -- Scan.repeat1 + (Parse.const_binding -- Scan.option (@{keyword "<="} |-- Parse.term))) + -- Scan.repeat (@{keyword "where"} |-- Parse.term)) >> (fn (((overloaded, x), (y, z)),rex) => - Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z rex))); + Toplevel.theory (add_doc_class_cmd {overloaded = overloaded} x y z rex))); + +end (* struct *) *} + + + + + + + + + + + + + section{* Testing and Validation *} -ML{* op >> ; +ML{* (* Parsing combinators in Scan *) + op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c; + op || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b; + op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e; + op |-- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'd * 'e; + op --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * 'e; + Scan.repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a; + Scan.option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a; +*} +ML{* Binding.print; +Syntax.read_sort; +Syntax.read_typ; Syntax.read_term; Syntax.pretty_typ; -try; + *} - -(* Look at this thingi ... *) -ML \ -fun document_command markdown (loc, txt) = - Toplevel.keep - (fn state => (case loc of - NONE => ignore (Thy_Output.output_text state markdown txt) - | SOME (_, pos) => error ("Illegal target specification -- not a theory context" - ^ Position.here pos))) - o Toplevel.present_local_theory loc - (fn state => ignore (Thy_Output.output_text state markdown txt)); - -\ - -text{* @{theory "Nat"} @{thm refl}*} ML\ open Markup; Markup.binding; open Position; +open Binding; Position.line; + Context.Theory; Context_Position.report_generic; Context_Position.report; diff --git a/MOF.sml b/MOF.sml new file mode 100644 index 00000000..61b787d1 --- /dev/null +++ b/MOF.sml @@ -0,0 +1,71 @@ +structure MOF : sig + type 'a equal + type num + type 'a rexp + type char + type attribute_types + type class_hierarchy + val mt : class_hierarchy + val classes : class_hierarchy -> string list + val all_entities : + class_hierarchy -> ((string * (string * string) rexp) list) list + val all_attributes : class_hierarchy -> ((string * attribute_types) list) list + val remove_overrides : 'b equal -> ('a -> 'b) -> 'a list -> 'a list +end = struct + +type 'a equal = {equal : 'a -> 'a -> bool}; +val equal = #equal : 'a equal -> 'a -> 'a -> bool; + +datatype int = Int_of_integer of IntInf.int; + +datatype num = One | Bit0 of num | Bit1 of num; + +datatype 'a rexp = Empty | Atom of 'a | Alt of 'a rexp * 'a rexp | + Conc of 'a rexp * 'a rexp | Star of 'a rexp; + +datatype char = Zero_char | Char of num; + +datatype attribute_types = File_T of string | Image_file_T of string | + Thms_T of string list | Int_T of int | Bool_T of bool | String_T of string | + Text_T of string | Range_T of int * int option | Enum_T of string list; + +datatype class_hierarchy = + Class_T of + string * class_hierarchy list * (string * attribute_types) list * + (string * (string * string) rexp) list; + +fun eq A_ a b = equal A_ a b; + +fun maps f [] = [] + | maps f (x :: xs) = f x @ maps f xs; + +fun implode _ = raise Fail "String.implode"; + +val mt : class_hierarchy = + Class_T (implode [Char (Bit1 (Bit1 (Bit1 (Bit1 (Bit0 One)))))], [], [], []); + +fun member A_ [] y = false + | member A_ (x :: xs) y = eq A_ x y orelse member A_ xs y; + +fun map f [] = [] + | map f (x21 :: x22) = f x21 :: map f x22; + +fun classes (Class_T (name, sub_classes, attr, comps)) = + name :: maps classes sub_classes; + +fun entities (Class_T (x1, x2, x3, x4)) = x4; + +fun all_entities (Class_T (name, sub_classes, attr, comps)) = + comps :: map entities sub_classes; + +fun attributes (Class_T (x1, x2, x3, x4)) = x3; + +fun all_attributes (Class_T (name, sub_classes, attr, comps)) = + attr :: map attributes sub_classes; + +fun remove_overrides B_ f [] = [] + | remove_overrides B_ f (a :: r) = + (if member B_ (map f r) (f a) then remove_overrides B_ f r + else a :: remove_overrides B_ f r); + +end; (*struct MOF*) diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy new file mode 100644 index 00000000..d70fbff7 --- /dev/null +++ b/examples/cenelec/Example.thy @@ -0,0 +1,113 @@ +theory Example + imports "../../ontologies/CENELEC_50126" +begin + +section{* Some show-off's of general antiquotations. *} + + +(* some show-off of standard anti-quotations: *) +print_attributes +print_antiquotations + +text{* @{thm refl} of name @{thm [source] refl} + @{thm[mode=Rule] conjI} + @{file "../../Isa_DOF.thy"} + @{value "3+4::int"} + @{const hd} + @{theory List}} + @{term "3"} + @{type bool} + @{term [show_types] "f x = a + x"} *} + +section{* Example *} + +text*[tralala] {* Brexit means Brexit *} + +text*[ass1::assumption] {* Brexit means Brexit *} + +text*[hyp1::hypothesis] {* P means not P *} + + +text*[ass122::srac] {* The overall sampling frequence of the odometer +subsystem is therefore 14 khz, which includes sampling, computing and +result communication times... *} + +text*[t10::test_result] {* This is a meta-test. This could be an ML-command +that governs the external test-execution via, eg., a makefile or specific calls +to a test-environment or test-engine *} + + +text \ As established by @{docref (unchecked) \t10\}, + @{docref (define) \t10\} \ +text \ the @{docref \t10\} + the @{docref \ass122\} + \ +text \ safety related applicability condition @{srac \ass122\}. \ +text \ exported constraint @{ec \ass122\}. + \ + +text{* And some ontologically inconsistent reference: @{hypothesis \ass1\} as well as *} +-- wrong + +text{* ... some more ontologically inconsistent reference: @{assumption \hyp1\} as well as *} +-- wrong + + + +text{* And a further ontologically totally inconsistent reference: + @{test_result \ass122\} as well as ... *} +-- wrong + +text{* the ontologically inconsistent reference: @{ec \t10\} *} +-- wrong + + + +section{* Some Tests for Ontology Framework and its CENELEC Instance *} + +declare_reference* [lalala::requirement, alpha="main", beta=42] + +declare_reference* [lalala::quod] (* shouldn't work *) + +declare_reference* [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1] + +paragraph*[sdf]{* just a paragraph *} +paragraph* [sdfk] \ just a paragraph - lexical variant \ + +subsection*[sdf]{* shouldn't work, multiple ref. *} + +section*[sedf::requirement, alpja= refl]{* works again. One can hover over the class constraint and + jump to its definition. *} +text\\label{sedf}\ (* Hack to make the LaTeX-ing running. Should disappear. *) + +section*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with attribute setting, +but wrong doc_class constraint. *} + +section{* Text Antiquotation Infrastructure ... *} + +text{* @{docref \lalala\} -- produces warning. *} +text{* @{docref (unchecked) \lalala\} -- produces no warning. *} + +text{* @{docref \ass122\} -- global reference to a text-item in another file. *} + +text{* @{ec \ass122\} -- global reference to a exported constraint in another file. + Note that the link is actually a srac, which, according to + the ontology, happens to be an "ec". *} + +text{* @{test_specification \ass122\} -- wrong: "reference ontologically inconsistent". *} + + + +text{* Here is a reference to @{docref \sedf\} *} +(* works currently only in connection with the above label-hack. + Try to hover over the sedf - link and activate it !!! *) + + +section{* Miscellaneous ...*} + +section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *) + + +end + + \ No newline at end of file diff --git a/examples/simple/Article.thy b/examples/simple/Article.thy new file mode 100644 index 00000000..faa5344e --- /dev/null +++ b/examples/simple/Article.thy @@ -0,0 +1,66 @@ +(* << *) +theory Article + imports "../../ontologies/scholarly_paper" +begin +(* >> *) + +open_monitor*[onto::article] + +text*[tit::title]{* Using The Isabelle Ontology Framework*} + +text*[stit::subtitle] \Linking the Formal with the Informal\ + +text*[auth1::author, affiliation="Université Paris-Sud"]\Burkhart Wolff\ + +text*[abs::abstract, keyword_list="[]"] {* Isabelle/Isar is a system +framework with many similarities to Eclipse; it is mostly known as part of +Isabelle/HOL, an interactive theorem proving and code generation environment. +Recently, an Document Ontology Framework has been developed as a plugin in +Isabelle/Isar, allowing to do both conventional typesetting \emph{as well} +as formal development. A particular asset is the possibility to control the links +between the formal and informal aspects of a document +via (a novel use of) Isabelle's antiquotation mechanism. *} + +section*[intro::introduction, comment="''This is a comment''"]{* Introduction *} +text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, +phasellus amet id massa nunc, pede suscipit repellendus, in ut tortor eleifend augue +pretium consectetuer. Lectus accumsan velit ultrices, mauris amet, id elit aliquam aptent id, +felis duis. Mattis molestie semper gravida in ullamcorper ut, id accumsan, fusce id +sed nibh ut lorem integer, maecenas sed mi purus non nunc, morbi pretium tortor.*} + +section*[bgrnd::text_section]{* Background: Isabelle and Isabelle_DOF *} +text{* As mentioned in @{introduction \intro\} ... *} + +update_instance*[bgrnd, main_author = "Some(''bu'')"] + +section*[ontomod::technical]{* Modeling Ontologies in Isabelle_DOF *} +text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi,*} + +subsection*[scholar_onto::example]{* A Scholar Paper: Eating one's own dogfood. *} + +subsection*[mathex_onto::example]{* Math-Exercise *} + +section*[con::conclusion]{* Future Work: Monitoring Classes *} +text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *} + +subsection*[related::related_work]{* Related Work *} +text{* +\ @{bold \XML\} and dtd's, +\ OWL and Protege, +\ LaTeX setups such as ... + @{url "https://pdi.fbk.eu/technologies/tex-owl-latex-style-syntax-authoring-owl-2-ontologies"} +\ Structured Assurance Case Metamodel Specification. + @{url "https://www.omg.org/spec/SACM/1.0/About-SACM/"}} +\ AADL Alisa, +\ RATP Ovado +*} + +subsection{* Discussion *} +text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *} + +close_monitor*[onto] + +(* << *) +end +(* >> *) + diff --git a/examples/simple/Example.thy b/examples/simple/Example.thy index 5429760b..4a32d76b 100644 --- a/examples/simple/Example.thy +++ b/examples/simple/Example.thy @@ -6,17 +6,76 @@ begin section{* Some show-off's of general antiquotations. *} -(* some show-off of standard anti-quotations: *) -text{* @{thm refl} - @{file "../../Isa_DOF.thy"} - @{value "3+4::int"} - @{const hd} - @{theory List}} - @{term "3"} - @{type bool} - @{term [show_types] "f x = a + x"} *} +(* some show-off of standard anti-quotations: *) +print_attributes +print_antiquotations + +text{* @{thm refl} of name @{thm [source] refl} + @{thm[mode=Rule] conjI} + @{file "../../Isa_DOF.thy"} + @{value "3+4::int"} + @{const hd} + @{theory List}} + @{term "3"} + @{type bool} + @{term [show_types] "f x = a + x"} *} +section{* Example *} + +text*[ass1::assumption] {* Brexit means Brexit *} + +text*[hyp1::hypothesis] {* P means not P *} + + +text*[ass122::srac] {* The overall sampling frequence of the odometer +subsystem is therefore 14 khz, which includes sampling, computing and +result communication times... *} + +text*[t10::test_result] {* This is a meta-test. This could be an ML-command +that governs the external test-execution via, eg., a makefile or specific calls +to a test-environment or test-engine *} + + +text \ As established by @{docref (unchecked) \t10\}, + @{docref (define) \t10\} + the @{docref \t10\} + the @{docref \ass122\} + \ +text \ safety related applicability condition @{srac \ass122\}. + exported constraint @{ec \ass122\}. + \ + +text{* + And some ontologically inconsistent reference: + @{hypothesis \ass1\} as well as + +*} +-- "very wrong" + +text{* + And some ontologically inconsistent reference: + @{assumption \hyp1\} as well as + +*} +-- "very wrong" + + + +text{* + And some ontologically inconsistent reference: + @{test_result \ass122\} as well as + +*} +-- wrong + +text{* + And some other ontologically inconsistent reference: + @{ec \t10\} as well as +*} +-- wrong + + section{* Some Tests for Ontology Framework and its CENELEC Instance *} @@ -90,8 +149,6 @@ term "a + b = b + a" section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *) - - end \ No newline at end of file diff --git a/ontologies/CENELEC_50126.thy b/ontologies/CENELEC_50126.thy index 4589962a..4e440156 100644 --- a/ontologies/CENELEC_50126.thy +++ b/ontologies/CENELEC_50126.thy @@ -9,7 +9,7 @@ Common Criteria identifies: (for the moment: defined by regular expressions describing the order of category instances in the overall document as a regular language) *} - + theory CENELEC_50126 imports "../Isa_DOF" begin @@ -62,7 +62,7 @@ doc_class assumption = requirement + text{*The category @{emph \exported constraint\} (or @{emph \ec\} for short) is used for formal assumptions, that arise during the analysis, design or implementation and have to be tracked till the final - evaluation target,and discharged by appropriate validation procedures + evaluation target, and discharged by appropriate validation procedures within the certification process, by it by test or proof. *} doc_class ec = assumption + @@ -144,46 +144,6 @@ doc_class test_documentation = - -section{* Example *} - -text*[ass122::srac] {* The overall sampling frequence of the odometer -subsystem is therefore 14 khz, which includes sampling, computing and -result communication times... *} - -text*[t10::test_result] {* This is a meta-test. This could be an ML-command -that governs the external test-execution via, eg., a makefile or specific calls -to a test-environment or test-engine *} - - -text \ As established by @{docref (unchecked) \t10\}, - @{docref (define) \t10\} - the @{docref \t10\} - assumption @{docref \ass122\} is validated. \ - - -section{* Provisory Setup *} - -(* Hack: This should be generated automatically: *) -ML{* -val _ = Theory.setup - ((DocAttrParser.doc_class_ref_antiquotation @{binding srac} - (DOF_core.name2doc_class_name @{theory} "srac") - ) #> - (DocAttrParser.doc_class_ref_antiquotation @{binding ec} - (DOF_core.name2doc_class_name @{theory} "ec") - )#> - (DocAttrParser.doc_class_ref_antiquotation @{binding test_specification} - (DOF_core.name2doc_class_name @{theory} "test_specification") - )) - -*} - - - - - - section{* Testing and Validation *} @@ -193,13 +153,15 @@ DOF_core.name2doc_class_name @{theory} "requirement"; DOF_core.name2doc_class_name @{theory} "srac"; DOF_core.is_defined_cid_global "srac" @{theory}; DOF_core.is_defined_cid_global "ec" @{theory}; - +"XXXXXXXXXXXXXXXXX"; +DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.ec"; DOF_core.is_subclass @{context} "CENELEC_50126.srac" "CENELEC_50126.ec"; DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.srac"; - -val ({maxano, tab},tab2) = DOF_core.get_data @{context}; -Symtab.dest tab; -Symtab.dest tab2; +DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.test_requirement"; +"XXXXXXXXXXXXXXXXX"; +val ({maxano, tab=ref_tab},class_tab) = DOF_core.get_data @{context}; +Symtab.dest ref_tab; +Symtab.dest class_tab; *} diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy new file mode 100644 index 00000000..7060964e --- /dev/null +++ b/ontologies/mathex_onto.thy @@ -0,0 +1,19 @@ +theory mathex_onto + +imports "../Isa_DOF" +begin + +doc_class Question = + content :: "(string + term) list" + +doc_class Response = + content :: "(string + term) list" + +doc_class Exercise_part = + question :: Question + response :: Response + +doc_class Exercise= + content :: "(Exercise_part) list" + +end \ No newline at end of file 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 898a0c0c..28f0e056 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)"