nicolas.meric
/
Isabelle_DOF
forked from Isabelle_DOF/Isabelle_DOF
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Revising Chapter 5.

This commit is contained in:
Achim D. Brucker 2021-02-13 17:04:17 +00:00
parent 018bfa4bcd
commit e495a7b2fe
1 changed files with 50 additions and 78 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

128
examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy
View File

@ -1,7 +1,7 @@
(************************************************************************* (*************************************************************************
* Copyright (C) * Copyright (C)
* 2019-2020 University of Exeter * 2019-2021 University of Exeter
* 2018-2019 University of Paris-Saclay * 2018-2021 University of Paris-Saclay
* 2018 The University of Sheffield * 2018 The University of Sheffield
* *
* License: * License:
@ -41,74 +41,55 @@ text\<open>
IDE support. IDE support.
\<close> \<close>
(* should work as text*, but doesn't. *) section\<open>\<^isadof>: A User-Defined Plugin in Isabelle/Isar\<close>
(* text\<open>
text*[xxx::SML] A plugin in Isabelle starts with defining the local data and registering it in the framework. As
mentioned before, contexts are structures with independent cells/compartments having three
primitives \<^boxed_sml>\<open>init\<close>, \<^boxed_sml>\<open>extend\<close> and \<^boxed_sml>\<open>merge\<close>. Technically this is done by
instantiating a functor \<^boxed_sml>\<open>Generic_Data\<close>, and the following fairly typical code-fragment
is drawn from \<^isadof>:
@{boxed_sml [display]
\<open>structure Data = Generic_Data \<open>structure Data = Generic_Data
( type T = docobj_tab * docclass_tab * ... ( type T = docobj_tab * docclass_tab * ...
val empty = (initial_docobj_tab, initial_docclass_tab, ...) val empty = (initial_docobj_tab, initial_docclass_tab, ...)
val extend = I val extend = I
fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...), fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...),
merge_docclass_tab(c1,c2,...)) merge_docclass_tab(c1,c2,...))
); );\<close>}
\<close> where the table \<^boxed_sml>\<open>docobj_tab\<close> manages document classes and \<^boxed_sml>\<open>docclass_tab\<close> the
*)
section\<open>\<^isadof>: A User-Defined Plugin in Isabelle/Isar\<close>
text\<open>
A plugin in Isabelle starts with defining the local data and registering it in the framework. As
mentioned before, contexts are structures with independent cells/compartments having three
primitives \inlinesml+init+, \inlinesml+extend+ and \inlinesml+merge+. Technically this is done by
instantiating a functor \inlinesml+Generic_Data+, and the following fairly typical code-fragment
is drawn from \<^isadof>:
\begin{sml}
structure Data = Generic_Data
( type T = docobj_tab * docclass_tab * ...
val empty = (initial_docobj_tab, initial_docclass_tab, ...)
val extend = I
fun merge((d1,c1,...),(d2,c2,...)) = (merge_docobj_tab (d1,d2,...),
merge_docclass_tab(c1,c2,...))
);
\end{sml}
where the table \inlinesml+docobj_tab+ manages document classes and \inlinesml+docclass_tab+ the
environment for class definitions (inducing the inheritance relation). Other tables capture, \eg, environment for class definitions (inducing the inheritance relation). Other tables capture, \eg,
the class invariants, inner-syntax antiquotations. Operations follow the MVC-pattern, where the class invariants, inner-syntax antiquotations. Operations follow the MVC-pattern, where
Isabelle/Isar provides the controller part. A typical model operation has the type: Isabelle/Isar provides the controller part. A typical model operation has the type:
\begin{sml} @{boxed_sml [display]
val opn :: <args_type> -> Context.generic -> Context.generic \<open>val opn :: <args_type> -> Context.generic -> Context.generic\<close>}
\end{sml}
representing a transformation on system contexts. For example, the operation of declaring a local representing a transformation on system contexts. For example, the operation of declaring a local
reference in the context is presented as follows: reference in the context is presented as follows:
\begin{sml} @{boxed_sml [display]
fun declare_object_local oid ctxt = \<open>fun declare_object_local oid ctxt =
let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab, let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab,
maxano=maxano} maxano=maxano}
in (Data.map(apfst decl)(ctxt) in (Data.map(apfst decl)(ctxt)
handle Symtab.DUP _ => handle Symtab.DUP _ =>
error("multiple declaration of document reference")) error("multiple declaration of document reference"))
end end\<close>}
\end{sml}
where \<^boxed_theory_text>\<open>Data.map\<close> is the update function resulting from the instantiation of the where \<^boxed_theory_text>\<open>Data.map\<close> is the update function resulting from the instantiation of the
functor \inlinesml|Generic_Data|. This code fragment uses operations from a library structure functor \<^boxed_sml>\<open>Generic_Data\<close>. This code fragment uses operations from a library structure
\inlinesml+Symtab+ that were used to update the appropriate table for document objects in \<^boxed_sml>\<open>Symtab\<close> that were used to update the appropriate table for document objects in
the plugin-local state. Possible exceptions to the update operation were mapped to a system-global the plugin-local state. Possible exceptions to the update operation were mapped to a system-global
error reporting function. error reporting function.
Finally, the view-aspects were handled by an API for parsing-combinators. The library structure Finally, the view-aspects were handled by an API for parsing-combinators. The library structure
\inlinesml+Scan+ provides the operators: \<^boxed_sml>\<open>Scan\<close> provides the operators:
\begin{sml} @{boxed_sml [display]
op || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b \<open>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 -> ('b * 'd) * 'e
op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c
op option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a op option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a
op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a \<close>}
\end{sml}
for alternative, sequence, and piping, as well as combinators for option and repeat. Parsing for alternative, sequence, and piping, as well as combinators for option and repeat. Parsing
combinators have the advantage that they can be smoothlessly integrated into standard programs, combinators have the advantage that they can be smoothlessly integrated into standard programs,
and they enable the dynamic extension of the grammar. There is a more high-level structure and they enable the dynamic extension of the grammar. There is a more high-level structure
@ -128,13 +109,12 @@ val attributes =(Parse.$$$ "[" |-- (reference
The ``model'' \<^boxed_theory_text>\<open>declare_reference_opn\<close> and ``new'' \<^boxed_theory_text>\<open>attributes\<close> parts were The ``model'' \<^boxed_theory_text>\<open>declare_reference_opn\<close> and ``new'' \<^boxed_theory_text>\<open>attributes\<close> parts were
combined via the piping operator and registered in the Isar toplevel: combined via the piping operator and registered in the Isar toplevel:
\begin{sml} @{boxed_sml [display]
fun declare_reference_opn (((oid,_),_),_) = \<open>fun declare_reference_opn (((oid,_),_),_) =
(Toplevel.theory (DOF_core.declare_object_global oid)) (Toplevel.theory (DOF_core.declare_object_global oid))
val _ = Outer_Syntax.command <@>{command_keyword "declare_reference"} val _ = Outer_Syntax.command <@>{command_keyword "declare_reference"}
"declare document reference" "declare document reference"
(attributes >> declare_reference_opn); (attributes >> declare_reference_opn);\<close>}
\end{sml}
Altogether, this gives the extension of Isabelle/HOL with Isar syntax and semantics for the Altogether, this gives the extension of Isabelle/HOL with Isar syntax and semantics for the
new \emph{command}: new \emph{command}:
@ -154,14 +134,13 @@ text\<open>
principle: based on a number of combinators, new user-defined antiquotation syntax and semantics principle: based on a number of combinators, new user-defined antiquotation syntax and semantics
can be added to the system that works on the internal plugin-data freely. For example, in can be added to the system that works on the internal plugin-data freely. For example, in
\begin{sml} @{boxed_sml [display]
val _ = Theory.setup( \<open>val _ = Theory.setup(
Thy_Output.antiquotation <@>{binding docitem} Thy_Output.antiquotation <@>{binding docitem}
docitem_antiq_parser docitem_antiq_parser
(docitem_antiq_gen default_cid) #> (docitem_antiq_gen default_cid) #>
ML_Antiquotation.inline <@>{binding docitem_value} ML_Antiquotation.inline <@>{binding docitem_value}
ML_antiq_docitem_value) ML_antiq_docitem_value)\<close>}
\end{sml}
the text antiquotation \<^boxed_theory_text>\<open>docitem\<close> is declared and bounded to a parser for the argument the text antiquotation \<^boxed_theory_text>\<open>docitem\<close> is declared and bounded to a parser for the argument
syntax and the overall semantics. This code defines a generic antiquotation to be used in text syntax and the overall semantics. This code defines a generic antiquotation to be used in text
elements such as elements such as
@ -188,9 +167,8 @@ text\<open>
late-binding table \<^boxed_theory_text>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation late-binding table \<^boxed_theory_text>\<open>ISA_transformer_tab\<close>, we register for each inner-syntax-annotation
(ISA's), a function of type (ISA's), a function of type
\begin{sml} @{boxed_sml [display]
theory -> term * typ * Position.T -> term option \<open> theory -> term * typ * Position.T -> term option\<close>}
\end{sml}
Executed in a second pass of term parsing, ISA's may just return \<^boxed_theory_text>\<open>None\<close>. This is Executed in a second pass of term parsing, ISA's may just return \<^boxed_theory_text>\<open>None\<close>. This is
adequate for ISA's just performing some checking in the logical context \<^boxed_theory_text>\<open>theory\<close>; adequate for ISA's just performing some checking in the logical context \<^boxed_theory_text>\<open>theory\<close>;
@ -205,8 +183,8 @@ text\<open>
For the moment, there is no high-level syntax for the definition of class invariants. A For the moment, there is no high-level syntax for the definition of class invariants. A
formulation, in SML, of the first class-invariant in @{docitem "sec:class_inv"} is straight-forward: formulation, in SML, of the first class-invariant in @{docitem "sec:class_inv"} is straight-forward:
\begin{sml} @{boxed_sml [display]
fun check_result_inv oid {is_monitor:bool} ctxt = \<open>fun check_result_inv oid {is_monitor:bool} ctxt =
let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here} let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here}
val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here} val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here}
val tS = HOLogic.dest_list prop val tS = HOLogic.dest_list prop
@ -216,10 +194,9 @@ fun check_result_inv oid {is_monitor:bool} ctxt =
| _ => false | _ => false
end end
val _ = Theory.setup (DOF_core.update_class_invariant val _ = Theory.setup (DOF_core.update_class_invariant
"tiny_cert.result" check_result_inv) "tiny_cert.result" check_result_inv)\<close>}
\end{sml}
The \inlinesml{setup}-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function The \<^boxed_sml>\<open>setup\<close>-command (last line) registers the \<^boxed_theory_text>\<open>check_result_inv\<close> function
into the \<^isadof> kernel, which activates any creation or modification of an instance of into the \<^isadof> kernel, which activates any creation or modification of an instance of
\<^boxed_theory_text>\<open>result\<close>. We cannot replace \<^boxed_theory_text>\<open>compute_attr_access\<close> by the corresponding \<^boxed_theory_text>\<open>result\<close>. We cannot replace \<^boxed_theory_text>\<open>compute_attr_access\<close> by the corresponding
antiquotation \<^boxed_theory_text>\<open>@{docitem_value kind::oid}\<close>, since \<^boxed_theory_text>\<open>oid\<close> is antiquotation \<^boxed_theory_text>\<open>@{docitem_value kind::oid}\<close>, since \<^boxed_theory_text>\<open>oid\<close> is
@ -232,10 +209,9 @@ text\<open>
deterministic automata. These are stored in the \<^boxed_theory_text>\<open>docobj_tab\<close> for monitor-objects deterministic automata. These are stored in the \<^boxed_theory_text>\<open>docobj_tab\<close> for monitor-objects
in the \<^isadof> component. We implemented the functions: in the \<^isadof> component. We implemented the functions:
\begin{sml} @{boxed_sml [display]
val enabled : automaton -> env -> cid list \<open> val enabled : automaton -> env -> cid list
val next : automaton -> env -> cid -> automaton val next : automaton -> env -> cid -> automaton\<close>}
\end{sml}
where \<^boxed_theory_text>\<open>env\<close> is basically a map between internal automaton states and class-id's where \<^boxed_theory_text>\<open>env\<close> is basically a map between internal automaton states and class-id's
(\<^boxed_theory_text>\<open>cid\<close>'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id, (\<^boxed_theory_text>\<open>cid\<close>'s). An automaton is said to be \<^emph>\<open>enabled\<close> for a class-id,
iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During
@ -252,41 +228,38 @@ text\<open>
``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \LaTeX-commands ``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \LaTeX-commands
are just wrappers for the corresponding commands from the keycommand package: are just wrappers for the corresponding commands from the keycommand package:
\begin{ltx} @{boxed_latex [display]
\newcommand\newisadof[1]{% \<open>\newcommand\newisadof[1]{%
\expandafter\newkeycommand\csname isaDof.#1\endcsname}% \expandafter\newkeycommand\csname isaDof.#1\endcsname}%
\newcommand\renewisadof[1]{% \newcommand\renewisadof[1]{%
\expandafter\renewkeycommand\csname isaDof.#1\endcsname}% \expandafter\renewkeycommand\csname isaDof.#1\endcsname}%
\newcommand\provideisadof[1]{% \newcommand\provideisadof[1]{%
\expandafter\providekeycommand\csname isaDof.#1\endcsname}% \expandafter\providekeycommand\csname isaDof.#1\endcsname}%\<close>}
\end{ltx}
The \LaTeX-generator of \<^isadof> maps each \<^boxed_theory_text>\<open>doc_item\<close> to an \LaTeX-environment (recall The \LaTeX-generator of \<^isadof> maps each \<^boxed_theory_text>\<open>doc_item\<close> to an \LaTeX-environment (recall
@{docitem "text-elements"}). As generic \<^boxed_theory_text>\<open>doc_item\<close> are derived from the text element, @{docitem "text-elements"}). As generic \<^boxed_theory_text>\<open>doc_item\<close> are derived from the text element,
the enviornment \inlineltx|{isamarkuptext*}| builds the core of \<^isadof>'s \LaTeX{} implementation. the enviornment \inlineltx|{isamarkuptext*}| builds the core of \<^isadof>'s \LaTeX{} implementation.
For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to
\begin{ltx} @{boxed_latex [display]
\begin{isamarkuptext*}% \<open>\begin{isamarkuptext*}%
[label = {ass122},type = {CENELEC_50128.SRAC}, [label = {ass122},type = {CENELEC_50128.SRAC},
args={label = {ass122}, type = {CENELEC_50128.SRAC}, args={label = {ass122}, type = {CENELEC_50128.SRAC},
CENELEC_50128.EC.assumption_kind = {formal}} CENELEC_50128.EC.assumption_kind = {formal}}
] The overall sampling frequence of the odometer subsystem is therefore ] The overall sampling frequence of the odometer subsystem is therefore
14 khz, which includes sampling, computing and result communication 14 khz, which includes sampling, computing and result communication
times ... times ...
\end{isamarkuptext*} \end{isamarkuptext*}\<close>}
\end{ltx}
This environment is mapped to a plain \LaTeX command via (again, recall @{docitem "text-elements"}): This environment is mapped to a plain \LaTeX command via (again, recall @{docitem "text-elements"}):
\begin{ltx} @{boxed_latex [display]
\NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} \<open> \NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} \<close>}
\end{ltx}
For the command-based setup, \<^isadof> provides a dispatcher that selects the most specific For the command-based setup, \<^isadof> provides a dispatcher that selects the most specific
implementation for a given \<^boxed_theory_text>\<open>doc_class\<close>: implementation for a given \<^boxed_theory_text>\<open>doc_class\<close>:
\begin{ltx} @{boxed_latex [display]
%% The Isabelle/DOF dispatcher: \<open>%% The Isabelle/DOF dispatcher:
\newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{% \newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{%
\ifcsname isaDof.\commandkey{type}\endcsname% \ifcsname isaDof.\commandkey{type}\endcsname%
\csname isaDof.\commandkey{type}\endcsname% \csname isaDof.\commandkey{type}\endcsname%
@ -307,8 +280,7 @@ implementation for a given \<^boxed_theory_text>\<open>doc_class\<close>:
definition for "\commandkey{env}" available either.}% definition for "\commandkey{env}" available either.}%
\fi% \fi%
\fi% \fi%
} }\<close>}
\end{ltx}
\<close> \<close>
(*<*) (*<*)