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 */