//////////////////////////////////////////////////////////////////////////////
//Copyright 2008
// Andrew Gacek, Steven Holte, Gopalan Nadathur, Xiaochu Qi, Zach Snow
//////////////////////////////////////////////////////////////////////////////
// This file is part of Teyjus. //
// //
// Teyjus is free software: you can redistribute it and/or modify //
// it under the terms of the GNU General Public License as published by //
// the Free Software Foundation, either version 3 of the License, or //
// (at your option) any later version. //
// //
// Teyjus is distributed in the hope that it will be useful, //
// but WITHOUT ANY WARRANTY; without even the implied warranty of //
// MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the //
// GNU General Public License for more details. //
// //
// You should have received a copy of the GNU General Public License //
// along with Teyjus. If not, see . //
//////////////////////////////////////////////////////////////////////////////
/****************************************************************************/
/* */
/* File hopu.c. This file contains the main routines implementing the */
/* interpretive part of higher-order pattern unification. */
/* */
/****************************************************************************/
#ifndef HOPU_C
#define HOPU_C
#include "hopu.h"
#include "mctypes.h"
#include "dataformats.h"
#include "hnorm.h"
#include "abstmachine.h"
#include "types.h"
#include "trail.h"
#include "../system/error.h"
#include "../system/memory.h"
#include
/* Unify types associated with constants. */
static void HOPU_typesUnify(DF_TypePtr tyEnv1, DF_TypePtr tyEnv2, int n)
{
AM_pdlError(2*n);
AM_initTypesPDL();
TY_pushPairsToPDL((MemPtr)tyEnv1, (MemPtr)tyEnv2, n);
TY_typesUnify();
}
/* Return the dereference of the abstraction body of the given term. */
DF_TermPtr HOPU_lamBody(DF_TermPtr tmPtr)
{
tmPtr = DF_termDeref(tmPtr);
while (DF_isLam(tmPtr)) tmPtr = DF_termDeref(DF_lamBody(tmPtr));
return tmPtr;
}
/***************************************************************************/
/* Globalize functions needed for HOPU_patternUnidyPair */
/***************************************************************************/
/* Globalize a rigid term. */
/* If the term pointer is not one referring to a heap address, the atomic */
/* content is then copied onto the current top of heap; the term pointer */
/* is updated to the new heap term. */
static DF_TermPtr HOPU_globalizeRigid(DF_TermPtr rPtr)
{
if (AM_nHeapAddr((MemPtr)rPtr)) {//rPtr must refer to const (no type), int,
//float, str, (stream), nil, cons
MemPtr nhreg = AM_hreg + DF_TM_ATOMIC_SIZE;
AM_heapError(nhreg);
DF_copyAtomic(rPtr, AM_hreg);
rPtr = (DF_TermPtr)AM_hreg;
AM_hreg = nhreg;
}
return rPtr;
}
/* Globalize a rigid term and make a variable binding. */
/* If the term pointer to the rigid term is not one referring to a heap */
/* address, its atomic content is then copied into the variable to be bound*/
/* Otherwise, the variable is made a reference to the rigid term. */
void HOPU_globalizeCopyRigid(DF_TermPtr rPtr, DF_TermPtr vPtr)
{
if (AM_nHeapAddr((MemPtr)rPtr)) //rPtr must refer to rigid atomic term
DF_copyAtomic(rPtr, (MemPtr)vPtr);
else DF_mkRef((MemPtr)vPtr, rPtr); //rPtr could also be app
}
/* Globalize a flex term. */
/* If the term pointer is one referring to a stack address, (in which case */
/* the flex term must be a free variable itself), the atomic content is */
/* copied onto the current top of heap; the free variable on stack is then */
/* bound to the new heap term, and the binding is trailed if necessary; the */
/* term pointer is updated to the new heap term. */
DF_TermPtr HOPU_globalizeFlex(DF_TermPtr fPtr)
{
if (AM_stackAddr((MemPtr)fPtr)) {//fPtr must be a reference to var
MemPtr nhreg = AM_hreg + DF_TM_ATOMIC_SIZE;
AM_heapError(nhreg);
DF_copyAtomic(fPtr, AM_hreg);
TR_trailETerm(fPtr);
DF_mkRef((MemPtr)fPtr, (DF_TermPtr)AM_hreg);
fPtr = (DF_TermPtr)AM_hreg;
AM_hreg = nhreg;
}
return fPtr;
}
/***************************************************************************/
/* Explicit eta expansion (on a rigid term) */
/***************************************************************************/
/* Eta expands a rigid term whose term pointer and decomposition are given */
/* by arguments. The new lambda body is returned. (It is unnecessary to */
/* create a new lambda term for the abstractions in the front of the eta */
/* expanded form. Note that the term head and argument vector are updated */
/* as side-effect. */
/* Note globalization on the term head is always performed and no */
/* specialized version of this function is provided based on the assumption*/
/* that explicit eta-expansion is rarely needed. */
static DF_TermPtr HOPU_etaExpand(DF_TermPtr *h, DF_TermPtr *args, int nargs,
int nabs)
{
DF_TermPtr hPtr = *h, oldArgs = *args, rtPtr;
MemPtr suspLoc; //where susps are to be created
int newArity = nargs + nabs;
if (DF_isBV(hPtr)){ //lift index by nabs if the head is a bound variable
int ind = DF_bvIndex(hPtr) + nabs;
AM_embedError(ind);
AM_heapError(AM_hreg + DF_TM_ATOMIC_SIZE);
*h = hPtr =(DF_TermPtr)AM_hreg; //update head pointer
DF_mkBV(AM_hreg,ind);
AM_hreg += DF_TM_ATOMIC_SIZE;
} else
//always perform globalization; eta expansion is rarely needed
*h = hPtr = HOPU_globalizeRigid(hPtr);
AM_arityError(newArity);
AM_heapError(AM_hreg + nargs * DF_TM_SUSP_SIZE + newArity*DF_TM_ATOMIC_SIZE
+ DF_TM_APP_SIZE);
suspLoc = AM_hreg;
AM_hreg += nargs * DF_TM_SUSP_SIZE; //allocate space for nargs suspensions
rtPtr = (DF_TermPtr)AM_hreg; //new application
DF_mkApp(AM_hreg, newArity, hPtr, (DF_TermPtr)(AM_hreg + DF_TM_APP_SIZE));
AM_hreg += DF_TM_APP_SIZE;
*args = (DF_TermPtr)AM_hreg; //update arg vector pointer
for (; nargs > 0; nargs--){//create suspensions over original arguments
DF_mkSusp(suspLoc, 0, nabs, DF_termDeref(oldArgs), DF_EMPTY_ENV);
DF_mkRef(AM_hreg, (DF_TermPtr)suspLoc);
suspLoc += DF_TM_SUSP_SIZE; AM_hreg += DF_TM_ATOMIC_SIZE;
oldArgs = (DF_TermPtr)(((MemPtr)oldArgs) + DF_TM_ATOMIC_SIZE);
}
for (; nabs > 0; nabs--){//create de Bruijn indices from #nabs to #1
DF_mkBV(AM_hreg, nabs);
AM_hreg += DF_TM_ATOMIC_SIZE;
}
return rtPtr;
}
/***************************************************************************/
/* PATTERN RECOGNITION */
/* */
/* Auxiliary functions for recognizing LLambda pattens for flexible terms. */
/***************************************************************************/
/* Whether a bound variable occurs in the given arguments. */
/* It is assumned that the given arguments can only contain bound variables*/
/* and constants. */
static Boolean HOPU_uniqueBV(int bvInd, DF_TermPtr args, int n)
{
DF_TermPtr tPtr;
for ( ; n > 0 ; n-- ){
tPtr = DF_termDeref(args);
if (DF_isBV(tPtr) && (bvInd == DF_bvIndex(tPtr))) return FALSE;
//otherwise different bv or constant, check the next
args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
}
return TRUE;
}
/* Whether a constant occurs in the given arguments. */
/* It is assumned that the given arguments can only contain bound variables*/
/* and constants. */
/* CHANGES have to be made here if the semantics of local constants are */
/* changed with respect to polymorphism. */
static Boolean HOPU_uniqueConst(DF_TermPtr cPtr, DF_TermPtr args, int n)
{
DF_TermPtr tPtr;
for ( ; n > 0 ; n--){
tPtr = DF_termDeref(args);
if (DF_isConst(tPtr) && DF_sameConsts(tPtr, cPtr)) {
if (DF_isTConst(tPtr)) {
EM_TRY {
HOPU_typesUnify(DF_constType(tPtr), DF_constType(cPtr),
AM_cstTyEnvSize(DF_constTabIndex(cPtr)));
} EM_CATCH {
if (EM_CurrentExnType == EM_FAIL) {
AM_resetTypesPDL();//remove tys from pdl for ty unif
return FALSE;
} else EM_RETHROW();
}
} else return FALSE;
} //otherwise different constant or bv, check the next
args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
} //for loop
return TRUE;
}
/* Checking whether the argments of the head normal form given by registers*/
/* AM_argVec, AM_numArgs and AM_numAbs are those of an eta-expanded form. */
/* Specifically, the arguments are attempted to match de Bruijn indices */
/* #n ... #1, where n is the current value of AM_numAbs. */
/* It is assumed that the argument vector is not empty. */
static Boolean HOPU_isEtaExpArgs()
{
if (AM_numArgs != AM_numAbs) return FALSE;
else {
int i = AM_numAbs;
Boolean match = TRUE;
DF_TermPtr oneArg = AM_argVec;
DF_TermPtr head = AM_head;
while (match && (i > 0)){
HN_hnorm(oneArg);
if (AM_numArgs == 0)
match = ((AM_numArgs == 0) && DF_isBV(AM_head) &&
(DF_bvIndex(AM_head) == i));
else
match = (DF_isBV(AM_head) && (DF_bvIndex(AM_head)-AM_numAbs==i)
&& HOPU_isEtaExpArgs());
oneArg = (DF_TermPtr)(((MemPtr)oneArg + DF_TM_ATOMIC_SIZE));
i--;
}
AM_head = head;
return match;
}
}
/* Checking whether the arguments of a flexible term satisfy with the */
/* LLambda pattern with respect to the universe count of its flex head. */
/* CHANGES have to be made here if the semantics of local constants are */
/* changed with respect to polymorphism. */
static Boolean HOPU_isLLambda(int uc, int nargs, DF_TermPtr args)
{
if (nargs == 0) return TRUE;
else {
int i;
DF_TermPtr myArgs = args;
for (i = 0; i < nargs; i++){
HN_hnorm(args);
if (AM_numArgs == 0) {
if (AM_numAbs != 0) return FALSE; //abstraction
if (DF_isBV(AM_head)) { //bound variable
if (!HOPU_uniqueBV(DF_bvIndex(AM_head), myArgs, i))
return FALSE;
} else if (DF_isConst(AM_head)) { //constant
if (!(uc < DF_constUnivCount(AM_head) &&
HOPU_uniqueConst(AM_head, myArgs, i))) return FALSE;
} else return FALSE; //other sort of terms
} else { //AM_numArgs != 0
if (DF_isBV(AM_head)) { //bound variable head
int dbInd = DF_bvIndex(AM_head) - AM_numAbs; //eta-norm
if (dbInd > 0 && HOPU_uniqueBV(dbInd, myArgs, i) &&
HOPU_isEtaExpArgs()) {
TR_trailHTerm(args);
DF_mkBV((MemPtr)args, dbInd);
} else return FALSE;
} else { //!(DF_isBV(AM_head))
if (DF_isConst(AM_head)) { //constant head
if (uc < DF_constUnivCount(AM_head) &&
HOPU_uniqueConst(AM_head, myArgs, i) &&
HOPU_isEtaExpArgs()) {
TR_trailHTerm(args);
if (DF_isTConst(AM_head))
DF_mkRef((MemPtr)args, AM_head);
else DF_copyAtomic(AM_head, (MemPtr)args);
} else return FALSE;
} else return FALSE; //other sort of terms
} //!(DF_isBV(AM_head))
} //AM_numArgs != 0
args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
} //for loop
return TRUE;
} //nargs != 0
}
/***************************************************************************/
/* BINDING */
/* */
/* Attempt to find bindings for free variables (counter part of mksubst in */
/* the sml pattern unfication code). */
/***************************************************************************/
/* A flag denoting whether new structure is created during the process of */
/* finding substitutions. */
Boolean HOPU_copyFlagGlb = FALSE;
/* Return a non-zero index of a bound variable appears in a list of */
/* arguments. Note the index is the position from the right and the */
/* embedding level is taken into account. */
static int HOPU_bvIndex(int dbInd, DF_TermPtr args, int nargs, int lev)
{
int ind;
dbInd -= lev;
for (ind = nargs; ind > 0; ind--){
DF_TermPtr tPtr = DF_termDeref(args);
if (DF_isBV(tPtr) && (dbInd == DF_bvIndex(tPtr))) return (ind+lev);
//otherwise try the next
args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
}
return 0; //not found
}
/* Return a non-zero index if a constant appears in a list of arguments. */
/* Note the index is the position from the right and the embedding level */
/* is taken into account. */
/* CHANGES have to be made here if the semantics of local constants are */
/* changed with respect to polymorphism. */
static int HOPU_constIndex(DF_TermPtr cPtr, DF_TermPtr args, int nargs, int lev)
{
int ind;
for (ind = nargs; ind > 0; ind--){
DF_TermPtr tPtr = DF_termDeref(args);
if (DF_isConst(tPtr) && DF_sameConsts(tPtr, cPtr)) {
if (DF_isTConst(tPtr)) {
Boolean found = FALSE;
EM_TRY {
HOPU_typesUnify(DF_constType(tPtr), DF_constType(cPtr),
AM_cstTyEnvSize(DF_constTabIndex(cPtr)));
found = TRUE;
} EM_CATCH {//remove types added for ty unif from the PDL
if (EM_CurrentExnType == EM_FAIL) AM_resetTypesPDL();
else EM_RETHROW();
}
if (found) return (ind+lev);
} else return (ind+lev); //cPtr does not have type associated
} //otherwise try the next
args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
}
return 0; //not found
}
/***************************************************************************/
/* BINDING FOR FLEX-FLEX */
/* */
/* Auxiliary functions for solving flex-flex pairs. */
/* Non-LLambda pairs are delayed onto the disagreement list. */
/***************************************************************************/
/* Collect raising components for internal variable in the LLambda case */
/* when it is known it has a higher universe index than the outside llambda*/
/* variable. */
/* It is assumned that the incoming argument vector has a size larger than */
/* zero. */
/* As a result of this process, segments of the argument vectors for both */
/* variables are decided. That for the internal variable is created on the */
/* current top of heap, while that for the outside variable, each */
/* argument of which must be a de Bruijn index, is recorded into an integer*/
/* array which is set by side-effect. */
/* The number returned by this procedure is the length of both of the */
/* argument vector segements. Raising occured when this number is non-zero.*/
/* CHANGES have to be made here if the semantics of local constants are */
/* changed with respect to polymorphism. */
static int HOPU_raise(int varuc, DF_TermPtr args, int nargs, int emblev,
int *args11)
{
int numRaised = 0; //number of args that have been raised
AM_heapError(AM_hreg + nargs * DF_TM_ATOMIC_SIZE);//max possible size
for (; nargs > 0; nargs--){
DF_TermPtr tmPtr = DF_termDeref(args);
if (DF_isConst(tmPtr) && (DF_constUnivCount(tmPtr) <= varuc)){
args11[numRaised] = nargs + emblev; //args11
if (DF_isTConst(tmPtr)) DF_mkRef(AM_hreg, tmPtr); //args21
else DF_copyAtomic(tmPtr, AM_hreg);
AM_hreg += DF_TM_ATOMIC_SIZE;
numRaised++;
}
args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
}
return numRaised;
}
/* Generate the indices for items not to be pruned when the internal */
/* variable is known to have a universe index greater than that of the */
/* external one. */
/* It is assumned that arg vector of the internal flex term has a size */
/* larger than zero. */
/* As a result of this process, segments of the argument vectors for both */
/* variables are decided. That for the internal variable is created on the */
/* current top of heap, while that for the outside variable, each */
/* argument of which must be a de Bruijn index, is recorded into an integer*/
/* array which is set by side-effect. */
/* The number returned by this procedure is the length of both of the */
/* argument vector segements. Pruning occured when this number is smaller */
/* than the size of the arg vector of the internal term. */
static int HOPU_prune(DF_TermPtr args1, int nargs1, DF_TermPtr args2,
int nargs2, int emblev, int *args12)
{
int numNotPruned = 0;
AM_heapError(AM_hreg + nargs2 * DF_TM_ATOMIC_SIZE);//max possible size
for (; nargs2 > 0; nargs2--){
DF_TermPtr tmPtr = DF_termDeref(args2);
if (DF_isConst(tmPtr)) {
int ind = HOPU_constIndex(tmPtr, args1, nargs1, emblev);
if (ind > 0) {
args12[numNotPruned] = ind; //args12
DF_mkBV(AM_hreg, nargs2); //args22
AM_hreg += DF_TM_ATOMIC_SIZE;
numNotPruned ++;
HOPU_copyFlagGlb = TRUE;
} //ind == 0 the argument is pruned
} else {//bv
int ind = DF_bvIndex(tmPtr);
if (ind > emblev) {
int newind = HOPU_bvIndex(ind, args1, nargs1, emblev);
if (newind > 0) {
args12[numNotPruned] = newind; //args12
DF_mkBV(AM_hreg, nargs2); //args22
AM_hreg += DF_TM_ATOMIC_SIZE;
numNotPruned ++;
if (ind != newind) HOPU_copyFlagGlb = TRUE;
} //newind == 0 the argument is pruned
} else {//ind <= lev
args12[numNotPruned] = ind; //args12
DF_mkBV(AM_hreg, nargs2); //args22
AM_hreg += DF_TM_ATOMIC_SIZE;
numNotPruned ++;
}
} //bv
args2 = (DF_TermPtr)(((MemPtr)args2) + DF_TM_ATOMIC_SIZE);
} //for loop
return numNotPruned;
}
/* When the index of the internal variable is less than or equal to that */
/* of the external one in the LLambda case, we have to raise the outside */
/* variable over those constants in the internal list that have smaller */
/* index and we have to prune other constants and bound variables in this */
/* list that are not shared. */
/* It is assumned that the arg vector of the internal flex term has a size */
/* larger than zero. */
/* As a result of this process, the argument vectors for both variables */
/* are decided. That for the outside variable is created on the current */
/* top of heap, while that for the internal variable, each argument of */
/* which must be a de Bruijn index, is recorded into an integer array which*/
/* is set by side-effect. */
/* The number returned by this procedure is the length of both of the */
/* argument vectors. Pruning occured when this number is smaller than the */
/* size of the arg vector of the internal term. */
/* CHANGES have to be made here if the semantics of local constants are */
/* changed with respect to polymorphism. */
static int HOPU_pruneAndRaise(DF_TermPtr args1, int nargs1, DF_TermPtr args2,
int nargs2, int emblev, int *args)
{
int numNotPruned = 0;
AM_heapError(AM_hreg + nargs2 * DF_TM_ATOMIC_SIZE); //max possible size
for (; nargs2 > 0; nargs2 --){
DF_TermPtr tmPtr = DF_termDeref(args2);
if (DF_isBV(tmPtr)){
int ind = DF_bvIndex(tmPtr);
if (ind > emblev) {
int newind = HOPU_bvIndex(ind, args1, nargs1, emblev);
if (newind > 0) {
DF_mkBV(AM_hreg, newind); //args for outside var
AM_hreg += DF_TM_ATOMIC_SIZE;
args[numNotPruned] = nargs2; //args for internal var
numNotPruned ++;
if (ind != newind) HOPU_copyFlagGlb = TRUE;
} // newind == 0, the argument is prubed
} else { //ind <= emblev
DF_mkBV(AM_hreg, ind); //args for outside var
AM_hreg += DF_TM_ATOMIC_SIZE;
args[numNotPruned] = nargs2; //args for internal var
numNotPruned ++;
}
} else { //tmPtr is const
if (DF_constUnivCount(tmPtr) > AM_adjreg){
int ind = HOPU_constIndex(tmPtr, args1, nargs1, emblev);
if (ind > 0) {
DF_mkBV(AM_hreg, ind); //args for outside var
AM_hreg += DF_TM_ATOMIC_SIZE;
args[numNotPruned] = nargs2; //args for internal var
numNotPruned ++;
HOPU_copyFlagGlb = TRUE;
} //else ind = 0, the argument is pruned
} else { //const uc <= AM_adjreg
if (DF_isTConst(tmPtr)) DF_mkRef(AM_hreg, tmPtr);//args out var
else DF_copyAtomic(tmPtr, AM_hreg);
AM_hreg += DF_TM_ATOMIC_SIZE;
args[numNotPruned] = nargs2; //args for internal var
numNotPruned ++;
}
}
args2 = (DF_TermPtr)(((MemPtr)args2) + DF_TM_ATOMIC_SIZE);
} //for loop
return numNotPruned;
}
/* Generating the arguments of a pruning substitution for the case when */
/* when trying to unify two flexible terms of the form */
/* (F a1 ... an) = lam(k, (F b1 ... bm)) */
/* The resulted argument vector is created on the current top of heap, and */
/* the integer returned by this procedure is the length of the argument */
/* vector resulted from pruning. Pruning takes place if this value is */
/* smaller that nargs2. */
/* It is assumed that the sum of n and k is the same as m. */
/* CHANGES have to be made here if the semantics of local constants are */
/* changed with respect to polymorphism. */
static int HOPU_pruneSameVar(DF_TermPtr args1, int nargs1, DF_TermPtr args2,
int nargs2, int lev)
{
if (nargs2 == 0) return 0;
else {
int numNotPruned = 0;
DF_TermPtr tPtr2;
AM_heapError(AM_hreg + nargs2 * DF_TM_ATOMIC_SIZE); //max possible size
nargs1 = nargs2 - nargs1; //reused nargs1
for (; nargs2 > nargs1; nargs2 --){
DF_TermPtr tPtr1 = DF_termDeref(args1);
tPtr2 = DF_termDeref(args2);
if (DF_isBV(tPtr1)){
int ind = DF_bvIndex(tPtr1) + lev;
if (DF_isBV(tPtr2) && (ind == DF_bvIndex(tPtr2))){
DF_mkBV(AM_hreg, nargs2); AM_hreg += DF_TM_ATOMIC_SIZE;
numNotPruned++;
if (nargs2 != ind) HOPU_copyFlagGlb = TRUE;
} //else this argument is pruned
} else {// tPtr1 is a constant
if (DF_isConst(tPtr2) && DF_sameConsts(tPtr1, tPtr2)){
if (DF_isTConst(tPtr2)) {
EM_TRY {
HOPU_typesUnify(DF_constType(tPtr1),DF_constType(tPtr2),
AM_cstTyEnvSize(DF_constTabIndex(tPtr1)));
DF_mkBV(AM_hreg, nargs2); AM_hreg += DF_TM_ATOMIC_SIZE;
numNotPruned++;
HOPU_copyFlagGlb = TRUE;
} EM_CATCH {//remove tys for type unif from the PDL
if (EM_CurrentExnType == EM_FAIL)
AM_resetTypesPDL();
else EM_RETHROW();
} //EM_catch
} else {//no type association
DF_mkBV(AM_hreg, nargs2); AM_hreg+=DF_TM_ATOMIC_SIZE;
numNotPruned++;
HOPU_copyFlagGlb = TRUE;
}
}//else pruned
} //tPtr1 is a constant
args1 = (DF_TermPtr)(((MemPtr)args1) + DF_TM_ATOMIC_SIZE);
args2 = (DF_TermPtr)(((MemPtr)args2) + DF_TM_ATOMIC_SIZE);
} //for (; nargs2 > nargs1; nargs2--)
for (; nargs2 > 0; nargs2--){
tPtr2 = DF_termDeref(args2);
if (DF_isBV(tPtr2) && (DF_bvIndex(tPtr2) == nargs2)){
DF_mkBV(AM_hreg, nargs2); AM_hreg += DF_TM_ATOMIC_SIZE;
numNotPruned++;
} //else pruned
args2 = (DF_TermPtr)(((MemPtr)args2) + DF_TM_ATOMIC_SIZE);
} //for (; nargs2 > 0; nargs2--)
return numNotPruned;
} //nargs2 != 0
}
/* Push a new free variable with given universe count onto the current heap */
/* top. */
static void HOPU_pushVarToHeap(int uc)
{
MemPtr newhtop = AM_hreg + DF_TM_ATOMIC_SIZE;
AM_heapError(newhtop);
DF_mkVar(AM_hreg, uc);
AM_hreg = newhtop;
}
/* Perform substitution to realize pruning and raising for an internal */
/* variable in the LLambda situation when the variable has an index greater*/
/* than that of the outside one */
/* This procedure is also used to perform substitution for flex-flex pairs */
/* with same variable heads in the LLambda situation. */
static void HOPU_mkPandRSubst(DF_TermPtr hPtr, DF_TermPtr args, int nargs,
DF_TermPtr vPtr, int nabs)
{
TR_trailTerm(vPtr); AM_bndFlag = ON;
if (nargs == 0) {
if (nabs == 0) DF_mkRef((MemPtr)vPtr, hPtr);
else DF_mkLam((MemPtr)vPtr, nabs, hPtr);
} else { //nargs > 0
DF_TermPtr tPtr = (DF_TermPtr)AM_hreg;
AM_heapError(AM_hreg + DF_TM_APP_SIZE);
AM_arityError(nargs);
DF_mkApp(AM_hreg, nargs, hPtr, args); //application body
AM_hreg += DF_TM_APP_SIZE;
AM_embedError(nabs);
if (nabs == 0) DF_mkRef((MemPtr)vPtr, tPtr);
else DF_mkLam((MemPtr)vPtr, nabs, tPtr);
}
}
/* Perform substitution to realize pruning and raising for an internal */
/* variable in the LLambda situation when the variable has an index smaller*/
/* than or equal to that of the outside one */
/* The arguments of the substitution which should be de Bruijn indices */
/* are given by an integer array. */
static void HOPU_mkPrunedSubst(DF_TermPtr hPtr, int *args, int nargs,
DF_TermPtr vPtr, int nabs)
{
AM_bndFlag = ON;
TR_trailTerm(vPtr);
if (nargs == 0) {
if (nabs == 0) DF_mkRef((MemPtr)vPtr, hPtr);
else DF_mkLam((MemPtr)vPtr, nabs, hPtr);
} else { //nargs > 0;
DF_TermPtr argvec = (DF_TermPtr)AM_hreg, appPtr;
int i;
AM_heapError(AM_hreg + DF_TM_APP_SIZE + nargs * DF_TM_ATOMIC_SIZE);
for (i = 0; i < nargs; i++){//commit bvs in args onto heap
DF_mkBV(AM_hreg, args[i]);
AM_hreg += DF_TM_ATOMIC_SIZE;
}
appPtr = (DF_TermPtr)AM_hreg;
DF_mkApp(AM_hreg, nargs, hPtr, argvec);
AM_hreg += DF_TM_APP_SIZE;
if (nabs == 0) DF_mkRef((MemPtr)vPtr, appPtr);
else DF_mkLam((MemPtr)vPtr, nabs, appPtr);
}
}
/* Generating the partial structure of a substitution to realize pruning */
/* and raising for an outside variable in the LLambda situation when the */
/* variable has an index smaller than that of the internal one. */
/* The arguments of the susbsitution consists of two segments of de Burijn */
/* indices, which are given by two integer arrays respectively. */
static DF_TermPtr HOPU_mkPandRTerm(DF_TermPtr hPtr, int args1[], int nargs1,
int args2[], int nargs2)
{
if ((nargs1 == 0) && (nargs2 == 0)) return hPtr;
else {
DF_TermPtr args = (DF_TermPtr)AM_hreg, rtPtr;
int nargs = nargs1 + nargs2; //new arity (non-zero)
int i;
AM_arityError(nargs);
AM_heapError(AM_hreg + DF_TM_APP_SIZE + nargs * DF_TM_ATOMIC_SIZE);
for (i = 0; i < nargs1 ; i++){ //commit bvs in a11 onto heap
DF_mkBV(AM_hreg, args1[i]);
AM_hreg += DF_TM_ATOMIC_SIZE;
}
for (i = 0; i < nargs2 ; i++){ //commit bvs in a12 onto heap
DF_mkBV(AM_hreg, args2[i]);
AM_hreg += DF_TM_ATOMIC_SIZE;
}
rtPtr = (DF_TermPtr)AM_hreg;
DF_mkApp(AM_hreg, nargs, hPtr, args);
AM_hreg += DF_TM_APP_SIZE;
return rtPtr;
}
}
/* Generating the partial structure of a substitution to realize pruning */
/* and raising for an internal variable in the LLambda situation when the */
/* variable has an index greater than or equal to that of the outside one. */
static DF_TermPtr HOPU_mkPrunedTerm(DF_TermPtr hPtr, DF_TermPtr args, int nargs)
{
if (nargs == 0) return hPtr;
else {
DF_TermPtr rtPtr = (DF_TermPtr)AM_hreg;
AM_heapError(AM_hreg + DF_TM_APP_SIZE);
DF_mkApp(AM_hreg, nargs, hPtr, args);
AM_hreg += DF_TM_APP_SIZE;
return rtPtr;
}
}
/* Find the (partial) structure of the substitution for a flex head of a */
/* LLambda term corresponding to an internal flex term which is known to be */
/* LLambda. The internal free variable is bound to a proper substitution as */
/* side-effect. */
/* The arguments of this procedure are: */
/* args1 : reference to the argument vector of the outside flex term */
/* nargs1: number of arguments of the outside flex term */
/* uc : universe count of the internal free variable */
/* tPtr2 : refers to the dereference of ABSTRACTION BODY of the internal */
/* flex term */
/* fhPtr : refers to the head of the internal flex term */
/* args2 : refers to the argument vector of the internal flex term */
/* nargs2: number of arguments of the internal flex term */
/* lev : the abstraction context of the internal flex term */
/* Note that the outside free variable and its universe count are assumed to */
/* be given by the global variables (registers) AM_vbbreg and AM_adjreg. */
static DF_TermPtr HOPU_flexNestedLLambda(DF_TermPtr args1, int nargs1, int uc,
DF_TermPtr tPtr2, DF_TermPtr fhPtr, DF_TermPtr args2,
int nargs2, int lev)
{
DF_TermPtr bnd; //(partial) binding for the outside free var
MemPtr oldhtop = AM_hreg;
DF_TermPtr heapArgs = (DF_TermPtr)AM_hreg;
if (AM_adjreg < uc){
int *args11 = NULL, *args12 = NULL; //hold args of bnd of the outside v
int nargs11 = 0, nargs12 = 0;
if (nargs1 != 0) {
args11 = (int*)EM_malloc(nargs1 * sizeof(int));
nargs11 = HOPU_raise(uc, args1, nargs1, lev, args11);
}
if (nargs2 != 0) {
args12 = (int*)EM_malloc(nargs2 * sizeof(int));
nargs12 = HOPU_prune(args1, nargs1, args2, nargs2, lev, args12);
}
if ((nargs11 == 0) && (nargs12 == nargs2)) {//neither raised nor pruned
AM_hreg = oldhtop; //the internal free var remains unbound
TR_trailTerm(fhPtr); AM_bndFlag = ON;
DF_modVarUC(fhPtr, AM_adjreg);
if (HOPU_copyFlagGlb)
bnd = HOPU_mkPandRTerm(fhPtr, args11, nargs11, args12, nargs12);
else bnd = tPtr2;
} else { //raised or pruned
DF_TermPtr newVar = (DF_TermPtr)AM_hreg;
HOPU_pushVarToHeap(AM_adjreg);
HOPU_mkPandRSubst(newVar, heapArgs, nargs11+nargs12, fhPtr, nargs2);
bnd = HOPU_mkPandRTerm(newVar, args11, nargs11, args12, nargs12);
HOPU_copyFlagGlb = TRUE;
}
if (nargs1 != 0) free(args11); if (nargs2 != 0) free(args12);
} else { //AM_adjreg >= uc
int *newargs2 = NULL;
int nnewargs2 = 0;
if (nargs2 != 0) {
newargs2 = (int*)EM_malloc(nargs2 * sizeof(int));
nnewargs2 = HOPU_pruneAndRaise(args1,nargs1,args2,nargs2,lev,
newargs2);
}
if (nnewargs2 == nargs2){//not pruned
if (HOPU_copyFlagGlb)
bnd = HOPU_mkPrunedTerm(fhPtr, heapArgs, nnewargs2);
else { AM_hreg = oldhtop; bnd = tPtr2; }
} else { //pruned
DF_TermPtr newVar = (DF_TermPtr)AM_hreg;
HOPU_pushVarToHeap(uc);
HOPU_mkPrunedSubst(newVar, newargs2, nnewargs2, fhPtr, nargs2);
bnd = HOPU_mkPrunedTerm(newVar, heapArgs, nnewargs2);
HOPU_copyFlagGlb = TRUE;
}
if (nargs2 != 0) free(newargs2);
} //AM_adjreg >= uc
return bnd;
}
/* Checking the arguments of a flex (non-LLambda) term to see whetehr a */
/* free variable same as that currently in the AM_vbbreg register, a free */
/* variable with higher univ count than that currently in the AM_adjreg */
/* register, a constant with higher univ count than that currently in */
/* AM_adjreg, or a de Bruijn index bound by abstractions over the variable */
/* for which a substitution is being constructed occurs. */
/* If one of the situations occurs, exception is raised. */
static void HOPU_flexCheck(DF_TermPtr args, int nargs, int emblev)
{
for (; nargs > 0; nargs --){
int nemblev;
HN_hnorm(args);
nemblev = emblev + AM_numAbs;
if (AM_rigFlag){
if (DF_isBV(AM_head)) {
if (DF_bvIndex(AM_head) > nemblev) EM_THROW(EM_FAIL);
} else {
if (DF_isConst(AM_head)&&(DF_constUnivCount(AM_head)>AM_adjreg))
EM_THROW(EM_FAIL);
} //otherwise succeeds
} else { //AM_rigFlag == FALSE
if ((AM_vbbreg == AM_head) || (DF_fvUnivCount(AM_head)>AM_adjreg))
EM_THROW(EM_FAIL);
}
HOPU_flexCheck(AM_argVec, AM_numArgs, nemblev);
args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
}
}
/* This version of flexCheckC is needed in the compiled form of pattern */
/* unification. The essential difference from the other version is that the */
/* variable being bound is already partially bound to a structure. */
/* The difference from the other procedure is the head normalization */
/* procedure invoked is one performs the occurs checking on partially bound */
/* variables */
static void HOPU_flexCheckC(DF_TermPtr args, int nargs, int emblev)
{
for (; nargs > 0; nargs--){
int nemblev;
HN_hnormOcc(args);
nemblev = emblev + AM_numAbs;
if (AM_rigFlag) {
if (DF_isBV(AM_head)) {
if (DF_bvIndex(AM_head) > nemblev) EM_THROW(EM_FAIL);
} else {
if (DF_isConst(AM_head)&&(DF_constUnivCount(AM_head)>AM_adjreg))
EM_THROW(EM_FAIL);
} //otherwise succeeds
} else //AM_rigFlag == FALSE
if (DF_fvUnivCount(AM_head) > AM_adjreg) EM_THROW(EM_FAIL);
HOPU_flexCheckC(AM_argVec, AM_numArgs, nemblev);
args = (DF_TermPtr)(((MemPtr)args)+DF_TM_ATOMIC_SIZE);
}
}
/* Generating a term on the top of heap which is to be added into a */
/* disagreement pair. */
/* The term has the following structure: */
/* (h [|a1, 0, lev, nil|] ... [|an, 0, lev, nil|] #lev ... #1) */
/* It is assumed that nargs and lev are not equal to zero. */
static void HOPU_mkTermNLL(DF_TermPtr h, DF_TermPtr args, int nargs, int lev)
{
int newArity = nargs + lev;
MemPtr newArgs = AM_hreg + DF_TM_APP_SIZE; //spare app (head) size on heap
AM_arityError(newArity);
AM_heapError(AM_hreg + nargs*DF_TM_SUSP_SIZE + newArity*DF_TM_ATOMIC_SIZE
+ DF_TM_APP_SIZE);
DF_mkApp(AM_hreg, newArity, h, (DF_TermPtr)newArgs);
AM_hreg += (DF_TM_APP_SIZE + newArity * DF_TM_ATOMIC_SIZE);//alloc arg vec
for (; nargs > 0; nargs--){ //[|ai, 0, lev, nil|], for i <= nargs
DF_mkRef(newArgs, (DF_TermPtr)AM_hreg);
DF_mkSusp(AM_hreg, 0, lev, DF_termDeref(args), DF_EMPTY_ENV);
newArgs += DF_TM_ATOMIC_SIZE; AM_hreg += DF_TM_SUSP_SIZE;
args = (DF_TermPtr)(((MemPtr)args) + DF_TM_ATOMIC_SIZE);
}
for (; lev > 0; lev--){ //#i, for i <= lev
DF_mkBV(newArgs, lev);
newArgs += DF_TM_ATOMIC_SIZE;
}
}
/* Generating a partial subsitution for the free head of a LLambda term */
/* corresponding to an internal flex term which is known to be non-LLambda.*/
/* The partial substitution is of form: */
/* (h #n ... #1) */
/* It is assumed that n is not equal to zero. */
static void HOPU_mkSubstNLL(DF_TermPtr h, int n)
{
AM_arityError(n);
AM_heapError(AM_hreg + DF_TM_APP_SIZE + n * DF_TM_ATOMIC_SIZE);
DF_mkApp(AM_hreg, n, h, (DF_TermPtr)(AM_hreg + DF_TM_APP_SIZE));
AM_hreg += DF_TM_APP_SIZE;
for (; n > 0; n--){
DF_mkBV(AM_hreg, n);
AM_hreg += DF_TM_ATOMIC_SIZE;
}
}
/* Try to solve G = ...(F a1 ... an)..., where F and G are different free */
/* variables, and (F a1 ... an) is non-LLambda. */
/* Either G is bound to (F a1 ... an) or an exception is raised. In the */
/* latter case, the caller of this function is responsible to add a */
/* disagreement pair to the live list. */
static void HOPU_bndVarNestedFlex(DF_TermPtr fhPtr, DF_TermPtr args, int nargs,
int lev)
{
HOPU_flexCheck(args, nargs, lev);
if (DF_fvUnivCount(fhPtr) > AM_adjreg) {
TR_trailTerm(fhPtr);
AM_bndFlag = ON;
DF_modVarUC(fhPtr, AM_adjreg);
}
}
/* Try to find the (partial) structure of the substitution for a flex head */
/* of a LLambda term corresponding to an internal flex term which is not */
/* known to be LLambda. */
/* If the internal flex term is LLambda, HOPU_flexNestedLLambda is invoked */
/* to generate the (parital) substitution for the outside variable, and */
/* perform proper substitutions on the internal free variable if necessary. */
/* Otherwise, a disagreement pair is added into the live list. */
static DF_TermPtr HOPU_flexNestedSubst(DF_TermPtr args1, int nargs1,
DF_TermPtr fhPtr, DF_TermPtr args2,
int nargs2, DF_TermPtr tmPtr, int emblev)
{
DF_TermPtr bnd;
int varuc = DF_fvUnivCount(fhPtr);
if (HOPU_isLLambda(varuc, nargs2, args2)){
if (fhPtr == AM_vbbreg) EM_THROW(EM_FAIL); //occurs check
bnd = HOPU_flexNestedLLambda(args1, nargs1, varuc, tmPtr, fhPtr, args2,
nargs2, emblev);
} else {// the internal flex term is not LLambda: delay (opt possible)
DF_TermPtr newVar;
DF_TermPtr newTerm;
Boolean found = FALSE;
if ((fhPtr != AM_vbbreg) && (nargs1 == 0)) {
EM_TRY{
HOPU_bndVarNestedFlex(fhPtr, args2, nargs2, emblev);
bnd = tmPtr;
found = TRUE;
} EM_CATCH {if (EM_CurrentExnType != EM_FAIL) EM_RETHROW();}
}
if (!found) {
newVar = (DF_TermPtr)AM_hreg;
HOPU_pushVarToHeap(AM_adjreg);
HOPU_copyFlagGlb = TRUE;
if ((nargs1 == 0) && (emblev == 0)) {
bnd = newVar;
AM_addDisPair(bnd, tmPtr);
} else {
newTerm = (DF_TermPtr)AM_hreg;
HOPU_mkTermNLL(newVar, args1, nargs1, emblev);
AM_addDisPair(newTerm, tmPtr);
bnd = (DF_TermPtr)AM_hreg;
HOPU_mkSubstNLL(newVar, emblev + nargs1);
}
}
}
return bnd;
}
/* This version of flexNestedSubst is needed in the compiled form of pattern */
/* unification. The essential difference from the other version is that the */
/* variable being bound is already partially bound to a structure. */
/* The difference from the other procedure is first the head normalization */
/* process invokded is one performs occurs checking on partially bound */
/* variables, and second, the "top-level" flexible term is a free variable: */
/* so there is no need to distinguish whether the other flex term is Llambda */
/* or not: the substitution can be found by an invocation of flexCheckC */
DF_TermPtr HOPU_flexNestedSubstC(DF_TermPtr fhPtr, DF_TermPtr args, int nargs,
DF_TermPtr tmPtr, int emblev)
{
DF_TermPtr bnd, newVar, newTerm;
int varuc;
Boolean found = FALSE;
EM_TRY {
HOPU_flexCheckC(args, nargs, emblev);
if (DF_fvUnivCount(fhPtr) > AM_adjreg){
TR_trailTerm(fhPtr);
AM_bndFlag = ON;
DF_modVarUC(fhPtr, AM_adjreg);
}
bnd = tmPtr;
found = TRUE;
} EM_CATCH { if (EM_CurrentExnType != EM_FAIL) EM_RETHROW(); }
if (!found) {
varuc = DF_fvUnivCount(fhPtr);
if (HOPU_isLLambda(varuc, nargs, args)){
bnd = HOPU_flexNestedLLambda(NULL, 0, varuc, tmPtr, fhPtr, args, nargs,
emblev);
} else {//otherwise delay this pair onto the live list
HOPU_copyFlagGlb = TRUE;
newVar = (DF_TermPtr)AM_hreg;
HOPU_pushVarToHeap(AM_adjreg);
if (emblev == 0) {
bnd = newVar;
AM_addDisPair(bnd, tmPtr);
} else {
newTerm = (DF_TermPtr)AM_hreg;
HOPU_mkTermNLL(newVar, NULL, 0, emblev);
AM_addDisPair(newTerm, tmPtr);
bnd = (DF_TermPtr)AM_hreg;
HOPU_mkSubstNLL(newVar, emblev);
}
}
}
return bnd;
}
/* Try to solve G = (F a1 ... an), where F and G are different free */
/* variables, and (F a1 ... an) is non-LLambda. */
/* Either G is bound to (F a1 ... an) or an exception is raised. In the */
/* latter case, the caller of this function is responsible to add a */
/* disagreement pair to the live list. */
static void HOPU_bndVarFlex(DF_TermPtr vPtr, DF_TermPtr fPtr, DF_TermPtr fhPtr,
DF_TermPtr args, int nargs)
{
AM_vbbreg = vPtr; AM_adjreg = DF_fvUnivCount(vPtr);
HOPU_flexCheck(args, nargs, 0);
if (DF_fvUnivCount(fhPtr) > AM_adjreg) {
TR_trailTerm(fPtr);
AM_bndFlag = ON;
DF_modVarUC(fhPtr, AM_adjreg);
}
TR_trailTerm(vPtr);
AM_bndFlag = ON;
DF_mkRef((MemPtr)vPtr, fPtr);
}
/* Try to solve (F a1 ... an) = lam(k, (G b1 ... bm)), where F and G are */
/* both free variables. */
/* The arguments are: */
/* tPtr1 : reference to the ABSTRACTION BODY of the first flex term */
/* h1 : reference to the flex head of the first term */
/* nargs1: number of arguments of the first flex term */
/* args1 : reference to the argument vector of the first flex term */
/* tPtr2 : reference to the ABSTRACTION BODY of the second flex term */
/* h2 : reference to the flex head of the second flex term */
/* nargs2: number of arguments of the second flex term */
/* args2 : reference to the argument vector of the second flex term */
/* lev : abstraction context of the second term with respect to the */
/* first one. */
/* */
/* Non-Llambda pairs could be encountered during this process, and in */
/* this situation, the pair is delayed onto the disagreement list. */
static void HOPU_flexMkSubst(DF_TermPtr tPtr1, DF_TermPtr h1, int nargs1,
DF_TermPtr args1, DF_TermPtr tPtr2, DF_TermPtr h2,
int nargs2, DF_TermPtr args2, int lev)
{
int uc = DF_fvUnivCount(h1);
if (HOPU_isLLambda(uc, nargs1, args1)){ //the first term is LLambda
DF_TermPtr bndBody;
if (h1 == h2) { //same variable (comparing addresses)
if (HOPU_isLLambda(uc, nargs2, args2)) {//same var common uc
MemPtr oldhtop = AM_hreg;
DF_TermPtr newArgs = (DF_TermPtr)AM_hreg;
HOPU_copyFlagGlb = FALSE;
nargs1 = HOPU_pruneSameVar(args1, nargs1, args2, nargs2, lev);
if ((nargs1 != nargs2) || HOPU_copyFlagGlb){
DF_TermPtr newVar = (DF_TermPtr)AM_hreg;
HOPU_pushVarToHeap(uc);
HOPU_mkPandRSubst(newVar, newArgs, nargs1, h1, nargs2);
} else AM_hreg = oldhtop; //unbound
} else { //(F a1 ... an)[ll] = (lam(k, (F b1 ... bm)))[non-ll]
if (lev == 0) AM_addDisPair(tPtr1, tPtr2);
else {
MemPtr nhtop = AM_hreg + DF_TM_LAM_SIZE;
DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg;
AM_heapError(AM_hreg);
DF_mkLam(AM_hreg, lev, tPtr2);
AM_hreg = nhtop;
AM_addDisPair(tPtr1, tmPtr);
} //(lev != 0)
} //tPtr2 not LLambda
} else { //different variable
int nabs;
AM_vbbreg = h1; AM_adjreg = uc; //set regs for occ
HOPU_copyFlagGlb = FALSE;
bndBody = HOPU_flexNestedSubst(args1, nargs1, h2, args2, nargs2,
tPtr2, lev);
nabs = lev + nargs1;
TR_trailTerm(h1); AM_bndFlag = ON;
if (nabs == 0) DF_mkRef((MemPtr)h1, bndBody);
else {
AM_embedError(nabs);
DF_mkLam((MemPtr)h1, nabs, bndBody);
}
} //different variable
} else { //the first term is non-LLambda
Boolean found = FALSE;
if ((nargs2 == 0) && (lev == 0) && (h1 != h2)) { // (F t1 ... tm) = G
EM_TRY{
HOPU_bndVarFlex(h2, tPtr1, h1, args1, nargs1);
found = TRUE;
} EM_CATCH {
if (EM_CurrentExnType != EM_FAIL) EM_RETHROW();
}
}
if (!found) {
if (lev == 0) AM_addDisPair(tPtr1, tPtr2);
else {
MemPtr nhtop = AM_hreg + DF_TM_LAM_SIZE;
DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg;
AM_heapError(AM_hreg);
DF_mkLam(AM_hreg, lev, tPtr2);
AM_hreg = nhtop;
AM_addDisPair(tPtr1, tmPtr);
} //(lev != 0)
}
} //the first term is non-LLambda
}
/* The counterpart of HOPU_flexMkSubst invoked from HOPU_patternUnifyPair. */
/* Care is taken to avoid making a reference to a stack address in binding */
/* and creating disagreement pairs. */
/* It is assumed that the first term (F a1 ... an) given by its */
/* is not embedded in any abstractions. */
static void HOPU_flexMkSubstGlb(DF_TermPtr tPtr1, DF_TermPtr h1, int nargs1,
DF_TermPtr args1,
DF_TermPtr tPtr2, DF_TermPtr h2, int nargs2,
DF_TermPtr args2,
DF_TermPtr topPtr2, int lev)
{
int uc = DF_fvUnivCount(h1);
if (HOPU_isLLambda(uc, nargs1, args1)) { //the first term is LLambda
DF_TermPtr bndBody;
if (h1 == h2) { //same variable (comparing addresses)
if (HOPU_isLLambda(uc, nargs2, args2)){//same var; common uc
MemPtr oldhtop = AM_hreg;
DF_TermPtr newArgs = (DF_TermPtr)AM_hreg;
HOPU_copyFlagGlb = FALSE;
nargs1 = HOPU_pruneSameVar(args1, nargs1, args2, nargs2, lev);
if ((nargs1 != nargs2) || HOPU_copyFlagGlb) {
DF_TermPtr newVar = (DF_TermPtr)AM_hreg;
HOPU_pushVarToHeap(uc);
HOPU_mkPandRSubst(newVar, newArgs, nargs1, h1, nargs2);
} else AM_hreg = oldhtop; //variable remain unbound
} else { //(F a1 ... an)[ll] = (lam(k, (F b1 ... bm)))[non-ll]
//non-LLambda term must locate on the heap
if (nargs1 == 0) tPtr1 = HOPU_globalizeFlex(tPtr1);
if (lev == 0) AM_addDisPair(tPtr1, tPtr2);
else AM_addDisPair(tPtr1, DF_termDeref(topPtr2));
} //tPtr2 not LLambda
} else { //different variable
int nabs;
AM_vbbreg = h1; AM_adjreg = uc; //set regs for occ
HOPU_copyFlagGlb = FALSE;
bndBody = HOPU_flexNestedSubst(args1, nargs1, h2, args2, nargs2,
tPtr2, lev);
nabs = nargs1 + lev;
TR_trailTerm(h1); AM_bndFlag = ON;
if (HOPU_copyFlagGlb == FALSE)
bndBody = HOPU_globalizeFlex(bndBody);
if (nabs == 0) DF_mkRef((MemPtr)h1, bndBody);
else {
AM_embedError(nabs);
DF_mkLam((MemPtr)h1, nabs, bndBody);
}
}
} else {//the first term is non-LLambda (must locate on heap)
Boolean found = FALSE;
if ((nargs2 == 0) && (lev == 0) && (h1 != h2)) {//(F t1...tm)[nll] = G
EM_TRY {
HOPU_bndVarFlex(h2, tPtr1, h1, args1, nargs1);
found = TRUE;
} EM_CATCH {
if (EM_CurrentExnType == EM_FAIL)
tPtr2 = HOPU_globalizeFlex(tPtr2);
else EM_RETHROW();
}
}
if (!found) {
if (lev == 0) AM_addDisPair(tPtr1, tPtr2);
else AM_addDisPair(tPtr1, DF_termDeref(topPtr2));
}
} //the first term is non-LLambda
}
/***************************************************************************/
/* BINDING FOR FLEX-RIGID */
/* */
/* Auxiliary functions for solving flex-rigid pairs. */
/* Non-LLambda pairs are delayed onto the disagreement list. */
/***************************************************************************/
/* Try to find the (partial) binding of the head of a flex term correponding */
/* to a rigid atom during the process of unifying the flex term with a */
/* rigid one. The global variable HOPU_copyFlagGlb is used to indicate */
/* whether a new term is created during this process. */
/* Note it is assumed that rPtr refers to the dereference of a rigid atom */
/* or cons. */
static DF_TermPtr HOPU_getHead(DF_TermPtr rPtr, DF_TermPtr args, int nargs,
int emblev)
{
DF_TermPtr rtPtr;
switch(DF_termTag(rPtr)){
case DF_TM_TAG_CONST:{
if (DF_constUnivCount(rPtr) > AM_adjreg){
MemPtr newhtop;
int ind = HOPU_constIndex(rPtr, args, nargs, emblev);
if (ind == 0) EM_THROW(EM_FAIL); //occurs-check
AM_embedError(ind);
newhtop = AM_hreg + DF_TM_ATOMIC_SIZE;
AM_heapError(newhtop);
HOPU_copyFlagGlb = TRUE; //new structure is created
rtPtr = (DF_TermPtr)AM_hreg; //create a db on the heap top
DF_mkBV(AM_hreg, ind);
AM_hreg = newhtop;
} else rtPtr = rPtr; //DF_constUnivCount(rPtr <= AM_adjreg)
break;
}
case DF_TM_TAG_BVAR: {
int dbInd = DF_bvIndex(rPtr);
if (dbInd > emblev){
int ind = HOPU_bvIndex(dbInd, args, nargs, emblev);
if (ind == 0) EM_THROW(EM_FAIL); //occurs-check
AM_embedError(ind);
if (ind == dbInd) rtPtr = rPtr; //use the old db term
else { //create a db on the heap top
MemPtr newhtop = AM_hreg + DF_TM_ATOMIC_SIZE;
AM_heapError(newhtop);
HOPU_copyFlagGlb = TRUE; //new structure is created
rtPtr = (DF_TermPtr)AM_hreg;
DF_mkBV(AM_hreg, ind);
AM_hreg = newhtop;
}
} else rtPtr = rPtr; //dbInd <= emlev
break;
}
default: { rtPtr = rPtr; break;} //other rigid head: cons,nil,int,fl,str
} //switch
return rtPtr;
}
/* Create a new cons or app term on the current heap top. */
static void HOPU_mkConsOrApp(DF_TermPtr tmPtr, DF_TermPtr funcPtr,
DF_TermPtr argvec, int nargs)
{
MemPtr newhtop;
if (DF_isCons(tmPtr)) {
newhtop = AM_hreg + DF_TM_CONS_SIZE;
AM_heapError(newhtop);
DF_mkCons(AM_hreg, argvec);
} else {// application
newhtop = AM_hreg + DF_TM_APP_SIZE;
AM_heapError(newhtop);
DF_mkApp(AM_hreg, nargs, funcPtr, argvec);
}
AM_hreg = newhtop;
}
/* Try to find the (partial) binding of the head of a flex term when */
/* unifying it with a rigid term possible under abstractions. */
/* The arguments are: */
/* fargs: reference to the arguments of the flex term */
/* fnargs: number of arguments of the flex term */
/* rhPtr: reference to the rigid head */
/* rPtr: reference to the ABSTRACTION BODY of the rigid term */
/* rargs: reference to the arguments of the rigid term */
/* rnargs: number of arguments of the rigid term */
/* emblev: abstraction context of the rigid term */
/* The global variable HOPU_copyFlagGlb is used to indicate whether new */
/* term is created in this process. */
/* Note that if the rigid term is app or cons, it is first assumed that */
/* a new argument vector is to be created. However, after all the args in */
/* the binding are calculated, a checking is made on whether this is */
/* really necessary. If it is not, the old arg vector is used, and the new */
/* one is abandoned. (Heap space for it is deallocated.) */
/* It is assumed that the flexible head and its universe count are */
/* in registers AM_vbbreg and AM_adjreg. */
static DF_TermPtr HOPU_rigNestedSubst(DF_TermPtr fargs, int fnargs,
DF_TermPtr rhPtr, DF_TermPtr rPtr,
DF_TermPtr rargs, int rnargs, int emblev)
{
rhPtr = HOPU_getHead(rhPtr, fargs, fnargs, emblev); //head of the binding
if (rnargs == 0) return rhPtr; //the rigid term is atomic
else { //the rigid term is cons or app
Boolean myCopyFlagHead = HOPU_copyFlagGlb, myCopyFlagArgs = FALSE;
int i;
MemPtr oldHreg = AM_hreg; //the old heap top
MemPtr argLoc = AM_hreg; //arg vector location
DF_TermPtr newArgs = (DF_TermPtr)AM_hreg; //new argument vector
DF_TermPtr oldArgs = rargs; //old argument vector
AM_heapError(AM_hreg + rnargs * DF_TM_ATOMIC_SIZE);
AM_hreg += rnargs * DF_TM_ATOMIC_SIZE; //allocate space for argvec
HOPU_copyFlagGlb = FALSE;
for (i = 0; i < rnargs; i++){
DF_TermPtr bnd;
int nabs;
MemPtr tmpHreg = AM_hreg;
HN_hnorm(rargs); nabs = AM_numAbs; //dereference of hnf
if (AM_hreg != tmpHreg) {myCopyFlagArgs = TRUE; }
if (AM_rigFlag){
bnd = HOPU_rigNestedSubst(fargs, fnargs, AM_head,
HOPU_lamBody(rargs), AM_argVec, AM_numArgs, nabs+emblev);
} else { //AM_rigFlag = FALSE
bnd = HOPU_flexNestedSubst(fargs, fnargs, AM_head, AM_argVec,
AM_numArgs, HOPU_lamBody(rargs), nabs+emblev);
}
if (nabs == 0) DF_mkRef(argLoc, bnd); //compact atomic??
else DF_mkLam(argLoc, nabs, bnd);
argLoc += DF_TM_ATOMIC_SIZE; //note: abs has atomic size
if (HOPU_copyFlagGlb) {myCopyFlagArgs=TRUE; HOPU_copyFlagGlb=FALSE;}
rargs = (DF_TermPtr)(((MemPtr)rargs)+DF_TM_ATOMIC_SIZE); //next arg
} //for loop
if (myCopyFlagArgs) {
DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg; //new cons or app
HOPU_mkConsOrApp(rPtr, rhPtr, newArgs, rnargs);
HOPU_copyFlagGlb = TRUE;
return tmPtr;
} else { //myCopyFlagBody == FALSE
AM_hreg = oldHreg; //deallocate space for the argument vector
//note no new terms are created form any argument
if (myCopyFlagHead){
DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg; //new cons or app
HOPU_mkConsOrApp(rPtr, rhPtr, oldArgs, rnargs);
HOPU_copyFlagGlb = TRUE;
return tmPtr;
} else return rPtr; //myCopyFlagHead==FALSE, myCopyFlagArgs==FALSE
}
}//rnargs > 0
}
/* This version of rigNestedSubstC is needed in the compiled form of pattern */
/* unification. The essential difference from the other version is that the */
/* variable being bound is already partially bound to a structure. */
/* The difference from the other procedure is first the head normalization */
/* procedure invoked is one performs the occurs checking on partially bound */
/* variables, and second, the incoming flexible term is in fact a free */
/* variable. */
DF_TermPtr HOPU_rigNestedSubstC(DF_TermPtr rhPtr, DF_TermPtr rPtr,
DF_TermPtr rargs, int rnargs, int emblev)
{
rhPtr = HOPU_getHead(rhPtr, NULL, 0, emblev);
if (rnargs == 0) return rhPtr;
else {
Boolean myCopyFlagHead = HOPU_copyFlagGlb, myCopyFlagArgs = FALSE;
int i;
MemPtr oldHreg = AM_hreg; //the old heap top
MemPtr argLoc = AM_hreg; //arg vector location
DF_TermPtr newArgs = (DF_TermPtr)AM_hreg; //new arg vector
DF_TermPtr oldArgs = rargs; //old arg vector
AM_heapError(AM_hreg + rnargs * DF_TM_ATOMIC_SIZE);
AM_hreg += rnargs * DF_TM_ATOMIC_SIZE; //alloc space for new args
HOPU_copyFlagGlb = FALSE;
for (i = 0; i < rnargs; i++) {
DF_TermPtr bnd;
int nabs;
MemPtr tmpHreg = AM_hreg;
HN_hnormOcc(rargs); nabs = AM_numAbs;
if (tmpHreg != AM_hreg) {myCopyFlagArgs = TRUE; }
if (AM_rigFlag)
bnd = HOPU_rigNestedSubstC(AM_head, HOPU_lamBody(rargs),
AM_argVec, AM_numArgs, nabs+emblev);
else //AM_rigFlag == FALSE
bnd = HOPU_flexNestedSubstC(AM_head, AM_argVec, AM_numArgs,
HOPU_lamBody(rargs), nabs+emblev);
if (nabs == 0) DF_mkRef(argLoc, bnd);
else DF_mkLam(argLoc, nabs, bnd);
argLoc += DF_TM_ATOMIC_SIZE;
if (HOPU_copyFlagGlb) {myCopyFlagArgs=TRUE; HOPU_copyFlagGlb=FALSE;}
rargs = (DF_TermPtr)(((MemPtr)rargs)+DF_TM_ATOMIC_SIZE);
} //for loop
if (myCopyFlagArgs) {
DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg; //new cons or app
HOPU_mkConsOrApp(rPtr, rhPtr, newArgs, rnargs);
HOPU_copyFlagGlb = TRUE;
return tmPtr;
} else { //myCopyFlagArgs == FALSE
AM_hreg = oldHreg;//deallocate space for arg vector
if (myCopyFlagHead) {
DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg;
HOPU_mkConsOrApp(rPtr, rhPtr, oldArgs, rnargs);
HOPU_copyFlagGlb = TRUE;
return tmPtr;
} else return rPtr; ////myCopyFlagHead==FALSE, myCopyFlagArgs==FALSE
}
}//rnargs > 0
}
/* Try to solve (F a1 ... an) = lam(k, (r b1 ... bm)), where r is rigid. */
/* The arguments are: */
/* fPtr : reference to the ABSTRACTION BODY of the flex term */
/* fhPtr : reference to the flex head */
/* fnargs: number of arguments of the flex term */
/* fargs : reference to the argument vector of the flex term */
/* rPtr : reference to the ABSTRACTION BODY of the rigid term */
/* rhPtr : reference to the rigid head (Note it could be cons) */
/* rnargs: number of arguments of the rigid term */
/* rargs : reference to the argument vector of the rigid term */
/* */
/* Non-Llambda pairs could be encountered during this process, and in */
/* this situation, the pair is delayed onto the disagreement list. */
static void HOPU_rigMkSubst(DF_TermPtr fPtr, DF_TermPtr fhPtr, int fnargs,
DF_TermPtr fargs, DF_TermPtr rPtr, DF_TermPtr rhPtr,
int rnargs, DF_TermPtr rargs, int emblev)
{
int uc = DF_fvUnivCount(fhPtr);
if (HOPU_isLLambda(uc, fnargs, fargs)){//Llambda pattern
DF_TermPtr bndBody; //abs body of bnd of the fv
int nabs;
AM_vbbreg = fhPtr; AM_adjreg = uc; //set regs for occurs check
HOPU_copyFlagGlb = FALSE;
bndBody = HOPU_rigNestedSubst(fargs, fnargs, rhPtr, rPtr,
rargs, rnargs, emblev);
nabs = emblev + fnargs; //# abs in the front of the binding
TR_trailTerm(fhPtr); AM_bndFlag = ON;
if (nabs == 0) DF_mkRef((MemPtr)fhPtr, bndBody);
else {
AM_embedError(nabs);
DF_mkLam((MemPtr)fhPtr, nabs, bndBody);
}
} else { //non-Llambda pattern
if (emblev == 0) AM_addDisPair(fPtr, rPtr);
else {
MemPtr nhtop = AM_hreg + DF_TM_LAM_SIZE;
DF_TermPtr tmPtr = (DF_TermPtr)AM_hreg;
AM_heapError(AM_hreg);
DF_mkLam(AM_hreg, emblev, rPtr);
AM_hreg = nhtop;
AM_addDisPair(fPtr, tmPtr);
} // (emblev != 0)
} //non-LLambda pattern
}
/* The counter part of HOPU_rigMkSubst invoked by HOPU_patternUnifyPair. */
/* Care is taken to avoid making a reference to a register/stack address in */
/* binding and creating disagreement pair. */
/* It is assumed that the pair of terms are not embedded in any abstractions*/
/* ie. (F a1 ... an) = (r b1 ... bm) */
/* Note both fPtr and rPtr are not dereferenced. */
static void HOPU_rigMkSubstGlb(DF_TermPtr fPtr, DF_TermPtr fhPtr, int fnargs,
DF_TermPtr fargs,
DF_TermPtr rPtr, DF_TermPtr rhPtr, int rnargs,
DF_TermPtr rargs)
{
int uc = DF_fvUnivCount(fhPtr);
if (HOPU_isLLambda(uc, fnargs, fargs)) { //LLambda pattern
DF_TermPtr bndBody;
AM_vbbreg = fhPtr; AM_adjreg = uc;
HOPU_copyFlagGlb = FALSE;
bndBody = HOPU_rigNestedSubst(fargs, fnargs, rhPtr, DF_termDeref(rPtr),
rargs, rnargs, 0);
TR_trailTerm(fhPtr); AM_bndFlag = ON;
if (HOPU_copyFlagGlb) {//bndBody must locate on the heap
if (fnargs == 0) DF_mkRef((MemPtr)fhPtr, bndBody);
else {
AM_embedError(fnargs);
DF_mkLam((MemPtr)fhPtr, fnargs, bndBody);
}
} else { //HOPU_copyFlagGlb == FALSE
/* //note: rPtr is the undereferenced rigid term; in this case,
// it is assumed rPtr cannot be a reference to the stack.
// This assumption should be ensured by the fact that atomic
// rigid terms on stack are alway copied into registers in
// binding.
if (fnargs == 0) DF_copyAtomic(rPtr, (MemPtr)fhPtr); */
if (fnargs == 0) HOPU_globalizeCopyRigid(bndBody, fhPtr);
else {
bndBody = HOPU_globalizeRigid(bndBody);
AM_embedError(fnargs);
DF_mkLam((MemPtr)fhPtr, fnargs, bndBody);
}
} //HOPU_copyFlagGlb == FALSE
} else //non_LLambda flex (must locate on the heap)
AM_addDisPair(DF_termDeref(fPtr),
HOPU_globalizeRigid(DF_termDeref(rPtr)));
}
/***************************************************************************/
/* TERM SIMPLIFICATION (RIGID-RIGID) */
/* */
/* Auxiliary functions for solving rigid-rigid pairs. */
/***************************************************************************/
/* Matching heads of two rigid terms. Eta-expansion is considered when */
/* necessary. It is assumed that the heads have been dereferenced. */
static void HOPU_matchHeads(DF_TermPtr hPtr1, DF_TermPtr hPtr2, int nabs)
{
switch(DF_termTag(hPtr1)){
case DF_TM_TAG_CONST:{
if (!(DF_isConst(hPtr2) && (DF_sameConsts(hPtr1, hPtr2))))
EM_THROW(EM_FAIL);
if (DF_isTConst(hPtr1)){ //(first-order) unify type environments
HOPU_typesUnify(DF_constType(hPtr1), DF_constType(hPtr2),
AM_cstTyEnvSize(DF_constTabIndex(hPtr1)));
}
break;
}
case DF_TM_TAG_BVAR: {
if (!DF_isBV(hPtr2)) EM_THROW(EM_FAIL);
else {
int ind = DF_bvIndex(hPtr2) + nabs; //lifting for eta-expansion
AM_embedError(ind);
if (DF_bvIndex(hPtr1) != ind) EM_THROW(EM_FAIL);
}
break;
}
case DF_TM_TAG_NIL: { if (!DF_isNil(hPtr2)) EM_THROW(EM_FAIL); break;}
case DF_TM_TAG_INT: {
if (!(DF_isInt(hPtr2) && (DF_intValue(hPtr2) == DF_intValue(hPtr1))))
EM_THROW(EM_FAIL);
break;
}
case DF_TM_TAG_FLOAT:{
if (!(DF_isFloat(hPtr2)&&(DF_floatValue(hPtr2)==DF_floatValue(hPtr1))))
EM_THROW(EM_FAIL);
break;
}
case DF_TM_TAG_STR: {
if (!(DF_isStr(hPtr2) && (DF_sameStrs(hPtr1, hPtr2))))
EM_THROW(EM_FAIL);
break;
}
case DF_TM_TAG_CONS: {
if (!(DF_isCons(hPtr2))) EM_THROW(EM_FAIL);
break;
}
} //switch
}
/* Set up PDL by sub problems resulted from rigid-rigid pairs upon */
/* successful matching of their heads. Eta-expansion is performed on-a-fly */
/* when necessary. */
void HOPU_setPDL(MemPtr args1, MemPtr args2, int nargs, int nabs)
{
if (nabs == 0){ //no need for eta-expansion
AM_pdlError(nargs * 2);
for (; nargs > 0; nargs --){
AM_pushPDL(args1); args1 += DF_TM_ATOMIC_SIZE;
AM_pushPDL(args2); args2 += DF_TM_ATOMIC_SIZE;
}
} else { //nabs > 0 (eta-expansion)
AM_pdlError((nargs + nabs) * 2);
AM_heapError(AM_hreg + nargs*DF_TM_SUSP_SIZE + nabs*DF_TM_ATOMIC_SIZE);
for (; nargs > 0; nargs --){ //[|ai, 0, nabs, nil|]
AM_pushPDL(args1); AM_pushPDL(AM_hreg);
DF_mkSusp(AM_hreg, 0, nabs, DF_termDeref((DF_TermPtr)args2),
DF_EMPTY_ENV);
AM_hreg += DF_TM_SUSP_SIZE;
args1 += DF_TM_ATOMIC_SIZE; args2 += DF_TM_ATOMIC_SIZE;
}
for (; nabs > 0; nabs --){ // bv(i)
AM_pushPDL(args1); AM_pushPDL(AM_hreg);
DF_mkBV(AM_hreg, nabs);
args1 += DF_TM_ATOMIC_SIZE; AM_hreg += DF_TM_ATOMIC_SIZE;
}
}
}
/***************************************************************************/
/* HIGHER_ORDER PATTERN UNIFICATION */
/* */
/* The main routines of this file. */
/***************************************************************************/
/* Perform higher-order pattern unification over the pairs delayed on the */
/* PDL stack. The PDL stack is empty upon successful termination of this */
/* procedure. */
void HOPU_patternUnifyPDL()
{
DF_TermPtr tPtr1, tPtr2, //pointers to terms to be unified
hPtr, //pointer to head of hnf
args; //arg vec of hnf
Flag rig; //rigid flag and cons flags
int nabs, nargs; //binder length and # of arguments of hnf
while (AM_nemptyPDL()){
//retrieve the pair of terms on the current top of PDL
tPtr1 = (DF_TermPtr)AM_popPDL(); tPtr2 = (DF_TermPtr)AM_popPDL();
HN_hnorm(tPtr1); //hnorm tPtr1
hPtr = AM_head; args = AM_argVec; nabs = AM_numAbs; nargs = AM_numArgs;
rig = AM_rigFlag; //bookkeeping relevant info of hnf of tPtr1
HN_hnorm(tPtr2); //hnorm tPtr2
if (rig){
if (AM_rigFlag){// rigid - rigid
if (nabs > AM_numAbs) {
nabs = nabs - AM_numAbs; //reuse nabs
HOPU_matchHeads(hPtr, AM_head, nabs);
HOPU_setPDL((MemPtr)args,(MemPtr)AM_argVec,AM_numArgs,nabs);
} else { //nabs <= AM_numAbs
nabs = AM_numAbs - nabs; //reuse nabs
HOPU_matchHeads(AM_head, hPtr, nabs);
HOPU_setPDL((MemPtr)AM_argVec, (MemPtr)args, nargs, nabs);
}
} else { // rigid - flex
DF_TermPtr rigBody = HOPU_lamBody(tPtr1);
DF_TermPtr flexBody = HOPU_lamBody(tPtr2);
if (nabs < AM_numAbs) { //eta expand rigid term first
nabs = AM_numAbs - nabs; //reuse nabs
rigBody = HOPU_etaExpand(&hPtr, &args, nargs, nabs);
HOPU_rigMkSubst(flexBody, AM_head, AM_numArgs, AM_argVec,
rigBody, hPtr, (nargs+nabs), args, 0);
} else HOPU_rigMkSubst(flexBody,AM_head, AM_numArgs, AM_argVec,
rigBody,hPtr,nargs,args,nabs-AM_numAbs);
} // rigid-flex
} else { //(rig == FALSE)
DF_TermPtr absBody1 = HOPU_lamBody(tPtr1);
DF_TermPtr absBody2 = HOPU_lamBody(tPtr2);
if (AM_rigFlag){// flex - rigid
if (AM_numAbs < nabs) { //eta expand rigid term first
nabs = nabs - AM_numAbs; //reuse nabs
absBody2 = HOPU_etaExpand(&AM_head, &AM_argVec, AM_numArgs,
nabs);
HOPU_rigMkSubst(absBody1, hPtr, nargs, args, absBody2,
AM_head, AM_numArgs+nabs, AM_argVec, 0);
}else HOPU_rigMkSubst(absBody1,hPtr,nargs,args,absBody2,AM_head,
AM_numArgs,AM_argVec,AM_numAbs-nabs);
} else { // flex - flex
if (AM_numAbs > nabs)
HOPU_flexMkSubst(absBody1, hPtr, nargs, args, absBody2,
AM_head, AM_numArgs, AM_argVec,
AM_numAbs-nabs);
else HOPU_flexMkSubst(absBody2, AM_head, AM_numArgs, AM_argVec,
absBody1,hPtr,nargs,args,nabs-AM_numAbs);
} // flex - flex
} //(rig == FALSE)
} // while (AM_nemptyPDL())
}
/* Interpretively pattern unify first the pairs delayed on the PDL, then */
/* those delayed on the live list, if binding occured during the first step */
/* or previous compiled unification process. */
/* Upon successful termination, PDL should be empty and pairs left on the */
/* live list should be those other than LLambda. */
void HOPU_patternUnify()
{
HOPU_patternUnifyPDL(); //first solve those left from compiled unification
while (AM_bndFlag && AM_nempLiveList()){
DF_DisPairPtr dset = AM_llreg;
do { //move everything in live list to PDL
AM_pdlError(2);
AM_pushPDL((MemPtr)DF_disPairSecondTerm(dset));
AM_pushPDL((MemPtr)DF_disPairFirstTerm(dset));
dset = DF_disPairNext(dset);
} while (DF_isNEmpDisSet(dset));
AM_bndFlag = OFF;
AM_llreg = DF_EMPTY_DIS_SET;
HOPU_patternUnifyPDL(); //unsolvable pairs are added to live list
}
}
/* Interpretively pattern unify a pair of terms given as parameters. This is*/
/* the counter part of HOPU_patterUnifyPDL that is invoked from the compiled*/
/* part of unification. In this situation, the procedure has to be applied */
/* to two terms as opposed to pairs delayed on the PDL stack. */
/* */
/* The input term pointers may dereference to register and stack addresses */
/* Care must be taken to avoid making a reference to a register (stack) */
/* address in binding a variable, and in making a disagreement pair. */
void HOPU_patternUnifyPair(DF_TermPtr tPtr1, DF_TermPtr tPtr2)
{
DF_TermPtr h1Ptr, h2Ptr, args1, args2;
Flag rig1, rig2;
int nabs1, nabs2, nargs1, nargs2;
MemPtr oldPdlBot = AM_pdlBot;
AM_pdlBot = AM_pdlTop;
HN_hnorm(tPtr1); h1Ptr = AM_head; args1 = AM_argVec;
nabs1 = AM_numAbs; nargs1 = AM_numArgs; rig1 = AM_rigFlag;
HN_hnorm(tPtr2); h2Ptr = AM_head; args2 = AM_argVec;
nabs2 = AM_numAbs; nargs2 = AM_numArgs; rig2 = AM_rigFlag;
if (rig1) {
if (rig2) { //rigid-rigid
if (nabs1 > nabs2) {
nabs1 = nabs1 - nabs2;
HOPU_matchHeads(h1Ptr, h2Ptr, nabs1);
HOPU_setPDL((MemPtr)args1, (MemPtr)args2, nargs2, nabs1);
} else {//nabs1 <= nabs2
nabs1 = nabs2 - nabs1;
HOPU_matchHeads(h2Ptr, h1Ptr, nabs1);
HOPU_setPDL((MemPtr)args2, (MemPtr)args1, nargs1, nabs1);
}
} else { //rigid-flex
if ((nabs1 == 0) && (nabs2 == 0))
HOPU_rigMkSubstGlb(tPtr2, h2Ptr, nargs2, args2,
tPtr1, h1Ptr, nargs1, args1);
else {
DF_TermPtr rigBody = HOPU_lamBody(tPtr1);
DF_TermPtr flexBody = HOPU_lamBody(tPtr2);
if (nabs1 < nabs2) {
nabs1 = nabs2 - nabs1;
rigBody = HOPU_etaExpand(&h1Ptr, &args1, nargs1, nabs1);
//now rigBody must locate on heap
HOPU_rigMkSubst(flexBody, h2Ptr, nargs2, args2, rigBody,
h1Ptr, nargs1+nabs1, args1, 0);
} else // (nabs1 >= nabs2)
HOPU_rigMkSubst(flexBody, h2Ptr, nargs2, args2, rigBody,
h1Ptr, nargs1, args1, nabs1-nabs2);
} // !(nabs1 == nabs2 == 0)
} //rigid-flex
} else { // rig1 = FALSE
if (rig2) { //flex-rigid
if ((nabs2 == 0) && (nabs1 == 0))
HOPU_rigMkSubstGlb(tPtr1, h1Ptr, nargs1, args1,
tPtr2, h2Ptr, nargs2, args2);
else { //!(nabs1 == nabs2 == 0)
DF_TermPtr rigBody = HOPU_lamBody(tPtr2);
DF_TermPtr flexBody = HOPU_lamBody(tPtr1);
if (nabs2 < nabs1) {
nabs1 = nabs2 - nabs1;
rigBody = HOPU_etaExpand(&h2Ptr, &args2, nargs2, nabs1);
//now rigBody must locate on heap
HOPU_rigMkSubst(flexBody, h1Ptr, nargs1, args1, rigBody,
h2Ptr, nargs2+nabs1, args2, 0);
} else //(nabs2 >= nabs1)
HOPU_rigMkSubst(flexBody, h1Ptr, nargs1, args1, rigBody,
h2Ptr, nargs2, args2, nabs2-nabs1);
} //!(nabs1 == nabs2 == 0)
} else { //flex-flex
if (nabs1 == 0) //nabs2 >= nabs1
HOPU_flexMkSubstGlb(DF_termDeref(tPtr1), h1Ptr, nargs1, args1,
HOPU_lamBody(tPtr2), h2Ptr, nargs2, args2,
tPtr2, nabs2);
else { //(nabs1 > 0)
if (nabs2 == 0) //nabs2 < nabs1
HOPU_flexMkSubstGlb(DF_termDeref(tPtr2),h2Ptr,nargs2,args2,
HOPU_lamBody(tPtr1),h1Ptr,nargs1,args1,
tPtr1,nabs1);
else { //nabs1 != 0 && nabs2 != 0
DF_TermPtr flexBody1 = HOPU_lamBody(tPtr1);
DF_TermPtr flexBody2 = HOPU_lamBody(tPtr2);
if (nabs2 > nabs1)
HOPU_flexMkSubst(flexBody1, h1Ptr, nargs1, args1,
flexBody2, h2Ptr, nargs2, args2,
nabs2-nabs1);
else //nabs2 <= nabs1
HOPU_flexMkSubst(flexBody2, h2Ptr, nargs2, args2,
flexBody1, h1Ptr, nargs1, args1,
nabs1-nabs2);
} //nabs1 != 0 && nabs2 != 0
} //(nabs1 > 0)
} //flex-flex
} //rig1 = FALSE
//solve the pairs (which must locate on heap) remaining on the PDL
HOPU_patternUnifyPDL();
AM_pdlBot = oldPdlBot;
}
#endif //HOPU_C