doc-src/Ref/undocumented.tex
 author wenzelm Sun, 15 Oct 2000 19:50:35 +0200 changeset 10220 2a726de6e124 parent 4276 a770eae2cdb0 permissions -rw-r--r--
proper symbol markup with \isamath, \isatext; support sub/super scripts:

%%%%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}.)