author paulson
Fri, 27 Nov 1998 13:13:22 +0100
changeset 5980 2e9314c07146
parent 4276 a770eae2cdb0
permissions -rw-r--r--
added Real/Hyperreal

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

op ---> : typ list * typ -> typ
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.

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

term_match: (term*term)list * term*term -> (term*term)list
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

op occs: term*term -> bool
Does one term occur in the other?
(This is a reflexive relation.)

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

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

mk_equals: term*term -> term
Given $t$ and $u$ makes the term $t\equiv u$.

dest_equals: term -> term*term
Given $t\equiv u$ returns the pair $(t,u)$.

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

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

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

list_equals: (term*term)list * term -> term
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\).

strip_equals: term -> (term*term) list * term
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)$.

rule_of: (term*term)list * term list * term -> term
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\)

strip_horn: term -> (term*term)list * term list * term
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).\)

strip_assums: term -> (term*int) list * (string*typ) list * term
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.

strip_prems: int * term list * term -> term list * term
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

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}
The operations of lookup, update, and generation of variables
are used during unification.

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

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

update: (indexname * term) * env -> env
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.

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

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

norm_term: env -> term -> term

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

rewrite: (env * (term*term)list) -> term -> term
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}

unifiers: env * ((term*term)list) -> (env * (term*term)list) Seq.seq
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).

smash_unifiers: env * (term*term)list -> env Seq.seq
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.  

type_assign: cterm -> cterm
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}.)