-
Notifications
You must be signed in to change notification settings - Fork 48
/
Copy pathtop2.html
3924 lines (3717 loc) · 545 KB
/
top2.html
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
<!DOCTYPE html>
<html lang="en">
<head>
<meta http-equiv="Content-Type" content="text/html; charset=US-ASCII">
<meta name="generator" content="hevea 2.36">
<style type="text/css">
.equationcontainer{position:relative;}
.equationnumber{float:right;left:auto;position:absolute;right:0}
.equationnumber-valign{float:right;left:auto;position:absolute;right:0;margin-top:-0.5em;}
.floatrule{background-color: black; border: none; height: 1px; width: 80%}
.phantom{display: inline-block; visibility: hidden}
.hphantom{display: inline-block; height: 0; visibility: hidden}
.vphantom{display: inline-block; visibility: hidden; width: 0}
.smash{display: inline-block; height: 0; line-height: 0}
.li-itemize{margin:1ex 0ex;}
.li-enumerate{margin:1ex 0ex;}
.dd-description{margin:0ex 0ex 1ex 4ex;}
.dt-description{margin:0ex;}
.toc{list-style:none;}
.footnotetext{margin:0ex; padding:0ex;}
div.footnotetext P{margin:0px; text-indent:1em;}
.thefootnotes{text-align:left;margin:0ex;}
.dt-thefootnotes{margin:0em;}
.dd-thefootnotes{margin:0em 0em 0em 2em;}
.footnoterule{background-color: black; border: none; height: 1px; margin: 1em auto 1em 0px; width: 40%}
.caption{padding-left:2ex; padding-right:2ex; margin-left:auto; margin-right:auto}
.title{margin:2ex auto;text-align:center}
.titlemain{margin:1ex 2ex 2ex 1ex;}
.titlerest{margin:0ex 2ex;}
.center{text-align:center;margin-left:auto;margin-right:auto;}
.flushleft{text-align:left;margin-left:0ex;margin-right:auto;}
.flushright{text-align:right;margin-left:auto;margin-right:0ex;}
div table{margin-left:inherit;margin-right:inherit;margin-bottom:2px;margin-top:2px}
td table{margin:auto;}
table{border-collapse:collapse;}
td{padding:0;}
.cellpadding0 tr td{padding:0;}
.cellpadding1 tr td{padding:1px;}
pre{text-align:left;margin-left:0ex;margin-right:auto;}
blockquote{margin-left:4ex;margin-right:4ex;text-align:left;}
td p{margin:0px;}
.quote{margin-left:3em;margin-right:3em;text-align:inherit;text-indent:0pt}
.quotation{margin-left:3em;margin-right:3em;text-align:inherit;text-indent:1.5em}
.verse{margin-left:3em;margin-right:3em;text-indent:1.5em hanging each-line}
.parbox{box-sizing: border-box;
display: inline-block;
text-indent: 0;
}
.rule-rect{fill: black;}
.lrbox{box-sizing:border-box;display:inline-block;overflow:visible;white-space:nowrap;}
.center-lrbox{display:inline-block;margin-left:50%;transform:translateX(-50%);}
.makebox{}
.framebox{border:1px solid black;padding:0.25em;}
.vertical-rule{border:none;width:2px;background-color:black;}
.horizontal-rule{border:none;background-color:black;}
.hrule{border:none;height:2px;width:100%;background-color:black;}
.hfill{border:none;height:1px;width:200%;background-color:black;}
.vdisplay{border-collapse:separate;border-spacing:2px;line-height:1.1;width:auto; empty-cells:show; border:2px solid red;}
.vdcell{white-space:nowrap;padding:0px; border:2px solid green;}
.display{border-collapse:separate;border-spacing:2px;line-height:1.1;width:auto; border:none;}
.dcell{white-space:nowrap;padding:0px; border:none;}
.dcenter{margin:0ex auto;}
.vdcenter{border:solid #FF8000 2px; margin:0ex auto;}
.minipage{text-align:left; margin-left:0em; margin-right:auto;}
.marginpar{border:solid thin black; margin-bottom:1ex; width:20%; text-align:left;}
.marginparleft{float:left; clear:left; margin-left:0ex; margin-right:1ex;}
.marginparright{float:right; clear:right; margin-left:1ex; margin-right:0ex;}
.theorem{text-align:left;margin:1ex auto 1ex 0ex;}
.part{margin:2ex auto;text-align:center}
</style>
<title>Ott: Tool Support for
Semantics
User Guide
version 0.34
</title>
</head>
<body >
<!--HEVEA command line is: hevea -fix top2 -->
<!--CUT STYLE article--><!--CUT DEF section 1 --><table class="title"><tr><td style="padding:1ex"><h1 class="titlemain">Ott: Tool Support for
Semantics <br>
User Guide<br>
version 0.34
</h1><h3 class="titlerest">Peter Sewell<sup>*</sup>   Francesco Zappa Nardelli<sup>**</sup>   Scott Owens <sup>*</sup> <br>
with Gilles Peskine<sup>*</sup>, Tom
Ridge<sup>*</sup>,<br>
Susmit Sarkar<sup>*</sup>, and Rok Strniša<sup>*</sup><br>
<sup>*</sup>University of Cambridge   <sup>**</sup>INRIA</h3></td></tr>
</table><!--TOC section id="sec1" <span style="font-size:small">Contents</span>-->
<h2 id="sec1" class="section"><span style="font-size:small">Contents</span></h2><!--SEC END --><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec2"><span style="font-size:small">1 Introduction</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec3"><span style="font-size:small">2 Getting started with Ott (the README)</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec4"><span style="font-size:small">2.1 Documentation</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec5"><span style="font-size:small">2.2 Papers</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec6"><span style="font-size:small">2.3 People</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec7"><span style="font-size:small">2.4 To install and build</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec8"><span style="font-size:small">2.4.1 With opam (released
version)</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec9"><span style="font-size:small">2.4.2 With opam (github
checkout)</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec10"><span style="font-size:small">2.4.3 Without opam</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec11"><span style="font-size:small">2.5 To run</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec12"><span style="font-size:small">2.6 Editor Plugins</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec13"><span style="font-size:small">2.6.1 Emacs mode</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec14"><span style="font-size:small">2.6.2 Visual Studio Code</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec15"><span style="font-size:small">2.7 Mailing lists</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec16"><span style="font-size:small">2.8 Bug Tracker</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec17"><span style="font-size:small">2.9 Directory contents</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec18"><span style="font-size:small">2.10 Examples</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec19"><span style="font-size:small">2.11 Copyright information</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec20"><span style="font-size:small">3 A minimal Ott source file: the untyped CBV lambda calculus</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec21"><span style="font-size:small">3.1 Index variables</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec22"><span style="font-size:small">4 Generating LaTeX</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec23"><span style="font-size:small">4.1 Specifying LaTeX for productions</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec24"><span style="font-size:small">4.2 Specifying LaTeX for grammar rules</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec25"><span style="font-size:small">4.3 Using the LaTeX code</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec26"><span style="font-size:small">5 Generating proof assistant definitions</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec27"><span style="font-size:small">5.1 Proof assistant code for grammar rules</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec28"><span style="font-size:small">5.2 Proof assistant code for inductive definitions</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec29"><span style="font-size:small">5.3 Representation of binding</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec30"><span style="font-size:small">5.4 Helper functions for free variable and substitution functions</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec31"><span style="font-size:small">5.5 Correctness of the generated proof assistant code</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec32"><span style="font-size:small">5.6 Using the generated proof assistant code</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec33"><span style="font-size:small">5.6.1 Coq</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec34"><span style="font-size:small">5.6.2 HOL</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec35"><span style="font-size:small">5.6.3 Isabelle</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec36"><span style="font-size:small">6 Judgments and formulae</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec37"><span style="font-size:small">6.1 Naming of premises for the Coq backend</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec38"><span style="font-size:small">6.2 In-line embedded prover code in premises</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec39"><span style="font-size:small">6.3 User syntax</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec40"><span style="font-size:small">7 Concrete terms and OCaml generation</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec41"><span style="font-size:small">8 Filtering: Using Ott syntax within LaTeX, Coq, Isabelle,
HOL, or OCaml</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec42"><span style="font-size:small">8.1 Filtering embedded code</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec43"><span style="font-size:small">8.2 Filtering files</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec44"><span style="font-size:small">9 Binding specifications</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec45"><span style="font-size:small">10 Generating substitution and free variable functions</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec46"><span style="font-size:small">11 Locally-nameless representation</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec47"><span style="font-size:small">12 List forms</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec48"><span style="font-size:small">12.1 List dot forms</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec49"><span style="font-size:small">12.2 List comprehension forms</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec50"><span style="font-size:small">12.3 Proof assistant code for list forms</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec51"><span style="font-size:small">12.3.1 Types</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec52"><span style="font-size:small">12.3.2 Terms (in inductive definition rules)</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec53"><span style="font-size:small">12.3.3 List forms in homomorphisms</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec54"><span style="font-size:small">13 Subrules</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec55"><span style="font-size:small">14 Context rules</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec56"><span style="font-size:small">15 Auxiliary Rules</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec57"><span style="font-size:small">16 Functions</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec58"><span style="font-size:small">17 Parsing Priorities</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec59"><span style="font-size:small">18 Combining multiple source files</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec60"><span style="font-size:small">19 Hom blocks</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec61"><span style="font-size:small">20 Isabelle syntax support</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec62"><span style="font-size:small">21 Isabelle code generation example</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec63"><span style="font-size:small">22 Reference: Command-line usage</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec64"><span style="font-size:small">23 Reference: The language of symbolic terms</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec65"><span style="font-size:small">24 Reference: Generation of proof assistant definitions</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec66"><span style="font-size:small">24.1 Generation of types</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec67"><span style="font-size:small">24.2 Generation of functions</span></a><span style="font-size:small">
</span><ul class="toc"><li class="li-toc"><span style="font-size:small">
</span><a href="#sec68"><span style="font-size:small">24.2.1 Subrule predicates</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec69"><span style="font-size:small">24.2.2 Binding auxiliaries</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec70"><span style="font-size:small">24.2.3 Free variables</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec71"><span style="font-size:small">24.2.4 Substitutions</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec72"><span style="font-size:small">24.3 Generation of relations</span></a><span style="font-size:small">
</span></li></ul><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec73"><span style="font-size:small">25 Reference: Summary of homomorphisms</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec74"><span style="font-size:small">26 Reference: The Ott source grammar</span></a><span style="font-size:small">
</span></li><li class="li-toc"><a href="#sec75"><span style="font-size:small">27 Reference: Examples</span></a><span style="font-size:small">
</span></li></ul>
<!--TOC section id="sec2" Introduction-->
<h2 id="sec2" class="section">1 Introduction</h2><!--SEC END --><p><a id="a1"></a>Ott is a tool for writing definitions of programming languages and
calculi.
It takes as input a definition of a language syntax and semantics, in
a concise and readable ASCII notation that is close to what one would
write in informal mathematics. It generates output:
</p><ol class="enumerate" type=1><li class="li-enumerate">a LaTeX source file that defines commands to build a typeset version of
the definition;
</li><li class="li-enumerate">a Coq version of the definition;
</li><li class="li-enumerate">a HOL version of the definition;
</li><li class="li-enumerate">an Isabelle/HOL version of the definition;
</li><li class="li-enumerate">a Lem version of the definition;
</li><li class="li-enumerate">an OCaml version of the syntax of the definition.
</li></ol><p>
Additionally, it can be run as a filter, taking a
LaTeX/Coq/Isabelle/HOL/Lem/OCaml source file
with embedded (symbolic) terms of the defined language, parsing them and replacing
them by typeset terms.</p><p>This document is a user guide for the tool. The papers
</p><ul class="itemize"><li class="li-itemize"><a href="http://www.cl.cam.ac.uk/users/pes20/ott/ott-jfp.pdf">Ott: Effective Tool Support for the Working Semanticist</a>. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles
Peskine, Thomas Ridge, Susmit Sarkar, Rok Strniša.
Journal of Functional Programming 20(1):71-122, 2010 [<a href="#ott-jfp"></a>].</li><li class="li-itemize"><a href="http://www.cl.cam.ac.uk/users/pes20/ott/paper.pdf">Ott: Effective Tool Support for the Working Semanticist</a>. Peter Sewell, Francesco Zappa Nardelli, Scott Owens, Gilles
Peskine, Thomas Ridge, Susmit Sarkar, Rok Strniša.
ICFP’07 [<a href="#ott-sub"></a>].</li></ul><p>
give an overview of the project, including discussion of motivation,
design decisions, and related work, and one should look at that together
with this manual. The project web page
</p><blockquote class="quotation">
<a href="http://www.cl.cam.ac.uk/users/pes20/ott/"><span style="font-family:monospace">http://www.cl.cam.ac.uk/users/pes20/ott/</span></a>
</blockquote><p>
links to the github source repository, with a
BSD-style licence. It also has a range of examples, including
untyped and simply typed CBV lambda calculus, ML polymorphism, various
first-order systems from Pierce’s TAPL [<a href="#Pierce%3ATypeSystems"></a>], the
POPLmark F<sub><:</sub> language [<a href="#poplmark"></a>], a module system by
Leroy [<a href="#Leroy-generativity"></a>, §4] (extended with a term language and an
operational semantics), the LJ Java fragment and LJAM Java module
system [<a href="#ljam-sub"></a>], and a substantial fragment of OCaml.</p><p>Our main goal is to support work on large programming language
definitions, where the scale makes it hard to keep a definition
internally consistent, and hard to keep a tight correspondence between a
definition and implementations.
We also wish to ease rapid prototyping work with smaller calculi,
and to make it easier to exchange definitions and definition fragments
between groups.
Most simply, the tool can be used to aid completely informal LaTeX mathematics.
Here it permits the definition, and terms within proofs and
exposition, to be written in a clear, editable, ASCII notation, without LaTeX
noise. It generates good-quality typeset output.
By parsing (and so sort-checking) this input, it quickly catches a
range of simple errors, e.g. inconsistent use of judgement forms or
metavariable naming conventions.
That same input, extended with some additional data, can be used to generate formal definitions for
Coq, HOL, Isabelle, and Lem. It should thereby enable a smooth transition
between use of informal and formal mathematics. Further, the
tool can automatically generate definitions of functions for free
variables, single and multiple substitutions, subgrammar checks
(e.g. for value subgrammars), and binding auxiliary functions.
Ott supports a ‘fully concrete’ representation, sufficient
for many examples but not dealing with general alpha equivalence.
An experimental Coq backend generates definitions in locally-nameless style for a subset of the Ott metalanguage.
The OCaml backend
generates type definitions that may be useful for developing a complete
implementation of the language, together with the functions listed
above. It does not generate anything for inductively defined relations
(the various proof-assistant code extraction facilities can
sometimes be used for that).
Our focus here is on the problem of writing and editing language
definitions, not (directly) on aiding mechanized proof of metatheory. If one
is involved in hard proofs about a relatively stable small calculus
then it will aid only a small part of the work (and one might choose
instead to work just within a single proof assistant), but for larger
languages the definition is a more substantial problem — so much so
that only a handful of full-scale languages have been given complete definitions. We
aim to make this more commonplace, less of a heroic task.</p><p><a id="ott"></p>
<!--TOC section id="sec3" Getting started with Ott (the README)-->
<h2 id="sec3" class="section">2 Getting started with Ott (the README)</h2><!--SEC END --><p></a></p><p>Ott is a tool for writing definitions of programming languages and
calculi. It takes as input a definition of a language syntax and
semantics, in a concise and readable ASCII notation that is close to
what one would write in informal mathematics. With appropriate
annotations, it can then generate output:</p><ul class="itemize"><li class="li-itemize">a LaTeX source file that defines commands to build a typeset version
of the definition;
</li><li class="li-itemize">a Coq version of the definition;
</li><li class="li-itemize">a HOL version of the definition;
</li><li class="li-itemize">an Isabelle/HOL version of the definition;
</li><li class="li-itemize">a Lem version of the definition;
</li><li class="li-itemize">an OCaml version of the syntax of the definition; and
</li><li class="li-itemize">(experimental) a menhir parser and crude pretty printer for the
syntax.
</li></ul><p>Additionally, it can be run as a filter, taking a
LaTeX/Coq/Isabelle/HOL/Lem/OCaml source file with embedded (symbolic)
terms of the defined language, parsing them and replacing them by
typeset terms.</p><p>Most simply, Ott can be used to aid informal LaTeX mathematics. Here it
permits the definition, and terms within proofs and exposition, to be
written in a clear, editable, ASCII notation, without LaTeX noise. It
generates good-quality typeset output. By parsing (and so sort-checking)
this input, it quickly catches a range of simple errors,
e.g. inconsistent use of judgement forms or metavariable naming
conventions.</p><p>That same input can be used to generate formal definitions, for Coq,
HOL, Isabelle, and Lem. It should thereby enable a smooth transition
between use of informal and formal mathematics. Additionally, the tool
can automatically generate definitions of functions for free variables,
single and multiple substitutions, subgrammar checks (e.g. for value
subgrammars), and binding auxiliary functions. At present only a fully
concrete representation of binding, without quotienting by alpha
equivalence, is fully supported. An experimental backend generates a
locally-nameless representation of terms for a subset of the Ott
metalanguage: details can be found at
http://moscova.inria.fr/~zappa/projects/ln_ott.</p><p>The distribution includes several examples, in varying levels of
completeness: untyped and simply typed lambda-calculus, a calculus with
ML polymorphism, the POPLmark Fsub with and without records, an ML
module system taken from (Leroy, JFP 1996) and equipped with an
operational semantics, and LJ, a lightweight Java fragment. More
substantially, Ott has been used for work on iJAM and LJAM, Java Module
Systems, by Rok Strnisa, and semantics for OCaml light, by Scott Owens.</p><p>As of 2024, Ott remains in continuous use.</p><p><a id="documentation"></p>
<!--TOC subsection id="sec4" Documentation-->
<h3 id="sec4" class="subsection">2.1 Documentation</h3><!--SEC END --><p></a></p><ul class="itemize"><li class="li-itemize">the manual is in the <a href="https://github.com/ott-lang/ott">Ott
github</a> built_doc directory, or
<a href="http://www.cl.cam.ac.uk/ pes20/ott/top2.html">here (html)</a>
</li><li class="li-itemize"><a href="http://www.cl.cam.ac.uk/users/pes20/ott/bind-doc.pdf">Binding
and Substitution</a>. Susmit Sarkar, Peter Sewell, Francesco Zappa
Nardelli. Note, 2007.
</li><li class="li-itemize"><a href="http://moscova.inria.fr/ zappa/projects/ln_ott">The experimental
Coq locally-nameless backend (html)</a>. Francesco Zappa Nardelli. Note,
2009.
</li></ul><p><a id="papers"></p>
<!--TOC subsection id="sec5" Papers-->
<h3 id="sec5" class="subsection">2.2 Papers</h3><!--SEC END --><p></a></p><ul class="itemize"><li class="li-itemize"><a href="http://www.cl.cam.ac.uk/users/pes20/ott/ott-jfp.pdf">Ott:
Effective Tool Support for the Working Semanticist</a>. Peter Sewell,
Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge,
Susmit Sarkar, Rok Strnisa.
<a href="http://journals.cambridge.org/repo_A71Keeig">Journal of
Functional Programming 20(1):71-122, 2010</a>
</li><li class="li-itemize"><a href="http://www.cl.cam.ac.uk/users/pes20/ott/paper.pdf">Ott:
Effective Tool Support for the Working Semanticist</a>. Peter Sewell,
Francesco Zappa Nardelli, Scott Owens, Gilles Peskine, Thomas Ridge,
Susmit Sarkar, Rok Strnisa. In
<a href="http://www.informatik.uni-bonn.de/%7Eralf/icfp07.html">ICFP
2007</a>
</li><li class="li-itemize"><a href="http://www.cl.cam.ac.uk/users/pes20/ott/wmm2010.pdf">Ott or
Nott</a>. Stephanie Weirich, Scott Owens, Peter Sewell, Francesco Zappa
Nardelli. In <a href="http://www.cis.upenn.edu/ bcpierce/wmm/">WMM 2010</a>:
5th ACM SIGPLAN Workshop on Mechanizing Metatheory.
</li></ul><p><a id="people"></p>
<!--TOC subsection id="sec6" People-->
<h3 id="sec6" class="subsection">2.3 People</h3><!--SEC END --><p></a></p><p>Ott has been principally developed by Peter Sewell, Francesco Zappa
Nardelli, and Scott Owens, with contributions from many others including
Joey Eremondi, Hannes Mehnert, Karl Palmskog, Matthew Parkinson, Thibaut
Perami, Gilles Peskine, Alastair Reid, Tom Ridge, Susmit Sarkar, Rok
Strnisa, Viktor Vafeiadis.</p><p><a id="to-install-and-build"></p>
<!--TOC subsection id="sec7" To install and build-->
<h3 id="sec7" class="subsection">2.4 To install and build</h3><!--SEC END --><p></a></p><p>Ott is available as an <a href="https://opam.ocaml.org">opam</a> package and a
<a href="https://github.com/ott-lang/ott">github repo</a>.</p><p><a id="with-opam-released-version"></p>
<!--TOC subsubsection id="sec8" With opam (released
version)-->
<h4 id="sec8" class="subsubsection">2.4.1 With opam (released
version)</h4><!--SEC END --><p></a></p><p>First, ensure you have opam (the OCaml package manager) installed,
version 2.0 or greater (opam 1 versions of ott are no longer supported).
You can use your system’s package manager
e.g. <span style="font-family:monospace">sudo apt-get install opam</span> (e.g. on Ubuntu 20.04) or
follow the <a href="https://opam.ocaml.org/doc/Install.html">instructions
from the opam website</a>. On older Ubuntu versions you will not be able to
use their package manager’s opam 1 version, and will need to install
opam 2 following the instructions on the opam website.</p><p>Then <span style="font-family:monospace">opam install ott</span> will install the latest Ott version.
The Emacs mode will be in
<span style="font-family:monospace">$(opam config var prefix)/share/emacs/site-lisp</span>, and
documentation in <span style="font-family:monospace">$(opam config var prefix)/doc/ott</span>.</p><p>If you want to use Ott with the Coq proof assistant, to install the Ott
auxiliary files for Coq, first activate the <span style="font-family:monospace">coq-released</span> OPAM
repository:</p><p><span style="font-family:monospace">opam repo add coq-released https://coq.inria.fr/opam/released</span></p><p>and then run <span style="font-family:monospace">opam install coq-ott</span>.</p><p><a id="with-opam-github-checkout"></p>
<!--TOC subsubsection id="sec9" With opam (github
checkout)-->
<h4 id="sec9" class="subsubsection">2.4.2 With opam (github
checkout)</h4><!--SEC END --><p></a></p><p>In the checkout directory, run <span style="font-family:monospace">opam pin add ott .</span>.</p><p>To rebuild and reinstall after local changes, run
<span style="font-family:monospace">opam upgrade --working-dir ott</span> (or
<span style="font-family:monospace">opam upgrade -w ott</span>).</p><p><a id="without-opam"></p>
<!--TOC subsubsection id="sec10" Without opam-->
<h4 id="sec10" class="subsubsection">2.4.3 Without opam</h4><!--SEC END --><p></a></p><p>Ott depends on OCaml version 4.07.0 or later and the ocamlgraph package.
It builds with (at least) OCaml 4.07.0 and 4.14.0, and ocamlgraph 1.8.8.</p><p>The command <span style="font-family:monospace">make</span> (<span style="font-family:monospace">make world</span>) builds the <span style="font-family:monospace">ott</span>
binary in the <span style="font-family:monospace">bin/</span> subdirectory.</p><p>This will compile Ott using <span style="font-family:monospace">ocamlopt</span>. To force it to compile
with <span style="font-family:monospace">ocamlc</span> (which may give significantly slower execution of
Ott), do <span style="font-family:monospace">make world.byt</span>.</p><p>To build the Ott auxiliary files for Coq, go to the <span style="font-family:monospace">coq/</span>
subdirectory and run <span style="font-family:monospace">make</span>. To install the resulting files in
Coq’s <span style="font-family:monospace">user-contrib</span>, run <span style="font-family:monospace">make install</span>.</p><p><a id="to-run"></p>
<!--TOC subsection id="sec11" To run-->
<h3 id="sec11" class="subsection">2.5 To run</h3><!--SEC END --><p></a></p><p>Ott runs as a command-line tool. Executing <span style="font-family:monospace">ott</span> shows the usage
and options. To run Ott on the test file <span style="font-family:monospace">tests/test10.ott</span>,
generating LaTeX in <span style="font-family:monospace">test10.tex</span> and Coq in <span style="font-family:monospace">test10.v</span>,
type:</p><p><span style="font-family:monospace">ott -i tests/test10.ott -o test10.tex -o test10.v</span></p><p>Isabelle, HOL, and Lem can be generated with options
<span style="font-family:monospace">-o test10.thy</span>, <span style="font-family:monospace">-o test10Script.sml</span>, and
<span style="font-family:monospace">-o test10.lem</span>, respectively.</p><p>The Makefile has various sample targets,
<span style="font-family:monospace">make tests/test10.out</span>, <span style="font-family:monospace">make test7</span>, etc. Typically
they generate:</p><p>
</p><blockquote class="table"><div class="center"><hr class="floatrule"></div><div class="center"><table style="border-spacing:6px;border-collapse:separate;" class="cellpading0"><tr><td style="text-align:left;white-space:nowrap" >
filename</td><td style="text-align:left;white-space:nowrap" >description </td></tr>
<tr><td style="text-align:left;white-space:nowrap" > </td></tr>
<tr><td style="text-align:left;white-space:nowrap" ><span style="font-family:monospace">out.tex</span></td><td style="text-align:left;white-space:nowrap" >LaTeX source for a definition </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">out.ps</span></td><td style="text-align:left;white-space:nowrap" >the postscript built from that </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">out.v</span></td><td style="text-align:left;white-space:nowrap" >Coq source </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">outScript.sml</span></td><td style="text-align:left;white-space:nowrap" >HOL source </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">out.thy</span></td><td style="text-align:left;white-space:nowrap" >Isabelle source </td></tr>
<tr><td style="text-align:left;white-space:nowrap" > </td></tr>
</table>
</div><div class="center"><hr class="floatrule"></div></blockquote><p>from files <span style="font-family:monospace">test10.ott</span>, <span style="font-family:monospace">test8.ott</span>, etc., in
<span style="font-family:monospace">tests/</span>.</p><p><a id="editor-plugins"></p>
<!--TOC subsection id="sec12" Editor Plugins-->
<h3 id="sec12" class="subsection">2.6 Editor Plugins</h3><!--SEC END --><p></a></p><p><a id="emacs-mode"></p>
<!--TOC subsubsection id="sec13" Emacs mode-->
<h4 id="sec13" class="subsubsection">2.6.1 Emacs mode</h4><!--SEC END --><p></a></p><p>The file <span style="font-family:monospace">emacs/ott-mode.el</span> defines a very simple Emacs mode for
syntax highlighting of Ott source files. It can be used by, for example,
adding the following to your <span style="font-family:monospace">.emacs</span> file, replacing
<span style="font-family:monospace">PATH</span> by a path to your Ott Emacs directory.</p><pre class="verbatim">(setq load-path (cons (expand-file-name "PATH") load-path))
(require 'ott-mode)
</pre><p>For installations using opam on *nix systems, it is sufficient to use
the following code, which will call <span style="font-family:monospace">opam config var prefix</span>
at load-time.</p><pre class="verbatim">(setq opam-share (substring (shell-command-to-string "opam config var share") 0 -1))
(add-to-list 'load-path (concat opam-share "/emacs/site-lisp"))
(require 'ott-mode)
</pre><p><a id="visual-studio-code"></p>
<!--TOC subsubsection id="sec14" Visual Studio Code-->
<h4 id="sec14" class="subsubsection">2.6.2 Visual Studio Code</h4><!--SEC END --><p></a></p><p>There is a
<a href="https://marketplace.visualstudio.com/items?itemName=JoeyEremondi.ott">plugin
for VSCode</a>, which features syntax highlighting and inline error
reporting.</p><p><a id="mailing-lists"></p>
<!--TOC subsection id="sec15" Mailing lists-->
<h3 id="sec15" class="subsection">2.7 Mailing lists</h3><!--SEC END --><p></a></p><ul class="itemize"><li class="li-itemize"><a href="https://lists.cam.ac.uk/mailman/listinfo/cl-ott-announce">cl-ott-announce
announcement mailing list</a>
</li><li class="li-itemize"><a href="https://lists.cam.ac.uk/mailman/listinfo/cl-ott-discuss">cl-ott-discuss
discussion mailing list</a>
</li></ul><p><a id="bug-tracker"></p>
<!--TOC subsection id="sec16" Bug Tracker-->
<h3 id="sec16" class="subsection">2.8 Bug Tracker</h3><!--SEC END --><p></a></p><ul class="itemize"><li class="li-itemize">Please now use the github issue tracker (though our resources for
fixing issues are very limited)
</li><li class="li-itemize">The previous issue tracker is here
</li></ul><p><a id="directory-contents"></p>
<!--TOC subsection id="sec17" Directory contents-->
<h3 id="sec17" class="subsection">2.9 Directory contents</h3><!--SEC END --><p></a></p><p>
</p><blockquote class="table"><div class="center"><hr class="floatrule"></div><div class="center"><table style="border-spacing:6px;border-collapse:separate;" class="cellpading0"><tr><td style="text-align:left;white-space:nowrap" >
directory</td><td style="text-align:left;white-space:nowrap" >description </td></tr>
<tr><td style="text-align:left;white-space:nowrap" > </td></tr>
<tr><td style="text-align:left;white-space:nowrap" ><span style="font-family:monospace">bin/</span></td><td style="text-align:left;white-space:nowrap" >the Ott binary </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">built_doc/</span></td><td style="text-align:left;white-space:nowrap" >the user guide, in html, pdf, and ps </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">coq/</span></td><td style="text-align:left;white-space:nowrap" >auxiliary files for Coq </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">doc/</span></td><td style="text-align:left;white-space:nowrap" >the user guide sources </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">emacs/</span></td><td style="text-align:left;white-space:nowrap" >an Ott Emacs mode </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">examples/</span></td><td style="text-align:left;white-space:nowrap" >some larger example Ott files </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">tex/</span></td><td style="text-align:left;white-space:nowrap" >auxiliary files for LaTeX </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">hol/</span></td><td style="text-align:left;white-space:nowrap" >auxiliary files for HOL </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">menhir/</span></td><td style="text-align:left;white-space:nowrap" >auxiliary files for menhir </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">regression/</span></td><td style="text-align:left;white-space:nowrap" >regression-test machinery </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">tests/</span></td><td style="text-align:left;white-space:nowrap" >various small example Ott files </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">tools/</span></td><td style="text-align:left;white-space:nowrap" >auxiliary code (y2l) used to build the user guide </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">src/</span></td><td style="text-align:left;white-space:nowrap" >the (OCaml) Ott sources </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">Makefile</span></td><td style="text-align:left;white-space:nowrap" >a Makefile for the examples </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">LICENCE</span></td><td style="text-align:left;white-space:nowrap" >the BSD-style licence terms </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">README.md</span></td><td style="text-align:left;white-space:nowrap" >this file (Section 2 of the user guide) </td></tr>
<tr><td style="text-align:left;white-space:nowrap" >
<span style="font-family:monospace">revisionhistory.txt</span></td><td style="text-align:left;white-space:nowrap" >the revision history </td></tr>
<tr><td style="text-align:left;white-space:nowrap" > </td></tr>
</table>
</div><div class="center"><hr class="floatrule"></div></blockquote><p><a id="examples"></p>
<!--TOC subsection id="sec18" Examples-->
<h3 id="sec18" class="subsection">2.10 Examples</h3><!--SEC END --><p></a></p><p>The following LaTeX, Coq, HOL, and Isabelle files, except the proof
scripts, are all automatically generated from the Ott sources.</p><p>System</p><p>Rules</p><p>Ott sources</p><p>Latex</p><p>Typeset</p><p>Dot</p><p>Coq</p><p>HOL</p><p>Isabelle</p><p>Defn</p><p>Proof</p><p>Defn</p><p>Proof</p><p>Defn</p><p>Proof</p><p>Untyped CBV lambda</p><p>3</p><p>test10.ott</p><p>test10.tex</p><p>(ps)</p><p>test10.v</p><p>test10Script.sml</p><p>test10.thy</p><p>Simply typed CBV lambda</p><p>6</p><p>test10st.ott</p><p>test10st.tex</p><p>(ps)</p><p>test10st.v</p><p>test10st_metatheory.v</p><p>test10stScript.sml</p><p>test10st_metatheoryScript.sml</p><p>test10st.thy</p><p>test10st_metatheory.thy</p><p>ML polymorphism</p><p>22</p><p>test8.ott</p><p>test8.tex</p><p>(ps)</p><p>test8.v</p><p>test8Script.sml</p><p>test8.thy</p><p>TAPL roughly-full-simple</p><p>63</p><p>(sources)</p><p>(ps)</p><p>(Coq (including records))</p><p>(HOL)</p><p>(script)</p><p>(Isabelle)</p><p>(script)</p><p>POPLmark Fsub (*)</p><p>48</p><p>(sources)</p><p>(latex)</p><p>(pdf)   (ps)</p><p>Leroy JFP96 module system (*)</p><p>67</p><p>leroy-jfp96.ott</p><p>(latex)</p><p>(ps)</p><p>(HOL)</p><p>LJ: Lightweight Java</p><p>85</p><p>(sources)</p><p>(pdf)</p><p>(Isabelle)</p><p>(zip)</p><p>LJAM: Java Module System</p><p>163</p><p>(sources)</p><p>(pdf)</p><p>(Isabelle)</p><p>(zip)</p><p>OCaml light</p><p>310</p><p>(sources)</p><p>(ps)</p><p>(ps)</p><p>(Coq)</p><p>(HOL)</p><p>(scripts)</p><p>(Isabelle)</p><p>(*) These systems would need explicit alpha conversion in the rules to
capture the intended semantics using the fully concrete representation.</p><p><a id="copyright-information"></p>
<!--TOC subsection id="sec19" Copyright information-->
<h3 id="sec19" class="subsection">2.11 Copyright information</h3><!--SEC END --><p></a></p><p>Files are distributed under the BSD-style licence in LICENCE.
</p>
<!--TOC section id="sec20" A minimal Ott source file: the untyped CBV lambda calculus-->
<h2 id="sec20" class="section">3 A minimal Ott source file: the untyped CBV lambda calculus</h2><!--SEC END --><p><a id="a51"></a>Fig. <a href="#a45">1</a> shows an Ott source file for an untyped call-by-value
(CBV) lambda calculus. This section explains the basic features that
appear there, while in the following sections we show what must be
added to generate typeset output, proof assistant definitions, and
other things.
</p><blockquote class="figure"><div class="center"><hr class="floatrule"></div>
<span class="lrbox framebox"><div class="minipage"><span style="font-size:small">
</span><pre><span style="font-size:small">
% minimal
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">metavar</span></span></span><span style="font-size:small"> termvar</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">,</span></span></span><span style="font-size:small"> x </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">grammar</span></span></span><span style="font-size:small">
t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> ’t_’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> x </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Var
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small"> x . t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Lam
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> t t’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> App
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> ( t ) </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">S</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Paren
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">{</span></span><span style="font-size:small"> t / x </span><span style="font-size:small"><span style="font-family:monospace">}</span></span><span style="font-size:small"> t’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">M</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Tsub
v </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> ’v_’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small"> x . t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Lam
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">subrules</span></span></span><span style="font-size:small">
v </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"><::</span></span></span><span style="font-size:small"> t
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">defns</span></span></span><span style="font-size:small">
Jop </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> ” </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">defn</span></span></span><span style="font-size:small">
t1 --> t2 </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small">reduce</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small">” </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">by</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"> --------------------------</span></span></span><span style="font-size:small"> :: ax_app
(</span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small">x.t12) v2 --> </span><span style="font-size:small"><span style="font-family:monospace">{</span></span><span style="font-size:small">v2/x</span><span style="font-size:small"><span style="font-family:monospace">}</span></span><span style="font-size:small">t12
t1 --> t1’
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"> --------------</span></span></span><span style="font-size:small"> :: ctx_app_fun
t1 t --> t1’ t
t1 --> t1’
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"> --------------</span></span></span><span style="font-size:small"> :: ctx_app_arg
v t1 --> v t1’
</span></pre><span style="font-size:small">
</span></div></span>
<div class="caption"><table style="border-spacing:6px;border-collapse:separate;" class="cellpading0"><tr><td style="vertical-align:top;text-align:left;" >Figure 1: Source: <span style="font-family:monospace">test10.0.ott</span><a id="a45"></a></td></tr>
</table></div>
<div class="center"><hr class="floatrule"></div></blockquote><p>
The figure is colourised, with Ott keywords like <span style="color:#A51815"><span style="font-family:monospace">this</span></span> and Ott
symbols such as <span style="color:#007FFF"><span style="font-family:monospace">|</span></span> and <span style="color:#007FFF"><span style="font-family:monospace">::</span></span>. Other user-specific input
appears like <span style="font-family:monospace">this</span>. Any text between % and the next newline is
discarded as a comment.</p><p>At the top of the figure, the <span style="color:#A51815"><span style="font-family:monospace">metavar</span></span> declaration introduces
a sort of <em>metavariables</em> <span style="font-family:monospace">termvar</span> (with synonym <span style="font-family:monospace">x</span>), for term
variables.
The following <span style="color:#A51815"><span style="font-family:monospace">grammar</span></span> introduces two grammar rules, one for terms, with
<em>nonterminal root</em>
<span style="font-family:monospace">t</span>, and one for values <span style="font-family:monospace">v</span>.
This specifies the concrete syntax of object-language terms,
the abstract syntax representations for proof-assistant mathematics,
and the syntax of symbolic terms to be used in semantic rules.</p><p>Each rule has a rule name prefix (e.g. <span style="font-family:monospace">’t_’</span>) and then a list
of productions. Each production, e.g.
</p><pre>
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> <span style="font-family:monospace">\</span> x . t <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> Lam
</pre><p>
specifies a syntactic form as a list of elements, here ‘<code class="verb">\</code>’,
‘<code class="verb">x</code>’, ‘<code class="verb">.</code>’, and ‘<code class="verb">t</code>’, each of which is either a
metavariable (the ‘<code class="verb">x</code>’), a nonterminal (the ‘<code class="verb">t</code>’), or a
terminal
(<span style="font-family:monospace">\</span> <span style="font-family:monospace">.</span> <span style="font-family:monospace">(</span> <span style="font-family:monospace">)</span> <span style="font-family:monospace">{</span> <span style="font-family:monospace">}</span> <span style="font-family:monospace">/</span> <span style="font-family:monospace">--></span>).
Within productions all elements must be whitespace-separated, so that
the tool can deduce which are terminals. In the symbolic terms in
the semantic rules below, however, whitespace is required only where necessary.
A few terminals have to be quoted (with <code class="verb">''</code>) if they appear in a grammar, e.g. to
use <span style="font-family:monospace">|</span> as an object-language token, as they are part of the Ott syntax, but they
do not have to be quoted at usage points.
(If one accidentally omits inter-token whitespace in the grammar, the
output of Ott can be surprising. This is best diagnosed by looking at
the colourised ASCII or LaTeX output from Ott.)</p><p>Metavariables and nonterminals can be formed from the specified
metavariable and nonterminal roots by appending a suffix, e.g. the
nonterminal <code class="verb">t'</code> in the <code class="verb">App</code> and <code class="verb">Tsub</code> productions. </p><p>Between the <span style="color:#007FFF"><span style="font-family:monospace">::</span></span>’s is an optional meta flag <span style="color:#A51815"><span style="font-family:monospace">M</span></span> or <span style="color:#A51815"><span style="font-family:monospace">S</span></span>. Non-meta
productions give rise to clauses of datatype definitions in the
Isabelle/Coq/HOL output, whereas meta productions do not. Later, we
will see how the user can specify how meta syntax should be translated
away when generating proof assistant output. The two flags <span style="color:#A51815"><span style="font-family:monospace">M</span></span>
and <span style="color:#A51815"><span style="font-family:monospace">S</span></span> are identical except that productions with the latter are
admitted when parsing example concrete terms; the <span style="color:#A51815"><span style="font-family:monospace">S</span></span> tag is thus
appropriate for lightweight syntactic sugar, such as productions for
parentheses. One can also use another flag, e.g. <span style="color:#A51815"><span style="font-family:monospace">X</span></span>, along with the command-line option <code class="verb">-tex_suppress_category</code>, to suppress
productions in the generated LaTeX.</p><p>Each production has a production name (e.g. <code class="verb">t_Lam</code>), composed of
the rule name prefix (here <code class="verb">t_</code>) and the production name kernel
that follows the <span style="color:#007FFF"><span style="font-family:monospace">::</span></span>’s (here <code class="verb">Lam</code>). The production name is
used as a constructor name in the generated Isabelle/Coq/HOL. </p><p>The tool supports arbitrary context-free grammars, extended with
special constructs for list forms (c.f. §<a href="#a61">12</a>). </p><p>Following the <span style="color:#A51815"><span style="font-family:monospace">grammar</span></span> in this example is a <span style="color:#A51815"><span style="font-family:monospace">subrule</span></span>
declaration
</p><pre>
<span style="color:#A51815"><span style="font-family:monospace">subrules</span></span>
v <span style="color:#007FFF"><span style="font-family:monospace"><::</span></span> t
</pre><p>
declaring that the <code class="verb">v</code> grammar rule (of values) is a
subgrammar of the <code class="verb">t</code> rule (of terms). The tool checks that
there is in fact a subgrammar relationship, i.e. that for each
production of the lower rule there exists a production of the higher
rule with corresponding elements (up to the subrule relation).
The subrule declaration means that, in the semantic rules below, we
will be able to use <code class="verb">v</code>’s in places where the grammar specifies <code class="verb">t</code>’s.
In the generated Isabelle/Coq/HOL for this example only one free
datatype will be generated, for the <code class="verb">t</code> rule, while for the <code class="verb">v</code>
rule we generate an <code class="verb">is_v</code> predicate over the <code class="verb">t</code> type. Usages of
<code class="verb">v</code> nonterminals in the semantic rules will have instances of this
predicate automatically inserted.</p><p>Finally, we give a collection of definitions of inductive relations.
In this example there is just one family of definitions (of
operational judgements), introduced by the <span style="color:#A51815"><span style="font-family:monospace">defns</span></span> <code class="verb">Jop</code>; it contains just one
definition of a relation, called <code class="verb">reduce</code>.
In general there may be many <span style="color:#A51815"><span style="font-family:monospace">defns</span></span> blocks, each of which introduces a
mutually recursive collection of <span style="color:#A51815"><span style="font-family:monospace">defn</span></span>s.
The relation definition
<span style="color:#A51815"><span style="font-family:monospace">defn</span></span><code class="verb"> ...</code>
also includes a grammar production specifying how elements of the
relation can be written and typeset, here
</p><pre class="verbatim"> t1 --> t2
</pre><p>
As in the main grammar, the tokens of this syntax definition in the
header must be space-separated, but usages of the syntax generally
need not be.
Syntax rules for each family of
judgements, and for their union, are implicitly generated.
The relation definition is given by a sequence of inference rules,
each with a horizontal line separating a number of premises from a
conclusion, for example as below.
</p><pre>
t1 --> t1’
<span style="color:#007FFF"><span style="font-family:monospace"> -------------- ::</span></span> ctx_app_arg
v t1 --> v t1’
</pre><p>
The conclusion must be a symbolic term of the form of the judgement being
defined.
In simple cases (as here) the premises can be symbolic terms of the
form of any of the defined judgements. More generally (see
§<a href="#a53">6</a>) they can be symbolic terms of a user-defined
<span style="color:#A51815"><span style="font-family:monospace">formula</span></span> grammar, or in-line embedded prover code.
Each rule
has a name, composed of a definition family prefix
(here empty), a definition prefix (here also empty) and a kernel
(the <code class="verb">ctx_app_arg</code>).
</p><p>The symbolic terms in semantic rules are parsed with a scannerless parser, built
using parser combinators over character-list inputs. The parser
searches for all parses of the input. If none are found, the ASCII
and TeX output are annotated <span style="font-family:monospace">no parses</span>, with a copy of the
input with <span style="font-family:monospace">***</span> inserted at the point where the last token was
read. This is often at the point of the error (though if, for
example, a putative dot form is read but the two element lists cannot
be anti-unified, it will be after the point of the error).
If multiple parses are found, the TeX output is annotated
<span style="font-family:monospace">multiple parses</span> and the different parses are output to the
console in detail during the Ott run.
If the option <span style="font-family:monospace">picky_multiple_parses</span> is set to
<span style="font-family:monospace">true</span>, multiple parses are always reported. If it set to
<span style="font-family:monospace">false</span>, a symbolic term is considered ambiguous only if two
different parses compile to different strings (for a target).
The parser combinators use memoization and continuation-passing to
achieve reasonable performance on the small symbolic terms that are
typical in semantic rules. Their performance on large (whole-program
size) examples is untested.
To resolve ambiguity one can add metaproductions for parentheses (as
in Fig. <a href="#a45">1</a>), or
production-name annotations in particular symbolic terms,
e.g. the <code class="verb">:t_tsub:</code> in the <code class="verb">AppAbs</code> rule of the POPLmark
example,
<span style="font-family:monospace">test7.ott</span>. There is currently no support for precedence
or associativity.</p><p>This file is included in the distribution as
<span style="font-family:monospace">tests/test10.0.ott</span>. It can be processed by executing
</p><pre>
bin/ott -i tests/test10.0.ott
</pre><p>
from the main directory. This simply reads in the file, checking that
it is well-formed. Adding options:
</p><pre>
bin/ott -show_sort true -show_defns true -i tests/test10.0.ott
</pre><p>
it echos a colourised version to the screen,
with metavariables in red, nonterminals
in yellow, terminals in green, and object variables in white.
The colourisation uses vt220 control codes; if they do not work on
your screen add <span style="font-family:monospace">-colour false</span> to the middle of the command
line. To suppress the echo of the definition, add
<span style="font-family:monospace">-show_sort false</span> and <span style="font-family:monospace">-show_defns false</span>.</p>
<!--TOC subsection id="sec21" Index variables-->
<h3 id="sec21" class="subsection">3.1 Index variables</h3><!--SEC END --><p>
In addition to the <span style="color:#A51815"><span style="font-family:monospace">metavar</span></span> declarations above, the user can declare any number of distinguished <em>index</em>
metavariables, e.g. by:
</p><pre>
<span style="color:#A51815"><span style="font-family:monospace">indexvar</span></span> index<span style="color:#007FFF"><span style="font-family:monospace">,</span></span> i<span style="color:#007FFF"><span style="font-family:monospace">,</span></span> j<span style="color:#007FFF"><span style="font-family:monospace">,</span></span> n<span style="color:#007FFF"><span style="font-family:monospace">,</span></span> m <span style="color:#007FFF"><span style="font-family:monospace">::=</span></span> <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">isa</span></span> num <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span> <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">coq</span></span> nat <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span> <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">hol</span></span> num <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span>
</pre><p>
Given such a declaration, <code class="verb">index</code>, <code class="verb">i</code>, <code class="verb">j</code>, <code class="verb">n</code>
and <code class="verb">m</code> can be used in suffixes, e.g. in the production
</p><pre>
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> ( t1 , <span style="color:#007FFF"><span style="font-family:monospace">....</span></span> , tn ) <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> Tuple
</pre><p>
There is a fixed ad-hoc language of suffixes, including numbers, primes, and index variables (see §<a href="#a17">23</a>).
Index metavariables cannot themselves be suffixed.</p>
<!--TOC section id="sec22" Generating LaTeX-->
<h2 id="sec22" class="section">4 Generating LaTeX</h2><!--SEC END --><p><a id="a58"></a>The example from the previous section can already be used to generate
LaTeX, for example by executing
</p><pre>
bin/ott -i tests/test10.0.ott -o out.tex
</pre><p>
to produce a LaTeX file <span style="font-family:monospace">out.tex</span>. One often needs to
fine-tune the default typesetting, as illustrated in
Figure <a href="#a46">2</a> (the Ott source) and Figure <a href="#a49">3</a>
(the resulting LaTeX).
(The latter was built using the additional option <code class="verb">-tex_show_meta false</code>, to
suppress display of the metaproductions.)
</p><blockquote class="figure"><div class="center"><hr class="floatrule"></div>
<span class="lrbox framebox"><div class="minipage"><span style="font-size:small">
</span><pre><span style="font-size:small">
% minimal + latex + comments
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">metavar</span></span></span><span style="font-size:small"> termvar</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">,</span></span></span><span style="font-size:small"> x </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">tex</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small">mathit</span><span style="font-size:small"><span style="font-family:monospace">{</span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span></span><span style="font-size:small">termvar</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span></span><span style="font-size:small"><span style="font-family:monospace">}</span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">grammar</span></span></span><span style="font-size:small">
t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> ’t_’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">com</span></span></span><span style="font-size:small"> term </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> x </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Var </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">com</span></span></span><span style="font-size:small"> variable</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small"> x . t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Lam </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">com</span></span></span><span style="font-size:small"> lambda </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> t t’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> App </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">com</span></span></span><span style="font-size:small"> app </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> ( t ) </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">S</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Paren
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">{</span></span><span style="font-size:small"> t / x </span><span style="font-size:small"><span style="font-family:monospace">}</span></span><span style="font-size:small"> t’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">M</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Tsub
v </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> ’v_’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">com</span></span></span><span style="font-size:small"> value </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small"> x . t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Lam </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">com</span></span></span><span style="font-size:small"> lambda </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">terminals</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> ’terminals_’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> lambda </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">tex</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small">lambda </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> --> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> red </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">tex</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small">longrightarrow </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">subrules</span></span></span><span style="font-size:small">
v </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"><::</span></span></span><span style="font-size:small"> t
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">defns</span></span></span><span style="font-size:small">
Jop </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> ” </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">defn</span></span></span><span style="font-size:small">
t1 --> t2 </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small">reduce</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small">” </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">com</span></span></span><span style="font-size:small"> $</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span></span><span style="font-size:small">t1</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span></span><span style="font-size:small">$ reduces to $</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span></span><span style="font-size:small">t2</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span></span><span style="font-size:small">$</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">by</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"> --------------------------</span></span></span><span style="font-size:small"> :: ax_app
(</span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small">x.t12) v2 --> </span><span style="font-size:small"><span style="font-family:monospace">{</span></span><span style="font-size:small">v2/x</span><span style="font-size:small"><span style="font-family:monospace">}</span></span><span style="font-size:small">t12
t1 --> t1’
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"> --------------</span></span></span><span style="font-size:small"> :: ctx_app_fun
t1 t --> t1’ t
t1 --> t1’
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"> --------------</span></span></span><span style="font-size:small"> :: ctx_app_arg
v t1 --> v t1’
</span></pre><span style="font-size:small">
</span></div></span>
<div class="caption"><table style="border-spacing:6px;border-collapse:separate;" class="cellpading0"><tr><td style="vertical-align:top;text-align:left;" >Figure 2: Source: <span style="font-family:monospace">test10.2.ott</span><a id="a46"></a></td></tr>
</table></div>
<div class="center"><hr class="floatrule"></div></blockquote><blockquote class="figure"><div class="center"><hr class="floatrule"></div>
<img src="top2001.png"><div class="caption"><table style="border-spacing:6px;border-collapse:separate;" class="cellpading0"><tr><td style="vertical-align:top;text-align:left;" >Figure 3: Generated LaTeX: <span style="font-family:monospace">test10.2.tex</span><a id="a49"></a></td></tr>
</table></div>
<div class="center"><hr class="floatrule"></div></blockquote><p>
The source file has three additions to the previous file.
Firstly, the <span style="color:#A51815"><span style="font-family:monospace">metavar</span></span> declaration is annotated with a
specification of how metavariables should be translated to LaTeX:
</p><pre>
<span style="color:#A51815"><span style="font-family:monospace">metavar</span></span> termvar<span style="color:#007FFF"><span style="font-family:monospace">,</span></span> x <span style="color:#007FFF"><span style="font-family:monospace">::=</span></span>
<span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> <span style="font-family:monospace">\</span>mathit<span style="font-family:monospace">{</span><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span>termvar<span style="color:#007FFF"><span style="font-family:monospace">]]</span></span><span style="font-family:monospace">}</span> <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span>
</pre><p>
Inside the <span style="font-family:monospace"><span style="color:#007FFF">{</span></span><span style="font-family:monospace"><span style="color:#007FFF">{</span></span><span style="font-family:monospace"> </span><span style="font-family:monospace"><span style="color:#A51815">tex</span></span><span style="font-family:monospace"> </span>…<span style="font-family:monospace"> </span><span style="font-family:monospace"><span style="color:#007FFF">}</span></span><span style="font-family:monospace"><span style="color:#007FFF">}</span></span>
is some LaTeX code
<span style="font-family:monospace">\</span><span style="font-family:monospace">mathit</span><span style="font-family:monospace">{</span><span style="font-family:monospace"><span style="color:#007FFF">$[[</span></span><span style="font-family:monospace">termvar</span><span style="font-family:monospace"><span style="color:#007FFF">]]$</span></span><span style="font-family:monospace">}</span>
giving the translation of a <span style="font-family:monospace">termvar</span> or <span style="font-family:monospace">x</span>. Here they
are typeset in math italic (which in fact is also the default).
Within the translation, the metavariable itself can be mentioned
inside double square brackets <span style="font-family:monospace"><span style="color:#007FFF">[[</span></span><span style="font-family:monospace"> </span>…<span style="font-family:monospace"> </span><span style="font-family:monospace"><span style="color:#007FFF">]]</span></span>.</p><p>Secondly, there is a grammar for a distinguished nonterminal root
<span style="color:#A51815"><span style="font-family:monospace">terminals</span></span>, with a
<span style="font-family:monospace"><span style="color:#007FFF">{</span></span><span style="font-family:monospace"><span style="color:#007FFF">{</span></span><span style="font-family:monospace"> </span><span style="font-family:monospace"><span style="color:#A51815">tex</span></span><span style="font-family:monospace"> </span>…<span style="font-family:monospace"> </span><span style="font-family:monospace"><span style="color:#007FFF">}</span></span><span style="font-family:monospace"><span style="color:#007FFF">}</span></span>
translation for each, overriding the default typesetting of some
terminals. Note that the other terminals
(<span style="font-family:monospace">.</span> <span style="font-family:monospace">(</span> <span style="font-family:monospace">)</span> <span style="font-family:monospace">{</span> <span style="font-family:monospace">}</span> <span style="font-family:monospace">/</span>)
are still given their default typesetting.
</p><pre>
<span style="color:#A51815"><span style="font-family:monospace">terminals</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> ’terminals_’ <span style="color:#007FFF"><span style="font-family:monospace">::=</span></span>
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> <span style="font-family:monospace">\</span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> lambda <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> <span style="font-family:monospace">\</span>lambda <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span>
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> --> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> red <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> <span style="font-family:monospace">\</span>longrightarrow <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span>
</pre><p>
Thirdly, the file has <span style="color:#A51815"><span style="font-family:monospace">com</span></span> comments, including
the
<span style="font-family:monospace"><span style="color:#007FFF">{</span></span><span style="font-family:monospace"><span style="color:#007FFF">{</span></span><span style="font-family:monospace"> </span><span style="font-family:monospace"><span style="color:#A51815">com</span></span><span style="font-family:monospace"> term </span><span style="font-family:monospace"><span style="color:#007FFF">}</span></span><span style="font-family:monospace"><span style="color:#007FFF">}</span></span>
attached to a grammar rule,
the
<span style="font-family:monospace"><span style="color:#007FFF">{</span></span><span style="font-family:monospace"><span style="color:#007FFF">{</span></span><span style="font-family:monospace"> </span><span style="font-family:monospace"><span style="color:#A51815">com</span></span><span style="font-family:monospace"> variable</span><span style="font-family:monospace"><span style="color:#007FFF">}</span></span><span style="font-family:monospace"><span style="color:#007FFF">}</span></span>
attached to a production, and the
<span style="font-family:monospace"><span style="color:#007FFF">{</span></span><span style="font-family:monospace"><span style="color:#007FFF">{</span></span><span style="font-family:monospace"> </span><span style="font-family:monospace"><span style="color:#A51815">com</span></span><span style="font-family:monospace"> </span><span style="font-family:monospace"><span style="color:#007FFF">[[</span></span><span style="font-family:monospace">t1</span><span style="font-family:monospace"><span style="color:#007FFF">]]</span></span><span style="font-family:monospace"> reduces to </span><span style="font-family:monospace"><span style="color:#007FFF">[[</span></span><span style="font-family:monospace">t2</span><span style="font-family:monospace"><span style="color:#007FFF">]]</span></span><span style="font-family:monospace"><span style="color:#007FFF">}</span></span><span style="font-family:monospace"><span style="color:#007FFF">}</span></span>
attached to a semantic relation. These appear in the LaTeX output
as shown in Figure <a href="#a49">3</a>.</p>
<!--TOC subsection id="sec23" Specifying LaTeX for productions-->
<h3 id="sec23" class="subsection">4.1 Specifying LaTeX for productions</h3><!--SEC END --><p>
One can also specify <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> translations for productions, overriding the default
LaTeX typesetting, e.g. as in this example of
a type abstraction production.
</p><pre>
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> X <: T . t <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> TLam <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> <span style="font-family:monospace">\</span>Lambda <span style="color:#007FFF"><span style="font-family:monospace">[[</span></span>X<span style="color:#007FFF"><span style="font-family:monospace">]]</span></span> <span style="color:#007FFF"><span style="font-family:monospace">[[</span></span><:<span style="color:#007FFF"><span style="font-family:monospace">]]</span></span> <span style="color:#007FFF"><span style="font-family:monospace">[[</span></span>T<span style="color:#007FFF"><span style="font-family:monospace">]]</span></span>. <span style="font-family:monospace">\</span>, <span style="color:#007FFF"><span style="font-family:monospace">[[</span></span>t<span style="color:#007FFF"><span style="font-family:monospace">]]</span></span> <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span>
</pre><p>
These <em>homomorphisms</em>, or <em>homs</em><sup><a id="text1" href="#note1">1</a></sup>, can refer to the metavariables and
nonterminals that occur in the production, e.g. the <span style="font-family:monospace"><span style="color:#007FFF">[[</span></span><span style="font-family:monospace">X</span><span style="font-family:monospace"><span style="color:#007FFF">]]</span></span>,
<span style="font-family:monospace"><span style="color:#007FFF">[[</span></span><span style="font-family:monospace">T</span><span style="font-family:monospace"><span style="color:#007FFF">]]</span></span>, and <span style="font-family:monospace"><span style="color:#007FFF">[[</span></span><span style="font-family:monospace">t</span><span style="font-family:monospace"><span style="color:#007FFF">]]</span></span> in the <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> hom above,
interleaved with arbitrary strings and with typeset elements of the
<span style="color:#A51815"><span style="font-family:monospace">terminals</span></span> grammar, e.g. the <span style="font-family:monospace"><span style="color:#007FFF">[[</span></span><span style="font-family:monospace"><:</span><span style="font-family:monospace"><span style="color:#007FFF">]]</span></span>.</p><p>Homomorphisms are applied recursively down the structure of symbolic
terms. For example, an F<sub><:</sub> term
</p><pre class="verbatim"> (\X<:T11.t12) [T2]
</pre><p>
would be LaTeX-pretty-printed, using the <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> clause above, as
</p><pre class="verbatim">( \, \Lambda \mathit{X} <: \mathit{T_{\mathrm{11}}} . \, \mathit{t_{\mathrm{12}}} \, )
\, \, [ \, \mathit{T_{\mathrm{2}}} \, ]
</pre><p>
which is typeset as below.
</p><table class="display dcenter"><tr style="vertical-align:middle"><td class="dcell">
<img src="top2002.png"></td></tr>
</table><p>
Note the <code class="verb">X</code>, <code class="verb">T11</code> and <code class="verb">t12</code> of the symbolic term are
used to instantiate the formal parameters <code class="verb">X</code>, <code class="verb">T</code> and
<code class="verb">t</code> of the homomorphism definition clause.
If the <code class="verb">t</code> itself had compound term structure, e.g. as below
</p><pre class="verbatim"> (\X<:T. \X'<:T'.x)
</pre><p>
the homomorphism would be applied recursively, producing
</p><pre class="verbatim">( \, \Lambda \mathit{X} <: \mathit{T} . \, \Lambda \mathit{X'} <: \mathit{T'}
. \, \mathit{x} \, \, )
</pre><p>
typeset as follows.
</p><table class="display dcenter"><tr style="vertical-align:middle"><td class="dcell">
<img src="top2003.png"></td></tr>
</table><p>
Where there is no user-supplied homomorphism clause the LaTeX
pretty-printing defaults to a sequence of the individual items
separated by thin spaces (<code class="verb">\,</code>),
with reasonable default fonts and making use of the <code class="verb">terminals</code> grammar where appropriate.</p>
<!--TOC subsection id="sec24" Specifying LaTeX for grammar rules-->
<h3 id="sec24" class="subsection">4.2 Specifying LaTeX for grammar rules</h3><!--SEC END --><p>
Grammar rules can include a <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> hom specifying how all the
nonterminal roots should be typeset, e.g.
</p><pre>
type<span style="color:#007FFF"><span style="font-family:monospace">,</span></span> t<span style="color:#007FFF"><span style="font-family:monospace">,</span></span> s <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> Typ_ <span style="color:#007FFF"><span style="font-family:monospace">::=</span></span> <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> <span style="font-family:monospace">\</span>mathsf<span style="font-family:monospace">{</span><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span>type<span style="color:#007FFF"><span style="font-family:monospace">]]</span></span><span style="font-family:monospace">}</span> <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span>
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> unit <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> unit
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> type * type’ <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> pair
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> type -> type’ <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> fun
</pre><p>Alternatively, the individual nonterminal roots can have <span style="color:#A51815"><span style="font-family:monospace">tex</span></span>
homs specifying how they should be typeset:
</p><pre>
G <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> <span style="font-family:monospace">\</span>Gamma <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span> <span style="color:#007FFF"><span style="font-family:monospace">,</span></span> D <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">tex</span></span> <span style="font-family:monospace">\</span>Delta <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> ’G_’ <span style="color:#007FFF"><span style="font-family:monospace">::=</span></span>
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> empty <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> empty
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> G , x : T <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> term
</pre><p>
permitting the user to write <code class="verb">G'</code>, <code class="verb">D12</code> etc. in symbolic
terms, to be typeset as
<img src="top2004.png">etc.</p>
<!--TOC subsection id="sec25" Using the LaTeX code-->
<h3 id="sec25" class="subsection">4.3 Using the LaTeX code</h3><!--SEC END --><p><a id="a64"></a>The generated LaTeX code can be used in two main ways.
By default, Ott generates a stand-alone LaTeX file,
with a standard wrapper (including a <code class="verb">\documentclass</code>, various
macro definitions, and a main body),
that gives the complete system definition.</p><p>The default header can be overridden by writing
<code class="verb"> embed {{ tex-wrap-pre ... }} </code> and the default footer by
writing <code class="verb">embed {{ tex-wrap-post ... }} </code>. Alternatively, the
program option <code class="verb">-tex_wrap false</code> with the <code class="verb">-tex_wrap false</code>
command-line argument, one can generate a file that can be included in
other LaTeX files, that just defines macros to typeset various
parts of the system (<code class="verb">-tex_wrap false</code> overrides any
<code class="verb">tex-wrap-pre/tex-wrap-post</code> embeds).</p><p>The generated LaTeX output is factored into individual LaTeX
commands: for the metavariable declarations, each rule of the syntax
definition, the collected syntax (<code class="verb">\ottgrammar</code>), each rule of the inductive relation
definitions, the collected rules for each relation, the collected
rules for each <code class="verb">defns</code> block, the union of those
(<code class="verb">\ottdefns</code>) and the whole (<code class="verb">\ottall</code>).
This makes it possible to quote individual parts of the definition,
possibly out-of-order, in a paper or technical report. </p><p>If one needs to include more than one system in a single LaTeX
document, the <code class="verb">ott</code> prefix can be replaced using the
<code class="verb">-tex_name_prefix</code> command-line argument. </p><p>The generated LaTeX is factored through some common style macros,
e.g. to typeset a comment, a production, and a grammar. If necessary
these can be redefined in an <span style="color:#A51815"><span style="font-family:monospace">embed</span></span> block (see Section <a href="#a60">8.1</a>).
For example, the file <code class="verb">tests/squishtex.ott</code>
</p><pre>
<span style="color:#A51815"><span style="font-family:monospace">embed</span></span>
<span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> tex-preamble
<span style="font-family:monospace">\</span>renewcommand<span style="font-family:monospace">{</span><span style="font-family:monospace">\</span><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span><span style="color:#A51815"><span style="font-family:monospace">TEX_NAME_PREFIX</span></span><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span>grammartabular<span style="font-family:monospace">}</span>[1]
<span style="font-family:monospace">{</span><span style="font-family:monospace">\</span>begin<span style="font-family:monospace">{</span>minipage<span style="font-family:monospace">}</span><span style="font-family:monospace">{</span><span style="font-family:monospace">\</span>columnwidth<span style="font-family:monospace">}</span><span style="font-family:monospace">\</span>begin<span style="font-family:monospace">{</span>tabular<span style="font-family:monospace">}</span><span style="font-family:monospace">{</span>ll<span style="font-family:monospace">}</span>#1<span style="font-family:monospace">\</span>end<span style="font-family:monospace">{</span>tabular<span style="font-family:monospace">}</span><span style="font-family:monospace">\</span>end<span style="font-family:monospace">{</span>minipage<span style="font-family:monospace">}</span> <span style="font-family:monospace">}</span>
<span style="font-family:monospace">\</span>renewcommand<span style="font-family:monospace">{</span><span style="font-family:monospace">\</span><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span><span style="color:#A51815"><span style="font-family:monospace">TEX_NAME_PREFIX</span></span><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span>rulehead<span style="font-family:monospace">}</span>[3]
<span style="font-family:monospace">{</span>$#1$ $#2$ & $#3$<span style="font-family:monospace">}</span>
<span style="font-family:monospace">\</span>renewcommand<span style="font-family:monospace">{</span><span style="font-family:monospace">\</span><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span><span style="color:#A51815"><span style="font-family:monospace">TEX_NAME_PREFIX</span></span><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span>prodline<span style="font-family:monospace">}</span>[6]
<span style="font-family:monospace">{</span> <span style="font-family:monospace">\</span>quad $#1$ <span style="font-family:monospace">\</span> $#2$ & <span style="font-family:monospace">\</span>quad $#3 #4$ $#5$ $#6$<span style="font-family:monospace">}</span>
<span style="font-family:monospace">\</span>renewcommand<span style="font-family:monospace">{</span><span style="font-family:monospace">\</span><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span><span style="color:#A51815"><span style="font-family:monospace">TEX_NAME_PREFIX</span></span><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span>interrule<span style="font-family:monospace">}</span>
<span style="font-family:monospace">{</span><span style="font-family:monospace">\</span><span style="font-family:monospace">\</span>[2.0mm]<span style="font-family:monospace">}</span>
<span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span>
</pre><p>
defines a more compact style for grammars. Note that the
<span style="font-family:monospace"><span style="color:#007FFF">[[</span></span><span style="font-family:monospace"><span style="color:#A51815">TEX_NAME_PREFIX</span></span><span style="font-family:monospace"><span style="color:#007FFF">]]</span></span> is replaced by whatever prefix is in force,
so such style files can be reused in different contexts.</p><p>A more sophisticated LaTeX package <code class="verb">ottlayout.sty</code>, providing fine control of how
inference rules and grammars should be typeset, is contained in the
<code class="verb">tex</code> directory of the distribution. It is described in the
manual therein.</p>
<!--TOC section id="sec26" Generating proof assistant definitions-->
<h2 id="sec26" class="section">5 Generating proof assistant definitions</h2><!--SEC END --><p><a id="a52"></a>To generate proof assistant definitions, for Coq, Isabelle, and HOL,
the minimal Ott source file of Section <a href="#a51">3</a>/Figure <a href="#a45">1</a> must
be extended with a modest amount of additional data, as shown in Figure <a href="#a47">4</a>.
Executing
</p><pre>
bin/ott -i tests/test10.4.ott -o out.v -o out.thy -o outScript.sml
</pre><p>
generates Coq <span style="font-family:monospace">out.v</span>, Isabelle <span style="font-family:monospace">out.thy</span>, and HOL
<span style="font-family:monospace">outScript.sml</span>, shown in Figures <a href="#a6">5</a>, <a href="#a5">6</a>, and <a href="#a40">7</a>.
The additional data can be combined with the annotations for
LaTeX of the previous section, but those are omitted here.
</p><blockquote class="figure"><div class="center"><hr class="floatrule"></div>
<span class="lrbox framebox"><div class="minipage"><span style="font-size:small">
</span><pre><span style="font-size:small">
% minimal + binding + subst + coq/hol/isa
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">metavar</span></span></span><span style="font-size:small"> termvar</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">,</span></span></span><span style="font-size:small"> x </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">isa</span></span></span><span style="font-size:small"> string</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">coq</span></span></span><span style="font-size:small"> nat</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">hol</span></span></span><span style="font-size:small"> string</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">coq-equality</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">grammar</span></span></span><span style="font-size:small">
t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> ’t_’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> x </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Var
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small"> x . t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Lam </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">(+</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">bind</span></span></span><span style="font-size:small"> x </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">in</span></span></span><span style="font-size:small"> t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">+)</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> t t’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> App
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> ( t ) </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">S</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Paren </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">icho</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span></span><span style="font-size:small">t</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">{</span></span><span style="font-size:small"> t / x </span><span style="font-size:small"><span style="font-family:monospace">}</span></span><span style="font-size:small"> t’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">M</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Tsub </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">{</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">icho</span></span></span><span style="font-size:small"> (tsubst_t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span></span><span style="font-size:small">t</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span></span><span style="font-size:small">x</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">[[</span></span></span><span style="font-size:small">t’</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">]]</span></span></span><span style="font-size:small">)</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">}</span></span></span><span style="font-size:small">
v </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> ’v_’ </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">|</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small"> x . t </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> Lam
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">subrules</span></span></span><span style="font-size:small">
v </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"><::</span></span></span><span style="font-size:small"> t
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">substitutions</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">single</span></span></span><span style="font-size:small"> t x </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> tsubst
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">defns</span></span></span><span style="font-size:small">
Jop </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> ” </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::=</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">defn</span></span></span><span style="font-size:small">
t1 --> t2 </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small"> </span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small">reduce</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace">::</span></span></span><span style="font-size:small">” </span><span style="font-size:small"><span style="color:#A51815"><span style="font-family:monospace">by</span></span></span><span style="font-size:small">
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"> --------------------------</span></span></span><span style="font-size:small"> :: ax_app
(</span><span style="font-size:small"><span style="font-family:monospace">\</span></span><span style="font-size:small">x.t12) v2 --> </span><span style="font-size:small"><span style="font-family:monospace">{</span></span><span style="font-size:small">v2/x</span><span style="font-size:small"><span style="font-family:monospace">}</span></span><span style="font-size:small">t12
t1 --> t1’
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"> --------------</span></span></span><span style="font-size:small"> :: ctx_app_fun
t1 t --> t1’ t
t1 --> t1’
</span><span style="font-size:small"><span style="color:#007FFF"><span style="font-family:monospace"> --------------</span></span></span><span style="font-size:small"> :: ctx_app_arg
v t1 --> v t1’
</span></pre><span style="font-size:small">
</span></div></span>
<div class="caption"><table style="border-spacing:6px;border-collapse:separate;" class="cellpading0"><tr><td style="vertical-align:top;text-align:left;" >Figure 4: Source: <span style="font-family:monospace">test10.4.ott</span><a id="a47"></a></td></tr>
</table></div>
<div class="center"><hr class="floatrule"></div></blockquote><p>
We add four things.
First, we specify proof assistant types to represent object-language
variables — in this example, choosing the <span style="font-family:monospace">string</span> type of
Isabelle and HOL, and the <span style="font-family:monospace">nat</span> type for Coq:
</p><pre>
<span style="color:#A51815"><span style="font-family:monospace">metavar</span></span> termvar<span style="color:#007FFF"><span style="font-family:monospace">,</span></span> x <span style="color:#007FFF"><span style="font-family:monospace">::=</span></span>
<span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">isa</span></span> string<span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span> <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">coq</span></span> nat<span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span> <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">hol</span></span> string<span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span> <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">coq-equality</span></span> <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span>
</pre><p>
For Coq output, one can specify <code class="verb">{{ coq-equality</code> <span style="font-style:italic">proof-script</span> <code class="verb">}}</code>
to build a decidable equality over the Coq representation type using
the proof <span style="font-style:italic">proof-script</span>. If the script is omitted, as in this
example, it defaults
to
</p><pre class="verbatim">Proof.
decide equality; auto with ott_coq_equality arith.
Defined.
</pre><p>
where the <code class="verb">ott_coq_equality</code> database contains the decidable
equalities of the representation types defined in the source. It is
possible to suppress type generation for specific metavariables or nonterminals, by adding the
declaration <code class="verb">{{ phantom }}</code>. This is useful in some cases, for
instance to avoid duplicate definitions of types already defined in an
imported library. Any type homs are taken into account when
the metavariable or nonterminal root is output as a type.</p><p>Second, we specify what the binding is in the object language, with
the <span style="font-family:monospace"><span style="color:#007FFF">(+</span></span><span style="font-family:monospace"> </span><span style="font-family:monospace"><span style="color:#A51815">bind</span></span><span style="font-family:monospace"> x </span><span style="font-family:monospace"><span style="color:#A51815">in</span></span><span style="font-family:monospace"> t </span><span style="font-family:monospace"><span style="color:#007FFF">+)</span></span>
annotation on the <span style="font-family:monospace">Lam</span> production:
</p><pre>
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> <span style="font-family:monospace">\</span> x . t <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> Lam <span style="color:#007FFF"><span style="font-family:monospace">(+</span></span> <span style="color:#A51815"><span style="font-family:monospace">bind</span></span> x <span style="color:#A51815"><span style="font-family:monospace">in</span></span> t <span style="color:#007FFF"><span style="font-family:monospace">+)</span></span>
</pre><p>
Section <a href="#a62">9</a> describes the full language of binding specifications.</p><p>Third, we add a block
</p><pre>
<span style="color:#A51815"><span style="font-family:monospace">substitutions</span></span>
<span style="color:#A51815"><span style="font-family:monospace">single</span></span> t x <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> tsubst
</pre><p>
to cause Ott to generate Coq/Isabelle/HOL definitions of a substitution
function, with name root <span style="font-family:monospace">tsubst</span>, replacing metavariables <span style="font-family:monospace">x</span> by terms <span style="font-family:monospace">t</span>. This is for single
substitutions; multiple substitution functions (taking lists of
substitutand/substitutee pairs) can also be generated with the keyword
<span style="color:#A51815"><span style="font-family:monospace">multiple</span></span>.
Substitution functions are generated for all rules of the grammar for
which they might be required — here, just over <code class="verb">t</code>, with a
function named <code class="verb">tsubst_t</code>.</p><p>Finally, we specify translations for the metaproductions:
</p><pre>
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> ( t ) <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#A51815"><span style="font-family:monospace">S</span></span><span style="color:#007FFF"><span style="font-family:monospace">::</span></span> Paren <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">icho</span></span> <span style="color:#007FFF"><span style="font-family:monospace">[[</span></span>t<span style="color:#007FFF"><span style="font-family:monospace">]]</span></span> <span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span>
<span style="color:#007FFF"><span style="font-family:monospace">|</span></span> <span style="font-family:monospace">{</span> t / x <span style="font-family:monospace">}</span> t’ <span style="color:#007FFF"><span style="font-family:monospace">::</span></span> <span style="color:#A51815"><span style="font-family:monospace">M</span></span><span style="color:#007FFF"><span style="font-family:monospace">::</span></span> Tsub <span style="color:#007FFF"><span style="font-family:monospace">{</span></span><span style="color:#007FFF"><span style="font-family:monospace">{</span></span> <span style="color:#A51815"><span style="font-family:monospace">icho</span></span> (tsubst_t <span style="color:#007FFF"><span style="font-family:monospace">[[</span></span>t<span style="color:#007FFF"><span style="font-family:monospace">]]</span></span> <span style="color:#007FFF"><span style="font-family:monospace">[[</span></span>x<span style="color:#007FFF"><span style="font-family:monospace">]]</span></span> <span style="color:#007FFF"><span style="font-family:monospace">[[</span></span>t’<span style="color:#007FFF"><span style="font-family:monospace">]]</span></span>)<span style="color:#007FFF"><span style="font-family:monospace">}</span></span><span style="color:#007FFF"><span style="font-family:monospace">}</span></span>
</pre><p>
These specify that <span style="font-family:monospace">(t)</span> should be translated into just the
translation of <span style="font-family:monospace">t</span>, whereas