Merge branch 'master' of logicalhacking.com:HOL-OCL/Isabelle_DOF
This commit is contained in:
commit
5503dafbce
|
@ -0,0 +1,189 @@
|
||||||
|
(*<*)
|
||||||
|
theory "04_IsaDofImpl"
|
||||||
|
imports "02_Background"
|
||||||
|
begin
|
||||||
|
(*>*)
|
||||||
|
|
||||||
|
|
||||||
|
chapter*[impl1::introduction,main_author="Some(@{docitem ''adb''}::author)"]
|
||||||
|
\<open>Isabelle Ontology Framework \isadof\<close>
|
||||||
|
text\<open>
|
||||||
|
In this section, we introduce our framework, called \isadof. \isadof
|
||||||
|
is based on several design-decisions:
|
||||||
|
\begin{compactitem}
|
||||||
|
\item the entire \isadof is conceived as ``pure add-on'', \ie, we
|
||||||
|
deliberately resign on the possibility to modify Isabelle itself
|
||||||
|
(thus accepting a minor loss in performance and some additional
|
||||||
|
complexity in the documentation generation process)
|
||||||
|
\item we decided to identify the ontology types with the Isabelle/HOL
|
||||||
|
type system, \ie, we reuse the same infrastructure for parsers and
|
||||||
|
type-checkers, but use the types on the meta-level of the document
|
||||||
|
structure
|
||||||
|
\item we decided to make the markup-generation by own means in order
|
||||||
|
to adapt it as good as possible to the needs of tracking the linking
|
||||||
|
in documents.
|
||||||
|
\end{compactitem}
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
|
||||||
|
subsection*["sec:plugins"::technical]{*Writing \isadof as User-Defined Plugin in Isabelle/Isar*}
|
||||||
|
text\<open>
|
||||||
|
Writing an own 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 already 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}
|
||||||
|
with some tables \inlinesml+docobj_tab+ and \inlinesml+docclass_tab+
|
||||||
|
(not explained here) capturing the specific data of the application in
|
||||||
|
mind, \ie, a table of document classes and another one capturing the
|
||||||
|
document class instances.
|
||||||
|
\enlargethispage{2\baselineskip}
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
All the text samples shown here have to be in the context of an SML
|
||||||
|
file or in an \inlineisar|ML{* ... *}| command inside a \verb|.thy|
|
||||||
|
file, which has the effect to type-check and compile these text
|
||||||
|
elements by the underlying SML compiler.
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
Operations are organized in a model-view-controller scheme, where
|
||||||
|
Isabelle/Isar provides the controller part. A typical model operation
|
||||||
|
has the type:\<close>
|
||||||
|
text\<open>
|
||||||
|
\begin{sml}
|
||||||
|
val opn :: <args_type> -> Context.generic -> Context.generic
|
||||||
|
\end{sml}
|
||||||
|
\ie, it represents a transformation on 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 =
|
||||||
|
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}
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
where \inlineisar+Data.map+ is the update function resulting from the
|
||||||
|
above functor instantiation. This code fragment uses operations from
|
||||||
|
a library structure \inlinesml+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.
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
Finally, the view-aspects where handled by an API for
|
||||||
|
parsing-combinators. The library structure \inlinesml+Scan+ provides,
|
||||||
|
for example, the operators:
|
||||||
|
\begin{sml}
|
||||||
|
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 -> 'd * 'e
|
||||||
|
op --| : ('a -> 'b * 'c) * ('c -> 'd * 'e) -> 'a -> 'b * '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}
|
||||||
|
for alternative, sequence, sequence-ignore-left,
|
||||||
|
sequence-ignore-right, and piping, as well as combinators for option
|
||||||
|
and repeat. The parsing combinator technology arrived meanwhile even
|
||||||
|
in mainstream languages such as Java or Scala and is nowadays
|
||||||
|
sufficiently efficient implemented to replace conventional Lex-Yacc
|
||||||
|
technology for most applications. It has the advantage to be
|
||||||
|
smoothlessly integrated into standard programs and allows for dynamic
|
||||||
|
grammar extensions. There is a more high-level structure
|
||||||
|
\inlinesml{Parse} providing specific combinators for the
|
||||||
|
command-language Isar:
|
||||||
|
\begin{sml}
|
||||||
|
val attribute = Parse.position Parse.name
|
||||||
|
-- Scan.optional (Parse.$$$ "=" |-- Parse.!!! Parse.name) "";
|
||||||
|
val reference = Parse.position Parse.name
|
||||||
|
-- Scan.option (Parse.$$$ "::" |-- Parse.!!!
|
||||||
|
(Parse.position Parse.name));
|
||||||
|
val attributes = (Parse.$$$ "[" |-- (reference
|
||||||
|
-- (Scan.optional(Parse.$$$ ","
|
||||||
|
|-- (Parse.enum "," attribute))) []))
|
||||||
|
--| Parse.$$$ "]"
|
||||||
|
\end{sml}
|
||||||
|
``Model'' and ``View'' parts were combined to ``parsers'' which were
|
||||||
|
registered in the interpreter toplevel of the Isabelle/Isar framework:
|
||||||
|
\begin{sml}
|
||||||
|
val _ = Outer_Syntax.command @ {command_keyword "declare_reference"}
|
||||||
|
"declare document reference"
|
||||||
|
(attributes >> (fn (((oid,pos),cid),doc_attrs) =>
|
||||||
|
(Toplevel.theory (DOF_core.declare_object_global oid))));
|
||||||
|
\end{sml}
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
Altogether, this gives the \emph{extension} of the Isar syntax
|
||||||
|
allowing to parse and interpret the new \emph{command} in a subsequent
|
||||||
|
\verb+.thy+ file:
|
||||||
|
\begin{isar}
|
||||||
|
declare_reference [lal::requirement, alpha="main", beta=42]
|
||||||
|
\end{isar}
|
||||||
|
where we ignore the semantics at the moment. The construction also
|
||||||
|
generates implicitely some markup information; for example, when
|
||||||
|
hovering over the \inlineisar|declare_reference| command in a
|
||||||
|
front-end supporting PIDE, a popup window with the text: ``declare
|
||||||
|
document reference'' will appear.
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
subsection*["sec:prog_anti"::technical]{*Programming Text Antiquotations*}
|
||||||
|
text\<open>
|
||||||
|
As mentioned in the introduction, Isabelle/Isar is configured with a
|
||||||
|
number of standard commands to annotate formal definitions and proofs
|
||||||
|
with text---the latter is used in particular to generate PDF and HTML
|
||||||
|
documents with internal hypertext-references. Inside these text
|
||||||
|
commands, a number of predefined antiquotations can be inserted which
|
||||||
|
were checked and decorated with markup during editing.
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
Moreover, there is an API for user-defined antiquotations. It follows
|
||||||
|
the lines of the MVC style system extensions presented in the previous
|
||||||
|
section. An excerpt of the table defining some antiquotations can be
|
||||||
|
found in \verb+thy_output.ML+ of the Isabelle sources and give the
|
||||||
|
basic idea:
|
||||||
|
\begin{sml}
|
||||||
|
val _ = Theory.setup
|
||||||
|
(basic_entity @ {binding term} (stp -- Args.term) pretty_term_style #>
|
||||||
|
basic_entity @ {binding prop} (stp -- Args.prop) pretty_term_style #>
|
||||||
|
... )
|
||||||
|
\end{sml}
|
||||||
|
where \inlinesml+stp+ (=\inlinesml+Term_Style.parse+),
|
||||||
|
\inlinesml+Args.term+ and \inlinesml+Args.prop+ are parsing
|
||||||
|
combinators from higher Isar-API's (that actually do the type checking
|
||||||
|
in the surrounding HOL context) and \inlinesml+pretty_term_style+ an
|
||||||
|
operation pretty-printing the parsed term for one of the possible
|
||||||
|
targets HTML or \LaTeX{} (converted to \verb+.pdf+ in a
|
||||||
|
post-compilation process). The construct \inlinesml+@ {binding term}+
|
||||||
|
decorates the keyword ``term'' with positioning markup (allowing
|
||||||
|
navigating to this defining place in \verb+thy_output.ML+ by
|
||||||
|
hyperlinking) and \inlinesml+Theory.setup+ the operator that
|
||||||
|
registers the entire parser/checker into the Isar framework.
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
Together, this establishes the syntax and semantics of, for example,
|
||||||
|
the antiquotation:
|
||||||
|
\begin{isar}
|
||||||
|
text{* @{term "fac 5"} *}
|
||||||
|
\end{isar}
|
||||||
|
inside the text command. A key contribution of this paper is that such
|
||||||
|
SML code is generated \emph{automatically} from an \isadof ontology
|
||||||
|
definition introduced in the subsequent section.
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
end
|
|
@ -0,0 +1,421 @@
|
||||||
|
(*<*)
|
||||||
|
theory "05_DesignImpl"
|
||||||
|
imports "04_isaDofImpl"
|
||||||
|
begin
|
||||||
|
(*>*)
|
||||||
|
|
||||||
|
chapter*[impl2::technical,main_author="Some(@{docitem ''bu''}::author)"]
|
||||||
|
{* \isadof: Design and Implementation*}
|
||||||
|
text\<open>
|
||||||
|
In this section, we present the design and implementation of \isadof.
|
||||||
|
\subsection{Document Ontology Modeling with \isadof}
|
||||||
|
First, we introduce an own language to define ontologies.
|
||||||
|
Conceptually, ontologies consist of:
|
||||||
|
\begin{compactitem}
|
||||||
|
\item a \emph{document class} that describes a concept, \ie, it
|
||||||
|
represents set of \emph{instances} of a document class,
|
||||||
|
i.e. references to document elements;
|
||||||
|
\item \emph{attributes} specific to document classes;
|
||||||
|
\item attributes should be typed (arbitrary HOL-types);
|
||||||
|
\item attributes can refer to other document classes,
|
||||||
|
thus, document classes must also be HOL-types
|
||||||
|
(Such attributes were called \emph{links});
|
||||||
|
\item a special link, the reference to a super-class,
|
||||||
|
establishes an \emph{is-a} relation between classes;
|
||||||
|
\item classes may refer to other classes via a regular expression in a
|
||||||
|
\emph{where} clause (classes with such an optional where clauses are
|
||||||
|
called \emph{monitor classes});
|
||||||
|
\item attributes may have default values in order to facilitate notation.
|
||||||
|
\end{compactitem}
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
|
||||||
|
For ontology modeling, we chose a syntax roughly similar to
|
||||||
|
Isabelle/HOL's extensible records. We present the syntax implicitly
|
||||||
|
by a conceptual example, that serves to introduce the key-features of
|
||||||
|
the modeling language:
|
||||||
|
\begin{isar}
|
||||||
|
doc_class A =
|
||||||
|
x :: "string"
|
||||||
|
|
||||||
|
doc_class B =
|
||||||
|
y :: "string list" <= "[]"
|
||||||
|
|
||||||
|
doc_class C = B +
|
||||||
|
z :: "A option" <= "None"
|
||||||
|
|
||||||
|
datatype enum = "X1" | "X2" | "X3
|
||||||
|
|
||||||
|
doc_class D = B +
|
||||||
|
a1 :: enum <= "X2"
|
||||||
|
a2 :: int <= "0"
|
||||||
|
|
||||||
|
doc_class F =
|
||||||
|
r :: "thm list"
|
||||||
|
b :: "(A \<times> B) set" <= "{}"
|
||||||
|
|
||||||
|
doc_class M =
|
||||||
|
trace :: "(A + C + D + F) list"
|
||||||
|
where "A . (C | D)* . [F]"
|
||||||
|
\end{isar}
|
||||||
|
Isabelle uses a two level syntax: the \emph{outer syntax} which is
|
||||||
|
defined and extended using the mechanisms described in
|
||||||
|
\autoref{sec:plugins} and the \emph{inner syntax}, is used to define
|
||||||
|
type and term expressions of the Isabelle framework. Since we reuse a
|
||||||
|
lot of infrastructure of HOL (with respect to basic type library
|
||||||
|
definitions), parsing and type-checking have been specialized to HOL
|
||||||
|
and extensions thereof. The ``switch'' between outer and inner syntax
|
||||||
|
happens with the quote symbols
|
||||||
|
\inlineisar+"..."+. % In exceptional cases, the latter can be
|
||||||
|
% omitted --- notably, if the type or term consists only of one type
|
||||||
|
% constructor symbol or constant symbol respectively.
|
||||||
|
%
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
The above ontology specification contains the document classes
|
||||||
|
\inlineisar+A+, \inlineisar+B+, \inlineisar+C+, \inlineisar+D+,
|
||||||
|
\inlineisar+F+, and \inlineisar+M+ with the respective attributes
|
||||||
|
\inlineisar+x+, \inlineisar+y+, \inlineisar+z+, \inlineisar+a1+,
|
||||||
|
\inlineisar+a2+, \inlineisar+b+ and \inlineisar+trace+.
|
||||||
|
\inlineisar+C+ and \inlineisar+D+ is are sub-classes from
|
||||||
|
\inlineisar+B+ as states the class extension \inlineisar*B + ... *.
|
||||||
|
|
||||||
|
\enlargethispage{2\baselineskip}
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
Each attribute is typed within the given context; the general HOL
|
||||||
|
library provides the types \inlineisar+string+, \inlineisar+_ list+,
|
||||||
|
\inlineisar+_ option+, and \inlineisar+_ set+. On the fly, other
|
||||||
|
special purpose types can be defined. We reuse here the Isabelle/HOL
|
||||||
|
\inlineisar+datatype+-statement, which can be mixed arbitrarily in
|
||||||
|
between the ontology definitions (like any other Isabelle/HOL command)
|
||||||
|
to define an enumeration type. Document classes---similar to
|
||||||
|
conventional class-definitions as in object-oriented
|
||||||
|
programming---\emph{induce} an implicit HOL type; for this reason the
|
||||||
|
class \inlineisar+C+ can have an attribute that refers to the
|
||||||
|
\inlineisar+A+ attribute classes. Document classes that contain
|
||||||
|
attributes referring to induced class types are called
|
||||||
|
\emph{links}. Links can be complex: the class \inlineisar+F+, for
|
||||||
|
example, contains a set of pairs, \ie, a relation between
|
||||||
|
\inlineisar+A+ and \inlineisar+B+ document instances. Each attribute
|
||||||
|
may be assigned (via \inlineisar+<=+) to a default value represented
|
||||||
|
by a HOL expression, whose syntax is either defined by library
|
||||||
|
operations or constant declarations like the
|
||||||
|
\inlineisar+datatype+-statement.
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
The document class \inlineisar+M+ is a \emph{monitor class}, \ie, a
|
||||||
|
class possessing a \inlineisar+where+ clause containing a regular
|
||||||
|
expression consisting of the class identifier \inlineisar+A+,
|
||||||
|
\inlineisar+B+, etc. Its use is discussed in \autoref{sec:monitor-class}.
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
subsection*[editing::example]{*Editing a Document with Ontology-Conform Meta-Data*}
|
||||||
|
text\<open>
|
||||||
|
As already mentioned, Isabelle/Isar comes with a number of standard
|
||||||
|
\emph{text commands} such as \inlineisar+section{* ... *}+ or
|
||||||
|
\inlineisar+text{* ... *}+ that offer the usual text structuring
|
||||||
|
primitives for documents. From the user point-of-view, text commands
|
||||||
|
offer the facility of spell-checking and IDE support for text
|
||||||
|
antiquotations (as discussed before), from a system point of view,
|
||||||
|
they are particular since they are not conceived to have side effects
|
||||||
|
on the global (formal) context, which is exploited in Isabelle's
|
||||||
|
parallel execution engine.\<close>
|
||||||
|
|
||||||
|
text\<open>
|
||||||
|
\isadof introduces an own family of text-commands based on the
|
||||||
|
standard command API of the Isar engine, which allows having
|
||||||
|
side effects of the global context and thus to store and manage own
|
||||||
|
meta-information (the standard text-command interface turned out not
|
||||||
|
to be flexible enough, and a change of this API conflicts with our
|
||||||
|
goal of not changing Isabelle itself). \isadof, \eg, provides
|
||||||
|
\inlineisar+section*[<meta-args>]{* ... *}+,
|
||||||
|
\inlineisar+subsection*[<meta-args>]{* ... *}+,
|
||||||
|
or \inlineisar+text*[<meta-args>]{* ... *}+, where
|
||||||
|
\inlineisar+<meta-args>+ is a syntax to declaring instance, class and
|
||||||
|
attributes for this text element. The syntax for
|
||||||
|
\inlineisar+<meta-args>+ follows the scheme:
|
||||||
|
\begin{isar}
|
||||||
|
<ref> :: <class_id>, attr_1 = "<expr>", ..., attr_n = "<expr>"
|
||||||
|
\end{isar}
|
||||||
|
where the \inlineisar+<class_id>+ can be optionally omitted which represents
|
||||||
|
the implicit superclass \inlineisar+text+, where \inlineisar+attr_i+ must
|
||||||
|
be declared attributes in the class and where the \inlineisar+"<expr>"+
|
||||||
|
must have the corresponding type. Attributes from a class definition may
|
||||||
|
be left undefined; definitions of attribute values \emph{override} default
|
||||||
|
values or values of super-classes. Overloading of attributes, however, is not
|
||||||
|
permitted in \isadof. \<close>
|
||||||
|
|
||||||
|
text\<open>
|
||||||
|
We can annotate a text as follows. First, we have to place a
|
||||||
|
particular document into the context of our conceptual example
|
||||||
|
ontology shown above:
|
||||||
|
\begin{isar}
|
||||||
|
theory Concept_Example
|
||||||
|
imports "../../ontologies/Conceptual"
|
||||||
|
begin
|
||||||
|
\end{isar}
|
||||||
|
which is contained contained a theory file
|
||||||
|
\verb+../../ontologies/Conceptual.thy+. Then we can continue to annotate
|
||||||
|
our text as follows:
|
||||||
|
\begin{isar}
|
||||||
|
section*[a::A, x = "''alpha''"] {* Lorem ipsum dolor sit amet, ... *}
|
||||||
|
|
||||||
|
text*[c1::C, x = "''beta''"]
|
||||||
|
{* ... suspendisse non arcu malesuada mollis, nibh morbi, ... *}
|
||||||
|
|
||||||
|
text*[d:D, a2="10"]{* Lorem ipsum dolor sit amet, consetetur ...*}
|
||||||
|
\end{isar}\<close>
|
||||||
|
|
||||||
|
text\<open>
|
||||||
|
Let's consider the last line:
|
||||||
|
this text is the instance \inlineisar+d+ which belongs to class
|
||||||
|
\inlineisar+D+, and the default of its attribute \inlineisar+a2+ is
|
||||||
|
overridden to the value \inlineisar+"10"+. Instances are mutable in
|
||||||
|
\isadof, the subsequent \isadof command:
|
||||||
|
\begin{isar}
|
||||||
|
update_instance*[d::D, a1 := X2, a2 := "20"]
|
||||||
|
\end{isar}
|
||||||
|
This changes the attribute values of \verb+d+. The typing
|
||||||
|
annotation \verb+D+ is optional here (if present, it is checked).\<close>
|
||||||
|
|
||||||
|
text\<open>
|
||||||
|
Document instances were used to reference textual content; in the
|
||||||
|
generated \LaTeX{} (PDF) and HTML documents they were supported by
|
||||||
|
hyperlinks. Since Isabelle/Isar has a top-down evaluation and
|
||||||
|
validation strategy for the global document, a kind of forward
|
||||||
|
declaration for references is sometimes necessary.
|
||||||
|
\begin{isar}
|
||||||
|
declare_reference* [<meta-args>]
|
||||||
|
\end{isar}
|
||||||
|
This declares the existence of a text-element and allows for
|
||||||
|
referencing it, although the actual text-element will occur later in
|
||||||
|
the document.\<close>
|
||||||
|
|
||||||
|
|
||||||
|
subsection*[ontolinks::technical]{*Ontology-Conform Logical Links: \isadof Antiquotations*}
|
||||||
|
text\<open>
|
||||||
|
Up to this point, the world of the formal and the informal document
|
||||||
|
parts are strictly separated. The main objective of \isadof are ways
|
||||||
|
to establish machine-checked links between these two universes by
|
||||||
|
instantiating automatically Isabelle/Isar's concept of
|
||||||
|
\emph{antiquoations}. The simplest form of link appears in the
|
||||||
|
following command:
|
||||||
|
\begin{isar}
|
||||||
|
text{* ... in ut tortor ... @ {docitem_ref {*a*}} ... @ {A {*a*}}*}
|
||||||
|
\end{isar}\<close>
|
||||||
|
text\<open>
|
||||||
|
This standard text-command contains two \isadof antiquotations; the
|
||||||
|
first represents just a link to the text-element \inlineisar$a$.
|
||||||
|
The second contains additionally the implicit constraint that the
|
||||||
|
reference to \inlineisar$a$ must also belong to the
|
||||||
|
\inlineisar$A$-class; the following input:
|
||||||
|
\begin{isar}
|
||||||
|
text{* ... ... ... @ {C (*a*}}*}
|
||||||
|
\end{isar}
|
||||||
|
results in the detection of an ontological inconsistency which will be
|
||||||
|
reported in PIDE at editing time. Of course, any modification of the
|
||||||
|
ontology or changes in the labeling of the meta-information will lead
|
||||||
|
to the usual re-checking of the Isabelle/Isar engine. A natural
|
||||||
|
representation of these semantic links inside \isadof documents would
|
||||||
|
be hyperlinks in generated PDF or HTML files.
|
||||||
|
\enlargethispage{2\baselineskip}\<close>
|
||||||
|
|
||||||
|
text\<open>
|
||||||
|
Besides text antiquotations from Isabelle/Isar, we introduced a novel
|
||||||
|
concept that we call \emph{inner syntax antiquotations}. It is a
|
||||||
|
crucial technical feature for establishing links between text-items as
|
||||||
|
well as document meta-data and formal entities of Isabelle such as
|
||||||
|
types, terms and theorems (reflecting the fundamental types
|
||||||
|
\inlineisar+typ+, \inlineisar+term+ and \inlineisar+thm+ of the
|
||||||
|
Isabelle kernel.) We start with a slightly simpler case is the
|
||||||
|
establishment of links between text-elements:
|
||||||
|
\begin{isar}
|
||||||
|
section*[f::F] {* Lectus accumsan velit ultrices, ... }*}
|
||||||
|
|
||||||
|
update_instance*[f,b:="{(@ {docitem ''a''}::A,@ {docitem ''c1''}::C),
|
||||||
|
(@ {docitem ''a''},@ {docitem ''c1''})}"]
|
||||||
|
\end{isar}\<close>
|
||||||
|
|
||||||
|
text\<open>
|
||||||
|
|
||||||
|
This example shows the construction of a relation between text
|
||||||
|
elements \emph{inside} HOL-expressions with the usual syntactic and
|
||||||
|
semantic machinery for sets, pairs, (thus: relations). Inside the
|
||||||
|
world of HOL-terms, we can refer to items of the ``meta-world'' by a
|
||||||
|
particular form of antiquotations called \emph{inner syntax
|
||||||
|
antiquotations}. Similarly, but conceptually different, it is
|
||||||
|
possible to refer in \isadof HOL-expressions to theorems of the
|
||||||
|
preceding context. Thus, it is possible to establish a theorem (or a
|
||||||
|
type or term), in the example below, by a proof ellipse in Isabelle:
|
||||||
|
\begin{isar}
|
||||||
|
theorem some_proof : "P" sorry
|
||||||
|
|
||||||
|
update_instance*[f,r:="[@ {thm ''some_proof''}]"]
|
||||||
|
\end{isar}\<close>
|
||||||
|
text\<open>
|
||||||
|
The resulting theorem is stored in a theorem list as part of the
|
||||||
|
meta-information of a section. Technically, theorems were introduced
|
||||||
|
in \isadof as abstract HOL types and some unspecified (Skolem)
|
||||||
|
HOL-constants with a particular infix-syntax. They are introduced for
|
||||||
|
example by:
|
||||||
|
\begin{isar}
|
||||||
|
typedecl "thm"
|
||||||
|
consts mk_thm :: "string \<Rightarrow> thm" ("@{thm _}")
|
||||||
|
\end{isar}
|
||||||
|
which introduces a new type \inlineisar+thm+ reflecting the internal
|
||||||
|
Isabelle type for established logical facts and the above notation to
|
||||||
|
the inner syntax parser. The \inlineisar+doc_class F+ in our schematic
|
||||||
|
example uses already this type. Whenever these expressions occur
|
||||||
|
inside an inner-syntax HOL-term, they are checked by the HOL parser
|
||||||
|
and type-checker as well as an \isadof checker that establishes that
|
||||||
|
\inlineisar+some_proof+ indeed refers to a known theorem of this name
|
||||||
|
in the current context.
|
||||||
|
% (this is, actually, the symmetry axiom of the equality in HOL).
|
||||||
|
To our knowledge, this is the first ontology-driven framework for
|
||||||
|
editing mathematical and technical documents that focuses particularly
|
||||||
|
on documents mixing formal and informal content---a type of documents
|
||||||
|
that is very common in technical certification processes. We see
|
||||||
|
mainly one area of related works: IDEs and text editors that support
|
||||||
|
editing and checking of documents based on an ontology. There is a
|
||||||
|
large group of ontology editors (\eg, Prot{\'e}g{\'e}~\cite{protege},
|
||||||
|
Fluent Editor~\cite{cognitum}, NeOn~\cite{neon}, or
|
||||||
|
OWLGrEd~\cite{owlgred}). With them, we share the support for defining
|
||||||
|
ontologies as well as auto-completion when editing documents based on
|
||||||
|
an ontology. While our ontology definitions are, currently, based on a
|
||||||
|
textual definition, widely used ontology editors (\eg,
|
||||||
|
OWLGrEd~\cite{owlgred}) also support graphical notations. This could
|
||||||
|
be added to \isadof in the future. A unique feature of \isadof is the
|
||||||
|
deep integration of formal and informal text parts. The only other
|
||||||
|
work in this area wea are aware of is rOntorium~\cite{rontorium}, a plugin
|
||||||
|
for Prot{\'e}g{\'e} that integrates R~\cite{adler:r:2010} into an
|
||||||
|
ontology environment. Here, the main motivation behind this
|
||||||
|
integration is to allow for statistically analyze ontological
|
||||||
|
documents. Thus, this is complementary to our work.\<close>
|
||||||
|
|
||||||
|
text\<open>
|
||||||
|
There is another form of antiquotations, so-called ML-antiquotations
|
||||||
|
in Isabelle, which we do not describe in detail in this paper. With
|
||||||
|
this specific antiquotations, it is possible to refer to the HOL-term
|
||||||
|
of all the attributes of the doc-item; by writing specific ML-code,
|
||||||
|
arbitrary user-defined criteria can be implemented establishing that
|
||||||
|
all meta-data of a document satisfies a particular validation. For
|
||||||
|
example, in the context of an ontology for scientific papers, we could
|
||||||
|
enforce that terms or theorems have a particular form or correspond to
|
||||||
|
``claims'' (contributions) listed in the introduction of the paper.
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
subsection*["sec:monitor-class"::technical]{*Monitor Document Classes*}
|
||||||
|
text\<open>
|
||||||
|
\autoref{lst:example} shows our conceptual running example in all
|
||||||
|
details. While inheritance on document classes allows for structuring
|
||||||
|
meta-data in an object-oriented manner, monitor classes such as
|
||||||
|
\inlineisar+M+ impose a structural relation on a document. The
|
||||||
|
\inlineisar+where+ clause permits to write a regular expression on
|
||||||
|
class names; the class names mentioned in the where clause are called
|
||||||
|
the ``controlled'' ones. The expression specifies that all
|
||||||
|
text-elements that are instances of controlled classes to occur in the
|
||||||
|
sequential order specified by the \inlineisar+where+-clause. Start and
|
||||||
|
end were marked by the corresponding monitor commands. Note that
|
||||||
|
monitors may be nested.
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
\begin{isar}[float, caption={Our running example},label={lst:example}]
|
||||||
|
theory Concept_Example
|
||||||
|
imports "../../ontologies/Conceptual"
|
||||||
|
begin
|
||||||
|
|
||||||
|
open_monitor*[struct::M]
|
||||||
|
|
||||||
|
section*[a::A, x = "''alpha''"] {* Lorem ipsum dolor sit amet, ... *}
|
||||||
|
|
||||||
|
text*[c1::C, x = "''beta''"]
|
||||||
|
{* ... suspendisse non arcu malesuada mollis, nibh morbi, ... *}
|
||||||
|
|
||||||
|
text*[d::D, a1 = "X3"]
|
||||||
|
{* ... phasellus amet id massa nunc, pede suscipit repellendus, ... *}
|
||||||
|
|
||||||
|
text*[c2::C, x = "''delta''"]
|
||||||
|
{* ... in ut tortor eleifend augue pretium consectetuer. *}
|
||||||
|
|
||||||
|
section*[f::F] {* Lectus accumsan velit ultrices, ... @ {docitem_ref {*a*} }*}
|
||||||
|
|
||||||
|
theorem some_proof : "P" sorry
|
||||||
|
|
||||||
|
update_instance*[f,r:="[@ {thm ''some_proof''}]"]
|
||||||
|
|
||||||
|
text{* ..., mauris amet, id elit aliquam aptent id, ... *}
|
||||||
|
|
||||||
|
update_instance*[f,b:="{(@ {docitem ''a''}::A,@ {docitem ''c1''}::C),
|
||||||
|
(@ {docitem ''a''}, @ {docitem ''c1''})}"]
|
||||||
|
|
||||||
|
close_monitor*[struct]
|
||||||
|
\end{isar}
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
section{*Document Generation*}
|
||||||
|
text\<open>
|
||||||
|
Up to know, we discussed the definition of ontologies and their
|
||||||
|
representation in an interactive development environment, \ie,
|
||||||
|
JEdit/PIDE. In many application areas, it is desirable to also
|
||||||
|
generate a ``static'' document, \eg, for long-term archiving. Isabelle
|
||||||
|
supports the generation of both HTML and PDF documents. Due to its
|
||||||
|
standardization, the latter (in particular in the variant PDF/A) is
|
||||||
|
particularly suitable for ensuring long-term access. Hence, our
|
||||||
|
prototype focuses currently on the generation of consistent PDF
|
||||||
|
documents.\<close>
|
||||||
|
|
||||||
|
text\<open>
|
||||||
|
Technically, the PDF generation is based on \LaTeX{} (this is mostly
|
||||||
|
hidden from the end users) as standard text formatting such as
|
||||||
|
itemize-lists or italic and bold fonts can be written in JEdit without
|
||||||
|
in a ``what-you-see-is-what-you-get''-style. We extended the \LaTeX{}
|
||||||
|
generation of Isabelle in such a way that for each ontological concept
|
||||||
|
that is formally defined in \isadof, is mapped to a dedicated
|
||||||
|
\LaTeX-command. This \LaTeX-command is responsible for the actual
|
||||||
|
typesetting of the concept as well as for generating the necessary
|
||||||
|
label and references. For each defined ontology, we need to define a
|
||||||
|
\LaTeX-style that defines these commands. For the standard commands
|
||||||
|
such as \inlineisar|section*[...]{* ... *}|, default implementations
|
||||||
|
are provided by \isadof. For example, the following is the \LaTeX{}
|
||||||
|
definition for processing \inlineisar|section*[...]{* ... *}|:
|
||||||
|
\begin{ltx}
|
||||||
|
\newkeycommand\isaDofSection[reference=,class_id=][1]{%
|
||||||
|
\isamarkupsection{#1}\label{\commandkey{reference}}%
|
||||||
|
}
|
||||||
|
\end{ltx}\<close>
|
||||||
|
text\<open>
|
||||||
|
This command gets all meta-arguments of the concepts a swell as the
|
||||||
|
actual arguments. The layout is delegated to Isabelle's standard
|
||||||
|
sectioning commands
|
||||||
|
(\inlineltx|\isamarkupsection{#1}|). Additionally, a label for
|
||||||
|
linking to this section is generated.
|
||||||
|
\enlargethispage{2\baselineskip}
|
||||||
|
\<close>
|
||||||
|
text\<open>
|
||||||
|
Considering an ontology defining the concepts for writing scientific
|
||||||
|
papers, a potential definition for typesetting abstracts (where an
|
||||||
|
abstract includes a list of keywords) is:
|
||||||
|
\begin{ltx}
|
||||||
|
\newkeycommand\isaDofTextAbstract[reference=,class_id=,keywordlist=][1]{%
|
||||||
|
\begin{isamarkuptext}%
|
||||||
|
\begin{abstract}\label{\commandkey{reference}}%
|
||||||
|
#1
|
||||||
|
|
||||||
|
\ifthenelse{\equal{\commandkey{keywordlist}}{}}{}{%
|
||||||
|
\medskip\noindent{\textbf{Keywords:}} \commandkey{keywordlist}%
|
||||||
|
}
|
||||||
|
\end{abstract}%
|
||||||
|
\end{isamarkuptext}%
|
||||||
|
}
|
||||||
|
\end{ltx}
|
||||||
|
Our generated \LaTeX{} is conceptually very close
|
||||||
|
SALT~\cite{DBLP:conf/esws/GrozaHMD07}--- but instead of writing
|
||||||
|
\LaTeX{} manually it is automatically generated and, additionally, can
|
||||||
|
also guarantee the consistency of the formal (mathematical/logical)
|
||||||
|
content.
|
||||||
|
\<close>
|
||||||
|
|
||||||
|
(*<*)
|
||||||
|
end
|
||||||
|
(*>*)
|
|
@ -1,6 +1,7 @@
|
||||||
(*<*)
|
(*<*)
|
||||||
theory "04_Conclusion"
|
theory "06_Conclusion"
|
||||||
imports "03_IsaDof"
|
imports "03_IsaDof"
|
||||||
|
(* imports "05_DesignImpl *)
|
||||||
begin
|
begin
|
||||||
(*>*)
|
(*>*)
|
||||||
|
|
|
@ -1,10 +1,10 @@
|
||||||
(*<*)
|
(*<*)
|
||||||
theory IsaDofManual
|
theory IsaDofManual
|
||||||
imports "04_Conclusion"
|
imports "06_Conclusion"
|
||||||
begin
|
begin
|
||||||
(*<*)
|
(*<*)
|
||||||
|
|
||||||
text*[bib::bibliography]\<open>TODO\<close>
|
text*[bib::bibliography]\<open>References\<close>
|
||||||
|
|
||||||
close_monitor*[this]
|
close_monitor*[this]
|
||||||
|
|
||||||
|
|
Loading…
Reference in New Issue