gf-3.4: src/runtime/c/teyjus/simulator/hnorm.c
//////////////////////////////////////////////////////////////////////////////
//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 <http://www.gnu.org/licenses/>. //
//////////////////////////////////////////////////////////////////////////////
/****************************************************************************/
/* */
/* File hnorm.c. */
/* This file contains the head normalization routines. */
/* These procedures are based on the suspension calculus, and the reduction */
/* strategy with lazy reduction, lazy substitution and lazy heap */
/* commitment is chosen. A SML realization of this process is described in */
/* paper "Choices in Representation and Reduction Strategies for Lambda */
/* Terms in Intersional Contexts". */
/****************************************************************************/
#ifndef HNORM_C
#define HNORM_C
#include <stdlib.h>
#include "dataformats.h"
#include "mctypes.h"
#include "hnorm.h"
#include "hnormlocal.h"
#include "abstmachine.h"
#include "../system/error.h"
//for debugging: to be removed
#include <stdio.h>
#include "printterm.h"
#include "../system/stream.h"
/*****************************************************************************/
/* a global(to file hnorm.c) encoding of the explicit suspension environment*/
/* and simple checking and updating functions on this environment */
/*****************************************************************************/
/* environment of the implicit suspension, which is initialized to empty*/
static int ol, nl;
static DF_EnvPtr envlist;
/* clean the environment to empty */
static void HN_setEmptyEnv() { ol = 0; nl = 0; envlist = DF_EMPTY_ENV; }
/* set the environment according to given values */
static void HN_setEnv(int o, int n, DF_EnvPtr e)
{ ol = o; nl = n; envlist = e; }
/* is an empty environment? */
static Boolean HN_isEmptyEnv() { return ((ol == 0) && (nl == 0)); }
/****************************************************************************/
/* Functions for creating (modifying) the environment list in the suspension*/
/* environment defined by ol, nl and envlist according to their current */
/* values. */
/****************************************************************************/
/* Add n (n > 0) dummy environment items to the front of the current
environment list: @(nl+n-1) :: ... :: @nl :: envlist.
New dummy env items are created on the current heap top.
*/
static DF_EnvPtr HN_addNDummyEnv(int n)
{
int i;
DF_EnvPtr last = envlist, current = NULL;
AM_heapError(AM_hreg + n * DF_ENV_DUMMY_SIZE);
for (i = 0; i < n; i++){
current = (DF_EnvPtr)AM_hreg;
DF_mkDummyEnv(AM_hreg, nl+i, last);
AM_hreg += DF_ENV_DUMMY_SIZE;
last = current;
}
return current;
}
/* Add n (n > 0) pair environment items to the front of the current
environment list as the following:
([|an,myol,mynl,myenv|],nl):: ... ::([|ai,myol,mynl,myenv|],nl)::envlist,
where ai is the ith argument in the vector referred to by argvec.
Note if ai is an atomic term, the suspension over it is eagerly evaluated.
*/
static DF_EnvPtr HN_addNPair(DF_TermPtr argvec, int myol, int mynl,
DF_EnvPtr myenv, int n)
{
int i;
DF_EnvPtr last = envlist, current = NULL;
MemPtr myEnvlist = AM_hreg;
MemPtr newhtop = AM_hreg + n * DF_ENV_PAIR_SIZE;
AM_heapError(newhtop);
AM_hreg = newhtop; //spare space for n pair env items
for (i = 1; i<= n; i++) {
current = (DF_EnvPtr)myEnvlist;
DF_mkPairEnv(myEnvlist, nl, HNL_suspAsEnv(argvec,myol,mynl,myenv),
last);
myEnvlist += DF_ENV_PAIR_SIZE;
last = current;
argvec = (DF_TermPtr)(((MemPtr)argvec) + DF_TM_ATOMIC_SIZE);
}
return current;
}
/* A specialized version of HN_addNPair when the incoming environment is
empty.
Now, n (n > 0) pair environment items are added to the front of the
current environment list as the following:
(an,0) :: ... :: (a1,0) :: envlist, where ai is the ith argument in the
vector referred to by argvec.
*/
static DF_EnvPtr HN_addNPairEmpEnv(DF_TermPtr argvec, int n)
{
int i;
DF_EnvPtr last = envlist, current = NULL;
AM_heapError(AM_hreg + n * DF_ENV_PAIR_SIZE);
for (i = 1; i <= n; i++) {
current = (DF_EnvPtr)AM_hreg;
DF_mkPairEnv(AM_hreg, 0, argvec, last);
AM_hreg += DF_ENV_PAIR_SIZE;
last = current;
argvec = (DF_TermPtr)(((MemPtr)argvec) + DF_TM_ATOMIC_SIZE);
}
return current;
}
/****************************************************************************/
/* A function for pushing suspension over n abstractions following the rule */
/* [|lam(n,body), ol, nl, envlist|] */
/* -> lam(n, [|body, ol+n, nl+n, @(nl+n-1) :: ... :: @nl :: envlist |] */
/* The result is committed on the current top of heap. */
/* The top-level (implicit) suspension is given by the global variable */
/* ol, nl, and envlist. */
/* This function is used in HN_hnormSusp, HN_hnormSuspOCC and HN_lnormSusp. */
/****************************************************************************/
static DF_TermPtr HN_pushSuspOverLam(DF_TermPtr lamPtr)
{
DF_TermPtr rtPtr; //term pointer to be returned
DF_TermPtr suspPtr; //explicit susp as the lam body in the result
int numabs =DF_lamNumAbs(lamPtr);
int newol = ol + numabs, newnl = nl + numabs;
MemPtr newhtop = AM_hreg+ DF_TM_SUSP_SIZE+ numabs*DF_TM_ATOMIC_SIZE;
DF_EnvPtr newenv;
AM_embedError(newol);
AM_embedError(newnl);
AM_heapError(newhtop);
newenv = HN_addNDummyEnv(numabs);
suspPtr = HNL_suspAsEnv(DF_lamBody(lamPtr), newol, newnl, newenv);
rtPtr = (DF_TermPtr)AM_hreg; //create lam over the susp
DF_mkLam(AM_hreg, numabs, suspPtr);
AM_hreg = newhtop;
return rtPtr;
}
/****************************************************************************/
/* functions for (weak) head normalizing terms of known categories */
/*--------------------------------------------------------------------------*/
/* General comments: */
/* An implicit suspension is given by the global variables ol, nl and */
/* envlist together with the first argument tmPtr to the sub-functions: */
/* [|tmPtr, ol, nl, envlist|] */
/* The suspension environment could be empty in which case the term */
/* being normalized is tmPtr itself. */
/* The second argument of the sub-functions whnf is a flag indicating */
/* whether a head normal form or a weak head normal form is being */
/* computed. */
/****************************************************************************/
static DF_TermPtr HN_hnormDispatch(DF_TermPtr tmPtr, Boolean whnf);
/* (weak) head normalize bound variable or implicit suspension with
bound variable as term skeleton. */
static DF_TermPtr HN_hnormBV(DF_TermPtr bvPtr, Boolean whnf)
{
DF_TermPtr rtPtr; //term pointer to be returned
if (HN_isEmptyEnv()){ //[|#i, 0, 0, nil|] -> #i
rtPtr = bvPtr;
HNL_setRegsRig(bvPtr);
} else { //non-empty env
int dbind = DF_bvIndex(bvPtr);
if (dbind > ol) { //[|#i,ol,nl,e|] -> #i-ol+nl
int newind = dbind - ol + nl;
AM_embedError(newind);
rtPtr =(DF_TermPtr)AM_hreg;
HNL_pushBV(newind);
HNL_setRegsRig(rtPtr);
HN_setEmptyEnv();
} else { // i <= ol
DF_EnvPtr envitem = DF_envListNth(envlist, dbind);
int nladj = nl-DF_envIndex(envitem);
if (DF_isDummyEnv(envitem)){ //[|#i,ol,nl,..@l..|]->#(nl-l)
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushBV(nladj);
HNL_setRegsRig(rtPtr);
HN_setEmptyEnv();
} else { //pair env [|#i,ol,nl,..(s,l)..|] -> [|s,0,(nl-l),nil|]
DF_TermPtr tmPtr = DF_termDeref(DF_envPairTerm(envitem));
if ((nladj != 0) && (DF_isSusp(tmPtr))) {//combine susp
int newnl = DF_suspNL(tmPtr)+nladj;
AM_embedError(newnl);
HN_setEnv(DF_suspOL(tmPtr), newnl, DF_suspEnv(tmPtr));
rtPtr = HN_hnormDispatch(DF_suspTermSkel(tmPtr), whnf);
} else {
HN_setEnv(0, nladj, DF_EMPTY_ENV);
rtPtr = HN_hnormDispatch(tmPtr, whnf);
}
} //pair env
} // i<= ol
} //non-empty env
return rtPtr;
}
/* (weak) head normalize an abstraction or implicit suspension with term
skeleton as an abstraction.
If an implicit suspension is weak head normalized, the suspension itself
is returned. The descendant of this suspension over its abstraction skeleton
is performed in the subsequent app case on a fly.
Note that this is the only case that hnorm termniates with a non-empty
environment.
*/
static DF_TermPtr HN_hnormLam(DF_TermPtr lamPtr, Boolean whnf)
{
DF_TermPtr rtPtr; //term pointer to be returned
if (whnf) return rtPtr = lamPtr; //weak hn
else { //whnf = FALSE
int numabs = DF_lamNumAbs(lamPtr);
DF_TermPtr newbody;
if (HN_isEmptyEnv()){
newbody = HN_hnormDispatch(DF_lamBody(lamPtr), FALSE);
rtPtr = lamPtr; //body must have been adjusted in place
} else { // non-empty env
//[|lam(n,t),ol,nl,e|] ->lam(n,[|t,ol+n,nl+n,@nl+n-1...::@nl::e|]
int newol = ol+numabs, newnl = nl+numabs;
AM_embedError(newol);
AM_embedError(newnl);
HN_setEnv(newol, newnl, HN_addNDummyEnv(numabs));
newbody = HN_hnormDispatch(DF_lamBody(lamPtr), FALSE);
/* create a new lam on the result of hn the lam body */
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushLam(newbody, numabs);
} // non-empty env
AM_numAbs += numabs;
} //whnf == FALSE
return rtPtr;
}
/* (weak) head normalize cons or implicit suspension over cons */
static DF_TermPtr HN_hnormCons(DF_TermPtr consPtr, Boolean whnf)
{
DF_TermPtr argvec = DF_consArgs(consPtr),
rtPtr; //term pointer to be returned
if (HN_isEmptyEnv()){
AM_argVec = argvec;
AM_numArgs = DF_CONS_ARITY;
rtPtr = consPtr;
} else {
Boolean changed = HNL_makeConsArgvec(argvec, ol, nl, envlist);
if (changed){ //new argvec is built because of pushing susp
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushCons(AM_argVec);
} else rtPtr = consPtr;
HN_setEmptyEnv();
}
HNL_setRegsCons(rtPtr);
return rtPtr;
}
/* (weak) head normalize application or implicit suspension over
application. The old application term is destructively changed into
a reference to its head normal form or its weak head normal form if
the weak heap normal form is not an implicit suspension (in which
case the term skeleton must be an abstraction.).
*/
static DF_TermPtr HN_hnormApp(DF_TermPtr appPtr, Boolean whnf)
{
DF_TermPtr funPtr = DF_appFunc(appPtr), argvec = DF_appArgs(appPtr),
rtPtr; // term pointer to be returned
DF_TermPtr oldFunPtr = funPtr;
int arity = DF_appArity(appPtr);
Boolean emptyTopEnv = HN_isEmptyEnv();
int myol, mynl; //for book keeping the implicit suspension env
DF_EnvPtr myenvlist; //for book keeping the implicit suspension env
int myarity = arity; //book keeping the arity before contraction
if (!emptyTopEnv) { //book keeping the current environment
myol = ol; mynl = nl; myenvlist = envlist;
}
funPtr = HN_hnormDispatch(funPtr, TRUE); //whf of the function
while ((arity > 0) && (DF_isLam(funPtr))) {
//perform contraction on top-level redexes while you can
DF_TermPtr lamBody = DF_lamBody(funPtr); //abs body
int numAbsInFun = DF_lamNumAbs(funPtr);
int numContract = ((arity<=numAbsInFun) ? arity : numAbsInFun);
DF_EnvPtr newenv;
int newol = ol + numContract;
AM_embedError(newol);
if (emptyTopEnv) newenv = HN_addNPairEmpEnv(argvec, numContract);
else newenv = HN_addNPair(argvec, myol, mynl, myenvlist, numContract);
HN_setEnv(newol, nl, newenv);
if (arity == numAbsInFun){
funPtr = HN_hnormDispatch(lamBody, whnf);
arity = 0;
} else if (arity > numAbsInFun) {
funPtr = HN_hnormDispatch(lamBody, TRUE);
argvec=(DF_TermPtr)(((MemPtr)argvec)+numAbsInFun*DF_TM_ATOMIC_SIZE);
arity -= numAbsInFun;
} else { //arity < numabsInFun
DF_TermPtr newBody = (DF_TermPtr)AM_hreg;
HNL_pushLam(lamBody, (numAbsInFun-arity));
funPtr = HN_hnormDispatch(newBody, whnf);
arity = 0;
}
}// while ((arity >0) && (DF_IsLam(fun)))
//update or create application
if (arity == 0) { //app disappears
rtPtr = funPtr;
if (emptyTopEnv && HN_isEmptyEnv()) HNL_updateToRef(appPtr, funPtr);
} else { //app persists; Note: now HN_isEmptyEnv must be TRUE
Boolean changed;
if (emptyTopEnv) changed = HNL_makeArgvecEmpEnv(argvec, arity);
else changed = HNL_makeArgvec(argvec,arity,myol,mynl,myenvlist);
if ((!changed) && (arity == myarity) && (funPtr == oldFunPtr)) {
rtPtr = appPtr;
} else {// create new app and in place update the old if empty top env
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushApp(AM_head, AM_argVec, AM_numArgs);
if (emptyTopEnv) HNL_updateToRef(appPtr, rtPtr);
}
}
return rtPtr;
}
/* (weak) head normalize (explicit) suspension or implicit suspension
with a suspension term skeletion. The explicit suspension is destructivly
changed to its head normal form or weak head normal form in case
that the whn is not an implicit susp itself (in which case the term
skeleton must be an abstraction).
*/
static DF_TermPtr HN_hnormSusp(DF_TermPtr suspPtr, Boolean whnf)
{
DF_TermPtr rtPtr; //term pointer to be returned
int myol, mynl ; // for book keeping the env of implicit susp
DF_EnvPtr myenvlist;
Boolean emptyTopEnv = HN_isEmptyEnv();
if (!emptyTopEnv){
myol = ol; mynl = nl; myenvlist = envlist;
}
//first (weak) head normalize the explicit susp
HN_setEnv(DF_suspOL(suspPtr), DF_suspNL(suspPtr), DF_suspEnv(suspPtr));
rtPtr = HN_hnormDispatch(DF_suspTermSkel(suspPtr), whnf);
if (emptyTopEnv) {
if (HN_isEmptyEnv()) {
HNL_updateToRef(suspPtr, rtPtr);
}
} else { // ! emptyTopEnv
if (HN_isEmptyEnv()) HNL_updateToRef(suspPtr, rtPtr);
else rtPtr = HN_pushSuspOverLam(rtPtr);
//(weak) head norm the top-level (imp) susp
HN_setEnv(myol, mynl, myenvlist);
/* note that AM_numabs, AM_numargs and AM_argvec have to be
re-initialized, because the (w)hnf of the inner suspension
is to be traversed again. */
HNL_initRegs();
rtPtr = HN_hnormDispatch(rtPtr, whnf);
}
return rtPtr;
}
/****************************************************************************/
/* Dispatching on various term categories. */
/****************************************************************************/
static DF_TermPtr HN_hnormDispatch(DF_TermPtr tmPtr, Boolean whnf)
{
restart:
switch (DF_termTag(tmPtr)){
case DF_TM_TAG_VAR:
{
if (!HN_isEmptyEnv()) HN_setEmptyEnv();
HNL_setRegsFlex(tmPtr);
return tmPtr;
}
case DF_TM_TAG_CONST:
case DF_TM_TAG_INT:
case DF_TM_TAG_FLOAT:
case DF_TM_TAG_NIL:
case DF_TM_TAG_STR:
case DF_TM_TAG_STREAM:
{
if (!HN_isEmptyEnv()) HN_setEmptyEnv();
HNL_setRegsRig(tmPtr);
return tmPtr;
}
case DF_TM_TAG_BVAR: { return HN_hnormBV(tmPtr, whnf); }
case DF_TM_TAG_CONS: { return HN_hnormCons(tmPtr, whnf); }
case DF_TM_TAG_LAM: { return HN_hnormLam(tmPtr, whnf); }
case DF_TM_TAG_APP: { return HN_hnormApp(tmPtr, whnf); }
case DF_TM_TAG_SUSP: { return HN_hnormSusp(tmPtr, whnf); }
case DF_TM_TAG_REF: { tmPtr = DF_termDeref(tmPtr); goto restart;}
}
//Impossible to reach this point.
return NULL;
}
/****************************************************************************/
/* the interface routine for head normalization */
/****************************************************************************/
void HN_hnorm(DF_TermPtr tmPtr)
{
HN_setEmptyEnv();
HNL_initRegs();
HN_hnormDispatch(DF_termDeref(tmPtr), FALSE);
}
/****************************************************************************/
/* HEAD (WEAK HEAD) NORMALIZATION WITH OCCURS CHECK */
/*--------------------------------------------------------------------------*/
/* General comments: */
/* Checkings are added when the (dereference of) term to be normlized is */
/* an application or a cons. If the term is an application, checking is */
/* made on whether the application is currently referred */
/* to by register AM_vbbreg, and this checking is added in the APP case */
/* of the dispatch function. If the term is a cons, checking is made on */
/* whether its argument vector is currently referred to by the register */
/* AM_vbbreg, and this checking is added in sub-function HN_hnormConsOcc. */
/****************************************************************************/
static DF_TermPtr HN_hnormDispatchOcc(DF_TermPtr tmPtr, Boolean whnf);
/****************************************************************************/
/* functions for (weak) head normalizing terms with occurs-check */
/* of known categories */
/****************************************************************************/
/* (weak) head normalize bound variable or implicit suspension with
bound variable as term skeleton. */
static DF_TermPtr HN_hnormBVOcc(DF_TermPtr bvPtr, Boolean whnf)
{
DF_TermPtr rtPtr; //term pointer to be returned
if (HN_isEmptyEnv()){ //[|#i, 0, 0, nil|] -> #i
rtPtr = bvPtr;
HNL_setRegsRig(bvPtr);
} else { //non-empty env
int dbind = DF_bvIndex(bvPtr);
if (dbind > ol) { //[|#i,ol,nl,e|] -> #i-ol+nl
int newind = dbind - ol + nl;
AM_embedError(newind);
rtPtr =(DF_TermPtr)AM_hreg;
HNL_pushBV(newind);
HNL_setRegsRig(rtPtr);
HN_setEmptyEnv();
} else { // i <= ol
DF_EnvPtr envitem = DF_envListNth(envlist, dbind);
int nladj = nl-DF_envIndex(envitem);
if (DF_isDummyEnv(envitem)){ //[|#i,ol,nl,..@l..|]->#(nl-l)
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushBV(nladj);
HNL_setRegsRig(rtPtr);
HN_setEmptyEnv();
} else { //pair env [|#i,ol,nl,..(s,l)..|] -> [|s,0,(nl-l),nil|]
DF_TermPtr tmPtr = DF_termDeref(DF_envPairTerm(envitem));
if ((nladj != 0) && (DF_isSusp(tmPtr))) {//combine susp
int newnl = DF_suspNL(tmPtr)+nladj;
AM_embedError(newnl);
HN_setEnv(DF_suspOL(tmPtr), newnl, DF_suspEnv(tmPtr));
rtPtr = HN_hnormDispatchOcc(DF_suspTermSkel(tmPtr), whnf);
} else {
HN_setEnv(0, nladj, DF_EMPTY_ENV);
rtPtr = HN_hnormDispatchOcc(tmPtr, whnf);
}
} //pair env
} // i<= ol
} //non-empty env
return rtPtr;
}
/* (weak) head normalize an abstraction or implicit suspension with term
skeleton as an abstraction. */
static DF_TermPtr HN_hnormLamOcc(DF_TermPtr lamPtr, Boolean whnf)
{
DF_TermPtr rtPtr; //term pointer to be returned
if (whnf) return rtPtr = lamPtr; //weak hn
else { //whnf = FALSE
int numabs = DF_lamNumAbs(lamPtr);
DF_TermPtr newbody;
if (HN_isEmptyEnv()){
newbody = HN_hnormDispatchOcc(DF_lamBody(lamPtr), FALSE);
rtPtr = lamPtr; //body must have been adjusted in place
} else { // non-empty env
//[|lam(n,t),ol,nl,e|] ->lam(n,[|t,ol+n,nl+n,@nl+n-1...::@nl::e|]
int newol = ol+numabs, newnl = nl+numabs;
AM_embedError(newol);
AM_embedError(newnl);
HN_setEnv(newol, newnl, HN_addNDummyEnv(numabs));
newbody = HN_hnormDispatchOcc(DF_lamBody(lamPtr), FALSE);
/* create a new lam on the result of hn the lam body */
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushLam(newbody, numabs);
} // non-empty env
AM_numAbs += numabs;
} //whnf == FALSE
return rtPtr;
}
/* (weak) head normalize cons or implicit suspension over cons.
Note checking on whether the argument vector of the cons term is referred to
by the register AM_vbbreg is made.
*/
static DF_TermPtr HN_hnormConsOcc(DF_TermPtr consPtr, Boolean whnf)
{
DF_TermPtr argvec = DF_consArgs(consPtr),
rtPtr; //term pointer to be returned
if (AM_vbbreg == argvec) EM_THROW(EM_FAIL);
if (HN_isEmptyEnv()){
AM_argVec = argvec;
AM_numArgs = DF_CONS_ARITY;
rtPtr = consPtr;
} else {
Boolean changed = HNL_makeConsArgvec(argvec, ol, nl, envlist);
if (changed){ //new argvec is built because of pushing susp
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushCons(AM_argVec);
} else rtPtr = consPtr;
HN_setEmptyEnv();
}
HNL_setRegsCons(rtPtr);
return rtPtr;
}
/* (weak) head normalize application or implicit suspension over
application.
*/
static DF_TermPtr HN_hnormAppOcc(DF_TermPtr appPtr, Boolean whnf)
{
DF_TermPtr funPtr = DF_appFunc(appPtr), argvec = DF_appArgs(appPtr),
rtPtr; // term pointer to be returned
DF_TermPtr oldFunPtr = funPtr;
int arity = DF_appArity(appPtr);
Boolean emptyTopEnv = HN_isEmptyEnv();
int myol, mynl; //for book keeping the implicit suspension env
DF_EnvPtr myenvlist; //for book keeping the implicit suspension env
int myarity = arity; //book keeping the arity before contraction
if (!emptyTopEnv) { //book keeping the current environment
myol = ol; mynl = nl; myenvlist = envlist;
}
funPtr = HN_hnormDispatchOcc(funPtr, TRUE); //whf of the function
while ((arity > 0) && (DF_isLam(funPtr))) {
//perform contraction on top-level redexes while you can
DF_TermPtr lamBody = DF_lamBody(funPtr); //abs body
int numAbsInFun = DF_lamNumAbs(funPtr);
int numContract = ((arity<=numAbsInFun) ? arity : numAbsInFun);
DF_EnvPtr newenv;
int newol = ol + numContract;
AM_embedError(newol);
if (emptyTopEnv) newenv = HN_addNPairEmpEnv(argvec, numContract);
else newenv = HN_addNPair(argvec, myol, mynl, myenvlist, numContract);
HN_setEnv(newol, nl, newenv);
if (arity == numAbsInFun){
funPtr = HN_hnormDispatchOcc(lamBody, whnf);
arity = 0;
} else if (arity > numAbsInFun) {
funPtr = HN_hnormDispatchOcc(lamBody, TRUE);
argvec=(DF_TermPtr)(((MemPtr)argvec)+numAbsInFun*DF_TM_ATOMIC_SIZE);
arity -= numAbsInFun;
} else { //arity < numabsInFun
DF_TermPtr newBody = (DF_TermPtr)AM_hreg;
HNL_pushLam(lamBody, (numAbsInFun-arity));
funPtr = HN_hnormDispatchOcc(newBody, whnf);
arity = 0;
}
}// while ((arity >0) && (DF_IsLam(fun)))
//update or create application
if (arity == 0) { //app disappears
rtPtr = funPtr;
if (emptyTopEnv && HN_isEmptyEnv()) HNL_updateToRef(appPtr, funPtr);
} else { //app persists; Note: now HN_isEmptyEnv must be TRUE
Boolean changed;
if (emptyTopEnv) changed = HNL_makeArgvecEmpEnv(argvec, arity);
else changed = HNL_makeArgvec(argvec,arity,myol,mynl,myenvlist);
if ((!changed) && (arity == myarity) && (oldFunPtr == funPtr)) {
rtPtr = appPtr;
} else {// create new app and in place update the old if empty top env
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushApp(AM_head, AM_argVec, AM_numArgs);
if (emptyTopEnv) HNL_updateToRef(appPtr, rtPtr);
}
}
return rtPtr;
}
/* (weak) head normalize (explicit) suspension or implicit suspension
with a suspension term skeletion.
*/
static DF_TermPtr HN_hnormSuspOcc(DF_TermPtr suspPtr, Boolean whnf)
{
DF_TermPtr rtPtr; //term pointer to be returned
int myol, mynl ; // for book keeping the env of implicit susp
DF_EnvPtr myenvlist;
Boolean emptyTopEnv = HN_isEmptyEnv();
if (!emptyTopEnv){
myol = ol; mynl = nl; myenvlist = envlist;
}
//first (weak) head normalize the explicit susp
HN_setEnv(DF_suspOL(suspPtr), DF_suspNL(suspPtr), DF_suspEnv(suspPtr));
rtPtr = HN_hnormDispatchOcc(DF_suspTermSkel(suspPtr), whnf);
if (emptyTopEnv) {
if (HN_isEmptyEnv()) HNL_updateToRef(suspPtr, rtPtr);
} else { // ! emptyTopEnv
if (HN_isEmptyEnv()) HNL_updateToRef(suspPtr, rtPtr);
else rtPtr = HN_pushSuspOverLam(rtPtr);
//(weak) head norm the top-level (imp) susp
HN_setEnv(myol, mynl, myenvlist);
/* note that AM_numabs, AM_numargs and AM_argvec have to be
re-initialized, because the (w)hnf of the inner suspension
is to be traversed again. */
HNL_initRegs();
rtPtr = HN_hnormDispatchOcc(rtPtr, whnf);
}
return rtPtr;
}
/****************************************************************************/
/* Dispatching on various term categories. */
/****************************************************************************/
static DF_TermPtr HN_hnormDispatchOcc(DF_TermPtr tmPtr, Boolean whnf)
{
restart_hnormOcc:
switch (DF_termTag(tmPtr)){
case DF_TM_TAG_VAR:
{
if (!HN_isEmptyEnv()) HN_setEmptyEnv();
HNL_setRegsFlex(tmPtr);
return tmPtr;
}
case DF_TM_TAG_CONST:
case DF_TM_TAG_INT:
case DF_TM_TAG_FLOAT:
case DF_TM_TAG_NIL:
case DF_TM_TAG_STR:
case DF_TM_TAG_STREAM:
{
if (!HN_isEmptyEnv()) HN_setEmptyEnv();
HNL_setRegsRig(tmPtr);
return tmPtr;
}
case DF_TM_TAG_BVAR: { return HN_hnormBVOcc(tmPtr, whnf); }
case DF_TM_TAG_CONS: { return HN_hnormConsOcc(tmPtr, whnf); }
case DF_TM_TAG_LAM: { return HN_hnormLamOcc(tmPtr, whnf); }
case DF_TM_TAG_APP: {
if (AM_vbbreg == tmPtr) EM_THROW(EM_FAIL);
return HN_hnormAppOcc(tmPtr, whnf); }
case DF_TM_TAG_SUSP: { return HN_hnormSuspOcc(tmPtr, whnf); }
case DF_TM_TAG_REF: {tmPtr=DF_termDeref(tmPtr); goto restart_hnormOcc;}
}
//Impossible to reach this point.
return NULL;
}
/****************************************************************************/
/* the interface routine for head normalization */
/****************************************************************************/
void HN_hnormOcc(DF_TermPtr tmPtr)
{
HN_setEmptyEnv();
HNL_initRegs();
tmPtr = HN_hnormDispatchOcc(DF_termDeref(tmPtr), FALSE);
}
/****************************************************************************/
/* FULL NORMALIZATION */
/****************************************************************************/
static DF_TermPtr HN_lnormDispatch(DF_TermPtr, Boolean whnf);
/****************************************************************************/
/* Functions for creating argument vectors in full normalization */
/*--------------------------------------------------------------------------*/
/* General comments: */
/* This is the counter part of HNL_makeArgvec functions (hnormlocal.c) */
/* in the full normalization process for arranging arguments of */
/* applications (cons) when their "heads" are in (head) normal forms. */
/* Nested applications are unfolded. */
/* The difference is that HN_lnormDispatch is invoked on each argument */
/* to fully normalize it. */
/****************************************************************************/
/* Fully normalize (implicit) suspensions [| ai, myol, mynl, myenv |],
where ai's are those in the vector referred to by argvec with size arity,
and myol, mynl, myenv are given by other parameters.
Note that a new argument vector is always created.
*/
static void HN_lnormArgvec(DF_TermPtr argvec, int arity, int myol, int mynl,
DF_EnvPtr myenv)
{
int i;
//book keeping relevant regs.
DF_TermPtr head = AM_head, myArgvec = AM_argVec;
int numAbs = AM_numAbs, numArgs = AM_numArgs;
Flag rigFlag = AM_rigFlag, consFlag = AM_consFlag;
MemPtr newArgvec = AM_hreg; //new argvec
MemPtr newhtop = newArgvec + arity * DF_TM_ATOMIC_SIZE;
AM_heapError(newhtop);
AM_hreg = newhtop; //arrange heap top for creating terms in norm args
for (i = 1; i <= arity; i++){
HN_setEnv(myol, mynl, myenv); //imp susp environment
HNL_initRegs();
DF_mkRef(newArgvec, HN_lnormDispatch(argvec, FALSE));
newArgvec += DF_TM_ATOMIC_SIZE;
argvec = (DF_TermPtr)(((MemPtr)argvec)+DF_TM_ATOMIC_SIZE);
}
//reset registers
AM_head = head; AM_argVec = myArgvec;
AM_numAbs = numAbs; AM_numArgs = numArgs;
AM_rigFlag = rigFlag; AM_consFlag = consFlag;
}
/* A specialized version of HN_lnormArgvec when the implicit suspension
over each argument in the vector is known to be empty.
Note that upon the return of HN_lnormDispatch, the argument has been
destructively updated to its normal form, which means the old argument
vector is always used.
*/
static void HN_lnormArgvecEmpEnv(DF_TermPtr argvec, int arity)
{
int i;
//book keeping relevant regs.
DF_TermPtr head = AM_head, myArgvec = AM_argVec;
int numAbs = AM_numAbs, numArgs = AM_numArgs;
Flag rigFlag = AM_rigFlag, consFlag = AM_consFlag;
for (i = 1; i <= arity; i++){
HNL_initRegs();
HN_lnormDispatch(argvec, FALSE);
argvec = (DF_TermPtr)(((MemPtr)argvec) + DF_TM_ATOMIC_SIZE);
}
//reset registers
AM_head = head; AM_argVec = myArgvec;
AM_numAbs = numAbs; AM_numArgs = numArgs;
AM_rigFlag = rigFlag; AM_consFlag = consFlag;
}
/* Create an argument vector for applications within a non-empty environment.
Actions are carried out in two steps:
First, nested applications are unfolded if arising. Second, the (implicit)
suspensions formed by each argument and given parameters are fully
normalized.
Note that a new argument vector is always created.
*/
static Boolean HN_makeArgvecLnorm(DF_TermPtr argvec, int arity, int myol,
int mynl, DF_EnvPtr myenv)
{
DF_TermPtr newArgvec = (DF_TermPtr)AM_hreg; //new argvec
int newArity;
if (AM_numArgs != 0){ //unfold nested app first
MemPtr newhtop = AM_hreg + AM_numArgs * DF_TM_ATOMIC_SIZE;
AM_heapError(newhtop);
newArity = arity + AM_numArgs;
AM_arityError(newArity);
HNL_copyArgs(AM_argVec, AM_numArgs); //layout inner args
} else newArity = arity;
//fully normalize arguments
HN_lnormArgvec(argvec, arity, myol, mynl, myenv);
AM_argVec = newArgvec;
AM_numArgs = newArity;
return TRUE;
}
/* A specilized version of HN_makeArgvecLnorm when the enclosing environment
is known to be empty. Note that new argument vecoter is created
if nested applications were unfolded. Otherwise, the old is used.
Boolean values TRUE or FALSE is returned to inidicate which situation it is.
*/
static Boolean HN_makeArgvecEmpEnvLnorm(DF_TermPtr argvec, int arity)
{
HN_lnormArgvecEmpEnv(argvec, arity); //lnorm arguments
if (AM_numArgs != 0){ //unfold nested app
int newArity = arity + AM_numArgs;
DF_TermPtr newArgvec = (DF_TermPtr)AM_hreg; //new argument vector
AM_arityError(newArity);
AM_heapError(((MemPtr)newArgvec + newArity * DF_TM_ATOMIC_SIZE));
HNL_copyArgs(AM_argVec, AM_numArgs);
HNL_copyArgs(argvec, arity);
AM_argVec = newArgvec;
AM_numArgs = newArity;
return TRUE;
} else {
AM_argVec = argvec;
AM_numArgs = arity;
return FALSE;
}
}
/****************************************************************************/
/* functions for fully normalizing terms of known categories */
/*--------------------------------------------------------------------------*/
/* General comments: */
/* */
/* An implicit suspension is given by the global variables ol, nl and */
/* envlist together with the first argument tmPtr to the sub-functions: */
/* [|tmPtr, ol, nl, envlist|] */
/* The suspension environment could be empty in which case the term */
/* being normalized is tmPtr itself. */
/* The second argument of the sub-functions whnf is a flag indicating */
/* whether a head normal form or a weak head normal form is being */
/* computed. */
/****************************************************************************/
/* Fully normalize or weak head normalize bound variable or implicit
suspension with bound variable as term skeleton.
The actions carried out are the same as the counter part in the head
normalization proceee, except that HN_lnormDispatch is invoked as opposed
to HN_hnormDispatch when necessary.
*/
static DF_TermPtr HN_lnormBV(DF_TermPtr bvPtr, Boolean whnf)
{
DF_TermPtr rtPtr; //term pointer to be returned
if (HN_isEmptyEnv()){ //[|#i, 0, 0, nil|] -> #i
rtPtr = bvPtr;
HNL_setRegsRig(bvPtr);
} else { //non-empty env
int dbind = DF_bvIndex(bvPtr);
if (dbind > ol) { //[|#i,ol,nl,e|] -> #i-ol+nl
int newind = dbind - ol + nl;
AM_embedError(newind);
rtPtr =(DF_TermPtr)AM_hreg;
HNL_pushBV(newind);
HNL_setRegsRig(rtPtr);
HN_setEmptyEnv();
} else { // i <= ol
DF_EnvPtr envitem = DF_envListNth(envlist, dbind);
int nladj = nl-DF_envIndex(envitem);
if (DF_isDummyEnv(envitem)){ //[|#i,ol,nl,..@l..|]->#(nl-l)
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushBV(nladj);
HNL_setRegsRig(rtPtr);
HN_setEmptyEnv();
} else { //pair env [|#i,ol,nl,..(s,l)..|] -> [|s,0,(nl-l),nil|]
DF_TermPtr tmPtr = DF_termDeref(DF_envPairTerm(envitem));
if ((nladj != 0) && (DF_isSusp(tmPtr))) {//combine susp
int newnl = DF_suspNL(tmPtr)+nladj;
AM_embedError(newnl);
HN_setEnv(DF_suspOL(tmPtr), newnl, DF_suspEnv(tmPtr));
rtPtr = HN_lnormDispatch(DF_suspTermSkel(tmPtr), whnf);
} else {
HN_setEnv(0, nladj, DF_EMPTY_ENV);
rtPtr = HN_lnormDispatch(tmPtr, whnf);
}
} //pair env
} // i<= ol
} //non-empty env
return rtPtr;
}
/* Fully normalize or weak head normalize abstractions or implicit suspension
with abstractions as term skeletons.
The actions carried out are the same as the counter part in the head
normalization process, except that HN_lnormDispatch is invoked as opposed
to HN_hnormDispatch when necessary.
*/
static DF_TermPtr HN_lnormLam(DF_TermPtr lamPtr, Boolean whnf)
{
DF_TermPtr rtPtr; //term pointer to be returned
if (whnf) return rtPtr = lamPtr; //weak hn
else { //whnf = FALSE
int numabs = DF_lamNumAbs(lamPtr);
DF_TermPtr newbody;
if (HN_isEmptyEnv()){
newbody = HN_lnormDispatch(DF_lamBody(lamPtr), FALSE);
rtPtr = lamPtr; //body must have been adjusted in place
} else { // non-empty env
//[|lam(n,t),ol,nl,e|] ->lam(n,[|t,ol+n,nl+n,@nl+n-1...::@nl::e|]
int newol = ol+numabs, newnl = nl+numabs;
AM_embedError(newol);
AM_embedError(newnl);
HN_setEnv(newol, newnl, HN_addNDummyEnv(numabs));
newbody = HN_lnormDispatch(DF_lamBody(lamPtr), FALSE);
/* create a new lam on the result of hn the lam body */
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushLam(newbody, numabs);
} // non-empty env
AM_numAbs += numabs;
} //whnf == FALSE
return rtPtr;
}
/* Fully normalize or weak head normalize cons or implicit suspension over
cons. The difference from HN_hnormCons is that the arguments of the cons
are fully normalized.
*/
static DF_TermPtr HN_lnormCons(DF_TermPtr consPtr, Boolean whnf)
{
DF_TermPtr argvec = DF_consArgs(consPtr),
rtPtr; //term pointer to be returned
if (HN_isEmptyEnv()){
HN_lnormArgvecEmpEnv(argvec, DF_CONS_ARITY);
AM_argVec = argvec;
AM_numArgs = DF_CONS_ARITY;
rtPtr = consPtr;
} else {
DF_TermPtr newArgvec = (DF_TermPtr)AM_hreg; //new argument vector
HN_lnormArgvec(argvec, DF_CONS_ARITY, ol, nl, envlist);
AM_argVec = newArgvec;
AM_numArgs = DF_CONS_ARITY;
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushCons(AM_argVec);
HN_setEmptyEnv();
}
HNL_setRegsCons(rtPtr);
return rtPtr;
}
/* Fully normalize or weak head normalize application or implicit suspension
over application. The actions carried out here is the same as those in
HN_hnormApp except that HN_lnormDispatch is invoked as HN_hnormDispatch, and
in making argument vectors makeArgvecLnorm functions are used to fully
normalize the arguments.
*/
static DF_TermPtr HN_lnormApp(DF_TermPtr appPtr, Boolean whnf)
{
DF_TermPtr funPtr = DF_appFunc(appPtr), argvec = DF_appArgs(appPtr),
rtPtr; // term pointer to be returned
DF_TermPtr oldFunPtr = funPtr;
int arity = DF_appArity(appPtr);
Boolean emptyTopEnv = HN_isEmptyEnv();
int myol, mynl; //for book keeping the implicit suspension env
DF_EnvPtr myenvlist; //for book keeping the implicit suspension env
int myarity = arity; //book keeping the arity before contraction
if (!emptyTopEnv) { //book keeping the current environment
myol = ol; mynl = nl; myenvlist = envlist;
}
funPtr = HN_lnormDispatch(funPtr, TRUE); //whf of the function
while ((arity > 0) && (DF_isLam(funPtr))) {
//perform contraction on top-level redexes while you can
DF_TermPtr lamBody = DF_lamBody(funPtr); //abs body
int numAbsInFun = DF_lamNumAbs(funPtr);
int numContract = ((arity<=numAbsInFun) ? arity : numAbsInFun);
DF_EnvPtr newenv;
int newol = ol + numContract;
AM_embedError(newol);
if (emptyTopEnv) newenv = HN_addNPairEmpEnv(argvec, numContract);
else newenv = HN_addNPair(argvec, myol, mynl, myenvlist, numContract);
HN_setEnv(newol, nl, newenv);
if (arity == numAbsInFun){
funPtr = HN_lnormDispatch(lamBody, whnf);
arity = 0;
} else if (arity > numAbsInFun) {
funPtr = HN_lnormDispatch(lamBody, TRUE);
argvec=(DF_TermPtr)(((MemPtr)argvec)+numAbsInFun*DF_TM_ATOMIC_SIZE);
arity -= numAbsInFun;
} else { //arity < numabsInFun
DF_TermPtr newBody = (DF_TermPtr)AM_hreg;
HNL_pushLam(lamBody, (numAbsInFun-arity));
funPtr = HN_lnormDispatch(newBody, whnf);
arity = 0;
}
}// while ((arity >0) && (DF_IsLam(fun)))
//update or create application
if (arity == 0) { //app disappears
rtPtr = funPtr;
if (emptyTopEnv && HN_isEmptyEnv()) HNL_updateToRef(appPtr, funPtr);
} else { //app persists; Note: now HN_isEmptyEnv must be TRUE
Boolean changed;
if (emptyTopEnv) changed = HN_makeArgvecEmpEnvLnorm(argvec, arity);
else changed = HN_makeArgvecLnorm(argvec,arity,myol,mynl,myenvlist);
if ((!changed) && (arity == myarity) && (oldFunPtr == funPtr)) {
rtPtr = appPtr;
} else {// create new app and in place update the old if empty top env
rtPtr = (DF_TermPtr)AM_hreg;
HNL_pushApp(AM_head, AM_argVec, AM_numArgs);
if (emptyTopEnv) HNL_updateToRef(appPtr, rtPtr);
}
}
return rtPtr;
}
/* Fuuly normlize or weak head normalize (explicit) suspension or implicit
suspension with a suspension term skeletion. The actions are the same
as those in HN_hnormSusp except that HN_lnormDispatch is used as opposed
to HN_hnormSusp with one exception: when the environment of the top-level
suspension is not empty, the inner suspension is head normalized
(HN_hnormDispatch).
*/
static DF_TermPtr HN_lnormSusp(DF_TermPtr suspPtr, Boolean whnf)
{
DF_TermPtr rtPtr; //term pointer to be returned
int myol, mynl; // for book keeping the env of implicit susp
DF_EnvPtr myenvlist;
Boolean emptyTopEnv = HN_isEmptyEnv();
if (!emptyTopEnv) {
myol = ol; mynl = nl; myenvlist = envlist;
}
HN_setEnv(DF_suspOL(suspPtr), DF_suspNL(suspPtr), DF_suspEnv(suspPtr));
if (emptyTopEnv){
rtPtr = HN_lnormDispatch(DF_suspTermSkel(suspPtr), whnf);
if (HN_isEmptyEnv()) HNL_updateToRef(suspPtr, rtPtr);
} else { //non-empty top-level env
rtPtr = HN_hnormDispatch(DF_suspTermSkel(suspPtr), whnf);
if (HN_isEmptyEnv()) HNL_updateToRef(suspPtr, rtPtr);
else rtPtr = HN_pushSuspOverLam(rtPtr);
//fully normalize top-level susp
HN_setEnv(myol, mynl, myenvlist);
/* note that AM_numabs, AM_numargs and AM_argvec have to be
re-initialized, because the (w)hnf of the inner suspension
is to be traversed again. */
HNL_initRegs();
rtPtr = HN_lnormDispatch(rtPtr, whnf);
}
return rtPtr;
}
/****************************************************************************/
/* Dispatching on various term categories. */
/****************************************************************************/
static DF_TermPtr HN_lnormDispatch(DF_TermPtr tmPtr, Boolean whnf)
{
restart_lnorm:
switch (DF_termTag(tmPtr)){
case DF_TM_TAG_VAR:
{
if (!HN_isEmptyEnv()) HN_setEmptyEnv();
HNL_setRegsFlex(tmPtr);
return tmPtr;
}
case DF_TM_TAG_CONST:
case DF_TM_TAG_INT:
case DF_TM_TAG_FLOAT:
case DF_TM_TAG_NIL:
case DF_TM_TAG_STR:
case DF_TM_TAG_STREAM:
{
if (!HN_isEmptyEnv()) HN_setEmptyEnv();
HNL_setRegsRig(tmPtr);
return tmPtr;
}
case DF_TM_TAG_BVAR: { return HN_lnormBV(tmPtr, whnf); }
case DF_TM_TAG_CONS: { return HN_lnormCons(tmPtr, whnf); }
case DF_TM_TAG_LAM: { return HN_lnormLam(tmPtr, whnf); }
case DF_TM_TAG_APP: { return HN_lnormApp(tmPtr, whnf); }
case DF_TM_TAG_SUSP: { return HN_lnormSusp(tmPtr, whnf); }
case DF_TM_TAG_REF: { tmPtr = DF_termDeref(tmPtr); goto restart_lnorm;}
}
//Impossible to reach this point.
return NULL;
}
/****************************************************************************/
/* the interface routine for head normalization */
/****************************************************************************/
void HN_lnorm(DF_TermPtr tmPtr)
{
HN_setEmptyEnv();
HNL_initRegs();
tmPtr = HN_lnormDispatch(DF_termDeref(tmPtr), FALSE);
}
#endif //HNORM_C