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

% ----------------------------------------------------------------------
% $Id: acfsf.red,v 1.9 1999/04/12 09:25:48 sturm Exp $
% ----------------------------------------------------------------------
% Copyright (c) 1995-1999 Andreas Dolzmann and Thomas Sturm
% ----------------------------------------------------------------------
% $Log: acfsf.red,v $
% Revision 1.9  1999/04/12 09:25:48  sturm
% Removed procedure acfsf_canegrel and acfsf_anegrel.
% Updated comments for exported procedures.
%
% Revision 1.8  1999/04/04 19:01:52  sturm
% Added fluid declaration for !*gbverbose.
%
% Revision 1.7  1999/03/23 12:26:29  sturm
% Renamed switch rlsisqf to rlsiatadv.
%
% Revision 1.6  1999/03/23 07:54:31  dolzmann
% Changed copyright information.
% Added list of exported procedures and import list.
% Added fluids for the rcsid of the file and for the copyright information.
%
% Revision 1.5  1999/03/21 13:33:02  dolzmann
% Registered acfsf_getineq as the black box implementation for rl_getineq.
% Use cl_bnfsimpl instead of acfsf_bnfsimpl.
% Removed black box rl_zero.
% Added service rlthsimpl.
% Registered service rlqeipo.
% Registered service rlgentheo.
%
% Revision 1.4  1997/10/02 13:14:39  sturm
% The CGB switches have been renamed from gcgb... to cgb...
%
% Revision 1.3  1997/10/01 11:13:42  dolzmann
% Added service rlqe.
%
% Revision 1.2  1997/08/24 16:18:39  sturm
% Added service rl_surep with black box rl_multsurep.
% Added service rl_siaddatl.
%
% Revision 1.1  1997/08/22 17:30:37  sturm
% Created an acfsf context based on ofsf.
%
% ----------------------------------------------------------------------
lisp <<
   fluid '(acfsf_rcsid!* acfsf_copyright!*);
   acfsf_rcsid!* := "$Id: acfsf.red,v 1.9 1999/04/12 09:25:48 sturm Exp $";
   acfsf_copyright!* := "Copyright (c) 1995-1999 A. Dolzmann and T. Sturm"
>>;

module acfsf;
% Algebraically closed field standard form. Main module. Algorithms on
% first-order formulas over algebraically closed fields. The language
% contains binary relations ['equal], ['neq].

create!-package(
   '(acfsf acfsfsiat acfsfsism acfsfbnf acfsfgs acfsfmisc acfsfqe),nil);

load!-package 'rltools;
load!-package 'cl;
load!-package 'cgb;

exports acfsf_simpterm,acfsf_prepat,acfsf_resimpat,acfsf_lengthat,
   acfsf_chsimpat,acfsf_simpat,acfsf_op,acfsf_arg2l,acfsf_arg2r,acfsf_argn,
   acfsf_mk2,acfsf_0mk2,acfsf_mkn,acfsf_opp,acfsf_simplat1,acfsf_smrmknowl,
   acfsf_smcpknowl,acfsf_smupdknowl,acfsf_smmkatl,acfsf_dnf,acfsf_cnf,
   acfsf_subsumption,acfsf_sacatlp,acfsf_sacat,acfsf_gsc,acfsf_gsd,acfsf_gsn,
   acfsf_gssimplify,acfsf_gssimplify0,acfsf_termprint,acfsf_clnegrel,
   acfsf_lnegrel,acfsf_fctrat,acfsf_negateat,
   acfsf_varlat,acfsf_varsubstat,acfsf_ordatp,acfsf_a2cdl,acfsf_t2cdl,
   acfsf_subat,acfsf_subalchk,acfsf_eqnrhskernels,acfsf_getineq,acfsf_structat,
   acfsf_ifstructat,acfsf_termmlat,acfsf_decdeg,acfsf_decdeg1,acfsf_multsurep,
   acfsf_gqe,acfsf_qe,acfsf_thsimpl;

imports rltools,cl,cgb;

fluid '(!*rlsiatadv !*rlsiexpl !*rlsiexpla !*rlgssub !*rlsiso !*rlgsrad
   !*rlgsred !*rlgsprod !*rlgserf !*rlverbose !*rlsifac !*rlbnfsac !*rlgsvb
   !*rlgsbnf !*rlgsutord !*rlnzden !*rladdcond !*rlqegen !*cgbgen !*cgbreal
   !*gbverbose);

flag('(acfsf),'rl_package);

% Parameters
put('acfsf,'rl_params,'(
   (rl_subat!* . acfsf_subat)
   (rl_subalchk!* . acfsf_subalchk)
   (rl_eqnrhskernels!* . acfsf_eqnrhskernels)
   (rl_ordatp!* . acfsf_ordatp)
   (rl_simplat1!* . acfsf_simplat1)
   (rl_smupdknowl!* . acfsf_smupdknowl)
   (rl_smrmknowl!* . acfsf_smrmknowl)
   (rl_smcpknowl!* . acfsf_smcpknowl)
   (rl_smmkatl!* . acfsf_smmkatl)
   (rl_smsimpl!-impl!* . cl_smsimpl!-impl)
   (rl_smsimpl!-equiv1!* . cl_smsimpl!-equiv1)
   (rl_negateat!* . acfsf_negateat)
   (rl_varlat!* . acfsf_varlat)
   (rl_varsubstat!* . acfsf_varsubstat)
   (rl_subsumption!* . acfsf_subsumption)
   (rl_bnfsimpl!* . cl_bnfsimpl)
   (rl_sacat!* . acfsf_sacat)
   (rl_sacatlp!* . acfsf_sacatlp)
   (rl_fctrat!* . acfsf_fctrat)
   (rl_tordp!* . ordp)
   (rl_a2cdl!* . acfsf_a2cdl)
   (rl_t2cdl!* . acfsf_t2cdl)
   (rl_getineq!* . acfsf_getineq)
   (rl_structat!* . acfsf_structat)
   (rl_ifstructat!* . acfsf_ifstructat)
   (rl_termmlat!* . acfsf_termmlat)
   (rl_multsurep!* . acfsf_multsurep)));

% Services
put('acfsf,'rl_services,'(
   (rl_subfof!* . cl_subfof)
   (rl_identifyonoff!* . cl_identifyonoff)
   (rl_simpl!* . cl_simpl)
   (rl_thsimpl!* . acfsf_thsimpl)
   (rl_nnf!* . cl_nnf)
   (rl_nnfnot!* . cl_nnfnot)
   (rl_pnf!* . cl_pnf)
   (rl_cnf!* . acfsf_cnf)
   (rl_dnf!* . acfsf_dnf)
   (rl_all!* . cl_all)
   (rl_ex!* . cl_ex)
   (rl_atnum!* . cl_atnum)
   (rl_tab!* . cl_tab)
   (rl_atab!* . cl_atab)
   (rl_itab!* . cl_itab)
   (rl_gsc!* . acfsf_gsc)
   (rl_gsd!* . acfsf_gsd)
   (rl_gsn!* . acfsf_gsn)
   (rl_ifacl!* . cl_ifacl)
   (rl_ifacml!* . cl_ifacml)
   (rl_matrix!* . cl_matrix)
   (rl_apnf!* . cl_apnf)
   (rl_atml!* . cl_atml)
   (rl_tnf!* . cl_tnf)
   (rl_atl!* . cl_atl)
   (rl_struct!* . cl_struct)
   (rl_ifstruct!* . cl_ifstruct)
   (rl_termml!* . cl_termml)
   (rl_terml!* . cl_terml)
   (rl_varl!* . cl_varl)
   (rl_fvarl!* . cl_fvarl)
   (rl_bvarl!* . cl_bvarl)
   (rl_gentheo!* . cl_gentheo)
   (rl_decdeg!* . acfsf_decdeg)
   (rl_decdeg1!* . acfsf_decdeg1)
   (rl_surep!* . cl_surep)
   (rl_qe!* . acfsf_qe)
   (rl_qeipo!* . cl_qeipo)
   (rl_siaddatl!* . cl_siaddatl)));

% Admin
put('acfsf,'simpfnname,'acfsf_simpfn);
put('acfsf,'simpdefault,'acfsf_simprel);

put('acfsf,'rl_prepat,'acfsf_prepat);
put('acfsf,'rl_resimpat,'acfsf_resimpat);
put('acfsf,'rl_lengthat,'acfsf_lengthat);

put('acfsf,'rl_prepterm,'prepf);
put('acfsf,'rl_simpterm,'acfsf_simpterm);

algebraic infix equal;
put('equal,'acfsf_simpfn,'acfsf_chsimpat);
put('equal,'number!-of!-args,2);

algebraic infix neq;
put('neq,'acfsf_simpfn,'acfsf_chsimpat);
put('neq,'number!-of!-args,2);
put('neq,'rtypefn,'quotelog);
newtok '((!< !>) neq);

flag('(equal neq),'spaced);
flag('(acfsf_chsimpat),'full);

procedure acfsf_simpterm(u);
   % Algebraically closed field simp term. [u] is Lisp Prefix. Returns
   % the [u] as an ACFSF term.
   numr simp u;

procedure acfsf_prepat(f);
   % Algebraically closed field prep atomic formula. [f] is an ACFSF
   % atomic formula. Returns [f] in Lisp prefix form.
   {acfsf_op f,prepf acfsf_arg2l f,prepf acfsf_arg2r f};

procedure acfsf_resimpat(f);
   % Algebraically closed field resimp atomic formula. [f] is an ACFSF
   % atomic formula. Returns the atomic formula [f] with resimplified
   % terms.
   acfsf_mk2(acfsf_op f,
      numr resimp !*f2q acfsf_arg2l f,numr resimp !*f2q acfsf_arg2r f);

procedure acfsf_lengthat(f);
   % Algebraically closed field length of atomic formula. [f] is an
   % atomic formula. Returns a number, the length of [f].
   2;

procedure acfsf_chsimpat(u);
   % Algebraically closed field chain simp atomic formula. [u] is the
   % Lisp prefix representation of a chain of atomic formulas, i.e.,
   % the operators are nested right associatively. Returns a formula,
   % which is the corresponding conjunction.
   rl_smkn('and,for each x in acfsf_chsimpat1 u collect acfsf_simpat x);

procedure acfsf_chsimpat1(u);
   % Algebraically closed field chain simp atomic formula. [u] is the
   % Lisp prefix representation of a chain of atomic formulas, i.e.,
   % the operators are nested right associatively.
   begin scalar leftl,rightl,lhs,rhs;
      lhs := cadr u;
      if pairp lhs and acfsf_opp car lhs then <<
	 leftl := acfsf_chsimpat1 lhs;
	 lhs := caddr lastcar leftl
      >>;
      rhs := caddr u;
      if pairp rhs and acfsf_opp car rhs then <<
	 rightl := acfsf_chsimpat1 rhs;
	 rhs := cadr car rightl
      >>;
      return nconc(leftl,{car u,lhs,rhs} . rightl)
   end;

procedure acfsf_simpat(u);
   % Algebraically closed field simp atomic formula. [u] is Lisp
   % prefix. Returns [u] as an atomic formula.
   begin scalar op,lhs,rhs,nlhs,f;
      op := car u;
      lhs := simp cadr u;
      if not (!*rlnzden or (domainp denr lhs)) then
 	 typerr(u,"atomic formula");
      rhs := simp caddr u;
      if not (!*rlnzden or (domainp denr rhs)) then
 	 typerr(u,"atomic formula");
      lhs := subtrsq(lhs,rhs);
      nlhs := numr lhs;
      if !*rlnzden and not domainp denr lhs then <<
	 f := acfsf_0mk2(op,nlhs);
	 if !*rladdcond then
	    f := rl_mkn('and,{acfsf_0mk2('neq,denr lhs),f});
	 return f
      >>;
      return acfsf_0mk2(op,nlhs)
   end;

procedure acfsf_op(atf);
   % Algebraically closed field operator. [atf] is an atomic formula
   % $R(t_1,t_2)$. Returns $R$.
   car atf;

procedure acfsf_arg2l(atf);
   % Algebraically closed field binary operator left hand side
   % argument. [atf] is an atomic formula $R(t_1,t_2)$. Returns $t_1$.
   cadr atf;

procedure acfsf_arg2r(atf);
   % Algebraically closed field binary operator right hand side
   % argument. [atf] is an atomic formula $R(t_1,t_2)$. Returns $t_2$.
   caddr atf;

procedure acfsf_argn(atf);
   % Algebraically closed field n-ary operator argument list. [atf] is
   % an atomic formula $R(t_1,t_2)$. Returns the list $(t_1,t_2)$.
   {cadr atf,caddr atf};

procedure acfsf_mk2(op,lhs,rhs);
   % Algebraically closed field make atomic formula for binary
   % operator. [op] is a relation; [lhs] and [rhs] are terms. Returns
   % the atomic formula $[op]([lhs],[rhs])$.
   {op,lhs,rhs};

procedure acfsf_0mk2(op,lhs);
   % Algebraically closed field make zero right hand side atomic
   % formula for binary operator. [op] is a relation [lhs] is a term.
   % Returns the atomic formula $[op]([lhs],0)$.
   {op,lhs,nil};

procedure acfsf_mkn(op,argl);
   % Algebraically closed field make atomic formula for n-ary
   % operator. [op] is a relation; [argl] is a list $(t_1,t_2)$ of
   % terms. Returns the atomic formula $[op](t_1,t_2)$.
   {op,car argl,cadr argl};

procedure acfsf_opp(op);
   % Algebraically closed field operator predicate. [op] is an
   % S-expression. Returns non-[nil] iff op is a relation.
   op memq '(equal neq);

endmodule;  % [acfsf]

end;  % of file