~trn/reduce-algebra

ca0a978446aec2d947dcc6834c6c4d21c8a84ff1 — Jeffrey H. Johnson 4 days ago d0317fb + fa54849
Merge branch 'svn/trunk'
M packages/redlog/cl/clqenew.red => packages/redlog/cl/clqenew.red +5 -5
@@ 70,7 70,7 @@ asserted procedure qedb_new(): Vector;
      return db
   end;

procedure qedb_print(db: Vector): Vector;
asserted procedure qedb_print(db: Vector): Vector;
   begin scalar !*nat;
      ioto_tprin2t {"{"};
      ioto_tprin2t {"    TypeTag:               ", getv(db, QEDB_TAG)};


@@ 92,7 92,7 @@ procedure qedb_print(db: Vector): Vector;
      return db
   end;

procedure qedb_verbosePrint(db: Vector): Vector;
asserted procedure qedb_verbosePrint(db: Vector): Vector;
   begin scalar !*nat;
      ioto_tprin2t {"{"};
      ioto_tprin2t {"    TypeTag:                ", getv(db, QEDB_TAG)};


@@ 221,7 221,7 @@ asserted procedure qeco_add(co: Container, new: NodeL): Container;
         return co;
      nodes := getv(co, 1);
      if getv(co, 3) eq 'bfs then <<
         lastNode := getv(co ,2);
         lastNode := getv(co, 2);
         if null lastNode then
            lastNode := nodes := {pop new};
         for each node in new do


@@ 355,7 355,7 @@ asserted procedure cl_qe1_new(db: Vector): Vector;
      qedb_setFormula(db, f);
      if null blocks then <<
         % TS has moved this down a bit. There are no quantifiers left after
         % initial simplification.  Note the remark before that
         % initial simplification. Note the remark before that
         % simplification! We are here at a point where the formula and the
         % theory have been set properly in the db. However, the answer is
         % still undefined. Recall that the semantics of the answer depends


@@ 377,7 377,7 @@ asserted procedure cl_qe1_new(db: Vector): Vector;
            % We have finished or at least reached the outmost block.
            answer := for each node in append(qedb_getSuccessNodes(db), qedb_getFailureNodes(db)) collect <<
               point := rl_qemkans(ce_ans(node), qedb_getLastBlockInputFormula(db))
                        where !*rlqestdans=(qedb_getAnswerMode(db) eq 'standard);
                        where !*rlqestdans = (qedb_getAnswerMode(db) eq 'standard);
               cl_unsplit_new(blocks, ce_f(node)) . point
            >>
         >> else

M packages/redlog/mri/mri.red => packages/redlog/mri/mri.red +2 -0
@@ 82,6 82,8 @@ put('mri,'rl_services,'(
put('mri,'rl_simpb,'pasf_simpb);
put('mri,'rl_resimpb,'pasf_resimpb);
put('mri,'rl_prepb,'pasf_prepb);
put('mri,'rl_pribq,'pasf_pribq);
put('mri,'rl_fancy!-pribq,'pasf_fancy!-pribq);

put('mri,'simpfnname,'mri_simpfn);
put('mri,'rl_prepat,'mri_prepat);

M packages/redlog/pasf/pasf.red => packages/redlog/pasf/pasf.red +7 -111
@@ 33,8 33,8 @@ copyright('pasf, "(c) 2002-2009 A. Dolzmann, A. Seidl, T. Sturm, 2010-2017 T. St
% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
%

create!-package('(pasf pasfbnf pasfmisc pasfnf pasfsiat pasfsibq pasfbqbb
   pasfqe pasfsusi pasfresolve), nil);
create!-package('(pasf pasfprint pasfbnf pasfmisc pasfnf pasfsiat pasfsibq
   pasfbqbb pasfqe pasfsusi pasfresolve), nil);

fluid '(!*rlnzden !*rlposden !*rladdcond !*rlqeasri !*rlsifac !*rlbrkcxk !*utf8);



@@ 188,7 188,7 @@ put('pasf,'rl_services,'(

put('pasf,'rl_simpb,'pasf_simpb);

asserted procedure pasf_simpb(u, x: Id, m: Formula): Formula;
asserted procedure pasf_simpb(u, x: Kernel): Formula;
   % Simp bound. Do not confuse with "simp bounded quantifer". redlog/rlami
   % knows about bounded quantifiers but the bounds are context-specific,
   % like atomic formulas. u is the unsimped bound. We also receive the


@@ 204,19 204,19 @@ asserted procedure pasf_simpb(u, x: Id, m: Formula): Formula;

put('pasf,'rl_resimpb,'pasf_resimpb);

asserted procedure pasf_resimpb(u: Formula): Formula;
asserted procedure pasf_resimpb(b: Formula): Formula;
   % Resimp bound. Do not confuse with "resimp bounded quantifer".
   % redlog/rlami knows about bounded quantifiers but the bounds are
   % context-specific, like atomic formulas.
   rl_resimp u;
   rl_resimp b;

put('pasf,'rl_prepb,'pasf_prepb);

asserted procedure pasf_prepb(u: Formula): LispPrefixForm;
asserted procedure pasf_prepb(b: Formula): LispPrefixForm;
   % Prep bound. Do not confuse with "prep bounded quantifer". redlog/rlami
   % knows about bounded quantifiers but the bounds are context-specific,
   % like atomic formulas.
   rl_prepfof u;
   rl_prepfof b;

put('pasf,'simpfnname,'pasf_simpfn);
put('pasf,'rl_prepat,'pasf_prepat);


@@ 235,50 235,36 @@ put('neq,'pasf_simpfn,'pasf_chsimpat);
put('neq,'number!-of!-args,2);
put('neq,'rtypefn,'quotelog);
newtok '((!< !>) neq);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('neq,'fancy!-infix!-symbol,"\,\neq\, ");

algebraic infix leq;
put('leq,'pasf_simpfn,'pasf_chsimpat);
put('leq,'number!-of!-args,2);
put('leq,'rtypefn,'quotelog);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('leq,'fancy!-infix!-symbol,"\,\leq\, ");

algebraic infix geq;
put('geq,'pasf_simpfn,'pasf_chsimpat);
put('geq,'number!-of!-args,2);
put('geq,'rtypefn,'quotelog);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('geq,'fancy!-infix!-symbol,"\,\geq\, ");

algebraic infix lessp;
put('lessp,'pasf_simpfn,'pasf_chsimpat);
put('lessp,'number!-of!-args,2);
put('lessp,'rtypefn,'quotelog);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('lessp,'fancy!-infix!-symbol,"\,<\, ");

algebraic infix greaterp;
put('greaterp,'pasf_simpfn,'pasf_chsimpat);
put('greaterp,'number!-of!-args,2);
put('greaterp,'rtypefn,'quotelog);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('greaterp,'fancy!-infix!-symbol,"\,>\, ");

algebraic operator cong;
put('cong,'prifn,'pasf_pricong);
put('cong,'pasf_simpfn,'pasf_simpat);
put('cong,'number!-of!-args,3);
put('cong,'rtypefn,'quotelog);
put('cong,'fancy!-prifn,'pasf_fancy!-pricong);

algebraic operator ncong;
put('ncong,'prifn,'pasf_princong);
put('ncong,'pasf_simpfn,'pasf_simpat);
put('ncong,'number!-of!-args,3);
put('ncong,'rtypefn,'quotelog);
put('ncong,'fancy!-prifn,'pasf_fancy!-pricong);

algebraic operator rnd;
put('rnd,'simpfn,'pasf_simprnd);


@@ 390,96 376,6 @@ procedure pasf_mkrndf(u,key);
   % [u] is an SF; [key] is an interned identifier. Returns an SF.
   numr simp {'rnd,prepf u,key};

procedure pasf_pricong(l);
   % Presburger arithmetic standard form print a congruence. [l] is a lisp
   % prefix. Returns 'failed iff printing failed.
   if null !*nat then
      'failed
   else if !*utf8 then
      pasf_gpricong l
   else <<
      maprin cadr l;
      prin2!* " ~";
      maprin cadddr l;
      prin2!* "~ ";
      maprin caddr l
   >>;

procedure pasf_gpricong(l);
   if numberp cadddr l then <<
      maprin cadr l;
      prin2!* " ";
      prin2!* intern compress nconc(explode car l,explode cadddr l);
      prin2!* " ";
      maprin caddr l
   >> else <<
      maprin cadr l;
      prin2!* " ";
      prin2!* car l;
      prin2!* " ";
      maprin caddr l;
      prin2!* " mod ";
      maprin cadddr l
   >>;

procedure pasf_princong(l);
   % Presburger arithmetic standard form print an incongruence. [l] is a lisp
   % prefix. Returns 'failed iff printing failed.
   if null !*nat then
      'failed
   else if !*utf8 then
      pasf_gpricong l
   else <<
      maprin cadr l;
      prin2!* " #";
      maprin cadddr l;
      prin2!* "# ";
      maprin caddr l
   >>;

procedure pasf_fancy!-pricong(l);
   % Presburger arithmetic standard form texmacs print a congruence. [l] is a
   % lisp prefix. Returns 'failed iff printing failed.
   if rl_texmacsp() or 'csl memq lispsystem!* then
      pasf_fancy!-pricong!-texmacs l
   else
      pasf_fancy!-pricong!-fm l;

procedure pasf_fancy!-pricong!-texmacs(l);
   % Presburger arithmetic standard form texmacs print a congruence. [l] is a
   % lisp prefix. Returns 'failed iff printing failed.
   if null !*nat then
      'failed
   else <<
      maprin cadr l; % lhs
      if car l eq 'cong then
         fancy!-prin2 "\,\equiv"
      else
         fancy!-prin2 "\,\not\equiv";
      fancy!-prin2!-underscore();
      fancy!-prin2 "{";
      maprin cadddr l; % modulus
      fancy!-prin2 "}\,";
      maprin caddr l; % rhs
   >>;

procedure pasf_fancy!-pricong!-fm(l);
   % Presburger arithmetic standard form texmacs print a congruence. [l] is a
   % lisp prefix. Returns 'failed iff printing failed.
   if null !*nat then
      'failed
   else <<
      maprin cadr l;
      if car l eq 'cong then
         fancy!-special!-symbol(186,2)
      else
         fancy!-special!-symbol(187,2);
      maprin caddr l;
      fancy!-prin2 " (";
      maprin cadddr l;
      fancy!-prin2 ")"
   >>;

procedure pasf_verbosep();
   % Presburger arithmetic standard form verbose switch. Returns t iff the
   % main switch rlverbose is on and the switch rlpasfvb is on.

A packages/redlog/pasf/pasfprint.red => packages/redlog/pasf/pasfprint.red +342 -0
@@ 0,0 1,342 @@
module pasfprint;

revision('pasfprint, "$Id$");

copyright('pasfprint, "(c) 2021 T. Sturm");

% Redistribution and use in source and binary forms, with or without
% modification, are permitted provided that the following conditions
% are met:
%
%    * Redistributions of source code must retain the relevant
%      copyright notice, this list of conditions and the following
%      disclaimer.
%    * Redistributions in binary form must reproduce the above
%      copyright notice, this list of conditions and the following
%      disclaimer in the documentation and/or other materials provided
%      with the distribution.
%
% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
% "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
% LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
% A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
% SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
% DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
% THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
% (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
%

put('pasf, 'rl_pribq, 'pasf_pribq);

switch rlpribqsm;
on1 'rlpribqsm;

asserted procedure pasf_pribq(f: LispPrefixForm): Void;
   % Print bound. We are called from rlprint/rl_pribq(). The variable v has
   % been printed already, and we are currently inside square brackets, where
   % we must print the bound b.
   begin
      if null !*nat then
        return 'failed;
      maprin car f;
      prin2!* " ";
      maprin cadr f;
      prin2!* " ";
      prin2!* "[";
      if !*rlpribqsm then
         maprin pasf_boundsm(caddr f, cadr f)
      else
         maprin caddr f;
      prin2!* "] ";
      prin2!* "(";
      maprin cadddr f;
      prin2!* ")"
   end;

asserted procedure pasf_boundsm(f: LispPrefixForm, v: Kernel): LispPrefixForm;
   begin scalar w, w1, w2, argl;
      if eqcar(f, 'or) then <<
         w := 'or . for each x in cdr f collect pasf_boundsm(x, v);
         return pasf_boundsmTryAbs w
      >>;
      argl := rl_argn f;
      if cddr argl then
         return f;
      w1 := pasf_boundsm1(car argl, v);
      if null w1 then
         return f;
      w2 := pasf_boundsm1(cadr argl, v);
      if null w2 then
         return f;
      if car w1 eq car w2 then
         return f;
      if eqcar(w1, 'ub) then <<
         w := w1;
         w1 := w2;
         w2 := w
      >>;
      w1 := cdr w1;
      w2 := cdr w2;
      if car(w1) neq car(w2) then
         if car(w1) eq 'leq then << % <= v <
            caddr w2 := reval {'plus, caddr w2, {'minus, 1}};
            car w2 := 'leq
         >>
         else << % < v <=
            cadr w1 := reval {'plus, cadr w1, 1};
            car w1 := 'leq
         >>;
      return nconc(w1, {caddr w2})
   end;

asserted procedure pasf_boundsm1(a: LispPrefixForm, v: Kernel): DottedPair;
   begin scalar w, c;
      if car a memq '(geq greaterp) then
         a := {pasf_anegrel car a, {'minus, cadr a}, 0};
      w := sfto_reorder(numr simp cadr a, v);
      if not domainp w and mvar w eq v then
         c := lc w;
      if car a memq '(leq lessp) and c = 1 then
         return 'ub . {car a, v, prepf negf red w};
      if car a memq '(leq lessp) and c = -1 then
         return 'lb . {car a, prepf red w, v}
   end;

asserted procedure pasf_boundsmTryAbs(f: LispPrefixForm): LispPrefixForm;
   begin scalar w, v, r1, r2, l1, l2, u1, u2;
      w := cdr f;
      if cddr w then
         return f;
      if length car w neq 4 or length cadr w neq 4 then
         return f;
      r1 := car car w;
      r2 := car cadr w;
      if r1 neq r2 or r1 eq 'cong then
         return f;
      l1 := numr simp cadr car w;
      v := caddr car w;
      u1 := numr simp cadddr car w;
      l2 := numr simp cadr cadr w;
      u2 := numr simp cadddr cadr w;
      if l1 = u2 and l2 = u1 and l1 = negf u1 and l2 = negf u2 then
         return {r1, {'minus, {'abs, prepf absf l1}}, v, {'abs, prepf absf u1}};
      return f
   end;

put('cong,'prifn,'pasf_pricong);

asserted procedure pasf_pricong(l: LispPrefixForm);
   % Presburger arithmetic standard form print a congruence.
   if null !*nat then
      'failed
   else if !*utf8 then
      pasf_pricongUtf8 l
   else <<
      maprin cadr l;
      prin2!* " ~";
      maprin cadddr l;
      prin2!* "~ ";
      maprin caddr l
   >>;

asserted procedure pasf_pricongUtf8(l: LispPrefixForm);
   if numberp cadddr l then <<
      maprin cadr l;
      prin2!* " ";
      prin2!* intern compress nconc(explode car l,explode cadddr l);
      prin2!* " ";
      maprin caddr l
   >> else <<
      maprin cadr l;
      prin2!* " ";
      prin2!* car l;
      prin2!* " ";
      maprin caddr l;
      prin2!* " mod ";
      maprin cadddr l
   >>;

put('ncong,'prifn,'pasf_princong);

asserted procedure pasf_princong(l: LispPrefixForm);
   % Presburger arithmetic standard form print an incongruence.
   if null !*nat then
      'failed
   else if !*utf8 then
      pasf_pricongUtf8 l
   else <<
      maprin cadr l;
      prin2!* " #";
      maprin cadddr l;
      prin2!* "# ";
      maprin caddr l
   >>;

% Here starts support for Texmacs, the CSL GUI, and for an old PSL GUI once
% used on Windows.

if rl_texmacsp() or 'csl memq lispsystem!* then <<
   put('bex, 'fancy!-functionsymbol, "\bigsqcup ");
   put('ball, 'fancy!-functionsymbol, "\bigsqcap ")
>>;

put('pasf, 'rl_fancy!-pribq, 'pasf_fancy!-pribq);

switch rlpribqlimits;
off1 'rlpribqlimits;

asserted procedure pasf_fancy!-pribq(qf: LispPrefixForm);
   if rl_texmacsp() then
      if !*rlpribqlimits then
         pasf_fancy!-pribq!-texmacs!-limits qf
      else
         pasf_fancy!-pribq!-texmacs!-classic qf
   else
      pasf_fancy!-pribq!-fm qf;

asserted procedure pasf_fancy!-pribq!-fm(qf: LispPrefixForm);
   % Used by the CSL GUI.
   begin scalar v, w;
      v := mkvect 0;
      if null !*nat then
         return 'failed;
      w := fancy!-prefix!-operator car qf;
      if w eq 'failed then <<
         fancy!-terpri!* t;
         fancy!-prefix!-operator car qf
      >>;
      fancy!-prin2 " ";
      w := fancy!-maprint!-atom(cadr qf, 0);
      if w eq 'failed then <<
         fancy!-terpri!* t;
         fancy!-maprint!-atom(cadr qf, 0)
      >>;
      fancy!-prin2 " ";
      % We abuse vectors, where it would be more appropriate to use
      % fancy!-in!-brackets with square brackets ![, !], but this produced
      % strange results in the CSL GUI.
      if !*rlpribqsm then
         putv(v, 0, pasf_boundsm(caddr qf, cadr qf))
      else
         putv(v, 0, caddr qf);
      w := fancy!-maprint!-atom(v, 0);
      if w eq 'failed then <<
         fancy!-terpri!* t;
         fancy!-maprint!-atom(v, 0)
      >>;
      fancy!-prin2 " ";
      w := fancy!-in!-brackets({'fancy!-maprint, mkquote cadddr qf, 0}, '!(, '!));
      if w eq 'failed then <<
         fancy!-terpri!* t;
         fancy!-in!-brackets({'fancy!-maprint, mkquote cadddr qf, 0}, '!(, '!))
      >>
   end;

% From here on, everything is for Texmacs.

asserted procedure pasf_fancy!-pribq!-texmacs!-classic(qf: LispPrefixForm);
   begin
      if null !*nat then
         return 'failed;
      fancy!-prefix!-operator car qf;
      fancy!-prin2 " ";
      fancy!-prin2 cadr qf;
      fancy!-prin2 " [";
      if !*rlpribqsm then
         fancy!-maprint(pasf_boundsm(caddr qf, cadr qf), 0)
      else
         fancy!-maprint(caddr qf, 0);
      fancy!-prin2 "] ";
      fancy!-prin2 "(";
      fancy!-maprint(cadddr qf, 0);
      fancy!-prin2 ")"
   end;

asserted procedure pasf_fancy!-pribq!-texmacs!-limits(qf: LispPrefixForm);
   begin
      if null !*nat then return 'failed;
      fancy!-prefix!-operator car qf;
      fancy!-prin2!-underscore();
      fancy!-prin2 "{";
      pasf_fancy!-prib(caddr qf, cadr qf);
      fancy!-prin2 "}";
      fancy!-prin2 "(";
      fancy!-maprint(cadddr qf, 0);
      fancy!-prin2 ")"
   end;

asserted procedure fancy!-prin2!-underscore();
   <<
      fancy!-line!* := '_ . fancy!-line!*;
      fancy!-pos!* := fancy!-pos!* #+ 1;
      if fancy!-pos!* #> 2 #* (linelength nil #+1 ) then overflowed!*:=t;
   >>;

asserted procedure pasf_fancy!-prib(f: LispPrefixForm, v: Kernel);
   <<
      fancy!-prin2 v;
      fancy!-prin2 ":";
      fancy!-prin2 " ";
      if !*rlpribqsm then
         fancy!-maprint(pasf_boundsm(f, v), 0)
      else
         fancy!-maprint(caddr f, 0);
   >>;

if rl_texmacsp() or 'csl memq lispsystem!* then <<
   put('neq,'fancy!-infix!-symbol,"\,\neq\, ");
   put('leq,'fancy!-infix!-symbol,"\,\leq\, ");
   put('geq,'fancy!-infix!-symbol,"\,\geq\, ");
   put('lessp,'fancy!-infix!-symbol,"\,<\, ");
   put('greaterp,'fancy!-infix!-symbol,"\,>\, ")
>>;

put('cong,'fancy!-prifn,'pasf_fancy!-pricong);
put('ncong,'fancy!-prifn,'pasf_fancy!-pricong);

asserted procedure pasf_fancy!-pricong(l: LispPrefixForm);
   % Presburger arithmetic standard form texmacs print a congruence.
   if rl_texmacsp() or 'csl memq lispsystem!* then
      pasf_fancy!-pricong!-texmacs l
   else
      pasf_fancy!-pricong!-fm l;

asserted procedure pasf_fancy!-pricong!-texmacs(l: LispPrefixForm);
   % Presburger arithmetic standard form texmacs print a congruence.
   if null !*nat then
      'failed
   else <<
      maprin cadr l; % lhs
      if car l eq 'cong then
         fancy!-prin2 "\,\equiv"
      else
         fancy!-prin2 "\,\not\equiv";
      fancy!-prin2!-underscore();
      fancy!-prin2 "{";
      maprin cadddr l; % modulus
      fancy!-prin2 "}\,";
      maprin caddr l; % rhs
   >>;

asserted procedure pasf_fancy!-pricong!-fm(l: LispPrefixForm);
   % Presburger arithmetic standard form texmacs print a congruence.
   if null !*nat then
      'failed
   else <<
      maprin cadr l;
      if car l eq 'cong then
         fancy!-special!-symbol(186, 2)
      else
         fancy!-special!-symbol(187, 2);
      maprin caddr l;
      fancy!-prin2 " (";
      maprin cadddr l;
      fancy!-prin2 ")"
   >>;

endmodule;

end;

M packages/redlog/rl/redlog.red => packages/redlog/rl/redlog.red +1 -0
@@ 485,6 485,7 @@ rl_builtin {
put('bex, 'rtypefn, 'quotelog);
put('bex, 'rl_simpfn, 'rl_simpbq);
put('bex, 'number!-of!-args, 3);
put('bex, 'rl_prepfn, 'rl_prepbq);

rl_builtin {
   name = ball, 

M packages/redlog/rl/rlami.red => packages/redlog/rl/rlami.red +2 -3
@@ 176,15 176,14 @@ asserted procedure rl_simpq(f: MixedPrefixForm): Formula;

asserted procedure rl_simpbq(f: MixedPrefixForm): Formula;
   % simp form that starts with a bounded quantifier.
   begin scalar simpb, x, m;
   begin scalar simpb, x;
      if null (simpb := get(car rl_cid!*, 'rl_simpb)) then
         rederr {"current context", rl_usedcname!*, "does not support bounded quantifiers"};
      x := reval cadr f;
      if not idp x then
         typerr(x, "bounded quantified variable");
      flag({x}, 'used!*);
      m := rl_simp1 cadddr f;
      return rl_mkbq(car f, x, apply(simpb, {caddr f, x, m}), m)
      return rl_mkbq(car f, x, apply(simpb, {caddr f, x}), rl_simp1 cadddr f)
   end;

asserted procedure rl_qvarchk(v: Any): Void;

M packages/redlog/rl/rlprint.red => packages/redlog/rl/rlprint.red +92 -284
@@ 1,8 1,9 @@
module rlprint;  % Reduce logic component printing.
module rlprint;
% Reduce logic package printing of algebraic mode output.

revision('rlprint, "$Id$");

copyright('rlprint, "(c) 1995-2009 A. Dolzmann, T. Sturm, 2017 T. Sturm");
copyright('rlprint, "(c) 1995-2009 A. Dolzmann, T. Sturm, 2017-2021 T. Sturm");

% Redistribution and use in source and binary forms, with or without
% modification, are permitted provided that the following conditions


@@ 29,87 30,38 @@ copyright('rlprint, "(c) 1995-2009 A. Dolzmann, T. Sturm, 2017 T. Sturm");
% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
%

asserted procedure rl_texmacsp(): Boolean;
   % Texmacs predicate. Returns [t] iff Texmacs is running.
   if getenv("TEXMACS_REDUCE_PATH") then t;

put('!*fof,'prifn,'rl_print!*fof);
put('!*fof,'fancy!-prifn,'rl_print!*fof);
put('!*fof,'fancy!-setprifn,'rl_setprint!*fof);
%put('!*fof,'prifn,'prin2!*);

put('and,'pprifn,'rl_ppriop);
put('and,'fancy!-pprifn,'rl_fancy!-ppriop);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('and,'fancy!-infix!-symbol,"\,\wedge\, ");

put('or,'pprifn,'rl_ppriop);
put('or,'fancy!-pprifn,'rl_fancy!-ppriop);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('or,'fancy!-infix!-symbol,"\,\vee\, ");

put('impl,'pprifn,'rl_ppriop);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('impl,'fancy!-infix!-symbol,"\,\longrightarrow\, ")
else
   put('impl,'fancy!-infix!-symbol,222);

put('repl,'pprifn,'rl_ppriop);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('repl,'fancy!-infix!-symbol,"\,\longleftarrow\, ")
else
   put('repl,'fancy!-infix!-symbol,220);

put('equiv,'pprifn,'rl_ppriop);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('equiv,'fancy!-infix!-symbol,"\,\longleftrightarrow\, ")
else
   put('equiv,'fancy!-infix!-symbol,219);

put('ex,'prifn,'rl_priq);
put('ex,'fancy!-prifn,'rl_fancy!-priq);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('ex,'fancy!-functionsymbol,"\exists ")
else
   put('ex,'fancy!-functionsymbol,36);
struct MixedPrefixForm asserted by mixedPrefixFormP;
struct PseudoPrefixForm asserted by pairp;

put('all,'prifn,'rl_priq);
put('all,'fancy!-prifn,'rl_fancy!-priq);
if rl_texmacsp()  or 'csl memq lispsystem!* then
   put('all,'fancy!-functionsymbol,"\forall ")
else
   put('all,'fancy!-functionsymbol,34);
put('!*fof, 'prifn, 'rl_print!*fof);

put('bex,'prifn,'rl_pribq);
put('bex,'rl_prepfn,'rl_prepbq); % semms not to be used!
%put('bex,'fancy!-functionsymbol,36);
put('bex,'fancy!-prifn,'rl_fancy!-pribq);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('bex,'fancy!-functionsymbol,"\bigsqcup ")
else
   put('bex,'fancy!-functionsymbol,36); %%% 36 okay?

put('ball,'prifn,'rl_pribq);
%put('ball,'fancy!-functionsymbol,34);
put('ball,'fancy!-prifn,'rl_fancy!-pribq);
if rl_texmacsp() or 'csl memq lispsystem!* then
   put('ball,'fancy!-functionsymbol,"\bigsqcap ")
else
   put('ball,'fancy!-functionsymbol,34); %%% 34 okay?

procedure rl_print!*fof(u);
asserted procedure rl_print!*fof(u: PseudoPrefixForm);
   maprin reval u;

procedure rl_setprint!*fof(x,u);
   <<
      fancy!-maprint(x,0);
      fancy!-prin2!*(":=",4);
      rl_print!*fof u
put('and, 'pprifn, 'rl_ppriop);
put('or, 'pprifn, 'rl_ppriop);
put('impl, 'pprifn, 'rl_ppriop);
put('repl, 'pprifn, 'rl_ppriop);
put('equiv, 'pprifn, 'rl_ppriop);

asserted procedure rl_ppriop(f: LispPrefixForm, n: Integer);
   % Infix Precedence print for operators and, or, impl, repl, equiv.
   if null !*nat or null !*rlbrop or eqn(n, 0) then
      'failed
   else <<
      prin2!* "(";
      inprint(car f, get(car f, 'infix), cdr f);
      prin2!* ")"
   >>;

procedure rl_priq(qf);
put('ex, 'prifn, 'rl_priq);
put('all, 'prifn, 'rl_priq);

asserted procedure rl_priq(qf: LispPrefixForm): Void;
   % Print formula starting with quantifier ex, all.
   begin scalar m;
      if null !*nat then return 'failed;
      if null !*nat then
        return 'failed;
      maprin car qf;
      if not !*utf8 then
         prin2!* " ";


@@ 124,123 76,73 @@ procedure rl_priq(qf);
      >>
   end;

procedure rl_pribq(qf);
   % Print bounded quantifer.
   begin
      if null !*nat then return
         'failed;
      maprin car qf; % print quantifier
      prin2!* " ";
      maprin cadr qf; % print variable
      prin2!* " ";
      prin2!* "[";
      rl_pribound(cadr qf,caddr qf); % print bound
      prin2!* "] ";
      prin2!* "(";
      maprin cadddr qf; % print matrix
      prin2!* ")"
put('bex, 'prifn, 'rl_pribq);
put('ball, 'prifn, 'rl_pribq);

asserted procedure rl_pribq(qf: LispPrefixForm): Void;
   % Print formula starting with bounded quantifer bex, ball.
   begin scalar w;
      if null (w := get(car rl_cid!*, 'rl_pribq)) then
         rederr {"current context", rl_usedcname!*, "does not support bounded quantifiers"};
      apply(w, {qf})
   end;

switch rlsmprint;
on1 'rlsmprint;
% Here starts support for Texmacs, the CSL GUI, and for an old PSL GUI once
% used on Windows.

procedure rl_pribound(v,f);
   maprin rl_fancybound(v,f);
asserted procedure rl_texmacsp(): Boolean;
   % Texmacs predicate. Returns t iff Texmacs is running.
   if getenv("TEXMACS_REDUCE_PATH") then t;

procedure rl_fancybound(v,f);
   begin scalar w,w1,w2,argl;
      if null !*rlsmprint then
         return f;
      if eqcar(f,'or) then <<
         w := 'or . for each x in cdr f collect rl_fancybound(v,x);
         return rl_fancybound!-try!-abs w
      >>;
      argl := rl_argn f;
      if cddr argl then
         return f;
      w1 := rl_fancybound1(v,car argl);
      if null w1 then
         return f;
      w2 := rl_fancybound1(v,cadr argl);
      if null w2 then
         return f;
      if car w1 eq car w2 then
         return f;
      if eqcar(w1,'ub) then <<
         w := w1;
         w1 := w2;
         w2 := w
      >>;
      w1 := cdr w1;
      w2 := cdr w2;
      if car(w1) neq car(w2) then
         if car(w1) eq 'leq then << % <= v <
            caddr w2 := reval {'plus, caddr w2, {'minus, 1}};
            car w2 := 'leq
         >>
         else << % < v <=
            cadr w1 := reval {'plus, cadr w1, 1};
            car w1 := 'leq
         >>;
      return nconc(w1,{caddr w2})
   end;
if rl_texmacsp() or 'csl memq lispsystem!* then <<
   put('and, 'fancy!-infix!-symbol, "\,\wedge\, ");
   put('or, 'fancy!-infix!-symbol, "\,\vee\, ");
   put('impl, 'fancy!-infix!-symbol, "\,\longrightarrow\, ");
   put('repl, 'fancy!-infix!-symbol, "\,\longleftarrow\, ");
   put('equiv, 'fancy!-infix!-symbol, "\,\longleftrightarrow\, ");
   put('ex, 'fancy!-functionsymbol, "\exists ");
   put('all, 'fancy!-functionsymbol, "\forall ")
>> else <<
   put('impl, 'fancy!-infix!-symbol, 222);
   put('repl, 'fancy!-infix!-symbol, 220);
   put('equiv, 'fancy!-infix!-symbol, 219);
   put('ex, 'fancy!-functionsymbol, 36);
   put('all, 'fancy!-functionsymbol, 34)
>>;

put('!*fof, 'fancy!-setprifn, 'rl_setprint!*fof);

asserted procedure rl_setprint!*fof(x: Kernel, u: LispPrefixForm);
   % Print assignment of a formula to a variable.
   <<
      fancy!-maprint(x, 0);
      fancy!-prin2!*(":=", 4);
      rl_print!*fof u
   >>;

procedure rl_fancybound1(v,a);
   begin scalar w,c;
      if car a memq '(geq greaterp) then
         a := {pasf_anegrel car a,{'minus,cadr a},0};
      w := sfto_reorder(numr simp cadr a,v);
      if not domainp w and mvar w eq v then
         c := lc w;
      if car a memq '(leq lessp) and c = 1 then
         return 'ub . {car a,v,prepf negf red w};
      if car a memq '(leq lessp) and c = -1 then
         return 'lb . {car a,prepf red w,v}
   end;
put('!*fof, 'fancy!-prifn, 'rl_print!*fof);

procedure rl_fancybound!-try!-abs(f);
   begin scalar w,v,r1,r2,l1,l2,u1,u2;
      w := cdr f;
      if cddr w then
         return f;
      if length car w neq 4 or length cadr w neq 4 then
         return f;
      r1 := car car w;
      r2 := car cadr w;
      if r1 neq r2 or r1 eq 'cong then
         return f;
      l1 := numr simp cadr car w;
      v := caddr car w;
      u1 := numr simp cadddr car w;
      l2 := numr simp cadr cadr w;
      u2 := numr simp cadddr cadr w;
      if l1 = u2 and l2 = u1 and l1 = negf u1 and l2 = negf u2 then
         return {r1,{'minus,{'abs,prepf absf l1}},v,{'abs,prepf absf u1}};
      return f
   end;
% procedure rl_print!*fof is defined above.

procedure rl_ppriop(f,n);
   if null !*nat or null !*rlbrop or eqn(n,0) then
      'failed
   else <<
      prin2!* "(";
      inprint(car f,get(car f,'infix),cdr f);
      prin2!* ")"
   >>;
put('and, 'fancy!-pprifn, 'rl_fancy!-ppriop);
put('or, 'fancy!-pprifn, 'rl_fancy!-ppriop);

procedure rl_fancy!-ppriop(f,n);
asserted procedure rl_fancy!-ppriop(f: LispPrefixForm, n: Integer);
   <<
      if null !*nat or null !*rlbrop or eqn(n,0) then
      if null !*nat or null !*rlbrop or eqn(n, 0) then
         'failed
      else if !*rlbrop then
         fancy!-in!-brackets(
            {'fancy!-inprint,mkquote car f,n,mkquote cdr f},'!(,'!))
            {'fancy!-inprint, mkquote car f, n, mkquote cdr f}, '!(, '!))
      else
         fancy!-inprint(car f,n,cdr f)
         fancy!-inprint(car f, n, cdr f)
   >>;

procedure rl_fancy!-priq(qf);
   begin scalar m,w;
put('ex, 'fancy!-prifn, 'rl_fancy!-priq);
put('all, 'fancy!-prifn, 'rl_fancy!-priq);

asserted procedure rl_fancy!-priq(qf: LispPrefixForm);
   begin scalar m, w;
      if null !*nat then
         return 'failed;
      w := fancy!-prefix!-operator car qf;


@@ 248,125 150,31 @@ procedure rl_fancy!-priq(qf);
         fancy!-terpri!* t;
         fancy!-prefix!-operator car qf
      >>;
      w := fancy!-maprint!-atom(cadr qf,0);
      w := fancy!-maprint!-atom(cadr qf, 0);
      if w eq 'failed then <<
         fancy!-terpri!* t;
         fancy!-maprint!-atom(cadr qf,0)
         fancy!-maprint!-atom(cadr qf, 0)
      >>;
      if pairp(m := caddr qf) and car m memq '(ex all) then
         return rl_fancy!-priq m;
      w := fancy!-in!-brackets({'fancy!-maprint,mkquote m,0},'!(,'!));
      w := fancy!-in!-brackets({'fancy!-maprint, mkquote m, 0}, '!(, '!));
      if w eq 'failed then <<
         fancy!-terpri!* t;
         return fancy!-in!-brackets({'fancy!-maprint,mkquote m,0},'!(,'!))
         return fancy!-in!-brackets({'fancy!-maprint, mkquote m, 0}, '!(, '!))
      >>
   end;

symbolic procedure fancy!-prin2!-underscore(); % --> fmprint
   <<
      fancy!-line!* := '_ . fancy!-line!*;
      fancy!-pos!* := fancy!-pos!* #+ 1;
      if fancy!-pos!* #> 2 #* (linelength nil #+1 ) then overflowed!*:=t;
   >>;

symbolic procedure rl_fancy!-prib(v,f);
   %   if car f eq 'and then <<
   %      fancy!-prin2 "{";
   %      rl_fancy!-prib1 cdr f;
   %      fancy!-prin2 "}";
   %   >> else
   <<
      fancy!-prin2 v;
      fancy!-prin2 ":";
      maprin f
   >>;

symbolic procedure rl_fancy!-prib1(fl);
   if cdr fl then <<
      fancy!-prin2 "\stackrel";
      fancy!-prin2 "{";
      fancy!-prin2 "\large{}";
      maprin car fl;
      fancy!-prin2 "}";
      fancy!-prin2 "{";
      rl_fancy!-prib1 cdr fl;
      fancy!-prin2 "}";
   >> else <<
      fancy!-prin2 "\stackrel";
      fancy!-prin2 "{";
      fancy!-prin2 "\large{}";
      maprin car fl;
      fancy!-prin2 "}";
      fancy!-prin2 "{";
      fancy!-prin2 "}";
%      fancy!-prin2 "\normalsize{}";
%      maprin car fl
   >>;

switch rlbqlimits;

procedure rl_fancy!-pribq(qf);
   if rl_texmacsp() then
      if !*rlbqlimits then
         rl_fancy!-pribq!-texmacs qf
      else
         rl_fancy!-pribq!-texmacs2 qf
   else
      rl_fancy!-pribq!-fm qf;

put('bex, 'fancy!-prifn, 'rl_fancy!-pribq);
put('ball, 'fancy!-prifn, 'rl_fancy!-pribq);

procedure rl_fancy!-pribq!-texmacs(qf);
   begin scalar m;
      if null !*nat then return 'failed;
      fancy!-prefix!-operator car qf;
      fancy!-prin2!-underscore();
      fancy!-prin2 "{";
      %maprin caddr qf;
      rl_fancy!-prib(cadr qf,caddr qf);
      fancy!-prin2 "}";
      if pairp(m := cadddr qf) and car m memq '(ex all bex ball) then
         maprin m
      else <<
         fancy!-prin2 "(";
         maprin m;
         fancy!-prin2 ")"
      >>
asserted procedure rl_fancy!-pribq(qf: LispPrefixForm);
   % Fancy-print formula starting with bounded quantifer bex, ball.
   begin scalar w;
      if null (w := get(car rl_cid!*, 'rl_fancy!-pribq)) then
         rederr {"current context", rl_usedcname!*, "does not support bounded quantifiers"};
      apply(w, {qf})
   end;

procedure rl_fancy!-pribq!-texmacs2(qf);
   begin scalar m;
      if null !*nat then return 'failed;
      fancy!-prefix!-operator car qf;
      fancy!-prin2 cadr qf;
      fancy!-prin2 "[";
      maprin caddr qf;
      fancy!-prin2 "]";
      if pairp(m := cadddr qf) and car m memq '(ex all bex ball) then
         maprin m
      else <<
         fancy!-prin2 "(";
         maprin m;
         fancy!-prin2 ")"
      >>
   end;

procedure rl_fancy!-pribq!-fm(qf);
   if null !*nat then
      'failed
   else
   <<
      fancy!-prefix!-operator car qf;
      fancy!-prin2 " ";
      maprin cadr qf;
      fancy!-prin2 " ";
      fancy!-prin2 "[";
      maprin caddr qf; % print bound
      fancy!-prin2 "]";
      fancy!-prin2 " (";
      maprin cadddr qf; % print matrix
      fancy!-prin2 ")"
   >>;

endmodule;

end;