home *** CD-ROM | disk | FTP | other *** search
/ Frozen Fish 1: Amiga / FrozenFish-Apr94.iso / bbs / alib / d5xx / d524 / kamin.lha / Kamin / src.lzh / prolog.c < prev    next >
C/C++ Source or Header  |  1991-06-28  |  28KB  |  1,304 lines
  1. /* Output from p2c, the Pascal-to-C translator */
  2. /* From input file "prolog.p" */
  3.  
  4.  
  5. /*****************************************************************
  6.  *                     DECLARATIONS                              *
  7.  *****************************************************************/
  8.  
  9. #include <p2c/p2c.h>
  10.  
  11.  
  12. #define NAMELENG        20   /* Maximum length of a name */
  13. #define MAXNAMES        300   /* Maximum number of different names */
  14. #define MAXINPUT        2000   /* Maximum length of an input */
  15.  
  16. #define PROMPT          "-> "
  17. #define PROMPT2         "> "
  18. #define COMMENTCHAR     ";"
  19.  
  20. #define TABCODE         9   /* in ASCII */
  21.  
  22.  
  23. typedef Char NAMESTRING[NAMELENG];
  24.  
  25. /* a NAME is an index in printNames */
  26.  
  27.  
  28. typedef struct GOALREC {
  29.   short pred;
  30.   struct EXPLISTREC *args;
  31. } GOALREC;
  32.  
  33. typedef struct GOALLISTREC {
  34.   GOALREC *head;
  35.   struct GOALLISTREC *tail;
  36. } GOALLISTREC;
  37.  
  38. typedef struct VARIABLEREC {
  39.   short varname;
  40.   long varindex;
  41. } VARIABLEREC;
  42.  
  43. typedef struct VARLISTREC {
  44.   VARIABLEREC *head;
  45.   struct VARLISTREC *tail;
  46. } VARLISTREC;
  47.  
  48. typedef enum {
  49.   VAREXP, INTEXP, APEXP
  50. } EXPTYPE;
  51.  
  52. typedef struct EXPREC {
  53.   EXPTYPE etype;
  54.   union {
  55.     VARIABLEREC *varble;
  56.     long intval;
  57.     struct {
  58.       short optr;
  59.       struct EXPLISTREC *args;
  60.     } U2;
  61.   } UU;
  62. } EXPREC;
  63.  
  64. typedef struct EXPLISTREC {
  65.   EXPREC *head;
  66.   struct EXPLISTREC *tail;
  67. } EXPLISTREC;
  68.  
  69. typedef struct CLAUSEREC {
  70.   GOALREC *lhs;
  71.   GOALLISTREC *rhs;
  72.   struct CLAUSEREC *nextclause;
  73. } CLAUSEREC;
  74.  
  75. typedef struct SUBSTREC {
  76.   VARLISTREC *domain;
  77.   EXPLISTREC *range;
  78. } SUBSTREC;
  79.  
  80.  
  81. Static CLAUSEREC *clauses, *lastclause;
  82.  
  83. Static GOALLISTREC *toplevelGoal;
  84.  
  85. Static Char userinput[MAXINPUT];
  86. Static short inputleng, pos_;
  87.  
  88. Static NAMESTRING printNames[MAXNAMES];
  89. Static short numNames, numBuiltins;
  90.  
  91. Static boolean quittingtime;
  92.  
  93.  
  94. /*****************************************************************
  95.  *                     DATA STRUCTURE OP'S                       *
  96.  *****************************************************************/
  97.  
  98. /* mkGoal - create a new GOAL with pred p and arguments a        */
  99. Static GOALREC *mkGoal(p, a)
  100. short p;
  101. EXPLISTREC *a;
  102. {
  103.   GOALREC *newg;
  104.  
  105.   newg = (GOALREC *)Malloc(sizeof(GOALREC));
  106.   newg->pred = p;
  107.   newg->args = a;
  108.   return newg;
  109. }  /* mkGoal */
  110.  
  111.  
  112. /* mkVAREXP - create a new EXP of type VAREXP                    */
  113. Static EXPREC *mkVAREXP(v)
  114. VARIABLEREC *v;
  115. {
  116.   EXPREC *newe;
  117.  
  118.   newe = (EXPREC *)Malloc(sizeof(EXPREC));
  119.   newe->etype = VAREXP;
  120.   newe->UU.varble = v;
  121.   return newe;
  122. }  /* mkVAREXP */
  123.  
  124.  
  125. /* mkINTEXP - create a new EXP of type INTEXP                    */
  126. Static EXPREC *mkINTEXP(n)
  127. long n;
  128. {
  129.   EXPREC *newe;
  130.  
  131.   newe = (EXPREC *)Malloc(sizeof(EXPREC));
  132.   newe->etype = INTEXP;
  133.   newe->UU.intval = n;
  134.   return newe;
  135. }  /* mkINTEXP */
  136.  
  137.  
  138. /* mkAPEXP - create a new EXP of type APEXP                      */
  139. Static EXPREC *mkAPEXP(o, a)
  140. short o;
  141. EXPLISTREC *a;
  142. {
  143.   EXPREC *newe;
  144.  
  145.   newe = (EXPREC *)Malloc(sizeof(EXPREC));
  146.   newe->etype = APEXP;
  147.   newe->UU.U2.optr = o;
  148.   newe->UU.U2.args = a;
  149.   return newe;
  150. }  /* mkAPEXP */
  151.  
  152.  
  153. /* mkVariable - create a new VARIABLE with name n and index i    */
  154. Static VARIABLEREC *mkVariable(n, i)
  155. short n;
  156. long i;
  157. {
  158.   VARIABLEREC *newv;
  159.  
  160.   newv = (VARIABLEREC *)Malloc(sizeof(VARIABLEREC));
  161.   newv->varname = n;
  162.   newv->varindex = i;
  163.   return newv;
  164. }  /* mkVariable */
  165.  
  166.  
  167. /* mkVarlist - create a new VARLIST with head v and tail vl      */
  168. Static VARLISTREC *mkVarlist(v, vl)
  169. VARIABLEREC *v;
  170. VARLISTREC *vl;
  171. {
  172.   VARLISTREC *newvl;
  173.  
  174.   newvl = (VARLISTREC *)Malloc(sizeof(VARLISTREC));
  175.   newvl->head = v;
  176.   newvl->tail = vl;
  177.   return newvl;
  178. }  /* mkVarlist */
  179.  
  180.  
  181. /* mkGoallist - return a GOALLIST with head g and tail gl        */
  182. Static GOALLISTREC *mkGoallist(g, gl)
  183. GOALREC *g;
  184. GOALLISTREC *gl;
  185. {
  186.   GOALLISTREC *newgl;
  187.  
  188.   newgl = (GOALLISTREC *)Malloc(sizeof(GOALLISTREC));
  189.   newgl->head = g;
  190.   newgl->tail = gl;
  191.   return newgl;
  192. }  /* mkGoallist */
  193.  
  194.  
  195. /* mkExplist - return an EXPLIST with head e and tail el         */
  196. Static EXPLISTREC *mkExplist(e, el)
  197. EXPREC *e;
  198. EXPLISTREC *el;
  199. {
  200.   EXPLISTREC *newel;
  201.  
  202.   newel = (EXPLISTREC *)Malloc(sizeof(EXPLISTREC));
  203.   newel->head = e;
  204.   newel->tail = el;
  205.   return newel;
  206. }  /* mkExplist */
  207.  
  208.  
  209. /* mkClause - create a new GOAL with lhs l and rhs r             */
  210. Static CLAUSEREC *mkClause(l, r)
  211. GOALREC *l;
  212. GOALLISTREC *r;
  213. {
  214.   CLAUSEREC *c;
  215.  
  216.   c = (CLAUSEREC *)Malloc(sizeof(CLAUSEREC));
  217.   c->lhs = l;
  218.   c->rhs = r;
  219.   c->nextclause = NULL;
  220.   return c;
  221. }  /* mkClause */
  222.  
  223.  
  224. /* eqVar - compare two VARIABLE's for equality                   */
  225. Static boolean eqVar(v1, v2)
  226. VARIABLEREC *v1, *v2;
  227. {
  228.   return (v1->varname == v2->varname && v1->varindex == v2->varindex);
  229. }  /* eqVar */
  230.  
  231.  
  232. /* lengthEL - return length of EXPLIST el                        */
  233. Static long lengthEL(el)
  234. EXPLISTREC *el;
  235. {
  236.   long i;
  237.  
  238.   i = 0;
  239.   while (el != NULL) {
  240.     i++;
  241.     el = el->tail;
  242.   }
  243.   return i;
  244. }  /* lengthEL */
  245.  
  246.  
  247. /*****************************************************************
  248.  *                     NAME MANAGEMENT                           *
  249.  *****************************************************************/
  250.  
  251. /* newClause - add new clause at end of clauses list             */
  252. Static Void newClause(l, r)
  253. GOALREC *l;
  254. GOALLISTREC *r;
  255. {
  256.   if (lastclause == NULL) {
  257.     clauses = mkClause(l, r);
  258.     lastclause = clauses;
  259.   } else {
  260.     lastclause->nextclause = mkClause(l, r);
  261.     lastclause = lastclause->nextclause;
  262.   }
  263. }  /* newClause */
  264.  
  265.  
  266. /* initNames - place all pre-defined names into printNames       */
  267. Static Void initNames()
  268. {
  269.   long i;
  270.  
  271.   clauses = NULL;
  272.   lastclause = NULL;
  273.   i = 1;
  274.   memcpy(printNames[i - 1], "plus                ", sizeof(NAMESTRING));
  275.   i++;
  276.   memcpy(printNames[i - 1], "minus               ", sizeof(NAMESTRING));
  277.   i++;
  278.   memcpy(printNames[i - 1], "less                ", sizeof(NAMESTRING));
  279.   i++;
  280.   memcpy(printNames[i - 1], "print               ", sizeof(NAMESTRING));
  281.   numBuiltins = i;
  282.   numNames = i;
  283. }  /* initNames */
  284.  
  285.  
  286. Static jmp_buf _JL99;
  287.  
  288.  
  289. /* install - insert new name into printNames                     */
  290. Static short install(nm)
  291. Char *nm;
  292. {
  293.   long i;
  294.   boolean found;
  295.  
  296.   i = 1;
  297.   found = false;
  298.   while (i <= numNames && !found) {
  299.     if (!memcmp(nm, printNames[i - 1], sizeof(NAMESTRING)))
  300.       found = true;
  301.     else
  302.       i++;
  303.   }
  304.   if (found)
  305.     return i;
  306.   if (i > MAXNAMES) {
  307.     printf("No more room for names\n");
  308.     longjmp(_JL99, 1);
  309.   }
  310.   numNames = i;
  311.   memcpy(printNames[i - 1], nm, sizeof(NAMESTRING));
  312.   return i;
  313. }  /* install */
  314.  
  315.  
  316. /* prName - print name nm                                        */
  317. Static Void prName(nm)
  318. short nm;
  319. {
  320.   long i;
  321.  
  322.   i = 1;
  323.   while (i <= NAMELENG) {
  324.     if (printNames[nm - 1][i - 1] != ' ') {
  325.       putchar(printNames[nm - 1][i - 1]);
  326.       i++;
  327.     } else
  328.       i = NAMELENG + 1;
  329.   }
  330. }  /* prName */
  331.  
  332.  
  333. /*****************************************************************
  334.  *                      INPUT                                    *
  335.  *****************************************************************/
  336.  
  337. /* isDelim - check if c is a delimiter                           */
  338. Static boolean isDelim(c)
  339. Char c;
  340. {
  341.   return (c == ';' || c == ' ' || c == ')' || c == '(');
  342. }  /* isDelim */
  343.  
  344.  
  345. /* skipblanks - return next non-blank position in userinput      */
  346. Static long skipblanks(p)
  347. long p;
  348. {
  349.   while (userinput[p - 1] == ' ')
  350.     p++;
  351.   return p;
  352. }  /* skipblanks */
  353.  
  354.  
  355. /* matches - check if string nm matches userinput[s .. s+ln]     */
  356. Static boolean matches(s, ln, nm)
  357. long s;
  358. char ln;
  359. Char *nm;
  360. {
  361.   boolean match;
  362.   long i;
  363.  
  364.   match = true;
  365.   i = 1;
  366.   while (match && i <= ln) {
  367.     if (userinput[s - 1] != nm[i - 1])
  368.       match = false;
  369.     i++;
  370.     s++;
  371.   }
  372.   if (!isDelim(userinput[s - 1]))
  373.     match = false;
  374.   return match;
  375. }  /* matches */
  376.  
  377.  
  378. /* nextchar - read next char - filter tabs and comments          */
  379. Local Void nextchar(c)
  380. Char *c;
  381. {
  382.   Char STR1[256];
  383.  
  384.   *c = getchar();
  385.   if (*c == '\n')
  386.     *c = ' ';
  387.   if (*c == (Char)TABCODE) {
  388.     *c = ' ';
  389.     return;
  390.   }
  391.   sprintf(STR1, "%c", *c);
  392.   if (strcmp(STR1, COMMENTCHAR))
  393.     return;
  394.   while (!P_eoln(stdin)) {
  395.     *c = getchar();
  396.     if (*c == '\n')
  397.       *c = ' ';
  398.   }
  399.   *c = ' ';
  400. }  /* nextchar */
  401.  
  402. /* readParens - read char's, ignoring newlines, to matching ')'  */
  403. Local Void readParens()
  404. {
  405.   long parencnt;
  406.   Char c;
  407.  
  408.   parencnt = 1;
  409.   do {
  410.     if (P_eoln(stdin))
  411.       fputs(PROMPT2, stdout);
  412.     nextchar(&c);
  413.     pos_++;
  414.     if (pos_ == MAXINPUT) {
  415.       printf("User input too long\n");
  416.       longjmp(_JL99, 1);
  417.     }
  418.     userinput[pos_ - 1] = c;
  419.     if (c == '(')
  420.       parencnt++;
  421.     if (c == ')')
  422.       parencnt--;
  423.   } while (parencnt != 0);   /* readParens */
  424. }
  425.  
  426. Local Void readInput()
  427. {
  428.   Char c;
  429.  
  430.   fputs(PROMPT, stdout);
  431.   pos_ = 0;
  432.   do {
  433.     pos_++;
  434.     if (pos_ == MAXINPUT) {
  435.       printf("User input too long\n");
  436.       longjmp(_JL99, 1);
  437.     }
  438.     nextchar(&c);
  439.     userinput[pos_ - 1] = c;
  440.     if (userinput[pos_ - 1] == '(')
  441.       readParens();
  442.   } while (!P_eoln(stdin));
  443.   inputleng = pos_;
  444.   userinput[pos_] = ';';   /* sentinel */
  445. }  /* readInput */
  446.  
  447.  
  448. /* reader - read char's into userinput; be sure input not blank  */
  449. Static Void reader()
  450. {
  451.  
  452.   /* readInput - read char's into userinput                        */
  453.   do {
  454.     readInput();
  455.     pos_ = skipblanks(1L);   /* ignore blank lines */
  456.   } while (pos_ > inputleng);   /* reader */
  457. }
  458.  
  459.  
  460. /* parseName - return (installed) NAME starting at userinput[pos]*/
  461. Static short parseName()
  462. {
  463.   NAMESTRING nm;   /* array to accumulate characters */
  464.   char leng;   /* length of name */
  465.  
  466.   leng = 0;
  467.   while ((pos_ <= inputleng) & (!isDelim(userinput[pos_ - 1]))) {
  468.     if (leng == NAMELENG) {
  469.       printf("Name too long, begins: %.*s\n", NAMELENG, nm);
  470.       longjmp(_JL99, 1);
  471.     }
  472.     leng++;
  473.     nm[leng - 1] = userinput[pos_ - 1];
  474.     pos_++;
  475.   }
  476.   if (leng == 0) {
  477.     printf("Error: expected name, instead read: %c\n", userinput[pos_ - 1]);
  478.     longjmp(_JL99, 1);
  479.   }
  480.   for (; leng < NAMELENG; leng++)
  481.     nm[leng] = ' ';
  482.   pos_ = skipblanks((long)pos_);   /* skip blanks after name */
  483.   return (install(nm));
  484. }  /* parseName */
  485.  
  486.  
  487. /* isVar - check if first character of name n is upper-case      */
  488. Static boolean isVar(n)
  489. short n;
  490. {
  491.   return isupper(printNames[n - 1][0]);
  492. }  /* isVar */
  493.  
  494.  
  495. Local boolean isDigits(pos)
  496. long pos;
  497. {
  498.   boolean Result;
  499.  
  500.   if (!isdigit(userinput[pos - 1]))
  501.     return false;
  502.   Result = true;
  503.   while (isdigit(userinput[pos - 1]))
  504.     pos++;
  505.   if (!isDelim(userinput[pos - 1]))
  506.     return false;
  507.   return Result;
  508. }  /* isDigits */
  509.  
  510.  
  511. /* isNumber - check if a number begins at pos                    */
  512. Static boolean isNumber(pos)
  513. long pos;
  514. {
  515.  
  516.   /* isDigits - check if sequence of digits begins at pos          */
  517.   return (isDigits(pos) | ((userinput[pos - 1] == '-') & isDigits(pos + 1)));
  518. }  /* isNumber */
  519.  
  520.  
  521. /* parseInt - return number starting at userinput[pos]           */
  522. Static long parseInt()
  523. {
  524.   long n, sign;
  525.  
  526.   n = 0;
  527.   sign = 1;
  528.   if (userinput[pos_ - 1] == '-') {
  529.     sign = -1;
  530.     pos_++;
  531.   }
  532.   while (isdigit(userinput[pos_ - 1])) {
  533.     n = n * 10 + userinput[pos_ - 1] - '0';
  534.     pos_++;
  535.   }
  536.   pos_ = skipblanks((long)pos_);   /* skip blanks after number */
  537.   return (n * sign);
  538. }  /* parseInt */
  539.  
  540.  
  541. Static EXPLISTREC *parseEL PV();
  542.  
  543.  
  544. /* parseExp - return EXP starting at userinput[pos]              */
  545. Static EXPREC *parseExp()
  546. {
  547.   short n;
  548.   EXPLISTREC *el;
  549.  
  550.   if (userinput[pos_ - 1] == '(') {
  551.     pos_ = skipblanks(pos_ + 1L);   /* skip '( ..' */
  552.     n = parseName();
  553.     el = parseEL();
  554.     return (mkAPEXP(n, el));
  555.   } else if (isNumber((long)pos_))
  556.     return (mkINTEXP(parseInt()));
  557.   else {
  558.     n = parseName();
  559.     if (isVar(n))
  560.       return (mkVAREXP(mkVariable(n, 0L)));
  561.     else
  562.       return (mkAPEXP(n, NULL));
  563.   }
  564. }  /* parseExp */
  565.  
  566.  
  567. /* parseEL - return EXPLIST starting at userinput[pos]           */
  568. Static EXPLISTREC *parseEL()
  569. {
  570.   EXPREC *e;
  571.   EXPLISTREC *el;
  572.  
  573.   if (userinput[pos_ - 1] == ')') {
  574.     pos_ = skipblanks(pos_ + 1L);   /* skip ') ..' */
  575.     return NULL;
  576.   } else {
  577.     e = parseExp();
  578.     el = parseEL();
  579.     return (mkExplist(e, el));
  580.   }
  581. }  /* parseEL */
  582.  
  583.  
  584. /* parseGoal - return GOAL starting at userinput[pos]            */
  585. Static GOALREC *parseGoal()
  586. {
  587.   short pred;
  588.   EXPLISTREC *il;
  589.  
  590.   if (userinput[pos_ - 1] != '(') {
  591.     pred = parseName();
  592.     il = NULL;
  593.     return (mkGoal(pred, il));
  594.   }
  595.   pos_ = skipblanks(pos_ + 1L);   /* skip '( ...' */
  596.   pred = parseName();
  597.   il = parseEL();
  598.   return (mkGoal(pred, il));
  599. }  /* parseGoal */
  600.  
  601.  
  602. /* parseGL - return GOALLIST starting at userinput[pos]          */
  603. Static GOALLISTREC *parseGL()
  604. {
  605.   GOALREC *g;
  606.   GOALLISTREC *gl;
  607.  
  608.   if (userinput[pos_ - 1] == ')') {
  609.     pos_ = skipblanks(pos_ + 1L);   /* skip ') ..' */
  610.     return NULL;
  611.   } else {
  612.     g = parseGoal();
  613.     gl = parseGL();
  614.     return (mkGoallist(g, gl));
  615.   }
  616. }  /* parseGL */
  617.  
  618.  
  619. /* parseClause - return CLAUSE at userinput[pos]                 */
  620. Static Void parseClause()
  621. {
  622.   GOALREC *h;
  623.   GOALLISTREC *g;
  624.  
  625.   pos_ = skipblanks(pos_ + 1L);   /* skip '( ..' */
  626.   pos_ = skipblanks(pos_ + 5L);   /* skip 'infer ..' */
  627.   h = parseGoal();
  628.   if (userinput[pos_ - 1] == ')')
  629.     g = NULL;
  630.   else {
  631.     pos_ = skipblanks(pos_ + 4L);   /* skip 'from ..' */
  632.     g = parseGL();
  633.   }
  634.   pos_ = skipblanks(pos_ + 1L);   /* skip ') ..' */
  635.   newClause(h, g);
  636. }  /* parseClause */
  637.  
  638.  
  639. /* parseQuery - return GOALLIST starting at userinput[pos]       */
  640. Static GOALLISTREC *parseQuery()
  641. {
  642.   GOALLISTREC *Result;
  643.  
  644.   pos_ = skipblanks(pos_ + 1L);   /* skip '( ..' */
  645.   pos_ = skipblanks(pos_ + 6L);   /* skip 'infer? ..' */
  646.   Result = parseGL();
  647.   pos_ = skipblanks(pos_ + 1L);   /* skip ') ..' */
  648.   return Result;
  649. }  /* parseQuery */
  650.  
  651.  
  652. Static Void prExplist PP((EXPLISTREC *el));
  653.  
  654. Local Void prVariable(v)
  655. VARIABLEREC *v;
  656. {
  657.   prName(v->varname);
  658.   if (v->varindex > 0)
  659.     printf("%ld", v->varindex);
  660. }  /* prVariable */
  661.  
  662. Local Void prExp(e)
  663. EXPREC *e;
  664. {
  665.  
  666.   /* prVariable - print variable, including index                  */
  667.   switch (e->etype) {
  668.  
  669.   case INTEXP:
  670.     printf("%ld", e->UU.intval);
  671.     break;
  672.  
  673.   case VAREXP:
  674.     prVariable(e->UU.varble);
  675.     break;
  676.  
  677.   case APEXP:
  678.     if (e->UU.U2.args == NULL)
  679.       prName(e->UU.U2.optr);
  680.     else {
  681.       putchar('(');
  682.       prName(e->UU.U2.optr);
  683.       if (e->UU.U2.args != NULL) {
  684.     putchar(' ');
  685.     prExplist(e->UU.U2.args);
  686.       }
  687.       putchar(')');
  688.     }
  689.     break;
  690.   }/* case */
  691. }  /* prExp */
  692.  
  693.  
  694. /*****************************************************************
  695.  *                     OUTPUT                                    *
  696.  *****************************************************************/
  697.  
  698. /* prExplist - print an EXPLIST                                  */
  699. Static Void prExplist(el)
  700. EXPLISTREC *el;
  701. {
  702.  
  703.   /* prExp - print an EXP                                          */
  704.   if (el == NULL)
  705.     return;
  706.   prExp(el->head);
  707.   if (el->tail != NULL) {
  708.     putchar(' ');
  709.     prExplist(el->tail);
  710.   }
  711. }  /* prExplist */
  712.  
  713.  
  714. /*****************************************************************
  715.  *                     SUBSTITUTIONS                             *
  716.  *****************************************************************/
  717.  
  718. /* emptySubst - create a substitution with no bindings           */
  719. Static SUBSTREC *emptySubst()
  720. {
  721.   SUBSTREC *s;
  722.  
  723.   s = (SUBSTREC *)Malloc(sizeof(SUBSTREC));
  724.   s->domain = NULL;
  725.   s->range = NULL;
  726.   return s;
  727. }  /* emptySubst */
  728.  
  729.  
  730. /* bindVar - bind variable v to expression e in sigma            */
  731. Static Void bindVar(v, e, sigma)
  732. VARIABLEREC *v;
  733. EXPREC *e;
  734. SUBSTREC *sigma;
  735. {
  736.   sigma->domain = mkVarlist(v, sigma->domain);
  737.   sigma->range = mkExplist(e, sigma->range);
  738. }  /* bindVar */
  739.  
  740.  
  741. /* findVar - look up variable v in sigma                         */
  742. Static EXPLISTREC *findVar(v, sigma)
  743. VARIABLEREC *v;
  744. SUBSTREC *sigma;
  745. {
  746.   VARLISTREC *dl;
  747.   EXPLISTREC *rl;
  748.   boolean found;
  749.  
  750.   found = false;
  751.   dl = sigma->domain;
  752.   rl = sigma->range;
  753.   while (dl != NULL && !found) {
  754.     if (eqVar(dl->head, v))
  755.       found = true;
  756.     else {
  757.       dl = dl->tail;
  758.       rl = rl->tail;
  759.     }
  760.   }
  761.   return rl;
  762. }  /* findVar */
  763.  
  764.  
  765. /* fetch - fetch binding of variable v in sigma                  */
  766. Static EXPREC *fetch(v, sigma)
  767. VARIABLEREC *v;
  768. SUBSTREC *sigma;
  769. {
  770.   EXPLISTREC *el;
  771.  
  772.   el = findVar(v, sigma);
  773.   return (el->head);
  774. }  /* fetch */
  775.  
  776.  
  777. /* isBound - check if variable v is bound in sigma               */
  778. Static boolean isBound(v, sigma)
  779. VARIABLEREC *v;
  780. SUBSTREC *sigma;
  781. {
  782.   return (findVar(v, sigma) != NULL);
  783. }  /* isBound */
  784.  
  785.  
  786. Static Void applyToExplist PP((SUBSTREC *s, EXPLISTREC *el));
  787.  
  788.  
  789. /* applyToExp - apply substitution s to e, modifying e           */
  790. Static Void applyToExp(s, e)
  791. SUBSTREC *s;
  792. EXPREC **e;
  793. {
  794.   switch ((*e)->etype) {
  795.  
  796.   case INTEXP:
  797.     /* blank case */
  798.     break;
  799.  
  800.   case VAREXP:
  801.     if (isBound((*e)->UU.varble, s))
  802.       *e = fetch((*e)->UU.varble, s);
  803.     break;
  804.  
  805.   case APEXP:
  806.     applyToExplist(s, (*e)->UU.U2.args);
  807.     break;
  808.   }
  809. }  /* applyToExp */
  810.  
  811.  
  812. /* applyToExplist - apply substitution s to el, modifying el     */
  813. Static Void applyToExplist(s, el)
  814. SUBSTREC *s;
  815. EXPLISTREC *el;
  816. {
  817.   while (el != NULL) {
  818.     applyToExp(s, &el->head);
  819.     el = el->tail;
  820.   }
  821. }  /* applyToExplist */
  822.  
  823.  
  824. /* applyToGoal - apply substitution s to g, modifying g          */
  825. Static Void applyToGoal(s, g)
  826. SUBSTREC *s;
  827. GOALREC *g;
  828. {
  829.   applyToExplist(s, g->args);
  830. }  /* applyToGoal */
  831.  
  832.  
  833. /* applyToGoallist - apply substitution s to gl, modifying gl    */
  834. Static Void applyToGoallist(s, gl)
  835. SUBSTREC *s;
  836. GOALLISTREC *gl;
  837. {
  838.   while (gl != NULL) {
  839.     applyToGoal(s, gl->head);
  840.     gl = gl->tail;
  841.   }
  842. }  /* applyToGoallist */
  843.  
  844.  
  845. /* compose - change substitution s1 to composition of s1 and s2  */
  846. Static Void compose(s1, s2)
  847. SUBSTREC *s1, *s2;
  848. {
  849.   VARLISTREC *dom;
  850.   EXPLISTREC *rng;
  851.  
  852.   applyToExplist(s2, s1->range);
  853.   if (s1->domain == NULL) {
  854.     s1->domain = s2->domain;
  855.     s1->range = s2->range;
  856.     return;
  857.   }
  858.   dom = s1->domain;
  859.   rng = s1->range;
  860.   while (dom->tail != NULL) {
  861.     dom = dom->tail;
  862.     rng = rng->tail;
  863.   }
  864.   dom->tail = s2->domain;
  865.   rng->tail = s2->range;
  866. }  /* compose */
  867.  
  868.  
  869. /* Local variables for unify: */
  870. struct LOC_unify {
  871.   EXPREC *diff1, *diff2;
  872. } ;
  873.  
  874. Local boolean findExpDiff PP((EXPREC *e1, EXPREC *e2, struct LOC_unify *LINK));
  875.  
  876. /* findELDiff - set diff1, diff2 to EXP's where el1, el2 differ  */
  877. Local boolean findELDiff(el1, el2, LINK)
  878. EXPLISTREC *el1, *el2;
  879. struct LOC_unify *LINK;
  880. {
  881.   boolean foundDiff;
  882.  
  883.   foundDiff = false;
  884.   while (el1 != NULL && !foundDiff) {
  885.     foundDiff = findExpDiff(el1->head, el2->head, LINK);
  886.     el1 = el1->tail;
  887.     el2 = el2->tail;
  888.   }
  889.   return foundDiff;
  890. }  /* findELDiff */
  891.  
  892. /* findExpDiff - set diff1, diff2 to EXP's where e1, e2 differ   */
  893. Local boolean findExpDiff(e1, e2, LINK)
  894. EXPREC *e1, *e2;
  895. struct LOC_unify *LINK;
  896. {
  897.   boolean Result;
  898.  
  899.   Result = true;
  900.   LINK->diff1 = e1;
  901.   LINK->diff2 = e2;
  902.   if (e1->etype != e2->etype)
  903.     return Result;
  904.   switch (e1->etype) {
  905.  
  906.   case VAREXP:
  907.     if (eqVar(e1->UU.varble, e2->UU.varble))
  908.       Result = false;
  909.     break;
  910.  
  911.   case INTEXP:
  912.     if (e1->UU.intval == e2->UU.intval)
  913.       Result = false;
  914.     break;
  915.  
  916.   case APEXP:
  917.     if (e1->UU.U2.optr == e2->UU.U2.optr)
  918.       Result = findELDiff(e1->UU.U2.args, e2->UU.U2.args, LINK);
  919.     break;
  920.   }/* case */
  921.   return Result;
  922. }  /* findExpDiff */
  923.  
  924. /* occursInExp - check whether variable v occurs in exp e        */
  925. Local boolean occursInExp(v, e, LINK)
  926. VARIABLEREC *v;
  927. EXPREC *e;
  928. struct LOC_unify *LINK;
  929. {
  930.   boolean Result, occurs;
  931.   EXPLISTREC *el;
  932.  
  933.   switch (e->etype) {
  934.  
  935.   case INTEXP:
  936.     Result = false;
  937.     break;
  938.  
  939.   case VAREXP:
  940.     Result = eqVar(v, e->UU.varble);
  941.     break;
  942.  
  943.   case APEXP:
  944.     occurs = false;
  945.     el = e->UU.U2.args;
  946.     while (el != NULL && !occurs) {
  947.       occurs = occursInExp(v, el->head, LINK);
  948.       el = el->tail;
  949.     }
  950.     Result = occurs;
  951.     break;
  952.   }/* case and with */
  953.   return Result;
  954. }  /* occursInExp */
  955.  
  956. /* makeSubst - bind d1 to d2 in s, first checking if possible    */
  957. Local Void makeSubst(d1, d2, s, LINK)
  958. EXPREC *d1, *d2;
  959. SUBSTREC **s;
  960. struct LOC_unify *LINK;
  961. {
  962.   if (d1->etype != VAREXP) {
  963.     *s = NULL;
  964.     return;
  965.   }
  966.   if (occursInExp(d1->UU.varble, d2, LINK))
  967.     *s = NULL;
  968.   else
  969.     bindVar(d1->UU.varble, d2, *s);
  970. }  /* makeSubst */
  971.  
  972.  
  973. /*****************************************************************
  974.  *                     UNIFICATION                               *
  975.  *****************************************************************/
  976.  
  977. /* unify - unify g1 and g2; return unifying subst. (or nil)      */
  978.  
  979. Static SUBSTREC *unify(g1, g2)
  980. GOALREC *g1, *g2;
  981. {
  982.   struct LOC_unify V;
  983.   SUBSTREC *sigma, *varsubst;
  984.   boolean foundDiff;
  985.  
  986.   sigma = emptySubst();
  987.   do {
  988.     foundDiff = findELDiff(g1->args, g2->args, &V);
  989.     varsubst = emptySubst();
  990.     if (foundDiff) {
  991.       if (V.diff1->etype == VAREXP)
  992.     makeSubst(V.diff1, V.diff2, &varsubst, &V);
  993.       else
  994.     makeSubst(V.diff2, V.diff1, &varsubst, &V);
  995.     }
  996.     if (foundDiff && varsubst != NULL) {   /* done */
  997.       applyToGoal(varsubst, g1);
  998.       applyToGoal(varsubst, g2);
  999.       compose(sigma, varsubst);
  1000.     }
  1001.   } while (foundDiff && varsubst != NULL);   /* not unifiable */
  1002.   if (varsubst == NULL)
  1003.     return NULL;
  1004.   else
  1005.     return sigma;
  1006. }  /* unify */
  1007.  
  1008.  
  1009. /* Local variables for applyPrim: */
  1010. struct LOC_applyPrim {
  1011.   boolean Result;
  1012.   SUBSTREC **sigma;
  1013.   EXPLISTREC *arglist;
  1014.   EXPREC *arg1, *arg2, *arg3;
  1015. } ;
  1016.  
  1017. Local Void applyArith(op, LINK)
  1018. long op;
  1019. struct LOC_applyPrim *LINK;
  1020. {
  1021.   long i;
  1022.  
  1023.   LINK->arg3 = LINK->arglist->tail->tail->head;
  1024.   if (LINK->arg3->etype == APEXP) {
  1025.     LINK->Result = false;
  1026.     return;
  1027.   }
  1028.   switch (op) {
  1029.  
  1030.   case 1:
  1031.     i = LINK->arg1->UU.intval + LINK->arg2->UU.intval;
  1032.     break;
  1033.  
  1034.   case 2:
  1035.     i = LINK->arg1->UU.intval - LINK->arg2->UU.intval;
  1036.     break;
  1037.   }
  1038.   if (LINK->arg3->etype == INTEXP) {
  1039.     if (LINK->arg3->UU.intval != i)
  1040.       LINK->Result = false;
  1041.   } else
  1042.     bindVar(LINK->arg3->UU.varble, mkINTEXP(i), *LINK->sigma);
  1043.  
  1044.   /* applyPrim already true */
  1045. }  /* applyArith */
  1046.  
  1047.  
  1048. /*****************************************************************
  1049.  *                     EVALUATION                                *
  1050.  *****************************************************************/
  1051.  
  1052. /* applyPrim - apply primitive predicate, modifying sigma        */
  1053. Static boolean applyPrim(g, sigma_)
  1054. GOALREC *g;
  1055. SUBSTREC **sigma_;
  1056. {
  1057.   struct LOC_applyPrim V;
  1058.  
  1059.   V.sigma = sigma_;
  1060.   *V.sigma = emptySubst();
  1061.   V.Result = true;
  1062.   V.arglist = g->args;
  1063.   if (g->pred == 4) {   /* print */
  1064.     prExplist(V.arglist);
  1065.     putchar('\n');
  1066.     return V.Result;
  1067.   }
  1068.   V.arg1 = V.arglist->head;
  1069.   V.arg2 = V.arglist->tail->head;
  1070.   if (V.arg1->etype != INTEXP || V.arg2->etype != INTEXP)
  1071.     return false;
  1072.   switch (g->pred) {
  1073.  
  1074.   case 1:
  1075.   case 2:   /* plus, minus */
  1076.     applyArith((long)g->pred, &V);
  1077.     break;
  1078.  
  1079.   case 3:   /* less */
  1080.     if (V.arg1->UU.intval >= V.arg2->UU.intval)
  1081.       V.Result = false;
  1082.     break;
  1083.   }/* case */
  1084.   return V.Result;
  1085. }  /* applyPrim */
  1086.  
  1087.  
  1088. Static GOALREC *copyGoal PP((GOALREC *g, long id));
  1089.  
  1090.  
  1091. /* copyGoallist - copy gl; rename variables if id<>0             */
  1092. Static GOALLISTREC *copyGoallist(gl, id)
  1093. GOALLISTREC *gl;
  1094. long id;
  1095. {
  1096.   if (gl == NULL)
  1097.     return NULL;
  1098.   else
  1099.     return (mkGoallist(copyGoal(gl->head, id), copyGoallist(gl->tail, id)));
  1100. }  /* copyGoallist */
  1101.  
  1102.  
  1103. /* Local variables for copyGoal: */
  1104. struct LOC_copyGoal {
  1105.   long id;
  1106. } ;
  1107.  
  1108. Local EXPLISTREC *copyExplist PP((EXPLISTREC *el, struct LOC_copyGoal *LINK));
  1109.  
  1110. /* Local variables for copyExplist: */
  1111. struct LOC_copyExplist {
  1112.   struct LOC_copyGoal *LINK;
  1113. } ;
  1114.  
  1115. Local EXPREC *copyExp(e, LINK)
  1116. EXPREC *e;
  1117. struct LOC_copyExplist *LINK;
  1118. {
  1119.   EXPREC *Result;
  1120.  
  1121.   switch (e->etype) {
  1122.  
  1123.   case INTEXP:
  1124.     Result = e;
  1125.     break;
  1126.  
  1127.   case VAREXP:
  1128.     if (LINK->LINK->id == 0)
  1129.       Result = mkVAREXP(mkVariable(e->UU.varble->varname,
  1130.                    e->UU.varble->varindex));
  1131.     else
  1132.       Result = mkVAREXP(mkVariable(e->UU.varble->varname, LINK->LINK->id));
  1133.     break;
  1134.  
  1135.   case APEXP:
  1136.     Result = mkAPEXP(e->UU.U2.optr, copyExplist(e->UU.U2.args, LINK->LINK));
  1137.     break;
  1138.   }/* case */
  1139.   return Result;
  1140. }  /* copyExp */
  1141.  
  1142. Local EXPLISTREC *copyExplist(el, LINK)
  1143. EXPLISTREC *el;
  1144. struct LOC_copyGoal *LINK;
  1145. {
  1146.  
  1147.   /* copyExp - copy e; rename variables if id<>0                   */
  1148.   struct LOC_copyExplist V;
  1149.  
  1150.   V.LINK = LINK;
  1151.   if (el == NULL)
  1152.     return NULL;
  1153.   else
  1154.     return (mkExplist(copyExp(el->head, &V), copyExplist(el->tail, LINK)));
  1155. }  /* copyExplist */
  1156.  
  1157.  
  1158. /* copyGoal - copy g; rename variables if id<>0                  */
  1159. Static GOALREC *copyGoal(g, id_)
  1160. GOALREC *g;
  1161. long id_;
  1162. {
  1163.  
  1164.   /* copyExplist - copy el; rename variables if id<>0              */
  1165.   struct LOC_copyGoal V;
  1166.  
  1167.   V.id = id_;
  1168.   return (mkGoal(g->pred, copyExplist(g->args, &V)));
  1169. }  /* copyGoal */
  1170.  
  1171.  
  1172. /* append - append second to end of first, modifying first       */
  1173. Static GOALLISTREC *append(first, second)
  1174. GOALLISTREC *first, *second;
  1175. {
  1176.   GOALLISTREC *Result;
  1177.  
  1178.   if (first == NULL)
  1179.     return second;
  1180.   Result = first;
  1181.   while (first->tail != NULL)
  1182.     first = first->tail;
  1183.   first->tail = second;
  1184.   return Result;
  1185. }  /* append */
  1186.  
  1187.  
  1188. Static SUBSTREC *prove PP((GOALLISTREC *gl, long id));
  1189.  
  1190. /* Local variables for prove: */
  1191. struct LOC_prove {
  1192.   long id;
  1193.   SUBSTREC *sigma0;
  1194. } ;
  1195.  
  1196. /* tryClause - try to match goal g and clause head of c          */
  1197. Local SUBSTREC *tryClause(clgoal, g, LINK)
  1198. GOALREC *clgoal, *g;
  1199. struct LOC_prove *LINK;
  1200. {
  1201.   SUBSTREC *Result;
  1202.  
  1203.   Result = NULL;
  1204.   if (!((clgoal->pred == g->pred) & (lengthEL(clgoal->args) == lengthEL(g->args))))
  1205.     return Result;
  1206.   clgoal = copyGoal(clgoal, LINK->id);
  1207.   g = copyGoal(g, 0L);
  1208.   return (unify(clgoal, g));
  1209. /* p2c: prolog.p: Note: Deleting unreachable code [255] */
  1210. }  /* tryClause */
  1211.  
  1212. /* proveRest - add subgoals to restofgoals and prove             */
  1213. Local SUBSTREC *proveRest(subgoals, restofgoals, LINK)
  1214. GOALLISTREC *subgoals, *restofgoals;
  1215. struct LOC_prove *LINK;
  1216. {
  1217.   subgoals = copyGoallist(subgoals, LINK->id);
  1218.   applyToGoallist(LINK->sigma0, subgoals);
  1219.   restofgoals = copyGoallist(restofgoals, 0L);
  1220.   applyToGoallist(LINK->sigma0, restofgoals);
  1221.   return (prove(append(subgoals, restofgoals), LINK->id + 1));
  1222. }  /* proveRest */
  1223.  
  1224.  
  1225. /* prove - prove goals gl; return subst; id used to rename var's */
  1226. Static SUBSTREC *prove(gl, id_)
  1227. GOALLISTREC *gl;
  1228. long id_;
  1229. {
  1230.   struct LOC_prove V;
  1231.   CLAUSEREC *cl;
  1232.   SUBSTREC *sigma1;
  1233.  
  1234.   V.id = id_;
  1235.   if (gl == NULL)
  1236.     return (emptySubst());
  1237.   else {
  1238.     if (gl->head->pred <= numBuiltins) {
  1239.       if (applyPrim(gl->head, &V.sigma0)) {
  1240.     applyToGoallist(V.sigma0, gl->tail);
  1241.     sigma1 = prove(gl->tail, V.id + 1);
  1242.       } else
  1243.     sigma1 = NULL;
  1244.     } else {
  1245.       sigma1 = NULL;
  1246.       cl = clauses;
  1247.       while (cl != NULL && sigma1 == NULL) {
  1248.     V.sigma0 = tryClause(cl->lhs, gl->head, &V);
  1249.     if (V.sigma0 != NULL)
  1250.       sigma1 = proveRest(cl->rhs, gl->tail, &V);
  1251.     cl = cl->nextclause;
  1252.       }  /* while */
  1253.     }
  1254.     if (sigma1 == NULL)
  1255.       return NULL;
  1256.     else {
  1257.       compose(V.sigma0, sigma1);
  1258.       return V.sigma0;
  1259.     }
  1260.   }
  1261. }  /* prove */
  1262.  
  1263.  
  1264. /*****************************************************************
  1265.  *                     READ-EVAL-PRINT LOOP                      *
  1266.  *****************************************************************/
  1267.  
  1268. main(argc, argv)
  1269. int argc;
  1270. Char *argv[];
  1271. {  /* prolog main */
  1272.   PASCAL_MAIN(argc, argv);
  1273.   if (setjmp(_JL99))
  1274.     goto _L99;
  1275.   initNames();
  1276.  
  1277.   quittingtime = false;
  1278. _L99:
  1279.   while (!quittingtime) {
  1280.     reader();
  1281.     if (matches((long)pos_, 4, "quit                ")) {
  1282.       quittingtime = true;
  1283.       break;
  1284.     }
  1285.     if (matches(skipblanks(pos_ + 1L), 5, "infer               ")) {
  1286.       parseClause();
  1287.       putchar('\n');
  1288.     } else {
  1289.       toplevelGoal = parseQuery();
  1290.       putchar('\n');
  1291.       if (prove(toplevelGoal, 1L) == NULL)
  1292.     printf("Not satisfied\n");
  1293.       else
  1294.     printf("Satisfied\n");
  1295.       putchar('\n');
  1296.     }
  1297.   }
  1298.   exit(0);
  1299. }  /* prolog */
  1300.  
  1301.  
  1302.  
  1303. /* End. */
  1304.