]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/binaries/transcript/gallina8Parser.mly
Initial implementation of statuses using objects in place of nested records.
[helm.git] / helm / software / components / binaries / transcript / gallina8Parser.mly
1 /* Copyright (C) 2000, HELM Team.
2  * 
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.
6  * 
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.
11  * 
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.
16  *
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,
20  * MA  02111-1307, USA.
21  * 
22  * For details, see the HELM World-Wide-Web page,
23  * http://cs.unibo.it/helm/.
24  */
25
26 %{
27    module T = Types
28    module O = Options
29
30    let out t s = if !O.verbose_parser then prerr_endline ("-- " ^ t ^ " " ^ s)
31
32    let trim = HExtlib.trim_blanks
33
34    let hd = List.hd
35
36    let cat x = String.concat " " x
37
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
41       List.map map idents
42
43    let strip2 s =
44       String.sub s 1 (String.length s - 2)
45
46    let strip1 s = 
47       String.sub s 1 (String.length s - 1)
48
49    let coercion str = 
50       [T.Coercion (false, str); T.Coercion (true, str)]
51
52    let notation str =
53       [T.Notation (false, str); T.Notation (true, str)]
54
55    let mk_flavour str =
56       match trim str with
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
65         | _            -> assert false
66
67    let mk_morphism ext =
68       let generate s = T.Inline (false, T.Con, ext ^ s, "", Some `Theorem, []) in
69       List.rev_map generate ["2"; "1"]
70
71 %}
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
74    %token EOF
75
76    %start items
77    %type <Types.items> items
78 %%
79 /* SPACED TOKENS ************************************************************/
80    
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    cn: CN spcs { $1 ^ $2 };
104    str: STR spcs { $1 ^ $2 };
105    id: ID spcs { $1 ^ $2 };
106    coerc: COERC spcs { $1 ^ $2 };
107    cm: CM spcs { $1 ^ $2 } | { "" }
108    wh: WITH spcs { $1 ^ $2 };
109
110 /* SPACES *******************************************************************/
111
112    comment:
113       | OQ verbatims CQ { $1 ^ $2 ^ $3 }
114    ;
115    spc:
116       | SPC     { $1 }
117       | comment { $1 }
118    ;
119    spcs:
120      |          { ""      }
121      | spc spcs { $1 ^ $2 }
122    ;
123    rspcs:
124      |           { ""      }
125      | SPC rspcs { $1 ^ $2 }
126    ;
127
128 /* IDENTIFIERS **************************************************************/
129
130    outer_keyword:
131       | LET   { $1 }
132       | TH    { $1 }
133       | VAR   { $1 }
134       | AX    { $1 }
135       | IND   { $1 }
136       | GEN   { $1 }
137       | SEC   { $1 }
138       | END   { $1 }
139       | UNX   { $1 }
140       | REQ   { $1 }
141       | LOAD  { $1 }
142       | SET   { $1 }
143       | NOT   { $1 }
144       | ID    { $1 }
145       | COERC { $1 }
146       | MOR   { $1 }
147    ;
148    inner_keyword:
149       | XP    { $1 }
150    ;
151    xident:
152       | IDENT         { $1 }
153       | outer_keyword { $1 }
154       | WITH          { $1 }
155    ;
156    qid:
157       | xident { [$1]            }
158       | qid AC { strip1 $2 :: $1 }
159    ;
160    idents:
161       | ident           { [$1]     }
162       | ident cm idents { $1 :: $3 }
163    ;
164
165 /* PLAIN SKIP ***************************************************************/
166
167    plain_skip:
168       | IDENT           { $1 }
169       | inner_keyword   { $1 }
170       | STR             { $1 }
171       | INT             { $1 }
172       | COE             { $1 }
173       | OC              { $1 }
174       | CC              { $1 }
175       | SC              { $1 }
176       | CN              { $1 }
177       | CM              { $1 }
178       | EXTRA           { $1 }
179    ;
180    inner_skip:
181       | plain_skip     { $1 }
182       | outer_keyword  { $1 }
183       | AC             { $1 }
184       | DEF            { $1 }
185       | PROOF          { $1 }
186       | QED            { $1 }
187       | FS             { $1 }
188       | WITH           { $1 }
189    ;
190
191 /* LEFT SKIP ****************************************************************/
192
193    rlskip:
194       | plain_skip       { $1, []                   }
195       | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
196       | op ocp_skips CP  { $1 ^ fst $2 ^ $3, snd $2 }
197       | IN               { $1, []                   }
198       | CP               { $1, []                   }
199    ;
200    xlskip:
201       | outer_keyword { $1, [] }
202       | AC            { $1, [] }
203       | WITH          { $1, [] }
204       | rlskip        { $1     }
205    ;
206    xlskips:
207       | xlskip spcs         { fst $1 ^ $2, snd $1                   }
208       | xlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
209    ;
210    lskips:
211       | rlskip spcs         { fst $1 ^ $2, snd $1                   }
212       | rlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
213    ;
214    opt_lskips:
215       | lskips { $1     }
216       |        { "", [] }
217    ;
218
219 /* GENERAL SKIP *************************************************************/ 
220
221    rskip:
222       | rlskip { $1     }
223       | DEF    { $1, [] }
224    ;
225    xskip:
226       | outer_keyword { $1, [] }
227       | AC            { $1, [] }
228       | WITH          { $1, [] }
229       | rskip         { $1     }
230    ;
231    xskips:
232       | xskip spcs        { fst $1 ^ $2, snd $1                   }
233       | xskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
234    ;
235    skips:
236       | rskip spcs        { fst $1 ^ $2, snd $1                   }
237       | rskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
238    ;
239
240 /* ABBREVIATION SKIP ********************************************************/
241
242    li_skip:
243       | inner_skip       { $1, []                   }
244       | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
245       | op ocp_skips CP  { $1 ^ fst $2 ^ $3, snd $2 }
246    ;
247    li_skips:
248       | li_skip spcs          { fst $1 ^ $2, snd $1                   }
249       | li_skip spcs li_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
250    ;
251
252 /* PARENTETIC SKIP **********************************************************/
253
254    ocp_skip:
255       | inner_skip       { $1, []                   }
256       | abbr li_skips IN { $1 ^ fst $2 ^ $3, snd $2 }
257       | op ocp_skips CP  { $1 ^ fst $2 ^ $3, snd $2 }
258       | IN               { $1, []                   }
259    ;
260    ocp_skips:
261       | ocp_skip spcs           { fst $1 ^ $2, snd $1                   }
262       | ocp_skip spcs ocp_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
263    ;
264
265 /* VERBATIM SKIP ************************************************************/
266    
267    verbatim:
268       | comment        { $1 }
269       | inner_skip     { $1 }
270       | ABBR           { $1 }
271       | IN             { $1 }
272       | OP             { $1 }
273       | CP             { $1 }
274       | SPC            { $1 }
275    ;
276    verbatims:
277       |                    { ""      }
278       | verbatim verbatims { $1 ^ $2 }
279    ;   
280
281 /* PROOF STEPS **************************************************************/
282
283    step:
284       | macro_step   { $1     }
285       | skips FS     { snd $1 }
286    ;
287    steps:
288       | step spcs       { $1      }
289       | step spcs steps { $1 @ $3 }
290    ;
291    just:
292       | steps qed                   { $1          }
293       | proof fs steps qed          { $3          }
294       | proof skips                 { snd $2      }
295       | proof wh skips fs steps qed { snd $3 @ $5 }
296    ;
297    macro_step:
298       | th ident opt_lskips def xskips FS
299          { out "TH" $2;
300            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1, [])]
301          }
302       | th ident lskips fs just FS 
303          { out "TH" $2;
304            $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1, [])]
305          }
306       | gen ident def xskips FS
307          { out "TH" $2;
308            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1, [])]
309          }      
310       | mor ident cn ident fs just FS
311          { out "MOR" $4; $6 @ mk_morphism (trim $4)                 }
312       | xlet ident opt_lskips def xskips FS
313          { out "TH" $2;
314            [T.Inline (true, T.Con, trim $2, "", mk_flavour $1, [])]
315          }
316       | xlet ident lskips fs just FS 
317          { out "TH" $2;
318            $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1, [])]
319          }
320       | var idents cn xskips FS
321          { out "VAR" (cat $2); mk_vars true $2                      }
322       | ax idents cn xskips FS
323          { out "AX" (cat $2); mk_vars false $2                      }
324       | ind ident skips FS
325          { out "IND" $2;
326            T.Inline (false, T.Ind, trim $2, "", None, []) :: snd $3
327          }
328       | sec ident FS
329          { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)]       }
330       | xend ident FS
331          { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)]      }
332       | unx xskips FS
333          { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
334       | req xp ident FS
335          { out "REQ" $3; [T.Include (true, trim $3)]               }
336       | req ident FS
337          { out "REQ" $2; [T.Include (true, trim $2)]               } 
338       | load str FS
339          { out "REQ" $2; [T.Include (true, strip2 (trim $2))]      }
340       | coerc qid spcs skips FS
341          { out "COERCE" (hd $2); coercion (hd $2)                   }
342       | id coerc qid spcs skips FS
343          { out "COERCE" (hd $3); coercion (hd $3)                   }
344       | th ident error 
345          { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
346       | ind ident error 
347          { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
348       | var idents error 
349          { let vs = cat $2 in
350            out "ERROR" vs; failwith ("macro_step " ^ vs)            }
351       | ax idents error 
352          { let vs = cat $2 in
353            out "ERROR" vs; failwith ("macro_step " ^ vs)            }
354    ;
355
356 /* VERNACULAR ITEMS *********************************************************/
357
358    item:
359       | OQ verbatims CQ       { [T.Comment $2]                       }
360       | macro_step            { $1                                   }
361       | set xskips FS         { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
362       | notation xskips FS    { notation ($1 ^ fst $2 ^ trim $3)     }
363       | error                 { out "ERROR" "item"; failwith "item"  }
364     ;
365     items:
366       | rspcs EOF        { []      }
367       | rspcs item items { $2 @ $3 }
368     ;
369
370
371 /*
372    oc: OC spcs { $1 ^ $2 };
373    coe: COE spcs { $1 ^ $2 };
374    sc: SC spcs { $1 ^ $2 };
375
376    cnot:
377       | EXTRA { $1 }
378       | INT   { $1 }
379    ;
380    cnots:
381       | cnot spcs       { $1 ^ $2      }
382       | cnot spcs cnots { $1 ^ $2 ^ $3 }
383    ;
384    
385    xstrict:
386       | AC               { $1           }
387       | INT              { $1           }
388       | EXTRA            { $1           }
389       | CN               { $1           }
390       | SC               { $1           }
391       | OC               { $1           }
392       | CC               { $1           }
393       | COE              { $1           }
394       | STR              { $1           }   
395       | abbr extends0 IN { $1 ^ $2 ^ $3 }
396       | op extends1 CP   { $1 ^ $2 ^ $3 }      
397    ;
398    strict:
399       | xstrict { $1 }
400       | IDENT   { $1 } 
401       | SET     { $1 }
402       | NOT     { $1 }
403    ;
404    restrict: 
405       | strict  { $1 }
406       | IN      { $1 }
407       | CP      { $1 }
408    ;
409    xre:
410       | xstrict { $1 }
411       | IN      { $1 }
412       | CP      { $1 }   
413    ;
414    restricts:
415       | restrict spcs           { $1 ^ $2      }
416       | restrict spcs restricts { $1 ^ $2 ^ $3 }
417    ;
418    xres:
419       | xre spcs           { $1 ^ $2      }
420       | xre spcs restricts { $1 ^ $2 ^ $3 }   
421    ;
422    extend0:
423       | strict { $1 }
424       | DEF    { $1 }
425    ;
426    extends0:
427       | extend0 spcs          { $1 ^ $2      }
428       | extend0 spcs extends0 { $1 ^ $2 ^ $3 }
429    ;
430    extend1:
431       | strict { $1 }
432       | DEF    { $1 }
433       | IN     { $1 }
434    ;
435    extends1:
436       | extend1 spcs          { $1 ^ $2      }
437       | extend1 spcs extends1 { $1 ^ $2 ^ $3 }
438    ;
439    unexport_ff:
440       | IDENT          { $1 }
441       | AC             { $1 }
442       | STR            { $1 }
443       | OP             { $1 }
444       | ABBR           { $1 }
445       | IN             { $1 }
446       | CP             { $1 }
447       | SET            { $1 }
448    ;   
449    unexport_rr:
450       | unexport_ff { $1 }
451       | INT         { $1 }
452       | EXTRA       { $1 }
453       | CN          { $1 }
454       | COE         { $1 }
455       | DEF         { $1 }
456    ;
457    unexport_r:
458       | unexport_rr       { $1, []                   }
459       | oc fields CC      { $1 ^ fst $2 ^ $3, snd $2 }
460       | oc unexport_ff CC { $1, []                   }
461    ;
462    unexports_r:
463       | unexport_r spcs             { fst $1 ^ $2, snd $1                   }
464       | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
465    ;
466    field: 
467       | ident cn unexports_r
468          { $1 ^ $2 ^ fst $3, snd $3                      }
469       | ident def unexports_r
470          { $1 ^ $2 ^ fst $3, snd $3                      }
471       | ident coe unexports_r 
472          { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
473    ;  
474    fields:
475       | field           { $1                                      }
476       | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3   } 
477       | cnots           { $1, []                                  }
478       | error           { out "ERROR" "fields"; failwith "fields" }
479    ;
480    unexport:
481       | unexport_r { $1     }
482       | SC         { $1, [] }
483       | CC         { $1, [] }
484       | IP         { $1, [] }
485       | LET        { $1, [] }       
486       | VAR        { $1, [] }
487       
488    ;   
489    unexports:
490       | unexport spcs           { fst $1 ^ $2, snd $1                   }
491       | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
492    ;
493    verbatim:
494       | unexport_rr    { $1 }
495       | reserved_ident { $1 }
496       | comment        { $1 }
497       | OC             { $1 }
498       | CC             { $1 }
499       | SC             { $1 }
500       | XP             { $1 } 
501       | IP             { $1 } 
502       | FS             { $1 }
503       | SPC            { $1 }
504    ;
505    verbatims:
506       |                    { ""      }
507       | verbatim verbatims { $1 ^ $2 }
508    ;   
509    step:
510       | macro_step   { $1 }
511       | restricts FS { [] }
512    ;
513    steps:
514       | step spcs       { []      }
515       | step spcs steps { $1 @ $3 }
516    ;
517       
518    macro_step:
519       | th ident restricts fs proof FS steps qed FS 
520          { out "TH" $2;
521            $7 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
522          }
523       | th ident restricts fs proof restricts FS
524          { out "TH" $2; 
525            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
526          }
527       | th ident restricts fs steps qed FS 
528          { out "TH" $2;
529            $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
530          }
531       | th ident restricts def restricts FS
532          { out "TH" $2;
533            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
534          }
535       | th ident def restricts FS
536          { out "TH" $2;
537            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
538          }
539       | gen ident def restricts FS
540          { out "TH" $2;
541            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
542          }      
543       | xlet ident restricts fs proof FS steps qed FS 
544          { out "LET" $2;
545            $7 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
546          }
547       | xlet ident restricts fs proof restricts FS
548          { out "LET" $2;
549            [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
550          }
551       | xlet ident restricts fs steps qed FS 
552          { out "LET" $2;
553            $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
554          }
555       | xlet ident restricts def restricts FS
556          { out "LET" $2;
557            [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
558          }
559       | xlet ident def restricts FS
560          { out "LET" $2;
561            [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
562          }
563       | var idents xres FS
564          { out "VAR" (cat $2); mk_vars true $2                      }
565       | ax idents xres FS
566          { out "AX" (cat $2); mk_vars false $2                      }
567       | ind ident unexports FS
568          { out "IND" $2;
569            T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
570          }
571       | sec ident FS
572          { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)]       }
573       | xend ident FS
574          { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)]      }
575       | unx unexports FS
576          { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
577       | req xp ident FS
578          { out "REQ" $3; [T.Include (trim $3)]                      }
579       | req ip ident FS
580          { out "REQ" $3; [T.Include (trim $3)]                      }
581       | req ident FS
582          { out "REQ" $2; [T.Include (trim $2)]                      } 
583       | load str FS
584          { out "REQ" $2; [T.Include (strip2 (trim $2))]             }
585       | coerc qid spcs cn unexports FS
586          { out "COERCE" (hd $2); coercion (hd $2)                   }
587       | id coerc qid spcs cn unexports FS
588          { out "COERCE" (hd $3); coercion (hd $3)                   }
589       | th ident error 
590          { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
591       | ind ident error 
592          { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
593       | var idents error 
594          { let vs = cat $2 in
595            out "ERROR" vs; failwith ("macro_step " ^ vs)            }
596       | ax idents error 
597          { let vs = cat $2 in
598            out "ERROR" vs; failwith ("macro_step " ^ vs)            }
599    ;
600    item:
601       | OQ verbatims CQ       { [T.Comment $2]                       }
602       | macro_step            { $1                                   }
603       | set unexports FS      { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
604       | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3)     }
605       | error                 { out "ERROR" "item"; failwith "item"  }
606     ;
607     items:
608       | rspcs EOF        { []      }
609       | rspcs item items { $2 @ $3 }
610     ;
611 */