home *** CD-ROM | disk | FTP | other *** search
/ OS/2 Shareware BBS: 10 Tools / 10-Tools.zip / lifeos2.zip / LIFE-1.02 / SOURCE / LOGIN.C < prev    next >
C/C++ Source or Header  |  1996-06-16  |  66KB  |  2,541 lines
  1. /* Copyright 1991 Digital Equipment Corporation.
  2.  ** All Rights Reserved.
  3.  *****************************************************************/
  4. /*     $Id: login.c,v 1.4 1995/01/14 00:25:33 duchier Exp $     */
  5.  
  6. #ifndef lint
  7. static char vcid[] = "$Id: login.c,v 1.4 1995/01/14 00:25:33 duchier Exp $";
  8. #endif /* lint */
  9.  
  10. #include "extern.h"
  11. #include "login.h"
  12. #include "trees.h"
  13. #include "copy.h"
  14. #include "parser.h"
  15. #include "token.h"
  16. #include "print.h"
  17. #ifndef OS2_PORT
  18. #include "built_ins.h"
  19. #else
  20. #include "built_in.h"
  21. #endif
  22. #include "types.h"
  23. #include "lefun.h"
  24. #include "memory.h"
  25. #include "error.h"
  26. #include "xpred.h"
  27. #include "modules.h" /*  RM: Jan 27 1993  */
  28. #ifndef OS2_PORT
  29. #include "interrupt.h"
  30. #else
  31. #include "interrup.h"
  32. #endif
  33.  
  34. int global_unify_attr();   /*  RM: Feb  9 1993  */
  35. int global_unify();        /*  RM: Feb 11 1993  */
  36.  
  37. /* Clean trail toggle */
  38. /* Removed temporarily because of comb bug 1.6 */
  39. #define CLEAN_TRAIL
  40.  
  41. /* Statistics on trail cleaning */
  42. long clean_iter=0;
  43. long clean_succ=0;
  44.  
  45. ptr_stack undo_stack;
  46. ptr_choice_point choice_stack;
  47. /* ptr_choice_point prompt_choice_stack; 12.7 */
  48. #ifdef TS
  49. /* Should never wrap (32 bit is enough) 9.6 */
  50. /* Rate of incrementing: One per choice point */
  51. unsigned long global_time_stamp=INIT_TIME_STAMP; /* 9.6 */
  52. #endif
  53.  
  54. ptr_goal goal_stack,aim;
  55.  
  56.  
  57. long goal_count;
  58. #ifndef OS2_PORT
  59. struct tms start_time,end_time;
  60. #else
  61. float start_time,end_time;
  62. #endif
  63. long ignore_eff; /* 'Ignore efficiency' flag */
  64.  
  65. long assert_first;
  66. long assert_ok;
  67.  
  68. long main_loop_ok;
  69. long xeventdelay;
  70. long xcount;
  71.  
  72. long more_u_attr; /* TRUE if U has attributes V doesn't */
  73. long more_v_attr; /* Vice-versa */
  74.  
  75. long u_func,v_func;  /* TRUE if U or V is a curried function */
  76. long new_stat;
  77.  
  78. char prompt_buffer[PROMPT_BUFFER];
  79.  
  80.  
  81. /******************************************************************************
  82.   
  83.   What follows are the functions which assert facts in their correct places:
  84.   function definitions, rule definitions or type definitions.
  85.   
  86.   ****************************************************************************/
  87.  
  88.  
  89.  
  90. /******** GET_TWO_ARGS(attr_list,arg1,arg2)
  91.   Get the arguments labelled '1' and '2' as quickly as possible from the
  92.   binary tree ATTR_LIST, place them in ARG1 and ARG2. This routine nearly
  93.   always makes a direct hit.
  94.   */
  95. void get_two_args(t,a,b)
  96.      ptr_node t;
  97.      ptr_psi_term *a;
  98.      ptr_psi_term *b;
  99. {
  100.   ptr_node n;
  101.   
  102.   *a=NULL;
  103.   *b=NULL;
  104.   if (t) {
  105.     if (t->key==one) {
  106.       *a=(ptr_psi_term )t->data;
  107.       n=t->right;
  108.       if (n) 
  109.     if (n->key==two)
  110.       *b=(ptr_psi_term )n->data;
  111.     else {
  112.       n=find(featcmp,two,t);
  113.       if(n==NULL)
  114.         *b=NULL;
  115.       else
  116.         *b=(ptr_psi_term )n->data;
  117.     }
  118.       else
  119.     *b=NULL;
  120.     }
  121.     else {
  122.       n=find(featcmp,one,t);
  123.       if (n==NULL)
  124.     *a=NULL;
  125.       else
  126.     *a=(ptr_psi_term )n->data;
  127.       n=find(featcmp,two,t);
  128.       if (n==NULL)
  129.     *b=NULL;
  130.       else
  131.     *b=(ptr_psi_term )n->data;
  132.     }
  133.   }
  134. }
  135.  
  136.  
  137.  
  138.  
  139. /******** GET_ONE_ARG(attr_list,arg1)
  140.   Get the argument labelled '1' as quickly as possible from the
  141.   binary tree ATTR_LIST, place it in ARG1. This routine nearly
  142.   always makes a direct hit.
  143.   */
  144. void get_one_arg(t,a)
  145.      ptr_node t;
  146.      ptr_psi_term *a;
  147. {
  148.   ptr_node n;
  149.   
  150.   *a=NULL;
  151.   if (t) {
  152.     if (t->key==one) {
  153.       *a=(ptr_psi_term)t->data;
  154.     }
  155.     else {
  156.       n=find(featcmp,one,t);
  157.       if (n==NULL)
  158.     *a=NULL;
  159.       else
  160.     *a=(ptr_psi_term)n->data;
  161.     }
  162.   }
  163. }
  164.  
  165.  
  166.  
  167.  
  168. /******** GET_ONE_ARG_ADDR(attr_list,arg1addr)
  169.   Get address of slot in the attr_list that points to the argument labelled
  170.   '1' as quickly as possible from the binary tree ATTR_LIST.
  171.   This routine nearly always makes a direct hit.
  172.   */
  173. void get_one_arg_addr(t,a)
  174.      ptr_node t;
  175.      ptr_psi_term **a;
  176. {
  177.   ptr_node n;
  178.   ptr_psi_term *b;
  179.   
  180.   *a=NULL;
  181.   if (t) {
  182.     if (t->key==one)
  183.       *a= (ptr_psi_term *)(&t->data);
  184.     else {
  185.       n=find(featcmp,one,t);
  186.       if (n==NULL)
  187.     *a=NULL;
  188.       else
  189.     *a= (ptr_psi_term *)(&n->data);
  190.     }
  191.   }
  192. }
  193.  
  194.  
  195.  
  196.  
  197. /******** ADD_RULE(head,body,typ)
  198.   The TYP argument is either 'predicate', 'function', or 'type'.
  199.   For predicates or functions, insert the clause 'HEAD :- BODY' or the rule
  200.   'HEAD -> BODY' into the definition of HEAD.
  201.   For types, insert HEAD as a term of type attributes and BODY as a type
  202.   constraint.
  203.   The global flag ASSERT_FIRST indicates whether to do the insertion at the
  204.   head or the tail of the existing list.
  205.   */
  206. void add_rule(head,body,typ)
  207.      ptr_psi_term head;
  208.      ptr_psi_term body;
  209.      def_type typ;
  210. {
  211.   psi_term succ;
  212.   ptr_psi_term head2;
  213.   ptr_definition def;
  214.   ptr_pair_list p, *p2;
  215.   
  216.   if (!body && typ==predicate) {
  217.     succ.type=succeed;
  218.     succ.value=NULL;
  219.     succ.coref=NULL;
  220.     succ.resid=NULL;
  221.     succ.attr_list=NULL;
  222.     body= ≻
  223.   }
  224.   
  225.   deref_ptr(head);
  226.   head2=head;
  227.   
  228.   /* assert(head->resid==NULL); 10.8 */
  229.   /* assert(body->resid==NULL); 10.8 */
  230.   
  231.   if (redefine(head)) {
  232.     
  233.     def=head->type;
  234.     
  235.     if (def->type==undef || def->type==typ)
  236.       
  237.       /*  RM: Jan 27 1993  */
  238.       if(TRUE
  239.      /* def->type==undef ||
  240.         def->keyword->module==current_module */
  241.      /*  RM: Feb  2 1993  Commented out */
  242.      ) {
  243.     if (def->rule && (unsigned long)def->rule<=MAX_BUILT_INS) {
  244.       Errorline("the built-in %T '%s' may not be redefined.\n",
  245.             def->type, def->keyword->symbol);
  246.     }
  247.     else {
  248.       def->type=typ;
  249.       
  250.       /* PVR single allocation in source */
  251.       p=HEAP_ALLOC(pair_list);
  252.       clear_copy();
  253.       /* p->a=exact_copy(head2,HEAP); 24.8 25.8 */
  254.       /* p->b=exact_copy(body,HEAP); 24.8 25.8 */
  255.       
  256.       p->a=quote_copy(head2,HEAP); /* 24.8 25.8 */
  257.       p->b=quote_copy(body,HEAP); /* 24.8 25.8 */
  258.       
  259.       if (assert_first) {
  260.         p->next=def->rule;
  261.         def->rule=p;
  262.       }
  263.       else {
  264.         p->next=NULL;
  265.         p2= &(def->rule);
  266.         while (*p2) {
  267.           p2= &((*p2)->next);
  268.         }
  269.         *p2=p;
  270.       }
  271.       assert_ok=TRUE;
  272.     }
  273.       }
  274.       else { /*  RM: Jan 27 1993  */
  275.     Errorline("the %T '%s' may not be redefined from within module %s.\n",
  276.           def->type,
  277.           def->keyword->combined_name,
  278.           current_module->module_name);
  279.       }
  280.     else {
  281.       Errorline("the %T '%s' may not be redefined as a %T.\n",
  282.                 def->type, def->keyword->symbol, typ);
  283.     }
  284.   }
  285. }
  286.  
  287.  
  288.  
  289. /******** ASSERT_RULE(t,typ)
  290.   Add a rule to the rule tree.
  291.   It may be either a predicate or a function.
  292.   The psi_term T is of the form 'H :- B' or 'H -> B', but it may be incorrect
  293.   (report errors). TYP is the type, function or predicate.
  294.   */
  295. void assert_rule(t,typ)
  296.      psi_term t;
  297.      def_type typ;
  298. {
  299.   ptr_psi_term head;
  300.   ptr_psi_term body;
  301.   
  302.   get_two_args(t.attr_list,&head,&body);
  303.   if (head)
  304.     if (body)
  305.       add_rule(head,body,typ);
  306.     else {
  307.       Syntaxerrorline("body missing in definition of %T '%P'.\n", typ, head);
  308.     }
  309.   else {
  310.     Syntaxerrorline("head missing in definition of %T.\n",typ);
  311.   }
  312. }
  313.  
  314.  
  315.  
  316. /******** ASSERT_CLAUSE(t)
  317.   Assert the clause T.
  318.   Cope with various syntaxes for predicates.
  319.   
  320.   ASSERT_FIRST is a flag indicating the position:
  321.   1= insert before existing rules (asserta),
  322.   0= insert after existing rules (assert),
  323.   */
  324.  
  325. void assert_clause(t)
  326.      ptr_psi_term t;
  327. {
  328.   ptr_psi_term arg1,arg2;
  329.   char *str;
  330.   
  331.   assert_ok=FALSE;  
  332.   deref_ptr(t);
  333.   
  334.   /*  RM: Feb 22 1993  defined c_alias in modules.c
  335.       if (equ_tok((*t),"alias")) {
  336.       get_two_args(t->attr_list,&arg1,&arg2);
  337.       if (arg1 && arg2) {
  338.       Warningline("'%s' has taken the meaning of '%s'.\n",
  339.       arg2->type->keyword->symbol, arg1->type->keyword->symbol);
  340.       str=arg2->type->keyword->symbol;
  341.       assert_ok=TRUE;
  342.       deref_ptr(arg1);
  343.       deref_ptr(arg2);
  344.       *(arg2->type)= *(arg1->type);
  345.       arg2->type->keyword->symbol=str;
  346.       }
  347.       else
  348.       Errorline("arguments missing in %P.\n",t);
  349.       }
  350.       else
  351.       */
  352.   
  353.   if (equ_tok((*t),":-"))
  354.     assert_rule((*t),predicate);
  355.   else
  356.     if (equ_tok((*t),"->"))
  357.       assert_rule((*t),function);
  358.     else
  359.       if (equ_tok((*t),"::"))
  360.     assert_attributes(t);
  361.       else
  362.     
  363. #ifdef CLIFE
  364.     if (equ_tok((*t),"block_struct"))
  365.       define_block(t);
  366.     else
  367. #endif /* CLIFE */
  368.       /* if (equ_tok((*t),"<<<-")) {   RM: Feb 10 1993
  369.          declare T as global. To do... maybe.
  370.          }
  371.          else
  372.          */
  373.       
  374.       if (equ_tok((*t),"<|") || equ_tok((*t),":="))
  375.         assert_complicated_type(t);
  376.       else
  377.         add_rule(t,NULL,predicate);
  378.   
  379.   /* if (!assert_ok && warning()) perr("the declaration is ignored.\n"); */
  380. }
  381.  
  382.  
  383.  
  384. /******** START_CHRONO()
  385.   This initialises the CPU time counter.
  386.   */
  387.  
  388. void start_chrono()
  389. {
  390.   times(&start_time);
  391. }
  392.  
  393.  
  394.  
  395. /******************************************************************************
  396.   
  397.   PROOF and UNIFICATION routines.
  398.   
  399.   These two different functions are written without using explicit recursion
  400.   so that backtracking can easily take place between the two. PROVE can call
  401.   UNIFY and vice-versa.
  402.   
  403.   The argument to PROVE is the adress of a PSI_TERM (psi-term) which represents
  404.   a goal to prove.
  405.   
  406.   Prove then passes that on the goal stack to MAIN_PROVE() which does
  407.   the real work, involving calls to UNIFY_AIM, PROVE_AIM and backtracking.
  408.   
  409.   ****************************************************************************/
  410.  
  411.  
  412.  
  413. /******* PUSH_PTR_VALUE(p)
  414.   Push the pair (P,*P) onto the stack of things to be undone (trail).
  415.   It needn't be done if P is greater than the latest choice point because in
  416.   that case memory is reclaimed.
  417.   */
  418. void push_ptr_value(t,p)
  419.      type_ptr t;
  420.      GENERIC *p;
  421. {
  422.   ptr_stack n;
  423.   
  424.   assert((GENERIC)p<heap_pointer); /*  RM: Feb 15 1993  */
  425.   
  426.   assert(VALID_ADDRESS(p));
  427.   if (p < (GENERIC *)choice_stack || p > (GENERIC *)stack_pointer) 
  428.     {
  429.       n=STACK_ALLOC(stack);
  430.       n->type=t;
  431.       n->a= (GENERIC)p;
  432.       n->b= *p;
  433.       n->next=undo_stack;
  434.       undo_stack=n;
  435.     }
  436. }
  437.  
  438.  
  439. /******** PUSH_DEF_PTR_VALUE(q,p) (9.6)
  440.   Same as push_ptr_value, but only for psi-terms whose definition field is
  441.   being modified.  (If another field is modified, use push_ptr_value.)
  442.   This routine implements the time-stamp technique of only trailing
  443.   once between choice point creations, even on multiple bindings.
  444.   q is address of psi-term, p is address of field inside psi-term
  445.   that is modified.  Both the definition and the time_stamp must be trailed.
  446.   */
  447. void push_def_ptr_value(q,p)
  448.      ptr_psi_term q;
  449.      GENERIC *p;
  450. {
  451.   ptr_stack m,n;
  452.   
  453.   assert(VALID_ADDRESS(q));
  454.   assert(VALID_ADDRESS(p));
  455. #ifdef TS
  456.   if (TRAIL_CONDITION(q) &&
  457.       /* (q->time_stamp != global_time_stamp) && */
  458.       (p < (GENERIC *)choice_stack || p > (GENERIC *)stack_pointer))
  459.     {
  460. #define TRAIL_TS
  461. #ifdef TRAIL_TS
  462.       
  463.       assert((GENERIC)q<heap_pointer); /*  RM: Feb 15 1993  */
  464.       
  465.       m=STACK_ALLOC(stack); /* Trail time_stamp */
  466.       m->type=int_ptr;
  467.       m->a= (GENERIC) &(q->time_stamp);
  468.       m->b= (GENERIC) (q->time_stamp);
  469.       m->next=undo_stack;
  470.       n=STACK_ALLOC(stack); /* Trail definition field (top of undo_stack) */
  471.       n->type=def_ptr;
  472.       n->a= (GENERIC)p;
  473.       n->b= *p;
  474.       n->next=m;
  475.       undo_stack=n;
  476. #else
  477.       n=STACK_ALLOC(stack); /* Trail definition field (top of undo_stack) */
  478.       n->type=def_ptr;
  479.       n->a= (GENERIC)p;
  480.       n->b= *p;
  481.       n->next=undo_stack;
  482.       undo_stack=n;
  483. #endif
  484.       q->time_stamp=global_time_stamp;
  485.     }
  486. #else
  487.   push_ptr_value(def_ptr,p);
  488. #endif
  489. }
  490.  
  491.  
  492.  
  493. /******** PUSH_PSI_PTR_VALUE(q,p) (9.6)
  494.   Same as push_ptr_value, but only for psi-terms whose coref field is being
  495.   modified.  (If another field is modified, use push_ptr_value.)
  496.   This routine implements the time-stamp technique of only trailing
  497.   once between choice point creations, even on multiple bindings.
  498.   q is address of psi-term, p is address of field inside psi-term
  499.   that is modified.  Both the coref and the time_stamp must be trailed.
  500.   */
  501. void push_psi_ptr_value(q,p)
  502.      ptr_psi_term q;
  503.      GENERIC *p;
  504. {
  505.   ptr_stack m,n;
  506.   
  507.   assert(VALID_ADDRESS(q));
  508.   assert(VALID_ADDRESS(p));
  509. #ifdef TS
  510.   if (TRAIL_CONDITION(q) &&
  511.       /* (q->time_stamp != global_time_stamp) && */
  512.       (p < (GENERIC *)choice_stack || p > (GENERIC *)stack_pointer))
  513.     {
  514. #define TRAIL_TS
  515. #ifdef TRAIL_TS
  516.       m=STACK_ALLOC(stack); /* Trail time_stamp */
  517.       m->type=int_ptr;
  518.       m->a= (GENERIC) &(q->time_stamp);
  519.       m->b= (GENERIC) (q->time_stamp);
  520.       m->next=undo_stack;
  521.       n=STACK_ALLOC(stack); /* Trail coref field (top of undo_stack) */
  522.       n->type=psi_term_ptr;
  523.       n->a= (GENERIC)p;
  524.       n->b= *p;
  525.       n->next=m;
  526.       undo_stack=n;
  527. #else
  528.       n=STACK_ALLOC(stack); /* Trail coref field (top of undo_stack) */
  529.       n->type=psi_term_ptr;
  530.       n->a= (GENERIC)p;
  531.       n->b= *p;
  532.       n->next=undo_stack;
  533.       undo_stack=n;
  534. #endif
  535.       q->time_stamp=global_time_stamp;
  536.     }
  537. #else
  538.   push_ptr_value(psi_term_ptr,p);
  539. #endif
  540. }
  541.  
  542.  
  543. /* Same as push_ptr_value, but for objects that must always be trailed. */
  544. /* This includes objects outside of the Life data space and entries in  */
  545. /* the var_tree. */
  546. void push_ptr_value_global(t,p)
  547.      type_ptr t;
  548.      GENERIC *p;
  549. {
  550.   ptr_stack n;
  551.   
  552.   assert(VALID_ADDRESS(p)); /* 17.8 */
  553.   n=STACK_ALLOC(stack);
  554.   n->type=t;
  555.   n->a= (GENERIC)p;
  556.   n->b= *p;
  557.   n->next=undo_stack;
  558.   undo_stack=n;
  559. }
  560.  
  561.  
  562.  
  563. /******* PUSH_WINDOW(type,disp,wind)
  564.   Push the window information (operation, display and window identifiers) on
  565.   the undo_stack (trail) so that the window can be destroyed, redrawn, or
  566.   hidden on backtracking.
  567.   */
  568. void push_window(type,disp,wind)
  569.      long type,disp,wind;
  570. {
  571.   ptr_stack n;
  572.   
  573.   assert(type & undo_action);
  574.   n=STACK_ALLOC(stack);
  575.   n->type=type;
  576.   n->a=(GENERIC)disp;
  577.   n->b=(GENERIC)wind;
  578.   n->next=undo_stack;
  579.   undo_stack=n;
  580. }
  581.  
  582.  
  583.  
  584. /******* PUSH2_PTR_VALUE(p)
  585.   Push the pair (P,V) onto the stack of things to be undone (trail).
  586.   It needn't be done if P is greater than the latest choice point because in
  587.   that case memory is reclaimed.
  588.   */
  589. void push2_ptr_value(t,p,v)
  590.      type_ptr t;
  591.      GENERIC *p;
  592.      GENERIC v;
  593. {
  594.   ptr_stack n;
  595.   
  596.   if (p<(GENERIC *)choice_stack || p>(GENERIC *)stack_pointer) {
  597.     n=STACK_ALLOC(stack);
  598.     n->type=t;
  599.     n->a= (GENERIC)p;
  600.     n->b= (GENERIC)v;
  601.     n->next=undo_stack;
  602.     undo_stack=n;
  603.   }
  604. }
  605.  
  606.  
  607.  
  608. /******** PUSH_GOAL(t,a,b,c)
  609.   Push a goal onto the goal stack.
  610.   T is the type of the goal, A,B and C are various parameters.
  611.   See PUSH_CHOICE_POINT(t,a,b,c).
  612.   */
  613. void push_goal(t,a,b,c)
  614.      goals t;
  615.      ptr_psi_term  a;
  616.      ptr_psi_term  b;
  617.      GENERIC c;
  618. {
  619.   ptr_goal thegoal;
  620.   
  621.   thegoal=STACK_ALLOC(goal);
  622.   
  623.   thegoal->type=t;
  624.   thegoal->a=a;
  625.   thegoal->b=b;
  626.   thegoal->c=c;
  627.   thegoal->next=goal_stack;
  628.   thegoal->pending=FALSE;
  629.   
  630.   goal_stack=thegoal;
  631. }
  632.  
  633.  
  634.  
  635. /******** PUSH_CHOICE_POINT(t,a,b,c)
  636.   T,A,B,C is an alternative goal to try.
  637.   T is the type of the goal: unify or prove.
  638.   
  639.   If T=prove then
  640.   a=goal to prove
  641.   b=definition to use
  642.   if b=DEFRULES then that means it's a first call.
  643.   
  644.   If T=unify then
  645.   a and b are the terms to unify.
  646.   
  647.   etc...
  648.   */
  649. void push_choice_point(t,a,b,c)
  650.      goals t;
  651.      ptr_psi_term a;
  652.      ptr_psi_term b;
  653.      GENERIC c;
  654. {
  655.   ptr_goal alternative;
  656.   ptr_choice_point choice;
  657.   GENERIC top;
  658.   
  659.   alternative=STACK_ALLOC(goal);
  660.   
  661.   alternative->type=t;
  662.   alternative->a=a;
  663.   alternative->b=b;
  664.   alternative->c=c;
  665.   alternative->next=goal_stack;
  666.   alternative->pending=FALSE;
  667.   
  668.   top=stack_pointer;
  669.   
  670.   choice=STACK_ALLOC(choice_point);
  671.   
  672.   choice->undo_point=undo_stack;
  673.   choice->goal_stack=alternative;
  674.   choice->next=choice_stack;
  675.   choice->stack_top=top;
  676.   
  677. #ifdef TS
  678.   choice->time_stamp=global_time_stamp; /* 9.6 */
  679.   global_time_stamp++; /* 9.6 */
  680. #endif
  681.   
  682.   choice_stack=choice;  
  683. }
  684.  
  685.  
  686. #define RESTORE_TIME_STAMP global_time_stamp=\
  687. choice_stack?choice_stack->time_stamp:INIT_TIME_STAMP;
  688.  
  689.  
  690.  
  691. /******** UNDO(limit)
  692.   Undoes any side-effects up to LIMIT. Limit being the adress of the stack of
  693.   side-effects you wish to return to.
  694.   
  695.   Possible improvement:
  696.   LIMIT is a useless parameter because GOAL_STACK is equivalent if one takes
  697.   care when stacking UNDO actions. Namely, anything to be undone must be
  698.   stacked LATER (=after) the goal which caused these things to be done, so that
  699.   when the goal fails, everything done after it can be undone and the memory
  700.   used can be reclaimed.
  701.   This routine could be modified in order to cope with goals to be proved
  702.   on backtracking: undo(goal).
  703.   */
  704. void undo(limit)
  705.      ptr_stack limit;
  706. {
  707.   /*
  708.     while((unsigned long)undo_stack>(unsigned long)goal_stack)
  709.     */
  710.   
  711.   while ((unsigned long)undo_stack>(unsigned long)limit) { 
  712. #ifdef X11
  713.     if (undo_stack->type & undo_action) {
  714.       /* Window operation on backtracking */
  715.       switch(undo_stack->type) { /*** RM 8/12/92 ***/
  716.       case destroy_window:
  717.         x_destroy_window((unsigned long)undo_stack->a,(unsigned long)undo_stack->b);
  718.     break;
  719.       case show_window:
  720.         x_show_window((unsigned long)undo_stack->a,(unsigned long)undo_stack->b);
  721.     break;
  722.       case hide_window:
  723.         x_hide_window((unsigned long)undo_stack->a,(unsigned long)undo_stack->b);
  724.     break;
  725.       case show_subwindow:
  726.         x_show_subwindow((unsigned long)undo_stack->a,(unsigned long)undo_stack->b);
  727.     break;
  728.       case hide_subwindow:
  729.         x_hide_subwindow((unsigned long)undo_stack->a,(unsigned long)undo_stack->b);
  730.     break;
  731.       }
  732.     }
  733.     else
  734. #endif
  735.       /* Restoring variable value on backtracking */
  736.       *((GENERIC *)(undo_stack->a))=undo_stack->b;
  737.     undo_stack=undo_stack->next;
  738.   }
  739. }
  740.  
  741.  
  742.  
  743. /******** UNDO_ACTIONS()
  744.   A subset of undo(limit) (the detrailing routine) that does all undo
  745.   actions on the undo_stack, but does not undo any variable bindings,
  746.   nor does it change the value of undo_stack.
  747.   */
  748. void undo_actions()
  749. {
  750.   ptr_stack u=undo_stack;
  751.   
  752.   Errorline("undo_actions should not be called.\n");
  753.   undo(NULL); /* 8.10 */
  754.   return;
  755.   /*
  756.     #ifdef X11
  757.     while ((unsigned long)u) {
  758.     if (u->type & undo_action) {
  759.     if (u->type==destroy_window) {
  760.     x_destroy_window((unsigned long)u->a,(unsigned long)u->b);
  761.     }
  762.     else if (u->type==show_window) {
  763.     x_show_window((unsigned long)u->a,(unsigned long)u->b);
  764.     }
  765.     else if (u->type==hide_window) {
  766.     x_hide_window((unsigned long)u->a,(unsigned long)u->b);
  767.     }
  768.     }
  769.     u=u->next;
  770.     }
  771.     #endif
  772.     */
  773. }
  774.  
  775.  
  776.  
  777. /******** BACKTRACK()
  778.   Undo everything back to the previous choice-point and take the alternative
  779.   decision. This routine would have to be modified, along with UNDO to cope
  780.   with goals to be proved on backtracking.
  781.   */
  782. void backtrack()
  783. {
  784.   long gts;
  785.   
  786.   goal_stack=choice_stack->goal_stack;
  787.   undo(choice_stack->undo_point);
  788. #ifdef TS
  789.   /* global_time_stamp=choice_stack->time_stamp; */ /* 9.6 */
  790. #endif
  791.   stack_pointer=choice_stack->stack_top;
  792.   choice_stack=choice_stack->next;
  793.   resid_aim=NULL;
  794.   
  795.   
  796.   /* assert((unsigned long)stack_pointer>=(unsigned long)cut_point); 13.6 */
  797.   /* This situation occurs frequently in some benchmarks (e.g comb) */
  798.   /* printf("*** Possible GC error: cut_point is dangling\n"); */
  799.   /* fflush(stdout); */
  800.   
  801.   /* assert((unsigned long)stack_pointer>=(unsigned long)match_date); 13.6 */
  802. }
  803.  
  804.  
  805.  
  806. /******** CLEAN_TRAIL(cutpt)
  807.   This routine removes all trail entries between the top of the undo_stack
  808.   and the cutpt, whose addresses are between the cutpt and stack_pointer.
  809.   (The cutpt is the choice point that will become the most recent
  810.   one after the cut.)
  811.   This routine should be called when a cut built-in is done.
  812.   This routine is careful not to remove any trailed entries that are
  813.   on the heap or outside of Life space.
  814.   */
  815. static void clean_trail(cutpt)
  816.      ptr_choice_point cutpt;
  817. {
  818.   ptr_stack *prev,u,cut_limit;
  819.   GENERIC cut_sp;
  820.   
  821.   u = undo_stack;
  822.   prev = &undo_stack;
  823.   if (cutpt) {
  824.     cut_sp = cutpt->stack_top;
  825.     cut_limit = cutpt->undo_point;
  826.   }
  827.   else {
  828.     cut_sp = mem_base; /* Empty stack */
  829.     cut_limit = NULL;  /* Empty undo_stack */
  830.   }
  831.   
  832.   while ((unsigned long)u > (unsigned long)cut_limit) {
  833.     clean_iter++;
  834.     if (!(u->type & undo_action) && VALID_RANGE(u->a) &&
  835.         (unsigned long)u->a>(unsigned long)cut_sp && (unsigned long)u->a<=(unsigned long)stack_pointer) {
  836.       *prev = u->next;
  837.       clean_succ++;
  838.     }
  839.     prev = &(u->next);
  840.     u = u->next;
  841.   }
  842. }
  843.  
  844.  
  845.  
  846. /******* CLEAN_UNDO_WINDOW(disp,wind)
  847.   Remove all trail entries that reference a given window.
  848.   This is called when the window is destroyed.
  849.   */
  850. void clean_undo_window(disp,wind)
  851.      long disp,wind;
  852. {
  853.   ptr_stack *prev,u;
  854.   ptr_choice_point c;
  855.   
  856. #ifdef X11
  857.   /* Remove entries on the trail */
  858.   u = undo_stack;
  859.   prev = &undo_stack;
  860.   while (u) {
  861.     if ((u->type & undo_action) &&
  862.         ((unsigned long)u->a==disp) && ((unsigned long)u->b==wind)) {
  863.       *prev = u->next;
  864.     }
  865.     prev = &(u->next);
  866.     u = u->next;
  867.   }
  868.   
  869.   /* Remove entries at the *tops* of trail entry points from the   */
  870.   /* choice point stack.  It's only necessary to look at the tops, */
  871.   /* since those are the only ones that haven't been touched by    */
  872.   /* the previous while loop. */
  873.   c = choice_stack;
  874.   while (c) {
  875.     u = c->undo_point;
  876.     prev = &(c->undo_point);
  877.     while (u && (u->type & undo_action) &&
  878.            ((unsigned long)u->a==disp) && ((unsigned long)u->b==wind)) {
  879.       *prev = u->next;
  880.       prev = &(u->next);
  881.       u = u->next;
  882.     }
  883.     c = c->next;
  884.   }
  885. #endif
  886. }
  887.  
  888.  
  889.  
  890. /* Unify the corresponding arguments */
  891. void merge1(u,v)
  892.      ptr_node *u,v;
  893. {
  894.   long cmp;
  895.   ptr_node temp;
  896.   
  897.   if (v) {
  898.     if (*u==NULL) {
  899.       /* push_ptr_value(int_ptr,u); */
  900.       /* (*u)=STACK_ALLOC(node); */
  901.       /* **u= *v; */
  902.       /* more_v_attr=TRUE; */
  903.     }
  904.     else {
  905.       cmp=featcmp((*u)->key,v->key);
  906.       if (cmp==0) {
  907.     if (v->right)
  908.       merge1(&((*u)->right),v->right);
  909.     
  910.     push_goal(unify,(*u)->data,v->data,NULL);
  911.     
  912.     if (v->left)
  913.       merge1(&((*u)->left),v->left);
  914.       }
  915.       else if (cmp>0) {
  916.     temp=v->right;
  917.     v->right=NULL;
  918.     merge1(&((*u)->left),v);
  919.     merge1(u,temp);
  920.     v->right=temp;
  921.       }
  922.       else {
  923.         temp=v->left;
  924.         v->left=NULL;
  925.         merge1(&((*u)->right),v);
  926.         merge1(u,temp);
  927.         v->left=temp;
  928.       }
  929.     }
  930.   }
  931.   else if (*u!=NULL) {
  932.     /* more_u_attr=TRUE; */
  933.   }
  934. }
  935.  
  936.  
  937. /* Evaluate the lone arguments (For LAZY failure + EAGER success) */
  938. /* Evaluate low numbered lone arguments first. */
  939. /* For each lone argument in either u or v, create a new psi-term to put */
  940. /* the (useless) result: This is needed so that *all* arguments of a uni-*/
  941. /* unified psi-term are evaluated, which avoids incorrect 'Yes' answers. */
  942. void merge2(u,v)
  943.      ptr_node *u,v;
  944. {
  945.   long cmp;
  946.   ptr_node temp;
  947.   
  948.   if (v) {
  949.     if (*u==NULL) {
  950.       ptr_psi_term t;
  951.       merge2(u,v->right);
  952.       t = (ptr_psi_term) v->data;
  953.       deref2_rec_eval(t); /* Assumes goal_stack is already restored. */
  954.       merge2(u,v->left);
  955.     }
  956.     else {
  957.       cmp=featcmp((*u)->key,v->key);
  958.       if (cmp==0) {
  959.     /* if (v->right) */
  960.     merge2(&((*u)->right),v->right);
  961.     
  962.     /* if (v->left) */
  963.     merge2(&((*u)->left),v->left);
  964.       }
  965.       else if (cmp>0) {
  966.     temp=v->right;
  967.     v->right=NULL;
  968.     merge2(&((*u)->left),v);
  969.     merge2(u,temp);
  970.     v->right=temp;
  971.       }
  972.       else {
  973.         temp=v->left;
  974.         v->left=NULL;
  975.         merge2(&((*u)->right),v);
  976.         merge2(u,temp);
  977.         v->left=temp;
  978.       }
  979.     }
  980.   }
  981.   else if (*u!=NULL) {
  982.     ptr_psi_term t;
  983.     merge2(&((*u)->right),v);
  984.     t = (ptr_psi_term) (*u)->data;
  985.     deref2_rec_eval(t); /* Assumes goal_stack is already restored. */
  986.     merge2(&((*u)->left),v);
  987.   }
  988. }
  989.  
  990.  
  991. /* Merge v's loners into u and evaluate the corresponding arguments */
  992. void merge3(u,v)
  993.      ptr_node *u,v;
  994. {
  995.   long cmp;
  996.   ptr_node temp;
  997.   
  998.   if (v) {
  999.     if (*u==NULL) {
  1000.       push_ptr_value(int_ptr,u);
  1001.       (*u)=STACK_ALLOC(node);
  1002.       **u= *v;
  1003.       more_v_attr=TRUE;
  1004.     }
  1005.     else {
  1006.       ptr_psi_term t1,t2;
  1007.       
  1008.       cmp=featcmp((*u)->key,v->key);
  1009.       if (cmp==0) {
  1010.     if (v->right)
  1011.       merge3(&((*u)->right),v->right);
  1012.     
  1013.         t1 = (ptr_psi_term) (*u)->data;
  1014.         /* t2 = (ptr_psi_term) v->data; */
  1015.         deref2_eval(t1);
  1016.         /* deref2_eval(t2); */
  1017.     /* push_goal(unify,(*u)->data,v->data,NULL); */
  1018.     
  1019.     if (v->left)
  1020.       merge3(&((*u)->left),v->left);
  1021.       }
  1022.       else if (cmp>0) {
  1023.     temp=v->right;
  1024.     v->right=NULL;
  1025.     merge3(&((*u)->left),v);
  1026.     merge3(u,temp);
  1027.     v->right=temp;
  1028.       }
  1029.       else {
  1030.         temp=v->left;
  1031.         v->left=NULL;
  1032.         merge3(&((*u)->right),v);
  1033.         merge3(u,temp);
  1034.         v->left=temp;
  1035.       }
  1036.     }
  1037.   }
  1038.   else if (*u!=NULL) {
  1039.     more_u_attr=TRUE;
  1040.   }
  1041. }
  1042.  
  1043.  
  1044.  
  1045.  
  1046. /******** MERGE(u,v)
  1047.   U and V are two binary trees containing the
  1048.   attributes fields of psi-terms.  U and V are merged together, that is U
  1049.   becomes the union of U and V:
  1050.   For each label L in V and L->Vpsi_term:
  1051.   If L is in U Then With L->Upsi_term Do unify(Upsi_term,Vpsi_term)
  1052.   Else merge L->Vpsi_term in U.
  1053.   Unification is simply done by appending the 2 psi_terms to the unification
  1054.   stack.  All effects must be recorded in the trail so that they can be
  1055.   undone on backtracking.
  1056.   */
  1057.  
  1058. #if FALSE
  1059. /* This version is not quite right */
  1060. void merge(u,v)
  1061.      ptr_node *u,v;
  1062. {
  1063.   long cmp;
  1064.   ptr_node temp;
  1065.   
  1066.   if (v) {
  1067.     if (*u==NULL) {
  1068.       ptr_psi_term t;
  1069.       merge(u,v->right);
  1070.       
  1071.       push_ptr_value(int_ptr,u);
  1072.       (*u)=STACK_ALLOC(node);
  1073.       **u= *v;
  1074.       more_v_attr=TRUE;
  1075.       
  1076.       t = (ptr_psi_term) v->data;
  1077.       deref2_rec_eval(t); /* Assumes goal_stack is already restored. */
  1078.       merge(u,v->left);
  1079.     }
  1080.     else {
  1081.       cmp=featcmp((*u)->key,v->key);
  1082.       if (cmp==0) {
  1083.         /* if (v->right) */
  1084.     merge(&((*u)->right),v->right);
  1085.     
  1086.         push_goal(unify,(*u)->data,v->data,NULL);
  1087.     
  1088.         /* if (v->left) */
  1089.     merge(&((*u)->left),v->left);
  1090.       }
  1091.       else if (cmp>0) {
  1092.         temp=v->right;
  1093.         v->right=NULL;
  1094.         merge(&((*u)->left),v);
  1095.         merge(u,temp);
  1096.         v->right=temp;
  1097.       }
  1098.       else {
  1099.         temp=v->left;
  1100.         v->left=NULL;
  1101.         merge(&((*u)->right),v);
  1102.         merge(u,temp);
  1103.         v->left=temp;
  1104.       }
  1105.     }
  1106.   }
  1107.   else if (*u!=NULL) {
  1108.     ptr_psi_term t;
  1109.     merge(&((*u)->right),v);
  1110.     t = (ptr_psi_term) (*u)->data;
  1111.     deref2_rec_eval(t); /* Assumes goal_stack is already restored. */
  1112.     merge(&((*u)->left),v);
  1113.     
  1114.     more_u_attr=TRUE;
  1115.   }
  1116. }
  1117. #endif
  1118.  
  1119. void merge(u,v)
  1120.      ptr_node *u,v;
  1121. {
  1122.   merge1(u,v); /* Unify corresponding arguments */
  1123.   merge2(u,v); /* Evaluate lone arguments (lazy failure + eager success) */
  1124.   merge3(u,v); /* Merge v's loners into u & evaluate corresponding arguments */
  1125. }
  1126.  
  1127. /* For built-ins.c */
  1128. void merge_unify(u,v)
  1129.      ptr_node *u,v;
  1130. {
  1131.   merge1(u,v); /* Unify corresponding arguments */
  1132.   merge3(u,v); /* Merge v's loners into u & evaluate corresponding arguments */
  1133. }
  1134.  
  1135.  
  1136.  
  1137.  
  1138. /******** SHOW_COUNT()
  1139.   This routine doesn't do anything if not in verbose mode.
  1140.   It prints the number of of sub-goals attempted, along with cpu-time
  1141.   spent during the proof etc...
  1142.   */
  1143. void show_count()
  1144. {
  1145.   float t;
  1146.   
  1147.   if (verbose) {
  1148.     printf("  [");
  1149.     
  1150.     times(&end_time);
  1151. #ifndef OS2_PORT
  1152.     t = (end_time.tms_utime - start_time.tms_utime)/60.0;
  1153. #else
  1154.     t = (end_time - start_time)/60.0;
  1155. #endif    
  1156.     printf("%1.3fs cpu, %ld goal%s",t,goal_count,(goal_count!=1?"s":""));
  1157.     
  1158.     if (t!=0.0) printf(" (%0.0f/s)",goal_count/t);
  1159.     
  1160.     printf(", %ld stack",sizeof(mem_base)*(stack_pointer-mem_base));
  1161.     printf(", %ld heap",sizeof(mem_base)*(mem_limit-heap_pointer));
  1162.     
  1163.     printf("]");
  1164.   }
  1165.   
  1166.   if(NOTQUIET) {
  1167.     printf("\n");
  1168.     stack_info(stdout);
  1169.   }
  1170.   
  1171.   goal_count=0;
  1172. }
  1173.  
  1174.  
  1175.  
  1176. /******** FETCH_DEF(psi_term)
  1177.   Fetch the type definition of a psi_term and execute it.
  1178.   That is, get the list of (term,predicate) pairs that define the type.
  1179.   Unify the psi_term with the term, then prove the predicate.
  1180.   
  1181.   This routine only gets the pairs that are defined in the type itself,
  1182.   not those defined in any types above it.  This is the correct behavior
  1183.   for enumerating type disjunctions--all higher constraints have already
  1184.   been checked.
  1185.   
  1186.   The above is true if allflag==FALSE.  If allflag==TRUE then all constraints
  1187.   are executed, not just those defined in the type itself.
  1188.   */
  1189. void fetch_def(u, allflag)
  1190.      ptr_psi_term u;
  1191.      long allflag;
  1192. {
  1193.   ptr_triple_list prop;
  1194.   ptr_psi_term v,w;
  1195.   ptr_definition utype;
  1196.   
  1197.   /* Uses SMASK because called from check_out */
  1198.   push2_ptr_value(int_ptr,&(u->status),(u->status & SMASK));
  1199.   u->status=(4 & SMASK) | (u->status & RMASK);
  1200.   
  1201.   utype=u->type;
  1202.   prop=u->type->properties;
  1203.   if (prop) {
  1204.     
  1205.     Traceline("fetching definition of %P\n",u);
  1206.     
  1207.     while (prop) {
  1208.       if (allflag || prop->c==utype) {
  1209.         clear_copy();
  1210.         v=eval_copy(prop->a,STACK);
  1211.         w=eval_copy(prop->b,STACK);
  1212.         
  1213.         if (w) push_goal(prove,w,DEFRULES,NULL);
  1214.         
  1215.         deref_ptr(v);
  1216.         v->status=4;
  1217.         push_goal(unify,u,v,NULL);
  1218.         i_eval_args(v->attr_list);
  1219.       }
  1220.       prop=prop->next;
  1221.     }
  1222.   }
  1223. }
  1224.  
  1225.  
  1226. /******** FETCH_DEF_LAZY(psi_term,type1,type2,attr_list1,attr_list2)
  1227.   Fetch the type definition of a psi_term and execute it.
  1228.   That is, get the list of (term,pred) pairs that define the type.
  1229.   'Term' is one of the type's attributes and 'pred' is a constraint.
  1230.   Unify the psi_term with the term, then prove pred.
  1231.   
  1232.   Only those (term,pred) pairs are executed whose original type is
  1233.   below both type1 and type2, the types of the two psi-terms whose
  1234.   unification created psi_term.  This avoids doing much superfluous work.
  1235.   
  1236.   The above behavior is correct for a psi_term when always_check==TRUE for
  1237.   that psi_term.  If always_check==FALSE for a psi_term, then if it does not
  1238.   have attributes it is not checked, and the addition of an attribute will
  1239.   force checking to occur.
  1240.   
  1241.   Example:
  1242.   
  1243.   :: t(a=>one,b=>two,c=> X) | thing(X).
  1244.   
  1245.   psi_term = A:t (it can be any psi_term of type t)
  1246.   term     = t(a=>one,b=>two,c=> X)
  1247.   pred     = thing(X)
  1248.   */
  1249. void fetch_def_lazy(u, old1, old2, old1attr, old2attr, old1stat, old2stat)
  1250.      ptr_psi_term u;
  1251.      ptr_definition old1, old2;
  1252.      ptr_node old1attr, old2attr;
  1253.      long old1stat, old2stat;
  1254. {
  1255.   ptr_triple_list prop;
  1256.   ptr_psi_term v,w;
  1257.   long checked1, checked2;
  1258.   long m1, m2;
  1259.   
  1260.   if (!u->type->always_check) if (u->attr_list==NULL) return;
  1261.   
  1262.   push_ptr_value(int_ptr,&(u->status));
  1263.   u->status=4;
  1264.   
  1265.   prop=u->type->properties;
  1266.   if (prop) {
  1267.     Traceline("fetching partial definition of %P\n",u);
  1268.     
  1269.     checked1 = old1attr || old1->always_check;
  1270.     checked2 = old2attr || old2->always_check;
  1271.  
  1272.     /* checked1 = (old1stat==4); */ /* 18.2.94 */
  1273.     /* checked2 = (old2stat==4); */
  1274.     
  1275.     while (prop) {
  1276.       /* Only do those constraints that have not yet been done: */
  1277.       /* In matches, mi is TRUE iff oldi <| prop->c.            */
  1278.       if (!checked1) m1=FALSE; else matches(old1,prop->c,&m1);
  1279.       if (!checked2) m2=FALSE; else matches(old2,prop->c,&m2);
  1280.       if (!m1 && !m2) {
  1281.     /* At this point, prop->c is an attribute that has not yet */
  1282.     /* been checked. */
  1283.     clear_copy();
  1284.     v=eval_copy(prop->a,STACK);
  1285.     w=eval_copy(prop->b,STACK);
  1286.     
  1287.     if (w) push_goal(prove,w,DEFRULES,NULL);
  1288.     
  1289.     deref_ptr(v);
  1290.     v->status=4;
  1291.     push_goal(unify,u,v,NULL);
  1292.     i_eval_args(v->attr_list);
  1293.       }
  1294.       prop=prop->next;
  1295.     }
  1296.   }
  1297. }
  1298.  
  1299.  
  1300.  
  1301. /******** UNIFY_AIM()
  1302.   This routine performs one unification step.
  1303.   AIM is the current unification goal.
  1304.   
  1305.   U and V are the two psi-terms to unify.
  1306.   
  1307.   It swaps the two psi-terms into chronological order.
  1308.   U is the oldest (smallest stack address).
  1309.   Calculates their GLB, check their values are unifiable.
  1310.   It deals with all the messy things like:
  1311.   curried functions gaining missing arguments,
  1312.   types which need checking,
  1313.   residuation variables whose constraints must be released,
  1314.   disjunctions appearing in the GLB etc...
  1315.   
  1316.   It's a rather lengthy routine, only its speed is fairly crucial in the
  1317.   overall performance of Wild_Life, and the code is not duplicated elsewhere.
  1318.   */
  1319.  
  1320. long unify_body();
  1321.  
  1322. long unify_aim_noeval()
  1323. {
  1324.   return unify_body(FALSE);
  1325. }
  1326.  
  1327. long unify_aim()
  1328. {
  1329.   return unify_body(TRUE);
  1330. }
  1331.  
  1332. long unify_body(eval_flag)
  1333.      long eval_flag;
  1334. {
  1335.   long success=TRUE,compare;
  1336.   ptr_psi_term u,v,tmp;
  1337.   ptr_list lu,lv;
  1338.   REAL r;
  1339.   ptr_definition new_type,old1,old2;
  1340.   ptr_node old1attr, old2attr;
  1341.   ptr_int_list new_code;
  1342.   ptr_int_list d=NULL;
  1343.   long old1stat,old2stat; /* 18.2.94 */
  1344.   
  1345.   u=(ptr_psi_term )aim->a;
  1346.   v=(ptr_psi_term )aim->b;
  1347.   
  1348.   deref_ptr(u);
  1349.   deref_ptr(v);
  1350.  
  1351.   Traceline("unify %P with %P\n",u,v);
  1352.   
  1353.   if (eval_flag) {
  1354.     deref(u);
  1355.     deref(v);
  1356.   }
  1357.   
  1358.   if (u!=v) {
  1359.     
  1360.     /**** Swap the two psi-terms to get them into chronological order ****/
  1361.     if (u>v) { tmp=v; v=u; u=tmp; }
  1362.       
  1363.     /**** Check for curried functions ****/
  1364.     u_func=(u->type->type==function);
  1365.     v_func=(v->type->type==function);
  1366.     old1stat=u->status; /* 18.2.94 */
  1367.     old2stat=v->status; /* 18.2.94 */
  1368.     
  1369.     /* PVR 18.2.94 */
  1370.     /* if (u_func && !(u->flags"ED_TRUE) && v->attr_list) { */
  1371.     if (u_func && u->status==4 && !(u->flags"ED_TRUE) && v->attr_list) {
  1372.       Errorline("attempt to unify with curried function %P\n", u);
  1373.       return FALSE;
  1374.     }
  1375.     /* if (v_func && !(v->flags"ED_TRUE) && u->attr_list) { */
  1376.     if (v_func && v->status==4 && !(v->flags"ED_TRUE) && u->attr_list) {
  1377.       Errorline("attempt to unify with curried function %P\n", v);
  1378.       return FALSE;
  1379.     }
  1380.  
  1381.     
  1382. #ifdef ARITY  /*  RM: Mar 29 1993  */
  1383.     arity_unify(u,v);
  1384. #endif
  1385.     
  1386.     /***** Deal with global vars ****   RM: Feb  8 1993  */
  1387.     if((GENERIC)v>=heap_pointer)
  1388.       return global_unify(u,v);
  1389.     
  1390.     
  1391.     /**** Calculate their Greatest Lower Bound and compare them ****/
  1392.     success=(compare=glb(u->type,v->type,&new_type,&new_code));
  1393.     
  1394.     if (success) {
  1395.       
  1396.       /**** Keep the old types for later use in incr. constraint checking ****/
  1397.       old1 = u->type;
  1398.       old2 = v->type;
  1399.       old1attr = u->attr_list;
  1400.       old2attr = v->attr_list;
  1401.       
  1402.       /**** DECODE THE RESULTING TYPE ****/
  1403.       if (!new_type) {
  1404.     d=decode(new_code);
  1405.     if (d) {
  1406.       new_type=(ptr_definition )d->value;
  1407.       d=d->next;
  1408.     }
  1409.     else
  1410.           Errorline("undecipherable sort code.\n");
  1411.       }
  1412.       
  1413.       /**** Make COMPARE a little more precise ****/
  1414.       if (compare==1)
  1415.     if (u->value && !v->value)
  1416.       compare=2;
  1417.     else
  1418.       if (v->value && !u->value)
  1419.         compare=3;
  1420.       
  1421.       /**** Determine the status of the resulting psi-term ****/
  1422.       new_stat=4;
  1423.       switch (compare) {
  1424.       case 1:
  1425.     if (u->status <4 && v->status <4)
  1426.       new_stat=2;
  1427.     break;
  1428.       case 2:
  1429.     if (u->status<4)
  1430.       new_stat=2;
  1431.     break;
  1432.       case 3:
  1433.     if (v->status<4)
  1434.       new_stat=2;
  1435.     break;
  1436.       case 4:
  1437.     new_stat=2;
  1438.     break;
  1439.       }
  1440.       
  1441.       /*
  1442.     printf("u=%s, v=%s, compare=%ld, u.s=%ld, v.s=%ld, ns=%ld\n",
  1443.     u->type->keyword->symbol,
  1444.     v->type->keyword->symbol,
  1445.     compare,
  1446.     u->status,
  1447.     v->status,
  1448.     new_stat);
  1449.     */
  1450.       
  1451.       /**** Check that integers have no decimals ****/
  1452.       if (u->value && sub_type(new_type,integer)) {
  1453.     r= *(REAL *)u->value;
  1454.     success=(r==floor(r));
  1455.       }
  1456.       if (success && v->value && sub_type(new_type,integer)) {
  1457.     r= *(REAL *)v->value;
  1458.     success=(r==floor(r));
  1459.       }
  1460.       
  1461.       /**** Unify the values of INTs REALs STRINGs LISTs etc... ****/
  1462.       if (success) {
  1463.         /* LAZY-EAGER */
  1464.     if (u->value!=v->value)
  1465.       if (!u->value) {
  1466.         compare=4;
  1467.         push_ptr_value(int_ptr,&(u->value));
  1468.         u->value=v->value;        
  1469.       }
  1470.       else if (v->value) {
  1471.         if (overlap_type(new_type,real))
  1472.               success=(*((REAL *)u->value)==(*((REAL *)v->value)));
  1473.             else if (overlap_type(new_type,quoted_string))
  1474.               success=(strcmp((char *)u->value,(char *)v->value)==0);
  1475.         else if (overlap_type(new_type,sys_bytedata)) {
  1476.           unsigned long ulen = *((unsigned long *)u->value);
  1477.           unsigned long vlen = *((unsigned long *)v->value);
  1478.               success=(ulen==vlen &&
  1479.                (bcmp((char *)u->value,(char *)v->value,ulen)==0));
  1480.         }
  1481.             else if (u->type==cut && v->type==cut) { /* 22.9 */
  1482.               GENERIC mincut;
  1483.               mincut = (u->value<v->value?u->value:v->value);
  1484.               if (mincut!=u->value) {
  1485.                 push_ptr_value(cut_ptr,&(u->value));
  1486.                 u->value=mincut;
  1487.               }
  1488.             }
  1489.             else {
  1490.               Warningline("'%s' may not be unified.\n",new_type->keyword->symbol);
  1491.               success=FALSE;
  1492.             }
  1493.           }
  1494.           else
  1495.         compare=4;
  1496.       }
  1497.       
  1498.       /**** Bind the two psi-terms ****/
  1499.       if (success) {
  1500.     /* push_ptr_value(psi_term_ptr,&(v->coref)); 9.6 */
  1501.     push_psi_ptr_value(v,&(v->coref));
  1502.     v->coref=u;
  1503.     
  1504.     if (!equal_types(u->type,new_type)) {          
  1505.       push_ptr_value(def_ptr,&(u->type));
  1506.           /* This does not seem to work right with cut.lf: */
  1507.           /* push_def_ptr_value(u,&(u->type)); */ /* 14.8 */
  1508.       u->type=new_type;
  1509.     }
  1510.     
  1511.     if (u->status!=new_stat) {
  1512.       push_ptr_value(int_ptr,&(u->status));
  1513.       u->status=new_stat;
  1514.     }
  1515.     
  1516.     /**** Unify the attributes ****/
  1517.     more_u_attr=FALSE;
  1518.     more_v_attr=FALSE;
  1519.     
  1520.     
  1521. #ifdef ARITY  /*  RM: Mar 29 1993  */
  1522.     arity_merge(u->attr_list,v->attr_list);
  1523. #endif
  1524.     
  1525.     
  1526.     if (u->attr_list || v->attr_list)
  1527.       merge(&(u->attr_list),v->attr_list);
  1528.     
  1529.     /**** Look after curried functions ****/
  1530.     /*
  1531.     if ((u_func && more_v_attr) || (v_func && more_u_attr)) {
  1532.       if (!(u->flags"ED_TRUE | v->flags"ED_TRUE)) {
  1533.             Traceline("re-evaluating curried expression %P\n", u);
  1534.         if (u->status!=0) {
  1535.           push_ptr_value(int_ptr,&(u->status));
  1536.           u->status=0;
  1537.         }
  1538.             check_func(u);
  1539.           }
  1540.       }
  1541.       */
  1542.     
  1543.     if (v->flags"ED_TRUE && !(u->flags"ED_TRUE)) { /* 16.9 */
  1544.       push_ptr_value(int_ptr,&(u->flags));
  1545.       u->flags|=QUOTED_TRUE;
  1546.         }
  1547.     
  1548.     /**** RELEASE RESIDUATIONS ****/
  1549.     /* This version implements the correct semantics. */
  1550.     if (u->resid)
  1551.       release_resid(u);
  1552.     if (v->resid)
  1553.       release_resid(v);
  1554.     
  1555.         /**** Alternatives in a type disjunction ****/
  1556.         if (d) {
  1557.           Traceline("pushing type disjunction choice point for %P\n",u);
  1558.           push_choice_point(type_disj,u,d,NULL);
  1559.         }
  1560.     
  1561.     /**** VERIFY CONSTRAINTS ****/
  1562.     /* if ((old1stat<4 || old2stat<4) &&
  1563.          (u->type->type==type || v->type->type==type)) { 18.2.94 */
  1564.         if (new_stat<4 && u->type->type==type) {
  1565.           /* This does not check the already-checked properties     */
  1566.           /* (i.e. those in types t with t>=old1 or t>=old2),       */
  1567.           /* and it does not check anything if u has no attributes. */
  1568.           /* It will, however, check the unchecked properties if a  */
  1569.           /* type gains attributes.                                 */
  1570.           fetch_def_lazy(u, old1, old2, 
  1571.                old1attr, old2attr,
  1572.              old1stat, old2stat);
  1573.         }
  1574.       }
  1575.     }
  1576.   }
  1577.   return success;
  1578. }
  1579.  
  1580.  
  1581.  
  1582. /******** DISJUNCT_AIM()
  1583.   This is the disjunction enumeration routine.
  1584.   If U is the disjunction {H|T} then first bind U to H, then on backtracking
  1585.   enumerate the disjunction T.  U is always passed along so that every choice
  1586.   of the disjunction can be bound to U.
  1587.   */
  1588. long disjunct_aim()
  1589. {
  1590.   ptr_psi_term u,v;
  1591.   ptr_list l;
  1592.   long success=TRUE;
  1593.   
  1594.   printf("Call to disjunct_aim\nThis routine inhibited by RM: Dec  9 1992\n");
  1595.   
  1596.   return success;
  1597. }
  1598.  
  1599.  
  1600.  
  1601. /******** PROVE_AIM()
  1602.   This is the proving routine.  It performs one
  1603.   proof step, that is: finding the definition to use to prove AIM, and
  1604.   unifying the HEAD with the GOAL before proving. It all works by pushing
  1605.   sub-goals onto the goal_stack. Special cases are CUT and AND (","). Built-in
  1606.   predicates written in C are called.
  1607.   */
  1608. long prove_aim()
  1609. {
  1610.   long success=TRUE;
  1611.   ptr_psi_term thegoal,head,body,arg1,arg2;
  1612.   ptr_pair_list rule;
  1613.   
  1614.   thegoal=(ptr_psi_term )aim->a;
  1615.   rule=(ptr_pair_list )aim->b;
  1616.   
  1617.   if (thegoal && rule) {
  1618.     
  1619.     deref_ptr(thegoal); /* Evaluation is explicitly handled later. */
  1620.     
  1621.     if (thegoal->type!=and) {
  1622.       if (thegoal->type!=cut)
  1623.     if(thegoal->type!=life_or) {
  1624.       /* User-defined predicates with unevaluated arguments */
  1625.       /* Built-ins do this themselves (see built_ins.c). */
  1626.       /* if (!thegoal->type->evaluate_args) mark_quote(thegoal); 24.8 25.8 */
  1627.       
  1628.       if(i_check_out(thegoal)) { /* RM: Apr  6 1993  */
  1629.         
  1630.         goal_stack=aim->next;
  1631.         goal_count++;
  1632.         
  1633.         if ((unsigned long)rule==DEFRULES) {
  1634.           rule=(ptr_pair_list)thegoal->type->rule;
  1635.           if (thegoal->type->type==predicate) {
  1636.         if (!rule) /* This can happen when RETRACT is used */
  1637.           success=FALSE;
  1638.           }
  1639.           else if ( thegoal->type->type==function
  1640.               || ( thegoal->type->type==type
  1641.              && sub_type(boolean,thegoal->type)
  1642.              )
  1643.                   ) {
  1644.         if (thegoal->type->type==function && !rule)
  1645.           /* This can happen when RETRACT is used */
  1646.           success=FALSE;
  1647.         else {
  1648.           ptr_psi_term bool_pred;
  1649.           ptr_node a;
  1650.           /* A function F in pred. position is called as */
  1651.           /* '*bool_pred*'(F), which succeeds if F returns true */
  1652.           /* and fails if it returns false.  It can residuate too. */
  1653.           bool_pred=stack_psi_term(0);
  1654.           bool_pred->type=boolpredsym;
  1655.           bool_pred->attr_list=(a=STACK_ALLOC(node));
  1656.           a->key=one;
  1657.           a->left=a->right=NULL;
  1658.           a->data=(GENERIC) thegoal;
  1659.           push_goal(prove,bool_pred,DEFRULES,NULL);
  1660.           return success; /* We're done! */
  1661.         }
  1662.           }
  1663.           else if (!thegoal->type->protected && thegoal->type->type==undef) {
  1664.         /* Don't give an error message for undefined dynamic objects */
  1665.         /* that do not yet have a definition */
  1666.         success=FALSE;
  1667.           }
  1668.           else if (thegoal->type==true || thegoal->type==false) {
  1669.         /* What if the 'true' or 'false' have arguments? */
  1670.         success=(thegoal->type==true);
  1671.         return success; /* We're done! */
  1672.           }
  1673.           else {
  1674.         /* Error: undefined predicate. */
  1675.         /* Call the call_handler (which may do an auto-load). */
  1676.         ptr_psi_term call_handler;
  1677.         /* mark_quote(thegoal); */
  1678.         
  1679.         /*  RM: Jan 27 1993 */
  1680.         /* Warningline("call handler invoked for %P\n",thegoal); */
  1681.         
  1682.         call_handler=stack_psi_term(0);
  1683.         call_handler->type=call_handlersym;
  1684.         stack_add_psi_attr(call_handler,"1",thegoal);
  1685.         push_goal(prove,call_handler,DEFRULES,NULL);
  1686.         return success; /* We're done! */
  1687.           }
  1688.         }
  1689.         
  1690.         if (success) {
  1691.           
  1692.           if ((unsigned long)rule<=MAX_BUILT_INS) {
  1693.         
  1694.         /* For residuation (RESPRED) */
  1695.         curried=FALSE;
  1696.         can_curry=TRUE;
  1697.         resid_vars=NULL;
  1698.         /* resid_limit=(ptr_goal )stack_pointer; 12.6 */
  1699.         
  1700.         if (thegoal->type!=tracesym) /* 26.1 */
  1701.           Traceline("prove built-in %P\n", thegoal);
  1702.         
  1703.         /* RESPRED */ resid_aim=aim;
  1704.         /* Residuated predicate must return success=TRUE */
  1705.         success=c_rule[(unsigned long)rule]();
  1706.         
  1707.         /* RESPRED */ if (curried)
  1708.         /* RESPRED */   do_currying();
  1709.         /* RESPRED */ else if (resid_vars)
  1710.         /* RESPRED */   success=do_residuation_user(); /* 21.9 */ /* PVR 9.2.94 */
  1711.           }
  1712.           else {
  1713.         
  1714.         /* Evaluate arguments of a predicate call before the call. */
  1715.         deref_args(thegoal,set_empty);
  1716.         
  1717.         Traceline("prove %P\n", thegoal);
  1718.         
  1719.         /* For residuation (RESPRED) */
  1720.         curried=FALSE;
  1721.         can_curry=TRUE;
  1722.         resid_vars=NULL;
  1723.         /* resid_limit=(ptr_goal )stack_pointer; 12.6 */
  1724.         
  1725.         while (rule && (rule->a==NULL || rule->b==NULL)) {
  1726.           rule=rule->next;
  1727.           Traceline("alternative clause has been retracted\n");
  1728.         }
  1729.         if (rule) {
  1730.           
  1731.           clear_copy();
  1732.           if (TRUE) /* 8.9 */
  1733.             /* if (thegoal->type->evaluate_args) 8.9 */
  1734.             head=eval_copy(rule->a,STACK);
  1735.           else
  1736.             head=quote_copy(rule->a,STACK);
  1737.  
  1738.           body=eval_copy(rule->b,STACK);
  1739.  
  1740.           /* What does this do?? */
  1741.           /* if (body->type==built_in) */
  1742.           /*   body->coref=head; */
  1743.           
  1744.           if (rule->next)
  1745.             push_choice_point(prove,thegoal,rule->next,NULL);
  1746.           
  1747.           if (body->type!=succeed)
  1748.             push_goal(prove,body,DEFRULES,NULL);
  1749.           
  1750.           /* push_ptr_value(psi_term_ptr,&(head->coref)); 9.6 */
  1751.           push_psi_ptr_value(head,&(head->coref));
  1752.           head->coref=thegoal;
  1753.           merge(&(thegoal->attr_list),head->attr_list);
  1754.           if (!head->status) {
  1755.             i_eval_args(head->attr_list);
  1756.           }
  1757.         }
  1758.         else {
  1759.           success=FALSE;
  1760.         }
  1761.           }
  1762.         }
  1763.       }
  1764.     }
  1765.     else { /* ';' built-in */
  1766.       /*  RM: Apr  6 1993  */
  1767.       goal_stack=aim->next;
  1768.       goal_count++;
  1769.       get_two_args(thegoal->attr_list,&arg1,&arg2);
  1770.       push_choice_point(prove,arg2,DEFRULES,NULL);
  1771.       push_goal(prove,arg1,DEFRULES,NULL);
  1772.     }
  1773.       else { /* 'Cut' built-in*/
  1774.     goal_stack=aim->next;
  1775.     goal_count++;
  1776.     /* assert((ptr_choice_point)(thegoal->value)<=choice_stack); 12.7 */
  1777.     cut_to(thegoal->value); /* 12.7 */
  1778. #ifdef CLEAN_TRAIL
  1779.         clean_trail(choice_stack);
  1780. #endif
  1781.         Traceline("cut all choice points back to %x\n",choice_stack);
  1782.       }
  1783.     }
  1784.     else { /* 'And' built-in */
  1785.       goal_stack=aim->next;
  1786.       goal_count++;
  1787.       get_two_args(thegoal->attr_list,&arg1,&arg2);
  1788.       push_goal(prove,arg2,DEFRULES,NULL);
  1789.       push_goal(prove,arg1,DEFRULES,NULL);
  1790.     }
  1791.   }
  1792.   else
  1793.     success=FALSE;
  1794.   
  1795.   /* RESPRED */ resid_aim=NULL;
  1796.   return success;
  1797. }
  1798.  
  1799.  
  1800.  
  1801. /******** TYPE_DISJ_AIM()
  1802.   This routine implements type disjunctions, that is, when a type has been
  1803.   decoded and found to be a disjunction of types, enumerates the different
  1804.   values one by one.
  1805.   */
  1806.  
  1807. void type_disj_aim()
  1808. {
  1809.   ptr_psi_term t;
  1810.   ptr_int_list d;
  1811.   
  1812.   t=(ptr_psi_term)aim->a;
  1813.   d=(ptr_int_list)aim->b;
  1814.   
  1815.   if (d->next) {
  1816.     Traceline("pushing type disjunction choice point for %P\n", t);
  1817.     push_choice_point(type_disj,t,d->next,NULL);
  1818.   }
  1819.   
  1820.   push_ptr_value(def_ptr,&(t->type));
  1821.   /* Below makes cut.lf behave incorrectly: */
  1822.   /* push_def_ptr_value(t,&(t->type)); */ /* 14.8 */
  1823.   t->type=(ptr_definition)d->value;
  1824.   
  1825.   Traceline("setting type disjunction to %s.\n", t->type->keyword->symbol);
  1826.   
  1827.   if ((t->attr_list || t->type->always_check) && t->status<4)
  1828.     fetch_def(t, FALSE);
  1829. }
  1830.  
  1831.  
  1832.  
  1833. /******** CLAUSE_AIM(r)
  1834.   Prove a CLAUSE or RETRACT goal. That is try to
  1835.   unify the calling argument with the current rule. If this succeeds and
  1836.   R=TRUE then delete the rule (RETRACT).
  1837.   */
  1838. long clause_aim(r)
  1839.      long r;
  1840. {
  1841.   long success=FALSE;
  1842.   ptr_pair_list *p;
  1843.   ptr_psi_term head,body,rule_head,rule_body;
  1844.   
  1845.   head=(ptr_psi_term)aim->a;
  1846.   body=(ptr_psi_term)aim->b;
  1847.   p=(ptr_pair_list *)aim->c;
  1848.   
  1849.   if ((unsigned long)(*p)>MAX_BUILT_INS) {
  1850.     success=TRUE;
  1851.     /* deref(head); 17.9 */
  1852.     
  1853.     if ((*p)->next) {
  1854.       if (r) {
  1855.         Traceline("pushing 'retract' choice point for %P\n", head);
  1856.     push_choice_point(del_clause,head,body,&((*p)->next));
  1857.     /* push_choice_point(del_clause,head,body,p); */
  1858.       }
  1859.       else {
  1860.         Traceline("pushing 'clause' choice point for %P\n", head);
  1861.     push_choice_point(clause,head,body,&((*p)->next));
  1862.       }
  1863.     }
  1864.     
  1865.     if (r)
  1866.       push_goal(retract,p,NULL,NULL);
  1867.     if ((*p)->a) {
  1868.       clear_copy();
  1869.       rule_head=quote_copy((*p)->a,STACK);
  1870.       rule_body=quote_copy((*p)->b,STACK);
  1871.       
  1872.       push_goal(unify,body,rule_body,NULL);
  1873.       push_goal(unify,head,rule_head,NULL);
  1874.       
  1875.       rule_head->status=4;
  1876.       rule_body->status=4;
  1877.       
  1878.       i_eval_args(rule_body->attr_list);
  1879.       i_eval_args(rule_head->attr_list);
  1880.       
  1881.       Traceline("fetching next clause for %s\n", head->type->keyword->symbol);
  1882.     }
  1883.     else {
  1884.       success=FALSE;
  1885.       Traceline("following clause had been retracted\n");
  1886.     }
  1887.   }
  1888.   else if ((unsigned long)(*p)>0) {
  1889.     if (r)
  1890.       Errorline("the built-in %P cannot be retracted.\n",head);
  1891.     else
  1892.       Errorline("the definition of built-in %P is not accessible.\n",head);
  1893.   }
  1894.   
  1895.   return success;
  1896. }
  1897.  
  1898.  
  1899. /* Return TRUE iff the top choice point is a what_next choice point */
  1900. /* or if there are no choice points. */
  1901. long no_choices()
  1902. {
  1903.   return (choice_stack==NULL) || (choice_stack->goal_stack->type==what_next);
  1904. }
  1905.  
  1906.  
  1907. /* Return the number of choice points on the choice point stack */
  1908. long num_choices()
  1909. {
  1910.   long num;
  1911.   ptr_choice_point cp;
  1912.   
  1913.   num=0;
  1914.   cp=choice_stack;
  1915.   while (cp) {
  1916.     num++;
  1917.     cp=cp->next;
  1918.   }
  1919.   return num;
  1920. }
  1921.  
  1922.  
  1923. /* Return the number of variables in the variable tree. */
  1924. long num_vars(vt)
  1925.      ptr_node vt;
  1926. {
  1927.   long num;
  1928.   
  1929.   return (vt?(num_vars(vt->left)+1+num_vars(vt->right)):0);
  1930. }
  1931.  
  1932.  
  1933.  
  1934. /* Cut away up to and including the first 'what_next' choice point. */
  1935. long what_next_cut()
  1936. {
  1937.   long flag=TRUE;
  1938.   long result=FALSE;
  1939.   
  1940.   do {
  1941.     if (choice_stack) {
  1942.       backtrack();
  1943.       if (goal_stack->type==what_next) {
  1944.         flag=FALSE;
  1945.         result=TRUE;
  1946.       }
  1947.     }
  1948.     else {
  1949.       /* This undo does the last undo actions before returning to top level. */
  1950.       /* It is not needed for variable undoing, but for actions (like */
  1951.       /* closing windows). */
  1952.       undo(NULL);
  1953.       /* undo(mem_base); 7.8 */
  1954. #ifdef TS
  1955.       /* global_time_stamp=INIT_TIME_STAMP; */ /* 9.6 */
  1956. #endif
  1957.       flag=FALSE;
  1958.     }
  1959.   } while (flag);
  1960.   
  1961.   return result;
  1962. }
  1963.  
  1964.  
  1965. /* UNUSED 12.7 */
  1966. /* Return the choice point corresponding to the first 'what_next' */
  1967. /* choice point in the choice point stack.  Return NULL if there is none. */
  1968. /* This is used to ensure that cuts don't go below the most recent */
  1969. /* 'what_next' choice point. */
  1970. ptr_choice_point topmost_what_next()
  1971. {
  1972.   ptr_choice_point cp=choice_stack;
  1973.   
  1974.   while (cp && cp->goal_stack && cp->goal_stack->type!=what_next)
  1975.     cp=cp->next;
  1976.   
  1977.   if (cp && cp->goal_stack && cp->goal_stack->type==what_next)
  1978.     return cp;
  1979.   else
  1980.     return (ptr_choice_point) NULL;
  1981. }
  1982.  
  1983.  
  1984. /* Called when level jumps back to zero.  Setting these two pointers to */
  1985. /* NULL causes an exit from main_prove and will then reset all other    */
  1986. /* global information. */
  1987. void reset_stacks()
  1988. {
  1989.   undo(NULL); /* 8.10 */
  1990.   goal_stack=NULL;
  1991.   choice_stack=NULL;
  1992. #ifdef TS
  1993.   /* global_time_stamp=INIT_TIME_STAMP; */ /* 9.6 */
  1994. #endif
  1995. }
  1996.  
  1997.  
  1998. /******** WHAT_NEXT_AIM()
  1999.   Find out what the user wants to do:
  2000.   a) retry current goal -> ';'
  2001.   b) quit current goal -> RETURN
  2002.   c) add current goal -> 'new goal ?'
  2003.   d) return to top level -> '.'
  2004.   */
  2005. long what_next_aim()
  2006. {
  2007.   long result=FALSE;
  2008.   ptr_psi_term s;
  2009.   long c, c2; /* 21.12 (prev. char) */
  2010.   char *pr;
  2011.   long sort,cut=FALSE;
  2012.   long level,i;
  2013.   long eventflag;
  2014.   ptr_stack save_undo_stack;
  2015.   
  2016.   begin_terminal_io();
  2017.   
  2018.   level=((unsigned long)aim->c);
  2019.   
  2020.   if (aim->a) {
  2021.     /* Must remember var_occurred from the what_next goal and from */
  2022.     /* execution of previous query (it may have contained a parse) */
  2023.     var_occurred=var_occurred || ((unsigned long)aim->b)&TRUEMASK; /* 18.8 */
  2024.     eventflag=(((unsigned long)aim->b)&(TRUEMASK*2))!=0;
  2025.     if (
  2026.         !var_occurred && no_choices() && level>0
  2027. #ifdef X11
  2028.         /* Keep level same if no window & no X event */
  2029.     && !x_window_creation && !eventflag
  2030. #endif
  2031.        ) {
  2032.       /* Keep level the same if in a query, the number of choice points */
  2033.       /* has not increased and there are no variables. */
  2034.       /* This has to have the same behavior as if an EOLN was typed */
  2035.       /* and no 'No' message should be given on the lowest level,   */
  2036.       level--;
  2037.       what_next_cut();
  2038.       if (level==0) { result=TRUE; }
  2039.     }
  2040.   }
  2041.     
  2042. #ifdef X11
  2043.   x_window_creation=FALSE;
  2044. #endif
  2045.   
  2046.   Infoline(aim->a?"\n*** Yes":"\n*** No");
  2047.   show_count();
  2048.   if (aim->a || level>0) print_variables(NOTQUIET);
  2049.  
  2050.   {
  2051.     long lev=(MAX_LEVEL<level?MAX_LEVEL:level);
  2052.     pr=prompt_buffer;
  2053.     /*  RM: Oct 13 1993  */
  2054.     if(current_module==user_module)
  2055.       *pr='\0';
  2056.     else
  2057.       strcpy(pr,current_module->module_name);
  2058.     pr += strlen(pr);
  2059.     for(i=1;i<=lev;i++) { *pr='-'; pr++; *pr='-'; pr++; }
  2060.     if (level>0)
  2061.       sprintf(pr,"%ld",level);
  2062.     strcat(pr,PROMPT);
  2063.     
  2064.     prompt=prompt_buffer;
  2065.   }
  2066.   
  2067.   stdin_cleareof();
  2068.   /* The system waits for either an input command or an X event. */
  2069.   /* An X event is treated *exactly* like an input command that  */
  2070.   /* has the same effect. */
  2071. #ifdef X11
  2072.   c=x_read_stdin_or_event(&eventflag);
  2073.   if (eventflag) {
  2074.     /* Include eventflag info in var_occurred field. */
  2075.     push_goal(what_next,TRUE,FALSE+2*TRUE,level /* +1 RM: Jun 22 1993 */);
  2076.     release_resid(xevent_existing);
  2077.     result=TRUE;
  2078.   }
  2079.   else
  2080. #else
  2081.     c=read_char();
  2082. #endif
  2083.   {
  2084.     while (c!=EOLN && c>0 && c<=32 && c!=EOF) {
  2085.       c=read_char();
  2086.     }
  2087.     if (c==EOF) {
  2088.       reset_stacks();
  2089.     }
  2090.     else if (c==EOLN) {
  2091.       cut=TRUE;
  2092.     }
  2093.     else if (c==';' || c=='.') {
  2094.       do {
  2095.         c2=read_char();
  2096.       } while (c2!=EOLN && c2!=EOF && c2>0 && c2<=32);
  2097.       if (c=='.') { /* 6.10 */
  2098.         reset_stacks();
  2099.         result=TRUE;
  2100.       }
  2101.     }
  2102.     else {
  2103.       if (level>0) push_choice_point(what_next,FALSE,FALSE,level);
  2104.   
  2105.       put_back_char(c);
  2106.       var_occurred=FALSE;
  2107.       save_undo_stack=undo_stack;
  2108.       s=stack_copy_psi_term(parse(&sort));
  2109.       
  2110.       if (s->type==eof) {
  2111.     reset_stacks();
  2112.     put_back_char(EOF);
  2113.       } else if (sort==QUERY) {
  2114.         push_goal(what_next,TRUE,var_occurred,level+1);
  2115.         push_goal(prove,s,DEFRULES,NULL);
  2116.         reset_step();
  2117.         result=TRUE;
  2118.       }
  2119.       else if (sort==FACT) { /* A declaration */
  2120.         push_goal(what_next,TRUE,FALSE,level+1); /* 18.5 */
  2121.         assert_first=FALSE;
  2122.         assert_clause(s);
  2123.         /* Variables in the query may be used in a declaration, */
  2124.         /* but the declaration may not add any variables. */
  2125.     undo(save_undo_stack); /* 17.8 */
  2126.     encode_types();
  2127.     result=TRUE;
  2128.       }
  2129.       else {
  2130.     /* Stay at same level on syntax error */
  2131.         push_goal(what_next,TRUE,FALSE,level+1); /* 20.8 */
  2132.     result=TRUE; /* 20.8 */
  2133.       }
  2134.     }
  2135.   }
  2136.  
  2137.   if (cut) result = what_next_cut() || result;
  2138.   
  2139.   end_terminal_io();
  2140.   
  2141.   var_occurred=FALSE;
  2142.   start_chrono();
  2143.   
  2144.   return result;
  2145. }
  2146.  
  2147.  
  2148.  
  2149. /******** LOAD_AIM()
  2150.   Continue loading a file from the current psi-term up to the next query.
  2151.   Files are loaded in blocks of assertions that end with a query.
  2152.   Such a chunk is loaded by a 'load' goal on the goal_stack.
  2153.   This goal contains the input file state information.  This guarantees that
  2154.   all queries in the input file are executed in the order they are encountered
  2155.   (which includes load operations).
  2156. */
  2157. long load_aim()
  2158. {
  2159.   long success=TRUE,exitloop;
  2160.   ptr_psi_term s;
  2161.   long sort;
  2162.   char *fn;
  2163.   long old_noisy,old_file_date;
  2164.   ptr_node old_var_tree;
  2165.   ptr_choice_point cutpt;
  2166.   long old_var_occurred; /* 18.8 */
  2167.   int end_of_file=FALSE; /*  RM: Jan 27 1993  */
  2168.  
  2169.   
  2170.   save_state(input_state);
  2171.   input_state=(ptr_psi_term)aim->a;
  2172.   restore_state(input_state);
  2173.   old_file_date=file_date;
  2174.   file_date=(unsigned long)aim->b;
  2175.   old_noisy=noisy;
  2176.   noisy=FALSE;
  2177.   fn=(char*)aim->c;
  2178.   exitloop=FALSE;
  2179.  
  2180.  
  2181.   
  2182.   do {
  2183.     /* Variables in queries in files are *completely independent* of top- */
  2184.     /* level variables.  I.e.: top-level variables are *not* recognized   */
  2185.     /* while loading files and variables in file queries are *not* added. */
  2186.     old_var_occurred=var_occurred; /* 18.8 */
  2187.     old_var_tree=var_tree;
  2188.     var_tree=NULL;
  2189.     s=stack_copy_psi_term(parse(&sort));
  2190.     var_tree=old_var_tree;
  2191.     var_occurred=old_var_occurred; /* 18.8 */
  2192.  
  2193.     if (s->type==eof) {
  2194.       encode_types();
  2195.       if (input_stream!=stdin) fclose(input_stream);
  2196.       exitloop=TRUE;
  2197.       end_of_file=TRUE; /*  RM: Jan 27 1993  */
  2198.     }
  2199.     else if (sort==FACT) {
  2200.       assert_first=FALSE;
  2201.       assert_clause(s);
  2202.     }
  2203.     else if (sort==QUERY) {
  2204.       encode_types();
  2205.       save_state(input_state);
  2206.       /* Handle both successful and failing queries correctly. */
  2207.       cutpt=choice_stack;
  2208.       push_choice_point(load,input_state,file_date,fn);
  2209.       push_goal(load,input_state,file_date,fn);
  2210.       push_goal(general_cut,cutpt,NULL,NULL);
  2211.       push_goal(prove,s,DEFRULES,NULL);
  2212.       exitloop=TRUE;
  2213.     }
  2214.     else {
  2215.       /* fprintf(stderr,"*** Error: in input file %c%s%c.\n",34,fn,34); */
  2216.       /* success=FALSE; */
  2217.       /* fail_all(); */
  2218.       if (input_stream!=stdin) fclose(input_stream);
  2219.       abort_life(TRUE);
  2220.       /* printf("\n*** Abort\n"); */
  2221.       /* main_loop_ok=FALSE; */
  2222.     }
  2223.   } while (success && !exitloop);
  2224.  
  2225.  
  2226.   /*  RM: Jan 27 1993 */
  2227.   if(end_of_file || !success) {
  2228.     /*
  2229.       printf("END OF FILE %s, setting module to %s\n",
  2230.       ((ptr_psi_term)get_attr(input_state,
  2231.       INPUT_FILE_NAME))->value,
  2232.       ((ptr_psi_term)get_attr(input_state,
  2233.       CURRENT_MODULE))->value);
  2234.       */
  2235.        
  2236.     set_current_module(
  2237.        find_module(((ptr_psi_term)get_attr(input_state,
  2238.        CURRENT_MODULE))->value));
  2239.   }
  2240.  
  2241.   
  2242.   noisy=old_noisy;
  2243.   file_date=old_file_date;
  2244.   open_input_file("stdin");
  2245.  
  2246.   
  2247.   return success;
  2248. }
  2249.  
  2250.  
  2251.  
  2252. /******** MAIN_PROVE()
  2253.   This is the inference engine.  It distributes sub-goals to the appropriate
  2254.   routines.  It deals with backtracking.  It fails if there is not enough
  2255.   memory available or if there is an interrupt that causes the current query
  2256.   to be aborted. 
  2257. */
  2258. void main_prove()
  2259. {
  2260.   long success=TRUE;
  2261.   ptr_pair_list *p;
  2262.   ptr_psi_term unused_match_date; /* 13.6 */
  2263.     
  2264.   xcount=0;
  2265.   xeventdelay=XEVENTDELAY;
  2266.   interrupted=FALSE;
  2267.   main_loop_ok=TRUE;
  2268.   
  2269.   while (main_loop_ok && goal_stack) {
  2270.  
  2271.     /*  RM: Oct 28 1993  For debugging a horrible mess.
  2272.     { 
  2273.       ptr_choice_point c=choice_stack;
  2274.       while(c) {
  2275.     if((GENERIC)stack_pointer<(GENERIC)c) {
  2276.       printf("########### Choice stack corrupted! %x\n",c);
  2277.       trace=TRUE;
  2278.       c=NULL;
  2279.     }
  2280.     else
  2281.       c=c->next;
  2282.       }
  2283.     }
  2284.     */
  2285.  
  2286.     
  2287.     aim=goal_stack;
  2288.     switch(aim->type) {
  2289.       
  2290.     case unify:
  2291.       goal_stack=aim->next;
  2292.       goal_count++;
  2293.       success=unify_aim();
  2294.       break;
  2295.       
  2296.     /* Same as above, but do not evaluate top level */
  2297.     /* Used to bind with unbound variables */
  2298.     case unify_noeval:
  2299.       goal_stack=aim->next;
  2300.       goal_count++;
  2301.       success=unify_aim_noeval();
  2302.       break;
  2303.       
  2304.     case prove:
  2305.       success=prove_aim();
  2306.       break;
  2307.       
  2308.     case eval:
  2309.       goal_stack=aim->next;
  2310.       goal_count++;
  2311.       success=eval_aim();
  2312.       break;
  2313.  
  2314.     case load:
  2315.       goal_stack=aim->next;
  2316.       goal_count++;
  2317.       success=load_aim();
  2318.       break;
  2319.       
  2320.     case match:
  2321.       goal_stack=aim->next;
  2322.       goal_count++;
  2323.       success=match_aim();
  2324.       break;
  2325.       
  2326.     case disj:
  2327.       goal_stack=aim->next;
  2328.       goal_count++;
  2329.       success=disjunct_aim();
  2330.       break;
  2331.  
  2332.     case general_cut:
  2333.       goal_stack=aim->next;
  2334.       goal_count++;
  2335.       /* assert((ptr_choice_point)aim->a <= choice_stack); 12.7 */
  2336.       /* choice_stack=(ptr_choice_point)aim->a; */
  2337.       cut_to(aim->a); /* 12.7 */
  2338. #ifdef CLEAN_TRAIL
  2339.       clean_trail(choice_stack);
  2340. #endif
  2341. #ifdef TS
  2342.       /* RESTORE_TIME_STAMP; */ /* 9.6 */
  2343. #endif
  2344.       break;
  2345.       
  2346.     case eval_cut:
  2347.       /* RESID */ restore_resid((ptr_resid_block)aim->c, &unused_match_date);
  2348.       if (curried)
  2349.     do_currying();
  2350.       else if (resid_vars) {
  2351.     success=do_residuation_user(); /* 21.9 */ /* PVR 9.2.94 */
  2352.       } else {
  2353.         if (resid_aim)
  2354.           Traceline("result of %P is %P\n", resid_aim->a, aim->a);
  2355.         goal_stack=aim->next;
  2356.         goal_count++;
  2357.         /* resid_aim=NULL; 21.9 */
  2358.         /* PVR 5.11 choice_stack=(ptr_choice_point)aim->b; */
  2359.         i_check_out(aim->a);
  2360.       }
  2361.       resid_aim=NULL; /* 21.9 */
  2362.       resid_vars=NULL; /* 22.9 */
  2363.       /* assert((ptr_choice_point)aim->b<=choice_stack); 12.7 */
  2364.       /* PVR 5.11 */ /* choice_stack=(ptr_choice_point)aim->b; */
  2365.       if (success) { /* 21.9 */
  2366.         cut_to(aim->b); /* 12.7 */
  2367. #ifdef CLEAN_TRAIL
  2368.         clean_trail(choice_stack);
  2369. #endif
  2370.         /* match_date=NULL; */ /* 13.6 */
  2371. #ifdef TS
  2372.         /* RESTORE_TIME_STAMP; */ /* 9.6 */
  2373. #endif
  2374.       }
  2375.       break;
  2376.       
  2377.     case freeze_cut:
  2378.       /* RESID */ restore_resid((ptr_resid_block)aim->c, &unused_match_date);
  2379.       if (curried) {
  2380.         Warningline("frozen goal has a missing parameter '%P' and fails.\n",aim->a);
  2381.     success=FALSE;
  2382.       }
  2383.       else if (resid_vars) {
  2384.     success=do_residuation_user(); /* 21.9 */ /* PVR 9.2.94 */
  2385.       } else {
  2386.         if (resid_aim) Traceline("releasing frozen goal: %P\n", aim->a);
  2387.     /* resid_aim=NULL; 21.9 */
  2388.     /* PVR 5.12 choice_stack=(ptr_choice_point)aim->b; */
  2389.     goal_stack=aim->next;
  2390.     goal_count++;
  2391.       }
  2392.       resid_aim=NULL; /* 21.9 */
  2393.       resid_vars=NULL; /* 22.9 */
  2394.       if (success) { /* 21.9 */
  2395.         /* assert((ptr_choice_point)aim->b<=choice_stack); 12.7 */
  2396.         /* PVR 5.12 */ /* choice_stack=(ptr_choice_point)aim->b; */
  2397.         cut_to(aim->b); /* 12.7 */
  2398. #ifdef CLEAN_TRAIL
  2399.         clean_trail(choice_stack);
  2400. #endif
  2401.         /* match_date=NULL; */ /* 13.6 */
  2402. #ifdef TS
  2403.         /* RESTORE_TIME_STAMP; */ /* 9.6 */
  2404. #endif
  2405.       }
  2406.       break;
  2407.       
  2408.     case implies_cut: /* 12.10 */
  2409.       /* This 'cut' is actually more like a no-op! */
  2410.       restore_resid((ptr_resid_block)aim->c, &unused_match_date);
  2411.       if (curried) {
  2412.         Warningline("implied goal has a missing parameter '%P' and fails.\n",aim->a);
  2413.     success=FALSE;
  2414.       }
  2415.       else if (resid_vars)
  2416.     success=FALSE;
  2417.       else {
  2418.         if (resid_aim) Traceline("executing implied goal: %P\n", aim->a);
  2419.     goal_stack=aim->next;
  2420.     goal_count++;
  2421.       }
  2422.       resid_aim=NULL; /* 21.9 */
  2423.       resid_vars=NULL; /* 22.9 */
  2424.       break;
  2425.  
  2426.     case fail:
  2427.       goal_stack=aim->next;
  2428.       success=FALSE;
  2429.       break;
  2430.       
  2431.     case what_next:
  2432.       goal_stack=aim->next;
  2433.       success=what_next_aim();
  2434.       break;
  2435.       
  2436.     case type_disj:
  2437.       goal_stack=aim->next;
  2438.       goal_count++;
  2439.       type_disj_aim();
  2440.       break;
  2441.       
  2442.     case clause:
  2443.       goal_stack=aim->next;
  2444.       goal_count++;
  2445.       success=clause_aim(0);
  2446.       break;
  2447.       
  2448.     case del_clause:
  2449.       goal_stack=aim->next;
  2450.       goal_count++;
  2451.       success=clause_aim(1);
  2452.       break;
  2453.       
  2454.     case retract:
  2455.       goal_stack=aim->next;
  2456.       goal_count++;
  2457.       p=(ptr_pair_list*)aim->a;
  2458.       Traceline("deleting clause (%P%s%P)\n",
  2459.                 (*p)->a,((*p)->a->type->type==function?"->":":-"),(*p)->b);
  2460.       (*p)->a=NULL;
  2461.       (*p)->b=NULL;
  2462.       (*p)=(*p)->next; /* Remove retracted element from pairlist */
  2463.       break;
  2464.  
  2465.     case c_what_next: /*  RM: Mar 31 1993  */
  2466.       main_loop_ok=FALSE; /* Exit the main loop */
  2467.       break;
  2468.       
  2469.     default:
  2470.       Errorline("bad goal on stack %d.\n",goal_stack->type);
  2471.       goal_stack=aim->next;
  2472.     }
  2473.  
  2474.     if (main_loop_ok) {
  2475.     
  2476.       if (success) {
  2477.  
  2478. #ifdef X11
  2479.     /* Polling on external events */
  2480.     if (xcount<=0 && aim->type==prove) {
  2481.       if (x_exist_event()) {
  2482.         /* printf("At event, xeventdelay = %ld.\n",xeventdelay); */
  2483.         xeventdelay=0;
  2484.         release_resid(xevent_existing);
  2485.       } else {
  2486.         if (xeventdelay<XEVENTDELAY)
  2487.           /* If XEVENTDELAY=1000 it takes 90000 goals to get back */
  2488.           /* from 100 at the pace of 1%. */
  2489.           xeventdelay=(xeventdelay*101)/100+2;
  2490.         else
  2491.           xeventdelay=XEVENTDELAY;
  2492.       }
  2493.       xcount=xeventdelay;
  2494.     }
  2495.     else
  2496.       xcount--;
  2497. #endif
  2498.     
  2499.       }
  2500.       else {
  2501.         if (choice_stack) {
  2502.       backtrack();
  2503.           Traceline("backtracking\n");
  2504.       success=TRUE;
  2505.         }
  2506.         else /* if (goal_stack) */ {
  2507.           undo(NULL); /* 8.10 */
  2508.       Infoline("\n*** No");
  2509.       /* printf("\n*** No (in main_prove)."); */
  2510.           show_count();
  2511. #ifdef TS
  2512.       /* global_time_stamp=INIT_TIME_STAMP; */ /* 9.6 */
  2513. #endif
  2514.       main_loop_ok=FALSE;
  2515.         }
  2516.       }
  2517.       
  2518.       if (heap_pointer-stack_pointer < GC_THRESHOLD)
  2519.         memory_check();
  2520.       
  2521.       if (interrupted || (stepflag && steptrace))
  2522.         handle_interrupt();
  2523.       else if (stepcount>0) {
  2524.         stepcount--;
  2525.         if (stepcount==0 && !stepflag) {
  2526.           stepflag=TRUE;
  2527.           handle_interrupt();
  2528.         }
  2529.       }
  2530.     }
  2531.   }
  2532. }
  2533.  
  2534.  
  2535. int dummy_printf(f,s,t)
  2536.      
  2537.      char *f, *s, *t;
  2538. {
  2539.   return strlen(f);
  2540. }
  2541.