module pattdefn; %Notational conveniences and low level routines for the
                 % UNIFY code.

% Author: Kevin McIsaac.
% Changes by Rainer M. Schoepf 1991.

fluid('(freevars op r p i upb
        identity expand acontract mcontract comb count symm ))$

% Binding routines.  These would be more efficient with a more direct
% mechanism.

symbolic procedure bind(u, v);         %push the value of v onto the
   put(u,'binding,v.get(u,'binding))$   %binding stack of u

symbolic procedure binding(u);              %Top most binding on stack
   (lambda x; if x then car x) get(u,'binding)$

symbolic procedure unbind(u);                  %pop binding off stack
   put(u,'binding, cdr get(u,'binding))$

symbolic procedure newenv(u);           % Mark a new environment.
   bind(u, 'unbound)$                   % Give UNIFY lexical scoping.

symbolic procedure restorenv(u);        % Should include error checks?
   unbind(u)$

symbolic procedure pm!:free(u);       % Is u a pm unbound free variable?
   binding(u) eq 'unbound$

symbolic procedure bound(u);           % Is u a pm bound free variable?
   (lambda x;  x and (x neq 'unbound)) binding u;

symbolic procedure meq(u,v);
 (lambda x; 
%    (if (x and (x neq 'unbound)) then x else u) eq meval v )
     (if (x and (x neq 'unbound)) then x else u) = v)
          binding u; 

% This has been fixed.
% symbolic procedure meval(u);
%    if eqcar(u,'minus) and numberp cadr u then -cadr u else u;


% Currently Mval does nothing.  It should be defined so that nosimp
% functions are handled properly.  By leaving it out the PM will not
% dynamically change pattern it is working on.  I.e.,
% m(f(1,2,3+c),f(?a,?b,?a+?b+?c)) will now return True.  If the code
% commented out is restored then this will give the expected result.
% However m(f(1_=natp 1),f(?a_=natp ?a)), where natp(?x) :- t, will not
% work.

symbolic procedure mval(u); u;
%===>   if not atom u then (reval bsubs(car u)) . cdr u
%===>   else bsubs u;

symbolic procedure bsubs(u);
   % Replaces free atoms by their bindings.  Would be nice to mark
   % expressions that no longer contain bunbound free variables
   if null u then u
   else if atom u then if bound(u) then binding u else u
   else for each j in u collect bsubs j;

symbolic procedure ident(op);
get(op,'identity)$

symbolic procedure genp(u);
   atom u and (get(u,'gen) or mgenp(u))$
   
symbolic procedure mgenp(u);
   atom u and get(u,'mgen)$

symbolic procedure suchp u;             %Is this a such that condition?
   not atom u and car u eq 'such!-that$

% False if any SUCH conditions are in wich all free variable are bound
% does not simplify to T.  Should we return free expressions partially
% simplified?

symbolic procedure chk u;
null u or u eq t or
(lambda x;
   if freexp(x) then 
      (lambda y; if null y then nil
                 else if y eq t then list x
                 else x.y) chk(cdr u)
   else if reval(x) eq t then chk(cdr u) else nil) bsubs car u$

symbolic procedure findnewvars u;
   if atom u then if genp u then list u else nil
    else for each j in u conc findnewvars j;

symbolic procedure freexp u;
   if atom u then pm!:free u else freexp car u or freexp cdr u;

symbolic procedure genexp u;
   if atom u then genp u else genexp car u or genexp cdr u;

endmodule;

end;
