Management of doc_classes added,
elementary checking of doc-class referencing.
This commit is contained in:
parent
e29ee3789d
commit
1d8872272b
|
|
@ -7,7 +7,7 @@ Common Criteria identifies:
|
|||
- their subtype relation (eg., a "SRAC" is an "assumption"),
|
||||
- their syntactical structure
|
||||
(for the moment: defined by regular expressions describing the
|
||||
order of category instances in the overall document)
|
||||
order of category instances in the overall document as a regular language)
|
||||
*}
|
||||
|
||||
theory CENELEC_50126
|
||||
|
|
@ -18,13 +18,13 @@ text{* Excerpt of the BE EN 50128:2011 *}
|
|||
|
||||
section {* Requirements-Analysis related Categories *}
|
||||
|
||||
doc_class requirement_analysis_item =
|
||||
doc_class requirement =
|
||||
long_name :: "string option"
|
||||
|
||||
|
||||
doc_class requirement_analysis =
|
||||
no :: "nat"
|
||||
where "requirement_analysis_item +"
|
||||
where "requirement_item +"
|
||||
|
||||
text{*The category @{emph \<open>hypothesis\<close>} is used for assumptions from the
|
||||
foundational mathematical or physical domain, so for example:
|
||||
|
|
@ -41,18 +41,18 @@ text{*The category @{emph \<open>hypothesis\<close>} is used for assumptions fro
|
|||
|
||||
datatype hyp_type = physical | mathematical | computational | other
|
||||
|
||||
doc_class hypothesis = requirement_analysis_item +
|
||||
hyp_type :: hyp_type -- physical (* default *)
|
||||
doc_class hypothesis = requirement +
|
||||
hyp_type :: hyp_type <= physical (* default *)
|
||||
|
||||
text{*The category @{emph \<open>assumption\<close>} is used for domain-specific assumptions.
|
||||
It has formal , semi-formal and informal sub-categories. They have to be
|
||||
It has formal, semi-formal and informal sub-categories. They have to be
|
||||
tracked and discharged by appropriate validation procedures within a
|
||||
certification process, by it by test or proof. *}
|
||||
|
||||
datatype ass_kind = informal | semiformal | formal
|
||||
|
||||
doc_class assumption = requirement_analysis_item +
|
||||
assumption_kind :: ass_kind
|
||||
doc_class assumption = requirement +
|
||||
assumption_kind :: ass_kind <= informal
|
||||
|
||||
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,
|
||||
|
|
@ -61,7 +61,7 @@ text{*The category @{emph \<open>exported constraint\<close>} (or @{emph \<open>
|
|||
within the certification process, by it by test or proof. *}
|
||||
|
||||
doc_class ec = assumption +
|
||||
assumption_kind :: ass_kind -- (*default *) formal
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
|
||||
text{*The category @{emph \<open>safety related application condition\<close>} (or @{emph \<open>srac\<close>}
|
||||
for short) is used for @{typ ec}'s that establish safety properties
|
||||
|
|
@ -69,7 +69,18 @@ text{*The category @{emph \<open>safety related application condition\<close>} (
|
|||
is therefore particularly critical. *}
|
||||
|
||||
doc_class srac = ec +
|
||||
assumption_kind :: ass_kind -- (*default *) formal
|
||||
assumption_kind :: ass_kind <= (*default *) formal
|
||||
|
||||
section {* Design related Categories *}
|
||||
|
||||
doc_class design_item =
|
||||
description :: string
|
||||
|
||||
datatype design_kind = unit | module | protocol
|
||||
|
||||
doc_class interface = design_item +
|
||||
kind :: design_kind
|
||||
|
||||
|
||||
section {* Requirements-Analysis related Categories *}
|
||||
|
||||
|
|
@ -105,7 +116,7 @@ datatype test_environment_kind = hardware_in_the_loop ("hil")
|
|||
|
||||
doc_class test_environment = test_item +
|
||||
descr :: string
|
||||
kind :: test_environment_kind -- shil
|
||||
kind :: test_environment_kind <= shil
|
||||
|
||||
doc_class test_tool = test_item +
|
||||
descr :: string
|
||||
|
|
@ -120,6 +131,8 @@ doc_class test_documentation =
|
|||
no :: "nat"
|
||||
where "(test_specification.((test_case.test_result)+.(test_environment|test_tool))+.
|
||||
[test_requirement].test_adm_role"
|
||||
where "(test_specification.((test_case.test_result)+.(test_environment|test_tool))+.
|
||||
[test_requirement].test_adm_role"
|
||||
|
||||
section{* Example *}
|
||||
|
||||
|
|
@ -142,6 +155,12 @@ val _ = Theory.setup
|
|||
(DocAttrParser.control_antiquotation @{binding requirement_analysis_item} {strict_checking=true} "\\label{" "}"))
|
||||
|
||||
*}
|
||||
|
||||
ML{*
|
||||
DocObjTab.is_defined_cid_global "srac" @{theory};
|
||||
DocObjTab.is_defined_cid_global "ec" @{theory};
|
||||
|
||||
*}
|
||||
|
||||
end
|
||||
|
||||
144
Isa_DOF.thy
144
Isa_DOF.thy
|
|
@ -40,20 +40,18 @@ op |>> : ('a * 'c) * ('a -> 'b) -> 'b * 'c;
|
|||
op ||> : ('c * 'a) * ('a -> 'b) -> 'c * 'b
|
||||
*}
|
||||
|
||||
ML{*
|
||||
fun H1 f (a,b) = (f a, b)
|
||||
fun H2 f (a,b) = (a, f b)
|
||||
*}
|
||||
|
||||
|
||||
ML{*
|
||||
|
||||
structure DocObjTab =
|
||||
struct
|
||||
datatype docclass_struct = DocClassStruct of
|
||||
{inherits_from : string option,
|
||||
pos : Position.T, thy_name : string,
|
||||
id : serial, (* for pide *)
|
||||
attribute_decl : (string * string * string option) list}
|
||||
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,
|
||||
attribute_decl : (binding * typ * term option) list
|
||||
(*, rex : term list -- not yet used *)}
|
||||
|
||||
|
||||
type docclass_tab = docclass_struct Symtab.table
|
||||
|
||||
|
|
@ -67,10 +65,9 @@ struct
|
|||
| SOME X => X
|
||||
fun father_is_sub s = case Symtab.lookup tab s of
|
||||
NONE => error "inconsistent doc_class hierarchy"
|
||||
| SOME (DocClassStruct{inherits_from=NONE, ...}) => s = t
|
||||
| SOME (DocClassStruct{inherits_from=SOME s', ...}) => s' = t
|
||||
orelse
|
||||
father_is_sub s'
|
||||
| SOME ({inherits_from=NONE, ...}) => s = t
|
||||
| SOME ({inherits_from=SOME (_,s'), ...}) => s' = t
|
||||
orelse father_is_sub s'
|
||||
in s = t orelse father_is_sub s
|
||||
end
|
||||
|
||||
|
|
@ -104,6 +101,14 @@ val map_data = Data.map;
|
|||
val get_data_global = Data.get o Context.Theory;
|
||||
val map_data_global = Context.theory_map o map_data;
|
||||
|
||||
val default_cid = "text"
|
||||
|
||||
fun is_defined_cid_global cid thy = let val t = snd(get_data_global thy)
|
||||
in cid=default_cid orelse Symtab.defined t cid end
|
||||
|
||||
fun is_defined_cid_local cid ctxt = let val t = snd(get_data ctxt)
|
||||
in cid=default_cid orelse Symtab.defined t cid end
|
||||
|
||||
|
||||
fun is_declared_oid_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy)
|
||||
in Symtab.defined t oid end
|
||||
|
|
@ -127,54 +132,71 @@ fun is_defined_oid_local oid thy = let val {tab=t,maxano=_} = fst(get_data th
|
|||
|
||||
|
||||
fun declare_object_global oid thy = (map_data_global
|
||||
(H1(fn {tab=t,maxano=x} =>
|
||||
{tab=Symtab.update_new(oid,NONE)t,
|
||||
maxano=x}))
|
||||
(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_local oid ctxt = (map_data (H1(fn {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"))
|
||||
|
||||
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 hurx = {params=params',
|
||||
name = binding,
|
||||
thy_name = nn,
|
||||
id = serial(), (* 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 *)}
|
||||
in if is_defined_cid_global cid thy
|
||||
then error("multiple definition of document reference")
|
||||
else map_data_global(apsnd(Symtab.update(cid,hurx)))(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 (H1(fn {tab=t,maxano=x} =>
|
||||
{tab=Symtab.update(oid,SOME bbb) t,
|
||||
maxano=x}))
|
||||
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 (H1(fn {tab=t,maxano=x} =>
|
||||
{tab=Symtab.update(oid,SOME bbb) t,maxano=x})) ctxt
|
||||
map_data (apfst(fn {tab=t,maxano=x} =>
|
||||
{tab=Symtab.update(oid,SOME bbb) t,maxano=x})) ctxt
|
||||
|
||||
|
||||
(* declares an anonyme label of a given type and generates a unique reference ... *)
|
||||
fun declare_anoobject_global thy cid = map_data_global
|
||||
(H1(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))
|
||||
(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_local ctxt cid = map_data
|
||||
(H1(fn {tab=t,maxano=x} =>
|
||||
let val str = cid^":"^Int.toString(x+1)
|
||||
val _ = writeln("Anonymous doc-ref declared: "
|
||||
(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))
|
||||
in {tab=Symtab.update(str,NONE)t, maxano=x+1}
|
||||
end))
|
||||
(ctxt)
|
||||
|
||||
fun get_object_global oid thy = let val {tab=t,maxano=_} = fst(get_data_global thy)
|
||||
|
|
@ -198,8 +220,6 @@ end (* struct *)
|
|||
|
||||
section{* Syntax for Annotated Documentation Commands (the '' View'') *}
|
||||
|
||||
|
||||
|
||||
|
||||
ML{*
|
||||
structure DocAttrParser =
|
||||
|
|
@ -208,10 +228,12 @@ 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.optional (Parse.$$$ "::" |-- Parse.!!! Parse.name) "";
|
||||
Parse.position Parse.name
|
||||
-- Scan.optional (Parse.$$$ "::" |-- Parse.!!! Parse.name) DocObjTab.default_cid;
|
||||
|
||||
val attributes = (Parse.$$$ "[" |-- (reference --
|
||||
(Scan.optional(Parse.$$$ "," |-- (Parse.enum "," attribute))) []))
|
||||
|
|
@ -246,7 +268,7 @@ fun enriched_document_command markdown (((((oid,pos),dtyp),doc_attrs),xstring_op
|
|||
((((string * Position.T) * string) * 'a) * (xstring * Position.T) option) * Input.source
|
||||
-> Toplevel.transition -> Toplevel.transition
|
||||
*)
|
||||
fun enriched_document_command markdown (((((oid,pos),dtyp:string),doc_attrs),
|
||||
fun enriched_document_command markdown (((((oid,pos),cid:string),doc_attrs),
|
||||
xstring_opt:(xstring * Position.T) option),
|
||||
toks:Input.source) =
|
||||
let
|
||||
|
|
@ -255,8 +277,11 @@ fun enriched_document_command markdown (((((oid,pos),dtyp:string),doc_attrs),
|
|||
(* creates a markup label for this position and reports it to the PIDE framework;
|
||||
this label is used as jump-target for point-and-click feature. *)
|
||||
fun enrich_trans thy = let val name = Context.theory_name thy
|
||||
val _ = if not (DocObjTab.is_defined_cid_global cid thy)
|
||||
then error("class reference undefined")
|
||||
else ()
|
||||
in DocObjTab.define_object_global (oid, {pos=pos, thy_name=name,
|
||||
id=id , cid=dtyp})
|
||||
id=id , cid=cid})
|
||||
(thy)
|
||||
end
|
||||
fun MMM(SOME(s,p)) = SOME(s^"XXX",p)
|
||||
|
|
@ -383,22 +408,31 @@ fun read_parent NONE ctxt = (NONE, ctxt)
|
|||
Type (name, Ts) => (SOME (Ts, name), fold Variable.declare_typ Ts ctxt)
|
||||
| T => error ("Bad parent record specification: " ^ Syntax.string_of_typ ctxt T));
|
||||
|
||||
|
||||
fun map_option f 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 fields = map2 (fn (x, _, mx) => fn T => (x, T, mx)) raw_fields Ts;
|
||||
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, ctxt') end;
|
||||
in (fields, terms, ctxt') end;
|
||||
|
||||
fun add_record_cmd overloaded (raw_params, binding) raw_parent raw_fields thy =
|
||||
fun add_record_cmd overloaded (raw_params, binding) raw_parent raw_fieldsNdefaults rex 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, ctxt3) = read_fields raw_fields ctxt2;
|
||||
val (fields, terms, ctxt3) = read_fields raw_fieldsNdefaults ctxt2;
|
||||
val fieldsNterms = (map (fn (a,b,_) => (a,b)) fields) ~~ terms
|
||||
val fieldsNterms' = map (fn ((x,y),z) => (x,y,z)) fieldsNterms
|
||||
val params' = map (Proof_Context.check_tfree ctxt3) params;
|
||||
in thy |> Record.add_record overloaded (params', binding) parent fields end;
|
||||
in thy |> Record.add_record overloaded (params', binding) parent fields
|
||||
|> DocObjTab.define_doc_class_global (params', binding) parent fieldsNterms'
|
||||
end;
|
||||
|
||||
|
||||
val _ =
|
||||
|
|
@ -406,10 +440,18 @@ val _ =
|
|||
(Parse_Spec.overloaded
|
||||
-- (Parse.type_args_constrained -- Parse.binding)
|
||||
-- (@{keyword "="} |-- Scan.option (Parse.typ --| @{keyword "+"})
|
||||
-- Scan.repeat1 Parse.const_binding)
|
||||
-- Scan.option (@{keyword "where"} |-- Parse.term)
|
||||
>> (fn (((overloaded, x), (y, z)),_) =>
|
||||
Toplevel.theory (add_record_cmd {overloaded = overloaded} x y z)));
|
||||
-- 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)));
|
||||
|
||||
*}
|
||||
|
||||
ML{*
|
||||
Binding.print;
|
||||
Syntax.read_term;
|
||||
try;
|
||||
|
||||
|
||||
*}
|
||||
|
||||
|
|
|
|||
|
|
@ -1,5 +1,5 @@
|
|||
theory Example
|
||||
imports Isa_DOF
|
||||
imports Isa_DOF CENELEC_50126
|
||||
keywords "Term" :: diag
|
||||
begin
|
||||
|
||||
|
|
@ -13,26 +13,39 @@ declare_reference [blablabla::cid, alpha=beta, beta=gamma]
|
|||
|
||||
paragraph*[sdf]{* just a paragraph *}
|
||||
|
||||
subsection*[sdf]{* shouldn't work *}
|
||||
subsection*[sdf]{* shouldn't work, multiple ref. *}
|
||||
|
||||
section*[sedf::requirement]{* works again *}
|
||||
text\<open>\label{sedf}\<close> (* Hack to make the LaTeX-ing running. Should disappear. *)
|
||||
|
||||
section*[seedf::integration_test, dfg=34,fgdfg=zf]{* and another example with attribute setting *}
|
||||
section*[seedf::integration_test, dfg=34,fgdfg=zf]{* and another example with attribute setting,
|
||||
but wrong doc_class constraint. *}
|
||||
|
||||
section{* Text Antiquotation Infrastructure ... *}
|
||||
|
||||
text{* @{docref lalala} *}
|
||||
text{* @{docref \<open>lalala\<close>} -- produces warning. *}
|
||||
|
||||
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 !!! *)
|
||||
|
||||
|
||||
|
||||
text{* @{thm refl} @{file "MOF.sml"} @{value 3} @{const hd} @{theory List}}
|
||||
(* some show-off of standard anti-quotations: *)
|
||||
text{* @{thm refl} @{file "MOF.sml"} @{value "3+4"} @{const hd} @{theory List}}
|
||||
@{term "3"} @{type bool} @{term [show_types] "f x = a + x"} *}
|
||||
|
||||
text{* Here is a reference to @{docref sedf} *}
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
|
||||
section{* A Small Example for a Command Definition *}
|
||||
section{* A Small Example for a Command Definition --- just to see how this works in principle. *}
|
||||
|
||||
ML{*
|
||||
val opt_modes =
|
||||
|
|
|
|||
Loading…
Reference in New Issue