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