% -*- Mode: LaTeX -*-

\section{Extensions}
\label{sec:extensions}

In this section we describe how to extend the use of the \tbx{close}
construct to mutable arrays and arbitrary, multi-level data-structures
involving a combination of references, tuples, functions and
arrays.\footnote{Extensions to include general algebraic datatypes
will be discussed in the full paper. We have dropped that discussion
from this technical summary due to lack of space.}

\subsection{Arrays}

The treatment of individual reference locations in
Sections~\ref{sec:dynamic-semantics} and \ref{sec:static-semantics}
directly extends to arrays of locations. A 1-dimensional array value
is modeled as a pair $\aval{l,\ul{n}}$ which denotes $n$ consecutive
array locations starting from $l$.  Since arrays are considered to be
homogeneous data-structures, a single region variable suffices to
represent the imperative properties of all the locations within an
array.  For example, a mutable vector containing values of type $\tau$
is typed as $(\tau\;\fn{vector}{r})$ (\cmp mutable references with
type $(\tau\;\fn{ref}{r})$).

The primitive dynamic rules for array allocation (\tbx{alloc\_vector
(l,u)}), array dereference (\tbx{a[i]}) and array assignment
(\tbx{a[i]:=b}) follow the corresponding rules for references
(see \fig{dynamic}). During vector allocation, $n$ fresh
locations are added to the domain of the store all of which possess
the read/write tag. The dynamic \cbx{close} rule for a vector closes
all its locations simultaneously. The safety of this operation is
ensured by the static \cbx{close} rule (see \fig{static}) that allows
converting a mutable vector type $(\tau\;\fn{vector}{r})$ into a
non-mutable vector type $(\tau\;\fn{vector}{\epsilon})$ only if the
region $r$ is not present in the enclosing type environment $E$ and in
the exported element type $\tau$.

The above machinery allows us to finally answer the problem in
\sec{problem} regarding functional arrays. The imperative
implementations for functions \tbx{make\_vector}
(Example~\ref{ex-make-vector-sol2}) and \tbx{histogram}
(Example~\ref{ex-histogram}) can now be verified and closed
automatically.

\subsection{Multi-level Data-Structures}

In our system, for each primitive or user-defined mutable datatype we
have specific rules regarding which regions may be closed and how to
verify the soundness of the closing operation. But in general, the
result of an arbitrary \tbx{close} expression may be a multi-level
data-structure involving a combination of references, arrays, tuples,
and functions. The user may want all or some of the locations present
in the result to be closed. This can be specified in our type system
using a {\em type annotation}:
\[\tbx{close}\;a :: \tau\]
The user annotates the expression to be closed with an appropriately
decorated type $\tau$ that shows all qualified type constructors along
with their region parameters.  Mutable types that need to be closed
are annotated with the null region ($\epsilon$).

In order to verify the soundness of such arbitrary \tbx{close}
expressions, the type system effectively synthesizes specialized
dynamic and static \cbx{close} rules on the lines of the semantics
presented in Sections~\ref{sec:dynamic-semantics} and
\ref{sec:static-semantics}. First, the annotation type is matched
against the inferred type of the expression to determine the exact set
of region variables being closed.  In order for the overall close
operation to be sound, none of the region variables being closed
should be present in the current type environment $E$ or the
annotation type $\tau$ (\cmp \cbx{close} rule in \fig{static}).
