summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
file |
latest |
revisions |
annotate |
diff |
comparison |
raw |
help

doc-src/Ref/undocumented.tex

author | paulson |

Wed, 07 Oct 1998 10:31:30 +0200 | |

changeset 5619 | 76a8c72e3fd4 |

parent 4276 | a770eae2cdb0 |

permissions | -rw-r--r-- |

new theorems

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