doc-src/Ref/undocumented.tex

move bool list stuff from BinOperations to BinBoolList;
reorganize BinBoolList into subsections

%%%%Currently UNDOCUMENTED low-level functions!  from previous manual

%%%%Low level information about terms and module Logic.
%%%%Mainly used for implementation of Pure.

%move to ML sources?

\subsection{Basic declarations}
The implication symbol is {\tt implies}.

The term \verb|all T| is the universal quantifier for type {\tt T}\@.

The term \verb|equals T| is the equality predicate for type {\tt T}\@.


There are a number of basic functions on terms and types.

\index{--->}
\beginprog
op ---> : typ list * typ -> typ
\endprog
Given types \([ \tau_1, \ldots, \tau_n]\) and \(\tau\), it
forms the type \(\tau_1\to \cdots \to (\tau_n\to\tau)\).

Calling {\prog{}type_of \${t}}\index{type_of} computes the type of the
term~$t$.  Raises exception {\tt TYPE} unless applications are well-typed.


Calling \verb|subst_bounds|$([u_{n-1},\ldots,u_0],\,t)$\index{subst_bounds}
substitutes the $u_i$ for loose bound variables in $t$.  This achieves
\(\beta\)-reduction of \(u_{n-1} \cdots u_0\) into $t$, replacing {\tt
Bound~i} with $u_i$.  For \((\lambda x y.t)(u,v)\), the bound variable
indices in $t$ are $x:1$ and $y:0$.  The appropriate call is
\verb|subst_bounds([v,u],t)|.  Loose bound variables $\geq n$ are reduced
by $n$ to compensate for the disappearance of $n$ lambdas.

\index{maxidx_of_term}
\beginprog
maxidx_of_term: term -> int
\endprog
Computes the maximum index of all the {\tt Var}s in a term.
If there are no {\tt Var}s, the result is \(-1\).

\index{term_match}
\beginprog
term_match: (term*term)list * term*term -> (term*term)list
\endprog
Calling \verb|term_match(vts,t,u)| instantiates {\tt Var}s in {\tt t} to
match it with {\tt u}.  The resulting list of variable/term pairs extends
{\tt vts}, which is typically empty.  First-order pattern matching is used
to implement meta-level rewriting.


\subsection{The representation of object-rules}
The module {\tt Logic} contains operations concerned with inference ---
especially, for constructing and destructing terms that represent
object-rules.

\index{occs}
\beginprog
op occs: term*term -> bool
\endprog
Does one term occur in the other?
(This is a reflexive relation.)

\index{add_term_vars}
\beginprog
add_term_vars: term*term list -> term list
\endprog
Accumulates the {\tt Var}s in the term, suppressing duplicates.
The second argument should be the list of {\tt Var}s found so far.

\index{add_term_frees}
\beginprog
add_term_frees: term*term list -> term list
\endprog
Accumulates the {\tt Free}s in the term, suppressing duplicates.
The second argument should be the list of {\tt Free}s found so far.

\index{mk_equals}
\beginprog
mk_equals: term*term -> term
\endprog
Given $t$ and $u$ makes the term $t\equiv u$.

\index{dest_equals}
\beginprog
dest_equals: term -> term*term
\endprog
Given $t\equiv u$ returns the pair $(t,u)$.

\index{list_implies:}
\beginprog
list_implies: term list * term -> term
\endprog
Given the pair $([\phi_1,\ldots, \phi_m], \phi)$
makes the term \([\phi_1;\ldots; \phi_m] \Imp \phi\).

\index{strip_imp_prems}
\beginprog
strip_imp_prems: term -> term list
\endprog
Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)
returns the list \([\phi_1,\ldots, \phi_m]\). 

\index{strip_imp_concl}
\beginprog
strip_imp_concl: term -> term
\endprog
Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)
returns the term \(\phi\). 

\index{list_equals}
\beginprog
list_equals: (term*term)list * term -> term
\endprog
For adding flex-flex constraints to an object-rule. 
Given $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$,
makes the term \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\).

\index{strip_equals}
\beginprog
strip_equals: term -> (term*term) list * term
\endprog
Given \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\),
returns $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$.

\index{rule_of}
\beginprog
rule_of: (term*term)list * term list * term -> term
\endprog
Makes an object-rule: given the triple
\[ ([(t_1,u_1),\ldots, (t_k,u_k)], [\phi_1,\ldots, \phi_m], \phi) \]
returns the term
\([t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m]\Imp \phi\)

\index{strip_horn}
\beginprog
strip_horn: term -> (term*term)list * term list * term
\endprog
Breaks an object-rule into its parts: given
\[ [t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m] \Imp \phi \]
returns the triple
\(([(t_k,u_k),\ldots, (t_1,u_1)], [\phi_1,\ldots, \phi_m], \phi).\)

\index{strip_assums}
\beginprog
strip_assums: term -> (term*int) list * (string*typ) list * term
\endprog
Strips premises of a rule allowing a more general form,
where $\Forall$ and $\Imp$ may be intermixed.
This is typical of assumptions of a subgoal in natural deduction.
Returns additional information about the number, names,
and types of quantified variables.


\index{strip_prems}
\beginprog
strip_prems: int * term list * term -> term list * term
\endprog
For finding premise (or subgoal) $i$: given the triple
\( (i, [], \phi_1;\ldots \phi_i\Imp \phi) \)
it returns another triple,
\((\phi_i, [\phi_{i-1},\ldots, \phi_1], \phi)\),
where $\phi$ need not be atomic.  Raises an exception if $i$ is out of
range.


\subsection{Environments}
The module {\tt Envir} (which is normally closed)
declares a type of environments.
An environment holds variable assignments
and the next index to use when generating a variable.
\par\indent\vbox{\small \begin{verbatim}
    datatype env = Envir of {asol: term xolist, maxidx: int}
\end{verbatim}}
The operations of lookup, update, and generation of variables
are used during unification.

\beginprog
empty: int->env
\endprog
Creates the environment with no assignments
and the given index.

\beginprog
lookup: env * indexname -> term option
\endprog
Looks up a variable, specified by its indexname,
and returns {\tt None} or {\tt Some} as appropriate.

\beginprog
update: (indexname * term) * env -> env
\endprog
Given a variable, term, and environment,
produces {\em a new environment\/} where the variable has been updated.
This has no side effect on the given environment.

\beginprog
genvar: env * typ -> env * term
\endprog
Generates a variable of the given type and returns it,
paired with a new environment (with incremented {\tt maxidx} field).

\beginprog
alist_of: env -> (indexname * term) list
\endprog
Converts an environment into an association list
containing the assignments.

\beginprog
norm_term: env -> term -> term
\endprog

Copies a term, 
following assignments in the environment,
and performing all possible \(\beta\)-reductions.

\beginprog
rewrite: (env * (term*term)list) -> term -> term
\endprog
Rewrites a term using the given term pairs as rewrite rules.  Assignments
are ignored; the environment is used only with {\tt genvar}, to generate
unique {\tt Var}s as placeholders for bound variables.


\subsection{The unification functions}


\beginprog
unifiers: env * ((term*term)list) -> (env * (term*term)list) Seq.seq
\endprog
This is the main unification function.
Given an environment and a list of disagreement pairs,
it returns a sequence of outcomes.
Each outcome consists of an updated environment and 
a list of flex-flex pairs (these are discussed below).

\beginprog
smash_unifiers: env * (term*term)list -> env Seq.seq
\endprog
This unification function maps an environment and a list of disagreement
pairs to a sequence of updated environments.  The function obliterates
flex-flex pairs by choosing the obvious unifier.  It may be used to tidy up
any flex-flex pairs remaining at the end of a proof.


\subsubsection{Multiple unifiers}
The unification procedure performs Huet's {\sc match} operation
\cite{huet75} in big steps.
It solves \(\Var{f}(t_1,\ldots,t_p) \equiv u\) for \(\Var{f}\) by finding
all ways of copying \(u\), first trying projection on the arguments
\(t_i\).  It never copies below any variable in \(u\); instead it returns a
new variable, resulting in a flex-flex disagreement pair.  


\beginprog
type_assign: cterm -> cterm
\endprog
Produces a cterm by updating the signature of its argument
to include all variable/type assignments.
Type inference under the resulting signature will assume the
same type assignments as in the argument.
This is used in the goal package to give persistence to type assignments
within each proof. 
(Contrast with {\sc lcf}'s sticky types \cite[page 148]{paulson-book}.)