author | haftmann |
Thu, 12 Nov 2009 15:49:01 +0100 | |
changeset 33633 | 9f7280e0c231 |
parent 4276 | a770eae2cdb0 |
permissions | -rw-r--r-- |
104 | 1 |
%%%%Currently UNDOCUMENTED low-level functions! from previous manual |
2 |
||
3 |
%%%%Low level information about terms and module Logic. |
|
4 |
%%%%Mainly used for implementation of Pure. |
|
5 |
||
6 |
%move to ML sources? |
|
7 |
||
8 |
\subsection{Basic declarations} |
|
9 |
The implication symbol is {\tt implies}. |
|
10 |
||
11 |
The term \verb|all T| is the universal quantifier for type {\tt T}\@. |
|
12 |
||
13 |
The term \verb|equals T| is the equality predicate for type {\tt T}\@. |
|
14 |
||
15 |
||
16 |
There are a number of basic functions on terms and types. |
|
17 |
||
18 |
\index{--->} |
|
19 |
\beginprog |
|
20 |
op ---> : typ list * typ -> typ |
|
21 |
\endprog |
|
22 |
Given types \([ \tau_1, \ldots, \tau_n]\) and \(\tau\), it |
|
23 |
forms the type \(\tau_1\to \cdots \to (\tau_n\to\tau)\). |
|
24 |
||
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. |
|
27 |
||
28 |
||
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. |
|
36 |
||
37 |
\index{maxidx_of_term} |
|
38 |
\beginprog |
|
39 |
maxidx_of_term: term -> int |
|
40 |
\endprog |
|
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\). |
|
43 |
||
44 |
\index{term_match} |
|
45 |
\beginprog |
|
46 |
term_match: (term*term)list * term*term -> (term*term)list |
|
47 |
\endprog |
|
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. |
|
52 |
||
53 |
||
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 |
|
57 |
object-rules. |
|
58 |
||
59 |
\index{occs} |
|
60 |
\beginprog |
|
61 |
op occs: term*term -> bool |
|
62 |
\endprog |
|
63 |
Does one term occur in the other? |
|
64 |
(This is a reflexive relation.) |
|
65 |
||
66 |
\index{add_term_vars} |
|
67 |
\beginprog |
|
68 |
add_term_vars: term*term list -> term list |
|
69 |
\endprog |
|
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. |
|
72 |
||
73 |
\index{add_term_frees} |
|
74 |
\beginprog |
|
75 |
add_term_frees: term*term list -> term list |
|
76 |
\endprog |
|
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. |
|
79 |
||
80 |
\index{mk_equals} |
|
81 |
\beginprog |
|
82 |
mk_equals: term*term -> term |
|
83 |
\endprog |
|
84 |
Given $t$ and $u$ makes the term $t\equiv u$. |
|
85 |
||
86 |
\index{dest_equals} |
|
87 |
\beginprog |
|
88 |
dest_equals: term -> term*term |
|
89 |
\endprog |
|
90 |
Given $t\equiv u$ returns the pair $(t,u)$. |
|
91 |
||
92 |
\index{list_implies:} |
|
93 |
\beginprog |
|
94 |
list_implies: term list * term -> term |
|
95 |
\endprog |
|
96 |
Given the pair $([\phi_1,\ldots, \phi_m], \phi)$ |
|
97 |
makes the term \([\phi_1;\ldots; \phi_m] \Imp \phi\). |
|
98 |
||
99 |
\index{strip_imp_prems} |
|
100 |
\beginprog |
|
101 |
strip_imp_prems: term -> term list |
|
102 |
\endprog |
|
103 |
Given \([\phi_1;\ldots; \phi_m] \Imp \phi\) |
|
104 |
returns the list \([\phi_1,\ldots, \phi_m]\). |
|
105 |
||
106 |
\index{strip_imp_concl} |
|
107 |
\beginprog |
|
108 |
strip_imp_concl: term -> term |
|
109 |
\endprog |
|
110 |
Given \([\phi_1;\ldots; \phi_m] \Imp \phi\) |
|
111 |
returns the term \(\phi\). |
|
112 |
||
113 |
\index{list_equals} |
|
114 |
\beginprog |
|
115 |
list_equals: (term*term)list * term -> term |
|
116 |
\endprog |
|
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\). |
|
120 |
||
121 |
\index{strip_equals} |
|
122 |
\beginprog |
|
123 |
strip_equals: term -> (term*term) list * term |
|
124 |
\endprog |
|
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)$. |
|
127 |
||
128 |
\index{rule_of} |
|
129 |
\beginprog |
|
130 |
rule_of: (term*term)list * term list * term -> term |
|
131 |
\endprog |
|
132 |
Makes an object-rule: given the triple |
|
133 |
\[ ([(t_1,u_1),\ldots, (t_k,u_k)], [\phi_1,\ldots, \phi_m], \phi) \] |
|
134 |
returns the term |
|
135 |
\([t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m]\Imp \phi\) |
|
136 |
||
137 |
\index{strip_horn} |
|
138 |
\beginprog |
|
139 |
strip_horn: term -> (term*term)list * term list * term |
|
140 |
\endprog |
|
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 \] |
|
143 |
returns the triple |
|
144 |
\(([(t_k,u_k),\ldots, (t_1,u_1)], [\phi_1,\ldots, \phi_m], \phi).\) |
|
145 |
||
146 |
\index{strip_assums} |
|
147 |
\beginprog |
|
148 |
strip_assums: term -> (term*int) list * (string*typ) list * term |
|
149 |
\endprog |
|
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. |
|
155 |
||
156 |
||
157 |
\index{strip_prems} |
|
158 |
\beginprog |
|
159 |
strip_prems: int * term list * term -> term list * term |
|
160 |
\endprog |
|
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)\), |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
327
diff
changeset
|
165 |
where $\phi$ need not be atomic. Raises an exception if $i$ is out of |
104 | 166 |
range. |
167 |
||
168 |
||
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} |
|
176 |
\end{verbatim}} |
|
177 |
The operations of lookup, update, and generation of variables |
|
178 |
are used during unification. |
|
179 |
||
180 |
\beginprog |
|
181 |
empty: int->env |
|
182 |
\endprog |
|
183 |
Creates the environment with no assignments |
|
184 |
and the given index. |
|
185 |
||
186 |
\beginprog |
|
187 |
lookup: env * indexname -> term option |
|
188 |
\endprog |
|
189 |
Looks up a variable, specified by its indexname, |
|
190 |
and returns {\tt None} or {\tt Some} as appropriate. |
|
191 |
||
192 |
\beginprog |
|
193 |
update: (indexname * term) * env -> env |
|
194 |
\endprog |
|
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. |
|
198 |
||
199 |
\beginprog |
|
200 |
genvar: env * typ -> env * term |
|
201 |
\endprog |
|
202 |
Generates a variable of the given type and returns it, |
|
203 |
paired with a new environment (with incremented {\tt maxidx} field). |
|
204 |
||
205 |
\beginprog |
|
206 |
alist_of: env -> (indexname * term) list |
|
207 |
\endprog |
|
208 |
Converts an environment into an association list |
|
209 |
containing the assignments. |
|
210 |
||
211 |
\beginprog |
|
212 |
norm_term: env -> term -> term |
|
213 |
\endprog |
|
214 |
||
215 |
Copies a term, |
|
216 |
following assignments in the environment, |
|
217 |
and performing all possible \(\beta\)-reductions. |
|
218 |
||
219 |
\beginprog |
|
220 |
rewrite: (env * (term*term)list) -> term -> term |
|
221 |
\endprog |
|
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. |
|
225 |
||
226 |
||
227 |
\subsection{The unification functions} |
|
228 |
||
229 |
||
230 |
\beginprog |
|
4276 | 231 |
unifiers: env * ((term*term)list) -> (env * (term*term)list) Seq.seq |
104 | 232 |
\endprog |
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). |
|
238 |
||
239 |
\beginprog |
|
4276 | 240 |
smash_unifiers: env * (term*term)list -> env Seq.seq |
104 | 241 |
\endprog |
242 |
This unification function maps an environment and a list of disagreement |
|
3485
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
327
diff
changeset
|
243 |
pairs to a sequence of updated environments. The function obliterates |
f27a30a18a17
Now there are TWO spaces after each full stop, so that the Emacs sentence
paulson
parents:
327
diff
changeset
|
244 |
flex-flex pairs by choosing the obvious unifier. It may be used to tidy up |
104 | 245 |
any flex-flex pairs remaining at the end of a proof. |
246 |
||
247 |
||
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. |
|
255 |
||
256 |
||
257 |
\beginprog |
|
258 |
type_assign: cterm -> cterm |
|
259 |
\endprog |
|
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 |
|
265 |
within each proof. |
|
266 |
(Contrast with {\sc lcf}'s sticky types \cite[page 148]{paulson-book}.) |
|
267 |
||
268 |