pierre.derathe
/
Isabelle_DOF
Archived
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF

This commit is contained in:
Achim D. Brucker 2018-04-07 21:29:35 +01:00
parent ebd844f212 5feca3e0e1
commit e4f5f9bf68
8 changed files with 604 additions and 293 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

437
Isa_DOF.thy
View File

@ -11,25 +11,18 @@ that provide direct support in the PIDE framework. *}
theory Isa_DOF (* Isabelle Document Ontology Framework *) theory Isa_DOF (* Isabelle Document Ontology Framework *)
imports Main (* Isa_MOF *) imports Main (* Isa_MOF *)
keywords "section*" "subsection*" "subsubsection*" 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 and
"doc_class" :: thy_decl "doc_class" :: thy_decl
begin begin
text{* section{*Primitive Markup Generators*}
@{thm [names_long] refl}
*}
section{* A HomeGrown Document Type Management (the ''Model'') *}
ML{* ML{*
curry;
op |>;
op #>;
op |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c;
op ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b;
val docrefN = "docref"; val docrefN = "docref";
val docclassN = "doc_class"; val docclassN = "doc_class";
@ -47,9 +40,9 @@ val docclass_markup = docref_markup_gen docclassN
*} *}
section{* A HomeGrown Document Type Management (the ''Model'') *}
ML{* ML{*
structure DOF_core = structure DOF_core =
struct struct
type docclass_struct = {params : (string * sort) list, (*currently not used *) type docclass_struct = {params : (string * sort) list, (*currently not used *)
@ -71,11 +64,11 @@ struct
fun is_subclass0 (tab:docclass_tab) s t = fun is_subclass0 (tab:docclass_tab) s t =
let val _ = case Symtab.lookup tab t of let val _ = case Symtab.lookup tab t of
NONE => if t <> default_cid NONE => if t <> default_cid
then error "document superclass not defined" then error ("document superclass not defined: "^t)
else default_cid else default_cid
| SOME _ => "" | SOME _ => ""
fun father_is_sub s = case Symtab.lookup tab s of 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=NONE, ...}) => s = t
| SOME ({inherits_from=SOME (_,s'), ...}) => | SOME ({inherits_from=SOME (_,s'), ...}) =>
s' = t orelse father_is_sub 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')} in {tab=Symtab.merge X (otab,otab'),maxano=Int.max(m,m')}
end) end)
(* registrating data of the Isa_DOF component *)
structure Data = Generic_Data structure Data = Generic_Data
( (
type T = docobj_tab * docclass_tab 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 end
fun is_declared_oid_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy) fun is_declared_oid_global oid thy = let val {tab,...} = fst(get_data_global thy)
in Symtab.defined t oid end in Symtab.defined tab oid end
fun is_declared_oid_local oid thy = let val {tab=t,maxano=_} = fst(get_data thy) fun is_declared_oid_local oid thy = let val {tab,...} = fst(get_data thy)
in Symtab.defined t oid end in Symtab.defined tab oid end
fun is_defined_oid_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy) fun is_defined_oid_global oid thy = let val {tab,...} = fst(get_data_global thy)
in case Symtab.lookup t oid of in case Symtab.lookup tab oid of
NONE => false NONE => false
|SOME(NONE) => false |SOME(NONE) => false
|SOME _ => true |SOME _ => true
end end
fun is_defined_oid_local oid thy = let val {tab=t,maxano=_} = fst(get_data thy) fun is_defined_oid_local oid thy = let val {tab,...} = fst(get_data thy)
in case Symtab.lookup t oid of in case Symtab.lookup tab oid of
NONE => false NONE => false
|SOME(NONE) => false |SOME(NONE) => false
|SOME _ => true |SOME _ => true
end end
fun declare_object_global oid thy = (map_data_global fun declare_object_global oid thy =
(apfst(fn {tab=t,maxano=x} => let fun decl {tab=t,maxano=x} = {tab=Symtab.update_new(oid,NONE)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_local oid ctxt = (map_data (apfst(fn {tab=t,maxano=x} => in (map_data_global (apfst(decl)) (thy)
{tab=Symtab.update_new(oid,NONE) t, handle Symtab.DUP _ => error("multiple declaration of document reference"))
maxano=x})) end
(ctxt)
handle Symtab.DUP _ => fun declare_object_local oid ctxt =
error("multiple declaration of document reference")) 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 = 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 let val nn = Context.theory_name thy (* in case that we need the thy-name to identify
the space where it is ... *) the space where it is ... *)
val cid = (Binding.name_of binding) val cid = (Binding.name_of binding)
val pos = (Binding.pos_of binding) val pos = (Binding.pos_of binding)
val _ = if is_defined_cid_global cid thy val _ = if is_defined_cid_global cid thy
then error("redefinition of document class") then error("redefinition of document class")
else () else ()
val _ = case parent of (* the doc_class may be root, but must refer val _ = case parent of (* the doc_class may be root, but must refer
to another doc_class and not just an to another doc_class and not just an
arbitrary type *) arbitrary type *)
NONE => () NONE => ()
| SOME(_,cid_parent) => | SOME(_,cid_parent) =>
if not (is_defined_cid_global cid_parent thy) if not (is_defined_cid_global cid_parent thy)
then error("document class undefined : " ^ cid_parent) then error("document class undefined : " ^ cid_parent)
else () else ()
val cid_long = name2doc_class_name thy cid val cid_long = name2doc_class_name thy cid
val id = serial (); val id = serial ();
val _ = Position.report pos (docclass_markup true cid id pos); val _ = Position.report pos (docclass_markup true cid id pos);
val info = {params=params', val info = {params=params',
name = binding, name = binding,
thy_name = nn, thy_name = nn,
id = id, (* for pide --- really fresh or better reconstruct id = id, (* for pide --- really fresh or better reconstruct
from prior record definition ? *) from prior record definition ? For the moment: own
inherits_from = parent, generation of serials ... *)
attribute_decl = fields (* currently unchecked *) inherits_from = parent,
(*, rex : term list -- not yet used *)} attribute_decl = fields (* currently unchecked *)
val _ = () (* XXX *) (*, rex : term list -- not yet used *)}
in map_data_global(apsnd(Symtab.update(cid_long,info)))(thy) in map_data_global(apsnd(Symtab.update(cid_long,info)))(thy)
end end
fun define_object_global (oid, bbb) thy = fun define_object_global (oid, bbb) thy =
let val nn = Context.theory_name thy (* in case that we need the thy-name to identify let val nn = Context.theory_name thy (* in case that we need the thy-name to identify
the space where it is ... *) the space where it is ... *)
in if is_defined_oid_global oid thy in if is_defined_oid_global oid thy
then error("multiple definition of document reference") then error("multiple definition of document reference")
else map_data_global (apfst(fn {tab=t,maxano=x} => else map_data_global (apfst(fn {tab=t,maxano=x} =>
{tab=Symtab.update(oid,SOME bbb) t, {tab=Symtab.update(oid,SOME bbb) t,
maxano=x})) maxano=x}))
(thy) (thy)
end end
fun define_object_local (oid, bbb) ctxt = fun define_object_local (oid, bbb) ctxt =
map_data (apfst(fn {tab=t,maxano=x} => map_data (apfst(fn{tab,maxano}=>{tab=Symtab.update(oid,SOME bbb)tab,maxano=maxano})) ctxt
{tab=Symtab.update(oid,SOME bbb) t,maxano=x})) ctxt
(* declares an anonyme label of a given type and generates a unique reference ... *) (* declares an anonyme label of a given type and generates a unique reference ... *)
fun declare_anoobject_global thy cid = map_data_global fun declare_anoobject_global thy cid =
(apfst(fn {tab=t,maxano=x} => let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1)
let val str = cid^":"^Int.toString(x+1) val _ = writeln("Anonymous doc-ref declared: " ^ str)
val _ = writeln("Anonymous doc-ref declared: " in {tab=Symtab.update(str,NONE)tab,maxano= maxano+1} end
^str) in map_data_global (apfst declare) (thy)
in {tab=Symtab.update(str,NONE)t,maxano=x+1} end
end))
(thy)
fun declare_anoobject_local ctxt cid = map_data fun declare_anoobject_local ctxt cid =
(apfst(fn {tab=t,maxano=x} => let fun declare {tab,maxano} = let val str = cid^":"^Int.toString(maxano+1)
let val str = cid^":"^Int.toString(x+1) val _ = writeln("Anonymous doc-ref declared: " ^str)
val _ = writeln("Anonymous doc-ref declared: " in {tab=Symtab.update(str,NONE)tab, maxano=maxano+1} end
^str) in map_data (apfst declare) (ctxt)
in {tab=Symtab.update(str,NONE)t, maxano=x+1} end
end))
(ctxt)
fun get_object_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy) fun get_object_global oid thy = let val {tab,...} = fst(get_data_global thy)
in case Symtab.lookup t oid of in case Symtab.lookup tab oid of
NONE => error"undefined reference" NONE => error"undefined reference"
|SOME(bbb) => bbb |SOME(bbb) => bbb
end end
fun get_object_local oid ctxt = let val {tab=t,maxano=_} = fst(get_data ctxt) fun get_object_local oid ctxt = let val {tab,...} = fst(get_data ctxt)
in case Symtab.lookup t oid of in case Symtab.lookup tab oid of
NONE => error"undefined reference" NONE => error"undefined reference"
|SOME(bbb) => bbb |SOME(bbb) => bbb
end end
fun get_doc_class_global cid thy = fun get_doc_class_global cid thy =
if cid = default_cid then error("default doc class acces") (* TODO *) if cid = default_cid then error("default doc class acces") (* TODO *)
else let val t = snd(get_data_global thy) else let val t = snd(get_data_global thy)
in (Symtab.lookup t cid) end in (Symtab.lookup t cid) end
fun get_doc_class_local cid ctxt = fun get_doc_class_local cid ctxt =
if cid = default_cid then error("default doc class acces") (* TODO *) if cid = default_cid then error("default doc class acces") (* TODO *)
else let val t = snd(get_data ctxt) else let val t = snd(get_data ctxt)
in (Symtab.lookup t cid) end in (Symtab.lookup t cid) end
fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt) fun is_defined_cid_local cid ctxt = let val t = 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) Symtab.defined t (name2doc_class_name_local ctxt cid)
end end
fun writeln_classrefs ctxt = let val t = snd(get_data ctxt) fun writeln_classrefs ctxt = let val tab = snd(get_data ctxt)
in writeln (String.concatWith "," (Symtab.keys t)) end in writeln (String.concatWith "," (Symtab.keys tab)) end
fun writeln_docrefs ctxt = let val {tab=t,maxano=_} = fst(get_data ctxt) fun writeln_docrefs ctxt = let val {tab,...} = fst(get_data ctxt)
in writeln (String.concatWith "," (Symtab.keys t)) end in writeln (String.concatWith "," (Symtab.keys tab)) end
end (* struct *) end (* struct *)
*} *}
section{* Syntax for Annotated Documentation Commands (the '' View'') *} section{* Syntax for Annotated Documentation Commands (the '' View'' Part I) *}
ML{* ML{*
structure DocAttrParser = structure AnnoTextelemParser =
struct struct
val semi = Scan.option (Parse.$$$ ";"); val semi = Scan.option (Parse.$$$ ";");
val attribute = val attribute =
Parse.position Parse.name Parse.position Parse.name
-- Scan.optional (Parse.$$$ "=" |-- Parse.!!! 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 = val reference =
Parse.position Parse.name Parse.position Parse.name
-- Scan.option (Parse.$$$ "::" |-- Parse.!!! (Parse.position Parse.name)); -- Scan.option (Parse.$$$ "::" |-- Parse.!!! (Parse.position Parse.name));
val attributes = (Parse.$$$ "[" |-- (reference -- val attributes =
(Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) [])) (Parse.$$$ "["
--| 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), 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") then error("document class undefined")
else () else ()
val cid_long = DOF_core.name2doc_class_name thy cid 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,...} = 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 markup = docclass_markup false cid id (Binding.pos_of bind_target);
val ctxt = Context.Theory thy val ctxt = Context.Theory thy
val _ = Context_Position.report_generic ctxt pos' markup; val _ = Context_Position.report_generic ctxt pos' markup;
@ -366,7 +356,7 @@ Context_Position.report_generic;
let val name = Context.theory_name thy let val name = Context.theory_name thy
in DOF_core.define_object_global in DOF_core.define_object_global
(oid, {pos=pos, thy_name=name, (oid, {pos=pos, thy_name=name,
id=id , cid=DOF_core.default_cid}) id=id, cid=DOF_core.default_cid})
(thy) (thy)
end end
fun MMM(SOME(s,p)) = SOME(s^"XXX",p) fun MMM(SOME(s,p)) = SOME(s^"XXX",p)
@ -410,11 +400,38 @@ val _ =
>> enriched_document_command {markdown = false}); >> enriched_document_command {markdown = false});
val _ = val _ =
Outer_Syntax.command @{command_keyword "declare_reference"} "declare document reference" Outer_Syntax.command @{command_keyword "declare_reference*"}
(attributes >> (fn (((oid,pos),cid),doc_attrs) => "declare document reference"
(Toplevel.theory (DOF_core.declare_object_global oid)))); (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 = 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 () else ()
in name end in name end
else if DOF_core.is_declared_oid_global name thy 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 (); name)
else error("undefined document reference:"^name) else error("undefined document reference:"^name)
end end
(* generic syntax for doc_class links. *) (* generic syntax for doc_class links. *)
val defineN = "define" val defineN = "define"
@ -446,36 +465,37 @@ val doc_ref_modes = Scan.optional (Args.parens (Args.$$$ defineN || Args.$$$ unc
>> (fn str => if str = defineN >> (fn str => if str = defineN
then {unchecked = false, define= true} then {unchecked = false, define= true}
else {unchecked = true, define= false})) else {unchecked = true, define= false}))
{unchecked = false, define= false}; {unchecked = false, define= false} (* default *);
fun doc_class_ref_antiquotation name cid_decl = fun doc_class_ref_antiquotation name cid_decl =
let fun open_par x = if x then (writeln "ctr_anti true"; "\\label{" ) let fun open_par x = if x then "\\label{"
else (writeln "ctr_anti false"; "\\autoref{" ) else "\\autoref{"
val close = "}" val close = "}"
in in
(* Thy_Output.antiquotation name (Scan.lift (args_alt -- Args.cartouche_input)) *)
Thy_Output.antiquotation name (Scan.lift (doc_ref_modes -- 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) => fn ({unchecked = x, define= y}, source:Input.source) =>
(Thy_Output.output_text state {markdown=false} #> (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) enclose (open_par y) close)
source) source)
end end
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*) (* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
val _ = Theory.setup val _ = Theory.setup (doc_class_ref_antiquotation @{binding docref} DOF_core.default_cid)
((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 ))
*) )
end (* struct *) end (* struct *)
*} *}
section{* Syntax for Ontologies (the '' View'' Part III) *}
ML{* ML{*
structure OntoParser =
struct
fun read_parent NONE ctxt = (NONE, ctxt) fun read_parent NONE ctxt = (NONE, ctxt)
| read_parent (SOME raw_T) ctxt = | read_parent (SOME raw_T) ctxt =
@ -488,70 +508,91 @@ fun map_option _ NONE = NONE
|map_option f (SOME x) = SOME (f x) |map_option f (SOME x) = SOME (f x)
fun read_fields raw_fields ctxt = fun read_fields raw_fields ctxt =
let let
val Ts = Syntax.read_typs ctxt (map (fn ((_, raw_T, _),_) => raw_T) raw_fields); 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 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 fields = map2 (fn ((x, _, mx),_) => fn T => (x, T, mx)) raw_fields Ts;
val ctxt' = fold Variable.declare_typ Ts ctxt; val ctxt' = fold Variable.declare_typ Ts ctxt;
in (fields, terms, ctxt') end; 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 let
val ctxt = Proof_Context.init_global thy; val ctxt = Proof_Context.init_global thy;
val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params; val params = map (apsnd (Typedecl.read_constraint ctxt)) raw_params;
val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt; val ctxt1 = fold (Variable.declare_typ o TFree) params ctxt;
val (parent, ctxt2) = read_parent raw_parent ctxt1; val (parent, ctxt2) = read_parent raw_parent ctxt1;
val (fields, terms, ctxt3) = read_fields raw_fieldsNdefaults ctxt2; val (fields, terms, ctxt3) = read_fields raw_fieldsNdefaults ctxt2;
val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ terms val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ terms
val fieldsNterms' = map (fn ((x,y),z) => (x,y,z)) fieldsNterms val fieldsNterms' = map (fn ((x,y),z) => (x,y,z)) fieldsNterms
val params' = map (Proof_Context.check_tfree ctxt3) params; 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' fun cid thy = DOF_core.name2doc_class_name thy (Binding.name_of binding)
end; 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 _ = val _ =
Outer_Syntax.command @{command_keyword doc_class} "define document class" Outer_Syntax.command @{command_keyword doc_class} "define document class"
(Parse_Spec.overloaded ((Parse_Spec.overloaded
-- (Parse.type_args_constrained -- Parse.binding) -- (Parse.type_args_constrained -- Parse.binding)
-- (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"}) -- (@{keyword "="}
-- Scan.repeat1 (Parse.const_binding -- Scan.option (@{keyword "<="} |-- Parse.term))) |-- Scan.option (Parse.typ --| @{keyword "+"})
-- Scan.repeat (@{keyword "where"} |-- Parse.term) -- Scan.repeat1
(Parse.const_binding -- Scan.option (@{keyword "<="} |-- Parse.term)))
-- Scan.repeat (@{keyword "where"} |-- Parse.term))
>> (fn (((overloaded, x), (y, z)),rex) => >> (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 *} 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; Binding.print;
Syntax.read_sort;
Syntax.read_typ;
Syntax.read_term; Syntax.read_term;
Syntax.pretty_typ; Syntax.pretty_typ;
try;
*} *}
(* Look at this thingi ... *)
ML \<open>
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));
\<close>
text{* @{theory "Nat"} @{thm refl}*}
ML\<open> ML\<open>
open Markup; open Markup;
Markup.binding; Markup.binding;
open Position; open Position;
open Binding;
Position.line; Position.line;
Context.Theory; Context.Theory;
Context_Position.report_generic; Context_Position.report_generic;
Context_Position.report; Context_Position.report;

71
MOF.sml Normal file
View File

@ -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*)

113
examples/cenelec/Example.thy Normal file
View File

@ -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 \<open> As established by @{docref (unchecked) \<open>t10\<close>},
@{docref (define) \<open>t10\<close>} \<close>
text \<open> the @{docref \<open>t10\<close>}
the @{docref \<open>ass122\<close>}
\<close>
text \<open> safety related applicability condition @{srac \<open>ass122\<close>}. \<close>
text \<open> exported constraint @{ec \<open>ass122\<close>}.
\<close>
text{* And some ontologically inconsistent reference: @{hypothesis \<open>ass1\<close>} as well as *}
-- wrong
text{* ... some more ontologically inconsistent reference: @{assumption \<open>hyp1\<close>} as well as *}
-- wrong
text{* And a further ontologically totally inconsistent reference:
@{test_result \<open>ass122\<close>} as well as ... *}
-- wrong
text{* the ontologically inconsistent reference: @{ec \<open>t10\<close>} *}
-- 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] \<open> just a paragraph - lexical variant \<close>
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\<open>\label{sedf}\<close> (* 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 \<open>lalala\<close>} -- produces warning. *}
text{* @{docref (unchecked) \<open>lalala\<close>} -- produces no warning. *}
text{* @{docref \<open>ass122\<close>} -- global reference to a text-item in another file. *}
text{* @{ec \<open>ass122\<close>} -- 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 \<open>ass122\<close>} -- wrong: "reference ontologically inconsistent". *}
text{* Here is a reference to @{docref \<open>sedf\<close>} *}
(* 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

66
examples/simple/Article.thy Normal file
View File

@ -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] \<open>Linking the Formal with the Informal\<close>
text*[auth1::author, affiliation="Université Paris-Sud"]\<open>Burkhart Wolff\<close>
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 \<open>intro\<close>} ... *}
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{*
\<bullet> @{bold \<open>XML\<close>} and dtd's,
\<bullet> OWL and Protege,
\<bullet> LaTeX setups such as ...
@{url "https://pdi.fbk.eu/technologies/tex-owl-latex-style-syntax-authoring-owl-2-ontologies"}
\<bullet> Structured Assurance Case Metamodel Specification.
@{url "https://www.omg.org/spec/SACM/1.0/About-SACM/"}}
\<bullet> AADL Alisa,
\<bullet> RATP Ovado
*}
subsection{* Discussion *}
text{* Lorem ipsum dolor sit amet, suspendisse non arcu malesuada mollis, nibh morbi, ... *}
close_monitor*[onto]
(* << *)
end
(* >> *)

79
examples/simple/Example.thy
View File

@ -6,17 +6,76 @@ begin
section{* Some show-off's of general antiquotations. *} section{* Some show-off's of general antiquotations. *}
(* some show-off of standard anti-quotations: *) (* some show-off of standard anti-quotations: *)
text{* @{thm refl} print_attributes
@{file "../../Isa_DOF.thy"} print_antiquotations
@{value "3+4::int"}
@{const hd} text{* @{thm refl} of name @{thm [source] refl}
@{theory List}} @{thm[mode=Rule] conjI}
@{term "3"} @{file "../../Isa_DOF.thy"}
@{type bool} @{value "3+4::int"}
@{term [show_types] "f x = a + x"} *} @{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 \<open> As established by @{docref (unchecked) \<open>t10\<close>},
@{docref (define) \<open>t10\<close>}
the @{docref \<open>t10\<close>}
the @{docref \<open>ass122\<close>}
\<close>
text \<open> safety related applicability condition @{srac \<open>ass122\<close>}.
exported constraint @{ec \<open>ass122\<close>}.
\<close>
text{*
And some ontologically inconsistent reference:
@{hypothesis \<open>ass1\<close>} as well as
*}
-- "very wrong"
text{*
And some ontologically inconsistent reference:
@{assumption \<open>hyp1\<close>} as well as
*}
-- "very wrong"
text{*
And some ontologically inconsistent reference:
@{test_result \<open>ass122\<close>} as well as
*}
-- wrong
text{*
And some other ontologically inconsistent reference:
@{ec \<open>t10\<close>} as well as
*}
-- wrong
section{* Some Tests for Ontology Framework and its CENELEC Instance *} 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 *) section(in order){* sdfsdf*} (* undocumented trouvaille when analysing the code *)
end end

56
ontologies/CENELEC_50126.thy
View File

@ -9,7 +9,7 @@ Common Criteria identifies:
(for the moment: defined by regular expressions describing the (for the moment: defined by regular expressions describing the
order of category instances in the overall document as a regular language) order of category instances in the overall document as a regular language)
*} *}
theory CENELEC_50126 theory CENELEC_50126
imports "../Isa_DOF" imports "../Isa_DOF"
begin begin
@ -62,7 +62,7 @@ doc_class assumption = requirement +
text{*The category @{emph \<open>exported constraint\<close>} (or @{emph \<open>ec\<close>} for short) text{*The category @{emph \<open>exported constraint\<close>} (or @{emph \<open>ec\<close>} for short)
is used for formal assumptions, that arise during the analysis, is used for formal assumptions, that arise during the analysis,
design or implementation and have to be tracked till the final 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. *} within the certification process, by it by test or proof. *}
doc_class ec = assumption + 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 \<open> As established by @{docref (unchecked) \<open>t10\<close>},
@{docref (define) \<open>t10\<close>}
the @{docref \<open>t10\<close>}
assumption @{docref \<open>ass122\<close>} is validated. \<close>
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 *} section{* Testing and Validation *}
@ -193,13 +153,15 @@ DOF_core.name2doc_class_name @{theory} "requirement";
DOF_core.name2doc_class_name @{theory} "srac"; DOF_core.name2doc_class_name @{theory} "srac";
DOF_core.is_defined_cid_global "srac" @{theory}; DOF_core.is_defined_cid_global "srac" @{theory};
DOF_core.is_defined_cid_global "ec" @{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.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.srac";
DOF_core.is_subclass @{context} "CENELEC_50126.ec" "CENELEC_50126.test_requirement";
val ({maxano, tab},tab2) = DOF_core.get_data @{context}; "XXXXXXXXXXXXXXXXX";
Symtab.dest tab; val ({maxano, tab=ref_tab},class_tab) = DOF_core.get_data @{context};
Symtab.dest tab2; Symtab.dest ref_tab;
Symtab.dest class_tab;
*} *}

19
ontologies/mathex_onto.thy Normal file
View File

@ -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

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

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