104

1 
%%%%Currently UNDOCUMENTED lowlevel 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 \verball T is the universal quantifier for type {\tt T}\@.


12 


13 
The term \verbequals 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 welltyped.


27 


28 


29 
Calling \verbsubst_bounds$([u_{n1},\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_{n1} \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 
\verbsubst_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 \verbterm_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. Firstorder pattern matching is used


51 
to implement metalevel rewriting.


52 


53 


54 
\subsection{The representation of objectrules}


55 
The module {\tt Logic} contains operations concerned with inference 


56 
especially, for constructing and destructing terms that represent


57 
objectrules.


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 flexflex constraints to an objectrule.


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 objectrule: 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 objectrule 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_{i1},\ldots, \phi_1], \phi)\),


165 
where $\phi$ need not be atomic. Raises an exception if $i$ is out of


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


231 
unifiers: env * ((term*term)list) > (env * (term*term)list) seq


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 flexflex pairs (these are discussed below).


238 


239 
\beginprog


240 
smash_unifiers: env * (term*term)list > env seq


241 
\endprog


242 
This unification function maps an environment and a list of disagreement


243 
pairs to a sequence of updated environments. The function obliterates


244 
flexflex pairs by choosing the obvious unifier. It may be used to tidy up


245 
any flexflex pairs remaining at the end of a proof.


246 


247 
\subsubsection{Flexibleflexible disagreement pairs}


248 


249 


250 
\subsubsection{Multiple unifiers}


251 
The unification procedure performs Huet's {\sc match} operation


252 
\cite{huet75} in big steps.


253 
It solves \(\Var{f}(t_1,\ldots,t_p) \equiv u\) for \(\Var{f}\) by finding


254 
all ways of copying \(u\), first trying projection on the arguments


255 
\(t_i\). It never copies below any variable in \(u\); instead it returns a


256 
new variable, resulting in a flexflex disagreement pair.


257 


258 


259 
\beginprog


260 
type_assign: cterm > cterm


261 
\endprog


262 
Produces a cterm by updating the signature of its argument


263 
to include all variable/type assignments.


264 
Type inference under the resulting signature will assume the


265 
same type assignments as in the argument.


266 
This is used in the goal package to give persistence to type assignments


267 
within each proof.


268 
(Contrast with {\sc lcf}'s sticky types \cite[page 148]{paulsonbook}.)


269 


270 
