1 %%%%Currently UNDOCUMENTED low-level functions! from previous manual
3 %%%%Low level information about terms and module Logic.
4 %%%%Mainly used for implementation of Pure.
8 \subsection{Basic declarations}
9 The implication symbol is {\tt implies}.
11 The term \verb|all T| is the universal quantifier for type {\tt T}\@.
13 The term \verb|equals T| is the equality predicate for type {\tt T}\@.
16 There are a number of basic functions on terms and types.
20 op ---> : typ list * typ -> typ
22 Given types \([ \tau_1, \ldots, \tau_n]\) and \(\tau\), it
23 forms the type \(\tau_1\to \cdots \to (\tau_n\to\tau)\).
25 Calling {\prog{}type_of \${t}}\index{type_of} computes the type of the
26 term~$t$. Raises exception {\tt TYPE} unless applications are well-typed.
29 Calling \verb|subst_bounds|$([u_{n-1},\ldots,u_0],\,t)$\index{subst_bounds}
30 substitutes the $u_i$ for loose bound variables in $t$. This achieves
31 \(\beta\)-reduction of \(u_{n-1} \cdots u_0\) into $t$, replacing {\tt
32 Bound~i} with $u_i$. For \((\lambda x y.t)(u,v)\), the bound variable
33 indices in $t$ are $x:1$ and $y:0$. The appropriate call is
34 \verb|subst_bounds([v,u],t)|. Loose bound variables $\geq n$ are reduced
35 by $n$ to compensate for the disappearance of $n$ lambdas.
37 \index{maxidx_of_term}
39 maxidx_of_term: term -> int
41 Computes the maximum index of all the {\tt Var}s in a term.
42 If there are no {\tt Var}s, the result is \(-1\).
46 term_match: (term*term)list * term*term -> (term*term)list
48 Calling \verb|term_match(vts,t,u)| instantiates {\tt Var}s in {\tt t} to
49 match it with {\tt u}. The resulting list of variable/term pairs extends
50 {\tt vts}, which is typically empty. First-order pattern matching is used
51 to implement meta-level rewriting.
54 \subsection{The representation of object-rules}
55 The module {\tt Logic} contains operations concerned with inference ---
56 especially, for constructing and destructing terms that represent
61 op occs: term*term -> bool
63 Does one term occur in the other?
64 (This is a reflexive relation.)
68 add_term_vars: term*term list -> term list
70 Accumulates the {\tt Var}s in the term, suppressing duplicates.
71 The second argument should be the list of {\tt Var}s found so far.
73 \index{add_term_frees}
75 add_term_frees: term*term list -> term list
77 Accumulates the {\tt Free}s in the term, suppressing duplicates.
78 The second argument should be the list of {\tt Free}s found so far.
82 mk_equals: term*term -> term
84 Given $t$ and $u$ makes the term $t\equiv u$.
88 dest_equals: term -> term*term
90 Given $t\equiv u$ returns the pair $(t,u)$.
94 list_implies: term list * term -> term
96 Given the pair $([\phi_1,\ldots, \phi_m], \phi)$
97 makes the term \([\phi_1;\ldots; \phi_m] \Imp \phi\).
99 \index{strip_imp_prems}
101 strip_imp_prems: term -> term list
103 Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)
104 returns the list \([\phi_1,\ldots, \phi_m]\).
106 \index{strip_imp_concl}
108 strip_imp_concl: term -> term
110 Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)
111 returns the term \(\phi\).
115 list_equals: (term*term)list * term -> term
117 For adding flex-flex constraints to an object-rule.
118 Given $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$,
119 makes the term \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\).
123 strip_equals: term -> (term*term) list * term
125 Given \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\),
126 returns $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$.
130 rule_of: (term*term)list * term list * term -> term
132 Makes an object-rule: given the triple
133 \[ ([(t_1,u_1),\ldots, (t_k,u_k)], [\phi_1,\ldots, \phi_m], \phi) \]
135 \([t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m]\Imp \phi\)
139 strip_horn: term -> (term*term)list * term list * term
141 Breaks an object-rule into its parts: given
142 \[ [t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m] \Imp \phi \]
144 \(([(t_k,u_k),\ldots, (t_1,u_1)], [\phi_1,\ldots, \phi_m], \phi).\)
148 strip_assums: term -> (term*int) list * (string*typ) list * term
150 Strips premises of a rule allowing a more general form,
151 where $\Forall$ and $\Imp$ may be intermixed.
152 This is typical of assumptions of a subgoal in natural deduction.
153 Returns additional information about the number, names,
154 and types of quantified variables.
159 strip_prems: int * term list * term -> term list * term
161 For finding premise (or subgoal) $i$: given the triple
162 \( (i, [], \phi_1;\ldots \phi_i\Imp \phi) \)
163 it returns another triple,
164 \((\phi_i, [\phi_{i-1},\ldots, \phi_1], \phi)\),
165 where $\phi$ need not be atomic. Raises an exception if $i$ is out of
169 \subsection{Environments}
170 The module {\tt Envir} (which is normally closed)
171 declares a type of environments.
172 An environment holds variable assignments
173 and the next index to use when generating a variable.
174 \par\indent\vbox{\small \begin{verbatim}
175 datatype env = Envir of {asol: term xolist, maxidx: int}
177 The operations of lookup, update, and generation of variables
178 are used during unification.
183 Creates the environment with no assignments
187 lookup: env * indexname -> term option
189 Looks up a variable, specified by its indexname,
190 and returns {\tt None} or {\tt Some} as appropriate.
193 update: (indexname * term) * env -> env
195 Given a variable, term, and environment,
196 produces {\em a new environment\/} where the variable has been updated.
197 This has no side effect on the given environment.
200 genvar: env * typ -> env * term
202 Generates a variable of the given type and returns it,
203 paired with a new environment (with incremented {\tt maxidx} field).
206 alist_of: env -> (indexname * term) list
208 Converts an environment into an association list
209 containing the assignments.
212 norm_term: env -> term -> term
216 following assignments in the environment,
217 and performing all possible \(\beta\)-reductions.
220 rewrite: (env * (term*term)list) -> term -> term
222 Rewrites a term using the given term pairs as rewrite rules. Assignments
223 are ignored; the environment is used only with {\tt genvar}, to generate
224 unique {\tt Var}s as placeholders for bound variables.
227 \subsection{The unification functions}
231 unifiers: env * ((term*term)list) -> (env * (term*term)list) Seq.seq
233 This is the main unification function.
234 Given an environment and a list of disagreement pairs,
235 it returns a sequence of outcomes.
236 Each outcome consists of an updated environment and
237 a list of flex-flex pairs (these are discussed below).
240 smash_unifiers: env * (term*term)list -> env Seq.seq
242 This unification function maps an environment and a list of disagreement
243 pairs to a sequence of updated environments. The function obliterates
244 flex-flex pairs by choosing the obvious unifier. It may be used to tidy up
245 any flex-flex pairs remaining at the end of a proof.
248 \subsubsection{Multiple unifiers}
249 The unification procedure performs Huet's {\sc match} operation
250 \cite{huet75} in big steps.
251 It solves \(\Var{f}(t_1,\ldots,t_p) \equiv u\) for \(\Var{f}\) by finding
252 all ways of copying \(u\), first trying projection on the arguments
253 \(t_i\). It never copies below any variable in \(u\); instead it returns a
254 new variable, resulting in a flex-flex disagreement pair.
258 type_assign: cterm -> cterm
260 Produces a cterm by updating the signature of its argument
261 to include all variable/type assignments.
262 Type inference under the resulting signature will assume the
263 same type assignments as in the argument.
264 This is used in the goal package to give persistence to type assignments
266 (Contrast with {\sc lcf}'s sticky types \cite[page 148]{paulson-book}.)