1module rlami;
2% Reduce logic component algebraic mode interface. Submodule of [redlog].
3
4revision('rlami, "$Id: rlami.red 5403 2020-09-20 14:25:44Z thomas-sturm $");
5
6copyright('rlami, "(c) 1995-2009 A. Dolzmann, T. Sturm, 2017 T. Sturm");
7
8% Redistribution and use in source and binary forms, with or without
9% modification, are permitted provided that the following conditions
10% are met:
11%
12%    * Redistributions of source code must retain the relevant
13%      copyright notice, this list of conditions and the following
14%      disclaimer.
15%    * Redistributions in binary form must reproduce the above
16%      copyright notice, this list of conditions and the following
17%      disclaimer in the documentation and/or other materials provided
18%      with the distribution.
19%
20% THIS SOFTWARE IS PROVIDED BY THE COPYRIGHT HOLDERS AND CONTRIBUTORS
21% "AS IS" AND ANY EXPRESS OR IMPLIED WARRANTIES, INCLUDING, BUT NOT
22% LIMITED TO, THE IMPLIED WARRANTIES OF MERCHANTABILITY AND FITNESS FOR
23% A PARTICULAR PURPOSE ARE DISCLAIMED. IN NO EVENT SHALL THE COPYRIGHT
24% OWNERS OR CONTRIBUTORS BE LIABLE FOR ANY DIRECT, INDIRECT, INCIDENTAL,
25% SPECIAL, EXEMPLARY, OR CONSEQUENTIAL DAMAGES (INCLUDING, BUT NOT
26% LIMITED TO, PROCUREMENT OF SUBSTITUTE GOODS OR SERVICES; LOSS OF USE,
27% DATA, OR PROFITS; OR BUSINESS INTERRUPTION) HOWEVER CAUSED AND ON ANY
28% THEORY OF LIABILITY, WHETHER IN CONTRACT, STRICT LIABILITY, OR TORT
29% (INCLUDING NEGLIGENCE OR OTHERWISE) ARISING IN ANY WAY OUT OF THE USE
30% OF THIS SOFTWARE, EVEN IF ADVISED OF THE POSSIBILITY OF SUCH DAMAGE.
31%
32
33procedure rl_mk!*fof(u);
34   % Reduce logic make tagged form of first-order formula. [u] is a
35   % first-order formula. Returns pseudo Lisp prefix of [u]. This is
36   % analogous to [mk!*sq] in [alg.red].
37   rl_mk!*fof1 rl_csimpl u;
38
39procedure rl_mk!*fof1(u);
40   % Reduce logic make tagged form of first-order formula subroutine.
41   % [u] is a first-order formula. Returns pseudo Lisp prefix of [u].
42   % This is analogous to [mk!*sq] in [alg.red].
43   if rl_tvalp u then
44      u
45   else if eqcar(u,'equal) then
46      rl_prepfof1 u
47   else
48      '!*fof . rl_cid!* . u . if !*resubs then !*sqvar!* else {nil};
49
50procedure rl_reval(u,v);
51   % Reduce logic [reval]. [u] is a formula in some mixed pseudo Lisp
52   % prefix form where [car u] is either ['!*fof] or a first-order
53   % operator; [v] is bool. Returns Lisp prefix of [u] in case [v] is
54   % non-[nil], and pseudo Lisp prefix of [u] else.
55   if v then rl_prepfof rl_simp1 u else rl_mk!*fof rl_simp1 u;
56
57procedure rl_csimpl(u);
58   % Conditional simplify.
59   if !*rlsimpl and getd 'rl_simpl then %???
60      rl_simpl(u,{},-1)
61   else
62      u;
63
64procedure rl_prepfof(f);
65   % [prep] first-order with bounded quantifers formula.
66   rl_prepfof1 rl_csimpl f;
67
68procedure rl_prepfof1(f);
69   % [prep] first-order formula with bounded quantifers subroutine.
70   begin scalar op,w;
71      op := rl_op f;
72      if rl_tvalp op then
73 	 return op;
74      if rl_quap op then
75	 return {op,rl_var f,rl_prepfof1 rl_mat f};
76      if rl_bquap op then
77	 return {op,rl_var f,rl_prepfof1 rl_b f,rl_prepfof1 rl_mat f};
78      if rl_boolp op then
79	 return op . for each x in rl_argn f collect rl_prepfof1 x;
80      if (w := rl_external(op,'rl_prepfof1)) then
81	 return apply(w,{f});
82      % [f] is atomic.
83      return apply(get(car rl_cid!*,'rl_prepat),{f})
84   end;
85
86asserted procedure rl_cleanup(u: Any, v: ExtraBoolean): Any;
87   % This is bound to the property [cleanupfn] of the rl_service!$ functions
88   % that are in turn the [psopfn] of the corresponding rlservice AM
89   % entrypoints. The [cleanupfn] is used with the evaluation of [psopfn] in
90   % [reval1] in [alg/reval.red], where it converts - in the right moment - the
91   % result of of rl_service!$ to Lisp prefix so that [part(rlservice(...),
92   % ...)] works properly. However, the final evaluation result is generally
93   % Pseudo Lisp Prefix.
94   reval1(u,v);
95
96procedure rl_simpa(u);
97   % simp an answer structure
98   for each a in cdr reval u collect
99      {rl_simp cadr a,
100	 for each b in cdaddr a collect
101	    rl_simp b, cdr cadddr a};
102
103procedure rl_simp(u);
104   % [simp] first-order formula.
105   rl_csimpl rl_simp1 u;
106
107procedure rl_simp1(u);
108   % Reduce logic [simp]. [u] is (pseudo) Lisp prefix of a formula.
109   % Returns the formula encoded by [u].
110   begin scalar w, h;
111      if null rl_cid!* then rederr {"select a context"};
112      if atom u then
113 	 return rl_simpatom u;
114      argnochk u where !*strict_argcount = t;
115      if (w := get(car u, 'rl_simpfn)) then
116 	 return if flagp(w, 'full) then apply(w, {u}) else apply(w, {cdr u});
117      if (w := get(car u, get(car rl_cid!*, 'simpfnname))) then
118	 return if flagp(w, 'full) then apply(w, {u}) else apply(w, {cdr u});
119      if (w := get(car u, 'psopfn)) then <<
120	 % u = (replaceby x 1) will return itself via a psopfn equalreplaceby.
121	 h := apply1(w, cdr u);
122	 if h neq u then
123 	    return rl_simp1 h
124      >>;
125      if flagp(car u, 'opfn) then
126	 return rl_simp1 apply(car u, for each x in cdr u collect reval x);
127      if (w := get(car u, 'prepfn2)) then
128 	 return rl_simp1 apply(w, {u});
129      h := ioto_form2str car u;
130      if (w := get(car u, 'prtch)) then
131	 h := lto_sconcat {ioto_form2str w, " (", h, ")"};
132      redmsg(h, "predicate");
133      put(car u, get(car rl_cid!*, 'simpfnname), get(car rl_cid!*, 'simpdefault));
134      return rl_simp1(u)
135   end;
136
137procedure rl_simpatom(u);
138   % Reduce logic simp atom. [u] is an atom.
139   begin scalar w;
140      if null u then typerr("nil","logical");
141      if numberp u then typerr({"number",u},"logical");
142      if stringp u then typerr({"string",u},"logical");
143      if rl_tvalp u then return u;
144      if (w := rl_gettype(u)) then <<
145	 if w memq '(logical equation scalar slprog) then
146	    return rl_simp1 cadr get(u,'avalue);
147	 typerr({w,u},"logical")
148      >>;
149      % [u] algebraically unbound.
150      if boundp u then return rl_simp1 eval u;
151      typerr({"unbound id",u},"logical")
152   end;
153
154procedure rl_simpbop(f);
155   % Reduce logic simp boolean operator.
156   rl_mkn(car f,for each x in cdr f collect rl_simp1 x);
157
158procedure rl_simpq(f);
159   % Reduce logic simp quantifier.
160   begin scalar vl,w;
161      vl := reval cadr f;
162      if eqcar(vl,'list) then
163	 vl := cdr vl
164      else
165	 vl := {vl};
166      w := rl_simp1 caddr f;
167      for each x in reverse vl do <<
168      	 rl_qvarchk x;
169	 w := rl_mkq(car f,x,w)
170      >>;
171      flag(vl,'used!*);
172      return w
173   end;
174
175procedure rl_simpbq(f);
176   % Reduce logic simp bounded quantifier. [f] is a list [(Q,x,b,f)]
177   % where [Q] is a quantifier, [x] is an id, and [b] and [f] are
178   % lisp-prefix. Returns a bounded quantifier headed formula.
179   begin scalar x,wb,wf;
180      if car rl_cid!* neq 'pasf then
181	 rederr "boundend quantifiers only allowed within PASF context";
182      x := reval cadr f;
183      if not idp x then typerr("not identifer","bounded quantified variable");
184      wb := rl_simp1 caddr f;
185      %%% test, wether x is the only free variable in [wb].
186      wf := rl_simp1 cadddr f;
187      % Test, wether the bounded quantifier has a finite solution set.
188      % rl_bsatp fails per definition if that is not the case.
189      rl_bsatp(wb,x);
190      flag({x},'used!*);
191      return rl_mkbq(car f,x,wb,wf)
192   end;
193
194procedure rl_qvarchk(v);
195   % Syntax-check quantified variable.
196   if not sfto_kernelp v or (!*rlbrkcxk and pairp v) then
197      typerr(v,"quantified variable");
198
199procedure rl_simp!*fof(u);
200   % Reduce logic simp [!*fof] operator. [u] is of the form
201   % $([tag],f,[!*sqvar!*])$ where [tag] is a context tag and $f$ is a
202   % formula.
203   begin scalar tag,f,w;
204      if caddr u then return cadr u;  % [!*sqvar!*=T]
205      tag := car u;
206      f := cadr u;
207      if tag neq rl_cid!* then <<
208	 w := rl_set tag where !*msg=nil;
209	 f := rl_prepfof f;
210	 rl_set w where !*msg=nil;
211	 return rl_simp f
212      >>;
213      return rl_resimp f
214   end;
215
216procedure rl_resimp(u);
217   % Reduce logic resimp. [u] is a formula.
218   begin scalar op,w;
219      op := rl_op u;
220      if rl_tvalp op then
221	 return u;
222      if rl_quap op then <<
223      	 if (w := rl_gettype(rl_var u)) then
224 	    typerr({w,rl_var u},"quantified variable");
225	 rl_qvarchk rl_var u;
226      	 return rl_mkq(op,rl_var u,rl_resimp rl_mat u)
227      >>;
228      if rl_bquap op then <<
229      	 if (w := rl_gettype(rl_var u)) then
230 	    typerr({w,rl_var u},"quantified variable");
231      	 return rl_mkbq(op,rl_var u,rl_resimp rl_b u,rl_resimp rl_mat u)
232      >>;
233      if rl_boolp op then
234	 return rl_mkn(op,for each x in rl_argn u collect rl_resimp x);
235      if (w := rl_external(op,'rl_resimp)) then
236	 return apply(w,{u});
237      return apply(get(car rl_cid!*,'rl_resimpat),{u})
238   end;
239
240procedure rl_gettype(v);
241   % Get type. Return type information if present. Handle scalars
242   % properly.
243   (if w then car w else get(v,'rtype)) where w = get(v,'avalue);
244
245procedure rl_lengthlogical(u);
246   rl_lengthfof rl_simp u;
247
248procedure rl_lengthfof(f);
249   % First order formula length. [u] is a formula. Returns the number
250   % of top-level constituents of [u].
251   begin scalar op;
252      op := rl_op f;
253      if rl_tvalp op then
254	 return 1;
255      if rl_quap op then
256	 return 2;
257      if rl_bquap op then
258	 return 3;
259      if rl_cxp op then
260	 return length rl_argn f;
261      % [f] is atomic.
262      return apply(get(car rl_cid!*,'rl_lengthat),{f})
263   end;
264
265procedure rl_sub!*fof(al,f);
266   rl_mk!*fof rl_subfof(al,rl_simp f);
267
268
269rl_builtin {
270   name = mkor,
271   doc = {
272      synopsis = {pos = 1, text = "for R mkor E"},
273      description = "for-loop action for constructing disjunctions",
274      returns = "Any",
275      arg = {pos = 1, name = "R", text = "range specification as documented in Sect.5.4 of the REDUCE manual "},
276      arg = {pos = 2, name = "E", text = "RLISP expression"}
277   }
278};
279
280rl_builtin {
281   name = mkand,
282   doc = {
283      synopsis = {pos = 1, text = "for R mkand E"},
284      description = "for-loop action for constructing conjunctions",
285      returns = "Any",
286      arg = {pos = 1, name = "R", text = "range specification as documented in Sect.5.4 of the REDUCE manual "},
287      arg = {pos = 2, name = "E", text = "RLISP expression"}
288   }
289};
290
291foractions!* := 'mkand . 'mkor . foractions!*;
292deflist('((mkand rlmkand) (mkor rlmkor)),'bin);
293deflist('((mkand (quote true)) (mkor (quote false))),'initval);
294
295symbolic operator rlmkor,rlmkand;
296
297procedure rlmkor(a,b);
298   if !*mode eq 'symbolic then
299      rederr "`mkor' invalid in symbolic mode"
300   else <<
301      if null a then a := 'false;
302      if null b then b := 'false;
303      a := if eqcar(a,'or) then cdr a else {a};
304      b := if eqcar(b,'or) then cdr b else {b};
305      'or . nconc(b,a)
306   >>;
307
308procedure rlmkand(a,b);
309   if !*mode eq 'symbolic then
310      rederr "`mkand' invalid in symbolic mode"
311   else <<
312      if null a then a := 'true;
313      if null b then b := 'true;
314      a := if eqcar(a,'and) then cdr a else {a};
315      b := if eqcar(b,'and) then cdr b else {b};
316      'and . nconc(b,a)
317   >>;
318
319endmodule;  % [rlami]
320
321end;  % of file
322