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/.
30 let out t s = if !O.verbose_parser then prerr_endline ("-- " ^ t ^ " " ^ s)
32 let trim = HExtlib.trim_blanks
36 let cat x = String.concat " " x
38 let mk_vars local idents =
39 let kind = if local then T.Var else T.Con in
40 let map ident = T.Inline (local, kind, trim ident, "", None) in
44 String.sub s 1 (String.length s - 2)
47 String.sub s 1 (String.length s - 1)
50 [T.Coercion (false, str); T.Coercion (true, str)]
53 [T.Notation (false, str); T.Notation (true, str)]
57 | "Remark" -> Some `Remark
58 | "Lemma" -> Some `Lemma
59 | "Theorem" -> Some `Theorem
60 | "Definition" -> Some `Definition
61 | "Fixpoint" -> Some `Definition
62 | "CoFixpoint" -> Some `Definition
63 | "Let" -> Some `Definition
64 | "Scheme" -> Some `Theorem
68 let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem) in
69 List.rev_map generate ["2"; "1"]
72 %token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC CM
73 %token <string> WITH ABBR IN LET TH PROOF QED VAR AX IND GEN SEC END UNX REQ XP SET NOT LOAD ID COERC MOR
77 %type <Types.items> items
79 /* SPACED TOKENS ************************************************************/
81 ident: xident spcs { $1 ^ $2 };
82 fs: FS spcs { $1 ^ $2 };
83 mor: MOR spcs { $1 ^ $2 };
84 th: TH spcs { $1 ^ $2 };
85 xlet: LET spcs { $1 ^ $2 };
86 proof: PROOF spcs { $1 ^ $2 };
87 qed: QED spcs { $1 ^ $2 };
88 gen: GEN spcs { $1 ^ $2 };
89 sec: SEC spcs { $1 ^ $2 };
90 xend: END spcs { $1 ^ $2 };
91 unx: UNX spcs { $1 ^ $2 };
92 def: DEF spcs { $1 ^ $2 };
93 op: OP spcs { $1 ^ $2 };
94 abbr: ABBR spcs { $1 ^ $2 };
95 var: VAR spcs { $1 ^ $2 };
96 ax: AX spcs { $1 ^ $2 };
97 req: REQ spcs { $1 ^ $2 };
98 load: LOAD spcs { $1 ^ $2 };
99 xp: XP spcs { $1 ^ $2 };
100 ind: IND spcs { $1 ^ $2 };
101 set: SET spcs { $1 ^ $2 };
102 notation: NOT spcs { $1 ^ $2 };
103 oc: OC spcs { $1 ^ $2 };
104 coe: COE spcs { $1 ^ $2 };
105 cn: CN spcs { $1 ^ $2 };
106 sc: SC spcs { $1 ^ $2 };
107 str: STR spcs { $1 ^ $2 };
108 id: ID spcs { $1 ^ $2 };
109 coerc: COERC spcs { $1 ^ $2 };
110 cm: CM spcs { $1 ^ $2 } | { "" }
111 wh: WITH spcs { $1 ^ $2 };
113 /* SPACES *******************************************************************/
116 | OQ verbatims CQ { $1 ^ $2 ^ $3 }
124 | spc spcs { $1 ^ $2 }
128 | SPC rspcs { $1 ^ $2 }
131 /* IDENTIFIERS **************************************************************/
156 | outer_keyword { $1 }
161 | qid AC { strip1 $2 :: $1 }
165 | ident cm idents { $1 :: $3 }
168 /* PLAIN SKIP ***************************************************************/
172 | inner_keyword { $1 }
185 | outer_keyword { $1 }
194 /* LEFT SKIP ****************************************************************/
197 | plain_skip { $1, [] }
198 | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
199 | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 }
204 | outer_keyword { $1, [] }
210 | xlskip spcs { fst $1 ^ $2, snd $1 }
211 | xlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
214 | rlskip spcs { fst $1 ^ $2, snd $1 }
215 | rlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
222 /* GENERAL SKIP *************************************************************/
229 | outer_keyword { $1, [] }
235 | xskip spcs { fst $1 ^ $2, snd $1 }
236 | xskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
239 | rskip spcs { fst $1 ^ $2, snd $1 }
240 | rskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
243 /* ABBREVIATION SKIP ********************************************************/
246 | inner_skip { $1, [] }
247 | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
248 | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 }
251 | li_skip spcs { fst $1 ^ $2, snd $1 }
252 | li_skip spcs li_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
255 /* PARENTETIC SKIP **********************************************************/
258 | inner_skip { $1, [] }
259 | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
260 | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 }
264 | ocp_skip spcs { fst $1 ^ $2, snd $1 }
265 | ocp_skip spcs ocp_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
268 /* VERBATIM SKIP ************************************************************/
281 | verbatim verbatims { $1 ^ $2 }
284 /* PROOF STEPS **************************************************************/
288 | skips FS { snd $1 }
292 | step spcs steps { $1 @ $3 }
296 | proof fs steps qed { $3 }
297 | proof skips { snd $2 }
298 | proof wh skips fs steps qed { snd $3 @ $5 }
301 | th ident opt_lskips def xskips FS
303 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
305 | th ident lskips fs just FS
307 $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
309 | gen ident def xskips FS
311 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
313 | mor ident cn ident fs just FS
314 { out "MOR" $4; $6 @ mk_morphism (trim $4) }
315 | xlet ident opt_lskips def xskips FS
317 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
319 | xlet ident lskips fs just FS
321 $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
323 | var idents cn xskips FS
324 { out "VAR" (cat $2); mk_vars true $2 }
325 | ax idents cn xskips FS
326 { out "AX" (cat $2); mk_vars false $2 }
329 T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
332 { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] }
334 { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] }
336 { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
338 { out "REQ" $3; [T.Include (trim $3)] }
340 { out "REQ" $2; [T.Include (trim $2)] }
342 { out "REQ" $2; [T.Include (strip2 (trim $2))] }
343 | coerc qid spcs skips FS
344 { out "COERCE" (hd $2); coercion (hd $2) }
345 | id coerc qid spcs skips FS
346 { out "COERCE" (hd $3); coercion (hd $3) }
348 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
350 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
353 out "ERROR" vs; failwith ("macro_step " ^ vs) }
356 out "ERROR" vs; failwith ("macro_step " ^ vs) }
359 /* VERNACULAR ITEMS *********************************************************/
362 | OQ verbatims CQ { [T.Comment $2] }
364 | set xskips FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
365 | notation xskips FS { notation ($1 ^ fst $2 ^ trim $3) }
366 | error { out "ERROR" "item"; failwith "item" }
370 | rspcs item items { $2 @ $3 }
380 | cnot spcs { $1 ^ $2 }
381 | cnot spcs cnots { $1 ^ $2 ^ $3 }
394 | abbr extends0 IN { $1 ^ $2 ^ $3 }
395 | op extends1 CP { $1 ^ $2 ^ $3 }
414 | restrict spcs { $1 ^ $2 }
415 | restrict spcs restricts { $1 ^ $2 ^ $3 }
418 | xre spcs { $1 ^ $2 }
419 | xre spcs restricts { $1 ^ $2 ^ $3 }
426 | extend0 spcs { $1 ^ $2 }
427 | extend0 spcs extends0 { $1 ^ $2 ^ $3 }
435 | extend1 spcs { $1 ^ $2 }
436 | extend1 spcs extends1 { $1 ^ $2 ^ $3 }
457 | unexport_rr { $1, [] }
458 | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 }
459 | oc unexport_ff CC { $1, [] }
462 | unexport_r spcs { fst $1 ^ $2, snd $1 }
463 | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
466 | ident cn unexports_r
467 { $1 ^ $2 ^ fst $3, snd $3 }
468 | ident def unexports_r
469 { $1 ^ $2 ^ fst $3, snd $3 }
470 | ident coe unexports_r
471 { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
475 | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
477 | error { out "ERROR" "fields"; failwith "fields" }
489 | unexport spcs { fst $1 ^ $2, snd $1 }
490 | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
494 | reserved_ident { $1 }
506 | verbatim verbatims { $1 ^ $2 }
510 | restricts FS { [] }
514 | step spcs steps { $1 @ $3 }
518 | th ident restricts fs proof FS steps qed FS
520 $7 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
522 | th ident restricts fs proof restricts FS
524 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
526 | th ident restricts fs steps qed FS
528 $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
530 | th ident restricts def restricts FS
532 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
534 | th ident def restricts FS
536 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
538 | gen ident def restricts FS
540 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
542 | xlet ident restricts fs proof FS steps qed FS
544 $7 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
546 | xlet ident restricts fs proof restricts FS
548 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
550 | xlet ident restricts fs steps qed FS
552 $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
554 | xlet ident restricts def restricts FS
556 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
558 | xlet ident def restricts FS
560 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
563 { out "VAR" (cat $2); mk_vars true $2 }
565 { out "AX" (cat $2); mk_vars false $2 }
566 | ind ident unexports FS
568 T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
571 { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] }
573 { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] }
575 { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
577 { out "REQ" $3; [T.Include (trim $3)] }
579 { out "REQ" $3; [T.Include (trim $3)] }
581 { out "REQ" $2; [T.Include (trim $2)] }
583 { out "REQ" $2; [T.Include (strip2 (trim $2))] }
584 | coerc qid spcs cn unexports FS
585 { out "COERCE" (hd $2); coercion (hd $2) }
586 | id coerc qid spcs cn unexports FS
587 { out "COERCE" (hd $3); coercion (hd $3) }
589 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
591 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
594 out "ERROR" vs; failwith ("macro_step " ^ vs) }
597 out "ERROR" vs; failwith ("macro_step " ^ vs) }
600 | OQ verbatims CQ { [T.Comment $2] }
602 | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
603 | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) }
604 | error { out "ERROR" "item"; failwith "item" }
608 | rspcs item items { $2 @ $3 }