From 7007edf080c9f07ee8ea966d9991c1afd0dfd4de Mon Sep 17 00:00:00 2001
From: Thibault Martin <thi.martin.pro@pm.me>
Date: Mon, 23 Sep 2024 17:30:28 +0200
Subject: [PATCH] [doc] Uniform naming for loaders/module importers
---
doc/developer/advance.tex | 36 +++++++++++++++++++-----------------
doc/userman/user-acsl.tex | 35 ++++++++++++++++++-----------------
2 files changed, 37 insertions(+), 34 deletions(-)
diff --git a/doc/developer/advance.tex b/doc/developer/advance.tex
index 550af9e271..a8193c6c6e 100644
--- a/doc/developer/advance.tex
+++ b/doc/developer/advance.tex
@@ -4126,18 +4126,19 @@ version in the interface:
\paragraph{External Modules.}
\label{par:ext-modules}
-Finally, let us introduce how to extend \acsl
-modules with external module importers. A typical usage is to import logical
-definitions from other languages, e.g. \textsf{Coq} or \textsf{Why3}, as regular
-\acsl module definitions. From the user point the view, this takes the form
-of an extended \verb+import+ clause:
+Finally, let us introduce how to extend \acsl modules with external module
+importers. A typical usage is to import logical definitions from other
+languages, e.g. \textsf{Coq} or \textsf{Why3}, as regular \acsl module
+definitions. From the user point the view, this takes the form of an extended
+\verb+import+ clause:
\begin{lstlisting}
//@ import <loader>: <module-name> [ \as <alias-name> ];
\end{lstlisting}
-The syntax is similar to the general ACSL \verb+import+ annotation, except that the
-module name is prefixed with the name of the loader extension. For instance:
+The syntax is similar to the general ACSL \verb+import+ annotation, except that
+the module name is prefixed with a loader corresponding to the name used when
+registering the module importer extension. For instance:
\begin{lstlisting}[style=c]
//@ import Foo: foo::bar::Jazz ;
@@ -4149,17 +4150,17 @@ to be imported.
To define such an external module loader, a plug-in shall call the
\scodeidxdef{Acsl\_extension}{register\_module\_importer}
-\verb+Acsl_extension.register_module_importer+ with a suitable loader function.
-The loader function is responsible for resolving the module name and defining
-the associated \acsl logic types, functions and predicates. Here is an example
-of such a loader function:
+\verb+Acsl_extension.register_module_importer+ with a suitable importer
+function. The importer function is responsible for resolving the module name and
+defining the associated \acsl logic types, functions and predicates. Here is an
+example of such a importer function:
\scodeidx{Logic\_typing}{module\_builder}
\begin{lstlisting}[language=OCaml]
open Cil_types
open Logic_typing
-let loader (ctxt: module_builder) (loc: location) (path: string list) =
+let importer (ctxt: module_builder) (loc: location) (path: string list) =
begin
(* in the example above, path is ["foo","bar","Jazz"] *)
(* ... read some file .. *)
@@ -4174,7 +4175,7 @@ let loader (ctxt: module_builder) (loc: location) (path: string list) =
(* ... *)
end
-let () = Acsl_extension.register_module_importer "Foo" loader
+let () = Acsl_extension.register_module_importer "Foo" importer
\end{lstlisting}
Added types and functions shall use local names, as in the example above.
@@ -4184,14 +4185,15 @@ in the example above.
As explained in the \framac source documentation, module importers might be
invoked multiple times by the kernel, e.g. when a given module is imported from
-different source files. Although the loader itself can use memoization
-techniques to save time, the module builder shall be populated on every call.
+different source files. Although the importer function itself can use
+memoization techniques to save time, the module builder shall be populated on
+every call.
When printing the internal AST from \framac command line using \verb+-print+
option, externally imported modules are listed with one single clause for each,
with no aliasing in order to avoid any ambiguity. For instance:
\begin{ccode}
-//@ import MyLoader: foo::bar::Jazz \as _ ;
+//@ import Foo: foo::bar::Jazz \as _ ;
\end{ccode}
Alternatively, you can debug the logical definitions actually imported by any
@@ -4204,7 +4206,7 @@ key:
With this option, the contents of the imported modules are printed like regular
module definitions, with only a comment to mention the origin of the plug-in:
\begin{ccode}
-/*@ // import MyLoader:
+/*@ // import Foo:
module foo::bar::Jazz {
...
}
diff --git a/doc/userman/user-acsl.tex b/doc/userman/user-acsl.tex
index 871d7c0d7f..725b1bf293 100644
--- a/doc/userman/user-acsl.tex
+++ b/doc/userman/user-acsl.tex
@@ -42,8 +42,8 @@ a sub-module \verb+B+ will actually defines the module \verb+A::B+, and so on.
Notice than for long identifiers like \verb+A::B::C+ to be valid, no space is
allowed around the \verb+:+ characters, and \verb+A+, \verb+B+, \verb+C+ must be
-regular \acsl identifiers, i.e.~they shall only consist of upper case or lower case letters, digits,
-underscores, and must start with a letter.
+regular \acsl identifiers, i.e.~they shall only consist of upper case or lower
+case letters, digits, underscores, and must start with a letter.
Inside module \verb+M+ declaration, where \verb+M+ it the long identifier of the
module being declared, a logic declaration \verb+a+ will actually define the
@@ -53,20 +53,21 @@ is also possible to use shortened names instead.
The rules for shortening long identifiers generalize to any depth of nested
modules. We only illustrate them in a simple case. Consider for instance a logic
-declaration \verb+a+ in module \verb+A::B+, depending on the context, it is possible to shorten
-its name as follows:
+declaration \verb+a+ in module \verb+A::B+, depending on the context, it is
+possible to shorten its name as follows:
\begin{itemize}
\item Everywhere, you can use \verb+A::B::a+;
\item Inside module \verb+A+, you can use \verb+B::a+;
\item Inside module \verb+A::B+, you can use \verb+a+;
-\item After annotation \lstinline[language=ACSL]|import A::B|, you can use \verb+B::a+;
-\item After annotation \lstinline[language=ACSL]|import A::B as C|, you can use \verb+C::a+;
+\item After annotation \lstinline[language=ACSL]|import A::B|, you can use
+ \verb+B::a+;
+\item After annotation \lstinline[language=ACSL]|import A::B as C|, you can use
+ \verb+C::a+;
\end{itemize}
You may also use local \lstinline[language=ACSL]+import+ annotations inside
-module definitions, in
-which case the introduced aliases will be only valid until the end of the module
-scope.
+module definitions, in which case the introduced aliases will be only valid
+until the end of the module scope.
Depending on dedicated plug-in support, you may also import modules definitions
from external specifications, generally from an external proof assistant like
@@ -74,22 +75,22 @@ from external specifications, generally from an external proof assistant like
specifications is as follows:
\begin{lstlisting}[language=ACSL]
-import <Driver>: <ModuleName> [ as <Name> ];
+import <Loader>: <ModuleName> [ as <Name> ];
\end{lstlisting}
This is a generalization of the regular \acsl \lstinline[language=ACSL]|import|
-clause just mentioned above. The \verb+<Driver>+ name identifies the kind of external
-specifications to be loaded. Drivers are defined by dedicated plug-in support
-only, and you shall consult the documentation of each plug-in to known which
-drivers are available.
+clause just mentioned above. The \verb+<Loader>+ name identifies the kind of
+external specifications to be loaded. Loaders are defined by dedicated plug-in
+support only, and you shall consult the documentation of each plug-in to known
+which loaders are available.
The \verb+<ModuleName>+ identifies both the name of the imported module and the
-external specification to be imported, with a \verb+<Driver>+ dependent meaning.
+external specification to be imported, with a \verb+<Loader>+ dependent meaning.
The alias name \verb+<Name>+, if provided, has the same meaning than when
importing regular module names (just described above) in the current scope.
-When importing \emph{external} specifications, depending on the \verb+<Driver>+
+When importing \emph{external} specifications, depending on the \verb+<Loader>+
used, it is possible to have logic identifiers with an extended lexical format:
\begin{itemize}
\item \verb+M::(op)+ where \verb+M+ is a regular module identifier, and
@@ -102,7 +103,7 @@ used, it is possible to have logic identifiers with an extended lexical format:
For instance, \verb+Foo::bar'jazz+ is a syntactically valid identifier.
\end{itemize}
-There is currently no support for external specification drivers from the
+There is currently no support for external specification loaders from the
standard distribution of \FramaC, although external plug-ins might define some
using the extension API, consult the plug-in developer manual for details.
--
GitLab