home *** CD-ROM | disk | FTP | other *** search
- /* Output from p2c, the Pascal-to-C translator */
- /* From input file "prolog.p" */
-
-
- /*****************************************************************
- * DECLARATIONS *
- *****************************************************************/
-
- #include <p2c/p2c.h>
-
-
- #define NAMELENG 20 /* Maximum length of a name */
- #define MAXNAMES 300 /* Maximum number of different names */
- #define MAXINPUT 2000 /* Maximum length of an input */
-
- #define PROMPT "-> "
- #define PROMPT2 "> "
- #define COMMENTCHAR ";"
-
- #define TABCODE 9 /* in ASCII */
-
-
- typedef Char NAMESTRING[NAMELENG];
-
- /* a NAME is an index in printNames */
-
-
- typedef struct GOALREC {
- short pred;
- struct EXPLISTREC *args;
- } GOALREC;
-
- typedef struct GOALLISTREC {
- GOALREC *head;
- struct GOALLISTREC *tail;
- } GOALLISTREC;
-
- typedef struct VARIABLEREC {
- short varname;
- long varindex;
- } VARIABLEREC;
-
- typedef struct VARLISTREC {
- VARIABLEREC *head;
- struct VARLISTREC *tail;
- } VARLISTREC;
-
- typedef enum {
- VAREXP, INTEXP, APEXP
- } EXPTYPE;
-
- typedef struct EXPREC {
- EXPTYPE etype;
- union {
- VARIABLEREC *varble;
- long intval;
- struct {
- short optr;
- struct EXPLISTREC *args;
- } U2;
- } UU;
- } EXPREC;
-
- typedef struct EXPLISTREC {
- EXPREC *head;
- struct EXPLISTREC *tail;
- } EXPLISTREC;
-
- typedef struct CLAUSEREC {
- GOALREC *lhs;
- GOALLISTREC *rhs;
- struct CLAUSEREC *nextclause;
- } CLAUSEREC;
-
- typedef struct SUBSTREC {
- VARLISTREC *domain;
- EXPLISTREC *range;
- } SUBSTREC;
-
-
- Static CLAUSEREC *clauses, *lastclause;
-
- Static GOALLISTREC *toplevelGoal;
-
- Static Char userinput[MAXINPUT];
- Static short inputleng, pos_;
-
- Static NAMESTRING printNames[MAXNAMES];
- Static short numNames, numBuiltins;
-
- Static boolean quittingtime;
-
-
- /*****************************************************************
- * DATA STRUCTURE OP'S *
- *****************************************************************/
-
- /* mkGoal - create a new GOAL with pred p and arguments a */
- Static GOALREC *mkGoal(p, a)
- short p;
- EXPLISTREC *a;
- {
- GOALREC *newg;
-
- newg = (GOALREC *)Malloc(sizeof(GOALREC));
- newg->pred = p;
- newg->args = a;
- return newg;
- } /* mkGoal */
-
-
- /* mkVAREXP - create a new EXP of type VAREXP */
- Static EXPREC *mkVAREXP(v)
- VARIABLEREC *v;
- {
- EXPREC *newe;
-
- newe = (EXPREC *)Malloc(sizeof(EXPREC));
- newe->etype = VAREXP;
- newe->UU.varble = v;
- return newe;
- } /* mkVAREXP */
-
-
- /* mkINTEXP - create a new EXP of type INTEXP */
- Static EXPREC *mkINTEXP(n)
- long n;
- {
- EXPREC *newe;
-
- newe = (EXPREC *)Malloc(sizeof(EXPREC));
- newe->etype = INTEXP;
- newe->UU.intval = n;
- return newe;
- } /* mkINTEXP */
-
-
- /* mkAPEXP - create a new EXP of type APEXP */
- Static EXPREC *mkAPEXP(o, a)
- short o;
- EXPLISTREC *a;
- {
- EXPREC *newe;
-
- newe = (EXPREC *)Malloc(sizeof(EXPREC));
- newe->etype = APEXP;
- newe->UU.U2.optr = o;
- newe->UU.U2.args = a;
- return newe;
- } /* mkAPEXP */
-
-
- /* mkVariable - create a new VARIABLE with name n and index i */
- Static VARIABLEREC *mkVariable(n, i)
- short n;
- long i;
- {
- VARIABLEREC *newv;
-
- newv = (VARIABLEREC *)Malloc(sizeof(VARIABLEREC));
- newv->varname = n;
- newv->varindex = i;
- return newv;
- } /* mkVariable */
-
-
- /* mkVarlist - create a new VARLIST with head v and tail vl */
- Static VARLISTREC *mkVarlist(v, vl)
- VARIABLEREC *v;
- VARLISTREC *vl;
- {
- VARLISTREC *newvl;
-
- newvl = (VARLISTREC *)Malloc(sizeof(VARLISTREC));
- newvl->head = v;
- newvl->tail = vl;
- return newvl;
- } /* mkVarlist */
-
-
- /* mkGoallist - return a GOALLIST with head g and tail gl */
- Static GOALLISTREC *mkGoallist(g, gl)
- GOALREC *g;
- GOALLISTREC *gl;
- {
- GOALLISTREC *newgl;
-
- newgl = (GOALLISTREC *)Malloc(sizeof(GOALLISTREC));
- newgl->head = g;
- newgl->tail = gl;
- return newgl;
- } /* mkGoallist */
-
-
- /* mkExplist - return an EXPLIST with head e and tail el */
- Static EXPLISTREC *mkExplist(e, el)
- EXPREC *e;
- EXPLISTREC *el;
- {
- EXPLISTREC *newel;
-
- newel = (EXPLISTREC *)Malloc(sizeof(EXPLISTREC));
- newel->head = e;
- newel->tail = el;
- return newel;
- } /* mkExplist */
-
-
- /* mkClause - create a new GOAL with lhs l and rhs r */
- Static CLAUSEREC *mkClause(l, r)
- GOALREC *l;
- GOALLISTREC *r;
- {
- CLAUSEREC *c;
-
- c = (CLAUSEREC *)Malloc(sizeof(CLAUSEREC));
- c->lhs = l;
- c->rhs = r;
- c->nextclause = NULL;
- return c;
- } /* mkClause */
-
-
- /* eqVar - compare two VARIABLE's for equality */
- Static boolean eqVar(v1, v2)
- VARIABLEREC *v1, *v2;
- {
- return (v1->varname == v2->varname && v1->varindex == v2->varindex);
- } /* eqVar */
-
-
- /* lengthEL - return length of EXPLIST el */
- Static long lengthEL(el)
- EXPLISTREC *el;
- {
- long i;
-
- i = 0;
- while (el != NULL) {
- i++;
- el = el->tail;
- }
- return i;
- } /* lengthEL */
-
-
- /*****************************************************************
- * NAME MANAGEMENT *
- *****************************************************************/
-
- /* newClause - add new clause at end of clauses list */
- Static Void newClause(l, r)
- GOALREC *l;
- GOALLISTREC *r;
- {
- if (lastclause == NULL) {
- clauses = mkClause(l, r);
- lastclause = clauses;
- } else {
- lastclause->nextclause = mkClause(l, r);
- lastclause = lastclause->nextclause;
- }
- } /* newClause */
-
-
- /* initNames - place all pre-defined names into printNames */
- Static Void initNames()
- {
- long i;
-
- clauses = NULL;
- lastclause = NULL;
- i = 1;
- memcpy(printNames[i - 1], "plus ", sizeof(NAMESTRING));
- i++;
- memcpy(printNames[i - 1], "minus ", sizeof(NAMESTRING));
- i++;
- memcpy(printNames[i - 1], "less ", sizeof(NAMESTRING));
- i++;
- memcpy(printNames[i - 1], "print ", sizeof(NAMESTRING));
- numBuiltins = i;
- numNames = i;
- } /* initNames */
-
-
- Static jmp_buf _JL99;
-
-
- /* install - insert new name into printNames */
- Static short install(nm)
- Char *nm;
- {
- long i;
- boolean found;
-
- i = 1;
- found = false;
- while (i <= numNames && !found) {
- if (!memcmp(nm, printNames[i - 1], sizeof(NAMESTRING)))
- found = true;
- else
- i++;
- }
- if (found)
- return i;
- if (i > MAXNAMES) {
- printf("No more room for names\n");
- longjmp(_JL99, 1);
- }
- numNames = i;
- memcpy(printNames[i - 1], nm, sizeof(NAMESTRING));
- return i;
- } /* install */
-
-
- /* prName - print name nm */
- Static Void prName(nm)
- short nm;
- {
- long i;
-
- i = 1;
- while (i <= NAMELENG) {
- if (printNames[nm - 1][i - 1] != ' ') {
- putchar(printNames[nm - 1][i - 1]);
- i++;
- } else
- i = NAMELENG + 1;
- }
- } /* prName */
-
-
- /*****************************************************************
- * INPUT *
- *****************************************************************/
-
- /* isDelim - check if c is a delimiter */
- Static boolean isDelim(c)
- Char c;
- {
- return (c == ';' || c == ' ' || c == ')' || c == '(');
- } /* isDelim */
-
-
- /* skipblanks - return next non-blank position in userinput */
- Static long skipblanks(p)
- long p;
- {
- while (userinput[p - 1] == ' ')
- p++;
- return p;
- } /* skipblanks */
-
-
- /* matches - check if string nm matches userinput[s .. s+ln] */
- Static boolean matches(s, ln, nm)
- long s;
- char ln;
- Char *nm;
- {
- boolean match;
- long i;
-
- match = true;
- i = 1;
- while (match && i <= ln) {
- if (userinput[s - 1] != nm[i - 1])
- match = false;
- i++;
- s++;
- }
- if (!isDelim(userinput[s - 1]))
- match = false;
- return match;
- } /* matches */
-
-
- /* nextchar - read next char - filter tabs and comments */
- Local Void nextchar(c)
- Char *c;
- {
- Char STR1[256];
-
- *c = getchar();
- if (*c == '\n')
- *c = ' ';
- if (*c == (Char)TABCODE) {
- *c = ' ';
- return;
- }
- sprintf(STR1, "%c", *c);
- if (strcmp(STR1, COMMENTCHAR))
- return;
- while (!P_eoln(stdin)) {
- *c = getchar();
- if (*c == '\n')
- *c = ' ';
- }
- *c = ' ';
- } /* nextchar */
-
- /* readParens - read char's, ignoring newlines, to matching ')' */
- Local Void readParens()
- {
- long parencnt;
- Char c;
-
- parencnt = 1;
- do {
- if (P_eoln(stdin))
- fputs(PROMPT2, stdout);
- nextchar(&c);
- pos_++;
- if (pos_ == MAXINPUT) {
- printf("User input too long\n");
- longjmp(_JL99, 1);
- }
- userinput[pos_ - 1] = c;
- if (c == '(')
- parencnt++;
- if (c == ')')
- parencnt--;
- } while (parencnt != 0); /* readParens */
- }
-
- Local Void readInput()
- {
- Char c;
-
- fputs(PROMPT, stdout);
- pos_ = 0;
- do {
- pos_++;
- if (pos_ == MAXINPUT) {
- printf("User input too long\n");
- longjmp(_JL99, 1);
- }
- nextchar(&c);
- userinput[pos_ - 1] = c;
- if (userinput[pos_ - 1] == '(')
- readParens();
- } while (!P_eoln(stdin));
- inputleng = pos_;
- userinput[pos_] = ';'; /* sentinel */
- } /* readInput */
-
-
- /* reader - read char's into userinput; be sure input not blank */
- Static Void reader()
- {
-
- /* readInput - read char's into userinput */
- do {
- readInput();
- pos_ = skipblanks(1L); /* ignore blank lines */
- } while (pos_ > inputleng); /* reader */
- }
-
-
- /* parseName - return (installed) NAME starting at userinput[pos]*/
- Static short parseName()
- {
- NAMESTRING nm; /* array to accumulate characters */
- char leng; /* length of name */
-
- leng = 0;
- while ((pos_ <= inputleng) & (!isDelim(userinput[pos_ - 1]))) {
- if (leng == NAMELENG) {
- printf("Name too long, begins: %.*s\n", NAMELENG, nm);
- longjmp(_JL99, 1);
- }
- leng++;
- nm[leng - 1] = userinput[pos_ - 1];
- pos_++;
- }
- if (leng == 0) {
- printf("Error: expected name, instead read: %c\n", userinput[pos_ - 1]);
- longjmp(_JL99, 1);
- }
- for (; leng < NAMELENG; leng++)
- nm[leng] = ' ';
- pos_ = skipblanks((long)pos_); /* skip blanks after name */
- return (install(nm));
- } /* parseName */
-
-
- /* isVar - check if first character of name n is upper-case */
- Static boolean isVar(n)
- short n;
- {
- return isupper(printNames[n - 1][0]);
- } /* isVar */
-
-
- Local boolean isDigits(pos)
- long pos;
- {
- boolean Result;
-
- if (!isdigit(userinput[pos - 1]))
- return false;
- Result = true;
- while (isdigit(userinput[pos - 1]))
- pos++;
- if (!isDelim(userinput[pos - 1]))
- return false;
- return Result;
- } /* isDigits */
-
-
- /* isNumber - check if a number begins at pos */
- Static boolean isNumber(pos)
- long pos;
- {
-
- /* isDigits - check if sequence of digits begins at pos */
- return (isDigits(pos) | ((userinput[pos - 1] == '-') & isDigits(pos + 1)));
- } /* isNumber */
-
-
- /* parseInt - return number starting at userinput[pos] */
- Static long parseInt()
- {
- long n, sign;
-
- n = 0;
- sign = 1;
- if (userinput[pos_ - 1] == '-') {
- sign = -1;
- pos_++;
- }
- while (isdigit(userinput[pos_ - 1])) {
- n = n * 10 + userinput[pos_ - 1] - '0';
- pos_++;
- }
- pos_ = skipblanks((long)pos_); /* skip blanks after number */
- return (n * sign);
- } /* parseInt */
-
-
- Static EXPLISTREC *parseEL PV();
-
-
- /* parseExp - return EXP starting at userinput[pos] */
- Static EXPREC *parseExp()
- {
- short n;
- EXPLISTREC *el;
-
- if (userinput[pos_ - 1] == '(') {
- pos_ = skipblanks(pos_ + 1L); /* skip '( ..' */
- n = parseName();
- el = parseEL();
- return (mkAPEXP(n, el));
- } else if (isNumber((long)pos_))
- return (mkINTEXP(parseInt()));
- else {
- n = parseName();
- if (isVar(n))
- return (mkVAREXP(mkVariable(n, 0L)));
- else
- return (mkAPEXP(n, NULL));
- }
- } /* parseExp */
-
-
- /* parseEL - return EXPLIST starting at userinput[pos] */
- Static EXPLISTREC *parseEL()
- {
- EXPREC *e;
- EXPLISTREC *el;
-
- if (userinput[pos_ - 1] == ')') {
- pos_ = skipblanks(pos_ + 1L); /* skip ') ..' */
- return NULL;
- } else {
- e = parseExp();
- el = parseEL();
- return (mkExplist(e, el));
- }
- } /* parseEL */
-
-
- /* parseGoal - return GOAL starting at userinput[pos] */
- Static GOALREC *parseGoal()
- {
- short pred;
- EXPLISTREC *il;
-
- if (userinput[pos_ - 1] != '(') {
- pred = parseName();
- il = NULL;
- return (mkGoal(pred, il));
- }
- pos_ = skipblanks(pos_ + 1L); /* skip '( ...' */
- pred = parseName();
- il = parseEL();
- return (mkGoal(pred, il));
- } /* parseGoal */
-
-
- /* parseGL - return GOALLIST starting at userinput[pos] */
- Static GOALLISTREC *parseGL()
- {
- GOALREC *g;
- GOALLISTREC *gl;
-
- if (userinput[pos_ - 1] == ')') {
- pos_ = skipblanks(pos_ + 1L); /* skip ') ..' */
- return NULL;
- } else {
- g = parseGoal();
- gl = parseGL();
- return (mkGoallist(g, gl));
- }
- } /* parseGL */
-
-
- /* parseClause - return CLAUSE at userinput[pos] */
- Static Void parseClause()
- {
- GOALREC *h;
- GOALLISTREC *g;
-
- pos_ = skipblanks(pos_ + 1L); /* skip '( ..' */
- pos_ = skipblanks(pos_ + 5L); /* skip 'infer ..' */
- h = parseGoal();
- if (userinput[pos_ - 1] == ')')
- g = NULL;
- else {
- pos_ = skipblanks(pos_ + 4L); /* skip 'from ..' */
- g = parseGL();
- }
- pos_ = skipblanks(pos_ + 1L); /* skip ') ..' */
- newClause(h, g);
- } /* parseClause */
-
-
- /* parseQuery - return GOALLIST starting at userinput[pos] */
- Static GOALLISTREC *parseQuery()
- {
- GOALLISTREC *Result;
-
- pos_ = skipblanks(pos_ + 1L); /* skip '( ..' */
- pos_ = skipblanks(pos_ + 6L); /* skip 'infer? ..' */
- Result = parseGL();
- pos_ = skipblanks(pos_ + 1L); /* skip ') ..' */
- return Result;
- } /* parseQuery */
-
-
- Static Void prExplist PP((EXPLISTREC *el));
-
- Local Void prVariable(v)
- VARIABLEREC *v;
- {
- prName(v->varname);
- if (v->varindex > 0)
- printf("%ld", v->varindex);
- } /* prVariable */
-
- Local Void prExp(e)
- EXPREC *e;
- {
-
- /* prVariable - print variable, including index */
- switch (e->etype) {
-
- case INTEXP:
- printf("%ld", e->UU.intval);
- break;
-
- case VAREXP:
- prVariable(e->UU.varble);
- break;
-
- case APEXP:
- if (e->UU.U2.args == NULL)
- prName(e->UU.U2.optr);
- else {
- putchar('(');
- prName(e->UU.U2.optr);
- if (e->UU.U2.args != NULL) {
- putchar(' ');
- prExplist(e->UU.U2.args);
- }
- putchar(')');
- }
- break;
- }/* case */
- } /* prExp */
-
-
- /*****************************************************************
- * OUTPUT *
- *****************************************************************/
-
- /* prExplist - print an EXPLIST */
- Static Void prExplist(el)
- EXPLISTREC *el;
- {
-
- /* prExp - print an EXP */
- if (el == NULL)
- return;
- prExp(el->head);
- if (el->tail != NULL) {
- putchar(' ');
- prExplist(el->tail);
- }
- } /* prExplist */
-
-
- /*****************************************************************
- * SUBSTITUTIONS *
- *****************************************************************/
-
- /* emptySubst - create a substitution with no bindings */
- Static SUBSTREC *emptySubst()
- {
- SUBSTREC *s;
-
- s = (SUBSTREC *)Malloc(sizeof(SUBSTREC));
- s->domain = NULL;
- s->range = NULL;
- return s;
- } /* emptySubst */
-
-
- /* bindVar - bind variable v to expression e in sigma */
- Static Void bindVar(v, e, sigma)
- VARIABLEREC *v;
- EXPREC *e;
- SUBSTREC *sigma;
- {
- sigma->domain = mkVarlist(v, sigma->domain);
- sigma->range = mkExplist(e, sigma->range);
- } /* bindVar */
-
-
- /* findVar - look up variable v in sigma */
- Static EXPLISTREC *findVar(v, sigma)
- VARIABLEREC *v;
- SUBSTREC *sigma;
- {
- VARLISTREC *dl;
- EXPLISTREC *rl;
- boolean found;
-
- found = false;
- dl = sigma->domain;
- rl = sigma->range;
- while (dl != NULL && !found) {
- if (eqVar(dl->head, v))
- found = true;
- else {
- dl = dl->tail;
- rl = rl->tail;
- }
- }
- return rl;
- } /* findVar */
-
-
- /* fetch - fetch binding of variable v in sigma */
- Static EXPREC *fetch(v, sigma)
- VARIABLEREC *v;
- SUBSTREC *sigma;
- {
- EXPLISTREC *el;
-
- el = findVar(v, sigma);
- return (el->head);
- } /* fetch */
-
-
- /* isBound - check if variable v is bound in sigma */
- Static boolean isBound(v, sigma)
- VARIABLEREC *v;
- SUBSTREC *sigma;
- {
- return (findVar(v, sigma) != NULL);
- } /* isBound */
-
-
- Static Void applyToExplist PP((SUBSTREC *s, EXPLISTREC *el));
-
-
- /* applyToExp - apply substitution s to e, modifying e */
- Static Void applyToExp(s, e)
- SUBSTREC *s;
- EXPREC **e;
- {
- switch ((*e)->etype) {
-
- case INTEXP:
- /* blank case */
- break;
-
- case VAREXP:
- if (isBound((*e)->UU.varble, s))
- *e = fetch((*e)->UU.varble, s);
- break;
-
- case APEXP:
- applyToExplist(s, (*e)->UU.U2.args);
- break;
- }
- } /* applyToExp */
-
-
- /* applyToExplist - apply substitution s to el, modifying el */
- Static Void applyToExplist(s, el)
- SUBSTREC *s;
- EXPLISTREC *el;
- {
- while (el != NULL) {
- applyToExp(s, &el->head);
- el = el->tail;
- }
- } /* applyToExplist */
-
-
- /* applyToGoal - apply substitution s to g, modifying g */
- Static Void applyToGoal(s, g)
- SUBSTREC *s;
- GOALREC *g;
- {
- applyToExplist(s, g->args);
- } /* applyToGoal */
-
-
- /* applyToGoallist - apply substitution s to gl, modifying gl */
- Static Void applyToGoallist(s, gl)
- SUBSTREC *s;
- GOALLISTREC *gl;
- {
- while (gl != NULL) {
- applyToGoal(s, gl->head);
- gl = gl->tail;
- }
- } /* applyToGoallist */
-
-
- /* compose - change substitution s1 to composition of s1 and s2 */
- Static Void compose(s1, s2)
- SUBSTREC *s1, *s2;
- {
- VARLISTREC *dom;
- EXPLISTREC *rng;
-
- applyToExplist(s2, s1->range);
- if (s1->domain == NULL) {
- s1->domain = s2->domain;
- s1->range = s2->range;
- return;
- }
- dom = s1->domain;
- rng = s1->range;
- while (dom->tail != NULL) {
- dom = dom->tail;
- rng = rng->tail;
- }
- dom->tail = s2->domain;
- rng->tail = s2->range;
- } /* compose */
-
-
- /* Local variables for unify: */
- struct LOC_unify {
- EXPREC *diff1, *diff2;
- } ;
-
- Local boolean findExpDiff PP((EXPREC *e1, EXPREC *e2, struct LOC_unify *LINK));
-
- /* findELDiff - set diff1, diff2 to EXP's where el1, el2 differ */
- Local boolean findELDiff(el1, el2, LINK)
- EXPLISTREC *el1, *el2;
- struct LOC_unify *LINK;
- {
- boolean foundDiff;
-
- foundDiff = false;
- while (el1 != NULL && !foundDiff) {
- foundDiff = findExpDiff(el1->head, el2->head, LINK);
- el1 = el1->tail;
- el2 = el2->tail;
- }
- return foundDiff;
- } /* findELDiff */
-
- /* findExpDiff - set diff1, diff2 to EXP's where e1, e2 differ */
- Local boolean findExpDiff(e1, e2, LINK)
- EXPREC *e1, *e2;
- struct LOC_unify *LINK;
- {
- boolean Result;
-
- Result = true;
- LINK->diff1 = e1;
- LINK->diff2 = e2;
- if (e1->etype != e2->etype)
- return Result;
- switch (e1->etype) {
-
- case VAREXP:
- if (eqVar(e1->UU.varble, e2->UU.varble))
- Result = false;
- break;
-
- case INTEXP:
- if (e1->UU.intval == e2->UU.intval)
- Result = false;
- break;
-
- case APEXP:
- if (e1->UU.U2.optr == e2->UU.U2.optr)
- Result = findELDiff(e1->UU.U2.args, e2->UU.U2.args, LINK);
- break;
- }/* case */
- return Result;
- } /* findExpDiff */
-
- /* occursInExp - check whether variable v occurs in exp e */
- Local boolean occursInExp(v, e, LINK)
- VARIABLEREC *v;
- EXPREC *e;
- struct LOC_unify *LINK;
- {
- boolean Result, occurs;
- EXPLISTREC *el;
-
- switch (e->etype) {
-
- case INTEXP:
- Result = false;
- break;
-
- case VAREXP:
- Result = eqVar(v, e->UU.varble);
- break;
-
- case APEXP:
- occurs = false;
- el = e->UU.U2.args;
- while (el != NULL && !occurs) {
- occurs = occursInExp(v, el->head, LINK);
- el = el->tail;
- }
- Result = occurs;
- break;
- }/* case and with */
- return Result;
- } /* occursInExp */
-
- /* makeSubst - bind d1 to d2 in s, first checking if possible */
- Local Void makeSubst(d1, d2, s, LINK)
- EXPREC *d1, *d2;
- SUBSTREC **s;
- struct LOC_unify *LINK;
- {
- if (d1->etype != VAREXP) {
- *s = NULL;
- return;
- }
- if (occursInExp(d1->UU.varble, d2, LINK))
- *s = NULL;
- else
- bindVar(d1->UU.varble, d2, *s);
- } /* makeSubst */
-
-
- /*****************************************************************
- * UNIFICATION *
- *****************************************************************/
-
- /* unify - unify g1 and g2; return unifying subst. (or nil) */
-
- Static SUBSTREC *unify(g1, g2)
- GOALREC *g1, *g2;
- {
- struct LOC_unify V;
- SUBSTREC *sigma, *varsubst;
- boolean foundDiff;
-
- sigma = emptySubst();
- do {
- foundDiff = findELDiff(g1->args, g2->args, &V);
- varsubst = emptySubst();
- if (foundDiff) {
- if (V.diff1->etype == VAREXP)
- makeSubst(V.diff1, V.diff2, &varsubst, &V);
- else
- makeSubst(V.diff2, V.diff1, &varsubst, &V);
- }
- if (foundDiff && varsubst != NULL) { /* done */
- applyToGoal(varsubst, g1);
- applyToGoal(varsubst, g2);
- compose(sigma, varsubst);
- }
- } while (foundDiff && varsubst != NULL); /* not unifiable */
- if (varsubst == NULL)
- return NULL;
- else
- return sigma;
- } /* unify */
-
-
- /* Local variables for applyPrim: */
- struct LOC_applyPrim {
- boolean Result;
- SUBSTREC **sigma;
- EXPLISTREC *arglist;
- EXPREC *arg1, *arg2, *arg3;
- } ;
-
- Local Void applyArith(op, LINK)
- long op;
- struct LOC_applyPrim *LINK;
- {
- long i;
-
- LINK->arg3 = LINK->arglist->tail->tail->head;
- if (LINK->arg3->etype == APEXP) {
- LINK->Result = false;
- return;
- }
- switch (op) {
-
- case 1:
- i = LINK->arg1->UU.intval + LINK->arg2->UU.intval;
- break;
-
- case 2:
- i = LINK->arg1->UU.intval - LINK->arg2->UU.intval;
- break;
- }
- if (LINK->arg3->etype == INTEXP) {
- if (LINK->arg3->UU.intval != i)
- LINK->Result = false;
- } else
- bindVar(LINK->arg3->UU.varble, mkINTEXP(i), *LINK->sigma);
-
- /* applyPrim already true */
- } /* applyArith */
-
-
- /*****************************************************************
- * EVALUATION *
- *****************************************************************/
-
- /* applyPrim - apply primitive predicate, modifying sigma */
- Static boolean applyPrim(g, sigma_)
- GOALREC *g;
- SUBSTREC **sigma_;
- {
- struct LOC_applyPrim V;
-
- V.sigma = sigma_;
- *V.sigma = emptySubst();
- V.Result = true;
- V.arglist = g->args;
- if (g->pred == 4) { /* print */
- prExplist(V.arglist);
- putchar('\n');
- return V.Result;
- }
- V.arg1 = V.arglist->head;
- V.arg2 = V.arglist->tail->head;
- if (V.arg1->etype != INTEXP || V.arg2->etype != INTEXP)
- return false;
- switch (g->pred) {
-
- case 1:
- case 2: /* plus, minus */
- applyArith((long)g->pred, &V);
- break;
-
- case 3: /* less */
- if (V.arg1->UU.intval >= V.arg2->UU.intval)
- V.Result = false;
- break;
- }/* case */
- return V.Result;
- } /* applyPrim */
-
-
- Static GOALREC *copyGoal PP((GOALREC *g, long id));
-
-
- /* copyGoallist - copy gl; rename variables if id<>0 */
- Static GOALLISTREC *copyGoallist(gl, id)
- GOALLISTREC *gl;
- long id;
- {
- if (gl == NULL)
- return NULL;
- else
- return (mkGoallist(copyGoal(gl->head, id), copyGoallist(gl->tail, id)));
- } /* copyGoallist */
-
-
- /* Local variables for copyGoal: */
- struct LOC_copyGoal {
- long id;
- } ;
-
- Local EXPLISTREC *copyExplist PP((EXPLISTREC *el, struct LOC_copyGoal *LINK));
-
- /* Local variables for copyExplist: */
- struct LOC_copyExplist {
- struct LOC_copyGoal *LINK;
- } ;
-
- Local EXPREC *copyExp(e, LINK)
- EXPREC *e;
- struct LOC_copyExplist *LINK;
- {
- EXPREC *Result;
-
- switch (e->etype) {
-
- case INTEXP:
- Result = e;
- break;
-
- case VAREXP:
- if (LINK->LINK->id == 0)
- Result = mkVAREXP(mkVariable(e->UU.varble->varname,
- e->UU.varble->varindex));
- else
- Result = mkVAREXP(mkVariable(e->UU.varble->varname, LINK->LINK->id));
- break;
-
- case APEXP:
- Result = mkAPEXP(e->UU.U2.optr, copyExplist(e->UU.U2.args, LINK->LINK));
- break;
- }/* case */
- return Result;
- } /* copyExp */
-
- Local EXPLISTREC *copyExplist(el, LINK)
- EXPLISTREC *el;
- struct LOC_copyGoal *LINK;
- {
-
- /* copyExp - copy e; rename variables if id<>0 */
- struct LOC_copyExplist V;
-
- V.LINK = LINK;
- if (el == NULL)
- return NULL;
- else
- return (mkExplist(copyExp(el->head, &V), copyExplist(el->tail, LINK)));
- } /* copyExplist */
-
-
- /* copyGoal - copy g; rename variables if id<>0 */
- Static GOALREC *copyGoal(g, id_)
- GOALREC *g;
- long id_;
- {
-
- /* copyExplist - copy el; rename variables if id<>0 */
- struct LOC_copyGoal V;
-
- V.id = id_;
- return (mkGoal(g->pred, copyExplist(g->args, &V)));
- } /* copyGoal */
-
-
- /* append - append second to end of first, modifying first */
- Static GOALLISTREC *append(first, second)
- GOALLISTREC *first, *second;
- {
- GOALLISTREC *Result;
-
- if (first == NULL)
- return second;
- Result = first;
- while (first->tail != NULL)
- first = first->tail;
- first->tail = second;
- return Result;
- } /* append */
-
-
- Static SUBSTREC *prove PP((GOALLISTREC *gl, long id));
-
- /* Local variables for prove: */
- struct LOC_prove {
- long id;
- SUBSTREC *sigma0;
- } ;
-
- /* tryClause - try to match goal g and clause head of c */
- Local SUBSTREC *tryClause(clgoal, g, LINK)
- GOALREC *clgoal, *g;
- struct LOC_prove *LINK;
- {
- SUBSTREC *Result;
-
- Result = NULL;
- if (!((clgoal->pred == g->pred) & (lengthEL(clgoal->args) == lengthEL(g->args))))
- return Result;
- clgoal = copyGoal(clgoal, LINK->id);
- g = copyGoal(g, 0L);
- return (unify(clgoal, g));
- /* p2c: prolog.p: Note: Deleting unreachable code [255] */
- } /* tryClause */
-
- /* proveRest - add subgoals to restofgoals and prove */
- Local SUBSTREC *proveRest(subgoals, restofgoals, LINK)
- GOALLISTREC *subgoals, *restofgoals;
- struct LOC_prove *LINK;
- {
- subgoals = copyGoallist(subgoals, LINK->id);
- applyToGoallist(LINK->sigma0, subgoals);
- restofgoals = copyGoallist(restofgoals, 0L);
- applyToGoallist(LINK->sigma0, restofgoals);
- return (prove(append(subgoals, restofgoals), LINK->id + 1));
- } /* proveRest */
-
-
- /* prove - prove goals gl; return subst; id used to rename var's */
- Static SUBSTREC *prove(gl, id_)
- GOALLISTREC *gl;
- long id_;
- {
- struct LOC_prove V;
- CLAUSEREC *cl;
- SUBSTREC *sigma1;
-
- V.id = id_;
- if (gl == NULL)
- return (emptySubst());
- else {
- if (gl->head->pred <= numBuiltins) {
- if (applyPrim(gl->head, &V.sigma0)) {
- applyToGoallist(V.sigma0, gl->tail);
- sigma1 = prove(gl->tail, V.id + 1);
- } else
- sigma1 = NULL;
- } else {
- sigma1 = NULL;
- cl = clauses;
- while (cl != NULL && sigma1 == NULL) {
- V.sigma0 = tryClause(cl->lhs, gl->head, &V);
- if (V.sigma0 != NULL)
- sigma1 = proveRest(cl->rhs, gl->tail, &V);
- cl = cl->nextclause;
- } /* while */
- }
- if (sigma1 == NULL)
- return NULL;
- else {
- compose(V.sigma0, sigma1);
- return V.sigma0;
- }
- }
- } /* prove */
-
-
- /*****************************************************************
- * READ-EVAL-PRINT LOOP *
- *****************************************************************/
-
- main(argc, argv)
- int argc;
- Char *argv[];
- { /* prolog main */
- PASCAL_MAIN(argc, argv);
- if (setjmp(_JL99))
- goto _L99;
- initNames();
-
- quittingtime = false;
- _L99:
- while (!quittingtime) {
- reader();
- if (matches((long)pos_, 4, "quit ")) {
- quittingtime = true;
- break;
- }
- if (matches(skipblanks(pos_ + 1L), 5, "infer ")) {
- parseClause();
- putchar('\n');
- } else {
- toplevelGoal = parseQuery();
- putchar('\n');
- if (prove(toplevelGoal, 1L) == NULL)
- printf("Not satisfied\n");
- else
- printf("Satisfied\n");
- putchar('\n');
- }
- }
- exit(0);
- } /* prolog */
-
-
-
- /* End. */
-