Isabelle_DOF
/
Isabelle_DOF
1
0
Fork 2
Code Issues 1 Pull Requests Releases Wiki Activity

Manual merge.

This commit is contained in:
Achim D. Brucker 2018-12-04 18:15:52 +00:00
parent 459538a1b7 a5f9442c6e
commit 781c1ed0dc
20 changed files with 500 additions and 134 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
Isa_COL.thy
View File

@ -31,20 +31,28 @@ doc_class side_by_side_figure = figure +
caption2 :: "string"
ML\<open>DOF_core.SPY;\<close>
doc_class figure_group =
(* trace :: "doc_class rexp list" <= "[]" automatically generated since monitor clause *)
caption :: "string"
rejects figure_group (* this forbids recursive figure-groups *)
accepts "\<lbrace>figure\<rbrace>\<^sup>+"
ML\<open>@{term "side_by_side_figure"};
@{typ "doc_class rexp"};
DOF_core.SPY;
\<close>
(* dito the future table *)
(* dito the future monitor: table - block *)
section\<open>Tests\<close>
ML\<open>@{term "side_by_side_figure"};
@{typ "doc_class rexp"};
DOF_core.SPY;
\<close>
end

157
Isa_DOF.thy
View File

@ -22,10 +22,10 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
keywords "+=" ":=" "accepts" "rejects"
and "title*" "subtitle*"
"chapter*" "section*" "subsection*" "subsubsection*"
"text*"
and "title*" "subtitle*"
"chapter*" "section*" "subsection*" "subsubsection*"
"paragraph*" "subparagraph*"
"text*"
"figure*"
"side_by_side_figure*"
:: document_body
@ -35,7 +35,7 @@ theory Isa_DOF (* Isabelle Document Ontology Framework *)
and "lemma*" "theorem*" "assert*" ::thy_decl
and "print_doc_classes" "print_doc_items" "gen_sty_template" :: diag
and "print_doc_classes" "print_doc_items" "gen_sty_template" "check_doc_global" :: diag
begin
@ -66,8 +66,9 @@ section\<open> A HomeGrown Document Type Management (the ''Model'') \<close>
ML\<open>
structure DOF_core =
struct
type docclass_struct = {params : (string * sort) list, (*currently not used *)
name : binding, thy_name : string, id : serial, (* for pide *)
type docclass_struct = {params : (string * sort) list, (*currently not used *)
name : binding,
thy_name : string, id : serial, (* for pide *)
inherits_from : (typ list * string) option, (* imports *)
attribute_decl : (binding * typ * term option) list, (* class local *)
rejectS : term list,
@ -121,7 +122,7 @@ struct
type ISA_transformer_tab = (theory -> term * typ * Position.T -> term option) Symtab.table
val initial_ISA_tab:ISA_transformer_tab = Symtab.empty
type docclass_inv_tab = (Context.generic -> bool) Symtab.table
type docclass_inv_tab = (string -> {is_monitor:bool} -> Context.generic -> bool) Symtab.table
val initial_docclass_inv_tab : docclass_inv_tab = Symtab.empty
type open_monitor_info = {accepted_cids : string list,
@ -175,7 +176,7 @@ fun upd_docobj_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab,d
{docobj_tab = f docobj_tab, docclass_tab=docclass_tab,
ISA_transformer_tab=ISA_transformer_tab, monitor_tab=monitor_tab,
docclass_inv_tab=docclass_inv_tab};
fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab, docclass_inv_tab} =
fun upd_docclass_tab f {docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab, docclass_inv_tab} =
{docobj_tab=x,docclass_tab = f y,ISA_transformer_tab = z, monitor_tab=monitor_tab,
docclass_inv_tab=docclass_inv_tab};
fun upd_ISA_transformers f{docobj_tab=x,docclass_tab = y,ISA_transformer_tab = z, monitor_tab, docclass_inv_tab} =
@ -188,7 +189,7 @@ fun upd_monitor_tabs f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab
fun upd_docclass_inv_tab f {docobj_tab,docclass_tab,ISA_transformer_tab, monitor_tab, docclass_inv_tab} =
{docobj_tab = docobj_tab,docclass_tab = docclass_tab,
ISA_transformer_tab = ISA_transformer_tab, monitor_tab = monitor_tab,
docclass_inv_tab= f docclass_inv_tab};
docclass_inv_tab = f docclass_inv_tab};
fun get_accepted_cids ({accepted_cids, ... } : open_monitor_info) = accepted_cids
@ -232,12 +233,19 @@ fun is_defined_cid_global cid thy = let val t = #docclass_tab(get_data_global th
Symtab.defined t (name2doc_class_name thy cid)
end
fun is_defined_cid_global' cid_long thy = let val t = #docclass_tab(get_data_global thy)
in cid_long=default_cid orelse Symtab.defined t cid_long end
fun is_defined_cid_local cid ctxt = let val t = #docclass_tab(get_data ctxt)
in cid=default_cid orelse
Symtab.defined t (name2doc_class_name_local ctxt cid)
end
fun is_defined_cid_local' cid_long ctxt = let val t = #docclass_tab(get_data ctxt)
in cid_long=default_cid orelse Symtab.defined t cid_long end
fun is_declared_oid_global oid thy = let val {tab,...} = #docobj_tab(get_data_global thy)
in Symtab.defined tab oid end
@ -272,6 +280,24 @@ fun declare_object_local oid ctxt =
handle Symtab.DUP _ => error("multiple declaration of document reference"))
end
fun update_class_invariant cid_long f thy =
let val _ = if is_defined_cid_global' cid_long thy then ()
else error("undefined class id : " ^cid_long)
in map_data_global (upd_docclass_inv_tab (Symtab.update (cid_long,
(fn ctxt => ((writeln("Inv check of : " ^cid_long); f ctxt ))))))
thy
end
fun get_class_invariant cid_long thy =
let val _ = if is_defined_cid_global' cid_long thy then ()
else error("undefined class id : " ^cid_long)
val {docclass_inv_tab, ...} = get_data_global thy
in case Symtab.lookup docclass_inv_tab cid_long of
NONE => K(K(K true))
| SOME f => f
end
val SPY = Unsynchronized.ref(Bound 0)
fun check_regexps term =
@ -464,9 +490,10 @@ fun update_value_global oid upd thy =
val ISA_prefix = "Isa_DOF.ISA_" (* ISA's must be declared in Isa_DOF.thy !!! *)
fun get_isa_global isa thy = case Symtab.lookup (#ISA_transformer_tab(get_data_global thy)) (ISA_prefix^isa) of
NONE => error("undefined inner syntax antiquotation: "^isa)
|SOME(bbb) => bbb
fun get_isa_global isa thy =
case Symtab.lookup (#ISA_transformer_tab(get_data_global thy)) (ISA_prefix^isa) of
NONE => error("undefined inner syntax antiquotation: "^isa)
| SOME(bbb) => bbb
fun get_isa_local isa ctxt = case Symtab.lookup (#ISA_transformer_tab(get_data ctxt)) (ISA_prefix^isa) of
@ -536,6 +563,14 @@ fun print_doc_classes b ctxt =
writeln "=====================================\n\n\n"
end;
fun check_doc_global (strict_checking : bool) ctxt =
let val {docobj_tab={tab = x, ...}, ...} = get_data ctxt;
val S = map_filter (fn (s,NONE) => SOME s | _ => NONE) (Symtab.dest x)
in if null S
then ()
else error("Global consistency error - Unresolved forward references: "^ String.concatWith "," S)
end
val _ =
Outer_Syntax.command @{command_keyword print_doc_classes}
"print document classes"
@ -548,6 +583,13 @@ val _ =
(Parse.opt_bang >> (fn b =>
Toplevel.keep (print_doc_items b o Toplevel.context_of)));
val _ =
Outer_Syntax.command @{command_keyword check_doc_global}
"check global document consistency"
(Parse.opt_bang >> (fn b =>
Toplevel.keep (check_doc_global b o Toplevel.context_of)));
fun toStringLaTeXNewKeyCommand env long_name =
"\\expandafter\\newkeycommand\\csname"^" "^"isaDof."^env^"."^long_name^"\\endcsname%\n"
@ -894,13 +936,13 @@ fun calc_update_term thy cid_long (S:(string * Position.T * string * term)list)
val _ = if Long_Name.base_name lhs = lhs orelse ln = lhs then ()
else error("illegal notation for attribute of "^cid_long)
fun join (ttt as @{typ "int"})
= Const (@{const_name "plus"}, ttt --> ttt --> ttt)
= Const (@{const_name "Groups.plus"}, ttt --> ttt --> ttt)
|join (ttt as @{typ "string"})
= Const (@{const_name "append"}, ttt --> ttt --> ttt)
= Const (@{const_name "List.append"}, ttt --> ttt --> ttt)
|join (ttt as Type(@{type_name "set"},_))
= Const (@{const_name "sup"}, ttt --> ttt --> ttt)
= Const (@{const_name "Lattices.sup"}, ttt --> ttt --> ttt)
|join (ttt as Type(@{type_name "list"},_))
= Const (@{const_name "append"}, ttt --> ttt --> ttt)
= Const (@{const_name "List.append"}, ttt --> ttt --> ttt)
|join _ = error("implicit fusion operation not defined for attribute: "^ lhs)
(* could be extended to bool, map, multisets, ... *)
val rhs' = instantiate_term tyenv' (generalize_term rhs)
@ -929,7 +971,7 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy =
along the super-class id. The evaluation is in parallel, simulating a product
semantics without expanding the subclass relationship. *)
fun is_enabled_for_cid moid =
let val {accepted_cids, rejected_cids, automatas} =
let val {accepted_cids, automatas, ...} =
the(Symtab.lookup monitor_tab moid)
val indexS= 1 upto (length automatas)
val indexed_autoS = automatas ~~ indexS
@ -954,16 +996,22 @@ fun register_oid_cid_in_open_monitors oid pos cid_long thy =
val _ = if null enabled_monitors then () else writeln "registrating in monitors ..."
val _ = app (fn n => writeln(oid^" : "^cid_long^" ==> "^n)) enabled_monitors;
(* check that any transition is possible : *)
fun inst_class_inv x = DOF_core.get_class_invariant(cid_of x) thy x {is_monitor=false}
fun class_inv_checks ctxt = map (fn x => inst_class_inv x ctxt) enabled_monitors
val delta_autoS = map is_enabled_for_cid enabled_monitors;
fun update_info (n, aS) (tab: DOF_core.monitor_tab) =
let val {accepted_cids,rejected_cids,automatas} = the(Symtab.lookup tab n)
let val {accepted_cids,rejected_cids,...} = the(Symtab.lookup tab n)
in Symtab.update(n, {accepted_cids=accepted_cids,
rejected_cids=rejected_cids,
automatas=aS}) tab end
fun update_trace mon_oid = DOF_core.update_value_global mon_oid (def_trans mon_oid)
val update_automatons = DOF_core.upd_monitor_tabs(fold update_info delta_autoS)
in thy |> fold (update_trace) (enabled_monitors)
|> DOF_core.map_data_global(update_automatons)
in thy |> (* update traces of all enabled monitors *)
fold (update_trace) (enabled_monitors)
|> (* check class invariants of enabled monitors *)
(fn thy => (class_inv_checks (Context.Theory thy); thy))
|> (* update the automata of enabled monitors *)
DOF_core.map_data_global(update_automatons)
end
@ -981,12 +1029,15 @@ fun create_and_check_docitem is_monitor oid pos cid_pos doc_attrs thy =
fun conv_attrs ((lhs, pos), rhs) = (markup2string lhs,pos,"=", Syntax.read_term_global thy rhs)
val assns' = map conv_attrs doc_attrs
val (value_term, _(*ty*), _) = calc_update_term thy cid_long assns' defaults
val check_inv = (DOF_core.get_class_invariant cid_long thy oid {is_monitor=is_monitor})
o Context.Theory
in thy |> DOF_core.define_object_global (oid, {pos = pos,
thy_name = Context.theory_name thy,
value = value_term,
id = id,
cid = cid_long})
|> register_oid_cid_in_open_monitors oid pos cid_long
|> (fn thy => (check_inv thy; thy))
end
@ -1011,18 +1062,26 @@ fun update_instance_command (((oid:string,pos),cid_pos),
Syntax.read_term_global thy rhs)
val assns' = map conv_attrs doc_attrs
val def_trans = #1 o (calc_update_term thy cid_long assns')
val check_inv = (DOF_core.get_class_invariant cid_long thy oid {is_monitor=false})
o Context.Theory
in
thy |> DOF_core.update_value_global oid (def_trans)
|> (fn thy => (check_inv thy; thy))
end
fun enriched_document_command markdown (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
fun enriched_document_command markdown level (((((oid,pos),cid_pos), doc_attrs) : meta_args_t,
xstring_opt:(xstring * Position.T) option),
toks:Input.source)
: Toplevel.transition -> Toplevel.transition =
let
fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy)
(* as side-effect, generates markup *)
fun check_text thy = (Thy_Output.output_text(Toplevel.theory_toplevel thy) markdown toks; thy)
(* generating the level-attribute syntax *)
val doc_attrs' = case level of
NONE => doc_attrs
| SOME(NONE) => (("level",@{here}),"None")::doc_attrs
| SOME(SOME x) => (("level",@{here}),"Some("^ Int.toString x ^"::int)")::doc_attrs
in
Toplevel.theory(create_and_check_docitem false oid pos cid_pos doc_attrs #> check_text)
(* Thanks Frederic Tuong! ! ! *)
@ -1059,7 +1118,11 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
SOME X => check_if_final X
| NONE => error ("Not belonging to a monitor class: "^oid)
val delete_monitor_entry = DOF_core.map_data_global (DOF_core.upd_monitor_tabs (Symtab.delete oid))
in thy |> update_instance_command args
val {cid=cid_long, ...} = the(DOF_core.get_object_global oid thy)
val check_inv = (DOF_core.get_class_invariant cid_long thy oid) {is_monitor=true}
o Context.Theory
in thy |> update_instance_command args
|> (fn thy => (check_inv thy; thy))
|> delete_monitor_entry
end
@ -1067,59 +1130,59 @@ fun close_monitor_command (args as (((oid:string,pos),cid_pos),
val _ =
Outer_Syntax.command ("title*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} NONE) ;
val _ =
Outer_Syntax.command ("subtitle*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} NONE);
val _ =
Outer_Syntax.command ("chapter*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 0)));
val _ =
Outer_Syntax.command ("section*", @{here}) "section heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 1)));
val _ =
Outer_Syntax.command ("subsection*", @{here}) "subsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 2)));
val _ =
Outer_Syntax.command ("subsubsection*", @{here}) "subsubsection heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 3)));
val _ =
Outer_Syntax.command ("paragraph*", @{here}) "paragraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 4)));
val _ =
Outer_Syntax.command ("subparagraph*", @{here}) "subparagraph heading"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} (SOME(SOME 5)));
val _ =
Outer_Syntax.command ("figure*", @{here}) "figure"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} NONE);
val _ =
Outer_Syntax.command ("side_by_side_figure*", @{here}) "multiple figures"
(attributes -- Parse.opt_target -- Parse.document_source --| semi
>> enriched_document_command {markdown = false});
>> enriched_document_command {markdown = false} NONE);
val _ =
Outer_Syntax.command ("text*", @{here}) "formal comment (primary style)"
(attributes -- Parse.opt_target -- Parse.document_source
>> enriched_document_command {markdown = true});
>> enriched_document_command {markdown = true} (SOME NONE));
val _ =
Outer_Syntax.command @{command_keyword "declare_reference*"}
@ -1288,6 +1351,7 @@ fun docitem_value_ML_antiquotation binding =
(* Setup for general docrefs of the global DOF_core.default_cid - class ("text")*)
val _ = Theory.setup((docitem_ref_antiquotation @{binding docref} DOF_core.default_cid) #>
(* deprecated syntax ^^^^^^*)
(docitem_ref_antiquotation @{binding docitem_ref} DOF_core.default_cid) #>
(* deprecated syntax ^^^^^^^^^^*)
(docitem_ref_antiquotation @{binding docitem} DOF_core.default_cid) #>
@ -1301,7 +1365,7 @@ ML\<open>
structure AttributeAccess =
struct
fun calculate_attr_access ctxt proj_term term =
fun calculate_attr_access0 ctxt proj_term term =
(* term assumed to be ground type, (f term) not necessarily *)
let val [subterm'] = Type_Infer_Context.infer_types ctxt [proj_term $ term]
val ty = type_of (subterm')
@ -1322,9 +1386,9 @@ fun calculate_attr_access ctxt proj_term term =
Syntax.string_of_term ctxt subterm')
end
fun calculate_attr_access_check ctxt attr oid pos = (* template *)
case DOF_core.get_value_local oid (Context.the_proof ctxt) of
SOME term => let val ctxt = Context.the_proof ctxt
fun calc_attr_access ctxt attr oid pos = (* template *)
case DOF_core.get_value_global oid (Context.theory_of ctxt) of
SOME term => let val ctxt = (Proof_Context.init_global (Context.theory_of ctxt))
val SOME{cid,pos=pos_decl,id,...} = DOF_core.get_object_local oid ctxt
val markup = docref_markup false oid id pos_decl;
val _ = Context_Position.report ctxt pos markup;
@ -1332,9 +1396,9 @@ fun calculate_attr_access_check ctxt attr oid pos = (* template *)
{long_name, typ=ty,...} =
case DOF_core.get_attribute_info_local cid attr ctxt of
SOME f => f
| NONE => error ("attribute undefined for ref"^ oid)
| NONE => error ("attribute undefined for reference: "^ oid)
val proj_term = Const(long_name,dummyT --> ty)
in calculate_attr_access ctxt proj_term term end
in calculate_attr_access0 ctxt proj_term term end
| NONE => error "identifier not a docitem reference"
val _ = Theory.setup
@ -1346,7 +1410,7 @@ val _ = Theory.setup
>>
(fn(attr:string,(oid:string,pos))
=> (ML_Syntax.atomic o ML_Syntax.print_term)
(calculate_attr_access_check ctxt attr oid pos))
(calc_attr_access ctxt attr oid pos))
: string context_parser
)
(ctxt, toks))
@ -1354,8 +1418,8 @@ val _ = Theory.setup
fun calculate_trace ctxt oid pos =
(* grabs attribute, and converts its HOL-term into (textual) ML representation *)
let fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
val term = calculate_attr_access_check ctxt "trace" oid pos
let val term = calc_attr_access ctxt "trace" oid pos
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
val string_pair_list = map conv (HOLogic.dest_list term)
val print_string_pair = ML_Syntax.print_pair ML_Syntax.print_string ML_Syntax.print_string
in ML_Syntax.print_list print_string_pair string_pair_list end
@ -1491,11 +1555,6 @@ ML\<open>
section\<open> Testing and Validation \<close>
text*[sdf] {* f @{thm refl}*}
text*[sdfg] {* fg @{thm refl}*}
text*[xxxy] {* dd @{docitem \<open>sdfg\<close>} @{thm refl}*}
(* the following test crashes the LaTeX generation - however, without the latter this output is
instructive
ML\<open>
@ -1507,6 +1566,4 @@ writeln (DOF_core.toStringDocItemRef "scholarly_paper.introduction" "XX" []);
\<close>
*)
end

5
ROOTS
View File

@ -1,3 +1,2 @@
AFP-contribs/Regular-Sets
AFP-contribs/Functional-Automata
examples/
AFP-contribs
examples

3
examples/cenelec/Example.thy
View File

@ -70,9 +70,6 @@ paragraph* [sdfk] \<open> just a paragraph - lexical variant \<close>
section\<open> Some global inspection commands for the status of docitem and doc-class tables ... \<close>
print_doc_classes
print_doc_items
section\<open> Text Antiquotation Infrastructure ... \<close>

2
examples/conceptual/Attributes.thy
View File

@ -10,7 +10,7 @@ print_doc_items
(* this corresponds to low-level accesses : *)
ML\<open>
val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab}
val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...}
= DOF_core.get_data @{context};
Symtab.dest docitem_tab;

50
examples/conceptual/Concept_Example.thy Normal file
View File

@ -0,0 +1,50 @@
chapter\<open>Setting and modifying attributes of doc-items\<close>
theory Concept_Example
imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *)
begin
text\<open>@{theory Conceptual} provides a monitor @{typ M} enforcing a particular document structure.
Here, we say: From now on, this structural rules are respected wrt. all doc\_classes M is
enabled for.\<close>
open_monitor*[struct::M]
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
text*[d::D, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus,
... @{docitem \<open>c1\<close>} @{thm "refl"}\<close>
update_instance*[d::D, a1 := X2]
text\<open> ... in ut tortor ... @{docitem \<open>a\<close>} ... @{A \<open>a\<close>}\<close>
text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer. \<close>
section*[f::F] \<open> Lectus accumsan velit ultrices, ... }\<close>
theorem some_proof : "P" sorry
text\<open>This is an example where we add a theorem into a kind of "result-list" of the doc-item f.\<close>
update_instance*[f::F,r:="[@{thm ''Concept_Example.some_proof''}]"]
text\<open> ..., mauris amet, id elit aliquam aptent id, ... @{docitem \<open>a\<close>} \<close>
text\<open>Here we add and maintain a link that is actually modeled as m-to-n relation ...\<close>
update_instance*[f::F,b:="{(@{docitem ''a''}::A,@{docitem ''c1''}::C),
(@{docitem ''a''}, @{docitem ''c2''})}"]
close_monitor*[struct]
text\<open>And the trace of the monitor is:\<close>
ML\<open>@{trace_attribute struct}\<close>
print_doc_classes
print_doc_items
end

108
examples/conceptual/Concept_ExampleInvariant.thy Normal file
View File

@ -0,0 +1,108 @@
chapter\<open>Setting and modifying attributes of doc-items\<close>
theory Concept_ExampleInvariant
imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *)
begin
section\<open>Example: Standard Class Invariant\<close>
text\<open>Status:\<close>
print_doc_classes
print_doc_items
text\<open>Watch out: The current programming interface to document class invariants is pretty low-level:
\<^item> No inheritance principle
\<^item> No high-level notation in HOL
\<^item> Typing on ML level is assumed to be correct.
The implementor of an ontology must know what he does ...
\<close>
text\<open>Setting a sample invariant, which simply produces some side-effect:\<close>
setup\<open>DOF_core.update_class_invariant "Conceptual.A" (fn oid =>
fn {is_monitor = b} =>
fn ctxt =>
(writeln ("sample echo : "^oid); true))\<close>
subsection*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
ML\<open>fun check_A_invariant oid {is_monitor:bool} ctxt =
let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here}
val (@{typ "int"},x_value) = HOLogic.dest_number term
in if x_value > 5 then error("class A invariant violation") else true end
\<close>
setup\<open>DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\<close>
subsection*[d::A, x = "4"] \<open> Lorem ipsum dolor sit amet, ... \<close>
(* test : update should not fail, invariant still valid *)
update_instance*[d::A, x += "1"]
section\<open>Example: Monitor Class Invariant\<close>
text\<open>Of particular interest are class invariants attached to monitor classes: since the
latter manage a trace-attribute, a class invariant on them can assure a global form of consistency.
It is possible to express:
\<^item> that attributes of a document element must satisfy particular conditions depending on the
prior document elements --- as long they have been observed in a monitor.
\<^item> non-regular properties on a trace not expressible in a regular expression
(like balanced ness of opening and closing text elements)
\<^item> etc.
\<close>
text\<open>A simple global trace-invariant is expressed in the following: it requires
that instances of class C occur more often as those of class D; note that this is meant
to take sub-classing into account:
\<close>
ML\<open>fun check_M_invariant oid {is_monitor} ctxt =
let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here}
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
val string_pair_list = map conv (HOLogic.dest_list term)
val cid_list = map fst string_pair_list
val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
fun is_C x = DOF_core.is_subclass ctxt' x "Conceptual.C"
fun is_D x = DOF_core.is_subclass ctxt' x "Conceptual.D"
val n = length (filter is_C cid_list)
val m = length (filter is_D cid_list)
in if m > n then error("class M invariant violation") else true end
\<close>
setup\<open>DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\<close>
open_monitor*[struct::M]
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
text*[d1::E, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer... \<close>
section*[f::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
(* test : close_monitor should fail :
section*[f2::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
*)
ML\<open>val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here};
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
val string_pair_list = map conv (HOLogic.dest_list term)
\<close>
(* trace example *)
text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
close_monitor*[struct]
end

2
examples/math_exam/BAC2017/BAC2017.thy
View File

@ -86,7 +86,7 @@ lemma q2_b : "0 \<le> x \<and> x \<le> y \<and> y \<le> 1 \<Longrightarrow> h x
lemma q2_c : "1 \<le> x \<and> x \<le> y \<Longrightarrow> h x \<ge> h y"
sorry
text*[v2::Validation, proofs="[@{thm ''q2_b''}, @{thm ''q2_c''}]"]
text*[v2::Validation, proofs="[@{thm ''BAC2017.q2_b''}, @{thm ''BAC2017.q2_c''}]"]
{* See lemmas @{thm q2_b} and @{thm q2_c}. *}

10
examples/scholarly_paper/2018_cicm/IsaDofApplications.thy
View File

@ -44,8 +44,8 @@ on top of Isabelle. \isadof allows for conventional typesetting
for enforcing a certain document structure, and discuss ontology-specific IDE support.
\<close>
section*[intro::introduction_title]\<open> Introduction \<close>
text*[introtext::introduction_elem]\<open>
section*[intro::introduction]\<open> Introduction \<close>
text*[introtext::introduction]\<open>
The linking of the \<^emph>\<open>formal\<close> to the \<^emph>\<open>informal\<close> is perhaps the
most pervasive challenge in the digitization of knowledge and its
propagation. This challenge incites numerous research efforts
@ -94,7 +94,7 @@ declare_reference*[ontomod::text_section]
declare_reference*[ontopide::text_section]
declare_reference*[conclusion::text_section]
(*>*)
text*[plan::introduction_elem]\<open> The plan of the paper is follows: we start by introducing the underlying
text*[plan::introduction]\<open> The plan of the paper is follows: we start by introducing the underlying
Isabelel sytem (@{docitem (unchecked) \<open>bgrnd\<close>}) followed by presenting the
essentials of \isadof and its ontology language (@{docitem (unchecked) \<open>isadof\<close>}).
It follows @{docitem (unchecked) \<open>ontomod\<close>}, where we present three application
@ -104,7 +104,7 @@ conclusions and discuss related work in @{docitem_ref (unchecked) \<open>conclu
section*[bgrnd::text_section,main_author="Some(@{docitem ''adb''}::author)"]
\<open> Background: The Isabelle System \<close>
text*[background::introduction_elem]\<open>
text*[background::introduction]\<open>
While Isabelle is widely perceived as an interactive theorem prover
for HOL (Higher-order Logic)~@{cite "nipkow.ea:isabelle:2002"}, we
would like to emphasize the view that Isabelle is far more than that:
@ -133,7 +133,7 @@ figure*[architecture::figure,relative_width="100",src="''figures/isabelle-archit
asynchronous communication between the Isabelle system and
the IDE (right-hand side). \<close>
text*[blug::introduction_elem]\<open> The Isabelle system architecture shown in @{docitem_ref \<open>architecture\<close>}
text*[blug::introduction]\<open> The Isabelle system architecture shown in @{docitem_ref \<open>architecture\<close>}
comes with many layers, with Standard ML (SML) at the bottom layer as implementation
language. The architecture actually foresees a \<^emph>\<open>Nano-Kernel\<close> (our terminology) which
resides in the SML structure \texttt{Context}. This structure provides a kind of container called

6
examples/simple/Concept_Example.thy
View File

@ -41,6 +41,10 @@ close_monitor*[struct]
text\<open>And the trace of the monitor is:\<close>
ML\<open>@{trace_attribute struct}\<close>
print_doc_classes
print_doc_items
check_doc_global
end

1
examples/technical_report/IsaDof_Manual/IsaDofManual.thy
View File

@ -10,6 +10,7 @@ text\<open>Resulting trace in doc\_item ''this'': \<close>
ML\<open>@{trace_attribute this}\<close>
(*<*)
end
(*>*)

17
examples/technical_report/TR_my_commented_isabelle/MyCommentedIsabelle.thy
View File

@ -271,7 +271,14 @@ Context.certificate_theory_id : Context.certificate -> Context.theory_id;
Context.theory_name : theory -> string;
Context.map_theory: (theory -> theory) -> Context.generic -> Context.generic;
*}
text\<open>ML structure @{ML_structure Proof_Context}:\<close>
ML\<open>
Proof_Context.init_global: theory -> Proof.context;
Context.Proof: Proof.context -> Context.generic; (* the path to a generic Context *)
Proof_Context.get_global: theory -> string -> Proof.context
\<close>
subsection\<open>Mechanism 2 : global arbitrary data structure that is attached to the global and
@ -783,6 +790,14 @@ Gentzen Natural Deduction (to which Isabelle/Pure is geared) reasoning and
Gentzen Sequent Deduction.\<close>
section\<open>The classical goal package\<close>
ML\<open> open Goal;
Goal.prove_internal : Proof.context -> cterm list -> cterm -> (thm list -> tactic) -> thm;
Goal.prove_global : theory -> string list -> term list -> term ->
({context: Proof.context, prems: thm list} -> tactic) -> thm
\<close>
section\<open>The Isar Engine\<close>

BIN
examples/technical_report/TR_my_commented_isabelle/output/document.pdf
View File

Binary file not shown.

35
ontologies/Conceptual.thy
View File

@ -6,14 +6,14 @@ doc_class A =
x :: int
doc_class B =
x :: "string" (* attributes live in their own name-space *)
y :: "string list" <= "[]" (* and can have arbitrary type constructors *)
(* LaTeX may have problems with this, though *)
doc_class C = B +
z :: "A option" <= None (* A LINK, i.e. an attribute that has a type
referring to a document class. Mathematical
relations over document items can be modeled. *)
x :: "string" (* attributes live in their own name-space *)
y :: "string list" <= "[]" (* and can have arbitrary type constructors *)
(* LaTeX may have problems with this, though *)
doc_class C = B +
z :: "A option" <= None (* A LINK, i.e. an attribute that has a type
referring to a document class. Mathematical
relations over document items can be modeled. *)
g :: "thm"
datatype enum = X1 | X2 | X3
@ -26,20 +26,29 @@ doc_class D = B +
a2 :: int <= 0
doc_class E = D +
x :: "string" <= "''qed''" (* overriding default *)
x :: "string" <= "''qed''" (* overriding default *)
doc_class F =
r :: "thm list"
u :: "file"
s :: "typ list"
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
to an association class. It can be used to track
claims to result - relations, for example.*)
b :: "(A \<times> C) set" <= "{}" (* This is a relation link, roughly corresponding
to an association class. It can be used to track
claims to result - relations, for example.*)
doc_class G = C +
g :: "thm" <= "@{thm ''HOL.refl''}"
doc_class M =
trace :: "(A + C + D + F) list"
accepts "A ~~ \<lbrace>C || D\<rbrace>\<^sup>* ~~ \<lbrakk>F\<rbrakk>"
section*[test::A]\<open> Test and Validation\<close>
text\<open>Defining some document elements to be referenced in later on in another theory: \<close>
text*[sdf] {* f @{thm refl}*}
text*[sdfg] {* fg @{thm refl}*}
text*[xxxy] {* dd @{docitem \<open>sdfg\<close>} @{thm refl}*}
end

33
ontologies/scholarly_paper.thy
View File

@ -25,17 +25,20 @@ doc_class abstract =
doc_class text_section =
main_author :: "author option" <= None
fixme_list :: "string list" <= "[]"
level :: "int option" <= "None"
(* we follow LaTeX terminology on levels
part = Some -1
chapter = Some 0
section = Some 1
subsection = Some 2
subsubsection = Some 3
... *)
(* for scholarly paper: invariant level > 0 *)
doc_class introduction = text_section +
comment :: string
claims :: "thm list"
doc_class introduction_title = introduction +
fixme_list :: "string list" <= "[]"
doc_class introduction_elem = introduction +
fixme_list :: "string list" <= "[]"
doc_class technical = text_section +
definition_list :: "string list" <= "[]"
formal_results :: "thm list"
@ -84,16 +87,14 @@ text \<open>underlying idea: a monitor class automatically receives a
doc_class article =
style_id :: string <= "''LNCS''"
version :: "(int \<times> int \<times> int)" <= "(0,0,0)"
accepts "(title ~~
\<lbrakk>subtitle\<rbrakk> ~~
\<lbrace>author\<rbrace>\<^sup>+ ~~
abstract ~~
introduction_title ~~
\<lbrace>introduction_elem\<rbrace>\<^sup>+ ~~
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
\<lbrakk>introduction\<rbrakk> ~~
conclusion ~~
bibliography)"
accepts "(title ~~
\<lbrakk>subtitle\<rbrakk> ~~
\<lbrace>author\<rbrace>\<^sup>+ ~~
abstract ~~
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
bibliography)"
gen_sty_template

35
ontologies/technical_report.thy
View File

@ -4,29 +4,36 @@ theory technical_report
imports "scholarly_paper"
begin
(* for reports paper: invariant: level \<ge> -1 *)
doc_class table_of_contents =
depth :: int <= 3
bookmark_depth :: int <= 3
depth :: int <= 3
doc_class front_matter =
style :: string
front_matter_style :: string (* TODO Achim :::: *)
doc_class index =
kind :: "doc_class"
level :: "int option"
doc_class "chapter" = text_section +
style :: string
doc_class report =
style_id :: string <= "''LNCS''"
version :: "(int \<times> int \<times> int)" <= "(0,0,0)"
accepts "(title ~~
\<lbrakk>subtitle\<rbrakk> ~~
\<lbrace>author\<rbrace>\<^sup>+ ~~
\<lbrakk>front_matter\<rbrakk> ~~
abstract ~~
\<lbrakk>table_of_contents\<rbrakk> ~~
introduction ~~
accepts "(title ~~
\<lbrakk>subtitle\<rbrakk> ~~
\<lbrace>author\<rbrace>\<^sup>+ ~~
\<lbrakk>front_matter\<rbrakk> ~~
abstract ~~
\<lbrakk>table_of_contents\<rbrakk> ~~
\<lbrace>introduction\<rbrace>\<^sup>+ ~~
\<lbrace>technical || example\<rbrace>\<^sup>+ ~~
conclusion ~~
\<lbrakk>table_of_contents\<rbrakk> ~~
\<lbrace>conclusion\<rbrace>\<^sup>+ ~~
\<lbrace>index\<rbrace>\<^sup>+ ~~
bibliography)"
ML\<open>
\<close>
end

4
test/cenelec/Example.thy
View File

@ -97,9 +97,9 @@ text{* @{test_specification \<open>ass122\<close>} -- wrong: "reference ontologi
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 !!! *)
(* shouldn't work: label exists, but definition was finally rejected to to errors. *)
check_doc_global (* shoudn't work : Unresolved forward references: lalala,blablabla *)
section \<open>Miscellaneous\<close>

36
test/conceptual/Attributes.thy
View File

@ -10,10 +10,11 @@ print_doc_items
(* corresponds to low-level accesses : *)
ML\<open>
val ({tab = x, ...},y,_)= DOF_core.get_data @{context};
Symtab.dest x;
val {docobj_tab={tab = docitem_tab, ...},docclass_tab, ISA_transformer_tab, monitor_tab,...}
= DOF_core.get_data @{context};
Symtab.dest docitem_tab;
"==============================================";
Symtab.dest y;
Symtab.dest docclass_tab;
\<close>
text*[dfgdfg::B, Conceptual.B.x ="''f''", y = "[''sdf'']"]\<open> sdfsdfs sdfsdf sdfsdf @{thm refl} \<close>
@ -63,34 +64,34 @@ text\<open>A not too trivial test: default y -> [].
The latter wins at access time.
Then @{term "t"}: creation of a multi inheritance object omega,
triple updates, the last one wins.\<close>
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::dfgdfg});
val t = HOLogic.dest_string (@{docitem_attr x::omega}); \<close>
ML\<open>val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::dfgdfg});
val t = HOLogic.dest_string (@{docitem_attribute x::omega}); \<close>
section\<open>Mutation of Attibutes in DocItems\<close>
ML\<open> val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attr a2::omega} \<close>
ML\<open> val Const ("Groups.zero_class.zero", @{typ "int"}) = @{docitem_attribute a2::omega} \<close>
update_instance*[omega::E, a2+="1"]
ML\<open> val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attr a2::omega} \<close>
ML\<open> val Const ("Groups.one_class.one", @{typ "int"})= @{docitem_attribute a2::omega} \<close>
update_instance*[omega::E, a2+="6"]
ML\<open> @{docitem_attr a2::omega} \<close>
ML\<open> HOLogic.dest_number @{docitem_attr a2::omega} \<close>
ML\<open> @{docitem_attribute a2::omega} \<close>
ML\<open> HOLogic.dest_number @{docitem_attribute a2::omega} \<close>
update_instance*[omega::E, x+="''inition''"]
ML\<open> val s = HOLogic.dest_string ( @{docitem_attr x::omega}) \<close>
ML\<open> val s = HOLogic.dest_string ( @{docitem_attribute x::omega}) \<close>
update_instance*[omega::E, y+="[''defini'',''tion'']"]
update_instance*[omega::E, y+="[''en'']"]
ML\<open> val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attr y::omega}); \<close>
ML\<open> val s = map HOLogic.dest_string (HOLogic.dest_list @{docitem_attribute y::omega}); \<close>
section\<open>Simulation of a Monitor\<close>
@ -98,20 +99,21 @@ open_monitor*[figs1::figure_group,
anchor="''fig-demo''",
caption="''Sample ''"]
figure*[fig_A::figure, spawn_columns=False,relative_width="''90''",
figure*[fig_A::figure, spawn_columns=False,relative_width="90",
src="''figures/A.png''"]
\<open> The A train \ldots \<close>
update_instance*[figs1::figure_group, trace+="[figure]"](* simulation : will disappear *)
figure*[fig_B::figure, spawn_columns=False,relative_width="''90''",
figure*[fig_B::figure, spawn_columns=False,relative_width="90",
src="''figures/B.png''"]
\<open> The B train \ldots \<close>
update_instance*[figs1::figure_group, trace+="[figure]"](* simulation : will disappear *)
close_monitor*[fig1]
close_monitor*[figs1]
ML\<open> map (fn Const(s,_) => s) (HOLogic.dest_list @{docitem_attr trace::figs1}) \<close>
text\<open>Resulting trace in figs1: \<close>
ML\<open>@{trace_attribute figs1}\<close>
print_doc_items
check_doc_global
end

109
test/conceptual/Concept_ExampleInvariant.thy Normal file
View File

@ -0,0 +1,109 @@
chapter\<open>Setting and modifying attributes of doc-items\<close>
theory Concept_ExampleInvariant
imports "../../ontologies/Conceptual" (* we use the generic "Conceptual" ontology *)
begin
section\<open>Example: Standard Class Invariant\<close>
text\<open>Status:\<close>
print_doc_classes
print_doc_items
text\<open>Watch out: The current programming interface to document class invariants is pretty low-level:
\<^item> No inheritance principle
\<^item> No high-level notation in HOL
\<^item> Typing on ML level is assumed to be correct.
The implementor of an ontology must know what he does ...
\<close>
text\<open>Setting a sample invariant, which simply produces some side-effect:\<close>
setup\<open>DOF_core.update_class_invariant "Conceptual.A" (fn oid =>
fn {is_monitor = b} =>
fn ctxt =>
(writeln ("sample echo : "^oid); true))\<close>
subsection*[b::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
ML\<open>fun check_A_invariant oid {is_monitor:bool} ctxt =
let val term = AttributeAccess.calc_attr_access ctxt "x" oid @{here}
val (@{typ "int"},x_value) = HOLogic.dest_number term
in if x_value > 5 then error("class A invariant violation") else true end
\<close>
setup\<open>DOF_core.update_class_invariant "Conceptual.A" check_A_invariant\<close>
(* test : should fail : *)
subsection*[c::A, x = "6"] \<open> Lorem ipsum dolor sit amet, ... \<close>
subsection*[d::A, x = "5"] \<open> Lorem ipsum dolor sit amet, ... \<close>
(* test : update should fail : *)
update_instance*[d::A, x += "1"]
section\<open>Example: Monitor Class Invariant\<close>
text\<open>Of particular interest are class invariants attached to monitor classes: since the
latter manage a trace-attribute, a class invariant on them can assure a global form of consistency.
It is possible to express:
\<^item> that attributes of a document element must satisfy particular conditions depending on the
prior document elements --- as long they have been observed in a monitor.
\<^item> non-regular properties on a trace not expressible in a regular expression
(like balanced ness of opening and closing text elements)
\<^item> etc.
\<close>
text\<open>A simple global trace-invariant is expressed in the following: it requires
that instances of class C occur more often as those of class D; note that this is meant
to take sub-classing into account:
\<close>
ML\<open>fun check_M_invariant oid {is_monitor} ctxt =
let val term = AttributeAccess.calc_attr_access ctxt "trace" oid @{here}
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
val string_pair_list = map conv (HOLogic.dest_list term)
val cid_list = map fst string_pair_list
val ctxt' = Proof_Context.init_global(Context.theory_of ctxt)
fun is_C x = DOF_core.is_subclass ctxt' x "Conceptual.C"
fun is_D x = DOF_core.is_subclass ctxt' x "Conceptual.D"
val n = length (filter is_C cid_list)
val m = length (filter is_D cid_list)
in if m > n then error("class M invariant violation") else true end
\<close>
setup\<open>DOF_core.update_class_invariant "Conceptual.M" check_M_invariant\<close>
open_monitor*[struct::M]
section*[a::A, x = "3"] \<open> Lorem ipsum dolor sit amet, ... \<close>
text*[c1::C, x = "''beta''"] \<open> ... suspendisse non arcu malesuada mollis, nibh morbi, ... \<close>
text*[d1::E, a1 = "X3"] \<open> ... phasellus amet id massa nunc, pede suscipit repellendus, ... \<close>
text*[c2::C, x = "''delta''"] \<open> ... in ut tortor eleifend augue pretium consectetuer... \<close>
section*[f::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
(* test : close_monitor should fail : *)
section*[f2::E] \<open> Lectus accumsan velit ultrices, ... }\<close>
ML\<open>val term = AttributeAccess.calc_attr_access (Context.Proof @{context}) "trace" "struct" @{here};
fun conv (Const(@{const_name "Pair"},_) $ Const(s,_) $ S) = (s, HOLogic.dest_string S)
val string_pair_list = map conv (HOLogic.dest_list term)
\<close>
(* trace example *)
text\<open>Setting a sample invariant, referring to attribute value "x":\<close>
close_monitor*[struct]
end

3
test/simple/Example.thy
View File

@ -95,8 +95,7 @@ section*[sedf::requirement, long_name = "None::string option"]
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*[seedf::test_case, dfg=34,fgdfg=zf]{* and another example with undefined attributes. *}
section{* Text Antiquotation Infrastructure ... *}