/[mojave]/metaprl/theories/itt/itt_comment.ml
ViewVC logotype

Contents of /metaprl/theories/itt/itt_comment.ml

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3584 - (show annotations) (download)
Thu Apr 25 15:28:40 2002 UTC (19 years, 3 months ago) by nogin
File size: 32352 byte(s)
- Added the comment module to the theories.pdf ("make latex").

- Added a hack allowing to override a theory display with another theory's
display. This is necessary for bootstrapping reasons - it allows one
to get a reasonable output of a theory (e.g. Comment) that is defined before
all essential display forms (e.g. the Summary ones) are there.

- Added debugging code to make it easier to find dforms that cause
zone begin/end mismatch (and used it to get rid of all
the "Unballanced buffer" warnings in "make latex").

- Minor dforms&comments updates.

1 (*!
2 * @begin[doc]
3 * @theory[Itt_comment]
4 *
5 * Terms used for comments in the @Nuprl type theory.
6 * @end[doc]
7 *
8 * ----------------------------------------------------------------
9 *
10 * @begin[license]
11 * Copyright (C) 2000 Jason Hickey, Caltech
12 *
13 * This program is free software; you can redistribute it and/or
14 * modify it under the terms of the GNU General Public License
15 * as published by the Free Software Foundation; either version 2
16 * of the License, or (at your option) any later version.
17 *
18 * This program is distributed in the hope that it will be useful,
19 * but WITHOUT ANY WARRANTY; without even the implied warranty of
20 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
21 * GNU General Public License for more details.
22 *
23 * You should have received a copy of the GNU General Public License
24 * along with this program; if not, write to the Free Software
25 * Foundation, Inc., 675 Mass Ave, Cambridge, MA 02139, USA.
26 *
27 * Author: Jason Hickey
28 * @email{jyh@cs.caltech.edu}
29 * @end[license]
30 *)
31
32 include Base_theory
33
34 (************************************************************************
35 * UNIVERSES AND EQUALITY
36 ************************************************************************)
37
38 declare math_type{'a}
39 declare math_univ{'i}
40 declare math_equal{'T; 'a; 'b}
41 declare math_member{'T; 'a}
42 declare math_cumulativity{'i; 'j}
43
44 prec prec_type
45 prec prec_equal
46
47 (************************************************
48 * TeX mode.
49 *)
50 dform math_type_df1 : mode[tex] :: math_type{'t} =
51 slot{'t}
52 izone `"\\,\\mathtt{" ezone
53 `"Type"
54 izone "}" ezone
55
56 dform math_univ_df : mode[tex] :: math_univ{'i} =
57 izone `"{\\mathbb U}_{" ezone
58 slot{'i}
59 izone `"}" ezone
60
61 dform math_equal_df1 : mode[tex] :: math_equal{'T; 'a; 'b} =
62 izone `"{" ezone
63 slot{'a}
64 izone `" = " ezone
65 slot{'b}
66 izone `" \\in " ezone
67 slot{'T}
68 izone `"}" ezone
69
70 dform math_member_df1 : mode[tex] :: math_member{'T; 'a} =
71 izone `"{" ezone
72 slot{'a}
73 izone `" \\in " ezone
74 slot{'T}
75 izone `"}" ezone
76
77 dform math_cumulativity_df1 : mode[tex] :: math_cumulativity{'i; 'j} =
78 izone `"{{\\it cumulativity}[" ezone
79 slot{'i}
80 izone `", " ezone
81 slot{'j}
82 izone `"]}" ezone
83
84 (************************************************
85 * Normal mode.
86 *)
87
88 dform equal_df : except_mode[tex] :: parens :: "prec"[prec_equal] :: math_equal{'T; 'a; 'b} =
89 szone pushm slot{'a} space `"= " slot{'b} space Nuprl_font!member `" " slot{'T} popm ezone
90
91 dform member_df2 : mode[tex] :: parens :: "prec"[prec_equal] :: math_member{'T; 'a} =
92 szone pushm slot{'a} space `"IN" hspace slot{'T} popm ezone
93
94 dform type_df1 : except_mode[tex] :: parens :: "prec"[prec_type] :: math_type{'a} =
95 slot{'a} " " `"Type"
96
97 dform univ_df1 : except_mode[tex] :: math_univ{'i} =
98 mathbbU `"[" slot{'i} `"]"
99
100 dform cumulativity_df : except_mode[tex] :: math_cumulativity{'i; 'j} =
101 `"cumulativity[" slot{'i} `";" slot{'j} `"]"
102
103 (************************************************************************
104 * VOID
105 ************************************************************************)
106
107 declare math_void
108 declare math_false
109
110 dform math_Void_df1 : math_void =
111 math_i["Void"]
112
113 dform math_False_df1 : mode[tex] :: math_false =
114 izone `"{\\bot}" ezone
115
116 dform math_False_df2 : except_mode[tex] :: math_false =
117 it["False"]
118
119 (************************************************************************
120 * UNIT
121 ************************************************************************)
122
123 declare math_unit
124 declare math_true
125 declare math_it
126
127 dform math_Unit_df1 : math_unit =
128 math_i["Unit"]
129
130 dform math_True_df1 : mode[tex] :: math_true =
131 izone `"{\\top}" ezone
132
133 dform math_True_df2 : except_mode[tex] :: math_true =
134 it["True"]
135
136 dform math_it_df1 : mode[tex] :: math_it =
137 izone `"\\cdot " ezone
138
139 dform math_it_df2 : except_mode[tex] :: math_it =
140 Nuprl_font!cdot
141
142 (************************************************************************
143 * ATOM
144 ************************************************************************)
145
146 declare math_atom
147 declare math_token{'t}
148
149 dform math_Atom_df1 : math_atom =
150 math_i["Atom"]
151
152 dform math_token_df1 : math_token{'t} =
153 math_i["token"] `"(" slot{'t} `")"
154
155 (************************************************************************
156 * BOOL
157 ************************************************************************)
158
159 declare math_bool
160 declare math_btrue
161 declare math_bfalse
162 declare math_bor{'a; 'b}
163 declare math_band{'a; 'b}
164 declare math_bimplies{'a; 'b}
165 declare math_bnot{'a}
166 declare math_assert{'t}
167 declare math_if{'a; 'b; 'c}
168
169 dform math_Bool_df1 : math_bool =
170 math_i["Bool"]
171
172 dform math_btrue_df1 : math_btrue =
173 math_i["tt"]
174
175 dform math_bfalse_df1 : math_bfalse =
176 math_i["ff"]
177
178 (************************************************
179 * TeX mode
180 *)
181 dform math_bor_df1 : mode[tex] :: math_bor{'a; 'b} =
182 izone `"{" ezone
183 slot{'a}
184 izone `"\\vee_b " ezone
185 slot{'b}
186 izone `"}" ezone
187
188 dform math_band_df1 : mode[tex] :: math_band{'a; 'b} =
189 izone `"{" ezone
190 slot{'a}
191 izone `"\\wedge_b " ezone
192 slot{'b}
193 izone `"}" ezone
194
195 dform math_bimplies_df1 : mode[tex] :: math_bimplies{'a; 'b} =
196 izone `"{" ezone
197 slot{'a}
198 izone `"\\Rightarrow_b " ezone
199 slot{'b}
200 izone `"}" ezone
201
202 dform math_bnot_df1 : mode[tex] :: math_bnot{'a} =
203 izone `"{\\neg_b " ezone
204 slot{'a}
205 izone `"}" ezone
206
207 dform math_assert_df1 : mode[tex] :: math_assert{'a} =
208 izone `"{\\uparrow " ezone
209 slot{'a}
210 izone `"}" ezone
211
212 dform math_if_df1 : mode[tex] :: math_if{'a; 'b; 'c} =
213 izone `"\\mathop{\\bf if}" ezone
214 szone{'a}
215 izone `"\\mathrel{\\bf then}" ezone
216 szone{'b}
217 izone `"\\mathrel{\\bf else}" ezone
218 szone{'c}
219
220 (************************************************
221 * Normal mode.
222 *)
223 prec prec_bimplies
224 prec prec_bor
225 prec prec_band
226 prec prec_bnot
227 prec prec_assert
228
229 prec prec_bimplies < prec_bor
230 prec prec_bor < prec_band
231 prec prec_band < prec_bnot
232 prec prec_bnot < prec_assert
233
234 dform bor_df : parens :: "prec"[prec_bor] :: except_mode[tex] :: math_bor{'a; 'b} =
235 slot{'a} " " vee subb " " slot{'b}
236
237 dform band_df : parens :: "prec"[prec_band] :: except_mode[tex] :: math_band{'a; 'b} =
238 slot{'a} " " wedge subb " " slot{'b}
239
240 dform bimplies_df : parens :: "prec"[prec_bimplies] :: except_mode[tex] :: math_bimplies{'a; 'b} =
241 slot{'a} " " Rightarrow subb " " slot{'b}
242
243 dform bnot_df : parens :: "prec"[prec_bnot] :: except_mode[tex] :: math_bnot{'a} =
244 tneg subb slot{'a}
245
246 dform ifthenelse_df : parens :: "prec"[prec_bor] :: except_mode[tex] :: math_if{'e1; 'e2; 'e3} =
247 szone pushm[0] pushm[3] `"if" `" " szone{'e1} `" " `"then" hspace
248 szone{'e2} popm hspace
249 pushm[3] `"else" hspace szone{'e3} popm popm ezone
250
251 dform assert_df : parens :: "prec"[prec_assert] :: except_mode[tex] :: math_assert{'t} =
252 downarrow slot{'t}
253
254 (************************************************************************
255 * INTEGERS
256 ************************************************************************)
257
258 declare math_int
259 declare math_number{'n}
260 declare math_ind{'i; 'm; 'z; 'down; 'base; 'm; 'z; 'up}
261 declare math_add{'a; 'b}
262 declare math_sub{'a; 'b}
263 declare math_mul{'a; 'b}
264 declare math_div{'a; 'b}
265 declare math_rem{'a; 'b}
266 declare math_lt{'a; 'b}
267 declare math_le{'a; 'b}
268 declare math_ge{'a; 'b}
269 declare math_gt{'a; 'b}
270
271 dform math_int_df1 : mode[tex] :: math_int =
272 izone `"{\\mathbb Z}" ezone
273
274 dform math_number_df1 : mode[tex] :: math_number{'i} =
275 izone `"{{\\it number}[" ezone
276 slot{'i}
277 izone `"]}" ezone
278
279 dform math_ind_df1 : mode[tex] :: math_ind{'i; 'a; 'b; 'down; 'base; 'c; 'd; 'up} =
280 izone `"{{\\it ind}(" ezone
281 slot{'i}
282 izone `"; " ezone
283 slot{'a}
284 izone `", " ezone
285 slot{'b}
286 izone `". " ezone
287 slot{'down}
288 izone `"; " ezone
289 slot{'base}
290 izone `"; " ezone
291 slot{'c}
292 izone `", " ezone
293 slot{'c}
294 izone `". " ezone
295 slot{'up}
296 izone `")}" ezone
297
298 dform math_add_df1 : mode[tex] :: math_add{'i; 'j} =
299 izone `"{" ezone
300 slot{'i}
301 izone `"+" ezone
302 slot{'j}
303 izone `"}" ezone
304
305 dform math_sub_df1 : mode[tex] :: math_sub{'i; 'j} =
306 izone `"{" ezone
307 slot{'i}
308 izone `"-" ezone
309 slot{'j}
310 izone `"}" ezone
311
312 dform math_mul_df1 : mode[tex] :: math_mul{'i; 'j} =
313 izone `"{" ezone
314 slot{'i}
315 izone `"*" ezone
316 slot{'j}
317 izone `"}" ezone
318
319 dform math_div_df1 : mode[tex] :: math_div{'i; 'j} =
320 izone `"{" ezone
321 slot{'i}
322 izone `"/" ezone
323 slot{'j}
324 izone `"}" ezone
325
326 dform math_rem_df1 : mode[tex] :: math_rem{'i; 'j} =
327 izone `"{" ezone
328 slot{'i}
329 izone `"\\mathrel{\\bf rem}" ezone
330 slot{'j}
331 izone `"}" ezone
332
333 dform math_gt_df1 : mode[tex] :: math_gt{'i; 'j} =
334 izone `"{" ezone
335 slot{'i}
336 izone `">" ezone
337 slot{'j}
338 izone `"}" ezone
339
340 dform math_ge_df1 : mode[tex] :: math_ge{'i; 'j} =
341 izone `"{" ezone
342 slot{'i}
343 izone `"\\ge " ezone
344 slot{'j}
345 izone `"}" ezone
346
347 dform math_lt_df1 : mode[tex] :: math_lt{'i; 'j} =
348 izone `"{" ezone
349 slot{'i}
350 izone `"<" ezone
351 slot{'j}
352 izone `"}" ezone
353
354 dform math_le_df1 : mode[tex] :: math_le{'i; 'j} =
355 izone `"{" ezone
356 slot{'i}
357 izone `"\\le " ezone
358 slot{'j}
359 izone `"}" ezone
360
361 (************************************************
362 * Normal mode
363 *)
364
365 prec prec_compare
366 prec prec_add
367 prec prec_mul
368
369 dform int_prl_df : except_mode [doc] :: math_int = mathbbZ
370
371 dform number_df : except_mode[tex] :: math_number{'n} =
372 slot{'n}
373
374 dform add_df1 : except_mode[tex] :: parens :: "prec"[prec_add] :: math_add{'a; 'b} =
375 slot["le"]{'a} `" + " slot["lt"]{'b}
376
377 dform sub_df1 : except_mode[tex] :: parens :: "prec"[prec_add] :: math_sub{'a; 'b} =
378 slot["lt"]{'a} `" - " slot["le"]{'b}
379
380 dform mul_df1 : except_mode[tex] :: parens :: "prec"[prec_mul] :: math_mul{'a; 'b} =
381 slot["lt"]{'a} `" * " slot["le"]{'b}
382
383 dform div_df1 : except_mode[tex] :: parens :: "prec"[prec_mul] :: math_div{'a; 'b} =
384 slot["lt"]{'a} Nuprl_font!"div" slot["le"]{'b}
385
386 dform rem_df1 : except_mode[tex] :: parens :: "prec"[prec_mul] :: math_rem{'a; 'b} =
387 slot["lt"]{'a} `" % " slot["le"]{'b}
388
389 dform lt_df1 : except_mode[tex] :: parens :: "prec"[prec_compare] :: math_lt{'a; 'b} =
390 slot["lt"]{'a} `" < " slot["le"]{'b}
391
392 dform le_df1 : except_mode[tex] :: parens :: "prec"[prec_compare] :: math_le{'a; 'b} =
393 slot["lt"]{'a} Nuprl_font!le slot["le"]{'b}
394
395 dform ge_df1 : except_mode[tex] :: parens :: "prec"[prec_compare] :: math_ge{'a; 'b} =
396 slot["lt"]{'a} Nuprl_font!ge slot["le"]{'b}
397
398 dform gt_df1 : except_mode[tex] :: parens :: "prec"[prec_compare] :: math_gt{'a; 'b} =
399 slot["lt"]{'a} `" > " slot["le"]{'b}
400
401 (************************************************************************
402 * UNION
403 ************************************************************************)
404
405 declare math_union{'A; 'B}
406 declare math_inl{'x}
407 declare math_inr{'x}
408 declare math_decide{'x; 'y; 'a; 'z; 'b}
409 declare math_or{'a; 'b}
410 declare math_cor{'a; 'b}
411
412 (************************************************
413 * TeX mode
414 *)
415 dform math_union_df1 : mode[tex] :: math_union{'A; 'B} =
416 izone `"{" ezone
417 slot{'A}
418 izone `"+" ezone
419 slot{'B}
420 izone `"}" ezone
421
422 dform math_inl_df1 : mode[tex] :: math_inl{'x} =
423 izone `"{{\\it inl}(" ezone
424 slot{'x}
425 izone `")}" ezone
426
427 dform math_inr_df1 : mode[tex] :: math_inr{'x} =
428 izone `"{{\\it inr}(" ezone
429 slot{'x}
430 izone `")}" ezone
431
432 dform math_decide_df1 : mode[tex] :: math_decide{'x; 'y; 'a; 'z; 'b} =
433 izone `"{\\mathop{\\bf match}" ezone
434 slot{'x}
435 izone `"\\mathrel{\\bf with}" ezone
436 math_inl{'y}
437 izone `"\\rightarrow " ezone
438 slot{'a}
439 izone `"\\mathrel{|} " ezone
440 math_inr{'z}
441 izone `"\\rightarrow " ezone
442 slot{'b}
443 izone `"}" ezone
444
445 dform math_or_df1 : mode[tex] :: math_or{'a; 'b} =
446 izone `"{" ezone
447 slot{'a}
448 izone `"\\vee " ezone
449 slot{'b}
450 izone `"}" ezone
451
452 dform math_cor_df1 : mode[tex] :: math_cor{'a; 'b} =
453 izone `"{" ezone
454 slot{'a}
455 izone `"\\vee_c " ezone
456 slot{'b}
457 izone `"}" ezone
458
459 (************************************************
460 * Normal display.
461 *)
462 prec prec_inl
463 prec prec_union
464 prec prec_or
465
466 dform union_df : except_mode[tex] :: parens :: "prec"[prec_union] :: math_union{'A; 'B} =
467 slot{'A} " " `"+" " " slot{'B}
468
469 dform inl_df : except_mode[tex] :: parens :: "prec"[prec_inl] :: math_inl{'a} =
470 `"inl" " " slot{'a}
471
472 dform inr_df : except_mode[tex] :: parens :: "prec"[prec_inl] :: math_inr{'a} =
473 `"inr" " " slot{'a}
474
475 dform decide_df : except_mode[tex] :: math_decide{'x; 'y; 'a; 'z; 'b} =
476 szone pushm[0] pushm[3] `"match" " " slot{'x} " " `"with" hspace
477 `"inl " slot{'y} `" -> " slot{'a} popm hspace
478 pushm[3] `" | inr " slot{'z} `" -> " slot{'b} popm popm ezone
479
480 declare or_df{'a}
481
482 dform or_df1 : parens :: "prec"[prec_or] :: math_or{'a; 'b} =
483 szone pushm[0] slot["le"]{'a} or_df{'b} popm ezone
484
485 dform or_df2 : or_df{math_or{'a; 'b}} =
486 or_df{'a} or_df{'b}
487
488 dform or_df3 : or_df{'a} =
489 hspace Nuprl_font!vee " " slot{'a}
490
491 declare cor_df{'a}
492
493 dform cor_df1 : except_mode[tex] :: parens :: "prec"[prec_or] :: math_cor{'a; 'b} =
494 szone pushm[0] slot["le"]{'a} cor_df{'b} popm ezone
495
496 dform cor_df2 : cor_df{math_cor{'a; 'b}} =
497 cor_df{'a} cor_df{'b}
498
499 dform cor_df3 : cor_df{'a} =
500 hspace Nuprl_font!vee `"c" " " slot{'a}
501
502 (************************************************************************
503 * FUNCTIONS
504 ************************************************************************)
505
506 declare math_rfun{'f; 'x; 'A; 'B}
507 declare math_fun{'x; 'A; 'B}
508 declare math_fun{'A; 'B}
509 declare math_lambda{'v; 'b}
510 declare math_apply{'f; 'a}
511 declare math_well_founded{'A; 'x; 'y; 'R}
512 declare math_well_founded_assum{'A; 'a1; 'a2; 'R; 'P}
513 declare math_well_founded_prop{'A}
514 declare math_well_founded_apply{'P; 'a}
515 declare math_fix{'f; 'b}
516
517 declare math_all{'x; 'A; 'B}
518 declare math_implies{'A; 'B}
519 declare math_iff{'A; 'B}
520 declare math_not{'A}
521
522 (************************************************
523 * TeX mode
524 *)
525 dform math_rfun_df1 : mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =
526 izone `"\\left\\{" ezone
527 'f
528 izone `"\\mathrel{|}" ezone
529 'x
530 izone `"\\colon " ezone
531 'A
532 izone `"\\rightarrow " ezone
533 'B
534 izone `"\\right\\}" ezone
535
536 dform math_dfun_df1 : mode[tex] :: math_fun{'x; 'A; 'B} =
537 'x
538 izone `"\\colon " ezone
539 'A
540 izone `"\\rightarrow " ezone
541 'B
542
543 dform math_fun_df1 : mode[tex] :: math_fun{'A; 'B} =
544 'A
545 izone `"\\rightarrow " ezone
546 'B
547
548 dform math_lambda_df1 : mode[tex] :: math_lambda{'v; 'b} =
549 izone `"\\lambda " ezone
550 'v
551 izone `"." ezone
552 'b
553
554 dform math_lambda_df1 : mode[tex] :: math_lambda =
555 izone `"\\lambda " ezone
556
557 dform math_apply_df1 : mode[tex] :: math_apply{'f; 'a} =
558 'f
559 izone `"\\ " ezone
560 'a
561
562 dform math_well_founded_df1 : mode[tex] :: math_well_founded{'A; 'x; 'y; 'R} =
563 izone `"{{\\it well\\_founded}(" ezone
564 'A
565 izone `";" ezone
566 'x
567 izone `"," ezone
568 'y
569 izone `"." ezone
570 'R
571 izone `")}" ezone
572
573 dform math_well_founded_assum_df1 : mode[tex] :: math_well_founded_assum{'A; 'x; 'y; 'R; 'P} =
574 izone `"{{\\it well\\_founded\\_assum}(" ezone
575 'A
576 izone `";" ezone
577 'x
578 izone `"," ezone
579 'y
580 izone `"." ezone
581 'R
582 izone `";" ezone
583 'P
584 izone `")}" ezone
585
586 dform math_well_founded_prop_df1 : mode[tex] :: math_well_founded_prop{'P} =
587 izone `"{{\\it well\\_founded\\_prop}(" ezone
588 'P
589 izone `")}" ezone
590
591 dform math_well_founded_apply_df1 : mode[tex] :: math_well_founded_apply{'P; 'a} =
592 izone `"{{\\it well\\_founded\\_apply}(" ezone
593 'P
594 izone `";" ezone
595 'a
596 izone `")}" ezone
597
598 dform math_fix_df1 : mode[tex] :: math_fix{'f; 'b} =
599 izone `"{{\\it fix}(" ezone
600 'f
601 izone `"." ezone
602 'b
603 izone `")}" ezone
604
605 dform math_all_df1 : mode[tex] :: math_all{'x; 'A; 'B} =
606 izone `"{\\forall " ezone
607 'x
608 izone `"\\colon " ezone
609 'A
610 izone `"." ezone
611 'B
612 izone `"}" ezone
613
614 dform math_implies_df1 : mode[tex] :: math_implies{'A; 'B} =
615 izone `"{" ezone
616 'A
617 izone `"\\Rightarrow " ezone
618 'B
619 izone `"}" ezone
620
621 dform math_iff_df1 : mode[tex] :: math_iff{'A; 'B} =
622 izone `"{" ezone
623 'A
624 izone `"\\Leftrightarrow " ezone
625 'B
626 izone `"}" ezone
627
628 dform math_not_df1 : mode[tex] :: math_not{'A} =
629 izone `"{\\neg " ezone
630 'A
631 izone `"}" ezone
632
633 (************************************************
634 * Normal mode.
635 *)
636 prec prec_fun
637 prec prec_apply
638 prec prec_lambda
639 prec prec_lambda < prec_apply
640 prec prec_fun < prec_apply
641 prec prec_fun < prec_lambda
642
643 prec prec_not
644 prec prec_quant
645 prec prec_iff
646 prec prec_implies
647
648 dform fun_df1 : parens :: "prec"[prec_fun] :: except_mode[tex] :: math_fun{'A; 'B} =
649 slot["le"]{'A} " " rightarrow " " slot["lt"]{'B}
650
651 dform fun_df2 : parens :: "prec"[prec_fun] :: except_mode[tex] :: math_fun{'x; 'A; 'B} =
652 slot{bvar{'x}} `":" slot{'A} " " rightarrow " " slot{'B}
653
654 dform fun_df3 : except_mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =
655 "{" " " slot{bvar{'f}} `" | " math_fun{'x; 'A; 'B} `" }"
656
657 dform apply_df1 : parens :: "prec"[prec_apply] :: except_mode[tex] :: math_apply{'f; 'a} =
658 slot["lt"]{'f} " " slot["le"]{'a}
659
660 dform lambda_df1 : parens :: "prec"[prec_lambda] :: except_mode[tex] :: math_lambda{'x; 'b} =
661 Nuprl_font!lambda slot{'x} `"." slot{'b}
662
663 dform fix_df1 : except_mode[tex] :: except_mode[tex] :: math_fix{'f; 'b} =
664 `"fix" `"(" slot{'f} `"." slot{'b} `")"
665
666 dform well_founded_prop_df : except_mode[tex] :: except_mode[tex] :: math_well_founded_prop{'A} =
667 `"WellFounded " slot{'A} " " rightarrow `" Prop"
668
669 dform well_founded_apply_df : except_mode[tex] :: except_mode[tex] :: math_well_founded_apply{'P; 'a} =
670 slot{'P} `"[" slot{'a} `"]"
671
672 dform well_founded_assum_df : except_mode[tex] :: except_mode[tex] :: math_well_founded_assum{'A; 'a1; 'a2; 'R; 'P} =
673 szone pushm[3] `"WellFounded " Nuprl_font!forall slot{'a2} `":" slot{'A} `"."
674 `"(" Nuprl_font!forall slot{'a1} `":" slot{'A} `". " slot{'R} " " Rightarrow math_well_founded_apply{'P; 'a1} `")"
675 Rightarrow math_well_founded_apply{'P; 'a2} popm ezone
676
677 dform well_founded_df : except_mode[tex] :: except_mode[tex] :: math_well_founded{'A; 'a; 'b; 'R} =
678 szone pushm[3] `"WellFounded " slot{'a} `"," slot{'b} `":" slot{'A} `"." slot{'R} popm ezone
679
680 (*
681 * Quantifiers.
682 *)
683 dform not_df1 : except_mode[tex] :: parens :: "prec"[prec_not] :: math_not{'a} =
684 Nuprl_font!tneg slot["le"]{'a}
685
686 dform implies_df : except_mode[tex] :: parens :: "prec"[prec_implies] :: math_implies{'a; 'b} =
687 slot["le"]{'a} " " Nuprl_font!Rightarrow " " slot["lt"]{'b}
688
689 dform iff_df : except_mode[tex] :: parens :: "prec"[prec_iff] :: math_iff{'a; 'b} =
690 slot["le"]{'a} " " Nuprl_font!Leftrightarrow " " slot["lt"]{'b}
691
692 dform all_df1 : except_mode[tex] :: parens :: "prec"[prec_quant] :: except_mode[tex] :: math_all{'x; 'A; 'B} =
693 pushm[3] Nuprl_font!forall slot{'x} `":" slot{'A} sbreak["",". "] slot{'B} popm
694
695 (************************************************************************
696 * PRODUCT
697 ************************************************************************)
698
699 declare math_prod{'x; 'A; 'B}
700 declare math_prod{'A; 'B}
701 declare math_pair{'a; 'b}
702 declare math_spread{'e; 'u; 'v; 'b}
703 declare math_fst{'e}
704 declare math_snd{'e}
705 declare math_and{'a; 'b}
706 declare math_cand{'a; 'b}
707 declare math_exists{'x; 'A; 'B}
708
709 (************************************************
710 * TeX mode.
711 *)
712 dform math_prod_df1 : mode[tex] :: math_prod{'x; 'A; 'B} =
713 izone `"{" ezone
714 slot{'x}
715 izone `"\\colon " ezone
716 slot{'A}
717 izone `"\\times " ezone
718 slot{'B}
719 izone `"}" ezone
720
721 dform math_prod_df2 : mode[tex] :: math_prod{'A; 'B} =
722 izone `"{" ezone
723 slot{'A}
724 izone `"\\times " ezone
725 slot{'B}
726 izone `"}" ezone
727
728 dform math_pair_df1 : mode[tex] :: math_pair{'a; 'b} =
729 izone `"{(" ezone
730 slot{'a}
731 izone `", " ezone
732 slot{'b}
733 izone `")}" ezone
734
735 dform math_spread_df1 : mode[tex] :: math_spread{'e; 'u; 'v; 'b} =
736 izone `"{\\mathop{{\\bf match}}" ezone
737 slot{'e}
738 izone `"\\mathrel{{\\bf with}}" ezone
739 math_pair{'u; 'v}
740 izone `"\\rightarrow " ezone
741 slot{'b}
742 izone `"}" ezone
743
744 dform math_fst_df1 : mode[tex] :: math_fst{'e} =
745 izone `"{{\\it fst}(" ezone
746 slot{'e}
747 izone `")}" ezone
748
749 dform math_snd_df1 : mode[tex] :: math_snd{'e} =
750 izone `"{{\\it snd}(" ezone
751 slot{'e}
752 izone `")}" ezone
753
754 dform math_and_df1 : mode[tex] :: math_and{'a; 'b} =
755 izone `"{" ezone
756 slot{'a}
757 izone `"\\wedge " ezone
758 slot{'b}
759 izone `"}" ezone
760
761 dform math_cand_df1 : mode[tex] :: math_cand{'a; 'b} =
762 izone `"{" ezone
763 slot{'a}
764 izone `"\\wedge_c " ezone
765 slot{'b}
766 izone `"}" ezone
767
768 dform math_exists_df1 : mode[tex] :: math_exists{'x; 'A; 'B} =
769 izone `"{\\exists " ezone
770 slot{'x}
771 izone `"\\colon " ezone
772 slot{'A}
773 izone `"." ezone
774 slot{'B}
775 izone `"}" ezone
776
777 dform math_exists_df1 : mode[tex] :: math_exists =
778 izone `"\\exists " ezone
779
780 (************************************************
781 * NORMAL MODE
782 *)
783 prec prec_prod
784 prec prec_spread
785 prec prec_and
786
787 prec prec_implies < prec_iff
788 prec prec_iff < prec_or
789 prec prec_or < prec_and
790 prec prec_and < prec_not
791 prec prec_quant < prec_iff
792
793 dform prod_df : parens :: "prec"[prec_prod] :: except_mode[tex] :: math_prod{'A; 'B} =
794 pushm[0] slot{'A} " " times " " slot{'B} popm
795
796 dform prod_df2 : parens :: "prec"[prec_prod] :: except_mode[tex] :: math_prod{'x; 'A; 'B} =
797 slot{'x} `":" slot{'A} " " times " " slot{'B}
798
799 dform pair_prl_df : except_mode[tex] :: except_mode[tex] :: math_pair{'a; 'b} =
800 pushm[0] `"(" slot{'a}`"," slot{'b} `")" popm
801
802 dform spread_prl_df1 : parens :: "prec"[prec_spread] :: except_mode[tex] :: except_mode[tex] :: math_spread{'e; 'u; 'v; 'b} =
803 szone pushm[1]
804 keyword["match"] `" " slot{'e} `" " keyword["with"] hspace
805 math_pair{'u; 'v} `" " Nuprl_font!rightarrow hspace
806 slot{'b}
807 popm ezone
808
809 dform fst_df1 : except_mode[tex] :: except_mode[tex] :: math_fst{'e} =
810 slot{'e} `".1"
811
812 dform snd_df1 : except_mode[tex] :: except_mode[tex] :: math_snd{'e} =
813 slot{'e} `".2"
814
815 declare and_df{'a}
816
817 dform and_df1 : except_mode[tex] :: parens :: "prec"[prec_and] :: math_and{'a; 'b} =
818 szone pushm[0] slot["le"]{'a} and_df{'b} popm ezone
819
820 dform and_df2 : and_df{math_and{'a; 'b}} =
821 and_df{'a} and_df{'b}
822
823 dform and_df3 : and_df{'a} =
824 hspace Nuprl_font!wedge " " slot{'a}
825
826 declare cand_df{'a}
827
828 dform cand_df1 : except_mode[tex] :: parens :: "prec"[prec_and] :: math_cand{'a; 'b} =
829 szone pushm[0] slot["le"]{'a} cand_df{'b} popm ezone
830
831 dform cand_df2 : and_df{math_cand{'a; 'b}} =
832 cand_df{'a} cand_df{'b}
833
834 dform cand_df3 : cand_df{'a} =
835 hspace Nuprl_font!wedge `"c" " " slot{'a}
836
837 dform exists_df1 : except_mode[tex] :: parens :: "prec"[prec_quant] :: except_mode[tex] :: math_exists{'x; 'A; 'B} =
838 pushm[3] Nuprl_font!"exists" slot{'x} `":" slot{'A} sbreak["",". "] slot{'B} popm
839
840 (************************************************************************
841 * SET TYPE
842 ************************************************************************)
843
844 declare math_set{'x; 'A; 'B}
845 declare math_squash{'A}
846
847 (************************************************
848 * TeX mode
849 *)
850
851 dform math_set_df1 : mode[tex] :: math_set{'x; 'A; 'B} =
852 izone `"{\\left\\{" ezone
853 slot{'x}
854 izone `"\\colon " ezone
855 slot{'A}
856 izone `"\\mathrel{|} " ezone
857 slot{'B}
858 izone `"\\right\\}}" ezone
859
860 dform math_squash_df1 : mode[tex] :: math_squash{'A} =
861 izone `"\\sq{" ezone
862 slot{'A}
863 izone `"}" ezone
864
865 (************************************************
866 * Normal mode
867 *)
868 dform set_df1 : except_mode[tex] :: math_set{'x; 'A; 'B} =
869 pushm[3] `"{ " bvar{'x} `":" slot{'A} `" | " slot{'B} `"}" popm
870
871 dform math_squash_df2 : except_mode[tex] :: math_squash{'A} = "[" 'A "]"
872
873 (************************************************************************
874 * Decidable
875 ************************************************************************)
876
877 declare math_decidable{'P}
878
879 (************************************************
880 * TeX mode
881 *)
882
883 dform math_decidable_df1 : mode[tex] :: math_decidable{'P} =
884 izone `"{{\\it decidable}(" ezone
885 slot{'P}
886 izone `")}" ezone
887
888 (************************************************
889 * Normal mode
890 *)
891 dform decidable_df1 : except_mode[tex] :: math_decidable{'A} =
892 `"decidable(" slot{'A} `")"
893
894 (************************************************************************
895 * INTERSECTION
896 ************************************************************************)
897
898 declare math_isect{'x; 'A; 'B}
899 declare math_top
900 declare math_record{'t}
901 declare math_bisect{'A; 'B}
902
903 (************************************************
904 * TeX mode
905 *)
906
907 dform math_isect_df1 : mode[tex] :: math_isect{'x; 'A; 'B} =
908 izone `"{\\bigcap_{" ezone
909 slot{'x}
910 izone `"\\colon " ezone
911 slot{'A}
912 izone `"} " ezone
913 slot{'B}
914 izone `"}" ezone
915
916 dform math_record_df1 : mode[tex] :: math_record{'t} =
917 izone `"{\\left\\{" ezone
918 slot{'t}
919 izone `"\\right\\}}" ezone
920
921 dform math_bisect_df1 : mode[tex] :: math_bisect{'A; 'B} =
922 izone `"{" ezone
923 slot{'A}
924 izone `"\\cap " ezone
925 slot{'B}
926 izone `"}" ezone
927
928 (************************************************
929 * Normal mode
930 *)
931 dform isect_df1 : except_mode[tex] :: math_isect{'x; 'A; 'B} =
932 cap slot{'x} `":" slot{'A} `"." slot{'B}
933
934 dform top_df : math_top =
935 math_i["Top"]
936
937 dform record_df : except_mode[tex] :: math_record{'t} =
938 pushm[0] szone `"{ " pushm[0] 't popm hspace `"}" ezone popm
939
940 prec prec_bisect
941
942 dform bisect_df : except_mode[tex] :: parens :: "prec"[prec_bisect] :: math_bisect{'A; 'B} =
943 slot["le"]{'A} `" " cap space slot{'B}
944
945 (************************************************************************
946 * UNION
947 ************************************************************************)
948
949 declare math_tunion{'x; 'A; 'B}
950 declare math_bunion{'A; 'B}
951
952 (************************************************
953 * TeX mode
954 *)
955
956 dform math_tunion_df1 : mode[tex] :: math_tunion{'x; 'A; 'B} =
957 izone `"{\\bigcup_{" ezone
958 slot{'x}
959 izone `"\\colon " ezone
960 slot{'A}
961 izone `"} " ezone
962 slot{'B}
963 izone `"}" ezone
964
965 dform math_bunion_df1 : mode[tex] :: math_bunion{'A; 'B} =
966 izone `"{" ezone
967 slot{'A}
968 izone `"\\cup " ezone
969 slot{'B}
970 izone `"}" ezone
971
972 (************************************************
973 * Normal mode
974 *)
975 dform tunion_df1 : except_mode[tex] :: math_tunion{'x; 'A; 'B} =
976 cup slot{'x} `":" slot{'A} `"." slot{'B}
977
978 prec prec_bunion
979
980 dform bunion_df : except_mode[tex] :: parens :: "prec"[prec_bunion] :: math_bunion{'A; 'B} =
981 slot["le"]{'A} `" " cup space slot{'B}
982
983 (************************************************************************
984 * RECURSIVE TYPES
985 ************************************************************************)
986
987 declare math_srec{'T; 'B}
988 declare math_prec{'T; 'y; 'B; 'a}
989 declare math_srecind{'t; 'a; 'b; 'c}
990 declare math_precind{'t; 'a; 'b; 'c}
991
992 declare math_w{'x; 'A; 'B}
993 declare math_tree{'a; 'f}
994 declare math_treeind{'z; 'a; 'f; 'g; 'body}
995
996 declare math_nil
997 declare math_cons{'a; 'b}
998 declare math_list{'l}
999 declare math_listind{'e; 'base; 'h; 't; 'f; 'step}
1000
1001 (************************************************
1002 * TeX mode
1003 *)
1004 dform math_srec_df1 : mode[tex] :: math_srec{'T; 'B} =
1005 izone `"{\\mu(" ezone
1006 slot{'T}
1007 izone `"." ezone
1008 slot{'B}
1009 izone `")}" ezone
1010
1011 dform math_srecind_df1 : mode[tex] :: math_srecind{'t; 'a; 'b; 'c} =
1012 izone `"{{\\it srec\\_ind}(" ezone
1013 slot{'t}
1014 izone `";" ezone
1015 slot{'a}
1016 izone `"," ezone
1017 slot{'b}
1018 izone `"." ezone
1019 slot{'c}
1020 izone `")}" ezone
1021
1022 dform math_prec_df1 : mode[tex] :: math_prec{'T; 'x; 'B; 'a} =
1023 izone `"{\\mu(" ezone
1024 slot{'T}
1025 izone `"," ezone
1026 slot{'x}
1027 izone `"." ezone
1028 slot{'B}
1029 izone `";" ezone
1030 slot{'a}
1031 izone `")}" ezone
1032
1033 dform math_precind_df1 : mode[tex] :: math_precind{'t; 'a; 'b; 'c} =
1034 izone `"{{\\it prec\\_ind}(" ezone
1035 slot{'t}
1036 izone `";" ezone
1037 slot{'a}
1038 izone `"," ezone
1039 slot{'b}
1040 izone `"." ezone
1041 slot{'c}
1042 izone `")}" ezone
1043
1044 dform math_w_df1 : mode[tex] :: math_w{'x; 'A; 'B} =
1045 izone `"{\\mathop{\\it W}(" ezone
1046 slot{'x}
1047 izone `"\\colon " ezone
1048 slot{'A}
1049 izone `"." ezone
1050 slot{'B}
1051 izone `")}" ezone
1052
1053 dform math_tree_df1 : mode[tex] :: math_tree{'A; 'B} =
1054 izone `"{{\\it tree}(" ezone
1055 slot{'A}
1056 izone `";" ezone
1057 slot{'B}
1058 izone `")}" ezone
1059
1060 dform math_treeind_df1 : mode[tex] :: math_treeind{'t; 'a; 'b; 'c; 'd} =
1061 izone `"{{\\it prec\\_ind}(" ezone
1062 slot{'t}
1063 izone `";" ezone
1064 slot{'a}
1065 izone `"," ezone
1066 slot{'b}
1067 izone `"," ezone
1068 slot{'c}
1069 izone `"." ezone
1070 slot{'d}
1071 izone `")}" ezone
1072
1073 dform math_nil_df1 : mode[tex] :: math_nil =
1074 izone `"{\\it nil}" ezone
1075
1076 dform math_cons_df1 : mode[tex] :: math_cons{'h; 't} =
1077 izone `"{{\\it cons}(" ezone
1078 slot{'h}
1079 izone `"," ezone
1080 slot{'t}
1081 izone `")}" ezone
1082
1083 dform math_list_df1 : mode[tex] :: math_list{'l} =
1084 izone `"{{\\it list}(" ezone
1085 slot{'l}
1086 izone `")}" ezone
1087
1088 dform math_listind_df1 : mode[tex] :: math_listind{'e; 'base; 'h; 't; 'f; 'step} =
1089 izone `"{\\mathop{\\bf match}" ezone
1090 slot{'e}
1091 izone `"\\mathrel{\\bf with}" ezone
1092 math_cons{'h; 't}
1093 izone `"." ezone
1094 slot{'f}
1095 izone `"\\rightarrow " ezone
1096 slot{'step}
1097 izone `"}" ezone
1098
1099 (************************************************
1100 * Normal mode
1101 *)
1102 dform srec_df : except_mode[tex] :: math_srec{'T; 'B} =
1103 szone mu `"{" slot{'T} `"." pushm[0] slot{'B} `"}" popm ezone
1104
1105 prec prec_w
1106 prec prec_tree_ind
1107
1108 dform w_df : except_mode[tex] :: parens :: "prec"[prec_w] :: math_w{'x; 'A; 'B} =
1109 mathbbW slot{'x} `":" slot{'A} `"." slot{'B}
1110
1111 dform tree_df : except_mode[tex] :: math_tree{'a; 'f} =
1112 `"tree(" slot{'a} `"," " " slot{'f} `")"
1113
1114 dform tree_ind_df : except_mode[tex] :: parens :: "prec"[prec_tree_ind] :: math_treeind{'z; 'a; 'f; 'g; 'body} =
1115 szone pushm[3] `"tree_ind(" slot{'g} `"." " "
1116 pushm[3] `"let tree(" slot{'a} `", " slot{'f} `") =" space slot{'z} space `"in" popm space
1117 slot{'body} popm ezone
1118
1119 prec prec_cons
1120 prec prec_list
1121
1122 declare search{'a; 'b}
1123 declare semicolons{'a}
1124 declare colons{'a}
1125
1126 (* Empty list *)
1127 dform nil_df : except_mode[tex] :: math_nil = `"[]"
1128
1129 (* Search for nil entry *)
1130 dform cons_df : except_mode[tex] :: math_cons{'a; 'b} =
1131 search{math_cons{'a; math_nil}; 'b}
1132
1133 (* Keep searching down the list *)
1134 dform search_df1 : search{'a; math_cons{'b; 'c}} =
1135 search{math_cons{'b; 'a}; 'c}
1136
1137 (* Found a nil terminator: use bracket notation *)
1138 dform search_df2 : search{'a; math_nil} =
1139 `"[" semicolons{'a} `"]"
1140
1141 (* No nil terminator, so use :: notation *)
1142 dform search_df3 : search{'a; 'b} =
1143 colons{'a} `"::" slot{'b}
1144
1145 (* Reverse entries and separate with ; *)
1146 dform semicolons_df1 : semicolons{math_cons{'a; math_nil}} =
1147 slot{'a}
1148
1149 dform semicolons_df2 : semicolons{math_cons{'a; 'b}} =
1150 semicolons{'b} `";" slot{'a}
1151
1152 (* Reverse entries and separate with :: *)
1153 dform colons_df1 : colons{math_cons{'a; math_nil}} =
1154 slot{'a}
1155
1156 dform colons_df2 : colons{math_cons{'a; 'b}} =
1157 colons{'b} `"::" slot{'a}
1158
1159 dform list_df1 : except_mode[tex] :: parens :: "prec"[prec_list] :: math_list{'a} =
1160 slot{'a} `" List"
1161
1162 dform list_ind_df1 : except_mode[tex] :: parens :: "prec"[prec_list] :: math_listind{'e; 'base; 'h; 't; 'f; 'step} =
1163 szone pushm[1] pushm[3]
1164 `"match " slot{'e} `" with" hspace
1165 `" [] ->" hspace slot{'base} popm hspace
1166 `"| " pushm[0] slot{'h} `"::" slot{'t} `"." slot{'f} `" ->" hspace slot{'step} popm popm ezone
1167
1168 (************************************************************************
1169 * QUOTIENT TYPE
1170 ************************************************************************)
1171
1172 declare math_quot{'T; 'x; 'y; 'E}
1173 declare math_esquash{'P}
1174
1175 (************************************************
1176 * TeX
1177 *)
1178 dform math_quot_df1 : mode[tex] :: math_quot{'T; 'x; 'y; 'E} =
1179 izone `"{" ezone
1180 slot{'x}
1181 izone `"," ezone
1182 slot{'y}
1183 izone `"\\colon " ezone
1184 slot{'T}
1185 izone `"// " ezone
1186 slot{'E}
1187 izone `"}" ezone
1188
1189 dform math_esquash_df1 : mode[tex] :: math_esquash{'P} =
1190 izone `"[\!" ezone
1191 `"[" slot{'P} `"]"
1192 izone `"\!]" ezone
1193
1194 (************************************************
1195 * Normal mode
1196 *)
1197
1198 prec prec_quot
1199
1200 dform quot_df1 : except_mode[tex] :: parens :: "prec"[prec_quot] :: math_quot{'A; 'x; 'y; 'E} =
1201 slot{'x} `", " slot{'y} `":" " " slot{'A} `" // " slot{'E}
1202
1203 dform math_esquash_df2 : except_mode[tex] :: math_esquash{'P} =
1204 `"[[" slot{'P} `"]]"
1205
1206 (*
1207 * -*-
1208 * Local Variables:
1209 * Caml-master: "compile"
1210 * End:
1211 * -*-
1212 *)

Properties

Name Value
svn:eol-style native
svn:keywords Author Date Id Revision

  ViewVC Help
Powered by ViewVC 1.1.26