doc-src/Ref/undocumented.tex
author paulson
Fri, 27 Nov 1998 13:13:22 +0100
changeset 5980 2e9314c07146
parent 4276 a770eae2cdb0
permissions -rw-r--r--
added Real/Hyperreal
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     1
%%%%Currently UNDOCUMENTED low-level functions!  from previous manual
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     2
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     3
%%%%Low level information about terms and module Logic.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     4
%%%%Mainly used for implementation of Pure.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     5
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     6
%move to ML sources?
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     7
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     8
\subsection{Basic declarations}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
     9
The implication symbol is {\tt implies}.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    10
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    11
The term \verb|all T| is the universal quantifier for type {\tt T}\@.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    12
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    13
The term \verb|equals T| is the equality predicate for type {\tt T}\@.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    14
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    15
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    16
There are a number of basic functions on terms and types.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    17
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    18
\index{--->}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    19
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    20
op ---> : typ list * typ -> typ
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    21
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    22
Given types \([ \tau_1, \ldots, \tau_n]\) and \(\tau\), it
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    23
forms the type \(\tau_1\to \cdots \to (\tau_n\to\tau)\).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    24
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    25
Calling {\prog{}type_of \${t}}\index{type_of} computes the type of the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    26
term~$t$.  Raises exception {\tt TYPE} unless applications are well-typed.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    27
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    28
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    29
Calling \verb|subst_bounds|$([u_{n-1},\ldots,u_0],\,t)$\index{subst_bounds}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    30
substitutes the $u_i$ for loose bound variables in $t$.  This achieves
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    31
\(\beta\)-reduction of \(u_{n-1} \cdots u_0\) into $t$, replacing {\tt
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    32
Bound~i} with $u_i$.  For \((\lambda x y.t)(u,v)\), the bound variable
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    33
indices in $t$ are $x:1$ and $y:0$.  The appropriate call is
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    34
\verb|subst_bounds([v,u],t)|.  Loose bound variables $\geq n$ are reduced
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    35
by $n$ to compensate for the disappearance of $n$ lambdas.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    36
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    37
\index{maxidx_of_term}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    38
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    39
maxidx_of_term: term -> int
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    40
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    41
Computes the maximum index of all the {\tt Var}s in a term.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    42
If there are no {\tt Var}s, the result is \(-1\).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    43
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    44
\index{term_match}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    45
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    46
term_match: (term*term)list * term*term -> (term*term)list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    47
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    48
Calling \verb|term_match(vts,t,u)| instantiates {\tt Var}s in {\tt t} to
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    49
match it with {\tt u}.  The resulting list of variable/term pairs extends
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    50
{\tt vts}, which is typically empty.  First-order pattern matching is used
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    51
to implement meta-level rewriting.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    52
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    53
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    54
\subsection{The representation of object-rules}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    55
The module {\tt Logic} contains operations concerned with inference ---
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    56
especially, for constructing and destructing terms that represent
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    57
object-rules.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    58
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    59
\index{occs}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    60
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    61
op occs: term*term -> bool
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    62
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    63
Does one term occur in the other?
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    64
(This is a reflexive relation.)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    65
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    66
\index{add_term_vars}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    67
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    68
add_term_vars: term*term list -> term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    69
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    70
Accumulates the {\tt Var}s in the term, suppressing duplicates.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    71
The second argument should be the list of {\tt Var}s found so far.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    72
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    73
\index{add_term_frees}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    74
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    75
add_term_frees: term*term list -> term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    76
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    77
Accumulates the {\tt Free}s in the term, suppressing duplicates.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    78
The second argument should be the list of {\tt Free}s found so far.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    79
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    80
\index{mk_equals}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    81
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    82
mk_equals: term*term -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    83
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    84
Given $t$ and $u$ makes the term $t\equiv u$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    85
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    86
\index{dest_equals}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    87
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    88
dest_equals: term -> term*term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    89
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    90
Given $t\equiv u$ returns the pair $(t,u)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    91
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    92
\index{list_implies:}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    93
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    94
list_implies: term list * term -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    95
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    96
Given the pair $([\phi_1,\ldots, \phi_m], \phi)$
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    97
makes the term \([\phi_1;\ldots; \phi_m] \Imp \phi\).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    98
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
    99
\index{strip_imp_prems}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   100
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   101
strip_imp_prems: term -> term list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   102
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   103
Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   104
returns the list \([\phi_1,\ldots, \phi_m]\). 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   105
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   106
\index{strip_imp_concl}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   107
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   108
strip_imp_concl: term -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   109
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   110
Given \([\phi_1;\ldots; \phi_m] \Imp \phi\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   111
returns the term \(\phi\). 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   112
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   113
\index{list_equals}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   114
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   115
list_equals: (term*term)list * term -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   116
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   117
For adding flex-flex constraints to an object-rule. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   118
Given $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   119
makes the term \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   120
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   121
\index{strip_equals}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   122
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   123
strip_equals: term -> (term*term) list * term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   124
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   125
Given \([t_1\equiv u_1;\ldots; t_k\equiv u_k]\Imp \phi\),
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   126
returns $([(t_1,u_1),\ldots, (t_k,u_k)], \phi)$.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   127
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   128
\index{rule_of}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   129
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   130
rule_of: (term*term)list * term list * term -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   131
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   132
Makes an object-rule: given the triple
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   133
\[ ([(t_1,u_1),\ldots, (t_k,u_k)], [\phi_1,\ldots, \phi_m], \phi) \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   134
returns the term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   135
\([t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m]\Imp \phi\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   136
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   137
\index{strip_horn}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   138
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   139
strip_horn: term -> (term*term)list * term list * term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   140
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   141
Breaks an object-rule into its parts: given
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   142
\[ [t_1\equiv u_1;\ldots; t_k\equiv u_k; \phi_1;\ldots; \phi_m] \Imp \phi \]
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   143
returns the triple
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   144
\(([(t_k,u_k),\ldots, (t_1,u_1)], [\phi_1,\ldots, \phi_m], \phi).\)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   145
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   146
\index{strip_assums}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   147
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   148
strip_assums: term -> (term*int) list * (string*typ) list * term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   149
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   150
Strips premises of a rule allowing a more general form,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   151
where $\Forall$ and $\Imp$ may be intermixed.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   152
This is typical of assumptions of a subgoal in natural deduction.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   153
Returns additional information about the number, names,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   154
and types of quantified variables.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   155
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   156
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   157
\index{strip_prems}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   158
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   159
strip_prems: int * term list * term -> term list * term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   160
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   161
For finding premise (or subgoal) $i$: given the triple
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   162
\( (i, [], \phi_1;\ldots \phi_i\Imp \phi) \)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   163
it returns another triple,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   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
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   166
range.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   167
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   168
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   169
\subsection{Environments}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   170
The module {\tt Envir} (which is normally closed)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   171
declares a type of environments.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   172
An environment holds variable assignments
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   173
and the next index to use when generating a variable.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   174
\par\indent\vbox{\small \begin{verbatim}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   175
    datatype env = Envir of {asol: term xolist, maxidx: int}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   176
\end{verbatim}}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   177
The operations of lookup, update, and generation of variables
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   178
are used during unification.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   179
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   180
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   181
empty: int->env
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   182
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   183
Creates the environment with no assignments
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   184
and the given index.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   185
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   186
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   187
lookup: env * indexname -> term option
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   188
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   189
Looks up a variable, specified by its indexname,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   190
and returns {\tt None} or {\tt Some} as appropriate.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   191
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   192
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   193
update: (indexname * term) * env -> env
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   194
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   195
Given a variable, term, and environment,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   196
produces {\em a new environment\/} where the variable has been updated.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   197
This has no side effect on the given environment.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   198
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   199
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   200
genvar: env * typ -> env * term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   201
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   202
Generates a variable of the given type and returns it,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   203
paired with a new environment (with incremented {\tt maxidx} field).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   204
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   205
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   206
alist_of: env -> (indexname * term) list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   207
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   208
Converts an environment into an association list
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   209
containing the assignments.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   210
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   211
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   212
norm_term: env -> term -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   213
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   214
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   215
Copies a term, 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   216
following assignments in the environment,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   217
and performing all possible \(\beta\)-reductions.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   218
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   219
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   220
rewrite: (env * (term*term)list) -> term -> term
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   221
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   222
Rewrites a term using the given term pairs as rewrite rules.  Assignments
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   223
are ignored; the environment is used only with {\tt genvar}, to generate
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   224
unique {\tt Var}s as placeholders for bound variables.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   225
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   226
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   227
\subsection{The unification functions}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   228
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   229
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   230
\beginprog
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3485
diff changeset
   231
unifiers: env * ((term*term)list) -> (env * (term*term)list) Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   232
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   233
This is the main unification function.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   234
Given an environment and a list of disagreement pairs,
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   235
it returns a sequence of outcomes.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   236
Each outcome consists of an updated environment and 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   237
a list of flex-flex pairs (these are discussed below).
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   238
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   239
\beginprog
4276
a770eae2cdb0 changed Pure/Sequence interface;
wenzelm
parents: 3485
diff changeset
   240
smash_unifiers: env * (term*term)list -> env Seq.seq
104
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   241
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   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
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   245
any flex-flex pairs remaining at the end of a proof.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   246
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   247
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   248
\subsubsection{Multiple unifiers}
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   249
The unification procedure performs Huet's {\sc match} operation
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   250
\cite{huet75} in big steps.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   251
It solves \(\Var{f}(t_1,\ldots,t_p) \equiv u\) for \(\Var{f}\) by finding
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   252
all ways of copying \(u\), first trying projection on the arguments
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   253
\(t_i\).  It never copies below any variable in \(u\); instead it returns a
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   254
new variable, resulting in a flex-flex disagreement pair.  
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   255
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   256
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   257
\beginprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   258
type_assign: cterm -> cterm
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   259
\endprog
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   260
Produces a cterm by updating the signature of its argument
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   261
to include all variable/type assignments.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   262
Type inference under the resulting signature will assume the
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   263
same type assignments as in the argument.
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   264
This is used in the goal package to give persistence to type assignments
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   265
within each proof. 
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   266
(Contrast with {\sc lcf}'s sticky types \cite[page 148]{paulson-book}.)
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   267
d8205bb279a7 Initial revision
lcp
parents:
diff changeset
   268