reduce-historical/r37/packages/redlog/acfsfmisc.red

% ----------------------------------------------------------------------
% $Id: acfsfmisc.red,v 1.7 1999/04/13 13:05:33 sturm Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: acfsfmisc.red,v $
% Revision 1.7  1999/04/13 13:05:33  sturm
% Minor corrections in comments.
%
% Revision 1.6  1999/04/12 09:25:48  sturm
% Removed procedure acfsf_canegrel and acfsf_anegrel.
% Updated comments for exported procedures.
%
% Revision 1.5  1999/04/01 11:27:16  dolzmann
% Added comment for acfsf_structat.
%
% Revision 1.4  1999/03/23 08:19:21  dolzmann
% Changed copyright information.
% Added fluids for the rcsid of the file and for the copyright information.
%
% Revision 1.3  1999/03/21 13:40:39  dolzmann
% Added procedure acfsf_canegrel and acfsf_anegrel which were commented out.
%
% Revision 1.2  1997/08/24 16:18:40  sturm
% Added service rl_surep with black box rl_multsurep.
% Added service rl_siaddatl.
%
% Revision 1.1  1997/08/22 17:30:40  sturm
% Created an acfsf context based on ofsf.
%
% ----------------------------------------------------------------------
lisp <<
   fluid '(acfsf_misc_rcsid!* acfsf_misc_copyright!*);
   acfsf_misc_rcsid!* :=
      "$Id: acfsfmisc.red,v 1.7 1999/04/13 13:05:33 sturm Exp $";
   acfsf_misc_copyright!* := "Copyright (c) 1995-1999 A. Dolzmann and T. Sturm"
>>;

module acfsfmisc;
% Algebraically closed field standard form other. Submodule of [acfsf].

procedure acfsf_termprint(u);
   % Algebraically closed field term print. [u] is a
   % term. The return value is not specified. Prints [u] AM-like.
   <<
      sqprint !*f2q u where !*nat=nil;
      ioto_prin2 nil
   >>;

procedure acfsf_clnegrel(r,flg);
   % Algebraically closed field conditionally logically negate
   % relation. [r] is a relation. Returns for [flg] equal to [nil] a
   % relation $R$ such that for terms $t_1$, $t_2$ we have
   % $R(t_1,t_2)$ equivalent to $\lnot [r](t_1,t_2)$. Returns [r] for
   % non-[nil] [flg].
   if flg then r else acfsf_lnegrel r;

procedure acfsf_lnegrel(r);
   % Algebraically closed field logically negate relation. [r] is a
   % relation. Returns a relation $R$ such that for terms $t_1$, $t_2$
   % we have $R(t_1,t_2)$ equivalent to $\lnot [r](t_1,t_2)$.
   if r eq 'equal then 'neq
   else if r eq 'neq then 'equal
   else rederr {"acfsf_lnegrel: unknown operator ",r};

procedure acfsf_fctrat(atf);
   % Algebraically closed field factorize atomic formula. [atf] is an
   % atomic formula. Returns the factorized left hand side of [atf] as
   % a list $(...,(f_i . n_i),...)$, where the $f_i$ are the factors
   % as SF's and the $n_i$ are the corresponding multiplicities. The
   % integer content is dropped.
   cdr fctrf acfsf_arg2l atf;

procedure acfsf_negateat(f);
   % Algebraically closed field negate atomic formula. [f] is an
   % atomic formula. Returns an atomic formula equivalent to $\lnot
   % [f]$.
   acfsf_mkn(acfsf_lnegrel acfsf_op f,acfsf_argn f);

procedure acfsf_varlat(atform);
   % Algebraically closed field variable list of atomic formula.
   % [atform] is an atomic formula. Returns the set of variables
   % contained in [atform] as a list.
   kernels acfsf_arg2l(atform);

procedure acfsf_varsubstat(atf,new,old);
   % Algebraically closed substitute variable for variable in atomic
   % formula. [atf] is an atomic formula; [new] and [old] are
   % variables. Returns [atf] with [new] substituted for [old].
   acfsf_0mk2(acfsf_op atf,numr subf(acfsf_arg2l atf,{old . new}));

procedure acfsf_ordatp(a1,a2);
   % Algebraically closed field order predicate for atomic formulas.
   % [a1] and [a2] are atomic formulas. Returns [T] iff [a1] is
   % strictly less than [a2] wrt. some syntactical ordering; returns
   % [nil] else. The specification that [nil] is returned if
   % $[a1]=[a2]$ is used in [acfsf_subsumeandcut].
   begin scalar lhs1,lhs2;
      lhs1 := acfsf_arg2l a1;
      lhs2 := acfsf_arg2l a2;
      if lhs1 neq lhs2 then return ordp(lhs1,lhs2);
      return acfsf_ordrelp(acfsf_op a1,acfsf_op a2)
   end;

procedure acfsf_ordrelp(r1,r2);
   % Algebraically closed field standard form relation order
   % predicate. [r1] and [r2] are acfsf-relations. Returns a [T] iff
   % $[r1] <= [r2]$.
   r1 eq r2 or r1 eq 'equal;

procedure acfsf_a2cdl(atml);
   % Algebraically closed field atomic formulas to case distinction
   % lists. [atml] is a multiplicity list of atomic formulas. Returns
   % a list $(...,(t_i = 0, t_i \neq 0),...)$ of case distinctions
   % lists, where the $t_i$ are the right hand side terms of the
   % atomic formulas in [atml].
   begin scalar x;
      return for each pr in atml collect <<
	 x := acfsf_arg2l car pr;
	 {acfsf_0mk2('equal,x),acfsf_0mk2('neq,x)}
      >>
   end;

procedure acfsf_t2cdl(term);
   % Algebraically closed field term to case distinction list. [term]
   % is a term. Returns a case distinction list $([term] = 0, [term]
   % \neq 0)$ wrt. [term].
   {acfsf_0mk2('equal,term),acfsf_0mk2('neq,term)};

procedure acfsf_subat(al,f);
   % Algebraically closed field substitute into atomic formula. [al]
   % is an ALIST $(..., (v_i . t_i), ...)$, where the $v_i$ are
   % kernels, and the $t_i$ are Lisp prefix terms; [f] is an atomic
   % formula. Returns [f] with $t_i$ substituted for each occurrence
   % of $v_i$. The $t_i$ must be such that the substitution does not
   % yield parametric denominators.
   begin scalar nlhs;
      nlhs := subf(acfsf_arg2l f,al);
      if not domainp denr nlhs then
	 rederr "parametric denominator after substitution";
      return acfsf_0mk2(acfsf_op f,numr nlhs)
   end;

procedure acfsf_subalchk(al);
   % Algebraically closed field substitution ALIST check. [al] is an
   % ALIST $(..., (v_i . t_i), ...)$, where the $v_i$ are kernels, and
   % the $t_i$ are Lisp prefix terms. The return value is unspecified.
   % Raises an error if some $t_i$ contains a parametric denominator.
   for each x in al do
      if not domainp denr simp cdr x then
	 rederr "parametric denominator in substituted term";

procedure acfsf_eqnrhskernels(x);
   % Algebraically closed field equation right hand side kernels. [x]
   % is an equation. Returns the set of kernels contained in the right
   % hand side of [x] as a list.
   nconc(kernels numr w,kernels denr w) where w=simp cdr x;

procedure acfsf_getineq(f,bvl);
   % Algebraically closed field generate theory get inequalities. [f]
   % is a formula; [bvl] is a list of variables. Returns the list of
   % all inequalities occuring in [f] that do not contain any of the
   % variables in [bvl].
   begin scalar atml,atf,cdl;
      atml := cl_atml f;
      while atml do <<
         atf := caar atml;
         atml := cdr atml;
	 if acfsf_op atf eq 'neq and
	    null intersection(bvl, kernels acfsf_arg2l atf) then
	    cdl := atf . cdl
      >>;
      return cdl
   end;

procedure acfsf_structat(at,al);
   % Algebraically closed field structure of an atomic formula. [at]
   % is an atomic formula $R(t,0)$; [al] is an ALIST. Returns an
   % atomic formula. [al] is of the form $(..., (t_i . v_i), ...)$,
   % where the $t_i$ are SF's and the $v_i$ are variables. The left
   % hand side $t$ of [at] matches one of the $t_i$ in [al]. Returns
   % the atomic formula $R(v_i,0)$.
   begin scalar lhs;
      lhs := acfsf_arg2l at;
      if domainp lhs then
	 return at;
      return acfsf_0mk2(acfsf_op at, numr simp cdr assoc(lhs,al))
   end;

procedure acfsf_ifstructat(at,al);
   % Algebraically closed field irreducible factor structure of an
   % atomic formula. [at] is an atomic formula $R(t,0)$ where $t = c
   % ... s_j ...$ is a factorization of $t$ into irreducible factors;
   % [al] is an ALIST. Returns an atomic formula. [al] is of the form
   % $(..., (t_i . v_i), ...)$, where the $t_i$ are SF's and the $v_i$
   % are variables. Each factor $s_j$ of the left hand side $t$ of
   % [at] matches one of the $t_i$ in [al]. Returns the atomic formula
   % $R(c ... v_i ..., 0)$.
   begin scalar w,r;
      w := fctrf acfsf_arg2l at;
      r := car w;
      for each x in cdr w do
	 r := multf(r,expf(numr simp cdr assoc(car x,al),cdr x));
      return acfsf_0mk2(acfsf_op at,r)
   end;

procedure acfsf_termmlat(at);
   % Algebraically closed field term multiplicity list of atomic
   % formula. [at] is an atomic formula. Returns the multiplicity list
   % of all non-zero terms in [at].
   if acfsf_arg2l at then
      {(acfsf_arg2l at . 1)};

procedure acfsf_decdeg(f);
   % Algebraically closed field decrease degrees. [f] is a formula.
   % Returns a formula equivalent to [f], hopefully decreasing the
   % degrees of the bound variables.
   acfsf_decdeg0 cl_rename!-vars f;

procedure acfsf_decdeg0(f);
   begin scalar op,w,gamma,newmat;
      op := rl_op f;
      if rl_boolp op then
	 return rl_mkn(op,for each subf in rl_argn f collect
   	    acfsf_decdeg0 subf);
      if rl_quap op then
	 return rl_mkq(op,rl_var f,
	    car acfsf_decdeg1(acfsf_decdeg0 rl_mat f,{rl_var f}));
      % [f] is not complex.
      return f
   end;

procedure acfsf_decdeg1(f,vl);
   % Algebraically closed field decrease degrees. [f] is a formula;
   % [vl] is either a list of variables $v$ that do not occur boundly
   % in [f], or the identifier [fvarl]. Returns a pair $(\phi . l)$;
   % $l$ is a list of pairs $(..., (v_i . d_i), ...)$, with $v_i \in
   % [vl]$ and integer $d_i$; $\phi$ is obtained from [f] by replacing
   % powers $v_i^{d_i}$ by $v_i$. We have $\exists [vl] ([f])$
   % equivalent to $\exists [vl] (\phi)$. [fvarl] selects the list of
   % all free variables in [f] as [vl].
   begin scalar dvl; integer n;
      if vl eq 'fvarl then
	 vl := cl_fvarl1 f;
      for each v in vl do <<
	 n := acfsf_decdeg2(f,v);
	 if n>1 then <<
	    f := acfsf_decdeg3(f,v,n);
	    dvl := (v . n) . dvl
	 >>
      >>;
      return f . dvl
   end;

procedure acfsf_decdeg2(f,v);
   % Algebraically closed field standard form decrement degree
   % subroutine. [f] is a formula; [v] is a variable. Returns an
   % INTEGER $n$. The degree of [v] in [f] can be decremented using
   % the substitution $[v]^n=v$.
   begin scalar a,w,atl,dgcd,!*gcd,oddp;
      !*gcd := T;
      atl := cl_atl1 f;
      dgcd := 0;
      while atl and dgcd neq 1 do <<
	 a := car atl;
	 atl := cdr atl;
	 w := acfsf_ignshift(a,v);
	 if null w then <<  % [w neq 'ignore]
	    a := sfto_reorder(acfsf_arg2l a,v);
	    while (not domainp a) and (mvar a eq v) and dgcd neq 1 do <<
	       dgcd := gcdf(dgcd,ldeg a);
	       a := red a
	    >>
      	 >>
      >>;
      if dgcd = 0 then
	 return 1;
      return dgcd
   end;

procedure acfsf_ignshift(at,v);
   % Orderd field standard form ignore shift. [at] is an atomic
   % formula; [v] is a variable. Returns [nil] or ['ignore].
   begin scalar w;
      w := sfto_reorder(acfsf_arg2l at,v);
      if not domainp w and null red w and mvar w eq v then
	 return 'ignore
   end;

procedure acfsf_decdeg3(f,v,n);
   % Algebraically closed field standard form decrement degree. [f] is
   % a formula; [v] is a variable; [n] is an integer. Returns a
   % formula.
   cl_apply2ats1(f,'acfsf_decdegat,{v,n});

procedure acfsf_decdegat(atf,v,n);
   % Algebraically closed field standard form decrement degree atomic
   % formula. [f] is an atomic formula; [v] is a variable; [n] is an
   % integer. Returns an atomic formula.
   if acfsf_ignshift(atf,v) then
      atf
   else
      acfsf_0mk2(acfsf_op atf,sfto_decdegf(acfsf_arg2l atf,v,n));

procedure acfsf_multsurep(at,atl);
   % Algebraically closed field multplicative sure predicate. [at] is
   % an atomic formula; [atl] is a theory. Tries to prove [at] wrt.
   % [atl]. Returns non-[nil] in case of success.
   if acfsf_op at eq 'equal then
      acfsf_multsurep!-equal(at,atl)
   else
      acfsf_multsurep!-neq(at,atl);

procedure acfsf_multsurep!-equal(at,atl);
   begin scalar c,a;
      c := acfsf_arg2l at;
      while atl do <<
	 a := car atl;
	 atl := cdr atl;
	 if acfsf_op a eq 'equal and quotf(c,acfsf_arg2l a) then <<
	    a := 'found;
	    atl := nil
	 >>
      >>;
      return a eq 'found
   end;

procedure acfsf_multsurep!-neq(at,atl);
   begin scalar c,a;
      c := acfsf_arg2l at;
      while atl do <<
	 a := car atl;
	 atl := cdr atl;
	 if acfsf_op a eq 'neq and quotf(acfsf_arg2l a,c) then <<
	    a := 'found;
	    atl := nil
	 >>
      >>;
      return a eq 'found
   end;

endmodule;  % [acfsfmisc]

end;  % of file