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

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

Parent Directory Parent Directory | Revision Log Revision Log


Revision 3584 - (hide 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 jyh 3058 (*!
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 nogin 3235 prec prec_type
45     prec prec_equal
46    
47 jyh 3058 (************************************************
48     * TeX mode.
49     *)
50     dform math_type_df1 : mode[tex] :: math_type{'t} =
51     slot{'t}
52 nogin 3235 izone `"\\,\\mathtt{" ezone
53     `"Type"
54     izone "}" ezone
55 jyh 3058
56 nogin 3223 dform math_univ_df : mode[tex] :: math_univ{'i} =
57 nogin 3235 izone `"{\\mathbb U}_{" ezone
58 jyh 3058 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 nogin 3223 declare math_bnot{'a}
166 jyh 3058 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 nogin 3324 izone `"\\mathop{\\bf if}" ezone
214     szone{'a}
215 jyh 3058 izone `"\\mathrel{\\bf then}" ezone
216 nogin 3324 szone{'b}
217 jyh 3058 izone `"\\mathrel{\\bf else}" ezone
218 nogin 3324 szone{'c}
219 jyh 3058
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 nogin 3324 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 jyh 3058
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 nogin 3223 declare math_fun{'x; 'A; 'B}
508 jyh 3058 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 nogin 3584 izone `"\\left\\{" ezone
527 jyh 3058 'f
528     izone `"\\mathrel{|}" ezone
529     'x
530     izone `"\\colon " ezone
531     'A
532     izone `"\\rightarrow " ezone
533     'B
534 nogin 3584 izone `"\\right\\}" ezone
535 jyh 3058
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 nogin 3584 izone `"\\lambda " ezone
550 jyh 3058 '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 nogin 3223 dform fun_df3 : except_mode[tex] :: math_rfun{'f; 'x; 'A; 'B} =
655     "{" " " slot{bvar{'f}} `" | " math_fun{'x; 'A; 'B} `" }"
656 jyh 3058
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 nogin 3223 declare math_prod{'A; 'B}
701 jyh 3058 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 nogin 3232 declare math_squash{'A}
846 jyh 3058
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 nogin 3232 dform math_squash_df1 : mode[tex] :: math_squash{'A} =
861     izone `"\\sq{" ezone
862 jyh 3058 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 nogin 3232 dform math_squash_df2 : except_mode[tex] :: math_squash{'A} = "[" 'A "]"
872 jyh 3058
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 nogin 3223 dform math_treeind_df1 : mode[tex] :: math_treeind{'t; 'a; 'b; 'c; 'd} =
1061 jyh 3058 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 nogin 3223 dform srec_df : except_mode[tex] :: math_srec{'T; 'B} =
1103 jyh 3058 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 nogin 3223 declare semicolons{'a}
1124     declare colons{'a}
1125 jyh 3058
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 nogin 3325 izone `"[\!" ezone
1191     `"[" slot{'P} `"]"
1192     izone `"\!]" ezone
1193 jyh 3058
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 nogin 3325 dform math_esquash_df2 : except_mode[tex] :: math_esquash{'P} =
1204     `"[[" slot{'P} `"]]"
1205 jyh 3058
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