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
1001
1002
1003
1004
1005
1006
1007
1008
1009
1010
1011
1012
1013
1014
1015
1016
1017
1018
1019
1020
1021
1022
1023
1024
1025
1026
1027
1028
1029
1030
1031
1032
1033
1034
1035
1036
1037
1038
1039
1040
1041
1042
1043
1044
1045
1046
1047
1048
1049
1050
1051
1052
1053
1054
1055
1056
1057
1058
1059
1060
1061
1062
1063
1064
1065
1066
1067
1068
1069
1070
1071
1072
1073
1074
1075
1076
1077
1078
1079
1080
1081
1082
1083
1084
1085
1086
1087
1088
1089
1090
1091
1092
1093
1094
1095
1096
1097
1098
1099
1100
1101
1102
1103
1104
1105
1106
1107
1108
1109
1110
1111
1112
1113
1114
1115
1116
1117
1118
1119
1120
1121
1122
1123
1124
1125
1126
1127
1128
1129
1130
1131
1132
1133
1134
1135
1136
1137
1138
1139
1140
1141
1142
1143
1144
1145
1146
1147
1148
1149
1150
1151
1152
1153
1154
1155
1156
1157
1158
1159
1160
1161
1162
1163
1164
1165
1166
1167
1168
1169
1170
1171
1172
1173
1174
1175
1176
1177
1178
1179
1180
1181
1182
1183
1184
1185
1186
1187
1188
1189
1190
1191
1192
1193
1194
1195
1196
1197
1198
1199
1200
1201
1202
1203
1204
1205
1206
1207
1208
1209
1210
1211
1212
1213
1214
1215
1216
1217
1218
1219
1220
1221
1222
1223
1224
1225
1226
1227
1228
1229
1230
1231
1232
1233
1234
1235
1236
1237
1238
1239
1240
1241
1242
1243
1244
1245
1246
1247
1248
1249
1250
1251
1252
1253
1254
1255
1256
1257
1258
1259
1260
1261
1262
1263
1264
1265
1266
1267
1268
1269
1270
1271
1272
1273
1274
1275
1276
1277
1278
1279
1280
1281
1282
1283
1284
1285
1286
1287
1288
1289
1290
1291
1292
1293
1294
1295
1296
1297
1298
1299
1300
1301
1302
1303
1304
1305
1306
1307
1308
1309
1310
1311
1312
1313
1314
1315
1316
1317
1318
1319
1320
1321
1322
1323
1324
1325
1326
1327
1328
1329
1330
1331
1332
1333
1334
1335
1336
1337
1338
1339
1340
1341
1342
1343
1344
1345
1346
1347
1348
1349
1350
1351
1352
1353
1354
1355
1356
1357
1358
1359
1360
1361
1362
1363
1364
1365
1366
1367
1368
1369
1370
1371
1372
1373
1374
1375
1376
1377
1378
1379
1380
1381
1382
1383
1384
1385
1386
1387
1388
1389
1390
1391
1392
1393
1394
1395
1396
1397
1398
1399
1400
1401
1402
1403
1404
1405
1406
1407
1408
1409
1410
1411
1412
1413
1414
1415
1416
1417
1418
1419
1420
1421
1422
1423
1424
1425
1426
1427
1428
1429
1430
1431
1432
1433
1434
1435
1436
1437
1438
1439
1440
1441
1442
1443
1444
1445
1446
1447
1448
1449
1450
1451
1452
1453
1454
1455
1456
1457
1458
1459
1460
1461
1462
1463
|
<!DOCTYPE html>
<html xmlns="http://www.w3.org/1999/xhtml" lang="" xml:lang="">
<head>
<meta charset="utf-8" />
<meta name="generator" content="pandoc" />
<meta name="viewport" content="width=device-width, initial-scale=1.0, user-scalable=yes" />
<meta name="author" content="Toshimi Sawada, Kokichi Futatsugi, Norbert Preining" />
<title>CafeOBJ Reference Manual</title>
<style type="text/css">
code{white-space: pre-wrap;}
span.smallcaps{font-variant: small-caps;}
span.underline{text-decoration: underline;}
div.column{display: inline-block; vertical-align: top; width: 50%;}
</style>
</head>
<body>
<header>
<h1 class="title">CafeOBJ Reference Manual</h1>
<p class="author">Toshimi Sawada, Kokichi Futatsugi, Norbert Preining</p>
<p class="date">2018-12-20 (v1.5.9)</p>
</header>
<nav id="TOC">
<ul>
<li><a href="#introduction">Introduction</a><ul>
<li><a href="#background-of-cafeobj">Background of CafeOBJ</a></li>
</ul></li>
<li><a href="#overview-of-the-system">Overview of the system</a><ul>
<li><a href="#sorts">Sorts</a></li>
<li><a href="#intro-imports">Imports</a></li>
<li><a href="#variables-and-operators">Variables and Operators</a></li>
<li><a href="#equations-or-axioms">Equations (or Axioms)</a></li>
</ul></li>
<li><a href="#cloudsync">CloudSync</a><ul>
<li><a href="#protocol">Protocol</a></li>
<li><a href="#specification">Specification</a></li>
<li><a href="#verification">Verification</a></li>
</ul></li>
<li><a href="#gorydetails">Gory Details</a><ul>
<li><a href="#ctrld">Ctrl-D</a></li>
<li><a href="#commandexec"><code>! <command></code></a></li>
<li><a href="#sharp-define"><code>#define <pattern> := <term> .</code></a></li>
<li><a href="#starstar"><code>**</code>, <code>**></code></a></li>
<li><a href="#dashdash"><code>--</code>, <code>--></code></a></li>
<li><a href="#dotsep"><code>.</code></a></li>
<li><a href="#axeq"><code>=</code></a></li>
<li><a href="#searchpredsymb"><code>=(n)=></code>, <code>=(n,m)=></code>, <code>=()=></code></a></li>
<li><a href="#bequality"><code>=*=</code></a></li>
<li><a href="#notequal"><code>=/=</code></a></li>
<li><a href="#equality"><code>==</code></a></li>
<li><a href="#transrel"><code>==></code></a></li>
<li><a href="#help"><code>? [<term>]</code></a></li>
<li><a href="#apropos"><code>?apropos <term> [<term> ...]</code></a></li>
<li><a href="#help-commands"><code>?com [ <term> ]</code></a></li>
<li><a href="#sortsymbol"><code>[</code></a></li>
<li><a href="#switch-accept"><code>accept =*= proof</code> switch</a></li>
<li><a href="#switch-all-axioms"><code>all axioms</code> switch</a></li>
<li><a href="#switch-always-memo"><code>always memo</code> switch</a></li>
<li><a href="#citp-apply"><code>:apply (<tactic> ...) [to <goal-name>]</code></a></li>
<li><a href="#apply"><code>apply <action> [ <subst> ] <range> <selection></code></a></li>
<li><a href="#citp-auto"><code>:auto</code></a></li>
<li><a href="#switch-auto-context"><code>auto context</code> switch</a></li>
<li><a href="#autoload"><code>autoload <module-name> <file-name></code></a></li>
<li><a href="#ax"><code>ax [ <label-exp> ] <term> = <term></code> .</a></li>
<li><a href="#axioms"><code>axioms { <decls> }</code></a></li>
<li><a href="#citp-backward"><code>:backward equation|rule</code></a></li>
<li><a href="#bax"><code>bax [ <label-exp> ] <term> = <term></code> .</a></li>
<li><a href="#bceq"><code>bceq [ <label-exp> ] <term> = <term> if <boolterm> .</code></a></li>
<li><a href="#bcrule"><code>bcrule [ <label-exp> ] <term> => <term> if <term> .</code></a></li>
<li><a href="#bctrans"><code>bctrans [ <label-exp> ] <term> => <term> if <bool> .</code></a></li>
<li><a href="#beq"><code>beq [ <label-exp> ] <term> = <term> .</code></a></li>
<li><a href="#bgoal"><code>bgoal <term> .</code></a></li>
<li><a href="#bgrind"><code>bgrind [in <module-name> :] <boolean-term> .</code></a></li>
<li><a href="#citp-bgrind"><code>:bgrind [in <goal-name> :] <boolean-term> .</code></a></li>
<li><a href="#bguess"><code>{bguess | :bguess} {imply|and|or} [ with <predicate name> ]</code></a></li>
<li><a href="#binspect"><code>binspect [in <module-name> :] <boolean-term> .</code></a></li>
<li><a href="#citp-binspect"><code>:binspect [in <goal-name> :] <boolean-term> .</code></a></li>
<li><a href="#bop"><code>bop <op-spec> : <sorts> -> <sort></code></a></li>
<li><a href="#bpred"><code>bpred <op-spec> : <sorts></code></a></li>
<li><a href="#breduce"><code>breduce [ in <mod-exp> : ] <term> .</code></a></li>
<li><a href="#bresolve"><code>{bresolve | :bresolve} [<limit>] [all]</code></a></li>
<li><a href="#brule"><code>brule [ <label-exp> ] <term> => <term> .</code></a></li>
<li><a href="#bshow"><code>{bshow | :bshow} [{ tree | grind }]</code></a></li>
<li><a href="#bsort"><code>bsort token-predicate creater printer term-predicate</code></a></li>
<li><a href="#btrans"><code>btrans [ <label-exp> ] <term> => <term> .</code></a></li>
<li><a href="#cbred"><code>cbred [ in <mod-exp> :] <term> .</code></a></li>
<li><a href="#cd"><code>cd <dirname></code></a></li>
<li><a href="#ceq"><code>ceq [ <label-exp> ] <term> = <term> if <boolterm> .</code></a></li>
<li><a href="#check"><code>check <options></code></a></li>
<li><a href="#switch-check"><code>check <something></code> switch</a></li>
<li><a href="#choose"><code>choose <selection></code></a></li>
<li><a href="#citp">CITP</a></li>
<li><a href="#clause"><code>clause <term> .</code></a></li>
<li><a href="#cleanmemo"><code>clean memo</code></a></li>
<li><a href="#switch-clean-memo"><code>clean memo</code> switch</a></li>
<li><a href="#close"><code>close</code></a></li>
<li><a href="#comshelp"><code>commands</code></a></li>
<li><a href="#comments">comments</a></li>
<li><a href="#switch-cond-limit"><code>cond limit</code> switch</a></li>
<li><a href="#cont"><code>cont</code></a></li>
<li><a href="#citp-cp"><code>:cp { "[" <label> "]" | "(" <sentence> . ")" } >< { "[" <label> "]" | "(" <sentence> .")" }</code></a></li>
<li><a href="#crule"><code>crule [ <label-exp> ] <term> => <term> if <term> .</code></a></li>
<li><a href="#citp-csp"><code>:csp { eq [ <label-exp>] <term> = <term> . ...}</code></a></li>
<li><a href="#citp-csp-"><code>:csp- { eq [ <label-exp>] <term> = <term> . ...}</code></a></li>
<li><a href="#citp-ctf"><code>:ctf { eq [ <label-exp> ] <term> = <term> .}</code></a></li>
<li><a href="#citp-ctf-"><code>:ctf- { eq [ <label-exp> ] <term> = <term> .}</code></a></li>
<li><a href="#ctrans"><code>ctrans [ <label-exp> ] <term> => <term> if <term> .</code></a></li>
<li><a href="#db"><code>db reset</code></a></li>
<li><a href="#citp-def"><code>:def <symbol> = { <ctf> | <csp> | <init> }</code></a></li>
<li><a href="#demod"><code>demod</code></a></li>
<li><a href="#citp-describe"><code>:describe proof</code></a></li>
<li><a href="#describe"><code>describe <something></code></a></li>
<li><a href="#dirs"><code>dirs</code></a></li>
<li><a href="#dribble"><code>dribble { <file-name> | .}</code></a></li>
<li><a href="#citp-embed"><code>:embed (<label> ... <label>) as <module_name></code></a></li>
<li><a href="#eof"><code>eof</code></a></li>
<li><a href="#eq"><code>eq [ <label-exp> ] <term> = <term> .</code></a></li>
<li><a href="#citp-equation"><code>:equation</code></a></li>
<li><a href="#escape"><code>esc return</code></a></li>
<li><a href="#switch-exec-limit"><code>exec limit</code> switch</a></li>
<li><a href="#switch-exec-trace"><code>exec trace</code> switch</a></li>
<li><a href="#execute-dash"><code>exec! [ in <mod-exp> : ] <term> .</code></a></li>
<li><a href="#execute"><code>execute [ in <mod-exp> : ] <term> .</code></a></li>
<li><a href="#extending"><code>extending ( <modexp> )</code></a></li>
<li><a href="#find"><code>find {+rule | -rule}</code></a></li>
<li><a href="#switch-find-all-rules"><code>find all rules</code> switch</a></li>
<li><a href="#flag"><code>flag(<name>, { on | off })</code></a></li>
<li><a href="#fullreset"><code>full reset</code></a></li>
<li><a href="#gendoc"><code>gendoc <pathname></code></a></li>
<li><a href="#citp-goal"><code>:goal { <sentence> . ... }</code></a></li>
<li><a href="#goal"><code>goal <term> .</code></a></li>
<li><a href="#citp-imply"><code>:imp "[" <label> "]" by "{" <variable> <- <term>; ..."}"</code></a></li>
<li><a href="#imports"><code>imports { <import-decl> }</code></a></li>
<li><a href="#switch-include-bool"><code>include BOOL</code> switch</a></li>
<li><a href="#switch-include-rwl"><code>include RWL</code> switch</a></li>
<li><a href="#including"><code>including ( <modexp> )</code></a></li>
<li><a href="#citp-ind"><code>:ind { on (<variable> ...) | '{' on (<variable> ...) base (<Term> . ... <Term> .) step (<Term> . ... <Term> .) '}'</code></a></li>
<li><a href="#init"><code>init [as <name>] { "[" <label> "]" | "(" <sentence> "")} by "{" <variable> <- <term>; ... "}"</code></a></li>
<li><a href="#citp-init"><code>:init [as <name>] { "[" <label> "]" | "(" <sentence> "")} by "{" <variable> <- <term>; ... "}"</code></a></li>
<li><a href="#input"><code>input <pathname></code></a></li>
<li><a href="#inspect"><code>inspect <term></code></a></li>
<li><a href="#instantiation">instantiation of parameterized modules</a></li>
<li><a href="#citp-is"><code>:is</code></a></li>
<li><a href="#let"><code>let <identifier> = <term> .</code></a></li>
<li><a href="#lex"><code>lex (<op>, ..., <op>)</code></a></li>
<li><a href="#switch-libpath"><code>libpath</code> switch</a></li>
<li><a href="#lisp"><code>lisp</code></a></li>
<li><a href="#lispq"><code>lispq</code></a></li>
<li><a href="#list"><code>list { axiom | sos | usable | flag | param | option | demod }</code></a></li>
<li><a href="#lookup"><code>look up <something></code></a></li>
<li><a href="#ls"><code>ls <pathname></code></a></li>
<li><a href="#make"><code>make <mod_name> ( <mod_exp> )</code></a></li>
<li><a href="#match"><code>match <term_spec> to <pattern> .</code></a></li>
<li><a href="#switch-memo"><code>memo</code> switch</a></li>
<li><a href="#module"><code>[sys:]module[!|*] <modname> [ ( <params> ) ] [ <principal_sort_spec> ] { mod_elements ... }</code></a></li>
<li><a href="#moduleexpression"><code>module expression</code></a></li>
<li><a href="#names"><code>names <mod-exp></code> .</a></li>
<li><a href="#no-autoload"><code>no autoload <module-name></code></a></li>
<li><a href="#citp-normalize"><code>:normalize { on | off}</code></a></li>
<li><a href="#onthefly">on-the-fly declarations</a></li>
<li><a href="#op"><code>op <op-spec> : <sorts> -> <sort> { <attribute-list> }</code></a></li>
<li><a href="#open"><code>open <mod_exp> .</code></a></li>
<li><a href="#opattr"><code>operator attributes</code></a></li>
<li><a href="#opprec"><code>operator precedence</code></a></li>
<li><a href="#option"><code>option { reset | = <name> }</code></a></li>
<li><a href="#citp-order"><code>:order (<op>, ..., <op>)</code></a></li>
<li><a href="#param"><code>param(<name>, <value>)</code></a></li>
<li><a href="#parameterizedmodule"><code>parameterized module</code></a></li>
<li><a href="#parse"><code>parse [ in <mod-exp> : ] <term> .</code></a></li>
<li><a href="#switch-parse-normalize"><code>parse normalize</code> switch</a></li>
<li><a href="#popd"><code>popd</code></a></li>
<li><a href="#pred"><code>pred <op-spec> : <sorts></code></a></li>
<li><a href="#prelude"><code>prelude <file></code></a></li>
<li><a href="#switch-print-depth"><code>print depth</code> switch</a></li>
<li><a href="#switch-print-mode"><code>print mode</code> switch</a></li>
<li><a href="#switch-print-trs"><code>print trs</code> switch</a></li>
<li><a href="#protect"><code>protect <module-name></code></a></li>
<li><a href="#protecting"><code>protecting ( <modexp> )</code></a></li>
<li><a href="#provide"><code>provide <feature></code></a></li>
<li><a href="#pushd"><code>pushd <directory></code></a></li>
<li><a href="#pvar"><code>pvar <var-name> : <sort-name></code></a></li>
<li><a href="#pwd"><code>pwd</code></a></li>
<li><a href="#qualifiedother">qualified sort/operator/parameter</a></li>
<li><a href="#qualified"><code>qualified term</code></a></li>
<li><a href="#switch-quiet"><code>quiet</code> switch</a></li>
<li><a href="#quit"><code>quit</code></a></li>
<li><a href="#citp-red"><code>{ :red | :exec | :bred } [in <goal-name> :] <term> .</code></a></li>
<li><a href="#reduce"><code>reduce [ in <mod-exp> : ] <term> .</code></a></li>
<li><a href="#switch-reduce-conditions"><code>reduce conditions</code> switch</a></li>
<li><a href="#regularize"><code>regularize <mod-name></code></a></li>
<li><a href="#switch-regularize-signature"><code>regularize signature</code> switch</a></li>
<li><a href="#require"><code>require <feature> [ <pathname> ]</code></a></li>
<li><a href="#citp-reset"><code>:reset</code></a></li>
<li><a href="#reset"><code>reset</code></a></li>
<li><a href="#resolve"><code>resolve {. | <file-path> }</code></a></li>
<li><a href="#restore"><code>restore <pathname></code></a></li>
<li><a href="#switch-rewrite"><code>rewrite limit</code> switch</a></li>
<li><a href="#citp-roll"><code>:roll back</code></a></li>
<li><a href="#citp-rule"><code>:rule</code></a></li>
<li><a href="#rule"><code>rule [ <label-exp> ] <term> => <term> .</code></a></li>
<li><a href="#save"><code>save <pathname></code></a></li>
<li><a href="#save-option"><code>save-option <name></code></a></li>
<li><a href="#scase"><code>scase (<term>) in (<mod-exp>) as <name> { <decl> ..} : <term> .</code></a></li>
<li><a href="#searchpredicate"><code>search predicates</code></a></li>
<li><a href="#citp-select"><code>:select <goal-name></code></a></li>
<li><a href="#select"><code>select <mod_exp> .</code></a></li>
<li><a href="#citp-set"><code>:set(<name>, { on | off | show })</code></a></li>
<li><a href="#set"><code>set <name> [option] <value></code></a></li>
<li><a href="#citp-show"><code>:show goal|unproved|proof|discharged</code></a></li>
<li><a href="#show"><code>show <something></code></a></li>
<li><a href="#switch-show-mode"><code>show mode</code> switch</a></li>
<li><a href="#sigmatch"><code>sigmatch (<mod-exp>) to (<mod-exp>)</code></a></li>
<li><a href="#signature"><code>signature { <sig-decl> }</code></a></li>
<li><a href="#sort">sort declaration</a></li>
<li><a href="#sos"><code>sos { = | + | - } { <clause> , ... }</code></a></li>
<li><a href="#citp-spoiler"><code>:spoiler { on | off}</code></a></li>
<li><a href="#start"><code>start <term> .</code></a></li>
<li><a href="#switch-statistics"><code>statistics</code> switch</a></li>
<li><a href="#switch-step"><code>step</code> switch</a></li>
<li><a href="#stop"><code>stop</code></a></li>
<li><a href="#switch-stop-pattern"><code>stop pattern</code> switch</a></li>
<li><a href="#switches">switches</a></li>
<li><a href="#citp-theory"><code>:theory <op_name> : <arity> -> <coarity> { assoc | comm | id: <term> }</code></a></li>
<li><a href="#switch-trace"><code>trace [whole]</code> switch</a></li>
<li><a href="#trans"><code>trans [ <label-exp> ] <term> => <term> .</code></a></li>
<li><a href="#unprotect"><code>unprotect <module-name></code></a></li>
<li><a href="#citp-use"><code>:use (<label> ... <label>)</code></a></li>
<li><a href="#using"><code>using ( <modexp> )</code></a></li>
<li><a href="#var"><code>var <var-name> : <sort-name></code></a></li>
<li><a href="#citp-verbose"><code>:verbose { on | off }</code></a></li>
<li><a href="#switch-verbose"><code>verbose</code> switch</a></li>
<li><a href="#version"><code>version</code></a></li>
<li><a href="#view"><code>view <name> from <modname> to <modname> { <viewelems> }</code></a></li>
</ul></li>
</ul>
</nav>
<!--
% \include{macros.gpp}
% \include{introduction.md}
% \include{overview.md}
% \include{cloudsync.md}
% \include{reference.md}
-->
<h1 id="introduction">Introduction</h1>
<p>This manual introduces the language CafeOBJ. Is is a reference manual with the aim to document the current status of the language, and not targeting at an exhaustive presentation of the mathematical and logical background. Still, the next section will give a short summary of the underlying formal approach and carry references for those in search for details.</p>
<p>The manual is structured into three parts. The first one being this introduction, the second one being the presentation of basic concepts of CafeOBJ by providing a simple protocol which will get specified and verified. Although the second part tries to give a view onto the core features and their usage, it should not be considered a course in CafeOBJ, and cannot replace a proper introduction to the language. The CafeOBJ distribution also includes a <em>user manual</em>. This user manual is slightly outdated with respect to the current status of the language, but is targeting those without and prior knowledge of CafeOBJ.</p>
<p>Finally, the last part consists of explanations of all current language elements in alphabetic order. This includes several higher level concepts, as well as heavy cross-referencing.</p>
<p>While we hope that this manual and the introductory part helps beginners to start programming in CafeOBJ, the main target are those who already have acquired a certain level of fluency, but are in need for a reference of the language.</p>
<h2 id="background-of-cafeobj">Background of CafeOBJ</h2>
<p>CafeOBJ is an algebraic specification and verification language. Although it can be employed for all kind of programming (since it is Turing complete), the main target are algebraic specification of software systems. This includes programs, protocols, and all kind of interaction specifications. In addition to being a specification language, it is also a <em>verification</em> language, that is, a specification given in CafeOBJ can be verified within the same language environment.</p>
<p><em>Specification</em> here means that we are trying to describe the inner workings of a software system in a mathematical way, while <em>verification</em> means that we give a mathematical proof of certain properties. A specification is a text, usually of formal syntax. It denotes an algebraic system constructed out of sorts (or data types) and sorted (or typed) operators. The system is characterize by the axioms in the specification. An axiom was traditionally a plain equation (``essentially algebraic’’), but is now construed much more broadly. For example, CafeOBJ accommodates conditional equations, directed transitions, and (limited) use of disequality.</p>
<p>CafeOBJ is based on three extensions to the basic many-sorted equational logic:</p>
<dl>
<dt>Order-sorted logic</dt>
<dd>In addition to having different sorts (similar to types in other programming languages), these sorts can be ordered, or in other words, one sort can be a subset of another sort: Take for example the number stack: CafeOBJ allows for the provision of natural numbers, which are part of the rational numbers, which are part of the real numbers. This concept allows for operator inheritance and overloading. Behavioral logic
</dd>
<dd>Algebraic modeling is often based on constructors, i.e., all terms under discussion are built up from given operations, and equality can be decided via an equational theory. While being very successful, it is often necessary to model infinite objects (like data streams), which cannot be achieved in this way. CafeOBJ includes <em>behavioral logic</em> and the respective <em>hidden sorts</em> as methodology to model infinite objects which identity is defined via behavior instead of the equational theory. Rewriting logic
</dd>
<dd>Aim of a algebraic specification and verification is to give a formal proof of correctness. CafeOBJ contains order-sorted term rewriting as operational semantics, which allows for <em>execution of proof scores</em>, CafeOBJ code which forms a proof of the required properties.
</dd>
</dl>
<p>There is a wide range of literature on all of these subjects for the interested reader in search for theoretical background. We refer the reader to as a starting point.</p>
<h1 id="overview-of-the-system">Overview of the system</h1>
<p>Let us start with a simple definition of a module, which are the basic building blocks of any CafeOBJ program:</p>
<pre><code>mod NATPAIR {
pr(NAT)
[Pair]
var P : Pair
op <_,_> : Nat Nat -> Pair {constr}
op fst : Pair -> Nat
op snd : Pair -> Nat
eq fst( < A:Nat , B:Nat > ) = A .
eq snd( < A:Nat , B:Nat > ) = B .
}</code></pre>
<p>This example already presents most of the core concepts of CafeOBJ:</p>
<ul>
<li>modules as the basic building blocks</li>
<li>import of other modules <code>pr(NAT)</code></li>
<li>sorts <code>[Pair]</code></li>
<li>operator signature and equations</li>
</ul>
<p>Let us start with sorts, as they are the fundamental types.</p>
<h2 id="sorts">Sorts</h2>
<p>Most programming languages allow for different sorts, or types of objects. In this respect CafeOBJ is not different and allows to have arbitrary sorts. In addition, these sorts can be ordered, more specific one sort can be declared a sub-sort of another. In the above example</p>
<pre><code>[ Pair ]</code></pre>
<p>a new sort called <code>Pair</code> is introduced. This is a completely new sort and is in no sub-sort relation to any other sort. This is a very common case, and reflects the different types of objects in other programming languages.</p>
<p>In case one wants to introduce ordering in the sorts, the order can be expressed together with the definition of the sort, as in:</p>
<pre><code>[ Nat < Set ]</code></pre>
<p>which would introduce a new sort <code>Set</code> and declares it as supersort of the (builtin) sort <code>Nat</code>.</p>
<p>For more details concerning sorts, see <a href="#sort"><code>sort declaration</code></a>.</p>
<h2 id="intro-imports">Imports</h2>
<p>CafeOBJ allows for importing and reusing of already defined modules:</p>
<pre><code>pr(NAT)</code></pre>
<p>for example pulls in the natural numbers (in a very minimal implementation). There are several modes of pulling in other modules, differing in the way the (semantic) models of the included module are treated.</p>
<p>After a statement of import, the sorts, variables, and operators of the imported modules can be used.</p>
<p>For more details see <a href="#protecting"><code>protecting</code></a>, <a href="#extending"><code>extending</code></a>, <a href="#using"><code>using</code></a>, <a href="#including"><code>including</code></a></p>
<h2 id="variables-and-operators">Variables and Operators</h2>
<p>While sorts define data types, variables hold objects of a specific type, and operators define functionality. For each variable its sort has to be declared, and for each operator the signature, i.e., the sorts of the input data and the sort of the output, has to be given.</p>
<pre><code>var P : Pair
op fst : Pair -> Nat</code></pre>
<p>This example declares a variable <code>P</code> of type pair, and an operator <code>fst</code> which maps the sort <code>Pair</code> to the sort <code>Nat</code>, or in other words, a function that maps pairs of natural numbers to natural numbers.</p>
<p>We have seen already a different way to specify operators, namely</p>
<pre><code>op <_,_> : Nat Nat -> Pair {constr}</code></pre>
<p>which introduces an infix operator. CafeOBJ is very flexible and allows to freely specify the syntax. In an operator declaration as the above, the underscores <code>_</code> represent arguments to the operator. That also means that the number of underscores must match the number of sorts given before the <code>-></code>. After the above declaration CafeOBJ will be able to parse terms like <code>< 3 , 4 ></code> and correctly type them as pair.</p>
<p>For further details, see <a href="#var"><code>var</code></a>, <a href="#op"><code>op</code></a>.</p>
<h2 id="equations-or-axioms">Equations (or Axioms)</h2>
<p>Using sorts, variables, and operators we have specified the terms that we want to speak about. In the following equations, or sometimes called axioms, will equate different terms. Equating here is meant in the algebraic sense, but also in the term-rewriting sense, as equations form the basis of rewrite rules which provide CafeOBJ with the executable semantics:</p>
<pre><code>eq fst( < A:Nat , B:Nat > ) = A .
eq snd( < A:Nat , B:Nat > ) = B .</code></pre>
<p>As soon as an operator like <code>fst</code> has been declared, we can give equations. In this case we define <code>fst</code> of a pair to return the first element.</p>
<p>For further details see <a href="#eq"><code>eq</code></a>.</p>
<hr />
<p>In the following chapter we will include the specification of a protocol with the full code, explaining some concepts on the way.</p>
<h1 id="cloudsync">CloudSync</h1>
<p>In the following we will model a very simple protocol for cloud synchronization of a set of PCs. The full code of the actual specification, as well as parts of the verification proof score will be included and discussed.</p>
<p>Besides giving an example of a specification and verification, we also try to explain several of the most important concepts in CafeOBJ using rather simple examples.</p>
<h2 id="protocol">Protocol</h2>
<p>One cloud computer and arbitrary many PCs have one value each that they want to keep in sync. This value is a natural number, and higher values mean more recent (like SVN revision numbers).</p>
<p>The Cloud can be in two states, <em>idle</em> and <em>busy</em>, while the PCs can be on of the following three states: <em>idle</em>, <em>gotvalue</em>, <em>updated</em>. The Cloud as well as all PCs are initially in the <em>idle</em> state. When a PC connects to the cloud, three things happen:</p>
<ol type="1">
<li>the cloud changes into <em>busy</em> state</li>
<li>the PC reads the value of the cloud and saves it in a temporary location</li>
<li>the PC changes into <em>gotvalue</em> state</li>
</ol>
<p>In the <em>gotvalue</em> state the PC compares his own value against the value it got from the cloud, and updates accordingly (changes either the cloud or the own value to the larger one). After this the PC changes into the <em>updated</em> state.</p>
<p>From the <em>update</em> state both the Cloud and the PC return into the <em>idle</em> state.</p>
<p>TODO include a graphic that shows this TODO</p>
<h2 id="specification">Specification</h2>
<p>We will now go through the full specification with explanations of some of the points surfacing. We are starting with two modules that specify the possible states the cloud and the PCs can be in:</p>
<pre><code>mod! CLLABEL {
[ClLabelLt < ClLabel]
ops idlecl busy : -> ClLabelLt {constr} .
eq (L1:ClLabelLt = L2:ClLabelLt) = (L1 == L2) .
}
mod! PCLABEL {
[PcLabelLt < PcLabel]
ops idlepc gotvalue updated : -> PcLabelLt {constr} .
eq (L1:PcLabelLt = L2:PcLabelLt) = (L1 == L2) .
}</code></pre>
<p>Both modules define two new sorts each, the actual label, and literals for the labels. One can see that we declare the signatures of the literal labels with the <a href="#op"><code>ops</code></a> keyword, which introduces several operators of the same signature at the same time.</p>
<p>The last equation in each models provides a definition of equality by using the <em>behavioral</em> equality <code>==</code>. The predicate <code>==</code> is the equivalence predicate defined via reduction. Thus, the two axioms given above state that two literals for labels are the same if they are syntactically the same, since they cannot be rewritten anymore.</p>
<p>Furthermore, note that we choose different names for the <em>idle</em> state of the PCs and the cloud, to have easy separation.</p>
<p>The next module introduces a parametrized pair module. Parametrizing modules is a very powerful construction, and common in object oriented programming languages. In principle we leave open what are the actual components of the pairs, and only specify the operational behavior on a single pair.</p>
<p>In this and the next example of the multi-set, there are no additional requirements on the sorts that can be used to instantiate a pair (or multi-set). In a more general setting the argument after the double colon <code>::</code> refers to a sort, and an instantiation must be adequate for this sort (details require deeper understanding of homomorphism).</p>
<pre><code>mod! PAIR(X :: TRIV,Y :: TRIV) {
[Pair]
op <_,_> : Elt.X Elt.Y -> Pair {constr}
op fst : Pair -> Elt.X
op snd : Pair -> Elt.Y
eq fst(< A:Elt.X,B:Elt.Y >) = A .
eq snd(< A:Elt.X,B:Elt.Y >) = B .
}</code></pre>
<p>The next module is also parametrized, axiomatizing the concept of multi-set where a certain element can appear multiple times in the multi-set. We want to use this module to present another feature, namely the option to specify additional properties of some operators. In this case we are specifying that the constructor for sets is associative <code>assoc</code>, commutative <code>comm</code>, and has as identity the <code>empty</code> set.</p>
<p>While it is easily possible to add associativity and commutativity as axioms directly, this is not advisable, especially for commutativity. Assume adding the simple equation <code>eq A * B = B * A .</code>. This defines a rewrite rule from left to right. But since <code>A</code> and <code>B</code> are variables the can be instantiated with arbitrary subterms, and one would end up with an infinite rewriting.</p>
<pre><code>mod MULTISET(X :: TRIV) {
[ Elt.X < MultiSet ]
op empty : -> MultiSet {constr} .
-- associative and commutative set constructor with identity empty
op (_ _) : MultiSet MultiSet -> MultiSet { constr assoc comm id: empty }
}</code></pre>
<p>With all this set up we can defined the cloud state as a pair of a natural number, and a state. Here we see how a parametrized module is instantiated. The details of the renaming for the second element are a bit involved, but thinking about renaming of sorts and operators to match the ones given is the best idea.</p>
<p>Having this in mind we see that when we put the <code>CLLABEL</code> into the second part of the pair, we tell the system that it should use the <code>ClLabel</code> sort for the instantiation of the <code>Elt</code> sort, and not the <code>ClLabelLt</code> sort.</p>
<p>Furthermore, after the instantiation we rename the final outcome again. In this case we rename the <code>Pair</code> to <code>ClState</code>, and the operators to their cousins with extension in the name.</p>
<pre><code>mod! CLSTATE {
pr(PAIR(NAT, CLLABEL{sort Elt -> ClLabel})*
{sort Pair -> ClState, op fst -> fst.clstate, op snd -> snd.clstate })
}</code></pre>
<p>The PC state is now very similar, only that we have to have a triple (<code>3TUPLE</code> is a builtin predicate of CafeOBJ), since we need one additional place for the temporary value. In the same way as above we rename the <code>Elt</code> to <code>PcLabel</code> and the outcome back to <code>PcState</code>.</p>
<pre><code>mod! PCSTATE {
pr(3TUPLE(NAT, NAT, PCLABEL{sort Elt -> PcLabel})*{sort 3Tuple -> PcState})
}</code></pre>
<p>As we will have an arbitrary set of PCs, we define the multi-set of all PC states, by instatiating the multi-set from above with the just defined <code>PcState</code> sort, and rename the result to <code>PcStates</code>.</p>
<pre><code>mod! PCSTATES {
pr(MULTISET(PCSTATE{sort Elt -> PcState})*{sort MultiSet -> PcStates})
}</code></pre>
<p>Finally, the state of the whole system is declared as a pair of the cloud state and the pc states.</p>
<pre><code>mod! STATE {
pr(PAIR(CLSTATE{sort Elt -> ClState},
PCSTATES{sort Elt -> PcStates})*{sort Pair -> State})
}</code></pre>
<p>The final part is to specify transitions. We have described the protocol by a state machine, and the following transitions will model the transitions in this machine.</p>
<p>The first transition is the initialization of the synchronization by reading the cloud value, saving it into the local register, and both partners go into busy state.</p>
<p>Note that, since we have declared multi-set as commutative and associative, we can assume that the first element of the multi-set is actually the one we are acting on.</p>
<p>Transitions are different from axioms in the sense that the do not state that two terms are the same, but only that one terms can change into another.</p>
<pre><code>mod! GETVALUE { pr(STATE)
trans[getvalue]:
< < ClVal:Nat , idlecl > ,
( << PcVal:Nat ; OldClVal:Nat ; idlepc >> S:PcStates ) >
=>
< < ClVal , busy > , ( << PcVal ; ClVal ; gotvalue >> S ) > .
}</code></pre>
<p>The next transition is the critical part, the update of the side with the lower value. Here we are using the built-in <code>if ... then ... else ... fi</code> operator.</p>
<pre><code>mod! UPDATE { pr(STATE)
trans[update]:
< < ClVal:Nat , busy > ,
( << PcVal:Nat ; GotClVal:Nat ; gotvalue >> S:PcStates ) >
=>
if PcVal <= GotClVal then
< < ClVal , busy > , ( << GotClVal ; GotClVal ; updated >> S ) >
else
< < PcVal , busy > , ( << PcVal ; PcVal ; updated >> S ) >
fi .
}</code></pre>
<p>The last transition is sending the both sides of the synchronization into the idle states.</p>
<pre><code>mod! GOTOIDLE { pr(STATE)
trans[gotoidle]:
< < ClVal:Nat , busy > ,
( << PcVal:Nat ; OldClVal:Nat ; updated >> S:PcStates ) >
=>
< < ClVal , idlecl > , ( << PcVal ; OldClVal ; idlepc >> S ) > .
}</code></pre>
<p>This completes the complete specification of the protocol, and we are defining a module <code>CLOUD</code> that collects all that.</p>
<pre><code>mod! CLOUD { pr(GETVALUE + UPDATE + GOTOIDLE) }</code></pre>
<h2 id="verification">Verification</h2>
<p>Aim of the verification is to show <em>correctness</em> in the sense that no two PCs are at the same time in the busy state. The idea of the proof is to show using induction on the length of transition sequences from initial states to reachable states, that for all reachable states this property is fulfilled.</p>
<p>More specific, we give a characterization of initial states, and show that for initial states the property holds (base case of the induction). Then we show that for all possible transitions, if the target property holds at the beginning of the transition, it also holds at the end of the transition.</p>
<p>Combining this with a (meta-level) induction proof on the length of transition sequences, we show that the target property holds for all reachable states.</p>
<p>Like with loop invariants in other verification schemes, it turns out that a single target property, the exclusion property mentioned above, does not suffice to hold over transitions, i.e., act as transition invariant. Thus, we have to extended it with additional properties.</p>
<p>The first part of this mini-tutorial on the specification of CloudSync contained the full code, but in the following we will, due to space reasons, only include partial code. The latest version of the CloudSync code can be obtained from .</p>
<p>But let us start with the definition of predicates for the initial states. The first step is to define some elementary functions on states, counting how many PCs are in a certain state:</p>
<pre><code>mod! STATEfuncs {
pr(NAT + STATE)
-- no pc in gotvalue state
pred zero-gotvalue : State .
pred zero-updated : State .
...
}</code></pre>
<p>We are collecting a set of predicates, indicated by their predicate name, and define <code>apply</code> as an operator that checks each single predicate against a state, and forms the conjunct of the results.</p>
<pre><code>mod! APPLYPREDS {
pr(STATE)
[PredName < PredNameSeq]
op (_ _) : PredNameSeq PredNameSeq -> PredNameSeq {assoc} .
op apply : PredNameSeq State -> Bool .
eq apply(P:PredName PS:PredNameSeq, S:State) = apply(P,S) and apply(PS,S) .
}</code></pre>
<p>Characterization of the initial state is easy, as it only requires that all PCs as well as the cloud is in idle state.</p>
<pre><code>mod! INITPREDS {
...
op cl-is-idle-name : -> PredName .
op pcs-are-idle-name : -> PredName .
...
}</code></pre>
<p>In the following we define the predicate specifying initial states:</p>
<pre><code>mod! INITIALSTATE {
pr(INITPREDS)
op init-name : -> PredNameSeq .
eq init-name = cl-is-idle-name pcs-are-idle-name .
pred init : State .
eq init(S:State) = apply(init-name, S) .
}</code></pre>
<p>Let us now turn to the most difficult part, that is finding an invariant. This is not a one-shot technique, but mostly iterative. One starts with a set of predicates, and realizes that the proofs don’t work out properly, due to some missing properties. Thus, we add new predicates and iterate until the induction proof finally succeeds.</p>
<p>In the following case we ended up with five different predicates that combined worked as invariant:</p>
<dl>
<dt><code>cloud-idle-pcs-idle</code></dt>
<dd>If the cloud is in the idle state, then all the pcs are also in the idle state.
</dd>
<dt><code>pc-clval</code></dt>
<dd>If the cloud is in busy state, then the value of the cloud and the value in the temporary storage area of any PCs in the <code>gotvalue</code> or <code>updated</code> states agree.
</dd>
<dt><code>one-active</code></dt>
<dd>At most one PC is out of the idle state.
</dd>
<dt><code>gotvalue-cloud-value</code></dt>
<dd>If a PC is in the <code>gotvalue</code> state, then the value saved in the temporary storage area and the one of the cloud agree.
</dd>
<dt><code>goal</code></dt>
<dd>If a PC is in the <code>updated</code> state, then the value of the PC and the value of the cloud agree.
</dd>
</dl>
<p>See the mentioned web-page for the full code of these modules.</p>
<p>In addition to the necessity to introduce additional predicates to obtain an invariant, it also often turns out that some properties, or lemmas, have to be stated or proven so that the verification can work out. In our case some properties on <code>if_then_else_fi</code> constructs, as well as consequences of rewriting are included in a module <code>NECESSARYFACTS</code>.</p>
<p>The final - and one of the most important parts - is the proof of the two properties:</p>
<ul>
<li>base case: if a state satisfies the initial state predicate, it also satisfies the invariant: <code>red init(S) implies invariant(S) .</code></li>
<li>induction step: if a state satisfies the invariant, and we apply a transition, then the next state also satisfies the invariant: `<code>red inv-condition(S, SS) .</code></li>
</ul>
<p>In both cases we cannot work with a general variable <code>S</code>, as in this case no rewriting can take place, and we will not obtain true. What has to be done is to provide a covering set of state expressions, i.e., a set of terms such that every possible instance of a state is also an instance of one of these terms. In our case this is quite easy to provide and consists of six different state terms, combining the three possibilities for a PC with two options of states for the cloud:</p>
<pre><code> ops s1 s2 s3 s4 t1 t2 t3 t4 : -> State .
eq s1 = < < N , idlecl > , ( << M ; K ; idlepc >> PCS ) > .
eq s2 = < < N , idlecl > , ( << M ; K ; gotvalue >> PCS ) > .
eq s3 = < < N , idlecl > , ( << M ; K ; updated >> PCS ) > .
eq t1 = < < N , busy > , ( << M ; K ; idlepc >> PCS ) > .
eq t2 = < < N , busy > , ( << M ; K ; gotvalue >> PCS ) > .
eq t3 = < < N , busy > , ( << M ; K ; updated >> PCS ) > .</code></pre>
<p>It is easy to see that any arbitrary state term can be obtained as instance of one of these six state terms.</p>
<p>What we then show is that the above properties do hold for each of these terms, and thus for each of the reachable states. In details, we show that:</p>
<pre><code> red init(s1) implies invariant(s1) .
red init(s2) implies invariant(s2) .
red init(s3) implies invariant(s3) .
red init(t1) implies invariant(t1) .
red init(t2) implies invariant(t2) .
red init(t3) implies invariant(t3) .</code></pre>
<p>all of these expressions reduce to <code>true</code>. And furthermore, all of the following expressions, too:</p>
<pre><code> red inv-condition(s1, SS) .
red inv-condition(s2, SS) .
red inv-condition(s3, SS) .
red inv-condition(t1, SS) .
red inv-condition(t2, SS) .
red inv-condition(t3, SS) .</code></pre>
<p>Unfortunately, in the case of <code>t2</code> this didn’t turn out to be directly possible, and a further case distinction was necessary to complete the proof.</p>
<p>This concludes the presentation of the CloudSync protocol. We described the cloud protocol using a <em>state system</em> and transitions. This is just one way of implementation. There are other approaches to specification using purely term-based expressions that do not use transitions, but equational theory only. One of the strength of CafeOBJ is that it does not require any specific approach to modeling, but allows for freedom in choosing methodology.</p>
<h1 id="gorydetails">Gory Details</h1>
<p>This chapter presents all syntactic elements of CafeOBJ as well as several meta-concepts in alphabetic order. Concepts are cross-linked for easy accessibility.</p>
<h2 id="ctrld">Ctrl-D</h2>
<p>Terminates the input and exit from the interpreter.</p>
<h2 id="commandexec"><code>! <command></code></h2>
<p>On Unix only, forks a shell and executes the given <code><command></code>.</p>
<h2 id="sharp-define"><code>#define <pattern> := <term> .</code></h2>
<p>Defines <pattern> to be <term>, that is, when <pattern> appers in term, it is expanded to <term> and then parsed.</p>
<h2 id="starstar"><code>**</code>, <code>**></code></h2>
<p>Starts a comment which extends to the end of the line. With the additional <code>></code> the comment is displayed while evaluated by the interpreter.</p>
<p>Related: <a href="#comments">comments</a>, <a href="#starstar"><code>--</code></a></p>
<h2 id="dashdash"><code>--</code>, <code>--></code></h2>
<p>Starts a comment which extends to the end of the line. With the additional <code>></code> the comment is displayed while evaluated by the interpreter.</p>
<p>Related: <a href="#comments">comments</a>, <a href="#starstar"><code>**</code></a></p>
<h2 id="dotsep"><code>.</code></h2>
<p>Input separator</p>
<h2 id="axeq"><code>=</code></h2>
<p>The syntax element <code>=</code> introduces an axiom of the equational theory, and is different from <code>==</code> which specifies an equality based on rewriting.</p>
<p>Related: <a href="#eq"><code>eq</code></a>, <a href="#equality"><code>==</code></a></p>
<h2 id="searchpredsymb"><code>=(n)=></code>, <code>=(n,m)=></code>, <code>=()=></code></h2>
<p>See <a href="#searchpredicate"><code>search predicates</code></a></p>
<h2 id="bequality"><code>=*=</code></h2>
<p>The predicate for behavioral equivalence, written <code>=*=</code>, is a binary operator defined on each hidden sort.</p>
<h2 id="notequal"><code>=/=</code></h2>
<p>Negation of the predicate <code>==</code>.</p>
<p>Related: <a href="#equality"><code>==</code></a></p>
<h2 id="equality"><code>==</code></h2>
<p>The predicate <code>==</code> is a binary operator defined for each visible sort and is defined in terms of evaluation. That is, for ground terms <code>t</code> and <code>t'</code> of the same sort, <code>t == t'</code> evaluates to <code>true</code> iff terms reduce to a common term. This is different from the equational <code>=</code> which specifies the equality of the theory.</p>
<h2 id="transrel"><code>==></code></h2>
<p>This binary predicate is defined on each visible sort, and defines the transition relation, which is reflexive, transitive, and closed under operator application. It expresses the fact that two states (terms) are connected via transitions.</p>
<p>Related: <a href="#searchpredicate">search predicates</a>, <a href="#trans"><code>trans</code></a></p>
<h2 id="help"><code>? [<term>]</code></h2>
<p>Without any argument, shows the brief guide of online help system. With argument gives the reference manual description of <code>term</code>. In addition to this, many commands allow for passing <code>?</code> as argument to obtain further help.</p>
<p>In case examples are provided for the <code><term></code>, they can be displayed using <code>?ex <term></code>. In this case the normal help output will also contain an informational message that examples are available.</p>
<p>When called as ?? both documentation and examples are shown.</p>
<h2 id="apropos"><code>?apropos <term> [<term> ...]</code></h2>
<p>Searches all available online docs for the terms passed. Terms are separated by white space. Each term is tested independently and all terms have to match. Testing is done either by simple sub-string search, or, if the term looks like a regular expression (Perl style), by regex matching. In case a regex-like term cannot be parsed as regular expression, it is used in normal sub-string search mode.</p>
<p>Note: Fancy quoting with single and double quotes might lead to unexpected problems.</p>
<h3 id="example">Example</h3>
<pre><code>CafeOBJ> ?ap prec oper</code></pre>
<p>will search for all entries that contain both <code>prec</code> and <code>oper</code> as sub-strings. Matching is done as simple sub-string match.</p>
<pre><code>CafeOBJ> ?ap foo att[er]</code></pre>
<p>will search for entries that contain the string <code>foo</code> as well as either the string <code>atte</code> or <code>attr</code>.</p>
<h2 id="help-commands"><code>?com [ <term> ]</code></h2>
<p>List commands or declarations categorized by the key <term>. <term> is one of ‘decl’, ‘module’, ‘parse’, ‘rewrite’, ‘inspect’, ‘switch’, ‘proof’, ‘system’, ‘inspect’, ‘library’, ‘help’, ‘io’ or ‘misc’. If <term> is omitted, the list of available <term> will be printed.</p>
<h2 id="sortsymbol"><code>[</code></h2>
<p>Starts a sort declaration. See <a href="#sort">sort declaration</a> for details.</p>
<h2 id="switch-accept"><code>accept =*= proof</code> switch</h2>
<p>accept system’s automatic proof of congruency of <code>=*=</code></p>
<h2 id="switch-all-axioms"><code>all axioms</code> switch</h2>
<p>Controls whether axioms from included modules are shown during a <code>show</code> invocation.</p>
<p>Related: <a href="#show"><code>show</code></a></p>
<h2 id="switch-always-memo"><code>always memo</code> switch</h2>
<p>Turns on memorization of computation also for operators without the <a href="#opattr"><code>memo</code></a> operator attribute.</p>
<p>Related: <a href="#opattr">operator attributes</a>, <a href="#switch-memo"><code>memo</code></a></p>
<h2 id="citp-apply"><code>:apply (<tactic> ...) [to <goal-name>]</code></h2>
<p>Apply the list of tactics given within parenthesis to either the current goal, or the goal given as <code><goal-name></code>.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="apply"><code>apply <action> [ <subst> ] <range> <selection></code></h2>
<p>Applies one of the following actions <code>reduce</code>, <code>exec</code>, <code>print</code>, or a rewrite rule to the term in focus.</p>
<dl>
<dt><code>reduce</code>, <code>exec</code>, <code>print</code></dt>
<dd>the operation acts on the (sub)term specified by <code><range></code> and <code><selection></code>.
</dd>
<dt>rewrite rule</dt>
<dd><p>in this case a rewrite rule spec has to be given in the following form:</p>
<p><code>[+|-][<mod_name>].<rule-id></code></p>
<p>where <code><mod_name></code> is the name of a module, and <code><rule-id></code> either a number n - in which case the n. equation in the current module is used, or the label of an equation. If the <code><mod_name></code> is not given, the equations of the current module are considered. If the leading <code>+</code> or no leading character is given, the equation is applied left-to-right, which with a leading <code>-</code> the equation is applied right-to-left.</p>
</dd>
</dl>
<p>The <code><subst></code> is of the form</p>
<p><code>with { <var_name> = <term> } +,</code></p>
<p>and is used when applying a rewrite rule. In this case the variables in the rule are bound to the given term.</p>
<p><code><range></code> is either <code>within</code> or <code>at</code>. In the former case the action is applied at or inside the (sub)term specified by the following selection. In the later case it means exactly at the (sub)term.</p>
<p>Finally, the <code><selection></code> is an expression</p>
<p><code><selector> { of <selector> } *</code></p>
<p>where each <code><selector></code> is one of</p>
<dl>
<dt><code>top</code>, <code>term</code></dt>
<dd>Selects the whole term
</dd>
<dt><code>subterm</code></dt>
<dd>Selects the pre-chosen subterm (see <a href="#choose"><code>choose</code></a>)
</dd>
<dt><code>( <number_list> )</code></dt>
<dd>A list of numbers separated by blanks as in <code>(2 1)</code> indicates a subterm by tree search. <code>(2 1)</code> means the first argument of the second argument.
</dd>
<dt><code>[ <number1> .. <number2> ]</code></dt>
<dd><p>This selector can only be used with associative operators. It indicates a subterm in a flattened structure and selects the subterm between and including the two numbers given. <code>[n .. n]</code> can be abbreviated to <code>[n]</code>.</p>
<p>Example: If the term is <code>a * b * c * d * e</code>, then the expression <code>[2 .. 4]</code> selects the subterm <code>b * c * d</code>.</p>
</dd>
<dt><code>{ <number_set> }</code></dt>
<dd>This selector can only be used with associative and commutative operators. It indicates a subterm in a multiset structure obtained from selecting the subterms at position given by the numbers.
</dd>
</dl>
<p>Example: If the operator <code>_*_</code> is declared as associative and commutative, and the current term is <code>b * c * d * c * e</code>, then then the expression <code>{2, 4, 5}</code> selects the subterm <code>c * c * e</code>.</p>
<p>Related: <a href="#start"><code>start</code></a>, <a href="#choose"><code>choose</code></a></p>
<h2 id="citp-auto"><code>:auto</code></h2>
<p>Applies the following set of tactics: <code>(SI CA TC IP RD)</code>.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="switch-auto-context"><code>auto context</code> switch</h2>
<p>Possible values: <code>on</code> or <code>off</code>, default is <code>off</code>.</p>
<p>If this switch is <code>on</code>, the context will automatically switch to the most recent module, i.e., defining a module or inspecting a module’s content will switch the current module.</p>
<h2 id="autoload"><code>autoload <module-name> <file-name></code></h2>
<p>When evaluating a <module-name> and found that it is not yet declared, the system read in <file-name> then retries the evaluation.</p>
<p>Related: <a href="#no-autoload"><code>no autoload</code></a></p>
<h2 id="ax"><code>ax [ <label-exp> ] <term> = <term></code> .</h2>
<p>(pignose)</p>
<h2 id="axioms"><code>axioms { <decls> }</code></h2>
<p>Block enclosing declarations of variables, equations, and transitions. Other statements are not allowed within the <code>axioms</code> block. Optional structuring of the statements in a module.</p>
<p>Related: <a href="#trans"><code>trans</code></a>, <a href="#eq"><code>eq</code></a>, <a href="#var"><code>var</code></a>, <a href="#imports"><code>imports</code></a>, <a href="#signature"><code>signature</code></a></p>
<h2 id="citp-backward"><code>:backward equation|rule</code></h2>
<p>Like <a href="#citp-equation"><code>:equation</code></a> and <a href="#citp-rule"><code>:rule</code></a>, but exchange the left and right side.</p>
<p>Related: <a href="#citp-rule"><code>:rule</code></a>, <a href="#citp-equation"><code>:equation</code></a>, <a href="#citp-cp"><code>:cp</code></a>, <a href="#citp"><code>citp</code></a></p>
<h2 id="bax"><code>bax [ <label-exp> ] <term> = <term></code> .</h2>
<p>(pignose)</p>
<h2 id="bceq"><code>bceq [ <label-exp> ] <term> = <term> if <boolterm> .</code></h2>
<p>Defines a behavioral conditional equation. For details see <a href="#ceq"><code>ceq</code></a>.</p>
<p>Related: <a href="#beq"><code>beq</code></a>, <a href="#ceq"><code>ceq</code></a>, <a href="#eq"><code>eq</code></a></p>
<h2 id="bcrule"><code>bcrule [ <label-exp> ] <term> => <term> if <term> .</code></h2>
<p>Synonym of <a href="#bctrans"><code>bctrans</code></a></p>
<p>Related: <a href="#bctrans"><code>bctrans</code></a></p>
<h2 id="bctrans"><code>bctrans [ <label-exp> ] <term> => <term> if <bool> .</code></h2>
<p>Defines a behavioral conditional transition. For details see <a href="#ctrans"><code>ctrans</code></a>.</p>
<p>Related: <a href="#btrans"><code>btrans</code></a>, <a href="#ctrans"><code>ctrans</code></a>, <a href="#trans"><code>trans</code></a></p>
<h2 id="beq"><code>beq [ <label-exp> ] <term> = <term> .</code></h2>
<p>Defines a behavioral equation. For details see <a href="#eq"><code>eq</code></a>.</p>
<p>Related: <a href="#bceq"><code>bceq</code></a>, <a href="#ceq"><code>ceq</code></a>, <a href="#eq"><code>eq</code></a></p>
<h2 id="bgoal"><code>bgoal <term> .</code></h2>
<p>(pignose)</p>
<h2 id="bgrind"><code>bgrind [in <module-name> :] <boolean-term> .</code></h2>
<p>Print given boolean term in ’grind’ed manner after computes its xor-and normal form.</p>
<h2 id="citp-bgrind"><code>:bgrind [in <goal-name> :] <boolean-term> .</code></h2>
<p>Used diring <a href="#citp">CITP</a> proofs instead of <a href="#bgrind"><code>bgrind</code></a></p>
<h2 id="bguess"><code>{bguess | :bguess} {imply|and|or} [ with <predicate name> ]</code></h2>
<p>Try to find true/false assignments which satisfies the Bool term specified by ‘binspect’ or ‘:binspect’.</p>
<h2 id="binspect"><code>binspect [in <module-name> :] <boolean-term> .</code></h2>
<p>Start an inspection of a Boolean term, that is, and abstracted form of the Boolean term is constructed. The abstracted term is shown (like calling <a href="#bshow"><code>bshow</code></a>.</p>
<h3 id="example-1">Example</h3>
<pre><code>CafeOBJ> module BTE { [S]
preds p1 p2 p3 p4 p5 p6 p7 : S
ops a b c : -> S .
}
CafeOBJ> binspect in BTE : (p1(X:S) or p2(X)) and p3(Y:S) or (p4(Y) and p1(Y)) .
...
--> ((p4(Y:S) and p1(Y)) xor ((p3(Y) and p1(X:S)) xor ((p2(X) and (p3(Y) and p1(X))) xor ((p3(Y) and p2(X)) xor ((p3(Y) and (p2(X) and (p4(Y) and p1(Y)))) xor ((p3(Y) and (p2(X) and (p1(X) and (p1(Y) and p4(Y))))) xor (p1(X) and (p3(Y) and (p1(Y) and p4(Y))))))))))
...</code></pre>
<h2 id="citp-binspect"><code>:binspect [in <goal-name> :] <boolean-term> .</code></h2>
<p>Used during <a href="#citp">CITP</a> proofs instead of <a href="#binspect"><code>binspect</code></a></p>
<h2 id="bop"><code>bop <op-spec> : <sorts> -> <sort></code></h2>
<p>Defines a behavioral operator by its domain, co-domain, and the term construct. <code><sorts></code> is a space separated list of sort names containing <em>exactly</em> one hidden sort. <code><sort></code> is a single sort name.</p>
<p>For <code><op-spec></code> see the explanations of <a href="#op"><code>op</code></a>.</p>
<p>Related: <a href="#op"><code>op</code></a></p>
<h2 id="bpred"><code>bpred <op-spec> : <sorts></code></h2>
<p>Short hand for <code>op <op-spec> : <sorts> -> Bool</code> defining a behavioral predicate.</p>
<p>Related: <a href="#pred"><code>pred</code></a>, <a href="#bop"><code>bop</code></a>, <a href="#op"><code>op</code></a></p>
<h2 id="breduce"><code>breduce [ in <mod-exp> : ] <term> .</code></h2>
<p>Reduce the given term in the given module, if <code><mod-exp></code> is given, otherwise in the current module.</p>
<p>For <code>breduce</code> equations, possibly conditional, possibly behavioral, are taken into account for reduction.</p>
<p>Related: <a href="#reduce"><code>reduce</code></a>, <a href="#execute"><code>execute</code></a></p>
<h2 id="bresolve"><code>{bresolve | :bresolve} [<limit>] [all]</code></h2>
<p>Computes all possible variable assignments that render an abstracted term <code>true</code>. The variant with leading colon is for usage during a <a href="#citp">CITP</a> proof. If an optional argument ‘all’ is specified, all solutions will be searched. Optional <limit> specifies maximal number of variable combination, i.e. if there are 3 variables v1, v2, and v3, and <limit> is 2, the following cases are examined: (1) v1 : true/false (2) v2 : true/false (3) v3 : true/false (4) v1/v2 : combinations of true/false of two variables (5) v1/v3 : combinations of true/false of two variables (6) v2/v3 : combinations of true/false of two variables</p>
<h3 id="example-2">Example</h3>
<pre><code>CafeOBJ> bresolve 2 all
** (1) The following assignment(s) makes the term to be 'true'.
[1] { P-3:Bool |-> true }
where
p-3 = P4(Y:S)
[2] { P-4:Bool |-> true }
where
p-4 = P1(X:S)
** (2) The following assignment(s) makes the term to be 'true'.
[1] { P-1:Bool |-> true, P-2:Bool |-> true }
where
p-1 = P3(Y:S)
p-2 = P2(X:S)
...</code></pre>
<h2 id="brule"><code>brule [ <label-exp> ] <term> => <term> .</code></h2>
<p>Synonym of <a href="#btrans"><code>btrans</code></a>.</p>
<p>Related: <a href="#btrans"><code>btrans</code></a></p>
<h2 id="bshow"><code>{bshow | :bshow} [{ tree | grind }]</code></h2>
<p>Shows the abstracted Boolean term computed by <a href="#binspect"><code>binspect</code></a>. If the argument <code>tree</code> is given, prints out a the abstracted term in tree form. The variant with leading colon is for usage during a <a href="#citp">CITP</a> proof.</p>
<h3 id="example-3">Example</h3>
<pre><code>CafeOBJ> bshow
((P-1:Bool and (P-2:Bool and (P-3:Bool and P-4:Bool))) xor ((P-1 and (P-2 and (P-4 and (P-5:Bool and P-3)))) xor ((P-2 and (P-1 and (P-5 and P-3))) xor ((P-5 and P-3) xor ((P-4 and (P-3 and P-5)) xor ((P-4 and P-3) xor (P-2 and P-1)))))))
where
P-1:Bool |-> p4(Y:S)
P-2:Bool |-> p1(Y:S)
P-3:Bool |-> p3(Y:S)
P-4:Bool |-> p1(X:S)
P-5:Bool |-> p2(X:S)</code></pre>
<h2 id="bsort"><code>bsort token-predicate creater printer term-predicate</code></h2>
<p>Defines a built-in sort. Internal use only.</p>
<h2 id="btrans"><code>btrans [ <label-exp> ] <term> => <term> .</code></h2>
<p>Defines a behavioral transition. For details see <a href="#trans"><code>trans</code></a>.</p>
<p>Related: <a href="#bctrans"><code>bctrans</code></a>, <a href="#ctrans"><code>ctrans</code></a>, <a href="#trans"><code>trans</code></a></p>
<h2 id="cbred"><code>cbred [ in <mod-exp> :] <term> .</code></h2>
<p>circular coinductive reduction: see <em>Goguen, Lin, Rosu: Circular Coinductive Rewriting</em> (Proceedings of Automated Software Engineering 2000) for details.</p>
<h2 id="cd"><code>cd <dirname></code></h2>
<p>Change the current working directory, like the Unix counterpart. The argument is necessary. No kind of expansion or substitution is done.</p>
<p>Related: <a href="#ls"><code>ls</code></a>, <a href="#pwd"><code>pwd</code></a></p>
<h2 id="ceq"><code>ceq [ <label-exp> ] <term> = <term> if <boolterm> .</code></h2>
<p>Defines a conditional equation. Spaces around the <code>if</code> are obligatory. <code><boolterm></code> needs to be a Boolean term. For other requirements see <a href="#eq"><code>eq</code></a>.</p>
<p>Related: <a href="#bceq"><code>bceq</code></a>, <a href="#beq"><code>beq</code></a>, <a href="#eq"><code>eq</code></a></p>
<h2 id="check"><code>check <options></code></h2>
<p>This command allows for checking of certain properties of modules and operators.</p>
<dl>
<dt><code>check regularity <mod_exp></code></dt>
<dd>Checks whether the module given by the module expression <code><mod_exp></code> is regular.
</dd>
<dt><code>check compatibility <mod_exp></code></dt>
<dd>Checks whether term rewriting system of the module given by the module expression <code><mod_exp></code> is compatible, i.e., every application of every rewrite rule to every well-formed term results in a well-formed term. (This is not necessarily the case in order-sorted rewriting!)
</dd>
<dt><code>check laziness <op_name></code></dt>
<dd>Checks whether the given operator can be evaluated lazily. If not <code><op_name></code> is given, all operators of the current module are checked.
</dd>
</dl>
<p>Related: <a href="#regularize"><code>regularize</code></a></p>
<h2 id="switch-check"><code>check <something></code> switch</h2>
<p>These switches turn on automatic checking of certain properties:</p>
<dl>
<dt><code>check coherency</code></dt>
<dd>check whether transitions and equations are coherent
</dd>
<dt><code>check compatibility</code></dt>
<dd>see the <a href="#check"><code>check</code></a> command
</dd>
<dt><code>check import</code></dt>
<dd>check conflicting importing mode of submodules
</dd>
<dt><code>check regularity</code></dt>
<dd>see the <a href="#check"><code>check</code></a> command
</dd>
<dt><code>check sensible</code></dt>
<dd>check whether a signature is sensible
</dd>
</dl>
<h2 id="choose"><code>choose <selection></code></h2>
<p>Chooses a subterm by the given <code><selection></code>. See <a href="#apply"><code>apply</code></a> for details on <code><selection></code>.</p>
<p>Related: <a href="#opattr"><code>strat</code> in operator attributes</a>, <a href="#start"><code>start</code></a>, <a href="#apply"><code>apply</code></a></p>
<h2 id="citp">CITP</h2>
<p>Constructor Based Induction Theorem Prover</p>
<p>The sub-system provides a certain level of automatization for theorem proving.</p>
<p>Please see the accompanying manual for CITP for details.</p>
<p>Related: <a href="#target_not_found"><code>:attr</code></a>, <a href="#citp-reset"><code>:reset</code></a>, <a href="#citp-embed"><code>:embed</code></a>, <a href="#citp-use"><code>:use</code></a>, <a href="#citp-order"><code>:ord</code></a>, <a href="#citp-imply"><code>:imp</code></a>, <a href="#citp-def"><code>:def</code></a>, <a href="#citp-ctf-"><code>:ctf-</code></a>, <a href="#citp-ctf"><code>:ctf</code></a>, <a href="#citp-csp-"><code>:csp-</code></a>, <a href="#citp-csp"><code>:csp</code></a>, <a href="#citp-red"><code>:red</code></a>, <a href="#citp-select"><code>:select</code></a>, <a href="#citp-backward"><code>:backward</code></a>, <a href="#citp-rule"><code>:rule</code></a>, <a href="#citp-equation"><code>:equation</code></a>, <a href="#citp-cp"><code>:cp</code></a>, <a href="#citp-init"><code>:init</code></a>, <a href="#citp-roll"><code>:roll</code></a>, <a href="#citp-auto"><code>:auto</code></a>, <a href="#citp-ind"><code>:ind</code></a>, <a href="#citp-apply"><code>:apply</code></a>, <a href="#citp-goal"><code>:goal</code></a></p>
<h2 id="clause"><code>clause <term> .</code></h2>
<p>(pignose)</p>
<h2 id="cleanmemo"><code>clean memo</code></h2>
<p>Resets (clears) the memo storage of the system. Memorized computations are forgotten.</p>
<p>Related: <a href="#switch-clean-memo">clean memo switch</a></p>
<h2 id="switch-clean-memo"><code>clean memo</code> switch</h2>
<p>Possible values: <code>on</code>, <code>off</code>, default <code>off</code>.</p>
<p>tells the system to be forgetful.</p>
<h2 id="close"><code>close</code></h2>
<p>This command closes a modification of a module started by <a href="#open"><code>open</code></a>.</p>
<p>Related: <a href="#open"><code>open</code></a></p>
<h2 id="comshelp"><code>commands</code></h2>
<p>Print outs the list of main toplevel commands.</p>
<h2 id="comments">comments</h2>
<p>The interpreter accepts the following strings as start of a comment that extends to the end of the line: <code>--</code>, <code>--></code>, <code>**</code>, <code>**></code>.</p>
<p>The difference in the variants with <code>></code> is that the comment is displayed when run through the interpreter.</p>
<p>Related: <a href="#starstar"><code>--</code></a>, <a href="#starstar"><code>**</code></a></p>
<h2 id="switch-cond-limit"><code>cond limit</code> switch</h2>
<p>Setting maximal number of evaluation of condition part of an axiom. This is useful for detecting a kind of inifinite loop of rewriting.</p>
<h2 id="cont"><code>cont</code></h2>
<p>In <a href="#switch-step">step mode</a>, continues the reduction until a <a href="#switch-stop-pattern">stop pattern</a> has been found.</p>
<h2 id="citp-cp"><code>:cp { "[" <label> "]" | "(" <sentence> . ")" } >< { "[" <label> "]" | "(" <sentence> .")" }</code></h2>
<p>Computes the critical pair of the two given equations. Here either a label or a full equation can be used to specify the equations.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h3 id="example-4">Example</h3>
<pre><code>:cp (ceq top(sq(S@Sys)) = I@Pid if pc(S@Sys,I@Pid) = cs .)
><
(ceq top(sq(S@Sys)) = J@Pid if pc(S@Sys,J@Pid) = cs .)</code></pre>
<h2 id="crule"><code>crule [ <label-exp> ] <term> => <term> if <term> .</code></h2>
<p>Synonym of <a href="#ctrans"><code>ctrans</code></a></p>
<p>Related: <a href="#rule"><code>rule</code></a>, <a href="#ctrans"><code>ctrans</code></a></p>
<h2 id="citp-csp"><code>:csp { eq [ <label-exp>] <term> = <term> . ...}</code></h2>
<p>Applies case splitting after a set of equations. Each of these equations creates one new sub-goal with the equation added.</p>
<p>The system does not check whether given set of equations exhausts all possible values.</p>
<p>Not discharged sub-goals will remain in the reduced form.</p>
<p>Related: <a href="#citp-csp-"><code>:csp-</code></a>, <a href="#citp"><code>citp</code></a></p>
<h2 id="citp-csp-"><code>:csp- { eq [ <label-exp>] <term> = <term> . ...}</code></h2>
<p>Like <a href="#citp-csp"><code>:csp</code></a>, but if sub-goals are not discharged, the CITP prover returns to the original state before the reduce action.</p>
<p>Related: <a href="#citp-csp"><code>:csp</code></a>, <a href="#citp"><code>citp</code></a></p>
<h2 id="citp-ctf"><code>:ctf { eq [ <label-exp> ] <term> = <term> .}</code></h2>
<p>Applies case splitting after a set of boolean expressions. Not discharged sub-goals will remain in the reduced form.</p>
<p>Related: <a href="#citp-ctf-"><code>:ctf-</code></a>, <a href="#citp"><code>citp</code></a></p>
<h2 id="citp-ctf-"><code>:ctf- { eq [ <label-exp> ] <term> = <term> .}</code></h2>
<p>Like <a href="#citp-ctf"><code>:ctf</code></a>, but if sub-goals are not discharged, the CITP prover returns to the original state before the reduce action.</p>
<p>Related: <a href="#citp-ctf"><code>:ctf</code></a>, <a href="#citp"><code>citp</code></a></p>
<h2 id="ctrans"><code>ctrans [ <label-exp> ] <term> => <term> if <term> .</code></h2>
<p>Defines a conditional transition. For details see <a href="#trans"><code>trans</code></a> and <a href="#ceq"><code>ceq</code></a>.</p>
<p>Related: <a href="#bctrans"><code>bctrans</code></a>, <a href="#btrans"><code>btrans</code></a>, <a href="#trans"><code>trans</code></a></p>
<h2 id="db"><code>db reset</code></h2>
<p>(pignose)</p>
<h2 id="citp-def"><code>:def <symbol> = { <ctf> | <csp> | <init> }</code></h2>
<p>Assigns a name to a specific case splitting (<code>:ctf</code> or <code>:csp</code>) or induction <code>:ind</code>), so that it can be used as tactics in <code>:apply</code>.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h3 id="example-5">Example</h3>
<pre><code>:def name-0 = :ind { :on (<Variable>...) :base <Term> . :step <Term> . }
:def name-1 = :ctf [ <Term> . ]
:def name-2 = :ctf-{ eq LHS = RHS . }
:def name-3 = :csp { eq lhs1 = rhs1 . eq lhs2 = rhs2 . }
:def name-4 = :csp-{ eq lhs3 = rhs3 . eq lhs4 = rhs4 . }
:apply(name-0 TC name-1 name-2 name-3 name-4)</code></pre>
<h2 id="demod"><code>demod</code></h2>
<p>(pignose)</p>
<h2 id="citp-describe"><code>:describe proof</code></h2>
<p>Describes the current proof in more detail.</p>
<p>Related: <a href="#citp-show"><code>:show</code></a>, <a href="#citp"><code>citp</code></a></p>
<h3 id="example-6">Example</h3>
<pre><code>PNAT> :describe proof
==> root*
-- context module: #Goal-root
-- targeted sentences:
eq [lemma-1]: M:PNat + 0 = M .
eq [lemma-2]: M:PNat + s N:PNat = s (M + N) .
[si] 1*
-- context module: #Goal-1
-- targeted sentences:
eq [lemma-1]: 0 + 0 = 0 .
eq [lemma-2]: 0 + s N:PNat = s (0 + N) .
...</code></pre>
<h2 id="describe"><code>describe <something></code></h2>
<p>Similar to the <code>show</code> command but with more details. Call <code>describe ?</code> for the possible set of invocations.</p>
<p>Related: <a href="#show"><code>show</code></a></p>
<h2 id="dirs"><code>dirs</code></h2>
<p>Displays the current push stack.</p>
<p>Related: <a href="#popd"><code>popd</code></a>, <a href="#pwd"><code>pwd</code></a>, <a href="#pushd"><code>pushd</code></a>, <a href="#cd"><code>cd</code></a>, <a href="#ls"><code>ls</code></a></p>
<h2 id="dribble"><code>dribble { <file-name> | .}</code></h2>
<p>If <file-name> is give, the evaluation process of the system is output to the <file-name> in internal form. ‘.’ stops the recording. Only usefule for developer of the system.</p>
<h2 id="citp-embed"><code>:embed (<label> ... <label>) as <module_name></code></h2>
<p>Incorporate proved goals into the module specified by <module_name> which will import the current proof context module.</p>
<h2 id="eof"><code>eof</code></h2>
<p>Terminates reading of the current file. Allows for keeping untested code or documentations below the <code>eof</code> mark. Has to be on a line by itself without leading spaces.</p>
<h2 id="eq"><code>eq [ <label-exp> ] <term> = <term> .</code></h2>
<p>Declares an axiom, or equation.</p>
<p>Spaces around the <code>=</code> are necessary to separate the left from the right hand side. The terms given must belong to the same connected component in the graph defined by the sort ordering.</p>
<p>In simple words, the objects determined by the terms must be interpretable as of the same sort.</p>
<p>The optional part <code><label-exp></code> serves two purposes, one is to give an axiom an identifier, and one is to modify its behavior. The <code><label-exp></code> is of the form:</p>
<p><code>[ <modifier> <label> ] :</code></p>
<p>Warning: The square brackets here are <em>not</em> specifying optional components, but syntactical elements. Thus, a labeled axiom can look like:</p>
<p><code>eq[foobar] : foo = bar .</code></p>
<p>The <code><modifier></code> part is used to change the rewriting behavior of the axiom. There are at the moment two possible modifiers, namely <code>:m-and (:m-and-also)</code> and <code>:m-or (:m-or-else)</code>. Both make sense only for operators where the arguments come from an associative sort. In this case both modifiers create all possible permutations of the arguments and rewrite the original term to the conjunction in case of <code>:m-and</code> or to the disjunction in case of <code>:m-or</code> of all the generated terms.</p>
<p>Assume that <code>NatSet</code> is a sort with associative constructor modeling a set of natural number, and let</p>
<pre><code> pred p1: Nat .
ops q1 q2 : NatSet -> Bool .
eq [:m-and]: q1(N1:Nat NS:NatSet) = p1(N1) .
eq [:m-or]: q2(N1:Nat NS:NatSet) = p1(N1) .</code></pre>
<p>In this case an expression like <code>q1(1 2 3)</code> would reduce to <code>p1(1) and p1(2) and p1(3)</code> (modulo AC), and <code>q2(1 2 3)</code> into the same term with <code>or</code> instead.</p>
<p>Related: <a href="#bceq"><code>bceq</code></a>, <a href="#beq"><code>beq</code></a>, <a href="#ceq"><code>ceq</code></a></p>
<h2 id="citp-equation"><code>:equation</code></h2>
<p>Adds the critical pair computed by the last <a href="#citp-cp"><code>:cp</code></a> command as equation to the current goal.</p>
<p>Related: <a href="#citp-rule"><code>:rule</code></a>, <a href="#citp-cp"><code>:cp</code></a>, <a href="#citp"><code>citp</code></a></p>
<h2 id="escape"><code>esc return</code></h2>
<p>In case that, after hitting <code>return</code> expecting some feed-back, no such feed-back whatsoever is returned, typing the <code>escape</code> key followed by the <code>return</code> key will make the interpreter discard the preceding input and make a fresh start.</p>
<h2 id="switch-exec-limit"><code>exec limit</code> switch</h2>
<p>Possible values: integers, default limit 4611686018427387903.</p>
<p>Controls the number of maximal transition steps.</p>
<p>Related: <a href="#reduce"><code>reduce</code></a></p>
<h2 id="switch-exec-trace"><code>exec trace</code> switch</h2>
<p>Possible values: <code>on</code> <code>off, default</code>off`.</p>
<p>controls whether further output is provided during reductions.</p>
<p>Related: <a href="#reduce"><code>reduce</code></a></p>
<h2 id="execute-dash"><code>exec! [ in <mod-exp> : ] <term> .</code></h2>
<p>Obsolete command. Implicitly invokes RWL search predicate in a specific manner.</p>
<h2 id="execute"><code>execute [ in <mod-exp> : ] <term> .</code></h2>
<p>Reduce the given term in the given module, if <code><mod-exp></code> is given, otherwise in the current module.</p>
<p>For <code>execute</code> equations and transitions, possibly conditional, are taken into account for reduction.</p>
<p>Related: <a href="#reduce"><code>reduce</code></a>, <a href="#breduce"><code>breduce</code></a></p>
<h2 id="extending"><code>extending ( <modexp> )</code></h2>
<p>Imports the object specified by <code>modexp</code> into the current module, allowing models to be inflated, but not collapsing. See <a href="#moduleexpression"><code>module expression</code></a> for format of <code>modexp</code>.</p>
<p>Related: <a href="#using"><code>using</code></a>, <a href="#protecting"><code>protecting</code></a>, <a href="#including"><code>including</code></a></p>
<h2 id="find"><code>find {+rule | -rule}</code></h2>
<p>Find all axioms which possibly rewrite the current term.</p>
<h2 id="switch-find-all-rules"><code>find all rules</code> switch</h2>
<p>If this switch is on, the <a href="#apply"><code>apply</code></a> command will search for applicable rules not only in the set of user-defined equations, but also in those added by the system.</p>
<h2 id="flag"><code>flag(<name>, { on | off })</code></h2>
<p>(pignose)</p>
<h2 id="fullreset"><code>full reset</code></h2>
<p>Reinitializes the internal state of the system. All supplied modules definitions are lost.</p>
<p>Related: <a href="#prelude"><code>prelude</code></a>, <a href="#reset"><code>reset</code></a></p>
<h2 id="gendoc"><code>gendoc <pathname></code></h2>
<p>generates reference manual from system’s on line help documents, and save it to <code>pathname</code>.</p>
<h2 id="citp-goal"><code>:goal { <sentence> . ... }</code></h2>
<p>Define the initial goal for CITP</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h3 id="example-7">Example</h3>
<pre><code>CafeOBJ> select PNAT .
PNAT> :goal {
eq [lemma-1]: M:PNat + 0 = M .
eq [lemma-2]: M:PNat + s N:PNat = s( M + N ) .
}</code></pre>
<h2 id="goal"><code>goal <term> .</code></h2>
<p>(pignose)</p>
<h2 id="citp-imply"><code>:imp "[" <label> "]" by "{" <variable> <- <term>; ..."}"</code></h2>
<p>TODO (future extension)</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="imports"><code>imports { <import-decl> }</code></h2>
<p>Block enclosing import of other modules (<code>protecting</code> etc). Other statements are not allowed within the <code>imports</code> block. Optional structuring of the statements in a module.</p>
<p>Related: <a href="#using"><code>using</code></a>, <a href="#protecting"><code>protecting</code></a>, <a href="#including"><code>including</code></a>, <a href="#extending"><code>extending</code></a>, <a href="#axioms"><code>axioms</code></a>, <a href="#signature"><code>signature</code></a></p>
<h2 id="switch-include-bool"><code>include BOOL</code> switch</h2>
<p>Possible values: <code>on</code> <code>off</code>, default <code>on</code>.</p>
<p>By default a couple of built-in modules are implicitly imported with protecting mode. In particular, BOOL is of practical importance. It defines Boolean operators. It is imported to admit conditional axioms.</p>
<p>This switch allows to disable automatic inclusion of BOOL.</p>
<h2 id="switch-include-rwl"><code>include RWL</code> switch</h2>
<p>Possible values: <code>on</code> <code>off</code>, default <code>off</code>.</p>
<p>This switch allows to disable automatic inclusion of RWL.</p>
<h2 id="including"><code>including ( <modexp> )</code></h2>
<p>Imports the object specified by <code>modexp</code> into the current module.</p>
<p>See <a href="#moduleexpression"><code>module expression</code></a> for format of <code>modexp</code>.</p>
<p>Related: <a href="#moduleexpression">module expression</a>, <a href="#using"><code>using</code></a>, <a href="#protecting"><code>protecting</code></a>, <a href="#extending"><code>extending</code></a></p>
<h2 id="citp-ind"><code>:ind { on (<variable> ...) | '{' on (<variable> ...) base (<Term> . ... <Term> .) step (<Term> . ... <Term> .) '}'</code></h2>
<p>‘:ind on (<variable> …)’ defines the variable for the induction tactic of CITP. ‘:ind { … }’ defines induction variable(s) and base pattern and step pattern specified by <Term>s.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h3 id="example-8">Example</h3>
<pre><code>:ind on (M:PNat)
:ind { on (M:PNat)
base (<Term> . ... <Term> .)
step (<Term> . ... <Term> .)
}</code></pre>
<h2 id="init"><code>init [as <name>] { "[" <label> "]" | "(" <sentence> "")} by "{" <variable> <- <term>; ... "}"</code></h2>
<p>Instantiates an equation specified by <code><label></code> by replacing the <code><variable></code>s in the equation with the respective <code><term></code>s. The resulting equation is added to the set of axioms. If optional <code>as <name></code> is given, label of the instantiated axiom is overwritten by <name>.</p>
<p>Related: <a href="#open"><code>open</code></a></p>
<h2 id="citp-init"><code>:init [as <name>] { "[" <label> "]" | "(" <sentence> "")} by "{" <variable> <- <term>; ... "}"</code></h2>
<p>Instantiates an equation specified by <code><label></code> by replacing the <code><variable></code>s in the equation with the respective <code><term></code>s. The resulting equation is added to the set of axioms. If optional <code>as <name></code> is given, label of the instantiated axiom is overwritten by <name>.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="input"><code>input <pathname></code></h2>
<p>Requests the system to read the file specified by the pathname. The file itself may contain <code>input</code> commands. CafeOBJ reads the file up to the end, or until it encounters a line that only contains (the literal) <code>eof</code>.</p>
<h2 id="inspect"><code>inspect <term></code></h2>
<p>Inspect the internal structure of <code><term></code>.</p>
<h2 id="instantiation">instantiation of parameterized modules</h2>
<p>Parameterized modules allow for instantiation. The process of instantiation binds actual parameters to formal parameters. The result of an instantiation is a new module, obtained by replacing occurrences of parameter sorts and operators by their actual counterparts. If, as a result of instantiation, a module is imported twice, it is assumed to be imported once and shared throughout.</p>
<p>Instantiation is done by</p>
<p><code><module_name> ( <bindings> )</code></p>
<p>where <code><module_name></code> is the name of a parameterized module, and <code><bindings></code> is a comma-separated list of binding constructs.</p>
<dl>
<dt>using declared views</dt>
<dd><p>you may bind an already declared view to a parameter:</p>
<p><code><parameter> <= <view_name></code></p>
<p>If a module <code>M</code> has a parameter <code>X :: T</code> and a view <code>V</code> from <code>T</code> to <code>M'</code> is declared, <code>V</code> may be bound to <code>X</code>, with the effect that</p>
<ol type="1">
<li><p>The sort and operator names of <code>T</code> that appear in the body of <code>M</code> are replaced by those in <code>M'</code>, in accordance with <code>V</code>,</p></li>
<li><p>The common submodules of <code>M</code> and <code>M'</code> are shared.</p></li>
</ol>
</dd>
<dt>using ephemeral views</dt>
<dd><p>In this case the view is declared and used at the same time.</p>
<p><code><parameter> <= view to <mod_name> { <view_elements> }</code></p>
<p>See <a href="#view"><code>view</code></a> for details concerning <code><view_elements></code>. The <code>from</code> parameter in the <code>view</code> declaration is taken from <code><parameter></code>.</p>
</dd>
</dl>
<p>To make notation more succinct, parameters can be identified also by position instead of names as in</p>
<p><code><mod_name> ( <view_name>, <view_name> )</code></p>
<p>which would bind the <code><view_name></code>s to the respective parameters of the parameterized module <code><mod_name></code>.</p>
<p>This can be combined with the ephemeral definition of a view like in the following example (assume <code>ILIST</code> has two parameters):</p>
<pre><code>module NAT-ILIST {
protecting ( ILIST(SIMPLE-NAT { sort Elt -> Nat },
DATATYPE { sort Elt -> Data }) )
}</code></pre>
<h2 id="citp-is"><code>:is</code></h2>
<p>Boolean expression: <code>A :is B</code> where <code>A</code> is a term and <code>B</code> is a sort. Returns true if <code>A</code> is of sort <code>B</code>.</p>
<h2 id="let"><code>let <identifier> = <term> .</code></h2>
<p>Using <code>let</code> one can define aliases, or context variables. Bindings are local to the current module. Variable defined with <code>let</code> can be used in various commands like <code>reduce</code> and <code>parse</code>.</p>
<p>Although <code>let</code> defined variable behave very similar to syntactic shorthands, they are not. The right hand side <code><term></code> needs to be a fully parsable expression.</p>
<h2 id="lex"><code>lex (<op>, ..., <op>)</code></h2>
<p>(pignose)</p>
<h2 id="switch-libpath"><code>libpath</code> switch</h2>
<p>Possible values: list of strings.</p>
<p>The switch <code>libpath</code> contains a list of directories where CafeOBJ searches for include files. Addition and removal of directories can be done with</p>
<pre><code>set libpath + <path1>:<path2>:...
set libpath - <path1>:<path2>:...</code></pre>
<p>or the full libpath reset by <code>set libpath <path1>:<path2>:...</code></p>
<p>The current directory has a privileged status: It is always searched first and cannot be suppressed.</p>
<h2 id="lisp"><code>lisp</code></h2>
<p>Evaluates the following lisp expression.</p>
<h3 id="example-9">Example</h3>
<pre><code>CafeOBJ> lisp (+ 4 5)
(+ 4 5) -> 9</code></pre>
<h2 id="lispq"><code>lispq</code></h2>
<p>Evaluates the following lisp expression, but does not display the result (q for quiet).</p>
<h2 id="list"><code>list { axiom | sos | usable | flag | param | option | demod }</code></h2>
<p>(pignose)</p>
<h2 id="lookup"><code>look up <something></code></h2>
<p>displays the location (module) and further information where <code><something></code> has been defined.</p>
<h3 id="example-10">Example</h3>
<pre><code>open INT .
%INT> look up Nat .
Nat
- sort declared in NAT-VALUE
- operator:
op Nat : -> SortId { constr prec: 0 }
-- declared in module NAT-VALUE
%INT></code></pre>
<h2 id="ls"><code>ls <pathname></code></h2>
<p>lists the given <code>pathname</code>. Argument is obligatory.</p>
<p>Related: <a href="#pwd"><code>pwd</code></a>, <a href="#cd"><code>cd</code></a></p>
<h2 id="make"><code>make <mod_name> ( <mod_exp> )</code></h2>
<p>This commands defines a new module <code><mod_name></code> by evaluating the module expression <code><mod_exp></code>.</p>
<p>Related: <a href="#moduleexpression"><code>module expression</code></a></p>
<h2 id="match"><code>match <term_spec> to <pattern> .</code></h2>
<p>Matches the term denoted by <code><term_spec></code> to the pattern. <code><term_spec></code> is either <code>top</code> or <code>term</code> for the term set by the <code>start</code> command; <code>subterm</code> for the term selected by the <code>choose</code> command; <code>it</code> has the same meaning as <code>subterm</code> if <code>choose</code> was used, otherwise the same meaning as <code>top</code>, or a normal term expression.</p>
<p>The given <code><pattern></code> is either <code>rules</code>, <code>-rules</code>, <code>+rules</code>, one of these three prefixed by <code>all</code>, or a term. If one of the <code>rules</code> are given, all the rules where the left side (for <code>+rules</code>), the right side (for <code>-rules</code>), or any side (for <code>rules</code>) matches. If the <code>all</code> (with separating space) is given all rules in the current context, including those declared in built-in modules, are inspected.</p>
<p>If a term is given, then the two terms are matched, and if successful, the matching substitution is printed.</p>
<h2 id="switch-memo"><code>memo</code> switch</h2>
<p>controls the memorization of computations. The system memorizes evaluations of operators declared with the <a href="#opattr"><code>memo</code></a> operator attribute. Turning this switch off disables all memorization.</p>
<h2 id="module"><code>[sys:]module[!|*] <modname> [ ( <params> ) ] [ <principal_sort_spec> ] { mod_elements ... }</code></h2>
<p>Defines a module, the basic building block of CafeOBJ. Possible elements are declarations of</p>
<ul>
<li>import - see <code>protecting</code>, <code>extending</code>, <code>including</code>, <code>using</code></li>
<li>sorts - see <code>sort declaration</code></li>
<li>variable - see <code>var</code></li>
<li>equation - see <code>op</code>, <code>eq</code>, <code>ceq</code>, <code>bop</code>, <code>beq</code>, <code>bceq</code></li>
<li>transition - see <code>trans</code>, <code>ctrans</code>, <code>btrans</code>, <code>bctrans</code></li>
</ul>
<p><code>modname</code> is an arbitrary string.</p>
<p><code>module*</code> introduces a loose semantic based module.</p>
<p><code>module!</code> introduces a strict semantic based module.</p>
<p><code>module</code> introduces a module without specified semantic type.</p>
<p>If <code>params</code> are given, it is a parameterized module. See <a href="#parameterizedmodule"><code>parameterized module</code></a> for more details.</p>
<p>If <code>principal_sort_spec</code> is given, it has to be of the form <code>principal-sort <sortname></code> (or <code>p-sort <sortname></code>). The principal sort of the module is specified, which allows more concise <code>view</code>s from single-sort modules as the sort mapping needs not be given.</p>
<h2 id="moduleexpression"><code>module expression</code></h2>
<p>In various syntax elements not only module names itself, but whole module expressions can appear. A typical example is</p>
<p><code>open <mod_exp> .</code></p>
<p>which opens a module expression. The following constructs are supported:</p>
<dl>
<dt>module name</dt>
<dd>using the name of a module
</dd>
<dt>renaming</dt>
<dd><p><code><mod_exp> * { <mappings> }</code></p>
<p>This expressions describes a new module where sort and/or operators are renamed. <code><mappings></code> are like in the case of <a href="#view"><code>view</code></a> a comma separated list of mappings of either sorts (<code>sort</code> and <code>hsort</code>) or operators (<code>op</code> and <code>bop</code>). Source names may be qualified, while target names are not, they are required to be new names. Renaming is often used in combination with <a href="#instantiation">instantiation</a>.</p>
</dd>
<dt>summation</dt>
<dd><p><code><mod_exp> + <mod_exp></code></p>
<p>This expression describes a module consisting of all the module elements of the summands. If a submodule is imported more than once, it is assumed to be shared.</p>
</dd>
</dl>
<h2 id="names"><code>names <mod-exp></code> .</h2>
<p>List up all the named objects in module <mod-exp>.</p>
<h2 id="no-autoload"><code>no autoload <module-name></code></h2>
<p>Stop <code>autoload</code> of module with the name <module-name> . Please refer to <code>autoload</code> command.</p>
<p>Related: <a href="#autoload"><code>autoload</code></a></p>
<h2 id="citp-normalize"><code>:normalize { on | off}</code></h2>
<p>Normalize the LHS of an instance of the axiom generated by :init command.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="onthefly">on-the-fly declarations</h2>
<p>Variables and constants can be declared <em>on-the-fly</em> (or <em>inline</em>). If an equation contains a qualified variable (see <a href="#qualified">qualified term</a>), i.e., <code><name>:<sort-name></code>, then from this point on <em>within</em> the current equation only <code><name></code> is declared as a variable of sort <code><sort-name></code>.</p>
<p>It is allowed to redeclare a previously defined variable name via an on-the-fly declaration, but as mentioned above, not via an explicit redeclaration.</p>
<p>Using a predeclared variable name within an equation first as is, that is as the predeclared variable, and later on in the same equation with an on-the-fly declaration is forbidden. That is, under the assumption that <code>A</code> has been declared beforehand, the following equation is <em>not</em> valid:</p>
<p><code>eq foo(A, A:S) = A .</code></p>
<p>On-the-fly declaration of constants are done the same way, where the <code><name></code> is a constant name as in `<code>a:Nat</code>. Using this construct is similar to defining an operator</p>
<p><code>op <name> : -> <sort></code></p>
<p>or in the above example, <code>op a : -> Nat .</code>, besides that the on-the-fly declaration of constants, like to one of variables, is only valid in the current context (i.e., term or axiom). These constant definitions are quite common in proof scores.</p>
<p>Related: <a href="#var"><code>var</code></a></p>
<h2 id="op"><code>op <op-spec> : <sorts> -> <sort> { <attribute-list> }</code></h2>
<p>Defines an operator by its domain, co-domain, and the term construct. <code><sorts></code> is a space separated list of sort names, <code><sort></code> is a single sort name. <code><op-spec></code> can be of the following forms:</p>
<dl>
<dt>prefix-spec</dt>
<dd><p>the <code><op-spec></code> does not contain a literal <code>_</code>: This defines a normal prefix operator with domain <code><sorts></code> and co-domain <code><sort></code></p>
<p>Example: <code>op f : S T -> U</code> mixfix-spec</p>
</dd>
<dd><p>the <code><op-spec></code> contains exactly as many literal <code>_</code> as there are sort names in <code><sorts></code>: This defines an arbitrary mixfix (including postfix) operator where the arguments are inserted into the positions designated by the underbars.</p>
<p>Example: <code>op _+_ : S S -> S</code></p>
</dd>
</dl>
<p>For the description of <code><attribute-list></code> see the entry for <a href="#opattr">operator attributes</a>.</p>
<h2 id="open"><code>open <mod_exp> .</code></h2>
<p>This command opens the module specified by the module expression <code><mod_exp></code> and allows for declaration of new sorts, operators, etc.</p>
<p>Related: <a href="#select"><code>select</code></a>, <a href="#moduleexpression"><code>module expression</code></a>, <a href="#close"><code>close</code></a></p>
<h2 id="opattr"><code>operator attributes</code></h2>
<p>In the specification of an operator using the <a href="#op"><code>op</code></a> (and related) keyword, attributes of the operator can be specified. An <code><attribute-list></code> is a space-separate list of single attribute definitions. Currently the following attributes are supported</p>
<dl>
<dt><code>associative</code></dt>
<dd>specifies an associative operator, alias <code>assoc</code>
</dd>
<dt><code>commutative</code></dt>
<dd>specifies a commutative operator, alias <code>comm</code>
</dd>
<dt><code>itempotence</code></dt>
<dd>specifies an idempotent operator, alias <code>idem</code>
</dd>
<dt><code>id: <const></code></dt>
<dd>specifies that an identity of the operator exists and that it is <code><const></code>
</dd>
<dt><code>prec: <int></code></dt>
<dd>specifies the parsing precedence of the operator, an integer <int>. Smaller precedence values designate stronger binding. See <a href="#opprec">operator precedence</a> for details of the predefined operator precedence values.
</dd>
<dt><code>l-assoc</code> and <code>r-assoc</code></dt>
<dd>specifies that the operator is left-associative or right-associative
</dd>
<dt><code>constr</code></dt>
<dd>specifies that the operator is a constructor of the coarity sort. (not evaluated at the moment)
</dd>
<dt><code>strat: ( <int-list> )</code></dt>
<dd><p>specifies the evaluation strategy. Each integer in the list refers to an argument of the operator, where <code>0</code> refers to the whole term, <code>1</code> for the first argument, etc. Evaluation proceeds in order of the <code><int-list></code>. Example:</p>
<p><code>op if_then_else_fi : Bool Int Int -> Int { strat: (1 0) }</code></p>
<p>In this case the first argument (the Boolean term) is tried to be evaluated, and depending on that either the second or third. But if the first (Boolean) argument cannot be evaluated, no evaluation in the subterms will appear.</p>
<p>Using negative values allows for lazy evaluation of the corresponding arguments.</p>
</dd>
<dt><code>memo</code></dt>
<dd>tells the system to remember the results of evaluations where the operator appeared. See <a href="#switch-memo"><code>memo</code> switch</a> for details.
</dd>
</dl>
<p>Remarks:</p>
<ul>
<li><p>Several operators of the same arity/coarity can be defined by using <code>ops</code> instead of <code>op</code>:</p>
<p><code>ops f g : S -> S</code></p>
<p>For the case of mixfix operators the underbars have to be given and the expression surrounded by parenthesis:</p>
<p><code>ops (_+_) (_*_) : S S -> S</code></p></li>
<li><p>Spaces <em>can</em> be part of the operator name, thus an operator definition of <code>op foo op : S -> S</code> is valid, but not advisable, as parsing needs hints.</p></li>
<li><p>A single underbar cannot be an operator name.</p></li>
</ul>
<p>Related: <a href="#bop"><code>bop</code></a></p>
<h2 id="opprec"><code>operator precedence</code></h2>
<p>CafeOBJ allows for complete freedom of syntax, in particular infix operators and overloading. To correctly parse terms that are ambiguous, all operators have precedence values. These values can be adjusted manually during definition of the operator (see <a href="#opattr">operator attributes</a>). In absence of manual specification of the operator precedence, the values are determined by the following rules:</p>
<ul>
<li>standard prefix operators, i.e., those of the form <code>op f : S1 .. Sk -> S</code>, receive operator precedence value 0.</li>
<li>unary operators, i.e., those of the form <code>op u_ : S1 -> S</code>, receive precedence 15.</li>
<li>mix-fix operators with first and last token being arguments, i.e., those of the form <code>op _ arg-or-op _ : S1 .. Sk -> S</code>, receive precedence 41.</li>
<li>all other operators (constants, operators of the form <code>a _ b</code>, etc.) receive precedence 0.</li>
</ul>
<p>Related: <a href="#opattr">operator attributes</a></p>
<h2 id="option"><code>option { reset | = <name> }</code></h2>
<p>(pignose)</p>
<h2 id="citp-order"><code>:order (<op>, ..., <op>)</code></h2>
<h2 id="param"><code>param(<name>, <value>)</code></h2>
<p>(pignose)</p>
<h2 id="parameterizedmodule"><code>parameterized module</code></h2>
<p>A module with a parameter list (see <code>module</code>) is a parameterized module. Parameters are given as a comma (<code>,</code>) separated list. Each parameter is of the form <code>[ <import_mode> ] <param_name> :: <module_name></code> (spaces around <code>::</code> are obligatory).</p>
<p>The parameter’s module gives minimal requirements on the module instantiation.</p>
<p>Within the module declaration sorts and operators of the parameter are qualified with <code>.<parameter_name></code> as seen in the example below.</p>
<p>Related: <a href="#qualifiedother">qualified sort</a></p>
<h3 id="example-11">Example</h3>
<pre><code>mod* C {
[A]
op add : A A -> A .
}
mod! TWICE(X :: C) {
op twice : A.X -> A.X .
eq twice(E:A.X) = add.X(E,E) .
}</code></pre>
<h2 id="parse"><code>parse [ in <mod-exp> : ] <term> .</code></h2>
<p>Tries to parse the given term within the module specified by the module expression <code><mod-exp></code>, or the current module if not given, and returns the parsed and qualified term.</p>
<p>In case of ambiguous terms, i.e., different possible parse trees, the command will prompt for one of the trees.</p>
<p>Related: <a href="#qualified"><code>qualified term</code></a></p>
<h2 id="switch-parse-normalize"><code>parse normalize</code> switch</h2>
<p>If this switch is ‘on’ (defalult is ‘off’), terms with associative operators are always parsed as right associative.</p>
<h2 id="popd"><code>popd</code></h2>
<p>Changes the current working directory to the last on on the push stack.</p>
<p>Related: <a href="#dirs"><code>dirs</code></a>, <a href="#pwd"><code>pwd</code></a>, <a href="#pushd"><code>pushd</code></a>, <a href="#cd"><code>cd</code></a>, <a href="#ls"><code>ls</code></a></p>
<h2 id="pred"><code>pred <op-spec> : <sorts></code></h2>
<p>Short hand for <code>op <op-spec> : <sorts> -> Bool</code> defining a predicate.</p>
<p>Related: <a href="#bpred"><code>bpred</code></a>, <a href="#op"><code>op</code></a></p>
<h2 id="prelude"><code>prelude <file></code></h2>
<p>Loads the given <code><file></code> as prelude. That is, a call to <a href="#reset"><code>reset</code></a> will reset the definitions made in this file.</p>
<p>Related: <a href="#fullreset"><code>full reset</code></a>, <a href="#reset"><code>reset</code></a></p>
<h2 id="switch-print-depth"><code>print depth</code> switch</h2>
<p>Possible values: natural numbers, default <code>unlimited</code>.</p>
<p>Controls to which depth terms are printed.</p>
<h2 id="switch-print-mode"><code>print mode</code> switch</h2>
<p>Possible values: <code>normal</code> <code>fancy</code> <code>tree</code> <code>s-expr</code></p>
<p>Selects one of the print modes.</p>
<h2 id="switch-print-trs"><code>print trs</code> switch</h2>
<p>Possible values: <code>on</code> <code>off</code>, default <code>off</code></p>
<p>If set to <code>on</code>, print the rules used during reduction of <code>=(_,_)=>+_if_suchThat_{_}</code>.</p>
<p>Related: <a href="#searchpredicate"><code>search predicates</code></a></p>
<h2 id="protect"><code>protect <module-name></code></h2>
<p>Protect a module from being overwritten. Some modules vital for the system are initially protected. Can be reversed with <code>unprotect</code>.</p>
<p>Related: <a href="#unprotect"><code>unprotect</code></a></p>
<h2 id="protecting"><code>protecting ( <modexp> )</code></h2>
<p>Imports the object specified by <code>modexp</code> into the current module, preserving all intended models as they are. See <a href="#moduleexpression"><code>module expression</code></a> for format of <code>modexp</code>.</p>
<p>Related: <a href="#including"><code>including</code></a>, <a href="#using"><code>using</code></a>, <a href="#extending"><code>extending</code></a></p>
<h2 id="provide"><code>provide <feature></code></h2>
<p>Discharges a feature requirement: once <code>provide</code>d, all the subsequent <code>require</code>ments of a feature are assumed to have been fulfilled already.</p>
<p>Related: <a href="#require"><code>require</code></a></p>
<h2 id="pushd"><code>pushd <directory></code></h2>
<p>Changes the working directory to <code><directory></code>, and puts the current directory onto the push stack. Going back can be done with <code>pop</code>.</p>
<p>Related: <a href="#dirs"><code>dirs</code></a>, <a href="#pwd"><code>pwd</code></a>, <a href="#popd"><code>popd</code></a>, <a href="#cd"><code>cd</code></a>, <a href="#ls"><code>ls</code></a></p>
<h2 id="pvar"><code>pvar <var-name> : <sort-name></code></h2>
<p>(pignose)</p>
<p>Related: <a href="#var"><code>vars</code></a>, <a href="#var"><code>var</code></a></p>
<h2 id="pwd"><code>pwd</code></h2>
<p>Prints the current working directory.</p>
<p>Related: <a href="#dirs"><code>dirs</code></a>, <a href="#popd"><code>popd</code></a>, <a href="#pushd"><code>pushd</code></a>, <a href="#ls"><code>ls</code></a>, <a href="#cd"><code>cd</code></a></p>
<h2 id="qualifiedother">qualified sort/operator/parameter</h2>
<p>CafeOBJ allows for using the same name for different sorts, operators, and parameters. One example is declaring the same sort in different modules. In case it is necessary to qualify the sort, operator, or parameter, the intended module name can be affixed after a literal <code>.</code>: <code><name>.<modname></code></p>
<p>Example: In case the same sort <code>Nat</code> is declared in both the module <code>SIMPLE-NAT</code> and <code>PANAT</code>, one can use <code>Nat.SIMPLE-NAT</code> to reference the sort from the former module.</p>
<p>Furthermore, a similar case can arise when operators of the same name have been declared with different number of arguments. During operator renaming (see <a href="#view">view</a>) the need for qualification of the number of parameters might arise. In this case the number can be specified after an affixed <code>/</code>: <code><opname>/<argnr></code></p>
<p>Related: <a href="#qualified"><code>qualified term</code></a>, <a href="#parameterizedmodule"><code>parameterized module</code></a></p>
<h2 id="qualified"><code>qualified term</code></h2>
<p>In case that a term can be parsed into different sort, it is possible to qualify the term to one of the possible sorts by affixing it with <code>: <sort-name></code> (spaces before and after the <code>:</code> are optional).</p>
<p>Related: <a href="#parse"><code>parse</code></a></p>
<h3 id="example-12">Example</h3>
<p><code>(1):NzNat</code> <code>(2):Nat</code></p>
<h2 id="switch-quiet"><code>quiet</code> switch</h2>
<p>Possible values: <code>on</code> <code>off</code>, default <code>off</code></p>
<p>If set to <code>on</code>, the system only issues error messages.</p>
<p>Related: <a href="#switch-verbose"><code>verbose</code></a></p>
<h2 id="quit"><code>quit</code></h2>
<p>Leaves the CafeOBJ interpreter.</p>
<h2 id="citp-red"><code>{ :red | :exec | :bred } [in <goal-name> :] <term> .</code></h2>
<p>reduce the term in specified goal <goal-name>.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="reduce"><code>reduce [ in <mod-exp> : ] <term> .</code></h2>
<p>Reduce the given term in the given module, if <code><mod-exp></code> is given, otherwise in the current module.</p>
<p>For <code>reduce</code> only equations and conditional equations are taken into account for reduction.</p>
<p>Related: <a href="#breduce"><code>breduce</code></a>, <a href="#execute"><code>execute</code></a></p>
<h2 id="switch-reduce-conditions"><code>reduce conditions</code> switch</h2>
<p>Possible values: <code>on</code> <code>off</code>, default <code>off</code>.</p>
<p>When using <a href="#apply"><code>apply</code></a> to step through a reduction, this switch allows to turn on automatic reduction of conditions in conditional equations.</p>
<p>Related: <a href="#apply"><code>apply</code></a></p>
<h2 id="regularize"><code>regularize <mod-name></code></h2>
<p>Regularizes the signature of the given module, ensuring that every term has exactly one minimal parse tree. In this process additional sorts are generated to ensure unique least sort of all terms.</p>
<p>Modules can be automatically regularized by the interpreter if the <code>regularize signature</code> switch is turn to <code>on</code>.</p>
<h2 id="switch-regularize-signature"><code>regularize signature</code> switch</h2>
<p>See <a href="#regularize">`regularize</a></p>
<h2 id="require"><code>require <feature> [ <pathname> ]</code></h2>
<p>Requires a feature, which usually denotes a set of module definitions. Given this command, the system searches for a file named the feature, and read the file if found. If the <code><feature></code> contains <code>::</code>, they are treated as path separators.</p>
<p>If a pathname is given, the system searches for a file named the pathname instead.</p>
<p>Related: <a href="#provide"><code>provide</code></a></p>
<h3 id="example-13">Example</h3>
<pre><code>CafeOBJ> require foo::bar</code></pre>
<p>would search for <code>foo/bar.cafe</code> in the pathes from <code>libpath</code></p>
<h2 id="citp-reset"><code>:reset</code></h2>
<p>Discard the current proof session.</p>
<h2 id="reset"><code>reset</code></h2>
<p>Restores the definitions of built-in modules and preludes, but does not affect other modules.</p>
<p>Related: <a href="#prelude"><code>prelude</code></a>, <a href="#fullreset"><code>full reset</code></a></p>
<h2 id="resolve"><code>resolve {. | <file-path> }</code></h2>
<p>(pignose)</p>
<h2 id="restore"><code>restore <pathname></code></h2>
<p>Restores module definitions from the designated file <code>pathname</code> which has been saved with the <code>save</code> command. <code>input</code> can also be used but the effects might be different.</p>
<p>TODO – should we keep the different effects? What is the real difference?</p>
<p>Related: <a href="#target_not_found"><code>save-system</code></a>, <a href="#save"><code>save</code></a>, <a href="#input"><code>input</code></a></p>
<h2 id="switch-rewrite"><code>rewrite limit</code> switch</h2>
<p>Possible values: positive integers, default not specified.</p>
<p>Allows limiting the number of rewrite steps during a step-wise execution.</p>
<p>Related: <a href="#switch-step"><code>step switch</code></a></p>
<h2 id="citp-roll"><code>:roll back</code></h2>
<p>Reverts the strategy that led to the current target goal. The current target goal is removed from the proof tree.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="citp-rule"><code>:rule</code></h2>
<p>Adds the critical pair computed by the last <a href="#citp-cp"><code>:cp</code></a> command as rule to the current goal.</p>
<p>Related: <a href="#citp-equation"><code>:equation</code></a>, <a href="#citp-cp"><code>:cp</code></a>, <a href="#citp"><code>citp</code></a></p>
<h2 id="rule"><code>rule [ <label-exp> ] <term> => <term> .</code></h2>
<p>Synonym of <a href="#trans"><code>trans</code></a>.</p>
<p>Related: <a href="#trans"><code>trans</code></a></p>
<h2 id="save"><code>save <pathname></code></h2>
<p>Saves module definitions into the designated file <code>pathname</code>. File names should be suffixed with <code>.bin</code>.</p>
<p><code>save</code> also saves the contents of prelude files as well as module definitions given in the current session.</p>
<p>Related: <a href="#target_not_found"><code>save-system</code></a>, <a href="#restore"><code>restore</code></a>, <a href="#input"><code>input</code></a></p>
<h2 id="save-option"><code>save-option <name></code></h2>
<p>(pignose)</p>
<h2 id="scase"><code>scase (<term>) in (<mod-exp>) as <name> { <decl> ..} : <term> .</code></h2>
<p>Obsolete citp command. Split the goal by user specified cases.</p>
<h2 id="searchpredicate"><code>search predicates</code></h2>
<p>CafeOBJ provides a whole set of search predicates, that searches the reachable states starting from a given state, optionally checking additional conditions. All of them based on the following three basic ones:</p>
<ul>
<li><code>S =(n,m)=>* SS [if Pred]</code> search states reachable by 0 or more transitions;</li>
<li><code>S =(n,m)=>+ SS [if Pred]</code> search states reachable by 1 or more transitions;</li>
<li><code>S =(n,m)=>! SS [if Pred]</code> search states reachable by 0 or more transitions, and require that the reached state is a final state, i.e., no further transitions can be applied.</li>
</ul>
<p>To allow for conditional transitions, a transition is only considered in the search if <code>Pred</code> holds.</p>
<p>The parameters <code>n</code> and <code>m</code> in these search predicates:</p>
<ul>
<li><code>n</code>, a natural number or <code>*</code>, gives the maximal number of solutions to be searched. If <code>*</code> is given all solutions are searched exhaustively.</li>
<li><code>m</code>, a natural number but not <code>*</code>, gives the maximal depth up to which search is performed.</li>
</ul>
<p>The predicates return true if there is a (chain of) transitions that fits the parameters (<code>n</code>,<code>m</code>, and <code>*</code>, <code>+</code>, <code>!</code>) and connects <code>S</code> with <code>SS</code>.</p>
<p>There are two orthogonal extension to this search predicate, one adds a <code>suchThat</code> clause, one adds a <code>withStateEq</code> clause.</p>
<dl>
<dt><code>S =(n,m)=>* SS [if Pred1] suchThat Pred2</code></dt>
<dd>(and similar for <code>!</code> and <code>+</code>) In this case not only the existence, of a transition sequence is tested, but also whether the predicate <code>Pred2</code>, which normally takes <code>S</code> and <code>SS</code> as arguments, holds.
</dd>
<dt><code>S =(n,m)=>* SS [if Pred1] withStateEq Pred2</code></dt>
<dd>(and similar for <code>!</code> and <code>+</code>) <code>Pred2</code> is used to determine whether a search continues at <code>SS</code> or not, by comparing <code>SS</code> with all states that have been traversed in the current search. If the predicate <code>Pred2</code> returns true on the combination of <code>SS</code> as first argument, and any of the previously visited states as second argument, then the search is <em>not</em> continued after <code>SS</code>. (This is a kind of loop detection.)
</dd>
</dl>
<p>These two cases can also be combined into</p>
<p><code>S =(n,m)=>* SS [if Pred1] suchThat Pred2 withStateEq Pred3</code></p>
<h2 id="citp-select"><code>:select <goal-name></code></h2>
<p>Select a goal for further application of tactics.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="select"><code>select <mod_exp> .</code></h2>
<p>Selects a module given by the module expression <code><mod_exp></code> as the current module. All further operations are carried out within the given module. In contrast to <code>open</code> this does not allow for modification of the module, e.g., addition of new sorts etc.</p>
<p>Related: <a href="#moduleexpression"><code>module expression</code></a>, <a href="#open"><code>open</code></a></p>
<h2 id="citp-set"><code>:set(<name>, { on | off | show })</code></h2>
<p>Set or show various flags of CITP CafeOBJ.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="set"><code>set <name> [option] <value></code></h2>
<p>Depending on the type of the switch, options and value specification varies. Possible value types for switches are Boolean (<code>on</code>, <code>off</code>), string (<code>"value"</code>), integers (5434443), lists (lisp syntax).</p>
<p>For a list of all available switches, use <code>set ?</code>. To see the current values, use <code>show switches</code>. To single out two general purpose switches, <code>verbose</code> and <code>quiet</code> tell the system to behave in the respective way.</p>
<p>Related: <a href="#switches"><code>switches</code></a>, <a href="#show"><code>show</code></a></p>
<h2 id="citp-show"><code>:show goal|unproved|proof|discharged</code></h2>
<p>Shows the current goal, the up-to-now unproven (sub-)goals, and the current proof.</p>
<p>Related: <a href="#citp-describe"><code>:describe</code></a>, <a href="#citp"><code>citp</code></a></p>
<h3 id="example-14">Example</h3>
<pre><code>PNAT> :show proof
root*
[si] 1*
[ca] 1-1*
[ca] 1-2*
[tc] 1-2-1*
[si] 2*
[ca] 2-1*
[ca] 2-2*
[tc] 2-2-1*
PNAT></code></pre>
<h2 id="show"><code>show <something></code></h2>
<p>The <code>show</code> command provides various ways to inspect all kind of objects of the CafeOBJ language. For a full list call <code>show ?</code>.</p>
<p>Some of the more important (but far from complete list) ways to call the <code>show</code> command are:</p>
<ul>
<li><code>show [ <modexp> ]</code> - describes the current modules of the one specified as argument</li>
<li><code>show module tree [ <modexp> ]</code> - displays submodules of <modexp> in tree format</li>
<li><code>show switches</code> - lists all possible switches</li>
<li><code>show term [ tree ]</code> - displays a term, possible in tree format</li>
</ul>
<p>See the entry for <a href="#switches"><code>switches</code></a> for a full list.</p>
<p>Related: <a href="#describe"><code>describe</code></a>, <a href="#switches"><code>switches</code></a></p>
<h2 id="switch-show-mode"><code>show mode</code> switch</h2>
<p>Possible values for <code>set show mode <mode></code> are <code>cafeobj</code> and <code>meta</code>.</p>
<h2 id="sigmatch"><code>sigmatch (<mod-exp>) to (<mod-exp>)</code></h2>
<p>(pignose)</p>
<h2 id="signature"><code>signature { <sig-decl> }</code></h2>
<p>Block enclosing declarations of sorts and operators. Other statements are not allowed within the <code>signature</code> block. Optional structuring of the statements in a module.</p>
<p>Related: <a href="#op"><code>op</code></a>, <a href="#sort"><code>sort</code></a>, <a href="#imports"><code>imports</code></a>, <a href="#axioms"><code>axioms</code></a></p>
<h2 id="sort">sort declaration</h2>
<p>CafeOBJ supports two kind of sorts, visible and hidden sorts. Visible sorts are introduced between <code>[</code> and <code>]</code>, while hidden sorts are introduced between <code>*[</code> and <code>]*</code>.</p>
<pre><code> [ Nat ]
*[ Obs ]*</code></pre>
<p>Several sorts can be declared at the same time, as in <code>[ Nat Int ]</code>.</p>
<p>Since CafeOBJ is based on order sorting, sorts can form a partial order. Definition of the partial order can be interleaved by giving</p>
<pre><code> [ <sorts> < <sorts> ]</code></pre>
<p>Where <code>sorts</code> is a list of sort names. This declaration defines an inclusion relation between each pair or left and right sorts.</p>
<h3 id="example-15">Example</h3>
<pre><code> [ A B , C D < A < E, B < D ]</code></pre>
<p>defines five sorts <code>A</code>,…,<code>E</code>, with the following relations: <code>C < A</code>, <code>D < A</code>, <code>A < E</code>, <code>B < D</code>.</p>
<h2 id="sos"><code>sos { = | + | - } { <clause> , ... }</code></h2>
<p>(pignose)</p>
<h2 id="citp-spoiler"><code>:spoiler { on | off}</code></h2>
<p>If the spoiler flag is on, after a strategy other than RD and SI has been applied, the generated sub-goals are automatically checked for provability using the RD strategy. Defaults to <code>off</code>.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="start"><code>start <term> .</code></h2>
<p>Sets the focus onto the given term <code><term></code> of the currently opened module or context. Commands like <code>apply</code>, <code>choose</code>, or <code>match</code> will then operate on this term.</p>
<p>Related: <a href="#match"><code>match</code></a>, <a href="#choose"><code>choose</code></a>, <a href="#apply"><code>apply</code></a></p>
<h2 id="switch-statistics"><code>statistics</code> switch</h2>
<p>Possible values: <code>on</code> <code>off</code>, default <code>on</code>.</p>
<p>After each reduction details about the reduction are shown. Information shown are the time for parsing the expression, the number of rewrites and run time during rewriting, and the number of total matches performed during the reduce.</p>
<h2 id="switch-step"><code>step</code> switch</h2>
<p>Possible values: <code>on</code> <code>off</code>, default <code>off</code>.</p>
<p>With this switch turned on, rewriting proceeds in steps and prompts the user interactively. At each prompt the following commands can be given to the stepper (with our without leading colon <code>:</code>):</p>
<dl>
<dt><code>help</code></dt>
<dd>(<code>h</code>, <code>?</code>) print out help page <code>next</code>
</dd>
<dd>(<code>n</code>) go one step <code>continue</code>
</dd>
<dd>(<code>c</code>) continue rewriting without stepping <code>quit</code>
</dd>
<dd>(<code>q</code>) leave stepper continuing rewrite <code>abort</code>
</dd>
<dd>(<code>a</code>) abort rewriting <code>rule</code>
</dd>
<dd>(<code>r</code>) print out current rewrite rule <code>subst</code>
</dd>
<dd>(<code>s</code>) print out substitution <code>limit</code>
</dd>
<dd>(<code>l</code>) print out rewrite limit count <code>pattern</code>
</dd>
<dd>(<code>p</code>) print out stop pattern <code>stop [<term>] .</code>
</dd>
<dd>set (or unset) stop pattern <code>rwt [<number>] .</code>
</dd>
<dd>set (or unset) max number of rewrite
</dd>
</dl>
<p>Other standard CafeOBJ commands that can be used are <a href="#show"><code>show</code></a>, <a href="#describe"><code>describe</code></a>, <a href="#dirs"><code>dirs</code></a>, <a href="#set"><code>set</code></a>, <a href="#cd"><code>cd</code></a>, <a href="#ls"><code>ls</code></a>, <a href="#pwd"><code>pwd</code></a>, <a href="#pushd"><code>pushd</code></a>, <a href="#popd"><code>popd</code></a>, <a href="#lisp"><code>lisp</code></a>, <a href="#lisp"><code>lispq</code></a>, and (on Unix only) <a href="#commandexec"><code>!</code></a>.</p>
<h2 id="stop"><code>stop</code></h2>
<p>Equivalent to <a href="#switch-stop-pattern"><code>stop pattern switch</code></a></p>
<h2 id="switch-stop-pattern"><code>stop pattern</code> switch</h2>
<p>In <a href="#switch-step">step mode</a>, this command causes reductions to stop when the reductants get to containing subterms that match the given term. If no term is given, this restriction is lifted.</p>
<p>Related: <a href="#switch-step"><code>step switch</code></a></p>
<h3 id="example-16">Example</h3>
<pre><code>CafeOBJ> open NAT .
%NAT> set step on .
%NAT> set stop pattern s 2 .
%NAT> red s s s s s s s s s 0 .
>> target: (s 0)
STEP[1]? c
>> term matches to stop pattern: (s 2)
<< will stop rewriting
>> stop because matches stop pattern.
>> target: (s 2)
STEP[3]? c
(9):NzNat</code></pre>
<h2 id="switches">switches</h2>
<p>Switches control various aspects of the computations and behavior of CafeOBJ. The current list of switches and their values can be shown with</p>
<pre><code>show switches</code></pre>
<p>The single switches are described separately in this manual.</p>
<p>Related: <a href="#show"><code>show</code></a>, <a href="#set"><code>set</code></a></p>
<h2 id="citp-theory"><code>:theory <op_name> : <arity> -> <coarity> { assoc | comm | id: <term> }</code></h2>
<p>Adds operator theory ‘associativity’, ‘commutativity’, and/or ‘identity’ to an operator specfied by ’<op_name> : <arity> -> <coarity> .</p>
<h2 id="switch-trace"><code>trace [whole]</code> switch</h2>
<p>During evaluation, it is sometimes desirable to see the rewrite sequences, not just the results. Setting the switch <code>trace whole</code> will result in the resultant term of each rewrite step being printed. Setting the switch <code>trace</code> will result in the display of which rule, substitution, and replacement are used.</p>
<h2 id="trans"><code>trans [ <label-exp> ] <term> => <term> .</code></h2>
<p>Defines a transition, which is like an equation but without symmetry.</p>
<p>See <a href="#eq"><code>eq</code></a> for specification of requirements on <code><label-exp></code> and the terms.</p>
<p>Transitions and equations server similar, but different purpose. In particular, reductions (both with or without behavior axioms used) do not take transitions into account. Only <a href="#execute"><code>exec</code></a> also uses transitions. On the other hand, the built-in <a href="#searchpredicate">search predicate</a> searches all possible transitions from a given term.</p>
<h2 id="unprotect"><code>unprotect <module-name></code></h2>
<p>Remove overwrite protection from a module that has been protected with the <code>protect</code> call. Some modules vital for the system are initially protected.</p>
<p>Related: <a href="#protect"><code>protect</code></a></p>
<h2 id="citp-use"><code>:use (<label> ... <label>)</code></h2>
<p>Incorporate discharged goal sentences as new axioms.</p>
<h2 id="using"><code>using ( <modexp> )</code></h2>
<p>Imports the object specified by <code>modexp</code> into the current module without any restrictions on the models. See <a href="#moduleexpression"><code>module expression</code></a> for format of <code>modexp</code>.</p>
<p>Related: <a href="#protecting"><code>protecting</code></a>, <a href="#including"><code>including</code></a>, <a href="#extending"><code>extending</code></a></p>
<h2 id="var"><code>var <var-name> : <sort-name></code></h2>
<p>Declares a variable <code><var-name></code> to be of sort <code><sort-name></code>. The scope of the variable is the current module. Redeclarations of variable names are not allowed. Several variable of the same sort can be declared at the same time using the <code>vars</code> construct:</p>
<p><code>vars <var-name> ... : <sort-name></code></p>
<p>Related: <a href="#onthefly"><code>on-the-fly</code></a>, <a href="#qualified"><code>qualified term</code></a>, <a href="#op"><code>op</code></a></p>
<h2 id="citp-verbose"><code>:verbose { on | off }</code></h2>
<p>Turns on verbose reporting of the CITP subsystem.</p>
<p>Related: <a href="#citp"><code>citp</code></a></p>
<h2 id="switch-verbose"><code>verbose</code> switch</h2>
<p>Possible values: <code>on</code> <code>off</code>, default <code>off</code>.</p>
<p>If turn <code>on</code>, the system is much more verbose in many commands.</p>
<p>Related: <a href="#switch-quiet"><code>quiet switch</code></a></p>
<h2 id="version"><code>version</code></h2>
<p>Prints out the version of CafeOBJ.</p>
<h2 id="view"><code>view <name> from <modname> to <modname> { <viewelems> }</code></h2>
<p>A view specifies ways to bind actual parameters to formal parameters (see <a href="#parameterizedmodule">parameterized module</a>). The view has to specify the mapping of the sorts as well as the operators.</p>
<p>The <code><viewelems></code> is a comma-separated list of expressions specifying these mappings:</p>
<pre><code>sort <sortname> -> <sortname>
hsort <sortname> -> <sortname>
op <opname> -> <opname>
bop <opname> -> <opname></code></pre>
<p>and also can contain variable declarations.</p>
<p>Infix operators are represented as terms containing the operator with either literal underscores <code>_</code>, or variables: <code>_*_</code> or <code>X * Y</code>. The <code><opname></code> can be qualified.</p>
<p>In specifying views some rules can be omitted:</p>
<ol type="1">
<li><p>If the source and target modules have common submodules, all the sorts and modules declared therein are assumed to be mapped to themselves;</p></li>
<li><p>If the source and target modules have sorts and/or operators with identical names, they are mapped to their respective counterparts;</p></li>
<li><p>If the source module has a single sort and the target has a principal sort, the single sort is mapped to the principal sort.</p></li>
</ol>
<h3 id="example-17">Example</h3>
<p>Assume a module <code>MONOID</code> with sort <code>M</code> and ops <code>e</code> and <code>*</code> are given, and another <code>SIMPLE-NAT</code> with sort <code>Nat</code> and operators <code>0</code> and <code>+</code> (with the same arity). Then the following expression constitutes a view:</p>
<pre><code>view NAT-AS-MONOID from MONOID to SIMPLE-NAT {
sort M -> Nat,
op e -> 0,
op _*_ -> _+_
}</code></pre>
</body>
</html>
|
