~trn/reduce-algebra

ref: b471c93636fbb9fa9c7886a7163344781871a0f2 reduce-algebra/packages/redlog/rlsupport/rlservice.red -rw-r--r-- 29.4 KiB
b471c936 — Jeffrey H. Johnson Merge branch 'svn/trunk' a month ago
                                                                                
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
module rlservice;

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

copyright('rlservice, "(c) 2016-2020 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.
%

% This module generates an AM-SM interface on the basis of formal
% specifications. The AM interface supports combinations of positional arguments
% and named arguments and optional arguments with default values given in the
% specification. Possible conflicts between positional and named arguments are
% resolved according to Python rules. In the AM->SM direction types of passed
% arguments are checked at runtime. It furthermore supports a dynamic online
% help system implemented in the submodule rlhelp.
%
%  AM            |   SM
%                |
%  rl<service> --+-> rl_<service>!$
%                |   ---> rl_servicewrapper
%                |        ---> rl_!*<service>
%                |             ---> rl_<service>
%                |                  ---> apply(rl_<service>!*)
%
%
%
% rl<service> is the AM entry point. It has a property (psopfn .
% rl_<service>!$). It has a property (intypes . <list of possibly composite
% types>), which is exclusively used with the dynamic help module. Those types
% are given as strings to preserve case. Similarly, there is (outtype .
% <string>).


fluid '(!*lower);
fluid '(!*raise);
fluid '(mode!*);

global '(rl_services!*);
fluid '(rl_servl!*);

% We provide a stat and a formfn for the rl_service specifications in
% redlog/rl/rlservices.red. Although, those specifications are just listed nests
% of equations, there are several issues parsing them directly with xread: The
% equations may contain RLISP keywords, default arguments should be xread in
% AM, and we want to parse types in CamelCase.

put('rl_service, 'stat, 'rl_serviceStat);

asserted procedure rl_serviceStat(): List;
   % Read the opening curly brace and clean up at the end. The main loop parsing
   % the list is in the next function.
   begin scalar spec;
      rl_skiplcbkt "rl_service";
      spec := rl_serviceStatList();
      scan();  % !*semicol!*
      return {'rl_service, spec}
   end;

asserted procedure rl_serviceStatList(): Alist;
   % We hav just read '{'. Parse a list with entries of the form [name = entry].
   % [name] is an alphabetic identifier. For [entry], there are four
   % cases:
   % (a) An atom. This is our default assumption.
   % (b) Another list such as the one we are currently parsing. This is
   %     triggered by the entry starting with '{.'
   % (c) An expression to be parsed by xread in algebraic mode. This is
   %     triggered by by the [name] "default."
   % (d) An expression to be parsed by xread in symbolic mode and
   %     case-sensitive. This is triggered by by the [name] "type."
   % At the time of writing this code Reduce is not case-sensitve, and upper
   % case would be folded by the Lisp reader. We are going to suppress that
   % folding when reading types, because we wangt to preserve CamelCase for our
   % help system. On the other hand, we do not want to bring mixed-case
   % identifiers into the system at the present stage. Our solution is to
   % keep all types as strings, and to convert them into expressions on the fly
   % when needed. The result is going to be an Alist corresponding to the input
   % (nested) list of equations, and a subsequent formfn is going to take care
   % of the rest.
   begin scalar spec, key, entry;
      scan();
      while cursym!* neq '!*rcbkt!* do <<
         % We are not on the right hand side of an equation. We need an
         % alphabetic identifier. We strictly admit only alphabetic characters,
         % no digits.
         if not lto_alphap cursym!* then
            rederr {"expecting alphabetic key in rl_service but found", cursym!*};
         key := cursym!*;
         % Now the four cases (a)-(d) discussed above:
         entry := if key eq '!d!e!f!a!u!l!t then  % case (c)
            rl_amReadDefaultToForm()
         else if key eq 'type then  % case (d)
            rl_csReadTypeToString()
         else  % case (a) or (b)
            rl_readListOrAtom();
         push(key . entry, spec);
         % Expecting ',' or '}' now:
         if cursym!* neq '!*rcbkt!* then <<
            if cursym!* neq '!*comma!* then
               rederr {"expecting ',' or '}' in rl_service but found", cursym!*};
            scan()
         >>
      >>;
      return reversip spec
   end;

asserted procedure rl_amReadDefaultToForm(): List;
   begin scalar !*mode;
      !*mode := 'algebraic;
      rl_skipequal "rl_service";
      return xread t
   end;

asserted procedure rl_csReadTypeToString(): String;
   % Locally case-sensitive scanning of CamelCase types. It is important to have
   % case-sensitivity switched on already with the scanning of the '=' because
   % there is a lookahead with nextsym!*.
   begin scalar !*lower, !*raise;
      rl_skipequal "rl_service";
      return ioto_smaprin xread t
   end;

asserted procedure rl_readListOrAtom(): String;
   begin scalar entry;
      rl_skipequal "rl_service";
      scan();
      if cursym!* eq '!*lcbkt!* then <<  % case (b)
         entry := rl_serviceStatList()
      >> else <<  % case (a)
         if not atom cursym!* then
            rederr {"expecting atomic entry or list in rl_service but found", cursym!*};
         entry := cursym!*
      >>;
      scan();
      return entry
   end;

put('rl_service, 'formfn, 'rl_formService);

asserted procedure rl_formService(argl: List, vars: List, m: Id): List;
   % Analyze the equational specifications of services, and generate
   % corresponding functions and bindings.
   begin scalar mode;
      % Valid choices for mode are sm and both. We always build the SM
      % interface, because it is called by the AM interface:
      mode := lto_eatsoc('mode, cadr argl, {"missing mode in", argl});
      if mode eq 'both then
         return rl_formServiceBoth cadr argl;
      if mode eq 'sm then
         return rl_formServiceSm cadr argl;
      rederr {"invalid mode", mode, "in", argl}
   end;

asserted procedure rl_formServiceBoth(spec: Alist): List;
   begin
      scalar b, doc, seealso, names, types, defaults, docs, rtype, rl_args, rl_!*args;
      scalar rl_b!*, rl_b, rl_!*b, rl_b!$, rlb;
      scalar p, docal, fluids;
      {b, doc, seealso, names, types, defaults, docs, rtype, rl_args, rl_!*args} :=
         rl_formServiceAnalyzeSpec spec;
      {rl_b!*, rl_b, rl_!*b, rl_b!$, rlb} :=
         rl_formServiceFunctionNames('rl_, b);
      % We are going construct a progn in [p], which is going to be the
      % result of rl_formService.
      %
      % "put(rlb, 'rtypefn, 'rtypepart)"
      % rtypepart is the rtype of the part function. TS does not exactly
      % understand anymore why this is used here. It might again have to do
      % with rl vs. sl.
      push({'put, mkquote rlb, ''rtypefn, ''rtypepart}, p);
      % "put(rlb, 'rl_support, 'amservice)"
      push({'put, mkquote rlb, ''rl_support, ''rl_amservice}, p);
      % "put(rlb, 'rl_smService, rl_b)"
      % a link to the corresponding SM service:
      push({'put, mkquote rlb, ''rl_smService, mkquote rl_b}, p);
      % "put(rlb, 'names, names)"
      % [names] is a list of identifiers, the formal arguments:
      push({'put, mkquote rlb, ''names, mkquote names}, p);
      % "put(rlb, 'types, types)"
      % [types] is the list of strings, the types of the formal arguments given
      % in [names]; length(types) = length(names):
      push({'put, mkquote rlb, ''intypes, mkquote types}, p);
      % "put(rlb, 'defaults, defaults)"
      % [defaults] is an Alist, keys are identifiers, entries are forms; this
      % gives default values for (only) some arguments from [names]:
      push({'put, mkquote rlb, ''defaults, mkquote defaults}, p);
      % "put(rlb, 'outtyoe, rtype)"
      % [rtype] is a string, the return type:
      push({'put, mkquote rlb, ''outtype, rtype}, p);
      % "put(rlb, 'description, doc)"
      % [doc] is a string; a one-line description of the function:
      push({'put, mkquote rlb, ''description, doc}, p);
      % "put(rlb, 'seealso, seealso)"
      % [seealso] is a list of AM services; those related to the function from a
      % documentation point of view.
      if seealso then
         push({'put, mkquote rlb, ''seealso,
            mkquote for each s in seealso collect compress('r . 'l . explode s)}, p);
      % "put(rlb, 'docs, docs)"
      % [docs] is a list of strings; documentation of the formal arguments given
      % in [names]; length(docs) = length(names):
      push({'put, mkquote rlb, ''docs, mkquote docs}, p);
%%       % An Alist for documentation with the rlhelp submodule:
%%       docal := {
%%       'synopsis . rl_docSynopsis(rlb, names, types, defaults),
%%       'returns . rtype,
%%       'description . doc,
%%       'arguments . rl_docArguments(names, types, docs),
%%       'switches . rl_docSwitches(names, types, docs)};
%%       push({'put, mkquote rlb, ''docal, mkquote docal}, p);
      %
      % Here starts the generation of the SM service:
      % "put(rl_b, 'rl_amService, rlb)"
      % a link to the corresponding SM service:
      push({'put, mkquote rl_b, ''rl_amService, mkquote rlb}, p);
      % A psopfn as the AM entry point:
      push({'put, mkquote rlb, ''psopfn, mkquote rl_b!$}, p);
      % "put(rl_b!$, 'cleanupfn, 'rl_cleanup)"
      % The function bound to the psopfn:
      push({'put, mkquote rl_b!$, ''cleanupfn, ''rl_cleanup}, p);
      % "put(rl_b!$, 'number!-of!-args, 1)"
      push({'put, mkquote rl_b!$, ''number!-of!-args, 1}, p);
      % procedure rl_b!$(u);
      %    rl_servicewrapper(rl_!*b, u, names, X, defaults, Y, rl_b!*, rlb),
      %       where X = for each x in types collect rl_typeString2TypeForm x,
      %             Y = rl_typeString2TypeForm rtype;
      push(
         {'de, rl_b!$, '(u),
            {'rl_servicewrapper,
               mkquote rl_!*b,
               'u,
               mkquote names,
               mkquote for each x in types collect rl_typeString2TypeForm x,
               mkquote defaults,
               mkquote rl_typeString2TypeForm rtype,
               mkquote rl_b!*,
               mkquote rlb}},
         p);
      % "fluid fluids"
      % All switches corresponding to switch arguments are made fluid:
      if fluids then push({'fluid, mkquote fluids}, p);
      % A wrapper around the SM entry point with lambda binding for the
      % switches:
      % "put(rl_!*b, 'number!-of!-args, length rl_!*args)"
      push({'put, mkquote rl_!*b, ''number!-of!-args, length rl_!*args}, p);
      % procedure rl_!*b(..., rl_!*args[i], ...);
      %    apply(rl_b, rl_args);
      push({'de, rl_!*b, rl_!*args,
         {'apply, mkquote rl_b, 'list . rl_args}}, p);
      p := rl_formServiceSm1(rl_b, rl_b!*, rl_args, p);
      return 'progn . reversip p
   end;

asserted procedure rl_formServiceAnalyzeSpec(spec: Alist): List;
   begin
      scalar b, doc, seealso, names, types, defaults, docs, rtype, rl_args, rl_!*args,
         default, pos, name, type;
      integer minswitch, maxother, maxall;
      % Determine the base name of the service:
      b := lto_eatsoc('name, spec, {"missing service name in", spec});
      % Determine arguments and their order. Construct corresponding lists of
      % formal parameters:
      minswitch := length spec;  % initialize with upper bound on number of args
      for each pr in spec do
         if car pr eq 'arg then <<
            name := lto_eatsoc('name, cdr pr,
               {"arg without name in service", b});
            pos := lto_eatsoc('pos, cdr pr,
               {"arg", name, "without pos in service", b});
            if assoc(pos, names) then
               rederr {"pos", pos, "specified twice in service", b};
            doc := lto_catsoc('doc, cdr pr) or "";
            % In [spec] there are both [type] and [typestring] present, where
            % the latter has been generated by the stat. We need the strings to
            % preserve case for the help system. Within the present function we
            % are using both [type] and [typestring]. For the sake of
            % modularization we return only the string, at the price of
            % converting them once more into identifiers later on. All this
            % happens during compilation and is not time-critical. Also, there
            % is some hope for a case-sensitive Reduce in the future where that
            % reduncance would entirly disappear.
            type := lto_eatsoc('type, cdr pr,
               {"arg", name, "without type in service", b});
            if type = "Switch" then <<
               % Switches are Redlog switches to be lambda-bound during the
               % call. The argument name is without the leading "rl." Default is
               % the corresponding (global) switch setting.
               minswitch := min2(pos, minswitch);  % smallest Switch position
               maxall := max2(pos, maxall);  % largest overall position
               default := intern compress append(explode '!*rl, explode name);
               push(pos . (name . default), defaults);
               push(pos . default, rl_!*args)
            >> else <<
               maxother := max2(pos, maxother);  % largest non-Switch position
               maxall := max2(pos, maxall);
               default := atsoc('default, cdr pr);
               if default then
                  push(pos . (name . cdr default), defaults);
               push(pos . name, rl_args);
               push(pos . name, rl_!*args)
            >>;
            push(pos . name, names);
            push(pos . doc, docs);
            push(pos . type, types)
         >> else if car pr eq 'returns then <<
            % [returns] may be not present at all, which means that the service
            % does not return anything meaningful. On the other hand, if it is
            % present, then we insist on the specification of a return type.
            rtype := lto_eatsoc('type, cdr pr,
               {"service", b, "without return type"})
         >> else if car pr eq 'seealso then <<
            push(cdr pr, seealso)
         >>;
      % We insist that positions are numbered 1, ..., n without gaps:
      if not eqn(maxall, length names) then
         rederr {"bad arg position numbering in service", b};
      % Switches must come after all other arguments:
      if minswitch neq length spec and minswitch neq maxother + 1 then
         rederr {"bad switch positions in service", b};
      % Argument names including Switches in the right order:
      names := rl_sortAndProject names;
      % Argument doc strings, possible empty, in the right order:
      docs := rl_sortAndProject docs;
      % Types including Switches in the right order:
      types := rl_sortAndProject types;
      % Argument names without Switches in the right order:
      rl_args := rl_sortAndProject rl_args;
      % Non-Switch argument names followed by defaults for the Switchs, i.e.
      % !*rl<flag> instead of <flag>. This will be used within the body of
      % rl_!*<b>:
      rl_!*args := rl_sortAndProject rl_!*args;
      % PSL has a limitation of 14 function arguments. We do not want to make an
      % effort to work around this in any way. Our philosophy is rather that no
      % function should depend on more than 14 parameters (including relevant
      % switches). At present, e.g., cl_simpl still depends on more. We must to
      % work on this.
      if length rl_!*args > 14 then
         rederr {"too many arguments for service", b};
      % An Alist mapping names (including Switchs) to default values:
      defaults := rl_sortAndProject defaults;
      doc := lto_catsoc('doc, spec) or "";
      seealso := sort(seealso, function ordp);
      return {b, doc, seealso, names, types, defaults, docs, rtype, rl_args, rl_!*args}
   end;

asserted procedure rl_formServiceFunctionNames(rl_: Id, b: Id): List;
   begin scalar rl, rl_b, rl_!*b, rlb, rl_b!$, rl_b!*;
      rl_ := reversip explode rl_;
      % The AM prefix has no underscore:
      rl := reverse cdr rl_;
      rl_ := reversip rl_;
      rl_b := intern compress append(rl_, explode b);
      rl_!*b := intern compress append(rl_, append(explode '!*, explode b));
      rlb := intern compress append(rl, explode b);
      rl_b!$ := intern compress nconc(explode rl_b, '(!! !$));
      % rl_b!* will actually be a fluid, not a function:
      rl_b!* := intern compress nconc(explode rl_b, '(!! !*));
      return {rl_b!*, rl_b, rl_!*b, rl_b!$, rlb}
   end;

asserted procedure rl_typeString2TypeForm(s: String): Any;
   % Here we are at a very subtle point: The string [s] contains a type either
   % atomic like "Integer" or composite like "List(Integer)." We want to use our
   % xread-based ioto_sxread rather than parsing composite types ourselves. The
   % problem is that we are not case-sensitve so that xread would crash on
   % reading Integer, which is an RLISP type. Our solution here is to once more
   % locally switch on case-sensitivity and then explicitly convert to lower
   % case AFTER parsing. Notice that there is an assumtion here that our type in
   % [s] is either an identifier or a flat list of identifiers. In fact, already
   % in our stat above, where [s] originates from, only local case-sensitivity
   % allowed us to parse types using xread. In the rltype module the problem
   % does not occur, because there are only atomic types, and we do not use
   % xread but scan. If Reduce becomes case-sensitive in the future the code
   % here must be revised, and all type strings would probably disappear. If
   % someone decided that in a case-sensitive Reduce both [integer] and
   % [Integer] should denote that RLISP type, then we would have to think even
   % more.
   begin scalar x;
      x := ioto_sxread s where !*lower=nil, !*raise=nil;
      if idp x then
         return intern lto_downcase x;
      return for each y in x collect lto_downcase y
   end;

asserted procedure rl_formServiceSm(spec: Alist): List;
   begin scalar b, rl_b, rl_b!*, argl, sl, docal, p; integer n;
      b := lto_eatsoc('name, spec, {"missing service name in", spec});
      rl_b := intern compress nconc(explode 'rl_, explode b);
      rl_b!* := intern compress nconc(explode rl_b, '(!! !*));
      n := lto_eatsoc('argnum, spec, {"missing argnum in", spec});
      push(lto_at2str rl_b, sl);
      push("/", sl);
      push(lto_at2str lto_int2id n, sl);
      docal := {
         'synopsis . lto_sconcat reversip sl,
         'description . lto_catsoc('doc, spec) or ""};
      push({'put, mkquote rl_b, ''docal, mkquote docal}, p);
      argl := for i := 1:n collect mkid('a, i);
      p := rl_formServiceSm1(rl_b, rl_b!*, argl, p);
      return 'progn . reversip p
   end;

asserted procedure rl_formServiceSm1(rl_b: Id, rl_b!*: Id, argl: List, p: List): List;
   % Build the SM interface: rl_<b> is the SM entry point. It applies the
   % function stored in a fluid rl_<b>!*. That function depends on the current
   % context. All those fluids are collected in in fluid list rl_servl!*, where
   % they are found and rebound with context swithes via rl_set. Prog statements
   % are added to p, all in reverse order.
   begin
      % Make the rl_<b>!* identifier fluid, and add it to rl_servl!*, which is
      % used by rl_set:
      push({'fluid, mkquote {rl_b!*}}, p);
      push({'setq, 'rl_servl!*, {'cons, mkquote rl_b!*, 'rl_servl!*}}, p);
      % "put(rlb, 'rl_support, 'smservice)"
      push({'put, mkquote rl_b, ''rl_support, ''rl_smservice}, p);
      % and add it to the list
      push({'setq, 'rl_services!*, {'cons, mkquote rl_b, 'rl_services!*}}, p);
      % Create the actual SM entry point function:
      push({'put, mkquote rl_b, ''number!-of!-args, length argl}, p);
      push({'de, rl_b, argl, {'apply, rl_b!*, 'list . argl}}, p);
      return p
   end;

asserted procedure rl_sortAndProject(al: Alist): List;
   for each pr in sort(al, function(lambda(x, y); car x < car y)) collect
      cdr pr;

asserted procedure rl_docSynopsis(f: Id, names: List, types: List, defaults: Alist): String;
   begin scalar sl, name, default;
      push(id2string f, sl);
      push("(", sl);
      while types and car types neq "Switch" do <<
         name := pop names;
         push(id2string name, sl);
         default := atsoc(name, defaults);
         if default then <<
            push(" = ", sl);
            if stringp cdr default then <<
               push("""", sl);
               push(cdr default, sl);
               push("""", sl)
            >> else
               push(ioto_smaprin cdr default, sl)
         >>;
         push(": ", sl);
         push(pop types, sl);
         if types then
            push(", ", sl)
      >>;
      if types then
         push("...", sl);
      push(")", sl);
      return lto_sconcat reversip sl
   end;

asserted procedure rl_docArguments(names: List, types: List, docs: List): Alist;
   begin scalar sl;
      while types and car types neq "Switch" do <<
         pop types;
         push(id2string pop names . pop docs, sl)
      >>;
      return reversip sl
   end;

asserted procedure rl_docSwitches(names: List, types: List, docs: List): Alist;
   begin scalar sl;
      while types and car types neq "Switch" do <<
         pop types;
         pop names;
         pop docs
      >>;
      while names do
         push(id2string pop names . pop docs, sl);
      return sl
   end;

asserted procedure rl_servicewrapper(rl_!*b: Applicable, u: List, names: List, types: List, defaults: Alist, rtype: Any, rl_b!*: Id, rlb: Id): Any;
   % [rl_bname] is the SM entry point of the service called. [args] are the
   % passed arguments; [names] are the names of the specified arguments, [types]
   % are their types, and defaults are their default values. [rtype] is the type
   % of the return value of [rl_bname].
   begin scalar g, rargs, nargs, w, name; integer argc, pos;
      if null eval rl_b!* then
         rederr {"service", rlb, "not available in current context", rl_cid!*};
      % Construct a list [rlist] to be filled in-place with the parameters
      % determined throughout this procedure. Switches are inintialized with
      % themselves, because the default is to use the global switch setting. All
      % other parameters are initialized with a safe placeholder.
      argc := length names;
      g := gensym();
      for i := 1:argc do push(g,rargs);
      % We follow the Python convention that positional parameters have priority
      % over named parameters. In a first pass we fill positional parameters
      % into [rargs] and save named parameters in an Alist [nargs].
      for each arg in u do <<
         pos := pos + 1;
         % For named parameters we admit both '=>' (replaceby) and '=' equal.
         % However, '=' can lead to ambiguities, when the "equations" occurs at
         % a position where it would make sense as a positional parameter (e.g.
         % a formula). In such cases we decide in favor of the positional
         % argument. We expect such situations to be rare. Users would use
         % variables names in single equations that do not clash with parameter
         % names, or just use '=>' in such cases. Relevant types are explicitly
         % flagged [equational].
         if eqcar(arg, 'replaceby) or
            eqcar(arg, 'equal) and not flagp(nth(types, pos), 'equational)
         then
            push(cadr arg . caddr arg, nargs)
         else
            nth(rargs, pos) := arg
      >>;
      % Second pass: Fill the gaps in [rargs] with named parameters while
      % makeing sure the following:
      % 1. Accept no clashes. In particular, named parameters must not clash
      %    with previously determined positional parameters.
      % 2. Accept no named parameter with an unknown name.
      for each arg in nargs do <<
         w := memq(car arg, names);
         if not w then
            rederr {"unknown named parameter", car arg};
         % Determine the position from the name, and check whether that spot is
         % stil free.
         pos := argc - length w + 1;
         if nth(rargs, pos) neq g then
            rederr {"ambiguous specification for parameter", car arg};
         % If so, fill it in-place.
         nth(rargs, pos) := cdr arg
      >>;
      % Third pass: In the end every formal parameter must be filled with
      % default values and those default values must exist. We do this also
      % in-place.
      pos := 0;
      for each arg on rargs do <<
         pos := pos + 1;
         if car arg eq g then <<
            name := nth(names, pos);
            w := atsoc(name, defaults);
            if not w then
               rederr {"missing parameter", name, "at position", pos};
            car arg := cdr w
         >>
      >>;
      % Now [rargs] is a complete list of arguments in the correct order, which
      % still have to be evaluated/converted.
      rargs := for each arg in rargs collect
         rl_convertArg(arg, pop types, 'a2s);
      % Finally apply the service, evaluate the result for AM, and return.
      w := apply(rl_!*b, rargs);
      if rl_excP w then  % handle exceptions
         rl_excErr w;
      w := rl_convertArg(w, rtype, 's2a);
      return w
   end;

asserted procedure rl_convertArg(x: Any, type: Any, x2y: Id): Any;
   apply(rl_conversionFunction(type, x2y), {x});

asserted procedure rl_conversionFunction(type: Any, x2y: Id): Any;
   begin scalar type, super, f, fl, kwl;
      if idp type then <<
         f := rl_typeEntry(type, x2y);
         if f then
            return f;
         super := rl_typeInherits type;
         if super then
            return rl_conversionFunction(super, x2y);
         rederr {"missing", x2y, "conversion for type", type}
      >>;
      if intern car type eq 'enum and x2y eq 'a2s then <<
         kwl := for each h in cdr type collect intern h;
         return {'lambda, '(x), {'apply, {'function, 'rl_a2sKeyword}, {'list, 'x, mkquote kwl}}};
      >>;
      if intern car type eq 'enum and x2y eq 's2a then
         return {'lambda, '(x), 'x};
      % Now type is something like Pair(List(Atom), Formula), where Pair, List,
      % Atom, Formula have conversion functions of arity 1+2, 1+1, 1+0, 1+0,
      % resp., counting "data + parameter functions."
      f . fl := for each ty in type collect
         {'function, rl_conversionFunction(ty, x2y)};
      return {'lambda, '(x), {'apply, f, {'cons, 'x, 'list . fl}}}
   end;

asserted procedure rl_a2sKeyword(x: Any, keywords: List);
   if x memq keywords then
      x
   else
      typerr(x, ioto_smaprin('!One!Of . keywords)) where !*lower=nil, !*raise=nil;

put('enum, 'rl_support, 'rl_type);
put('enum, 'rl_type, '((doc . (
   (description . "literal enumeration of admissible Redlog keywords")
   (example . "Enum(auto, cnf, dnf)")))));

% The following documents how to implement fancy printing of Enum types.
% However, with the current setup, it is necessary that the printed form can be
% parsed by xread for type conversion.
%
% asserted procedure rl_priEnum(s);
%    <<
%       prin2!* "[";
%       prin2!* cadr s;
%       for each x in cddr s do << prin2!* "|", prin2!* x >>;
%       prin2!* "]";
%       terpri!* nil
%    >>;
%
% put('!Enum, 'prifn, 'rl_priEnum);

asserted procedure rl_smServiceP(x: Any): Boolean;
   idp x and get(x, 'rl_support) eq 'rl_smservice;

asserted procedure rl_amServiceP(x: Any): Boolean;
   idp x and get(x, 'rl_support) eq 'rl_amservice;

asserted procedure rl_knownImplementations(x: Id): List;
   get(x, 'rl_knownImplementations);

asserted procedure rl_exc(x: Any): DottedPair;
   % Create an "exception" as a return value in case of unexpected situations,
   % e.g. inconsistent theories. Exceptions are recognized by
   % [rl_servicewrapper] in the AM/SM interface, where rl_excErr is called with
   % ['!*rl_exc!* . x]. SM Redlog code might explicitly checked for exceptions
   % using [rl_excP] and not necessarily throw an error, since some exceptions
   % can be managed.
   '!*rl_exc!* . x;

% Return values constructed with [rl_exc] should be ignored by the assert
% module. For Redlog it is recommended to specifiy, e.g., "Formula" as a return
% type of a function, which might use [rl_exc].
flag('(!*rl_exc!*), 'assert_ignore);

asserted procedure rl_excP(x: Any): Boolean;
   % Check is return value is an exception.
   eqcar(x, '!*rl_exc!*);

asserted procedure rl_excErr(exc: DottedPair);
   % Throw an error in case of exception.
   rederr cdr exc;

% The following is temporary, and when finally removing it the corresponding
% autoloads in support/entry.red must be removed, too. Note that using copyd
% here would not be compatible with autoloading.

asserted procedure rl_exception(x: Any): DottedPair;
   rl_exc x;

asserted procedure rl_exceptionp(x: Any): Boolean;
   rl_excp x;

endmodule;

end;