From 3338fffe199e9d5e74f6892118d1366180297cee Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 4 Apr 2018 10:45:56 +0200 Subject: [PATCH 01/12] General SML code cleanup. Further approximation to DocRef Generation. --- Isa_DOF.thy | 241 ++++++++++++++++++------------------ examples/simple/Example.thy | 23 ++-- 2 files changed, 134 insertions(+), 130 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 16f9435..15fbeac 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -154,137 +154,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 ? *) + 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 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,12 +285,12 @@ 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 *) *} @@ -312,13 +305,13 @@ 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 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 -- @@ -342,15 +335,6 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos),doc_attrs), 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) val markup = docclass_markup false cid id (Binding.pos_of bind_target); @@ -495,7 +479,7 @@ fun read_fields raw_fields ctxt = 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 = +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; @@ -505,8 +489,18 @@ fun add_record_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaul 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; + val cid = case raw_parent of + NONE => DOF_core.default_cid + | SOME X => X + val gen_antiquot = DocAttrParser.doc_class_ref_antiquotation +(* fun setup_antiquot thy = let val _ = Theory.setup (gen_antiquot binding cid) + in thy end + *) + fun setup_antiquot thy = let val _ = Theory.setup (gen_antiquot Binding.empty cid) + in thy end in thy |> Record.add_record overloaded (params', binding) parent fields |> DOF_core.define_doc_class_global (params', binding) parent fieldsNterms' + (* |> setup_antiquot *) end; @@ -518,18 +512,26 @@ val _ = -- 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))); *} 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; Binding.print; +Syntax.read_sort; +Syntax.read_typ; Syntax.read_term; Syntax.pretty_typ; -try; *} @@ -556,6 +558,7 @@ Context.Theory; Context_Position.report_generic; Context_Position.report; Term_Style.parse; +open Binding; \ end \ No newline at end of file diff --git a/examples/simple/Example.thy b/examples/simple/Example.thy index 5429760..35e8ff0 100644 --- a/examples/simple/Example.thy +++ b/examples/simple/Example.thy @@ -6,15 +6,18 @@ 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"} *} @@ -90,8 +93,6 @@ term "a + b = b + a" section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *) - - end \ No newline at end of file From 5bc9ddfd5201cf62d02f9158405800122e5e43b9 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 4 Apr 2018 14:44:21 +0200 Subject: [PATCH 02/12] Running Version for Antiquotqtion Generation - with a Big - direct sons lead to false errors --- Isa_DOF.thy | 142 +++++++++++++++++++---------------- examples/simple/Example.thy | 58 +++++++++++++- ontologies/CENELEC_50126.thy | 46 +----------- 3 files changed, 137 insertions(+), 109 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 15fbeac..b0a13f0 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -17,19 +17,10 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) 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 +38,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 *) @@ -100,7 +91,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 @@ -215,11 +206,11 @@ fun define_doc_class_global (params', binding) parent fields thy = name = binding, thy_name = nn, id = id, (* for pide --- really fresh or better reconstruct - from prior record definition ? *) + 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 *)} - val _ = () (* XXX *) in map_data_global(apsnd(Symtab.update(cid_long,info)))(thy) end @@ -295,11 +286,10 @@ 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.$$$ ";"); @@ -334,9 +324,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 {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; @@ -350,7 +339,7 @@ fun enriched_document_command markdown (((((oid,pos),cid_pos),doc_attrs), 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) @@ -398,7 +387,15 @@ val _ = (attributes >> (fn (((oid,pos),cid),doc_attrs) => (Toplevel.theory (DOF_core.declare_object_global oid)))); +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 = @@ -416,11 +413,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" @@ -430,36 +429,44 @@ 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 = "}" + val _ = writeln ("XXX" ^ cid_decl) + fun cid_decl' ctxt = let val thy = (Proof_Context.theory_of ctxt) + val str = (Binding.name_of name) + val name = DOF_core.name2doc_class_name thy str + val _ = writeln ("YYY" ^ name) + in str end 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' 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 = @@ -489,34 +496,48 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdef 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; - val cid = case raw_parent of - NONE => DOF_core.default_cid - | SOME X => X - val gen_antiquot = DocAttrParser.doc_class_ref_antiquotation -(* fun setup_antiquot thy = let val _ = Theory.setup (gen_antiquot binding cid) - in thy end - *) - fun setup_antiquot thy = let val _ = Theory.setup (gen_antiquot Binding.empty cid) - in thy end + val cid = case raw_parent of (* why the parent ? ? ? *) + NONE => DOF_core.default_cid + | SOME X => DOF_core.name2doc_class_name thy X + 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' - (* |> setup_antiquot *) + |> gen_antiquotation binding cid (* 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_doc_class_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{* (* Parsing combinators in Scan *) @@ -527,38 +548,27 @@ ML{* (* Parsing combinators in Scan *) 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; + *} - -(* 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; Term_Style.parse; -open Binding; \ end \ No newline at end of file diff --git a/examples/simple/Example.thy b/examples/simple/Example.thy index 35e8ff0..4a32d76 100644 --- a/examples/simple/Example.thy +++ b/examples/simple/Example.thy @@ -8,7 +8,8 @@ section{* Some show-off's of general antiquotations. *} (* some show-off of standard anti-quotations: *) print_attributes - print_antiquotations +print_antiquotations + text{* @{thm refl} of name @{thm [source] refl} @{thm[mode=Rule] conjI} @{file "../../Isa_DOF.thy"} @@ -20,6 +21,61 @@ text{* @{thm refl} of name @{thm [source] refl} @{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 *} diff --git a/ontologies/CENELEC_50126.thy b/ontologies/CENELEC_50126.thy index 4589962..a2a770b 100644 --- a/ontologies/CENELEC_50126.thy +++ b/ontologies/CENELEC_50126.thy @@ -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,9 +153,11 @@ 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}; - +"hallo"; +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"; +DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.test_requirement"; val ({maxano, tab},tab2) = DOF_core.get_data @{context}; Symtab.dest tab; From 4d09fc5e34ac6314df6a3c56bcf379b52e576dc3 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 4 Apr 2018 16:14:37 +0200 Subject: [PATCH 03/12] slight re-arrangement of the examples: the simple example becomes a cenelec example, and simple got an example called Article based on to the LNCS_onto. --- examples/{simple => cenelec}/Example.thy | 0 examples/simple/Article.thy | 73 ++++++++++++++++++++++++ 2 files changed, 73 insertions(+) rename examples/{simple => cenelec}/Example.thy (100%) create mode 100644 examples/simple/Article.thy diff --git a/examples/simple/Example.thy b/examples/cenelec/Example.thy similarity index 100% rename from examples/simple/Example.thy rename to examples/cenelec/Example.thy diff --git a/examples/simple/Article.thy b/examples/simple/Article.thy new file mode 100644 index 0000000..f8e6f68 --- /dev/null +++ b/examples/simple/Article.thy @@ -0,0 +1,73 @@ +theory Article + imports "../../ontologies/LNCS_onto" +begin + +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\} ... *} + +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 *} + +subsection*[cenelec_onto::example]{* CENELEC *} + +section*[con::conclusion]{* Future Work: Monitoring Classes *} +text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... + +The control of monitors is done by the commands: +\ open_monitor +\ close_monitor +where the automaton of the monitor class is expected +to be in a final state. + +Monitors can be nested, so it is possible to "overlay" one or more monitoring +classes and imposing different sets of structural constraints in a + +Classes neither directly or via inheritance indirectly +mentioned in the monitor are @{bold \nested\} +from a monitor and may occur freely. +*} + +subsection*[related::related_work]{* Related Work *} +text{* +\ 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 *} + + +end + From 229997d60ae34bb17570cbc97b80eed97ca69126 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 4 Apr 2018 16:25:33 +0200 Subject: [PATCH 04/12] Added open/close monitor syntax. --- Isa_DOF.thy | 12 +++++++++++- examples/simple/Article.thy | 27 ++++++++------------------- 2 files changed, 19 insertions(+), 20 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index b0a13f0..b73493b 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -11,7 +11,8 @@ 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"::thy_decl and "doc_class" :: thy_decl @@ -387,6 +388,15 @@ val _ = (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 *) + end (* struct *) *} diff --git a/examples/simple/Article.thy b/examples/simple/Article.thy index f8e6f68..e81fd88 100644 --- a/examples/simple/Article.thy +++ b/examples/simple/Article.thy @@ -1,6 +1,8 @@ theory Article imports "../../ontologies/LNCS_onto" begin + +open_monitor[onto::article] text*[tit::title]{* Using The Isabelle Ontology Framework*} @@ -36,28 +38,12 @@ subsection*[scholar_onto::example]{* A Scholar Paper: Eating one's own dogfood. subsection*[mathex_onto::example]{* Math-Exercise *} -subsection*[cenelec_onto::example]{* CENELEC *} - section*[con::conclusion]{* Future Work: Monitoring Classes *} -text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... - -The control of monitors is done by the commands: -\ open_monitor -\ close_monitor -where the automaton of the monitor class is expected -to be in a final state. - -Monitors can be nested, so it is possible to "overlay" one or more monitoring -classes and imposing different sets of structural constraints in a - -Classes neither directly or via inheritance indirectly -mentioned in the monitor are @{bold \nested\} -from a monitor and may occur freely. -*} +text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *} subsection*[related::related_work]{* Related Work *} text{* -\ XML and dtd's, +\ @{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"} @@ -66,8 +52,11 @@ text{* \ AADL Alisa, \ RATP Ovado *} + subsection{* Discussion *} - +text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *} + +close_monitor[onto] end From 027361fb03c2384f17bde2682cb39d8192b92e18 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 4 Apr 2018 17:04:19 +0200 Subject: [PATCH 05/12] unified syntax: renamed declare_reference open_monitor close_monitor into declare_reference* open_monitor* close_monitor* in order to simplify the task for Achim. --- Isa_DOF.thy | 8 ++++---- examples/simple/Article.thy | 24 +++++++++++++----------- ontologies/CENELEC_50126.thy | 2 +- 3 files changed, 18 insertions(+), 16 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index b73493b..8c859c2 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -12,7 +12,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) imports Main (* Isa_MOF *) keywords "section*" "subsection*" "subsubsection*" "paragraph*" "subparagraph*" "text*" - "open_monitor" "close_monitor" "declare_reference"::thy_decl + "open_monitor*" "close_monitor*" "declare_reference*"::thy_decl and "doc_class" :: thy_decl @@ -384,17 +384,17 @@ val _ = >> enriched_document_command {markdown = false}); val _ = - Outer_Syntax.command @{command_keyword "declare_reference"} "declare document reference" + 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" + 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" + 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 *) end (* struct *) diff --git a/examples/simple/Article.thy b/examples/simple/Article.thy index e81fd88..fa6feff 100644 --- a/examples/simple/Article.thy +++ b/examples/simple/Article.thy @@ -1,9 +1,11 @@ +(* << *) theory Article imports "../../ontologies/LNCS_onto" begin - -open_monitor[onto::article] +(* >> *) +open_monitor*[onto::article] + text*[tit::title]{* Using The Isabelle Ontology Framework*} text*[stit::subtitle] \Linking the Formal with the Informal\ @@ -12,14 +14,12 @@ 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 +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. - *} +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, @@ -56,7 +56,9 @@ text{* subsection{* Discussion *} text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *} -close_monitor[onto] - +close_monitor*[onto] + +(* << *) end +(* >> *) diff --git a/ontologies/CENELEC_50126.thy b/ontologies/CENELEC_50126.thy index a2a770b..62ea09a 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 From 5e48dcffdfe603496bff5818371e1aee1cfc64a3 Mon Sep 17 00:00:00 2001 From: bu Date: Wed, 4 Apr 2018 18:08:18 +0200 Subject: [PATCH 06/12] Ontology checking bug for unrelated direct sub_classes fixed. Enfin ! --- Isa_DOF.thy | 20 +++------- examples/cenelec/Example.thy | 75 ++++++++---------------------------- ontologies/CENELEC_50126.thy | 10 ++--- 3 files changed, 28 insertions(+), 77 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 8c859c2..641c696 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -63,11 +63,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' @@ -446,19 +446,12 @@ fun doc_class_ref_antiquotation name cid_decl = let fun open_par x = if x then "\\label{" else "\\autoref{" val close = "}" - val _ = writeln ("XXX" ^ cid_decl) - fun cid_decl' ctxt = let val thy = (Proof_Context.theory_of ctxt) - val str = (Binding.name_of name) - val name = DOF_core.name2doc_class_name thy str - val _ = writeln ("YYY" ^ name) - in str end in Thy_Output.antiquotation name (Scan.lift (doc_ref_modes -- Args.cartouche_input)) (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' ctxt) *) cid_decl ({strict_checking = not x}) (Input.pos_of source) #> @@ -506,15 +499,14 @@ fun add_doc_class_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdef 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; - val cid = case raw_parent of (* why the parent ? ? ? *) - NONE => DOF_core.default_cid - | SOME X => DOF_core.name2doc_class_name thy X + + 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' - |> gen_antiquotation binding cid (* defines the ontology-checked - text antiquotation to this document class *) + |> (fn thy => gen_antiquotation binding (cid thy) thy) + (* defines the ontology-checked text antiquotation to this document class *) end; diff --git a/examples/cenelec/Example.thy b/examples/cenelec/Example.thy index 4a32d76..d70fbff 100644 --- a/examples/cenelec/Example.thy +++ b/examples/cenelec/Example.thy @@ -1,6 +1,5 @@ theory Example imports "../../ontologies/CENELEC_50126" - keywords "Term" :: diag begin section{* Some show-off's of general antiquotations. *} @@ -19,10 +18,11 @@ text{* @{thm refl} of name @{thm [source] refl} @{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 *} @@ -38,52 +38,38 @@ to a test-environment or test-engine *} text \ As established by @{docref (unchecked) \t10\}, - @{docref (define) \t10\} - the @{docref \t10\} + @{docref (define) \t10\} \ +text \ the @{docref \t10\} the @{docref \ass122\} \ -text \ safety related applicability condition @{srac \ass122\}. - exported constraint @{ec \ass122\}. +text \ safety related applicability condition @{srac \ass122\}. \ +text \ exported constraint @{ec \ass122\}. \ -text{* - And some ontologically inconsistent reference: - @{hypothesis \ass1\} as well as - -*} --- "very wrong" +text{* And some ontologically inconsistent reference: @{hypothesis \ass1\} as well as *} +-- wrong -text{* - And some ontologically inconsistent reference: - @{assumption \hyp1\} as well as - -*} --- "very wrong" +text{* ... some more ontologically inconsistent reference: @{assumption \hyp1\} as well as *} +-- wrong -text{* - And some ontologically inconsistent reference: - @{test_result \ass122\} as well as - -*} +text{* And a further ontologically totally inconsistent reference: + @{test_result \ass122\} as well as ... *} -- wrong -text{* - And some other ontologically inconsistent reference: - @{ec \t10\} as well as -*} +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::requirement, alpha="main", beta=42] -declare_reference [lalala::quod] (* shouldn't work *) +declare_reference* [lalala::quod] (* shouldn't work *) -declare_reference [blablabla::cid, alpha="beta sdf", beta=gamma, delta=dfg_fgh\<^sub>1] +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 \ @@ -117,34 +103,7 @@ text{* Here is a reference to @{docref \sedf\} *} Try to hover over the sedf - link and activate it !!! *) - - - - - - - - - - - -section{* A Small Example for a Command Definition --- just to see how this works in principle. *} - -ML{* -val opt_modes = - Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []; - -val _ = - Outer_Syntax.command @{command_keyword Term} "read and print term" - (opt_modes -- Parse.term >> Isar_Cmd.print_term); - -*} - -lemma "True" by simp - -Term "a + b = b + a" - -term "a + b = b + a" +section{* Miscellaneous ...*} section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *) diff --git a/ontologies/CENELEC_50126.thy b/ontologies/CENELEC_50126.thy index 62ea09a..4e44015 100644 --- a/ontologies/CENELEC_50126.thy +++ b/ontologies/CENELEC_50126.thy @@ -153,15 +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}; -"hallo"; +"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"; DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.test_requirement"; - -val ({maxano, tab},tab2) = DOF_core.get_data @{context}; -Symtab.dest tab; -Symtab.dest tab2; +"XXXXXXXXXXXXXXXXX"; +val ({maxano, tab=ref_tab},class_tab) = DOF_core.get_data @{context}; +Symtab.dest ref_tab; +Symtab.dest class_tab; *} From f8692dd801c5d0eaa94f48acbfaeb4f466e81705 Mon Sep 17 00:00:00 2001 From: bu Date: Thu, 5 Apr 2018 12:09:58 +0200 Subject: [PATCH 07/12] =?UTF-8?q?Renamed=20LNCS=5Fonto=20into=20=E2=80=9Cs?= =?UTF-8?q?cholarly=5Fpaper=E2=80=9D.=20Decided=20for=20the=20trace=20vari?= =?UTF-8?q?ant=20semantics=20of=20monitors.=20(more=20power,=20easier=20to?= =?UTF-8?q?=20implement)?= 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)" From 46e1be6411361a760c8616beb2e45992ccad6b51 Mon Sep 17 00:00:00 2001 From: bu Date: Thu, 5 Apr 2018 12:44:52 +0200 Subject: [PATCH 08/12] =?UTF-8?q?Added=20syntax=20for=20update=5Finstance*?= =?UTF-8?q?=E2=80=A6=20+=3D=20variant=20does=20not=20yet=20work.?= MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit --- Isa_DOF.thy | 50 ++++++++++++++++++++++++++++--------- examples/simple/Article.thy | 6 +++-- 2 files changed, 42 insertions(+), 14 deletions(-) diff --git a/Isa_DOF.thy b/Isa_DOF.thy index 9b71fae..efdf90b 100644 --- a/Isa_DOF.thy +++ b/Isa_DOF.thy @@ -12,7 +12,8 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *) imports Main (* Isa_MOF *) keywords "section*" "subsection*" "subsubsection*" "paragraph*" "subparagraph*" "text*" - "open_monitor*" "close_monitor*" "declare_reference*"::thy_decl + "open_monitor*" "close_monitor*" "declare_reference*" + "update_instance*" ::thy_decl and "doc_class" :: thy_decl @@ -299,15 +300,30 @@ val attribute = 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)); -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), @@ -384,18 +400,28 @@ 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)))); + 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 *) + 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 *) diff --git a/examples/simple/Article.thy b/examples/simple/Article.thy index fa6feff..faa5344 100644 --- a/examples/simple/Article.thy +++ b/examples/simple/Article.thy @@ -1,6 +1,6 @@ (* << *) theory Article - imports "../../ontologies/LNCS_onto" + imports "../../ontologies/scholarly_paper" begin (* >> *) @@ -30,7 +30,9 @@ 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,*} From 376c3fdd3b10a548128ec58448916e84af1d5010 Mon Sep 17 00:00:00 2001 From: Idir AIT SADOUNE Date: Fri, 6 Apr 2018 14:13:17 +0200 Subject: [PATCH 09/12] no message --- MOF.sml | 71 +++++++++++++ examples/simple/Example.thy | 154 +++++++++++++++++++++++++++++ examples/simple/IdirExample.thy | 9 ++ ontologies/ScientificPaperOnto.thy | 26 +++++ 4 files changed, 260 insertions(+) create mode 100644 MOF.sml create mode 100644 examples/simple/Example.thy create mode 100644 examples/simple/IdirExample.thy create mode 100644 ontologies/ScientificPaperOnto.thy diff --git a/MOF.sml b/MOF.sml new file mode 100644 index 0000000..61b787d --- /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/simple/Example.thy b/examples/simple/Example.thy new file mode 100644 index 0000000..4a32d76 --- /dev/null +++ b/examples/simple/Example.thy @@ -0,0 +1,154 @@ +theory Example + imports "../../ontologies/CENELEC_50126" + keywords "Term" :: diag +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*[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 *} + +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{* A Small Example for a Command Definition --- just to see how this works in principle. *} + +ML{* +val opt_modes = + Scan.optional (@{keyword "("} |-- Parse.!!! (Scan.repeat1 Parse.name --| @{keyword ")"})) []; + +val _ = + Outer_Syntax.command @{command_keyword Term} "read and print term" + (opt_modes -- Parse.term >> Isar_Cmd.print_term); + +*} + +lemma "True" by simp + +Term "a + b = b + a" + +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/examples/simple/IdirExample.thy b/examples/simple/IdirExample.thy new file mode 100644 index 0000000..270dbbd --- /dev/null +++ b/examples/simple/IdirExample.thy @@ -0,0 +1,9 @@ +theory IdirExample + imports "../../ontologies/ScientificPaperOnto" + +begin + +text*[p1::Paragraph] {* ceci est un paragraphe *} +text*[abs::Abstract, content = p1]{* *} + +end \ No newline at end of file diff --git a/ontologies/ScientificPaperOnto.thy b/ontologies/ScientificPaperOnto.thy new file mode 100644 index 0000000..6f80612 --- /dev/null +++ b/ontologies/ScientificPaperOnto.thy @@ -0,0 +1,26 @@ +theory ScientificPaperOnto + imports "../Isa_DOF" + +begin + +doc_class Paragraph = + content :: "string list" + +doc_class Abstract = + content :: Paragraph + +doc_class SubSection = + id :: integer + content :: "Paragraph list" + +doc_class Section = + id :: integer + content :: "Paragraph list" + itsSubSection :: "SubSection list" + +doc_class Article = + content :: "(Abstract + Section) list" + where + "(Abstract. + Section*)" +end \ No newline at end of file From c3a411183340c2f7108b694506ad87a3b017ec2e Mon Sep 17 00:00:00 2001 From: Idir AIT SADOUNE Date: Fri, 6 Apr 2018 14:25:21 +0200 Subject: [PATCH 10/12] no message --- examples/simple/IdirExample.thy | 9 --------- ontologies/ScientificPaperOnto.thy | 26 -------------------------- ontologies/mathex_onto.thy | 6 ++++++ 3 files changed, 6 insertions(+), 35 deletions(-) delete mode 100644 examples/simple/IdirExample.thy delete mode 100644 ontologies/ScientificPaperOnto.thy create mode 100644 ontologies/mathex_onto.thy diff --git a/examples/simple/IdirExample.thy b/examples/simple/IdirExample.thy deleted file mode 100644 index 270dbbd..0000000 --- a/examples/simple/IdirExample.thy +++ /dev/null @@ -1,9 +0,0 @@ -theory IdirExample - imports "../../ontologies/ScientificPaperOnto" - -begin - -text*[p1::Paragraph] {* ceci est un paragraphe *} -text*[abs::Abstract, content = p1]{* *} - -end \ No newline at end of file diff --git a/ontologies/ScientificPaperOnto.thy b/ontologies/ScientificPaperOnto.thy deleted file mode 100644 index 6f80612..0000000 --- a/ontologies/ScientificPaperOnto.thy +++ /dev/null @@ -1,26 +0,0 @@ -theory ScientificPaperOnto - imports "../Isa_DOF" - -begin - -doc_class Paragraph = - content :: "string list" - -doc_class Abstract = - content :: Paragraph - -doc_class SubSection = - id :: integer - content :: "Paragraph list" - -doc_class Section = - id :: integer - content :: "Paragraph list" - itsSubSection :: "SubSection list" - -doc_class Article = - content :: "(Abstract + Section) list" - where - "(Abstract. - Section*)" -end \ No newline at end of file diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy new file mode 100644 index 0000000..39b238b --- /dev/null +++ b/ontologies/mathex_onto.thy @@ -0,0 +1,6 @@ +theory mathex_onto + +imports "../Isa_DOF" +begin + +end \ No newline at end of file From 9ee8811576445060c1491c23b177060c3dfdb0cc Mon Sep 17 00:00:00 2001 From: Idir AIT SADOUNE Date: Fri, 6 Apr 2018 14:32:22 +0200 Subject: [PATCH 11/12] no message --- ontologies/mathex_onto.thy | 11 +++++++++++ 1 file changed, 11 insertions(+) diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index 39b238b..062866d 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -3,4 +3,15 @@ theory mathex_onto imports "../Isa_DOF" begin +doc_class Question = + content :: "string list" + +doc_class Response = + content :: "string list" + +doc_class Exercise = + question :: Question + response :: Response + + end \ No newline at end of file From 5feca3e0e1b7345cb0c5daf7680a49c5dd2a1e59 Mon Sep 17 00:00:00 2001 From: Idir AIT SADOUNE Date: Fri, 6 Apr 2018 14:48:43 +0200 Subject: [PATCH 12/12] no message --- ontologies/mathex_onto.thy | 8 +++++--- 1 file changed, 5 insertions(+), 3 deletions(-) diff --git a/ontologies/mathex_onto.thy b/ontologies/mathex_onto.thy index 062866d..7060964 100644 --- a/ontologies/mathex_onto.thy +++ b/ontologies/mathex_onto.thy @@ -4,14 +4,16 @@ imports "../Isa_DOF" begin doc_class Question = - content :: "string list" + content :: "(string + term) list" doc_class Response = - content :: "string list" + content :: "(string + term) list" -doc_class Exercise = +doc_class Exercise_part = question :: Question response :: Response +doc_class Exercise= + content :: "(Exercise_part) list" end \ No newline at end of file