1 /* Copyright (C) 2000, HELM Team.
3 * This file is part of HELM, an Hypertextual, Electronic
4 * Library of Mathematics, developed at the Computer Science
5 * Department, University of Bologna, Italy.
7 * HELM is free software; you can redistribute it and/or
8 * modify it under the terms of the GNU General Public License
9 * as published by the Free Software Foundation; either version 2
10 * of the License, or (at your option) any later version.
12 * HELM is distributed in the hope that it will be useful,
13 * but WITHOUT ANY WARRANTY; without even the implied warranty of
14 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
15 * GNU General Public License for more details.
17 * You should have received a copy of the GNU General Public License
18 * along with HELM; if not, write to the Free Software
19 * Foundation, Inc., 59 Temple Place - Suite 330, Boston,
22 * For details, see the HELM World-Wide-Web page,
23 * http://cs.unibo.it/helm/.
29 let out t s = prerr_endline ("-- " ^ t ^ " " ^ s)
31 let trim = HExtlib.trim_blanks
35 let cat x = String.concat " " x
37 let mk_vars local idents =
38 let kind = if local then T.Var else T.Con in
39 let map ident = T.Inline (local, kind, trim ident, "", None) in
43 String.sub s 1 (String.length s - 2)
46 String.sub s 1 (String.length s - 1)
49 [T.Coercion (false, str); T.Coercion (true, str)]
52 [T.Notation (false, str); T.Notation (true, str)]
56 | "Remark" -> Some `Remark
57 | "Lemma" -> Some `Lemma
58 | "Theorem" -> Some `Theorem
59 | "Definition" -> Some `Definition
60 | "Fixpoint" -> Some `Definition
61 | "Let" -> Some `Definition
62 | "Scheme" -> Some `Theorem
66 let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem) in
67 List.rev_map generate ["2"; "1"]
70 %token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC CM
71 %token <string> WITH ABBR IN LET TH PROOF QED VAR AX IND GEN SEC END UNX REQ XP SET NOT LOAD ID COERC MOR
75 %type <Types.items> items
77 /* SPACED TOKENS ************************************************************/
79 ident: xident spcs { $1 ^ $2 };
80 fs: FS spcs { $1 ^ $2 };
81 mor: MOR spcs { $1 ^ $2 };
82 th: TH spcs { $1 ^ $2 };
83 xlet: LET spcs { $1 ^ $2 };
84 proof: PROOF spcs { $1 ^ $2 };
85 qed: QED spcs { $1 ^ $2 };
86 gen: GEN spcs { $1 ^ $2 };
87 sec: SEC spcs { $1 ^ $2 };
88 xend: END spcs { $1 ^ $2 };
89 unx: UNX spcs { $1 ^ $2 };
90 def: DEF spcs { $1 ^ $2 };
91 op: OP spcs { $1 ^ $2 };
92 abbr: ABBR spcs { $1 ^ $2 };
93 var: VAR spcs { $1 ^ $2 };
94 ax: AX spcs { $1 ^ $2 };
95 req: REQ spcs { $1 ^ $2 };
96 load: LOAD spcs { $1 ^ $2 };
97 xp: XP spcs { $1 ^ $2 };
98 ind: IND spcs { $1 ^ $2 };
99 set: SET spcs { $1 ^ $2 };
100 notation: NOT spcs { $1 ^ $2 };
101 oc: OC spcs { $1 ^ $2 };
102 coe: COE spcs { $1 ^ $2 };
103 cn: CN spcs { $1 ^ $2 };
104 sc: SC spcs { $1 ^ $2 };
105 str: STR spcs { $1 ^ $2 };
106 id: ID spcs { $1 ^ $2 };
107 coerc: COERC spcs { $1 ^ $2 };
108 cm: CM spcs { $1 ^ $2 } | { "" }
109 wh: WITH spcs { $1 ^ $2 };
111 /* SPACES *******************************************************************/
114 | OQ verbatims CQ { $1 ^ $2 ^ $3 }
122 | spc spcs { $1 ^ $2 }
126 | SPC rspcs { $1 ^ $2 }
129 /* IDENTIFIERS **************************************************************/
154 | outer_keyword { $1 }
159 | qid AC { strip1 $2 :: $1 }
163 | ident cm idents { $1 :: $3 }
166 /* PLAIN SKIP ***************************************************************/
170 | inner_keyword { $1 }
183 | outer_keyword { $1 }
192 /* LEFT SKIP ****************************************************************/
195 | plain_skip { $1, [] }
196 | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
197 | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 }
202 | outer_keyword { $1, [] }
208 | xlskip spcs { fst $1 ^ $2, snd $1 }
209 | xlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
212 | rlskip spcs { fst $1 ^ $2, snd $1 }
213 | rlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
220 /* GENERAL SKIP *************************************************************/
227 | outer_keyword { $1, [] }
233 | xskip spcs { fst $1 ^ $2, snd $1 }
234 | xskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
237 | rskip spcs { fst $1 ^ $2, snd $1 }
238 | rskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
241 /* ABBREVIATION SKIP ********************************************************/
244 | inner_skip { $1, [] }
245 | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
246 | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 }
249 | li_skip spcs { fst $1 ^ $2, snd $1 }
250 | li_skip spcs li_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
253 /* PARENTETIC SKIP **********************************************************/
256 | inner_skip { $1, [] }
257 | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
258 | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 }
262 | ocp_skip spcs { fst $1 ^ $2, snd $1 }
263 | ocp_skip spcs ocp_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
266 /* VERBATIM SKIP ************************************************************/
279 | verbatim verbatims { $1 ^ $2 }
282 /* PROOF STEPS **************************************************************/
286 | skips FS { snd $1 }
290 | step spcs steps { $1 @ $3 }
294 | proof fs steps qed { $3 }
295 | proof skips { snd $2 }
296 | proof wh skips fs steps qed { snd $3 @ $5 }
299 | th ident opt_lskips def xskips FS
301 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
303 | th ident lskips fs just FS
305 $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
307 | gen ident def xskips FS
309 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
311 | mor ident cn ident fs just FS
312 { out "MOR" $4; $6 @ mk_morphism (trim $4) }
313 | xlet ident opt_lskips def xskips FS
315 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
317 | xlet ident lskips fs just FS
319 $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
321 | var idents cn xskips FS
322 { out "VAR" (cat $2); mk_vars true $2 }
323 | ax idents cn xskips FS
324 { out "AX" (cat $2); mk_vars false $2 }
327 T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
330 { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] }
332 { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] }
334 { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
336 { out "REQ" $3; [T.Include (trim $3)] }
338 { out "REQ" $2; [T.Include (trim $2)] }
340 { out "REQ" $2; [T.Include (strip2 (trim $2))] }
341 | coerc qid spcs skips FS
342 { out "COERCE" (hd $2); coercion (hd $2) }
343 | id coerc qid spcs skips FS
344 { out "COERCE" (hd $3); coercion (hd $3) }
346 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
348 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
351 out "ERROR" vs; failwith ("macro_step " ^ vs) }
354 out "ERROR" vs; failwith ("macro_step " ^ vs) }
357 /* VERNACULAR ITEMS *********************************************************/
360 | OQ verbatims CQ { [T.Comment $2] }
362 | set xskips FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
363 | notation xskips FS { notation ($1 ^ fst $2 ^ trim $3) }
364 | error { out "ERROR" "item"; failwith "item" }
368 | rspcs item items { $2 @ $3 }
378 | cnot spcs { $1 ^ $2 }
379 | cnot spcs cnots { $1 ^ $2 ^ $3 }
392 | abbr extends0 IN { $1 ^ $2 ^ $3 }
393 | op extends1 CP { $1 ^ $2 ^ $3 }
412 | restrict spcs { $1 ^ $2 }
413 | restrict spcs restricts { $1 ^ $2 ^ $3 }
416 | xre spcs { $1 ^ $2 }
417 | xre spcs restricts { $1 ^ $2 ^ $3 }
424 | extend0 spcs { $1 ^ $2 }
425 | extend0 spcs extends0 { $1 ^ $2 ^ $3 }
433 | extend1 spcs { $1 ^ $2 }
434 | extend1 spcs extends1 { $1 ^ $2 ^ $3 }
455 | unexport_rr { $1, [] }
456 | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 }
457 | oc unexport_ff CC { $1, [] }
460 | unexport_r spcs { fst $1 ^ $2, snd $1 }
461 | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
464 | ident cn unexports_r
465 { $1 ^ $2 ^ fst $3, snd $3 }
466 | ident def unexports_r
467 { $1 ^ $2 ^ fst $3, snd $3 }
468 | ident coe unexports_r
469 { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
473 | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
475 | error { out "ERROR" "fields"; failwith "fields" }
487 | unexport spcs { fst $1 ^ $2, snd $1 }
488 | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
492 | reserved_ident { $1 }
504 | verbatim verbatims { $1 ^ $2 }
508 | restricts FS { [] }
512 | step spcs steps { $1 @ $3 }
516 | th ident restricts fs proof FS steps qed FS
518 $7 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
520 | th ident restricts fs proof restricts FS
522 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
524 | th ident restricts fs steps qed FS
526 $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
528 | th ident restricts def restricts FS
530 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
532 | th ident def restricts FS
534 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
536 | gen ident def restricts FS
538 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
540 | xlet ident restricts fs proof FS steps qed FS
542 $7 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
544 | xlet ident restricts fs proof restricts FS
546 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
548 | xlet ident restricts fs steps qed FS
550 $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
552 | xlet ident restricts def restricts FS
554 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
556 | xlet ident def restricts FS
558 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
561 { out "VAR" (cat $2); mk_vars true $2 }
563 { out "AX" (cat $2); mk_vars false $2 }
564 | ind ident unexports FS
566 T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
569 { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] }
571 { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] }
573 { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
575 { out "REQ" $3; [T.Include (trim $3)] }
577 { out "REQ" $3; [T.Include (trim $3)] }
579 { out "REQ" $2; [T.Include (trim $2)] }
581 { out "REQ" $2; [T.Include (strip2 (trim $2))] }
582 | coerc qid spcs cn unexports FS
583 { out "COERCE" (hd $2); coercion (hd $2) }
584 | id coerc qid spcs cn unexports FS
585 { out "COERCE" (hd $3); coercion (hd $3) }
587 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
589 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
592 out "ERROR" vs; failwith ("macro_step " ^ vs) }
595 out "ERROR" vs; failwith ("macro_step " ^ vs) }
598 | OQ verbatims CQ { [T.Comment $2] }
600 | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
601 | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) }
602 | error { out "ERROR" "item"; failwith "item" }
606 | rspcs item items { $2 @ $3 }