login.c File Reference

login More...

Go to the source code of this file.

Macros
#define	CLEAN_TRAIL
#define	TRAIL_TS
#define	TRAIL_TS
#define	RESTORE_TIME_STAMP

Functions
void	get_two_args (ptr_node t, ptr_psi_term *a, ptr_psi_term *b)
	get_two_args More...
void	get_one_arg (ptr_node t, ptr_psi_term *a)
	get_one_arg More...
void	get_one_arg_addr (ptr_node t, ptr_psi_term **a)
	get_one_arg_addr More...
void	add_rule (ptr_psi_term head, ptr_psi_term body, def_type typ)
	add_rule More...
void	assert_rule (psi_term t, def_type typ)
	assert_rule More...
void	assert_clause (ptr_psi_term t)
	assert_clause More...
void	start_chrono ()
	start_chrono More...
void	push_ptr_value (type_ptr t, GENERIC *p)
	push_ptr_value More...
void	push_def_ptr_value (ptr_psi_term q, GENERIC *p)
	push_def_ptr_value More...
void	push_psi_ptr_value (ptr_psi_term q, GENERIC *p)
	push_psi_ptr_value More...
void	push_ptr_value_global (type_ptr t, GENERIC *p)
	push_ptr_value_global More...
void	push_window (long type, long disp, long wind)
	push_window More...
void	push2_ptr_value (type_ptr t, GENERIC *p, GENERIC v)
	push2_ptr_value More...
void	push_goal (goals t, ptr_psi_term aaaa_5, ptr_psi_term bbbb_5, GENERIC cccc_5)
	push_goal More...
void	push_choice_point (goals t, ptr_psi_term aaaa_6, ptr_psi_term bbbb_6, GENERIC cccc_6)
	push_choice_point More...
void	undo (ptr_stack limit)
	undo More...
void	undo_actions ()
	undo_actions More...
void	backtrack ()
	backtrack More...
static void	clean_trail (ptr_choice_point cutpt)
	clean_trail More...
void	clean_undo_window (long disp, long wind)
	clean_undo_window More...
void	merge1 (ptr_node *u, ptr_node v)
	merge1 More...
void	merge2 (ptr_node *u, ptr_node v)
	merge2 More...
void	merge3 (ptr_node *u, ptr_node v)
	merge3 More...
void	merge (ptr_node *u, ptr_node v)
	merge More...
void	merge_unify (ptr_node *u, ptr_node v)
	merge_unify More...
void	show_count ()
	show_count More...
void	fetch_def (ptr_psi_term u, long allflag)
	fetch_def More...
void	fetch_def_lazy (ptr_psi_term u, ptr_definition old1, ptr_definition old2, ptr_node old1attr, ptr_node old2attr, long old1stat, long old2stat)
	fetch_def_lazy More...
long	unify_aim ()
	unify_aim More...
long	unify_aim_noeval ()
	unify_aim_noeval More...
long	unify_body (long eval_flag)
	unify_body More...
long	disjunct_aim ()
	disjunct_aim More...
long	prove_aim ()
	prove_aim More...
void	type_disj_aim ()
	type_disj_aim More...
long	clause_aim (long r)
	clause_aim More...
long	no_choices ()
	no_choices More...
long	num_choices ()
	num_choices More...
long	num_vars (ptr_node vt)
	num_vars More...
long	what_next_cut ()
	what_next_cut More...
ptr_choice_point	topmost_what_next ()
	topmost_what_next More...
void	reset_stacks ()
	reset_stacks More...
long	what_next_aim ()
	what_next_aim More...
long	load_aim ()
	load_aim More...
void	main_prove ()
	main_prove More...
int	dummy_printf (char *f, char *s, char *t)
	dummy_printf More...
long	trail_condition (psi_term *Q)
	trail_condition More...

Variables
long	clean_iter = 0
long	clean_succ = 0
unsigned long	global_time_stamp =INIT_TIME_STAMP

Detailed Description

login

What follows are the functions which assert facts in their correct places: function definitions, rule definitions or type definitions.

Definition in file login.c.

Macro Definition Documentation

#define CLEAN_TRAIL

Definition at line 19 of file login.c.

#define RESTORE_TIME_STAMP

Value:

global_time_stamp=\
choice_stack?choice_stack->time_stamp:INIT_TIME_STAMP;

Definition at line 670 of file login.c.

#define TRAIL_TS

#define TRAIL_TS

Function Documentation

void add_rule	(	ptr_psi_term	head,
		ptr_psi_term	body,
		def_type	typ
	)

add_rule

Parameters

head	- ptr_psi_term head
body	- ptr_psi_term body
typ	- def_type typ

ADD_RULE(head,body,typ) The TYP argument is either 'predicate', 'function', or 'type'. For predicates or functions, insert the clause 'HEAD :- BODY' or the rule 'HEAD -> BODY' into the definition of HEAD. For types, insert HEAD as a term of type attributes and BODY as a type constraint. The global flag ASSERT_FIRST indicates whether to do the insertion at the head or the tail of the existing list.

Definition at line 167 of file login.c.

References wl_pair_list::aaaa_2, assert_first, assert_ok, wl_psi_term::attr_list, wl_pair_list::bbbb_2, clear_copy(), wl_keyword::combined_name, wl_psi_term::coref, current_module, deref_ptr, Errorline(), HEAP, HEAP_ALLOC, wl_definition::keyword, MAX_BUILT_INS, wl_module::module_name, wl_pair_list::next, NULL, predicate_it, quote_copy(), redefine(), wl_psi_term::resid, wl_definition::rule, succeed, wl_keyword::symbol, TRUE, wl_psi_term::type, wl_definition::type_def, undef_it, and wl_psi_term::value_3.

{
  psi_term succ;
  ptr_psi_term head2;
  ptr_definition def;
  ptr_pair_list p, *p2;
  
  if (!body && typ==(def_type)predicate_it) {
    succ.type=succeed;
    succ.value_3=NULL;
    succ.coref=NULL;
    succ.resid=NULL;
    succ.attr_list=NULL;
    body= ≻
  }
  
  deref_ptr(head);
  head2=head;
  
  /* assert(head->resid==NULL); 10.8 */
  /* assert(body->resid==NULL); 10.8 */
  
  if (redefine(head)) {
    
    def=head->type;
    
    if (def->type_def==(def_type)undef_it || def->type_def==typ)
      
      /*  RM: Jan 27 1993  */
      if(TRUE
     /* def->type==undef_it ||
        def->keyword->module==current_module */
     /*  RM: Feb  2 1993  Commented out */
     ) {
    if (def->rule && (unsigned long)def->rule<=MAX_BUILT_INS) {
      Errorline("the built-in %T '%s' may not be redefined.\n",
            def->type_def, def->keyword->symbol);
    }
    else {
      def->type_def=typ;
      
      /* PVR single allocation in source */
      p=HEAP_ALLOC(pair_list);
      clear_copy();
      /* p->aaaa_3=exact_copy(head2,HEAP); 24.8 25.8 */
      /* p->bbbb_3=exact_copy(body,HEAP); 24.8 25.8 */
      
      p->aaaa_2=quote_copy(head2,HEAP); /* 24.8 25.8 */
      p->bbbb_2=quote_copy(body,HEAP); /* 24.8 25.8 */
      
      if (assert_first) {
        p->next=def->rule;
        def->rule=p;
      }
      else {
        p->next=NULL;
        p2= &(def->rule);
        while (*p2) {
          p2= &((*p2)->next);
        }
        *p2=p;
      }
      assert_ok=TRUE;
    }
      }
      else { /*  RM: Jan 27 1993  */
    Errorline("the %T '%s' may not be redefined from within module %s.\n",
          def->type_def,
          def->keyword->combined_name,
          current_module->module_name);
      }
    else {
      Errorline("the %T '%s' may not be redefined as a %T.\n",
                def->type_def, def->keyword->symbol, typ);
    }
  }
}

void assert_clause

(

ptr_psi_term

t

)

assert_clause

Parameters

t	- ptr_psi_term t

ASSERT_CLAUSE(t) Assert the clause T. Cope with various syntaxes for predicates.

ASSERT_FIRST is a flag indicating the position: 1= insert before existing rules (asserta), 0= insert after existing rules (assert),

Definition at line 287 of file login.c.

References add_rule(), assert_attributes(), assert_complicated_type(), assert_ok, assert_rule(), deref_ptr, equ_tok, FALSE, function_it, NULL, and predicate_it.

{
  assert_ok=FALSE;  
  deref_ptr(t);
  
  /*  RM: Feb 22 1993  defined c_alias in modules.c
      if (equ_tok((*t),"alias")) {
      get_two_args(t->attr_list,&arg1,&arg2);
      if (arg1 && arg2) {
      warningline("'%s' has taken the meaning of '%s'.\n",
      arg2->type->keyword->symbol, arg1->type->keyword->symbol);
      str=arg2->type->keyword->symbol;
      assert_ok=TRUE;
      deref_ptr(arg1);
      deref_ptr(arg2);
      *(arg2->type)= *(arg1->type);
      arg2->type->keyword->symbol=str;
      }
      else
      Errorline("arguments missing in %P.\n",t);
      }
      else
      */
  
  if (equ_tok((*t),":-"))
    assert_rule((*t),(def_type)predicate_it);
  else
    if (equ_tok((*t),"->"))
      assert_rule((*t),(def_type)function_it);
    else
      if (equ_tok((*t),"::"))
    assert_attributes(t);
      else
    
#ifdef CLIFE
    if (equ_tok((*t),"block_struct"))
      define_block(t);
    else
#endif /* CLIFE */
      /* if (equ_tok((*t),"<<<-")) {   RM: Feb 10 1993
         declare T as global. To do... maybe.
         }
         else
         */
      
      if (equ_tok((*t),"<|") || equ_tok((*t),":="))
        assert_complicated_type(t);
      else
        add_rule(t,NULL,(def_type)predicate_it);
  
  /* if (!assert_ok && warning()) perr("the declaration is ignored.\n"); */
}

void assert_rule	(	psi_term	t,
		def_type	typ
	)

assert_rule

Parameters

t	- psi_term t
typ	- def_type typ

ASSERT_RULE(t,typ) Add a rule to the rule tree. It may be either a predicate or a function. The psi_term T is of the form 'H :- B' or 'H -> B', but it may be incorrect (report errors). TYP is the type, function or predicate.

Definition at line 257 of file login.c.

References add_rule(), wl_psi_term::attr_list, get_two_args(), and Syntaxerrorline().

{
  ptr_psi_term head;
  ptr_psi_term body;
  
  get_two_args(t.attr_list,&head,&body);
  if (head)
    if (body)
      add_rule(head,body,typ);
    else {
      Syntaxerrorline("body missing in definition of %T '%P'.\n", typ, head);
    }
  else {
    Syntaxerrorline("head missing in definition of %T.\n",typ);
  }
}

void backtrack

(

)

backtrack

BACKTRACK() Undo everything back to the previous choice-point and take the alternative decision. This routine would have to be modified, along with UNDO to cope with goals to be proved on backtracking.

Definition at line 772 of file login.c.

References choice_stack, wl_choice_point::goal_stack, goal_stack, wl_choice_point::next, NULL, resid_aim, stack_pointer, wl_choice_point::stack_top, undo(), and wl_choice_point::undo_point.

{
  //  long gts;
  
  goal_stack=choice_stack->goal_stack;
  undo(choice_stack->undo_point);
#ifdef TS
  /* global_time_stamp=choice_stack->time_stamp; */ /* 9.6 */
#endif
  stack_pointer=choice_stack->stack_top;
  choice_stack=choice_stack->next;
  resid_aim=NULL;
  
  
  /* assert((unsigned long)stack_pointer>=(unsigned long)cut_point); 13.6 */
  /* This situation occurs frequently in some benchmarks (e.g comb) */
  /* printf("*** Possible GC error: cut_point is dangling\n"); */
  /* fflush(stdout); */
  
  /* assert((unsigned long)stack_pointer>=(unsigned long)match_date); 13.6 */
}

long clause_aim

(

long

r

)

clause_aim

Parameters

r

- long r

CLAUSE_AIM(r) Prove a CLAUSE or RETRACT goal. That is try to unify the calling argument with the current rule. If this succeeds and R=TRUE then delete the rule (RETRACT).

Definition at line 1879 of file login.c.

References wl_goal::aaaa_1, aim, wl_psi_term::attr_list, wl_goal::bbbb_1, wl_goal::cccc_1, clause, clear_copy(), del_clause, Errorline(), FALSE, i_eval_args(), wl_definition::keyword, MAX_BUILT_INS, NULL, push_choice_point(), push_goal(), quote_copy(), retract, STACK, wl_psi_term::status, wl_keyword::symbol, traceline(), TRUE, wl_psi_term::type, and unify.

{
  long success=FALSE;
  ptr_pair_list *p;
  ptr_psi_term head,body,rule_head,rule_body;
  
  head=(ptr_psi_term)aim->aaaa_1;
  body=(ptr_psi_term)aim->bbbb_1;
  p=(ptr_pair_list *)aim->cccc_1;
  
  if ((unsigned long)(*p)>MAX_BUILT_INS) {
    success=TRUE;
    /* deref(head); 17.9 */
    
    if ((*p)->next) {
      if (r) {
        traceline("pushing 'retract' choice point for %P\n", head);
    push_choice_point(del_clause,head,(ptr_psi_term)body,(GENERIC)&((*p)->next));
    /* push_choice_point(del_clause,head,body,p); */
      }
      else {
        traceline("pushing 'clause' choice point for %P\n", head);
    push_choice_point(clause,head,(ptr_psi_term)body,(GENERIC)&((*p)->next));
      }
    }
    
    if (r)
      push_goal(retract,(ptr_psi_term)p,(ptr_psi_term)NULL,NULL);
    if ((*p)->aaaa_2) {
      clear_copy();
      rule_head=quote_copy((*p)->aaaa_2,STACK);
      rule_body=quote_copy((*p)->bbbb_2,STACK);
      
      push_goal(unify,(ptr_psi_term)body,(ptr_psi_term)rule_body,NULL);
      push_goal(unify,(ptr_psi_term)head,(ptr_psi_term)rule_head,NULL);
      
      rule_head->status=4;
      rule_body->status=4;
      
      (void)i_eval_args(rule_body->attr_list);
      (void)i_eval_args(rule_head->attr_list);
      
      traceline("fetching next clause for %s\n", head->type->keyword->symbol);
    }
    else {
      success=FALSE;
      traceline("following clause had been retracted\n");
    }
  }
  else if ((unsigned long)(*p)>0) {
    if (r)
      Errorline("the built-in %P cannot be retracted.\n",head);
    else
      Errorline("the definition of built-in %P is not accessible.\n",head);
  }
  
  return success;
}

static void clean_trail ( ptr_choice_point  cutpt )

static

clean_trail

Parameters

cutpt

- ptr_choice_point cutpt

CLEAN_TRAIL(cutpt) This routine removes all trail entries between the top of the undo_stack and the cutpt, whose addresses are between the cutpt and stack_pointer. (The cutpt is the choice point that will become the most recent one after the cut.) This routine should be called when a cut built-in is done. This routine is careful not to remove any trailed entries that are on the heap or outside of Life space.

Definition at line 810 of file login.c.

References wl_stack::aaaa_3, clean_iter, clean_succ, mem_base, wl_stack::next, NULL, stack_pointer, wl_choice_point::stack_top, wl_stack::type, undo_action, wl_choice_point::undo_point, undo_stack, and VALID_RANGE.

{
  ptr_stack *prev,u,cut_limit;
  GENERIC cut_sp;
  
  u = undo_stack;
  prev = &undo_stack;
  if (cutpt) {
    cut_sp = cutpt->stack_top;
    cut_limit = cutpt->undo_point;
  }
  else {
    cut_sp = mem_base; /* Empty stack */
    cut_limit = NULL;  /* Empty undo_stack */
  }
  
  while ((unsigned long)u > (unsigned long)cut_limit) {
    clean_iter++;
    if (!(u->type & undo_action) && VALID_RANGE(u->aaaa_3) &&
        (unsigned long)u->aaaa_3>(unsigned long)cut_sp && (unsigned long)u->aaaa_3<=(unsigned long)stack_pointer) {
      *prev = u->next;
      clean_succ++;
    }
    prev = &(u->next);
    u = u->next;
  }
}

void clean_undo_window	(	long	disp,
		long	wind
	)

clean_undo_window

Parameters

disp	- long disp
wind	- long wind

CLEAN_UNDO_WINDOW(disp,wind) Remove all trail entries that reference a given window. This is called when the window is destroyed.

Definition at line 848 of file login.c.

References wl_stack::aaaa_3, wl_stack::bbbb_3, choice_stack, wl_stack::next, wl_choice_point::next, wl_stack::type, undo_action, wl_choice_point::undo_point, and undo_stack.

{
  ptr_stack *prev,u;
  ptr_choice_point c;
  
#ifdef X11
  /* Remove entries on the trail */
  u = undo_stack;
  prev = &undo_stack;
  while (u) {
    if ((u->type & undo_action) &&
        ((unsigned long)u->aaaa_3==disp) && ((unsigned long)u->bbbb_3==wind)) {
      *prev = u->next;
    }
    prev = &(u->next);
    u = u->next;
  }
  
  /* Remove entries at the *tops* of trail entry points from the   */
  /* choice point stack.  It's only necessary to look at the tops, */
  /* since those are the only ones that haven't been touched by    */
  /* the previous while loop. */
  c = choice_stack;
  while (c) {
    u = c->undo_point;
    prev = &(c->undo_point);
    while (u && (u->type & undo_action) &&
           ((unsigned long)u->aaaa_3==disp) && ((unsigned long)u->bbbb_3==wind)) {
      *prev = u->next;
      prev = &(u->next);
      u = u->next;
    }
    c = c->next;
  }
#endif
}

long disjunct_aim

(

)

disjunct_aim

DISJUNCT_AIM() This is the disjunction enumeration routine. If U is the disjunction {H|T} then first bind U to H, then on backtracking enumerate the disjunction T. U is always passed along so that every choice of the disjunction can be bound to U.

Definition at line 1621 of file login.c.

References TRUE.

{
  //  ptr_psi_term u,v;
  //  ptr_list l;
  long success=TRUE;
  
  printf("Call to disjunct_aim\nThis routine inhibited by RM: Dec  9 1992\n");
  
  return success;
}

int dummy_printf	(	char *	f,
		char *	s,
		char *	t
	)

dummy_printf

Parameters

f	- char *f
s	- char *s
t	- char *t

Definition at line 2617 of file login.c.

{
  return strlen(f);
}

void fetch_def	(	ptr_psi_term	u,
		long	allflag
	)

fetch_def

Parameters

u	- ptr_psi_term u
allflag	- long allflag

FETCH_DEF(psi_term) Fetch the type definition of a psi_term and execute it. That is, get the list of (term,predicate) pairs that define the type. Unify the psi_term with the term, then prove the predicate.

This routine only gets the pairs that are defined in the type itself, not those defined in any types above it. This is the correct behavior for enumerating type disjunctions–all higher constraints have already been checked.

The above is true if allflag==FALSE. If allflag==TRUE then all constraints are executed, not just those defined in the type itself.

Definition at line 1208 of file login.c.

References wl_triple_list::aaaa_4, wl_psi_term::attr_list, wl_triple_list::bbbb_4, wl_triple_list::cccc_4, clear_copy(), DEFRULES, deref_ptr, eval_copy(), i_eval_args(), int_ptr, wl_triple_list::next, NULL, wl_definition::properties, prove, push2_ptr_value(), push_goal(), RMASK, SMASK, STACK, wl_psi_term::status, traceline(), wl_psi_term::type, and unify.

{
  ptr_triple_list prop;
  ptr_psi_term v,w;
  ptr_definition utype;
  
  /* Uses SMASK because called from check_out */
  push2_ptr_value(int_ptr,(GENERIC *)&(u->status),(GENERIC)(u->status & SMASK));
  u->status=(4 & SMASK) | (u->status & RMASK);
  
  utype=u->type;
  prop=u->type->properties;
  if (prop) {
    
    traceline("fetching definition of %P\n",u);
    
    while (prop) {
      if (allflag || prop->cccc_4==utype) {
        clear_copy();
        v=eval_copy(prop->aaaa_4,STACK);
        w=eval_copy(prop->bbbb_4,STACK);
        
        if (w) push_goal(prove,(ptr_psi_term)w,(ptr_psi_term)DEFRULES,NULL);
        
        deref_ptr(v);
        v->status=4;
        push_goal(unify,(ptr_psi_term)u,(ptr_psi_term)v,NULL);
        (void)i_eval_args(v->attr_list);
      }
      prop=prop->next;
    }
  }
}

void fetch_def_lazy	(	ptr_psi_term	u,
		ptr_definition	old1,
		ptr_definition	old2,
		ptr_node	old1attr,
		ptr_node	old2attr,
		long	old1stat,
		long	old2stat
	)

fetch_def_lazy

Parameters

u	-ptr_psi_term u
old1	- ptr_definition old1
old2	- ptr_definition old2
old1attr	- ptr_node old1attr
old2attr	- ptr_node old2attr
old1stat	- long old1stat
old2stat	- long old2stat

FETCH_DEF_LAZY(psi_term,type1,type2,attr_list1,attr_list2) Fetch the type definition of a psi_term and execute it. That is, get the list of (term,pred) pairs that define the type. 'Term' is one of the type's attributes and 'pred' is a constraint. Unify the psi_term with the term, then prove pred.

Only those (term,pred) pairs are executed whose original type is below both type1 and type2, the types of the two psi-terms whose unification created psi_term. This avoids doing much superfluous work.

The above behavior is correct for a psi_term when always_check==TRUE for that psi_term. If always_check==FALSE for a psi_term, then if it does not have attributes it is not checked, and the addition of an attribute will force checking to occur.

Example:

:: t(a=>one,b=>two,c=> X) | thing(X).

psi_term = A:t (it can be any psi_term of type t) term = t(a=>one,b=>two,c=> X) pred = thing(X)

Definition at line 1276 of file login.c.

References wl_triple_list::aaaa_4, wl_definition::always_check, wl_psi_term::attr_list, wl_triple_list::bbbb_4, wl_triple_list::cccc_4, clear_copy(), DEFRULES, deref_ptr, eval_copy(), FALSE, i_eval_args(), int_ptr, matches(), wl_triple_list::next, NULL, wl_definition::properties, prove, push_goal(), push_ptr_value(), STACK, wl_psi_term::status, traceline(), wl_psi_term::type, and unify.

{
  ptr_triple_list prop;
  ptr_psi_term v,w;
  long checked1, checked2;
  long m1, m2;
  
  if (!u->type->always_check) if (u->attr_list==NULL) return;
  
  push_ptr_value(int_ptr,(GENERIC *)&(u->status));
  u->status=4;
  
  prop=u->type->properties;
  if (prop) {
    traceline("fetching partial definition of %P\n",u);
    
    checked1 = old1attr || old1->always_check;
    checked2 = old2attr || old2->always_check;

    /* checked1 = (old1stat==4); */ /* 18.2.94 */
    /* checked2 = (old2stat==4); */
    
    while (prop) {
      /* Only do those constraints that have not yet been done: */
      /* In matches, mi is TRUE iff oldi <| prop->cccc_1.            */
      if (!checked1) m1=FALSE; else (void)matches(old1,prop->cccc_4,&m1);
      if (!checked2) m2=FALSE; else (void)matches(old2,prop->cccc_4,&m2);
      if (!m1 && !m2) {
    /* At this point, prop->cccc_1 is an attribute that has not yet */
    /* been checked. */
    clear_copy();
    v=eval_copy(prop->aaaa_4,STACK);
    w=eval_copy(prop->bbbb_4,STACK);
    
    if (w) push_goal(prove,(ptr_psi_term)w,(ptr_psi_term)DEFRULES,NULL);
    
    deref_ptr(v);
    v->status=4;
    push_goal(unify,(ptr_psi_term)u,(ptr_psi_term)v,NULL);
    (void)i_eval_args(v->attr_list);
      }
      prop=prop->next;
    }
  }
}

void get_one_arg	(	ptr_node	t,
		ptr_psi_term *	a
	)

get_one_arg

Parameters

t	- ptr_node t
a	- ptr_psi_term *a

GET_ONE_ARG(attr_list,arg1) Get the argument labelled '1' as quickly as possible from the binary tree ATTR_LIST, place it in ARG1. This routine nearly always makes a direct hit.

Definition at line 99 of file login.c.

References wl_node::data, FEATCMP, find(), wl_node::key, NULL, and one.

{
  ptr_node n;
  
  *a=NULL;
  if (t) {
    if (t->key==one) {
      *a=(ptr_psi_term)t->data;
    }
    else {
      n=find(FEATCMP,one,t);
      if (n==NULL)
    *a=NULL;
      else
    *a=(ptr_psi_term)n->data;
    }
  }
}

void get_one_arg_addr	(	ptr_node	t,
		ptr_psi_term **	a
	)

get_one_arg_addr

Parameters

t	- ptr_node t
a	- ptr_psi_term **a

GET_ONE_ARG_ADDR(attr_list,arg1addr) Get address of slot in the attr_list that points to the argument labelled '1' as quickly as possible from the binary tree ATTR_LIST. This routine nearly always makes a direct hit.

Definition at line 132 of file login.c.

References wl_node::data, FEATCMP, find(), wl_node::key, NULL, and one.

{
  ptr_node n;
  //  ptr_psi_term *b;
  
  *a=NULL;
  if (t) {
    if (t->key==one)
      *a= (ptr_psi_term *)(&t->data);
    else {
      n=find(FEATCMP,one,t);
      if (n==NULL)
    *a=NULL;
      else
    *a= (ptr_psi_term *)(&n->data);
    }
  }
}

void get_two_args	(	ptr_node	t,
		ptr_psi_term *	a,
		ptr_psi_term *	b
	)

get_two_args

Parameters

t	- ptr_node t,
a	- ptr_psi_term *a
b	- ptr_psi_term *b

GET_TWO_ARGS(attr_list,arg1,arg2) Get the arguments labelled '1' and '2' as quickly as possible from the binary tree ATTR_LIST, place them in ARG1 and ARG2. This routine nearly always makes a direct hit.

Definition at line 47 of file login.c.

References wl_node::data, FEATCMP, find(), wl_node::key, NULL, one, wl_node::right, and two.

{
  ptr_node n;
  
  *a=NULL;
  *b=NULL;
  if (t) {
    if (t->key==one) {
      *a=(ptr_psi_term )t->data;
      n=t->right;
      if (n) 
    if (n->key==two)
      *b=(ptr_psi_term )n->data;
    else {
      n=find(FEATCMP,two,t);
      if(n==NULL)
        *b=NULL;
      else
        *b=(ptr_psi_term )n->data;
    }
      else
    *b=NULL;
    }
    else {
      n=find(FEATCMP,one,t);
      if (n==NULL)
    *a=NULL;
      else
    *a=(ptr_psi_term )n->data;
      n=find(FEATCMP,two,t);
      if (n==NULL)
    *b=NULL;
      else
    *b=(ptr_psi_term )n->data;
    }
  }
}

long load_aim

(

)

load_aim

LOAD_AIM() Continue loading a file from the current psi-term up to the next query. Files are loaded in blocks of assertions that end with a query. Such a chunk is loaded by a 'load' goal on the goal_stack. This goal contains the input file state information. This guarantees that all queries in the input file are executed in the order they are encountered (which includes load operations).

Definition at line 2232 of file login.c.

References wl_goal::aaaa_1, abort_life(), aim, assert_clause(), assert_first, wl_goal::bbbb_1, wl_goal::cccc_1, choice_stack, CURRENT_MODULE, DEFRULES, encode_types(), eof, FACT, FALSE, file_date, find_module(), general_cut, get_attr(), input_state, input_stream, load, noisy, NULL, open_input_file(), parse(), prove, push_choice_point(), push_goal(), QUERY, restore_state(), save_state(), set_current_module(), stack_copy_psi_term(), TRUE, wl_psi_term::type, var_occurred, and var_tree.

{
  long success=TRUE,exitloop;
  ptr_psi_term s;
  long sort;
  char *fn;
  long old_noisy,old_file_date;
  ptr_node old_var_tree;
  ptr_choice_point cutpt;
  long old_var_occurred; /* 18.8 */
  int end_of_file=FALSE; /*  RM: Jan 27 1993  */

  
  save_state(input_state);
  input_state=(ptr_psi_term)aim->aaaa_1;
  restore_state(input_state);
  old_file_date=file_date;
  file_date=(unsigned long)aim->bbbb_1;
  old_noisy=noisy;
  noisy=FALSE;
  fn=(char*)aim->cccc_1;
  exitloop=FALSE;
  
  do {
    /* Variables in queries in files are *completely independent* of top- */
    /* level variables.  I.e.: top-level variables are *not* recognized   */
    /* while loading files and variables in file queries are *not* added. */
    old_var_occurred=var_occurred; /* 18.8 */
    old_var_tree=var_tree;
    var_tree=NULL;
    s=stack_copy_psi_term(parse(&sort));
    var_tree=old_var_tree;
    var_occurred=old_var_occurred; /* 18.8 */

    if (s->type==eof) {
      encode_types();
      if (input_stream!=stdin) (void)fclose(input_stream);
      exitloop=TRUE;
      end_of_file=TRUE; /*  RM: Jan 27 1993  */
    }
    else if (sort==FACT) {
      assert_first=FALSE;
      assert_clause(s);
    }
    else if (sort==QUERY) {
      encode_types();
      save_state(input_state);
      /* Handle both successful and failing queries correctly. */
      cutpt=choice_stack;
      push_choice_point(load,input_state,(ptr_psi_term)file_date,(GENERIC) fn);
      push_goal(load,(ptr_psi_term)input_state,(ptr_psi_term)file_date,(GENERIC)fn);
      push_goal(general_cut,(ptr_psi_term)cutpt,(ptr_psi_term)NULL,(GENERIC)NULL);
      push_goal(prove,(ptr_psi_term)s,(ptr_psi_term)DEFRULES,(GENERIC)NULL);
      exitloop=TRUE;
    }
    else {
      /* fprintf(stderr,"*** Error: in input file %c%s%c.\n",34,fn,34); */
      /* success=FALSE; */
      /* fail_all(); */
      if (input_stream!=stdin) (void)fclose(input_stream);
      (void)abort_life(TRUE);
      /* printf("\n*** Abort\n"); */
      /* main_loop_ok=FALSE; */
    }
  } while (success && !exitloop);


  /*  RM: Jan 27 1993 */
  if(end_of_file || !success) {
    /*
      printf("END OF FILE %s, setting module to %s\n",
      ((ptr_psi_term)get_attr(input_state,
      INPUT_FILE_NAME))->value,
      ((ptr_psi_term)get_attr(input_state,
      CURRENT_MODULE))->value);
      */
       
    (void)set_current_module(
               find_module((char *)((ptr_psi_term)get_attr(input_state,
       CURRENT_MODULE))->value_3));
  }

  
  noisy=old_noisy;
  file_date=old_file_date;
  (void)open_input_file("stdin");

  
  return success;
}

void main_prove

(

)

main_prove

MAIN_PROVE() This is the inference engine. It distributes sub-goals to the appropriate routines. It deals with backtracking. It fails if there is not enough memory available or if there is an interrupt that causes the current query to be aborted.

Definition at line 2333 of file login.c.

References wl_goal::aaaa_1, aim, backtrack(), wl_goal::bbbb_1, c_what_next, wl_goal::cccc_1, choice_stack, clause, clause_aim(), clean_trail(), curried, cut_to, del_clause, disj, disjunct_aim(), do_currying(), do_residuation_user(), Errorline(), eval, eval_aim(), eval_cut, fail, FALSE, freeze_cut, function_it, GC_THRESHOLD, general_cut, goal_count, goal_stack, handle_interrupt(), heap_pointer, i_check_out(), implies_cut, infoline(), interrupted, load, load_aim(), main_loop_ok, match, match_aim(), memory_check(), wl_goal::next, NULL, prove, prove_aim(), release_resid(), resid_aim, resid_vars, restore_resid(), retract, show_count(), stack_pointer, stepcount, stepflag, steptrace, traceline(), TRUE, wl_goal::type, type_disj, type_disj_aim(), undo(), unify, unify_aim(), unify_aim_noeval(), unify_noeval, warningline(), what_next, what_next_aim(), x_exist_event(), xcount, xevent_existing, XEVENTDELAY, and xeventdelay.

{
  long success=TRUE;
  ptr_pair_list *p;
  ptr_psi_term unused_match_date; /* 13.6 */
    
  xcount=0;
  xeventdelay=XEVENTDELAY;
  interrupted=FALSE;
  main_loop_ok=TRUE;
  
  while (main_loop_ok && goal_stack) {

    /*  RM: Oct 28 1993  For debugging a horrible mess.
    { 
      ptr_choice_point c=choice_stack;
      while(c) {
    if((ptr_psi_term)stack_pointer<(ptr_psi_term)c) {
      printf("########### Choice stack corrupted! %x\n",c);
      trace=TRUE;
      c=NULL;
    }
    else
      c=c->next;
      }
    }
    */

    
    aim=goal_stack;
    switch(aim->type) {
      
    case unify:
      goal_stack=aim->next;
      goal_count++;
      success=unify_aim();
      break;
      
    /* Same as above, but do not evaluate top level */
    /* Used to bind with unbound variables */
    case unify_noeval:
      goal_stack=aim->next;
      goal_count++;
      success=unify_aim_noeval();
      break;
      
    case prove:
      success=prove_aim();
      break;
      
    case eval:
      goal_stack=aim->next;
      goal_count++;
      success=eval_aim();
      break;

    case load:
      goal_stack=aim->next;
      goal_count++;
      success=load_aim();
      break;
      
    case match:
      goal_stack=aim->next;
      goal_count++;
      success=match_aim();
      break;
      
    case disj:
      goal_stack=aim->next;
      goal_count++;
      success=disjunct_aim();
      break;

    case general_cut:
      goal_stack=aim->next;
      goal_count++;
      /* assert((ptr_choice_point)aim->aaaa_1 <= choice_stack); 12.7 */
      /* choice_stack=(ptr_choice_point)aim->aaaa_1; */
      cut_to(aim->aaaa_1); /* 12.7 */
#ifdef CLEAN_TRAIL
      clean_trail(choice_stack);
#endif
#ifdef TS
      /* RESTORE_TIME_STAMP; */ /* 9.6 */
#endif
      break;
      
    case eval_cut:
      /* RESID */ restore_resid((ptr_resid_block)aim->cccc_1, &unused_match_date);
      if (curried)
    do_currying();
      else if (resid_vars) {
    success=do_residuation_user(); /* 21.9 */ /* PVR 9.2.94 */
      } else {
        if (resid_aim)
          traceline("result of %P is %P\n", resid_aim->aaaa_1, aim->aaaa_1);
        goal_stack=aim->next;
        goal_count++;
        /* resid_aim=NULL; 21.9 */
        /* PVR 5.11 choice_stack=(ptr_choice_point)aim->bbbb_1; */
        (void)i_check_out(aim->aaaa_1);
      }
      resid_aim=NULL; /* 21.9 */
      resid_vars=NULL; /* 22.9 */
      /* assert((ptr_choice_point)aim->bbbb_1<=choice_stack); 12.7 */
      /* PVR 5.11 */ /* choice_stack=(ptr_choice_point)aim->bbbb_1; */
      if (success) { /* 21.9 */
        cut_to(aim->bbbb_1); /* 12.7 */
#ifdef CLEAN_TRAIL
        clean_trail(choice_stack);
#endif
        /* match_date=NULL; */ /* 13.6 */
#ifdef TS
        /* RESTORE_TIME_STAMP; */ /* 9.6 */
#endif
      }
      break;
      
    case freeze_cut:
      /* RESID */ restore_resid((ptr_resid_block)aim->cccc_1, &unused_match_date);
      if (curried) {
        warningline("frozen goal has a missing parameter '%P' and fails.\n",aim->aaaa_1);
    success=FALSE;
      }
      else if (resid_vars) {
    success=do_residuation_user(); /* 21.9 */ /* PVR 9.2.94 */
      } else {
        if (resid_aim) traceline("releasing frozen goal: %P\n", aim->aaaa_1);
    /* resid_aim=NULL; 21.9 */
    /* PVR 5.12 choice_stack=(ptr_choice_point)aim->bbbb_1; */
    goal_stack=aim->next;
    goal_count++;
      }
      resid_aim=NULL; /* 21.9 */
      resid_vars=NULL; /* 22.9 */
      if (success) { /* 21.9 */
        /* assert((ptr_choice_point)aim->bbbb_1<=choice_stack); 12.7 */
        /* PVR 5.12 */ /* choice_stack=(ptr_choice_point)aim->bbbb_1; */
        cut_to(aim->bbbb_1); /* 12.7 */
#ifdef CLEAN_TRAIL
        clean_trail(choice_stack);
#endif
        /* match_date=NULL; */ /* 13.6 */
#ifdef TS
        /* RESTORE_TIME_STAMP; */ /* 9.6 */
#endif
      }
      break;
      
    case implies_cut: /* 12.10 */
      /* This 'cut' is actually more like a no-op! */
      restore_resid((ptr_resid_block)aim->cccc_1, &unused_match_date);
      if (curried) {
        warningline("implied goal has a missing parameter '%P' and fails.\n",aim->aaaa_1);
    success=FALSE;
      }
      else if (resid_vars)
    success=FALSE;
      else {
        if (resid_aim) traceline("executing implied goal: %P\n", aim->aaaa_1);
    goal_stack=aim->next;
    goal_count++;
      }
      resid_aim=NULL; /* 21.9 */
      resid_vars=NULL; /* 22.9 */
      break;

    case fail:
      goal_stack=aim->next;
      success=FALSE;
      break;
      
    case what_next:
      goal_stack=aim->next;
      success=what_next_aim();
      break;
      
    case type_disj:
      goal_stack=aim->next;
      goal_count++;
      type_disj_aim();
      break;
      
    case clause:
      goal_stack=aim->next;
      goal_count++;
      success=clause_aim(0);
      break;
      
    case del_clause:
      goal_stack=aim->next;
      goal_count++;
      success=clause_aim(1);
      break;
      
    case retract:
      goal_stack=aim->next;
      goal_count++;
      p=(ptr_pair_list*)aim->aaaa_1;
      traceline("deleting clause (%P%s%P)\n",
                (*p)->aaaa_2,((*p)->aaaa_2->type->type_def==(def_type)function_it?"->":":-"),(*p)->bbbb_2);
      (*p)->aaaa_2=NULL;
      (*p)->bbbb_2=NULL;
      (*p)=(*p)->next; /* Remove retracted element from pairlist */
      break;

    case c_what_next: /*  RM: Mar 31 1993  */
      main_loop_ok=FALSE; /* Exit the main loop */
      break;
      
    default:
      Errorline("bad goal on stack %d.\n",goal_stack->type);
      goal_stack=aim->next;
    }

    if (main_loop_ok) {
    
      if (success) {

#ifdef X11
    /* Polling on external events */
    if (xcount<=0 && aim->type==prove) {
      if (x_exist_event()) {
        /* printf("At event, xeventdelay = %ld.\n",xeventdelay); */
        xeventdelay=0;
        release_resid(xevent_existing);
      } else {
        if (xeventdelay<XEVENTDELAY)
          /* If XEVENTDELAY=1000 it takes 90000 goals to get back */
          /* from 100 at the pace of 1%. */
          xeventdelay=(xeventdelay*101)/100+2;
        else
          xeventdelay=XEVENTDELAY;
      }
      xcount=xeventdelay;
    }
    else
      xcount--;
#endif
    
      }
      else {
        if (choice_stack) {
      backtrack();
          traceline("backtracking\n");
      success=TRUE;
        }
        else /* if (goal_stack) */ {
          undo(NULL); /* 8.10 */
      infoline("\n*** No");
      /* printf("\n*** No (in main_prove)."); */
          show_count();
#ifdef TS
      /* global_time_stamp=INIT_TIME_STAMP; */ /* 9.6 */
#endif
      main_loop_ok=FALSE;
        }
      }
      
      if (heap_pointer-stack_pointer < GC_THRESHOLD)
        (void)memory_check();
      
      if (interrupted || (stepflag && steptrace))
        handle_interrupt();
      else if (stepcount>0) {
        stepcount--;
        if (stepcount==0 && !stepflag) {
          stepflag=TRUE;
          handle_interrupt();
        }
      }
    }
  }
}

void merge	(	ptr_node *	u,
		ptr_node	v
	)

merge

Parameters

u	- ptr_node *u
v	- ptr_node v

MERGE(u,v) U and V are two binary trees containing the attributes fields of psi-terms. U and V are merged together, that is U becomes the union of U and V: For each label L in V and L->Vpsi_term: If L is in U Then With L->Upsi_term Do unify(Upsi_term,Vpsi_term) Else merge L->Vpsi_term in U. Unification is simply done by appending the 2 psi_terms to the unification stack. All effects must be recorded in the trail so that they can be undone on backtracking.

Definition at line 1131 of file login.c.

References merge1(), merge2(), and merge3().

{
  merge1(u,v); /* Unify corresponding arguments */
  merge2(u,v); /* Evaluate lone arguments (lazy failure + eager success) */
  merge3(u,v); /* Merge v's loners into u & evaluate corresponding arguments */
}

void merge1	(	ptr_node *	u,
		ptr_node	v
	)

merge1

Parameters

u	- ptr_node *u
v	- ptr_node v

Unify the corresponding arguments

Definition at line 893 of file login.c.

References wl_node::data, featcmp(), wl_node::key, wl_node::left, NULL, push_goal(), wl_node::right, and unify.

{
  long cmp;
  ptr_node temp;
  
  if (v) {
    if (*u==NULL) {
      /* push_ptr_value(int_ptr,u); */
      /* (*u)=STACK_ALLOC(node); */
      /* **u= *v; */
      /* more_v_attr=TRUE; */
    }
    else {
      cmp=featcmp((*u)->key,v->key);
      if (cmp==0) {
    if (v->right)
      merge1(&((*u)->right),v->right);
    
    push_goal(unify,(ptr_psi_term)(*u)->data,(ptr_psi_term)v->data,NULL);
    
    if (v->left)
      merge1(&((*u)->left),v->left);
      }
      else if (cmp>0) {
    temp=v->right;
    v->right=NULL;
    merge1(&((*u)->left),v);
    merge1(u,temp);
    v->right=temp;
      }
      else {
        temp=v->left;
        v->left=NULL;
        merge1(&((*u)->right),v);
        merge1(u,temp);
        v->left=temp;
      }
    }
  }
  else if (*u!=NULL) {
    /* more_u_attr=TRUE; */
  }
}

void merge2	(	ptr_node *	u,
		ptr_node	v
	)

merge2

Parameters

u	- ptr_node *u
v	- ptr_node v

Evaluate the lone arguments (For LAZY failure + EAGER success) Evaluate low numbered lone arguments first. For each lone argument in either u or v, create a new psi-term to put the (useless) result: This is needed so that all arguments of a uni- unified psi-term are evaluated, which avoids incorrect 'Yes' answers.

Definition at line 949 of file login.c.

References wl_node::data, deref2_rec_eval(), featcmp(), wl_node::key, wl_node::left, NULL, and wl_node::right.

{
  long cmp;
  ptr_node temp;
  
  if (v) {
    if (*u==NULL) {
      ptr_psi_term t;
      merge2(u,v->right);
      t = (ptr_psi_term) v->data;
      deref2_rec_eval(t); /* Assumes goal_stack is already restored. */
      merge2(u,v->left);
    }
    else {
      cmp=featcmp((*u)->key,v->key);
      if (cmp==0) {
    /* if (v->right) */
    merge2(&((*u)->right),v->right);
    
    /* if (v->left) */
    merge2(&((*u)->left),v->left);
      }
      else if (cmp>0) {
    temp=v->right;
    v->right=NULL;
    merge2(&((*u)->left),v);
    merge2(u,temp);
    v->right=temp;
      }
      else {
        temp=v->left;
        v->left=NULL;
        merge2(&((*u)->right),v);
        merge2(u,temp);
        v->left=temp;
      }
    }
  }
  else if (*u!=NULL) {
    ptr_psi_term t;
    merge2(&((*u)->right),v);
    t = (ptr_psi_term) (*u)->data;
    deref2_rec_eval(t); /* Assumes goal_stack is already restored. */
    merge2(&((*u)->left),v);
  }
}

void merge3	(	ptr_node *	u,
		ptr_node	v
	)

merge3

Parameters

u	- ptr_node *u
v	- ptr_node v

Merge v's loners into u and evaluate the corresponding arguments

Definition at line 1004 of file login.c.

References deref2_eval(), featcmp(), int_ptr, wl_node::key, wl_node::left, more_u_attr, more_v_attr, NULL, push_ptr_value(), wl_node::right, STACK_ALLOC, and TRUE.

{
  long cmp;
  ptr_node temp;
  
  if (v) {
    if (*u==NULL) {
      push_ptr_value(int_ptr,(GENERIC *)u);
      (*u)=STACK_ALLOC(node);
      **u= *v;
      more_v_attr=TRUE;
    }
    else {
      ptr_psi_term t1; // ,t2;
      
      cmp=featcmp((*u)->key,v->key);
      if (cmp==0) {
    if (v->right)
      merge3(&((*u)->right),v->right);
    
        t1 = (ptr_psi_term) (*u)->data;
        /* t2 = (ptr_psi_term) v->data; */
        deref2_eval(t1);
        /* deref2_eval(t2); */
    /* push_goal(unify,(ptr_psi_term)(*u)->data,(ptr_psi_term)v->data,NULL); */
    
    if (v->left)
      merge3(&((*u)->left),v->left);
      }
      else if (cmp>0) {
    temp=v->right;
    v->right=NULL;
    merge3(&((*u)->left),v);
    merge3(u,temp);
    v->right=temp;
      }
      else {
        temp=v->left;
        v->left=NULL;
        merge3(&((*u)->right),v);
        merge3(u,temp);
        v->left=temp;
      }
    }
  }
  else if (*u!=NULL) {
    more_u_attr=TRUE;
  }
}

void merge_unify	(	ptr_node *	u,
		ptr_node	v
	)

merge_unify

Parameters

u	- ptr_node *u
v	- ptr_node v

For built-ins.c

Definition at line 1146 of file login.c.

References merge1(), and merge3().

{
  merge1(u,v); /* Unify corresponding arguments */
  merge3(u,v); /* Merge v's loners into u & evaluate corresponding arguments */
}

long no_choices

(

)

no_choices

Return TRUE iff the top choice point is a what_next choice point or if there are no choice points.

Definition at line 1945 of file login.c.

References choice_stack, wl_choice_point::goal_stack, NULL, wl_goal::type, and what_next.

{
  return (choice_stack==NULL) || (choice_stack->goal_stack->type==what_next);
}

long num_choices

(

)

num_choices

Return the number of choice points on the choice point stack

Definition at line 1956 of file login.c.

References choice_stack, and wl_choice_point::next.

{
  long num;
  ptr_choice_point cp;
  
  num=0;
  cp=choice_stack;
  while (cp) {
    num++;
    cp=cp->next;
  }
  return num;
}

long num_vars

(

ptr_node

vt

)

num_vars

Parameters

vt	- ptr_node vt

Return the number of variables in the variable tree.

Definition at line 1976 of file login.c.

References wl_node::left, and wl_node::right.

{
  return (vt?(num_vars(vt->left)+1+num_vars(vt->right)):0);
}

long prove_aim

(

)

prove_aim

PROVE_AIM() This is the proving routine. It performs one proof step, that is: finding the definition to use to prove AIM, and unifying the HEAD with the GOAL before proving. It all works by pushing sub-goals onto the goal_stack. Special cases are CUT and AND (","). Built-in predicates written in C are called.

Definition at line 1645 of file login.c.

References wl_goal::aaaa_1, wl_pair_list::aaaa_2, aim, and, wl_psi_term::attr_list, wl_goal::bbbb_1, wl_pair_list::bbbb_2, boolpredsym, c_rule, call_handlersym, can_curry, choice_stack, clean_trail(), clear_copy(), wl_psi_term::coref, curried, cut, cut_to, wl_node::data, DEFRULES, deref_args, deref_ptr, do_currying(), do_residuation_user(), eval_copy(), FALSE, function_it, get_two_args(), goal_count, goal_stack, i_check_out(), i_eval_args(), wl_node::key, wl_node::left, lf_false, lf_true, life_or, MAX_BUILT_INS, merge(), wl_pair_list::next, wl_goal::next, NULL, one, predicate_it, wl_definition::protected, prove, push_choice_point(), push_goal(), push_psi_ptr_value(), quote_copy(), resid_aim, resid_vars, wl_node::right, wl_definition::rule, set_empty, STACK, stack_add_psi_attr(), STACK_ALLOC, stack_psi_term(), wl_psi_term::status, sub_type(), succeed, traceline(), tracesym, TRUE, wl_psi_term::type, wl_definition::type_def, type_it, undef_it, and wl_psi_term::value_3.

{
  long success=TRUE;
  ptr_psi_term thegoal,head,body,arg1,arg2;
  ptr_pair_list rule;
  
  thegoal=(ptr_psi_term )aim->aaaa_1;
  rule=(ptr_pair_list )aim->bbbb_1;
  
  if (thegoal && rule) {
    
    deref_ptr(thegoal); /* Evaluation is explicitly handled later. */
    
    if (thegoal->type!=and) {
      if (thegoal->type!=cut)
    if(thegoal->type!=life_or) {
      /* User-defined predicates with unevaluated arguments */
      /* Built-ins do this themselves (see built_ins.c). */
      /* if (!thegoal->type->evaluate_args) mark_quote(thegoal); 24.8 25.8 */
      
      if(i_check_out(thegoal)) { /* RM: Apr  6 1993  */
        
        goal_stack=aim->next;
        goal_count++;
        
        if ((unsigned long)rule==DEFRULES) {
          rule=(ptr_pair_list)thegoal->type->rule;
          if (thegoal->type->type_def==(def_type)predicate_it) {
        if (!rule) /* This can happen when RETRACT is used */
          success=FALSE;
          }
          else if ( thegoal->type->type_def==(def_type)function_it
              || ( thegoal->type->type_def==(def_type)type_it
             && sub_type(boolean,thegoal->type)
             )
                  ) {
        if (thegoal->type->type_def==(def_type)function_it && !rule)
          /* This can happen when RETRACT is used */
          success=FALSE;
        else {
          ptr_psi_term bool_pred;
          ptr_node a;
          /* A function F in pred. position is called as */
          /* '*bool_pred*'(F), which succeeds if F returns true */
          /* and fails if it returns false.  It can residuate too. */
          bool_pred=stack_psi_term(0);
          bool_pred->type=boolpredsym;
          bool_pred->attr_list=(a=STACK_ALLOC(node));
          a->key=one;
          a->left=a->right=NULL;
          a->data=(GENERIC) thegoal;
          push_goal(prove,(ptr_psi_term)bool_pred,(ptr_psi_term)DEFRULES,NULL);
          return success; /* We're done! */
        }
          }
          else if (!thegoal->type->protected && thegoal->type->type_def==(def_type)undef_it) {
        /* Don't give an error message for undefined dynamic objects */
        /* that do not yet have a definition */
        success=FALSE;
          }
          else if (thegoal->type==lf_true || thegoal->type==lf_false) {
        /* What if the 'lf_true' or 'lf_false' have arguments? */
        success=(thegoal->type==lf_true);
        return success; /* We're done! */
          }
          else {
        /* Error: undefined predicate. */
        /* Call the call_handler (which may do an auto-load). */
        ptr_psi_term call_handler;
        /* mark_quote(thegoal); */
        
        /*  RM: Jan 27 1993 */
        /* warningline("call handler invoked for %P\n",thegoal); */
        
        call_handler=stack_psi_term(0);
        call_handler->type=call_handlersym;
        stack_add_psi_attr(call_handler,"1",thegoal);
        push_goal(prove,(ptr_psi_term)call_handler,(ptr_psi_term)DEFRULES,NULL);
        return success; /* We're done! */
          }
        }
        
        if (success) {
          
          if ((unsigned long)rule<=MAX_BUILT_INS) {
        
        /* For residuation (RESPRED) */
        curried=FALSE;
        can_curry=TRUE;
        resid_vars=NULL;
        /* resid_limit=(ptr_goal )stack_pointer; 12.6 */
        
        if (thegoal->type!=tracesym) /* 26.1 */
          traceline("prove built-in %P\n", thegoal);
        
        /* RESPRED */ resid_aim=aim;
        /* Residuated predicate must return success=TRUE */
        success=c_rule[(unsigned long)rule]();
        
        /* RESPRED */ if (curried)
        /* RESPRED */   do_currying();
        /* RESPRED */ else if (resid_vars)
        /* RESPRED */   success=do_residuation_user(); /* 21.9 */ /* PVR 9.2.94 */
          }
          else {
        
        /* Evaluate arguments of a predicate call before the call. */
        deref_args(thegoal,set_empty);
        
        traceline("prove %P\n", thegoal);
        
        /* For residuation (RESPRED) */
        curried=FALSE;
        can_curry=TRUE;
        resid_vars=NULL;
        /* resid_limit=(ptr_goal )stack_pointer; 12.6 */
        
        while (rule && (rule->aaaa_2==NULL || rule->bbbb_2==NULL)) {
          rule=rule->next;
          traceline("alternative clause has been retracted\n");
        }
        if (rule) {
          
          clear_copy();
          if (TRUE) /* 8.9 */
            /* if (thegoal->type->evaluate_args) 8.9 */
            head=eval_copy(rule->aaaa_2,STACK);
          else
            head=quote_copy(rule->aaaa_2,STACK);

          body=eval_copy(rule->bbbb_2,STACK);

          /* What does this do?? */
          /* if (body->type==built_in) */
          /*   body->coref=head; */
          
          if (rule->next)
            push_choice_point(prove,thegoal,(ptr_psi_term)rule->next,NULL);
          
          if (body->type!=succeed)
            push_goal(prove,(ptr_psi_term)body,(ptr_psi_term)DEFRULES,NULL);
          
          /* push_ptr_value(psi_term_ptr,&(head->coref)); 9.6 */
          push_psi_ptr_value(head,(GENERIC *)&(head->coref));
          head->coref=thegoal;
          merge(&(thegoal->attr_list),head->attr_list);
          if (!head->status) {
            (void)i_eval_args(head->attr_list);
          }
        }
        else {
          success=FALSE;
        }
          }
        }
      }
    }
    else { /* ';' built-in */
      /*  RM: Apr  6 1993  */
      goal_stack=aim->next;
      goal_count++;
      get_two_args(thegoal->attr_list,&arg1,&arg2);
      push_choice_point(prove,arg2,(ptr_psi_term)DEFRULES,NULL);
      push_goal(prove,(ptr_psi_term)arg1,(ptr_psi_term)DEFRULES,NULL);
    }
      else { /* 'Cut' built-in*/
    goal_stack=aim->next;
    goal_count++;
    /* assert((ptr_choice_point)(thegoal->value)<=choice_stack); 12.7 */
    cut_to(thegoal->value_3); /* 12.7 */
#ifdef CLEAN_TRAIL
        clean_trail(choice_stack);
#endif
        traceline("cut all choice points back to %x\n",choice_stack);
      }
    }
    else { /* 'And' built-in */
      goal_stack=aim->next;
      goal_count++;
      get_two_args(thegoal->attr_list,&arg1,&arg2);
      push_goal(prove,(ptr_psi_term)arg2,(ptr_psi_term)DEFRULES,NULL);
      push_goal(prove,(ptr_psi_term)arg1,(ptr_psi_term)DEFRULES,NULL);
    }
  }
  else
    success=FALSE;
  
  /* RESPRED */ resid_aim=NULL;
  return success;
}

void push2_ptr_value	(	type_ptr	t,
		GENERIC *	p,
		GENERIC	v
	)

push2_ptr_value

Parameters

t	- type_ptr t
p	- GENERIC *p
v	- GENERIC v

PUSH2_PTR_VALUE(t,*p,v) Push the pair (P,V) onto the stack of things to be undone (trail). It needn't be done if P is greater than the latest choice point because in that case memory is reclaimed.

Definition at line 573 of file login.c.

References wl_stack::aaaa_3, wl_stack::bbbb_3, choice_stack, wl_stack::next, STACK_ALLOC, stack_pointer, wl_stack::type, and undo_stack.

{
  ptr_stack n;
  
  if (p<(GENERIC *)choice_stack || p>(GENERIC *)stack_pointer) {
    n=STACK_ALLOC(stack);
    n->type=t;
    n->aaaa_3= (GENERIC *)p;
    n->bbbb_3= (GENERIC *)v;
    n->next=undo_stack;
    undo_stack=n;
  }
}

void push_choice_point	(	goals	t,
		ptr_psi_term	aaaa_6,
		ptr_psi_term	bbbb_6,
		GENERIC	cccc_6
	)

push_choice_point

Parameters

t	- goals t
aaaa_6	ptr_psi_term aaaa_6
bbbb_6	ptr_psi_term bbbb_6
cccc_6	GENERIC cccc_6

PUSH_CHOICE_POINT(t,a,b,c) T,A,B,C is an alternative goal to try. T is the type of the goal: unify or prove.

If T=prove then a=goal to prove b=definition to use if b=DEFRULES then that means it's a first call.

If T=unify then a and b are the terms to unify.

etc...

Definition at line 638 of file login.c.

References wl_goal::aaaa_1, wl_goal::bbbb_1, wl_goal::cccc_1, choice_stack, FALSE, global_time_stamp, wl_choice_point::goal_stack, goal_stack, wl_goal::next, wl_choice_point::next, wl_goal::pending, STACK_ALLOC, stack_pointer, wl_choice_point::stack_top, wl_choice_point::time_stamp, wl_goal::type, wl_choice_point::undo_point, and undo_stack.

{
  ptr_goal alternative;
  ptr_choice_point choice;
  GENERIC top_loc;
  
  alternative=STACK_ALLOC(goal);
  
  alternative->type=t;
  alternative->aaaa_1=aaaa_6;
  alternative->bbbb_1=bbbb_6;
  alternative->cccc_1=cccc_6;
  alternative->next=goal_stack;
  alternative->pending=FALSE;
  
  top_loc=stack_pointer;
  
  choice=STACK_ALLOC(choice_point);
  
  choice->undo_point=undo_stack;
  choice->goal_stack=alternative;
  choice->next=choice_stack;
  choice->stack_top=top_loc;
  
#ifdef TS
  choice->time_stamp=global_time_stamp; /* 9.6 */
  global_time_stamp++; /* 9.6 */
#endif
  
  choice_stack=choice;  
}

void push_def_ptr_value	(	ptr_psi_term	q,
		GENERIC *	p
	)

push_def_ptr_value

Parameters

q	- ptr_psi_term q
p	- GENERIC *p

PUSH_DEF_PTR_VALUE(q,p) (9.6) Same as push_ptr_value, but only for psi-terms whose definition field is being modified. (If another field is modified, use push_ptr_value.) This routine implements the time-stamp technique of only trailing once between choice point creations, even on multiple bindings. q is address of psi-term, p is address of field inside psi-term that is modified. Both the definition and the time_stamp must be trailed.

Definition at line 416 of file login.c.

References wl_stack::aaaa_3, assert, wl_stack::bbbb_3, choice_stack, def_ptr, global_time_stamp, heap_pointer, int_ptr, wl_stack::next, push_ptr_value(), STACK_ALLOC, stack_pointer, trail_condition(), wl_stack::type, undo_stack, and VALID_ADDRESS.

{
  ptr_stack m,n;
  
  assert(VALID_ADDRESS(q));
  assert(VALID_ADDRESS(p));
#ifdef TS
  if (trail_condition(q) &&
      /* (q->time_stamp != global_time_stamp) && */
      (p < (GENERIC *)choice_stack || p > (GENERIC *)stack_pointer))
    {
#define TRAIL_TS
#ifdef TRAIL_TS
      
      assert((GENERIC)q<heap_pointer); /*  RM: Feb 15 1993  */
      
      m=STACK_ALLOC(stack); /* Trail time_stamp */
      m->type=int_ptr;
      m->aaaa_3= (GENERIC *) &(q->time_stamp);
      m->bbbb_3= (GENERIC *) (q->time_stamp);
      m->next=undo_stack;
      n=STACK_ALLOC(stack); /* Trail definition field (top of undo_stack) */
      n->type=def_ptr;
      n->aaaa_3=  p;
      n->bbbb_3= (GENERIC *)*p;
      n->next=m;
      undo_stack=n;
#else
      n=STACK_ALLOC(stack); /* Trail definition field (top of undo_stack) */
      n->type=def_ptr;
      n->aaaa_3= p;
      n->bbbb_3= (GENERIC *) *p;
      n->next=undo_stack;
      undo_stack=n;
#endif
      q->time_stamp=global_time_stamp;
    }
#else
  push_ptr_value(def_ptr,p);
#endif
}

void push_goal	(	goals	t,
		ptr_psi_term	aaaa_5,
		ptr_psi_term	bbbb_5,
		GENERIC	cccc_5
	)

push_goal

Parameters

t	- goals t
aaaa_5	ptr_psi_term aaaa_5
bbbb_5	ptr_psi_term bbbb_5
cccc_5	GENERIC cccc_5

PUSH_GOAL(t,a,b,c) Push a goal onto the goal stack. T is the type of the goal, A,B and C are various parameters. See PUSH_CHOICE_POINT(t,a,b,c).

Definition at line 600 of file login.c.

References wl_goal::aaaa_1, wl_goal::bbbb_1, wl_goal::cccc_1, FALSE, goal_stack, wl_goal::next, wl_goal::pending, STACK_ALLOC, and wl_goal::type.

{
  ptr_goal thegoal;
  
  thegoal=STACK_ALLOC(goal);
  
  thegoal->type=t;
  thegoal->aaaa_1=aaaa_5;
  thegoal->bbbb_1=bbbb_5;
  thegoal->cccc_1=cccc_5;
  thegoal->next=goal_stack;
  thegoal->pending=FALSE;
  
  goal_stack=thegoal;
}

void push_psi_ptr_value	(	ptr_psi_term	q,
		GENERIC *	p
	)

push_psi_ptr_value

Parameters

q	- ptr_psi_term q
p	- GENERIC *p

PUSH_PSI_PTR_VALUE(q,p) (9.6) Same as push_ptr_value, but only for psi-terms whose coref field is being modified. (If another field is modified, use push_ptr_value.) This routine implements the time-stamp technique of only trailing once between choice point creations, even on multiple bindings. q is address of psi-term, p is address of field inside psi-term that is modified. Both the coref and the time_stamp must be trailed.

Definition at line 474 of file login.c.

References wl_stack::aaaa_3, assert, wl_stack::bbbb_3, choice_stack, global_time_stamp, int_ptr, wl_stack::next, psi_term_ptr, push_ptr_value(), STACK_ALLOC, stack_pointer, trail_condition(), wl_stack::type, undo_stack, and VALID_ADDRESS.

{
  ptr_stack m,n;
  
  assert(VALID_ADDRESS(q));
  assert(VALID_ADDRESS(p));
#ifdef TS
  if (trail_condition(q) &&
      /* (q->time_stamp != global_time_stamp) && */
      (p < (GENERIC *)choice_stack || p > (GENERIC *)stack_pointer))
    {
#define TRAIL_TS
#ifdef TRAIL_TS
      m=STACK_ALLOC(stack); /* Trail time_stamp */
      m->type=int_ptr;
      m->aaaa_3= (GENERIC *) &(q->time_stamp);
      m->bbbb_3= (GENERIC *) (q->time_stamp);
      m->next=undo_stack;
      n=STACK_ALLOC(stack); /* Trail coref field (top of undo_stack) */
      n->type=psi_term_ptr;
      n->aaaa_3= (GENERIC *) p;
      n->bbbb_3= (GENERIC *) *p;
      n->next=m;
      undo_stack=n;
#else
      n=STACK_ALLOC(stack); /* Trail coref field (top of undo_stack) */
      n->type=psi_term_ptr;
      n->aaaa_3= (ptr_psi_term)p;
      n->bbbb_3= *p;
      n->next=undo_stack;
      undo_stack=n;
#endif
      q->time_stamp=global_time_stamp;
    }
#else
  push_ptr_value(psi_term_ptr,(ptr_psi_term *)p);
#endif
}

void push_ptr_value	(	type_ptr	t,
		GENERIC *	p
	)

push_ptr_value

Parameters

t	- type_ptr t
p	- GENERIC *p

PUSH_PTR_VALUE(t,*p) Push the pair (P,*P) onto the stack of things to be undone (trail). It needn't be done if P is greater than the latest choice point because in that case memory is reclaimed.

Definition at line 383 of file login.c.

References wl_stack::aaaa_3, assert, wl_stack::bbbb_3, choice_stack, heap_pointer, wl_stack::next, STACK_ALLOC, stack_pointer, wl_stack::type, undo_stack, and VALID_ADDRESS.

{
  ptr_stack n;
  
  assert(p<(GENERIC *)heap_pointer); /*  RM: Feb 15 1993  */
  
  assert(VALID_ADDRESS(p));
  if (p < (GENERIC *)choice_stack || p > (GENERIC *)stack_pointer) 
    {
      n=STACK_ALLOC(stack);
      n->type=t;
      n->aaaa_3= (GENERIC *) p;
      n->bbbb_3= (GENERIC *) *p;
      n->next=undo_stack;
      undo_stack=n;
    }
}

void push_ptr_value_global	(	type_ptr	t,
		GENERIC *	p
	)

push_ptr_value_global

Parameters

t	- type_ptr t
p	- GENERIC *p

Same as push_ptr_value, but for objects that must always be trailed. This includes objects outside of the Life data space and entries in the var_tree.

Definition at line 523 of file login.c.

References wl_stack::aaaa_3, assert, wl_stack::bbbb_3, wl_stack::next, STACK_ALLOC, wl_stack::type, undo_stack, and VALID_ADDRESS.

{
  ptr_stack n;
  
  assert(VALID_ADDRESS(p)); /* 17.8 */
  n=STACK_ALLOC(stack);
  n->type=t;
  n->aaaa_3= (GENERIC *) p;
  n->bbbb_3= (GENERIC *) *p;
  n->next=undo_stack;
  undo_stack=n;
}

void push_window	(	long	type,
		long	disp,
		long	wind
	)

push_window

Parameters

type	- long type
disp	- long disp
wind	- long wind

PUSH_WINDOW(type,disp,wind) Push the window information (operation, display and window identifiers) on the undo_stack (trail) so that the window can be destroyed, redrawn, or hidden on backtracking.

Definition at line 548 of file login.c.

References wl_stack::aaaa_3, assert, wl_stack::bbbb_3, wl_stack::next, STACK_ALLOC, wl_stack::type, undo_action, and undo_stack.

{
  ptr_stack n;
  
  assert(type & undo_action);
  n=STACK_ALLOC(stack);
  n->type=type;
  n->aaaa_3=(GENERIC *)disp;
  n->bbbb_3=(GENERIC *)wind;
  n->next=undo_stack;
  undo_stack=n;
}

void reset_stacks

(

)

reset_stacks

Called when level jumps back to zero. Setting these two pointers to NULL causes an exit from main_prove and will then reset all other global information.

Definition at line 2047 of file login.c.

References choice_stack, goal_stack, NULL, and undo().

{
  undo(NULL); /* 8.10 */
  goal_stack=NULL;
  choice_stack=NULL;
#ifdef TS
  /* global_time_stamp=INIT_TIME_STAMP; */ /* 9.6 */
#endif
}

void show_count

(

)

show_count

SHOW_COUNT() This routine doesn't do anything if not in verbose mode. It prints the number of of sub-goals attempted, along with cpu-time spent during the proof etc...

Definition at line 1161 of file login.c.

References end_time, goal_count, heap_pointer, mem_base, mem_limit, NOTQUIET, stack_info(), stack_pointer, and verbose.

{
  float t;
  
  if (verbose) {
    printf("  [");
    
    (void)times(&end_time);
    t = (end_time.tms_utime - start_time.tms_utime)/60.0;
    
    printf("%1.3fs cpu, %ld goal%s",t,goal_count,(goal_count!=1?"s":""));
    
    if (t!=0.0) printf(" (%0.0f/s)",goal_count/t);
    
    printf(", %ld stack",sizeof(mem_base)*(stack_pointer-mem_base));
    printf(", %ld heap",sizeof(mem_base)*(mem_limit-heap_pointer));
    
    printf("]");
  }
  
  if(NOTQUIET) {
    printf("\n");
    stack_info(stdout);
  }
  
  goal_count=0;
}

void start_chrono

(

)

start_chrono

START_CHRONO() This initialises the CPU time counter.

Definition at line 349 of file login.c.

{
  (void)times(&start_time);
}

ptr_choice_point topmost_what_next

(

)

topmost_what_next

UNUSED 12.7 Return the choice point corresponding to the first 'what_next' choice point in the choice point stack. Return NULL if there is none. This is used to ensure that cuts don't go below the most recent 'what_next' choice point.

Definition at line 2026 of file login.c.

References choice_stack, wl_choice_point::goal_stack, wl_choice_point::next, NULL, wl_goal::type, and what_next.

{
  ptr_choice_point cp=choice_stack;
  
  while (cp && cp->goal_stack && cp->goal_stack->type!=what_next)
    cp=cp->next;
  
  if (cp && cp->goal_stack && cp->goal_stack->type==what_next)
    return cp;
  else
    return (ptr_choice_point) NULL;
}

long trail_condition

(

psi_term *

Q

)

trail_condition

Parameters

Q	- psi_term *Q

Definition at line 2630 of file login.c.

References choice_stack, and wl_choice_point::time_stamp.

{
  return  (choice_stack && choice_stack->time_stamp>=Q->time_stamp);
}

void type_disj_aim

(

)

type_disj_aim

TYPE_DISJ_AIM() This routine implements type disjunctions, that is, when a type has been decoded and found to be a disjunction of types, enumerates the different values one by one.

Definition at line 1845 of file login.c.

References wl_goal::aaaa_1, aim, wl_definition::always_check, wl_psi_term::attr_list, wl_goal::bbbb_1, def_ptr, FALSE, fetch_def(), wl_definition::keyword, wl_int_list::next, NULL, push_choice_point(), push_ptr_value(), wl_psi_term::status, wl_keyword::symbol, traceline(), wl_psi_term::type, type_disj, and wl_int_list::value_1.

{
  ptr_psi_term t;
  ptr_int_list d;
  
  t=(ptr_psi_term)aim->aaaa_1;
  d=(ptr_int_list)aim->bbbb_1;
  
  if (d->next) {
    traceline("pushing type disjunction choice point for %P\n", t);
    push_choice_point(type_disj,t,(ptr_psi_term)d->next,NULL);
  }
  
  push_ptr_value(def_ptr,(GENERIC *)&(t->type));
  /* Below makes cut.lf behave incorrectly: */
  /* push_def_ptr_value(t,&(t->type)); */ /* 14.8 */
  t->type=(ptr_definition)d->value_1;
  
  traceline("setting type disjunction to %s.\n", t->type->keyword->symbol);
  
  if ((t->attr_list || t->type->always_check) && t->status<4)
    fetch_def(t, FALSE);
}

void undo

(

ptr_stack

limit

)

undo

Parameters

limit

- ptr_stack limit

UNDO(limit) Undoes any side-effects up to LIMIT. Limit being the adress of the stack of side-effects you wish to return to.

Possible improvement: LIMIT is a useless parameter because GOAL_STACK is equivalent if one takes care when stacking UNDO actions. Namely, anything to be undone must be stacked LATER (=after) the goal which caused these things to be done, so that when the goal fails, everything done after it can be undone and the memory used can be reclaimed. This routine could be modified in order to cope with goals to be proved on backtracking: undo(goal).

Definition at line 691 of file login.c.

References wl_stack::aaaa_3, wl_stack::bbbb_3, destroy_window, hide_subwindow, hide_window, wl_stack::next, show_subwindow, show_window, wl_stack::type, undo_action, undo_stack, x_destroy_window(), x_hide_subwindow(), x_hide_window(), x_show_subwindow(), and x_show_window().

{
  /*
    while((unsigned long)undo_stack>(unsigned long)goal_stack)
    */
  
  while ((unsigned long)undo_stack>(unsigned long)limit) { 
#ifdef X11
    if (undo_stack->type & undo_action) {
      /* Window operation on backtracking */
      switch(undo_stack->type) { /*** RM 8/12/92 ***/
      case destroy_window:
        x_destroy_window((Display *)undo_stack->aaaa_3,(Window)undo_stack->bbbb_3);
    break;
      case show_window:
        x_show_window((Display *)undo_stack->aaaa_3,(Window)undo_stack->bbbb_3);
    break;
      case hide_window:
        x_hide_window((Display *)undo_stack->aaaa_3,(Window)undo_stack->bbbb_3);
    break;
      case show_subwindow:
        x_show_subwindow((Display *)undo_stack->aaaa_3,(Window)undo_stack->bbbb_3);
    break;
      case hide_subwindow:
        x_hide_subwindow((Display *)undo_stack->aaaa_3,(Window)undo_stack->bbbb_3);
    break;
      }
    }
    else
#endif
      /* Restoring variable value on backtracking */
      *((GENERIC *)(undo_stack->aaaa_3))=(GENERIC)undo_stack->bbbb_3;
    undo_stack=undo_stack->next;
  }
}

void undo_actions

(

)

undo_actions

UNDO_ACTIONS() A subset of undo(limit) (the detrailing routine) that does all undo actions on the undo_stack, but does not undo any variable bindings, nor does it change the value of undo_stack.

Definition at line 736 of file login.c.

References Errorline(), NULL, and undo().

{
  // ptr_stack u=undo_stack;
  
  Errorline("undo_actions should not be called.\n");
  undo(NULL); /* 8.10 */
  return;
  /*
    #ifdef X11
    while ((unsigned long)u) {
    if (u->type & undo_action) {
    if (u->type==destroy_window) {
    x_destroy_window((unsigned long)u->aaaa_3,(unsigned long)u->bbbb_3);
    }
    else if (u->type==show_window) {
    x_show_window((unsigned long)u->aaaa_3,(unsigned long)u->bbbb_3);
    }
    else if (u->type==hide_window) {
    x_hide_window((unsigned long)u->aaaa_3,(unsigned long)u->bbbb_3);
    }
    }
    u=u->next;
    }
    #endif
    */
}

long unify_aim

(

)

unify_aim

UNIFY_AIM() This routine performs one unification step. AIM is the current unification goal.

U and V are the two psi-terms to unify.

It swaps the two psi-terms into chronological order. U is the oldest (smallest stack address). Calculates their GLB, check their values are unifiable. It deals with all the messy things like: curried functions gaining missing arguments, types which need checking, residuation variables whose constraints must be released, disjunctions appearing in the GLB etc...

It's a rather lengthy routine, only its speed is fairly crucial in the overall performance of Wild_Life, and the code is not duplicated elsewhere.

Definition at line 1344 of file login.c.

References TRUE, and unify_body().

{
  return unify_body(TRUE);
}

long unify_aim_noeval

(

)

unify_aim_noeval

Definition at line 1354 of file login.c.

References FALSE, and unify_body().

{
  return unify_body(FALSE);
}

long unify_body

(

long

eval_flag

)

unify_body

Parameters

eval_flag

- long eval_flag

Definition at line 1365 of file login.c.

References wl_goal::aaaa_1, aim, wl_psi_term::attr_list, wl_goal::bbbb_1, wl_psi_term::coref, cut, cut_ptr, decode(), def_ptr, deref, deref_ptr, equal_types, Errorline(), FALSE, fetch_def_lazy(), wl_psi_term::flags, function_it, glb(), global_unify(), heap_pointer, int_ptr, integer, wl_definition::keyword, merge(), more_u_attr, more_v_attr, new_stat, wl_int_list::next, NULL, overlap_type(), push_choice_point(), push_psi_ptr_value(), push_ptr_value(), quoted_string, QUOTED_TRUE, REAL, real, release_resid(), wl_psi_term::resid, wl_psi_term::status, sub_type(), wl_keyword::symbol, sys_bytedata, traceline(), TRUE, wl_psi_term::type, wl_definition::type_def, type_disj, type_it, u_func, v_func, wl_int_list::value_1, wl_psi_term::value_3, and warningline().

{
  long success=TRUE,compare;
  ptr_psi_term u,v,tmp;
  REAL r;
  ptr_definition new_type,old1,old2;
  ptr_node old1attr, old2attr;
  ptr_int_list new_code;
  ptr_int_list d=NULL;
  long old1stat,old2stat; /* 18.2.94 */
  
  u=(ptr_psi_term )aim->aaaa_1;
  v=(ptr_psi_term )aim->bbbb_1;
  
  deref_ptr(u);
  deref_ptr(v);

  traceline("unify %P with %P\n",u,v);
  
  if (eval_flag) {
    deref(u);
    deref(v);
  }
  
  if (u!=v) {
    
    /**** Swap the two psi-terms to get them into chronological order ****/
    if (u>v) { tmp=v; v=u; u=tmp; }
      
    /**** Check for curried functions ****/
    u_func=(u->type->type_def==(def_type)function_it);
    v_func=(v->type->type_def==(def_type)function_it);
    old1stat=u->status; /* 18.2.94 */
    old2stat=v->status; /* 18.2.94 */
    
    /* PVR 18.2.94 */
    /* if (u_func && !(u->flags&QUOTED_TRUE) && v->attr_list) { */
    if (u_func && u->status==4 && !(u->flags&QUOTED_TRUE) && v->attr_list) {
      Errorline("attempt to unify with curried function %P\n", u);
      return FALSE;
    }
    /* if (v_func && !(v->flags&QUOTED_TRUE) && u->attr_list) { */
    if (v_func && v->status==4 && !(v->flags&QUOTED_TRUE) && u->attr_list) {
      Errorline("attempt to unify with curried function %P\n", v);
      return FALSE;
    }

    
#ifdef ARITY  /*  RM: Mar 29 1993  */
    arity_unify(u,v);
#endif
    
    /***** Deal with global vars ****   RM: Feb  8 1993  */
    if((GENERIC) v>=heap_pointer)
      return global_unify(u,v);
    
    
    /**** Calculate their Greatest Lower Bound and compare them ****/
    success=(compare=glb(u->type,v->type,&new_type,&new_code));
    
    if (success) {
      
      /**** Keep the old types for later use in incr. constraint checking ****/
      old1 = u->type;
      old2 = v->type;
      old1attr = u->attr_list;
      old2attr = v->attr_list;
      
      /**** DECODE THE RESULTING TYPE ****/
      if (!new_type) {
    d=decode(new_code);
    if (d) {
      new_type=(ptr_definition)d->value_1;
      d=d->next;
    }
    else
          Errorline("undecipherable sort code.\n");
      }
      
      /**** Make COMPARE a little more precise ****/
      if (compare==1)
    if (u->value_3 && !v->value_3)
      compare=2;
    else
      if (v->value_3 && !u->value_3)
        compare=3;
      
      /**** Determine the status of the resulting psi-term ****/
      new_stat=4;
      switch (compare) {
      case 1:
    if (u->status <4 && v->status <4)
      new_stat=2;
    break;
      case 2:
    if (u->status<4)
      new_stat=2;
    break;
      case 3:
    if (v->status<4)
      new_stat=2;
    break;
      case 4:
    new_stat=2;
    break;
      }
      
      /*
    printf("u=%s, v=%s, compare=%ld, u.s=%ld, v.s=%ld, ns=%ld\n",
    u->type->keyword->symbol,
    v->type->keyword->symbol,
    compare,
    u->status,
    v->status,
    new_stat);
    */
      
      /**** Check that integers have no decimals ****/
      if (u->value_3 && sub_type(new_type,integer)) {
    r= *(REAL *)u->value_3;
    success=(r==floor(r));
      }
      if (success && v->value_3 && sub_type(new_type,integer)) {
    r= *(REAL *)v->value_3;
    success=(r==floor(r));
      }
      
      /**** Unify the values of INTs REALs STRINGs LISTs etc... ****/
      if (success) {
        /* LAZY-EAGER */
    if (u->value_3!=v->value_3)
      if (!u->value_3) {
        compare=4;
        push_ptr_value(int_ptr,(GENERIC *)&(u->value_3));
        u->value_3=v->value_3;      
      }
      else if (v->value_3) {
        if (overlap_type(new_type,real))
              success=(*((REAL *)u->value_3)==(*((REAL *)v->value_3)));
            else if (overlap_type(new_type,quoted_string))
              success=(strcmp((char *)u->value_3,(char *)v->value_3)==0);
        else if (overlap_type(new_type,sys_bytedata)) {
          unsigned long ulen = *((unsigned long *)u->value_3);
          unsigned long vlen = *((unsigned long *)v->value_3);
              success=(ulen==vlen &&
               (bcmp((char *)u->value_3,(char *)v->value_3,ulen)==0));
        }
            else if (u->type==cut && v->type==cut) { /* 22.9 */
              ptr_psi_term mincut;
              mincut = (ptr_psi_term)  (u->value_3 < (GENERIC) v->value_3? u->value_3 : v->value_3);
              if (mincut!=(ptr_psi_term)u->value_3) {
                push_ptr_value(cut_ptr,(GENERIC *)&(u->value_3));
                u->value_3=(GENERIC)mincut;
              }
            }
            else {
              warningline("'%s' may not be unified.\n",new_type->keyword->symbol);
              success=FALSE;
            }
          }
          else
        compare=4;
      }
      
      /**** Bind the two psi-terms ****/
      if (success) {
    /* push_ptr_value(psi_term_ptr,(ptr_psi_term *)&(v->coref)); 9.6 */
    push_psi_ptr_value(v,(GENERIC *)&(v->coref));
    v->coref=u;
    
    if (!equal_types(u->type,new_type)) {         
      push_ptr_value(def_ptr,(GENERIC *)&(u->type));
          /* This does not seem to work right with cut.lf: */
          /* push_def_ptr_value(u,&(u->type_3)); */ /* 14.8 */
      u->type=new_type;
    }
    
    if (u->status!=new_stat) {
      push_ptr_value(int_ptr,(GENERIC *)&(u->status));
      u->status=new_stat;
    }
    
    /**** Unify the attributes ****/
    more_u_attr=FALSE;
    more_v_attr=FALSE;
    
    
#ifdef ARITY  /*  RM: Mar 29 1993  */
    arity_merge(u->attr_list,v->attr_list);
#endif
    
    
    if (u->attr_list || v->attr_list)
      merge(&(u->attr_list),v->attr_list);
    
    /**** Look after curried functions ****/
    /*
    if ((u_func && more_v_attr) || (v_func && more_u_attr)) {
      if (!(u->flags&QUOTED_TRUE | v->flags&QUOTED_TRUE)) {
            traceline("re-evaluating curried expression %P\n", u);
        if (u->status!=0) {
          push_ptr_value(int_ptr,(ptr_psi_term *)&(u->status));
          u->status=0;
        }
            check_func(u);
          }
      }
      */
    
    if (v->flags&QUOTED_TRUE && !(u->flags&QUOTED_TRUE)) { /* 16.9 */
      push_ptr_value(int_ptr,(GENERIC *)&(u->flags));
      u->flags|=QUOTED_TRUE;
        }
    
    /**** RELEASE RESIDUATIONS ****/
    /* This version implements the correct semantics. */
    if (u->resid)
      release_resid(u);
    if (v->resid)
      release_resid(v);
    
        /**** Alternatives in a type disjunction ****/
        if (d) {
          traceline("pushing type disjunction choice point for %P\n",u);
          push_choice_point(type_disj,u,(ptr_psi_term)d,NULL);
        }
    
    /**** VERIFY CONSTRAINTS ****/
    /* if ((old1stat<4 || old2stat<4) &&
         (u->type->type==type || v->type->type==type)) { 18.2.94 */
        if (new_stat<4 && u->type->type_def==(def_type)type_it) {
          /* This does not check the already-checked properties     */
          /* (i.e. those in types t with t>=old1 or t>=old2),       */
          /* and it does not check anything if u has no attributes. */
          /* It will, however, check the unchecked properties if a  */
          /* type gains attributes.                                 */
          fetch_def_lazy(u, old1, old2, 
             old1attr, old2attr,
             old1stat, old2stat);
        }
      }
    }
  }
  return success;
}

long what_next_aim

(

)

what_next_aim

WHAT_NEXT_AIM() Find out what the user wants to do: a) retry current goal -> ';' b) quit current goal -> RETURN c) add current goal -> 'new goal ?' d) return to top level -> '.'

Definition at line 2068 of file login.c.

References wl_goal::aaaa_1, aborthooksym, aim, assert_clause(), assert_first, wl_goal::bbbb_1, begin_terminal_io(), wl_goal::cccc_1, current_module, DEFRULES, encode_types(), end_terminal_io(), eof, EOLN, FACT, FALSE, function_it, infoline(), MAX_LEVEL, wl_module::module_name, no_choices(), NOTQUIET, NULL, parse(), print_variables(), PROMPT, prompt, prompt_buffer, prove, push_choice_point(), push_goal(), put_back_char(), QUERY, read_char(), release_resid(), reset_stacks(), reset_step(), show_count(), stack_copy_psi_term(), start_chrono(), stdin_cleareof(), TRUE, TRUEMASK, wl_psi_term::type, wl_definition::type_def, undo(), undo_stack, user_module, var_occurred, what_next, what_next_cut(), x_read_stdin_or_event(), x_window_creation, and xevent_existing.

{
  long result=FALSE;
  ptr_psi_term s;
  long c, c2; /* 21.12 (prev. char) */
  char *pr;
  long sort,cut_loc=FALSE;
  long level,i;
  long eventflag;
  ptr_stack save_undo_stack;
  long lev1,lev2;
  begin_terminal_io();
  
  level=((unsigned long)aim->cccc_1);
  
  if (aim->aaaa_1) {
    /* Must remember var_occurred from the what_next goal and from */
    /* execution of previous query (it may have contained a parse) */
    var_occurred=var_occurred || ((unsigned long)aim->bbbb_1)&TRUEMASK; /* 18.8 */
    eventflag=(((unsigned long)aim->bbbb_1)&(TRUEMASK*2))!=0;
    if (
        !var_occurred && no_choices() && level>0
#ifdef X11
        /* Keep level same if no window & no X event */
    && !x_window_creation && !eventflag
#endif
       ) {
      /* Keep level the same if in a query, the number of choice points */
      /* has not increased and there are no variables. */
      /* This has to have the same behavior as if an EOLN was typed */
      /* and no 'No' message should be given on the lowest level,   */
      level--;
      (void)what_next_cut();
      if (level==0) { result=TRUE; }
    }
  }
    
#ifdef X11
  x_window_creation=FALSE;
#endif
  
  infoline(aim->aaaa_1?"\n*** Yes":"\n*** No");
  show_count();
  if (aim->aaaa_1   ||  level>0  ) (void)print_variables(NOTQUIET); // had commente || ... DJD 

  {
    if (level > 0 && aborthooksym->type_def != (def_type)function_it )
      {
    lev1=MAX_LEVEL<level?MAX_LEVEL:(level);
    lev2=level;
      }
    else
      {
    lev1 = 0;
    lev2 = 0;
      }
    
    pr=prompt_buffer;
    /*  RM: Oct 13 1993  */
    if(current_module==user_module)
      *pr='\0';
    else
      strcpy(pr,current_module->module_name);
    pr += strlen(pr);
    for(i=1;i<=lev1;i++) { *pr='-'; pr++; *pr='-'; pr++; }
    if (lev2>0)
      sprintf(pr,"%ld",lev2);
    strcat(pr,PROMPT);
    
    prompt=prompt_buffer;
  }
  
  stdin_cleareof();
  /* The system waits for either an input command or an X event. */
  /* An X event is treated *exactly* like an input command that  */
  /* has the same effect. */
#ifdef X11
  c=x_read_stdin_or_event(&eventflag);
  if (eventflag) {
    /* Include eventflag info in var_occurred field. */
    push_goal(what_next,(ptr_psi_term)TRUE,(ptr_psi_term)(FALSE+2*TRUE),(GENERIC)level /* +1 RM: Jun 22 1993 */);
    release_resid(xevent_existing);
    result=TRUE;
  }
  else
#else
    c=read_char();
#endif
  {
    while (c!=EOLN && c>0 && c<=32 && c!=EOF) {
      c=read_char();
    }
    if (c==EOF) {
      reset_stacks();
    }
    else if (c==EOLN) {
      cut_loc=TRUE;
    }
    else if (c==';' || c=='.') {
      do {
        c2=read_char();
      } while (c2!=EOLN && c2!=EOF && c2>0 && c2<=32);
      if (c=='.') { /* 6.10 */
        reset_stacks();
        result=TRUE;
      }
    }
    else {
      if (level>0) push_choice_point(what_next,FALSE,(ptr_psi_term)FALSE,(GENERIC)level);
  
      put_back_char(c);
      var_occurred=FALSE;
      save_undo_stack=undo_stack;
      s=stack_copy_psi_term(parse(&sort));
      
      if (s->type==eof) {
    reset_stacks();
    put_back_char(EOF);
      } else if (sort==QUERY) {
        push_goal(what_next,(ptr_psi_term)TRUE,(ptr_psi_term)var_occurred,(GENERIC)(level+1));
        push_goal(prove,(ptr_psi_term)s,(ptr_psi_term)DEFRULES,NULL);
        reset_step();
        result=TRUE;
      }
      else if (sort==FACT) { /* A declaration */
        push_goal(what_next,(ptr_psi_term)TRUE,(ptr_psi_term)FALSE,(GENERIC)(level + 1)); /* 18.5 */ // HERE
        assert_first=FALSE;
        assert_clause(s);
        /* Variables in the query may be used in a declaration, */
        /* but the declaration may not add any variables. */
    undo(save_undo_stack); /* 17.8 */
    encode_types();
    result=TRUE;
      }
      else {
    /* Stay at same level on syntax error */
        push_goal(what_next,(ptr_psi_term)TRUE,(ptr_psi_term)FALSE,(GENERIC)(level+1)); /* 20.8 */
    result=TRUE; /* 20.8 */
      }
    }
  }

  if (cut_loc) result = what_next_cut() || result;
  
  end_terminal_io();
  
  var_occurred=FALSE;
  start_chrono();
  
  return result;
}

long what_next_cut

(

)

what_next_cut

Cut away up to and including the first 'what_next' choice point.

Definition at line 1987 of file login.c.

References backtrack(), choice_stack, FALSE, goal_stack, NULL, TRUE, wl_goal::type, undo(), and what_next.

{
  long flag=TRUE;
  long result=FALSE;
  
  do {
    if (choice_stack) {
      backtrack();
      if (goal_stack->type==what_next) {
        flag=FALSE;
        result=TRUE;
      }
    }
    else {
      /* This undo does the last undo actions before returning to top level. */
      /* It is not needed for variable undoing, but for actions (like */
      /* closing windows). */
      undo(NULL);
      /* undo(mem_base); 7.8 */
#ifdef TS
      /* global_time_stamp=INIT_TIME_STAMP; */ /* 9.6 */
#endif
      flag=FALSE;
    }
  } while (flag);
  
  return result;
}

Variable Documentation

long clean_iter = 0

Definition at line 22 of file login.c.

long clean_succ = 0

Definition at line 23 of file login.c.

unsigned long global_time_stamp =INIT_TIME_STAMP

Definition at line 28 of file login.c.