-
Notifications
You must be signed in to change notification settings - Fork 0
/
support.dtx
2310 lines (2309 loc) · 86.1 KB
/
support.dtx
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
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
%
% \iffalse driver
%<*driver>
\documentclass{mtmtcl}
\begin{document}
\DocInput{support.dtx}
\end{document}
%</driver>
% \fi
%
%
%
% \section{Auxilliary interfaces}
%
% \subsection{Equality}
% \label{Ssec:Equality}
%
% A very great number of basic mathematical claims have the form of
% an equality, but a prerequisite for speaking about that is that
% there is an equality relation in the first place. Like all other
% relations, equality is something relative to a structure.
%
% \begin{APIspec}{equality}{1.0}
% The |equality| interface v\,1.0 is applicable to principal
% structures. It implies that there exists a method
% \begin{APIdescription}{structure}
% \begin{APImethod}{=}
% \word{element} \word{element}
% \end{APImethod}
% which returns a boolean, and thus constitutes a binary relation
% on the principal set of elements $S$. Moreover this relation
% must be an equivalence relation, i.e.,
% \begin{displaysyntax}
% [\meta{structure} = $a$ $a$]
% \end{displaysyntax}
% is boolean true for any \(a \in S\) (reflexivity),
% \begin{displaysyntax}
% [\meta{structure} = $a$ $b$]\par
% [\meta{structure} = $b$ $a$]
% \end{displaysyntax}
% are equivalent for any \(a,b \in S\) (symmetry), and for all
% \(a,b,c \in S\) if both of
% \begin{displaysyntax}
% [\meta{structure} = $a$ $b$]\par
% [\meta{structure} = $b$ $c$]
% \end{displaysyntax}
% are true then
% \begin{displaysyntax}
% [\meta{structure} = $a$ $c$]
% \end{displaysyntax}
% must be true as well (transitivity).
% \end{APIdescription}
% \end{APIspec}
%
% \begin{definition}
% A method taking as input zero or more elements of structures
% which support the |equality| v\,1.0 interface is said to be
% \defining{congruent} if two arguments lists which are pointwise
% |=|-equal produce equal output, where the latter `equal' should
% be interpreted in accordance to how the output values of the
% method is described.
% \end{definition}
%
% \begin{APIspec}{equality}{1.1}
% Version 1.1 of the |equality| interface extends the |=| to be
% variadic.
% \begin{APIdescription}{structure}
% \begin{APImethod}{=}
% \word{element}\regstar
% \end{APImethod}
% Returns boolean true if the binary form would return true for
% any two of \word{element}s.
%
% As usual, the status of |=| as equivalence relation implies that
% \begin{displaysyntax}
% [$S$ = $a_1$ $a_2$ $\dots$ $a_n$]
% \end{displaysyntax}
% is true if and only if all of
% \begin{displaysyntax}
% [$S$ = $a_1$ $a_2$]\par
% [$S$ = $a_2$ $a_3$]\par
% $\vdots$\par
% [$S$ = $a_{n-1}$ $a_n$]
% \end{displaysyntax}
% are true.
% \end{APIdescription}
% The nullary and unary forms of |=| always return true, but this is
% sensible behaviour when applied to expanded lists. In particular,
% it is a consequence of having as property that adding extra
% \word{element}s can change the result from true to false, but not
% vice versa.
% \end{APIspec}
%
% \begin{tcl}
%<*docstrip.tcl::catalogue>
pkgProvide mtmtcl::adaptors::equality 1.0 adaptors::equality
%</docstrip.tcl::catalogue>
%<*adaptors::equality>
namespace eval mtmtcl::adaptors::equality {}
% \end{tcl}
% \setnamespace{mtmtcl::adaptors::equality}
%
% \begin{proc}{variadic_equal}
% Knowing the above two versions of \APIref{equality}{1.1}, one thing
% that can be done is to implement a variadic equality on top of
% the binary one. To that end, this procedure has the call syntax
% \begin{displaysyntax}
% |variadic_equal| \word{binary-equal} \word{argument}\regstar
% \end{displaysyntax}
% where the \word{binary-equal} is a command prefix with the syntax
% \begin{displaysyntax}
% \meta{binary-equal} \word{left} \word{right}
% \end{displaysyntax}
% that returns boolean true if \word{left} and \word{right} are
% equal, and boolean false otherwise. |variadic_equal| furthermore
% presumes that the relation so defined is an equivalence relation.
% It returns |1| if all \word{argument}s compare as equal, and |0|
% otherwise.
% \begin{tcl}
proc mtmtcl::adaptors::equality::variadic_equal {prefix args} {
if {![llength $args]} then {return 1}
set left [lindex $args 0]
foreach right [lrange $args 1 end] {
if {![{*}$prefix $left $right]} then {return 0}
}
return 1
}
% \end{tcl}
% \end{proc}
%
% \begin{proc}{to-1.1}
% This procedure constructs a command prefix satisfying
% \APIref+{equality}{1.1} from one satisfying
% \APIref+{equality}{1.0}. The call syntax is
% \begin{displaysyntax}
% mtmtcl::adaptors::equality::to-1.1 \word{base}
% \begin{regblock}[\regstar] \word{option} \word{value}
% \end{regblock}
% \end{displaysyntax}
% and the return value is the constructed command prefix.
% Currently, the only option supported is \texttt{-strict}, which
% takes a boolean value and defaults to false. Strictness refers
% to adherence to the API mechanism in general; see below for
% details on what this means.
%
% First check the basics: If \meta{base} already supports
% version~1.1 of \texttt{equality}, then it is the wanted result.
% If \meta{base} doesn't support version~1.0, then there's nothing
% we can do about it.
% \begin{tcl}
proc mtmtcl::adaptors::equality::to-1.1 {base args} {
if {[{*}$base API equality 1.1]} then {return $base}
if {![{*}$base API equality 1.0]} then {
return -code error "Prefix does not support equality 1.0: $base"
}
% \end{tcl}
% With those trivial cases out of the way, it is time to get down
% to business. In this case, the prefix will be a call to a lambda
% that dispatches the |=| subcommand to the |variadic_equal|
% procedure. It also handles the |API| subcommand, since it changes
% what version of \texttt{equality} is supported. The syntax for a
% complete call will be
% \begin{displaysyntax}
% apply \word{lambda} \word{base} \word{API-dict}
% \word{subcommand} \word{argument}\regstar
% \end{displaysyntax}
% \begin{tcl}
set lambda [list {base API subcmd args}]
% \end{tcl}
% What it does with other subcommands than |=| and |API| depends on
% the \describeopt+{to-1.1}{-strict} setting; in the non-strict case,
% it maps all other subcommands to their \meta{base} counterparts
% and presumes no other interface is affected by the redefinition of
% |=| (and also that the interfaces are static).
% \begin{tcl}
if {[dict exists $args -strict] && [dict get $args -strict]} then {
lappend lambda {
if {$subcmd eq "="} then {
variadic_equal [list {*}$base =] {*}$args
} elseif {$subcmd eq "API"} then {
::API::static $API {*}$args
} else {
tailcall {*}$base $subcmd {*}$args
}
}
set API [{*}$base API]
dict set API equality 1.1
} else {
% \end{tcl}
% If going strictly by the book however, one cannot assume that any
% interface other than \texttt{equality} version~1.1 is supported
% by the result, so that is all that will be claimed. The
% unmodified \meta{base} structure is made available using a new
% |understructure| method, i.e., \meta{result}| understructure API|
% queries the \meta{base} |API|.
% \begin{tcl}
lappend lambda {
switch -- $subcmd "=" {
variadic_equal [list {*}$base =] {*}$args
} "API" {
::API::static $API {*}$args
} "understructure" {
tailcall {*}$base {*}$args
} default {
tailcall {*}$base $subcmd {*}$args
}
}
set API {equality 1.1}
}
lappend lambda [namespace current]
return [list ::apply $lambda $base $API]
}
%</adaptors::equality>
% \end{tcl}
% \end{proc}
%
% In some cases, it is important to have a canonical representation for
% an value. The most immediate need for this occurs when values are
% used as keys in \Tcl\ dictionaries, as equality of keys is always
% string equality. There are two naturally occurring approaches to
% canonical representation: automatic and manual conversion to
% canonical form. Automatic canonicity is something often seen with
% numbers (in particular integers), whereas for quotient algebras the
% problem of canonical representation (normal forms) is felt even at
% the mathematical level.
%
% In \Tcl, lists are containers with automatic canonicity\Ldash two
% lists generated by list commands are equal as strings if and only if
% they have the same number of elements and the $i$th elements of the
% lists are equal as strings\Dash whereas dictionaries are not. The
% catch for dictionaries is that the order of the keys is not uniquely
% determined, and even though only a few orders occur in practice,
% the exact order used depends on how the dictionary was constructed.
%
%
% \begin{APIspec}{canonise}{1.0}
% The |canonise| interface v\,1.0 is applicable to principal
% structures. It implies that there exists a method
% \begin{APIdescription}{structure}
% \begin{APImethod}{canonise}
% \word{element}
% \end{APImethod}
% which returns the canonical form of the \word{element}. This
% method has to satisfy the property that
% \begin{displaysyntax}
% [$S$ canonise [$S$ canonise $a$]]\par
% [$S$ canonise $a$]
% \end{displaysyntax}
% are equal as strings for all elements $a$ of the
% \meta{structure} $S$.
% \end{APIdescription}
% \end{APIspec}
%
% \begin{APIspec}{canonise}{1.1}
% It is natural to relate canonicity to equality, but that requires
% having an equality relation to relate it to.
% \begin{APIdescription}{structure}
% \begin{APImethod}{=}
% \word{element} \word{element}
% \end{APImethod}
% This method satisfies the \texttt{equality} (v\,1.0) interface.
%
% \begin{APImethod}{canonise}
% \word{element}
% \end{APImethod}
% Two elements $a$ and $b$ of a \meta{structure} $S$ are
% |=|-equal if and only if the two expressions
% \begin{displaysyntax}
% [$S$ canonise $a$]\par
% [$S$ canonise $b$]
% \end{displaysyntax}
% are equal as strings.
% \end{APIdescription}
% \end{APIspec}
%
% At this point, it would be possible to define an adaptor that from
% a \APIref+{canonise}{1.0} structure constructs a
% \APIref+{canonise}{1.1}, just as above. For the moment, that
% programming task is left as an exercise to the reader.
% Alternatively, one could modify the above |equality::to-1.1|
% procedure so that it will create an \APIref+{equality}{1.1}
% structure out of a \APIref+{canonise}{1.0} structure.
%
%
% \subsection{Data export}
%
% The basic format for exporting structure elements is as a
% data-tree, so that further processing is easy in \Tcl.
% The node types (\word{tag}s) used should primarily be those defined
% in the OpenMath standard, but there are exceptions (e.g.~|integer|)
% in which a more \Tcl-native encoding is preferable.
% For processing to the end of rendering data, it is often
% interesting to incorporate presentation-oriented information in the
% data-tree. Here it is preferable to use MathML-elements to encode
% such information, when there is one which is suitable for the
% problem at hand (e.g.~|mfenced| for bracketing subexpressions).
% MathML does however seem less useful as a \emph{standard} for the
% data.
%
% \changes{0}{2008/10/01}{Prioritising OpenMath over MathML.
% Introducing the idea of \emph{temporary} conversions from
% OpenMath node types to specialised node types. (LH)}
%
%
% \stringtypeheading{node type}{Data-tree node types:}
% \stringtypeheading{attribute}{Data-tree attributes:}
%
% The key route from \mtl\ to OpenMath is the |export| interface,
% which specifies how structure elements are converted to
% near-OpenMath data-trees.
%
% \begin{APIspec}{export}{2.0} \label{export-2.0}
% This interface is applicable to principal structures. It provides
% a method |export| for converting the internal representation of
% an element to an external format. The syntax for this method is:
% \begin{APIdescription}{structure}
% \begin{APImethod}{export}
% \word{element} \word{common attributes}
% \end{APImethod}
% where \word{element} is the element to export. The return
% value is a data-tree that encodes the \word{element} as
% near-OpenMath.
%
% The \word{common attributes} is a dictionary of common
% attributes for nodes in the tree. The |export| method is
% however allowed to override part or all of it, so it is
% prefectly acceptable to ignore the \word{common attributes}
% entirely for some sets of nodes. The typical use is that
% the \word{common attributes} are used for |OMA| nodes and
% get |cd| and |name| entries added in |OMS| nodes.
%
% For |export| methods that call other |export| methods
% recursively, there is however the condition that they must
% update the \describestring+[attribute]{mtmtcl:path} entry in
% the \word{common attributes} dictionary. The value of this
% attribute is a list of strings, typically a list of method
% names. The purpose of this list is to establish a system for
% addressing subordinate structures by mirroring the command
% prefix that would be used to access its methods. If a
% structure $S_1$ makes use of the |export| method of another
% structure $S_2$ and $S_2$ can be accessed using the $s$
% method of $S_1$, then the |mtmtcl:path| used for the
% \texttt{[$S_2$ export $\dotsb$]} call should have an $s$
% append to its value from the \texttt{[$S_1$ export $\dotsb$]}
% call.
%
% The |mtmtcl:path| may be extended with method names also when
% there is no recursive call to the |export| method. This can
% be done e.g.~to clarify which method corresponds to a
% particular operation symbol.
% \end{APIdescription}
% \end{APIspec}
%
% \medskip
%
% \begin{APIspec}{import}{1.0}
% Where there is export, this is usually also import.
% \begin{APIdescription}{structure}
% \begin{APImethod}{import}
% \word{path} \word{data-tree}
% \end{APImethod}
% returns the element of the \meta{structure} that corresponds
% to the \word{data-tree}, or throws an error if the
% \word{data-tree} couldn't be interpreted as an element of the
% \meta{structure}. The |-errorcode| of such an error should be
% \begin{displaysyntax}
% API import EDOM \word{who} \word{bad node}
% \end{displaysyntax}
% where |EDOM| is POSIX for ``domain error'', \word{who} is the
% \word{path} of the party detecting the error, and \word{bad
% node} should be the \word{data-tree} which couldn't be
% interpreted.
%
% The \word{path} serves two purposes. One is that it may be
% matched against \describestring+[attribute]{mtmtcl:path}
% attributes in the \word{data-tree}, which can aid in
% interpreting abbreviated \word{data-tree}s (for example trees
% where unary addition or multiplication nodes have been
% elided). The other is to identify the substructure that
% has thrown an |EDOM| error. The idea is that it should be
% handled as |mtmtcl:path| by the |export| method, i.e., if the
% |import| method of structure $S_1$ makes use of the |import|
% method of structure $S_2$, and $S_2$ can be accessed using
% the $s$ method of $S_1$, then the \texttt{[$S_2$ import $P_2$
% $\dotsb$]} call used by the \texttt{[$S_1$ import $P_1$
% $\dotsb$]} should be such that \(P_2 = P_1 s\) (list append).
%
% The \word{path} should not be taken into account when
% interpreting a \word{data-tree} without |mtmtcl:path|
% attributes.
% \end{APIdescription}
% \end{APIspec}
%
% \medskip
%
%
% \subsection{More on equality}
% \label{Ssec:MoreEquality}
%
% \begin{APIspec}{onlycanonical}{1.0}
% The |onlycanonical| interface is applicable to arbitrary structure.
% Version 1.0 of it means that the \emph{only} valid representations
% for elements are the canonical ones.
% \end{APIspec}
%
%
% \begin{APIspec}{autocanonical}{1.0}
% The |autocanonical| interface v\,1.0 is applicable to
% arbitrary structures. It is supported if all elements computed
% by the structure methods are on canonical form.
% \end{APIspec}
%
% Version~1.0 of |autocanonical| is problematic in that it makes a
% vague reference to ``all elements computed by the structure''\Dash
% a promise that it might be hard to verify. Two alternatives are:
% \begin{enumerate}
% \item
% Split |autocanonical| into a family of interfaces (one for each
% method).
% \item
% Create a new version of the interface which makes provides a
% method for quering whether a method is autocanonical.
% \end{enumerate}
% Both are possible, although the first looks a bit strange.
%
% \begin{APIspec}{autocanonical \meta{method}}{1.0}
% This interface claims that elements output from the \meta{method}
% are on canonical form. \textbf{Note:} For greater
% distinctiveness, the \meta{method} is \emph{the canonical
% list-coded form of the method name}, rather than the raw
% string.\footnote{
% Note to self:
% Therefore the interface name should preferably appear as
% \texttt{autocanonical\PrintChar{32}\word{method}} rather than
% \texttt{autocanonical\PrintChar{32}\meta{method}}, but that
% will have to wait until the \textsf{tclldoc} \LaTeX\ package
% gets based on \textsf{harmless}.
% }
% This makes a difference if for example the method name contains a
% space.
% \end{APIspec}
%
% \begin{APIspec}{autocanonical}{2.0}
% Structures supporting version 2.0 of the |autocanonical| interface
% have a method
% \begin{APIdescription}{structure}
% \begin{APImethod}{autocanonical}
% \word{method}
% \end{APImethod}
% This call returns a boolean. If it returns boolean true, then
% this \meta{structure} has a method \word{method} which only
% outputs elements on canonical form.
% \end{APIdescription}
% \end{APIspec}
%
% \begin{tcl}
%<*pkg>
namespace eval ::mtmtcl::sets {
namespace path [list [namespace parent]]
}
%</pkg>
% \end{tcl}
% \setnamespace{mtmtcl::sets}
%
% \begin{tcl}
%<*docstrip.tcl::catalogue>
pkgProvide mtmtcl::sets::universe 1.0 universe
%</docstrip.tcl::catalogue>
%<*universe,pkg>
package require mtmtcl::openmath 1.0
namespace eval ::mtmtcl::sets {}
% \end{tcl}
%
% \begin{proc}{universe}
% The |universe| structure simply has as elements all \Tcl\
% strings, but no actual operations on them. It is meant as a dummy
% structure to use in cases where a set of values need to be
% presented as residing in a structure, but one doesn't want to
% wrap the true thing up as a structure.
% \changes{0.1}{2010/01/28}{Structure added. (LH)}
%
% The call syntax is
% \begin{displaysyntax}
% ::mtmtcl::sets::universe \word{subcommand} \word{argument}\regstar
% \end{displaysyntax}
% \begin{tcl}
proc ::mtmtcl::sets::universe {subcmd args} {
switch -- $subcmd "API" {
% \end{tcl}
% The set of subcommands and supported interfaces are chosen so that
% it at least becomes possible to form formal linear combinations
% of |universe| elements.
% \begin{tcl}
::API::static {
equality 1.0
canonise 1.1
onlycanonical 1.0
export 2.0
import 1.0
} {*}$args
} "=" {
string equal [lindex $args 0] [lindex $args 1]
} "canonise" {
lindex $args 0
} "export" {
list OMFOREIGN [
dict replace [lindex $args 1] encoding\
application/x-mtmtcl-internal-representation
] [list [list \#text [lindex $args 0]]]
} "import" {
if {[lindex $args 1 0] eq "OMFOREIGN"} then {
::mtmtcl::openmath::gettext [lindex $args 1] ""
} else {
return -code error\
-errorcode [concat [list API import EDOM] [lrange $args 0 1]]\
"Universe elements are expected to be OMFOREIGN"
}
} default {
return -code error "Unknown subcommand \"$subcmd\": must be\
API, =, canonise, export, or import"
}
}
%</universe,pkg>
% \end{tcl}
% \end{proc}
%
% \begin{APIspec}{finite set}{1.0}
% The |finite set| interface v\,1 is for sets like
% $\{a_1,\dotsc,a_n\}$ that are introduced by listing all the
% elements. It is in particular a single-sorted interface.
%
% \begin{APIdescription}{set}
% \begin{APImethod}{=}
% \word{element} \word{element}
% \end{APImethod}
% The |=| method satisfies v\,1.0 of the |equality| interface.
%
% \begin{APImethod}{elements}
% \end{APImethod}
% The |elements| method returns the list of elements in the set.
% No two elements of this list may be |=|-equal.
% \end{APIdescription}
% \end{APIspec}
%
% \begin{APIspec}{finite set}{1.1}
% Version 1.1 of |finite set| refines version 1.0 by making it
% possible to identify elements by index.
% \begin{APIdescription}{set}
% \begin{APImethod}{elements}
% \end{APImethod}
% The order of elements in the list returned by this method must
% not change over time.
% \end{APIdescription}
% \end{APIspec}
%
%
% \begin{tcl}
%<*docstrip.tcl::catalogue>
pkgProvide mtmtcl::sets::finite_ordinal 1.0 ordinal
%</docstrip.tcl::catalogue>
% \end{tcl}
%
%
% \begin{proc}{finite_ordinal}
% In set theory (at least the most common flavours of it), the
% \emph{ordinal numbers} is a number system construction where each
% number is the set of all smaller numbers, so that \(0 =
% \emptyset\), \(1 = \{0\} = \{\emptyset\}\), \(2 = \{0,1\} = \bigl\{
% \emptyset, \{\emptyset\} \bigr\}\), \(3 = \{0,1,2\} = \Bigl\{
% \emptyset, \{\emptyset\}, \bigl\{ \emptyset, \{\emptyset\} \bigr\}
% \Bigr\}\), and so on. Theoretically this is useful mostly for the
% infinite ordinals, where one can define the first inifinite ordinal
% $\omega$ simply as the set of all finite ordinals (natural
% numbers), and then continue with \(\omega + 1 = \omega \cup
% \{\omega\}\), \(\omega + 2 = \omega \cup \{\omega, \omega+1\}\),
% etc., with the first uncountable ordinal arising precisely as the
% set of all countable ordinals. Obviously, these transfinite
% applications are not the subject here.
%
% Instead, this procedure merely usurps the name for the family of
% finite set structures of the form $\{0,\dotsc,n-1\}$, since these
% technically happen to be finite ordinals. The basic call syntax is
% \begin{displaysyntax}
% |::mtmtcl::sets::finite_ordinal| \word{cardinality}
% \word{method} \word{argument}\regstar
% \end{displaysyntax}
% whereas the return value depends on the \word{method}.
% \begin{tcl}
%<*ordinal,pkg>
namespace eval ::mtmtcl::sets {}
proc ::mtmtcl::sets::finite_ordinal {card method args} {
switch -- $method {
% \end{tcl}
%
% \begin{procmethod}{elements}
% This is the main method of this structure: construct a list of
% the integers $0$ through one less than the cardinality.
% \begin{tcl}
elements {
set res [list]
for {set n 0} {$n < $card} {incr n} {lappend res $n}
return $res
}
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{=}
% Equality is straightforward.
% \begin{tcl}
= { expr {[lindex $args 0] == [lindex $args 1]} }
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{canonise}
% However, since the above allows arbitrary integer
% representations, it might be best to define a canonisation
% method as well. This can be a good place to check argument
% validity.
% \begin{tcl}
canonise {
if {
[string is integer -strict [lindex $args 0]] &&\
[lindex $args 0] >= 0 && [lindex $args 0] < $card
} then {
return [expr {[lindex $args 0] + 0}]
} else {
return -code error "Not an element"
}
}
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{API}
% Finally, the supported interfaces must be listed.
% \begin{tcl}
API {
::API::static {equality 1.0 "finite set" 1.1 \
canonise 1.0} {*}$args
}
% \end{tcl}
% \end{procmethod}
%
% \begin{tcl}
}
}
%</ordinal,pkg>
% \end{tcl}
% \end{proc}
%
%
% \begin{tcl}
%<*docstrip.tcl::catalogue>
pkgProvide mtmtcl::sets::string_set 1.0 stringset
%</docstrip.tcl::catalogue>
% \end{tcl}
%
% \begin{proc}{string_set}
% This procedure implements a finite set of strings as a structure.
% The basic call syntax is
% \begin{displaysyntax}
% |::mtmtcl::sets::string_set| \word{element-list}
% \word{method} \word{argument}\regstar
% \end{displaysyntax}
% whereas the return value depends on the \word{method}.
% \begin{tcl}
%<*stringset,pkg>
namespace eval ::mtmtcl::sets {}
proc ::mtmtcl::sets::string_set {elements method args} {
switch -- $method {
% \end{tcl}
%
% \begin{procmethod}{elements}
% The list of elements is simply the |elements| parameter.
% \begin{tcl}
elements {return $elements}
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{=}
% Equality is as strings.
% \begin{tcl}
= { string equal [lindex $args 0] [lindex $args 1] }
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{canonise}
% The only valid representations are the canonical ones, but
% it is convenient to provide a canonisation method for users
% that expect one, even if it is trivial.
% \begin{tcl}
canonise {return [lindex $args 0]}
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{export}
% An appropriate implementation of this is to take the element
% as an |OMSTR| node.
% \begin{tcl}
export {
return [list OMSTR [lindex $args 1]\
[list [list \#text [lindex $args 0]]]]
}
% \end{tcl}
% It is quite likely that this implementation may seem
% inappropriate, and that other outputs (|OMV| nodes, |OMS|
% nodes, either of the above with |OMATTR|) are wanted
% instead. This is not an error, but an opportunity to provide
% alternative methods implementing the |finite set| interface;
% regardless of how one proceeds, it would be necessary to
% provide additional parameters for the structure.
% \end{procmethod}
%
% \begin{procmethod}{API}
% Finally, the supported interfaces must be listed.
% \begin{tcl}
API {
::API::static {equality 1.0 "finite set" 1.1 \
canonise 1.0 onlycanonical 1.0 export 2.0} {*}$args
}
% \end{tcl}
% \end{procmethod}
%
% \begin{tcl}
}
}
%</stringset,pkg>
% \end{tcl}
% \end{proc}
%
%
%
% \subsection{Naming}
%
% It is often useful to have symbolic names (that are independent of
% the string representation) for important structure elements, and
% translate back and forth between elements and names. Possible
% applications of this include
% \begin{longtable}{ll}
% \textbf{Command}& \textbf{Result}\endhead
% |float named pi|& $3.14159265359$\\
% |float named e|& $2.71828182846$\\
% |integer named Taxicab(2)|& $1729$\\
% $\mathbb{C}$| named i|& $i = \sqrt{-1}$\\
% $\mathbb{Q}[x,y]$| named x|& $x$
% \end{longtable}\noindent
% with the last two perhaps being the most interesting\Dash to give
% practical access to distinguished generators of a structure.
% Accordingly, some of the |generated|\dots\ interfaces below return
% names of generators (rather than the actual generator elements) since
% this is more convenient for several applications.
%
% \begin{APIspec}{named element}{1.0}
% The \verb*|named element| interface provides the basic
% functionality of mapping symbolic names to structure elements.
% \begin{APIdescription}{structure}
% \begin{APImethod}{named}
% \word{string}
% \end{APImethod}
% Returns the structure element whose symbolic name is
% \word{string}. It is not required that all return values are of
% the same sort, but whatever provides the name \word{string}
% should also provide information about what sort of element it
% denotes.
% \end{APIdescription}
% \end{APIspec}
%
% A natural extension would be to have an inverse operation |nameof|
% which returns the name of an element (or throws an error if it isn't
% one of the named elements), but this is complicated by the
% possibility of having several sorts; it is in principle possible that
% the same string could be the representation of two different named
% elements (provided they have different sorts). On the other hand, it
% could also be reasonable in some cases to have several names for a
% single element\dots
%
% Another natural extension is to have an operation |names| which
% returns the list of known symbolic names of elements. This would in
% particular imply that the list is finite, which is closely related to
% the property of being finitely generated.
%
% \begin{tcl}
%<*docstrip.tcl::catalogue>
pkgProvide mtmtcl::sets::variable_set 1.0 varset
%</docstrip.tcl::catalogue>
% \end{tcl}
%
% \begin{proc}{variable_set}
% This procedure implements a finite set of variables as a
% structure. It improves upon |string_set| in that it offers
% control over the presentation of a variable, and in that it
% supports naming variables. The basic call syntax is
% \begin{displaysyntax}
% |::mtmtcl::sets::variable_set| \word{element-list}
% \word{extra-dict} \word{method} \word{argument}\regstar
% \end{displaysyntax}
% where \word{element-list} is the list of variable names (|name|
% attribute values) and \word{extra-dict} is a dictionary of
% additional information. The primary keys into this dictionary are
% very much like options, whereas element-specific information (if
% any) typically appears under a secondary key. The primary keys
% currently supported are:
% \begin{description}
% \renewcommand{\makelabel}[1]{\hspace\labelsep
% \describeopt*+[mtmtcl::sets]{variable_sep}[proc]{#1}[key]^^A
% }
% \item[LaTeX_encoding]
% This entry is a dictionary, indexed by elements. The value is
% the |LaTeX_encoding| for the element in question.
% \item[names]
% This entry is a dictionary, indexed by names recognised by
% the |named| method, and the entries are corresponding
% variable names. If for example a variable is technically
% |name|d $\delta$, but one wishes to write |delta| in one's
% code, then one can put
% \begin{quote}
% |names {delta \u03B4 |\dots| }|
% \end{quote}
% in one's \word{extra-dict}.
% \item[pseudoexpression]
% This entry is a dictionary, indexed by elements. The value
% is a near-OpenMath data-tree that is used as the ``content''
% of the |OMV| node upon export. This can be used to improve
% the presentation of the variable.
% \end{description}
%
% The internal representation of an element of this structure is as
% a string, more precisely as a string which is an element of the
% \word{element-list}.
% \begin{tcl}
%<*varset,pkg>
namespace eval ::mtmtcl::sets {}
proc ::mtmtcl::sets::variable_set {elements extra method args} {
switch -- $method {
% \end{tcl}
%
% \begin{procmethod}{elements}
% The list of elements is simply the |elements| parameter.
% \begin{tcl}
elements {return $elements}
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{=}
% Equality is as strings.
% \begin{tcl}
= { string equal [lindex $args 0] [lindex $args 1] }
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{canonise}
% The only valid representations are the canonical ones, but
% it is convenient to provide a canonisation method for users
% that expect one, even if it is trivial.
% \begin{tcl}
canonise {return [lindex $args 0]}
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{named}
% Names are first looked up in the |names| dictionary, then taken
% as explicit variable |name|s.
% \begin{tcl}
named {
if {[llength $args] != 1} then {
return -code error "wrong # arguments, should be:\
<variable set> named {name}"
}
if {[dict exists $extra names [lindex $args 0]]} then {
return [dict get $extra names [lindex $args 0]]
} elseif {[lindex $args 0] in $elements} then {
return [lindex $args 0]
} else {
return -code error "unknown variable: [lindex $args 0]"
}
}
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{names}
% The set of variable names is just the set of elements.
% \begin{tcl}
names {return $elements}
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{export}
% This is the most complex method, since no less than two of the
% \word{extra-dict} entries exist to provide data for it. On the
% other hand, it's a pretty straightforward arrangement of
% available data in the requested format.
% \begin{tcl}
export {
if {[llength $args] != 2} then {
return -code error "wrong # arguments, should be:\
<variable set> export {element} {attributes}"
}
foreach {var attr} $args break
set res {}
if {[dict exists $extra pseudoexpression $var]} then {
lappend res [dict get $extra pseudoexpression $var]
}
set res [list OMV [dict replace $attr name $var] $res]
if {[dict exists $extra LaTeX_encoding $var]} then {
set res [list OMATTR $attr [list [
list OMATP {} [list\
{OMS {cd altenc name LaTeX_encoding} {}}\
[openmath::OM STR [dict get $extra LaTeX_encoding $var]]]
] $res]]
}
return $res
}
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{import}
% Import is pretty straightforward here; the things that might
% occur at this point are precisely the OpenMath variables. The
% only complication is that they may carry an attribution, but
% that is ignored. Variable |name|s must match exactly.
% \begin{tcl}
import {
if {[llength $args] != 2} then {
return -code error "wrong # arguments, should be:\
<variable set> import {tree} {path}"
}
set tree [lindex $args 0]
while {[lindex $tree 0] eq "OMATTR"} {
set tree [lindex $tree 2 1]
}
if {[lindex $tree 0] eq "OMV"} then {
set var [dict get [lindex $tree 1] name]
if {$var in $elements} then {return $var}
return -code error\
-errorcode [list API import EDOM $path $tree]\
"unknown variable: $var"
}
return -code error\
-errorcode [list API import EDOM $path $tree]\
"Expected OMV, got [lindex $tree 0]"
}
% \end{tcl}
% \end{procmethod}
%
% \begin{procmethod}{API}
% Finally, the supported interfaces must be listed.
% \begin{tcl}
API {
::API::static {equality 1.0 "finite set" 1.1 \
canonise 1.0 onlycanonical 1.0 "named element" 1.0 \
export 2.0 import 1.0} {*}$args
}
% \end{tcl}
% \end{procmethod}
%
% \begin{tcl}
default {
return -code error "Unknown subcommand \"$method\",\
must be: =, API, canonise, elements, export, import,\
or named"
}
}
}
%</varset,pkg>
% \end{tcl}
% \end{proc}
%
%
%
%
% \subsection{Understructure access}
%
% It could be convenient, as a curtesy by adapters and adaptors, to
% provide access to the underlying structure. Algorithms should not
% make use of this, but it can be awfully useful for debugging.
%
% The natural format would be to have a method which accesses the
% underlying structure, but what should it be called? Possibilities
% are:
% \begin{longtable}{lp{0.6\linewidth}}
% base& But that's too close to basis and such.\\
% understructure& Surprisingly enough, an official English word.
% Feels a bit childish, though (perhaps because it mixes Germanic
% and Latin components).\\
% foundation& Certainly posh enough, and seems unclaimed in math.\\
% fundament& Ditto.\\
% stem& To the point, but could perhaps be useful for other things.
% \end{longtable}
% Since it's not to be used in production, |understructure| might
% actually be appropriate; otherwise |fundament| seems best.
%
%
% \begin{APIspec}{subset}{1.0}
% One case of understructure that has applications beyond mere
% debugging is that when one structure is defined as a subset of
% another, e.g.~a matrix group is typically defined as some subset
% of a matrix ring. In this case, every element of the |subset| is
% also an element of the |superset|, but not necessarily vice versa.
%
% \begin{APIdescription}{subset}
% \begin{APImethod}{superset}