From e495a7b2fe92955e5d46c180dfb334c132f5b251 Mon Sep 17 00:00:00 2001 From: "Achim D. Brucker" Date: Sat, 13 Feb 2021 17:04:17 +0000 Subject: [PATCH] Revising Chapter 5. --- .../Isabelle_DOF-Manual/05_Implementation.thy | 128 +++++++----------- 1 file changed, 50 insertions(+), 78 deletions(-) diff --git a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy index 4377317..14150b3 100755 --- a/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy +++ b/examples/technical_report/Isabelle_DOF-Manual/05_Implementation.thy @@ -1,7 +1,7 @@ (************************************************************************* * Copyright (C) - * 2019-2020 University of Exeter - * 2018-2019 University of Paris-Saclay + * 2019-2021 University of Exeter + * 2018-2021 University of Paris-Saclay * 2018 The University of Sheffield * * License: @@ -41,74 +41,55 @@ text\ IDE support. \ -(* should work as text*, but doesn't. *) -(* -text*[xxx::SML] +section\\<^isadof>: A User-Defined Plugin in Isabelle/Isar\ +text\ + 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>\init\, \<^boxed_sml>\extend\ and \<^boxed_sml>\merge\. Technically this is done by + instantiating a functor \<^boxed_sml>\Generic_Data\, and the following fairly typical code-fragment + is drawn from \<^isadof>: + +@{boxed_sml [display] \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,...)) -); -\ -*) - - - -section\\<^isadof>: A User-Defined Plugin in Isabelle/Isar\ -text\ - 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 +);\} + where the table \<^boxed_sml>\docobj_tab\ manages document classes and \<^boxed_sml>\docclass_tab\ the environment for class definitions (inducing the inheritance relation). Other tables capture, \eg, 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: -\begin{sml} -val opn :: -> Context.generic -> Context.generic -\end{sml} +@{boxed_sml [display] +\val opn :: -> Context.generic -> Context.generic\} representing a transformation on system contexts. For example, the operation of declaring a local reference in the context is presented as follows: -\begin{sml} -fun declare_object_local oid ctxt = +@{boxed_sml [display] +\fun declare_object_local oid ctxt = let fun decl {tab,maxano} = {tab=Symtab.update_new(oid,NONE) tab, maxano=maxano} in (Data.map(apfst decl)(ctxt) handle Symtab.DUP _ => error("multiple declaration of document reference")) -end -\end{sml} +end\} where \<^boxed_theory_text>\Data.map\ is the update function resulting from the instantiation of the - functor \inlinesml|Generic_Data|. This code fragment uses operations from a library structure - \inlinesml+Symtab+ that were used to update the appropriate table for document objects in + functor \<^boxed_sml>\Generic_Data\. This code fragment uses operations from a library structure + \<^boxed_sml>\Symtab\ 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 error reporting function. Finally, the view-aspects were handled by an API for parsing-combinators. The library structure - \inlinesml+Scan+ provides the operators: + \<^boxed_sml>\Scan\ provides the operators: -\begin{sml} -op || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b +@{boxed_sml [display] +\op || : ('a -> 'b) * ('a -> 'b) -> 'a -> 'b op -- : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> ('b * 'd) * 'e op >> : ('a -> 'b * 'c) * ('b -> 'd) -> 'a -> 'd * 'c op option : ('a -> 'b * 'a) -> 'a -> 'b option * 'a -op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a -\end{sml} +op repeat : ('a -> 'b * 'a) -> 'a -> 'b list * 'a \} 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, 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>\declare_reference_opn\ and ``new'' \<^boxed_theory_text>\attributes\ parts were combined via the piping operator and registered in the Isar toplevel: -\begin{sml} - fun declare_reference_opn (((oid,_),_),_) = +@{boxed_sml [display] +\fun declare_reference_opn (((oid,_),_),_) = (Toplevel.theory (DOF_core.declare_object_global oid)) val _ = Outer_Syntax.command <@>{command_keyword "declare_reference"} "declare document reference" - (attributes >> declare_reference_opn); -\end{sml} + (attributes >> declare_reference_opn);\} Altogether, this gives the extension of Isabelle/HOL with Isar syntax and semantics for the new \emph{command}: @@ -154,14 +134,13 @@ text\ 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 -\begin{sml} -val _ = Theory.setup( +@{boxed_sml [display] +\val _ = Theory.setup( Thy_Output.antiquotation <@>{binding docitem} docitem_antiq_parser (docitem_antiq_gen default_cid) #> ML_Antiquotation.inline <@>{binding docitem_value} - ML_antiq_docitem_value) -\end{sml} + ML_antiq_docitem_value)\} the text antiquotation \<^boxed_theory_text>\docitem\ 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 elements such as @@ -188,9 +167,8 @@ text\ late-binding table \<^boxed_theory_text>\ISA_transformer_tab\, we register for each inner-syntax-annotation (ISA's), a function of type -\begin{sml} - theory -> term * typ * Position.T -> term option -\end{sml} +@{boxed_sml [display] +\ theory -> term * typ * Position.T -> term option\} Executed in a second pass of term parsing, ISA's may just return \<^boxed_theory_text>\None\. This is adequate for ISA's just performing some checking in the logical context \<^boxed_theory_text>\theory\; @@ -205,8 +183,8 @@ text\ 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: -\begin{sml} -fun check_result_inv oid {is_monitor:bool} ctxt = +@{boxed_sml [display] +\fun check_result_inv oid {is_monitor:bool} ctxt = let val kind = compute_attr_access ctxt "kind" oid <@>{here} <@>{here} val prop = compute_attr_access ctxt "property" oid <@>{here} <@>{here} val tS = HOLogic.dest_list prop @@ -216,10 +194,9 @@ fun check_result_inv oid {is_monitor:bool} ctxt = | _ => false end val _ = Theory.setup (DOF_core.update_class_invariant - "tiny_cert.result" check_result_inv) -\end{sml} + "tiny_cert.result" check_result_inv)\} - The \inlinesml{setup}-command (last line) registers the \<^boxed_theory_text>\check_result_inv\ function + The \<^boxed_sml>\setup\-command (last line) registers the \<^boxed_theory_text>\check_result_inv\ function into the \<^isadof> kernel, which activates any creation or modification of an instance of \<^boxed_theory_text>\result\. We cannot replace \<^boxed_theory_text>\compute_attr_access\ by the corresponding antiquotation \<^boxed_theory_text>\@{docitem_value kind::oid}\, since \<^boxed_theory_text>\oid\ is @@ -232,10 +209,9 @@ text\ deterministic automata. These are stored in the \<^boxed_theory_text>\docobj_tab\ for monitor-objects in the \<^isadof> component. We implemented the functions: -\begin{sml} - val enabled : automaton -> env -> cid list - val next : automaton -> env -> cid -> automaton -\end{sml} +@{boxed_sml [display] +\ val enabled : automaton -> env -> cid list + val next : automaton -> env -> cid -> automaton\} where \<^boxed_theory_text>\env\ is basically a map between internal automaton states and class-id's (\<^boxed_theory_text>\cid\'s). An automaton is said to be \<^emph>\enabled\ for a class-id, iff it either occurs in its accept-set or its reject-set (see @{docitem "sec:monitors"}). During @@ -252,41 +228,38 @@ text\ ``keycommand''~@{cite "chervet:keycommand:2010"} package. In fact, the core \<^isadof> \LaTeX-commands are just wrappers for the corresponding commands from the keycommand package: -\begin{ltx} -\newcommand\newisadof[1]{% +@{boxed_latex [display] +\\newcommand\newisadof[1]{% \expandafter\newkeycommand\csname isaDof.#1\endcsname}% \newcommand\renewisadof[1]{% \expandafter\renewkeycommand\csname isaDof.#1\endcsname}% \newcommand\provideisadof[1]{% - \expandafter\providekeycommand\csname isaDof.#1\endcsname}% -\end{ltx} + \expandafter\providekeycommand\csname isaDof.#1\endcsname}%\} The \LaTeX-generator of \<^isadof> maps each \<^boxed_theory_text>\doc_item\ to an \LaTeX-environment (recall @{docitem "text-elements"}). As generic \<^boxed_theory_text>\doc_item\ are derived from the text element, the enviornment \inlineltx|{isamarkuptext*}| builds the core of \<^isadof>'s \LaTeX{} implementation. For example, the @{docitem "ass123"} from page \pageref{ass123} is mapped to -\begin{ltx} -\begin{isamarkuptext*}% +@{boxed_latex [display] +\\begin{isamarkuptext*}% [label = {ass122},type = {CENELEC_50128.SRAC}, args={label = {ass122}, type = {CENELEC_50128.SRAC}, CENELEC_50128.EC.assumption_kind = {formal}} ] The overall sampling frequence of the odometer subsystem is therefore 14 khz, which includes sampling, computing and result communication times ... -\end{isamarkuptext*} -\end{ltx} +\end{isamarkuptext*}\} This environment is mapped to a plain \LaTeX command via (again, recall @{docitem "text-elements"}): -\begin{ltx} - \NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} -\end{ltx} +@{boxed_latex [display] +\ \NewEnviron{isamarkuptext*}[1][]{\isaDof[env={text},#1]{\BODY}} \} For the command-based setup, \<^isadof> provides a dispatcher that selects the most specific implementation for a given \<^boxed_theory_text>\doc_class\: -\begin{ltx} -%% The Isabelle/DOF dispatcher: +@{boxed_latex [display] +\%% The Isabelle/DOF dispatcher: \newkeycommand+[\|]\isaDof[env={UNKNOWN},label=,type={dummyT},args={}][1]{% \ifcsname isaDof.\commandkey{type}\endcsname% \csname isaDof.\commandkey{type}\endcsname% @@ -307,8 +280,7 @@ implementation for a given \<^boxed_theory_text>\doc_class\: definition for "\commandkey{env}" available either.}% \fi% \fi% -} -\end{ltx} +}\} \ (*<*)