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 | "Let" -> Some `Definition
63 | "Scheme" -> Some `Theorem
67 let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem) in
68 List.rev_map generate ["2"; "1"]
71 %token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC CM
72 %token <string> WITH ABBR IN LET TH PROOF QED VAR AX IND GEN SEC END UNX REQ XP SET NOT LOAD ID COERC MOR
76 %type <Types.items> items
78 /* SPACED TOKENS ************************************************************/
80 ident: xident spcs { $1 ^ $2 };
81 fs: FS spcs { $1 ^ $2 };
82 mor: MOR spcs { $1 ^ $2 };
83 th: TH spcs { $1 ^ $2 };
84 xlet: LET spcs { $1 ^ $2 };
85 proof: PROOF spcs { $1 ^ $2 };
86 qed: QED spcs { $1 ^ $2 };
87 gen: GEN spcs { $1 ^ $2 };
88 sec: SEC spcs { $1 ^ $2 };
89 xend: END spcs { $1 ^ $2 };
90 unx: UNX spcs { $1 ^ $2 };
91 def: DEF spcs { $1 ^ $2 };
92 op: OP spcs { $1 ^ $2 };
93 abbr: ABBR spcs { $1 ^ $2 };
94 var: VAR spcs { $1 ^ $2 };
95 ax: AX spcs { $1 ^ $2 };
96 req: REQ spcs { $1 ^ $2 };
97 load: LOAD spcs { $1 ^ $2 };
98 xp: XP spcs { $1 ^ $2 };
99 ind: IND spcs { $1 ^ $2 };
100 set: SET spcs { $1 ^ $2 };
101 notation: NOT spcs { $1 ^ $2 };
102 oc: OC spcs { $1 ^ $2 };
103 coe: COE spcs { $1 ^ $2 };
104 cn: CN spcs { $1 ^ $2 };
105 sc: SC spcs { $1 ^ $2 };
106 str: STR spcs { $1 ^ $2 };
107 id: ID spcs { $1 ^ $2 };
108 coerc: COERC spcs { $1 ^ $2 };
109 cm: CM spcs { $1 ^ $2 } | { "" }
110 wh: WITH spcs { $1 ^ $2 };
112 /* SPACES *******************************************************************/
115 | OQ verbatims CQ { $1 ^ $2 ^ $3 }
123 | spc spcs { $1 ^ $2 }
127 | SPC rspcs { $1 ^ $2 }
130 /* IDENTIFIERS **************************************************************/
155 | outer_keyword { $1 }
160 | qid AC { strip1 $2 :: $1 }
164 | ident cm idents { $1 :: $3 }
167 /* PLAIN SKIP ***************************************************************/
171 | inner_keyword { $1 }
184 | outer_keyword { $1 }
193 /* LEFT SKIP ****************************************************************/
196 | plain_skip { $1, [] }
197 | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
198 | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 }
203 | outer_keyword { $1, [] }
209 | xlskip spcs { fst $1 ^ $2, snd $1 }
210 | xlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
213 | rlskip spcs { fst $1 ^ $2, snd $1 }
214 | rlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
221 /* GENERAL SKIP *************************************************************/
228 | outer_keyword { $1, [] }
234 | xskip spcs { fst $1 ^ $2, snd $1 }
235 | xskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
238 | rskip spcs { fst $1 ^ $2, snd $1 }
239 | rskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
242 /* ABBREVIATION SKIP ********************************************************/
245 | inner_skip { $1, [] }
246 | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
247 | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 }
250 | li_skip spcs { fst $1 ^ $2, snd $1 }
251 | li_skip spcs li_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
254 /* PARENTETIC SKIP **********************************************************/
257 | inner_skip { $1, [] }
258 | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
259 | op ocp_skips CP { $1 ^ fst $2 ^ $3, snd $2 }
263 | ocp_skip spcs { fst $1 ^ $2, snd $1 }
264 | ocp_skip spcs ocp_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
267 /* VERBATIM SKIP ************************************************************/
280 | verbatim verbatims { $1 ^ $2 }
283 /* PROOF STEPS **************************************************************/
287 | skips FS { snd $1 }
291 | step spcs steps { $1 @ $3 }
295 | proof fs steps qed { $3 }
296 | proof skips { snd $2 }
297 | proof wh skips fs steps qed { snd $3 @ $5 }
300 | th ident opt_lskips def xskips FS
302 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
304 | th ident lskips fs just FS
306 $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
308 | gen ident def xskips FS
310 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
312 | mor ident cn ident fs just FS
313 { out "MOR" $4; $6 @ mk_morphism (trim $4) }
314 | xlet ident opt_lskips def xskips FS
316 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
318 | xlet ident lskips fs just FS
320 $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
322 | var idents cn xskips FS
323 { out "VAR" (cat $2); mk_vars true $2 }
324 | ax idents cn xskips FS
325 { out "AX" (cat $2); mk_vars false $2 }
328 T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
331 { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] }
333 { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] }
335 { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
337 { out "REQ" $3; [T.Include (trim $3)] }
339 { out "REQ" $2; [T.Include (trim $2)] }
341 { out "REQ" $2; [T.Include (strip2 (trim $2))] }
342 | coerc qid spcs skips FS
343 { out "COERCE" (hd $2); coercion (hd $2) }
344 | id coerc qid spcs skips FS
345 { out "COERCE" (hd $3); coercion (hd $3) }
347 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
349 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
352 out "ERROR" vs; failwith ("macro_step " ^ vs) }
355 out "ERROR" vs; failwith ("macro_step " ^ vs) }
358 /* VERNACULAR ITEMS *********************************************************/
361 | OQ verbatims CQ { [T.Comment $2] }
363 | set xskips FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
364 | notation xskips FS { notation ($1 ^ fst $2 ^ trim $3) }
365 | error { out "ERROR" "item"; failwith "item" }
369 | rspcs item items { $2 @ $3 }
379 | cnot spcs { $1 ^ $2 }
380 | cnot spcs cnots { $1 ^ $2 ^ $3 }
393 | abbr extends0 IN { $1 ^ $2 ^ $3 }
394 | op extends1 CP { $1 ^ $2 ^ $3 }
413 | restrict spcs { $1 ^ $2 }
414 | restrict spcs restricts { $1 ^ $2 ^ $3 }
417 | xre spcs { $1 ^ $2 }
418 | xre spcs restricts { $1 ^ $2 ^ $3 }
425 | extend0 spcs { $1 ^ $2 }
426 | extend0 spcs extends0 { $1 ^ $2 ^ $3 }
434 | extend1 spcs { $1 ^ $2 }
435 | extend1 spcs extends1 { $1 ^ $2 ^ $3 }
456 | unexport_rr { $1, [] }
457 | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 }
458 | oc unexport_ff CC { $1, [] }
461 | unexport_r spcs { fst $1 ^ $2, snd $1 }
462 | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
465 | ident cn unexports_r
466 { $1 ^ $2 ^ fst $3, snd $3 }
467 | ident def unexports_r
468 { $1 ^ $2 ^ fst $3, snd $3 }
469 | ident coe unexports_r
470 { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
474 | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
476 | error { out "ERROR" "fields"; failwith "fields" }
488 | unexport spcs { fst $1 ^ $2, snd $1 }
489 | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
493 | reserved_ident { $1 }
505 | verbatim verbatims { $1 ^ $2 }
509 | restricts FS { [] }
513 | step spcs steps { $1 @ $3 }
517 | th ident restricts fs proof FS steps qed FS
519 $7 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
521 | th ident restricts fs proof restricts FS
523 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
525 | th ident restricts fs steps qed FS
527 $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
529 | th ident restricts def restricts FS
531 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
533 | th ident def restricts FS
535 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
537 | gen ident def restricts FS
539 [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
541 | xlet ident restricts fs proof FS steps qed FS
543 $7 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
545 | xlet ident restricts fs proof restricts FS
547 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
549 | xlet ident restricts fs steps qed FS
551 $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
553 | xlet ident restricts def restricts FS
555 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
557 | xlet ident def restricts FS
559 [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
562 { out "VAR" (cat $2); mk_vars true $2 }
564 { out "AX" (cat $2); mk_vars false $2 }
565 | ind ident unexports FS
567 T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
570 { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)] }
572 { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)] }
574 { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
576 { out "REQ" $3; [T.Include (trim $3)] }
578 { out "REQ" $3; [T.Include (trim $3)] }
580 { out "REQ" $2; [T.Include (trim $2)] }
582 { out "REQ" $2; [T.Include (strip2 (trim $2))] }
583 | coerc qid spcs cn unexports FS
584 { out "COERCE" (hd $2); coercion (hd $2) }
585 | id coerc qid spcs cn unexports FS
586 { out "COERCE" (hd $3); coercion (hd $3) }
588 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
590 { out "ERROR" $2; failwith ("macro_step " ^ $2) }
593 out "ERROR" vs; failwith ("macro_step " ^ vs) }
596 out "ERROR" vs; failwith ("macro_step " ^ vs) }
599 | OQ verbatims CQ { [T.Comment $2] }
601 | set unexports FS { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
602 | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3) }
603 | error { out "ERROR" "item"; failwith "item" }
607 | rspcs item items { $2 @ $3 }