helm/software/components/binaries/transcript/v8Parser.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    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 };
 112
 113 /* SPACES *******************************************************************/
 114
 115    comment:
 116       | OQ verbatims CQ { $1 ^ $2 ^ $3 }
 117    ;
 118    spc:
 119       | SPC     { $1 }
 120       | comment { $1 }
 121    ;
 122    spcs:
 123      |          { ""      }
 124      | spc spcs { $1 ^ $2 }
 125    ;
 126    rspcs:
 127      |           { ""      }
 128      | SPC rspcs { $1 ^ $2 }
 129    ;
 130
 131 /* IDENTIFIERS **************************************************************/
 132
 133    outer_keyword:
 134       | LET   { $1 }
 135       | TH    { $1 }
 136       | VAR   { $1 }
 137       | AX    { $1 }
 138       | IND   { $1 }
 139       | GEN   { $1 }
 140       | SEC   { $1 }
 141       | END   { $1 }
 142       | UNX   { $1 }
 143       | REQ   { $1 }
 144       | LOAD  { $1 }
 145       | SET   { $1 }
 146       | NOT   { $1 }
 147       | ID    { $1 }
 148       | COERC { $1 }
 149       | MOR   { $1 }
 150    ;
 151    inner_keyword:
 152       | XP    { $1 }
 153    ;
 154    xident:
 155       | IDENT         { $1 }
 156       | outer_keyword { $1 }
 157       | WITH          { $1 }
 158    ;
 159    qid:
 160       | xident { [$1]            }
 161       | qid AC { strip1 $2 :: $1 }
 162    ;
 163    idents:
 164       | ident           { [$1]     }
 165       | ident cm idents { $1 :: $3 }
 166    ;
 167
 168 /* PLAIN SKIP ***************************************************************/
 169
 170    plain_skip:
 171       | IDENT           { $1 }
 172       | inner_keyword   { $1 }
 173       | STR             { $1 }
 174       | INT             { $1 }
 175       | COE             { $1 }
 176       | OC              { $1 }
 177       | CC              { $1 }
 178       | SC              { $1 }
 179       | CN              { $1 }
 180       | CM              { $1 }
 181       | EXTRA           { $1 }
 182    ;
 183    inner_skip:
 184       | plain_skip     { $1 }
 185       | outer_keyword  { $1 }
 186       | AC             { $1 }
 187       | DEF            { $1 }
 188       | PROOF          { $1 }
 189       | QED            { $1 }
 190       | FS             { $1 }
 191       | WITH           { $1 }
 192    ;
 193
 194 /* LEFT SKIP ****************************************************************/
 195
 196    rlskip:
 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 }
 200       | IN               { $1, []                   }
 201       | CP               { $1, []                   }
 202    ;
 203    xlskip:
 204       | outer_keyword { $1, [] }
 205       | AC            { $1, [] }
 206       | WITH          { $1, [] }
 207       | rlskip        { $1     }
 208    ;
 209    xlskips:
 210       | xlskip spcs         { fst $1 ^ $2, snd $1                   }
 211       | xlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
 212    ;
 213    lskips:
 214       | rlskip spcs         { fst $1 ^ $2, snd $1                   }
 215       | rlskip spcs xlskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
 216    ;
 217    opt_lskips:
 218       | lskips { $1     }
 219       |        { "", [] }
 220    ;
 221
 222 /* GENERAL SKIP *************************************************************/
 223
 224    rskip:
 225       | rlskip { $1     }
 226       | DEF    { $1, [] }
 227    ;
 228    xskip:
 229       | outer_keyword { $1, [] }
 230       | AC            { $1, [] }
 231       | WITH          { $1, [] }
 232       | rskip         { $1     }
 233    ;
 234    xskips:
 235       | xskip spcs        { fst $1 ^ $2, snd $1                   }
 236       | xskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
 237    ;
 238    skips:
 239       | rskip spcs        { fst $1 ^ $2, snd $1                   }
 240       | rskip spcs xskips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
 241    ;
 242
 243 /* ABBREVIATION SKIP ********************************************************/
 244
 245    li_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 }
 249    ;
 250    li_skips:
 251       | li_skip spcs          { fst $1 ^ $2, snd $1                   }
 252       | li_skip spcs li_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
 253    ;
 254
 255 /* PARENTETIC SKIP **********************************************************/
 256
 257    ocp_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 }
 261       | IN               { $1, []                   }
 262    ;
 263    ocp_skips:
 264       | ocp_skip spcs           { fst $1 ^ $2, snd $1                   }
 265       | ocp_skip spcs ocp_skips { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
 266    ;
 267
 268 /* VERBATIM SKIP ************************************************************/
 269
 270    verbatim:
 271       | comment        { $1 }
 272       | inner_skip     { $1 }
 273       | ABBR           { $1 }
 274       | IN             { $1 }
 275       | OP             { $1 }
 276       | CP             { $1 }
 277       | SPC            { $1 }
 278    ;
 279    verbatims:
 280       |                    { ""      }
 281       | verbatim verbatims { $1 ^ $2 }
 282    ;
 283
 284 /* PROOF STEPS **************************************************************/
 285
 286    step:
 287       | macro_step   { $1     }
 288       | skips FS     { snd $1 }
 289    ;
 290    steps:
 291       | step spcs       { $1      }
 292       | step spcs steps { $1 @ $3 }
 293    ;
 294    just:
 295       | steps qed                   { $1          }
 296       | proof fs steps qed          { $3          }
 297       | proof skips                 { snd $2      }
 298       | proof wh skips fs steps qed { snd $3 @ $5 }
 299    ;
 300    macro_step:
 301       | th ident opt_lskips def xskips FS
 302          { out "TH" $2;
 303            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
 304          }
 305       | th ident lskips fs just FS
 306          { out "TH" $2;
 307            $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
 308          }
 309       | gen ident def xskips FS
 310          { out "TH" $2;
 311            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
 312          }
 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
 316          { out "TH" $2;
 317            [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
 318          }
 319       | xlet ident lskips fs just FS
 320          { out "TH" $2;
 321            $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
 322          }
 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                      }
 327       | ind ident skips FS
 328          { out "IND" $2;
 329            T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
 330          }
 331       | sec ident FS
 332          { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)]       }
 333       | xend ident FS
 334          { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)]      }
 335       | unx xskips FS
 336          { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
 337       | req xp ident FS
 338          { out "REQ" $3; [T.Include (trim $3)]                      }
 339       | req ident FS
 340          { out "REQ" $2; [T.Include (trim $2)]                      }
 341       | load str FS
 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)                   }
 347       | th ident error
 348          { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
 349       | ind ident error
 350          { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
 351       | var idents error
 352          { let vs = cat $2 in
 353            out "ERROR" vs; failwith ("macro_step " ^ vs)            }
 354       | ax idents error
 355          { let vs = cat $2 in
 356            out "ERROR" vs; failwith ("macro_step " ^ vs)            }
 357    ;
 358
 359 /* VERNACULAR ITEMS *********************************************************/
 360
 361    item:
 362       | OQ verbatims CQ       { [T.Comment $2]                       }
 363       | macro_step            { $1                                   }
 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"  }
 367     ;
 368     items:
 369       | rspcs EOF        { []      }
 370       | rspcs item items { $2 @ $3 }
 371     ;
 372
 373
 374 /*
 375    cnot:
 376       | EXTRA { $1 }
 377       | INT   { $1 }
 378    ;
 379    cnots:
 380       | cnot spcs       { $1 ^ $2      }
 381       | cnot spcs cnots { $1 ^ $2 ^ $3 }
 382    ;
 383
 384    xstrict:
 385       | AC               { $1           }
 386       | INT              { $1           }
 387       | EXTRA            { $1           }
 388       | CN               { $1           }
 389       | SC               { $1           }
 390       | OC               { $1           }
 391       | CC               { $1           }
 392       | COE              { $1           }
 393       | STR              { $1           }
 394       | abbr extends0 IN { $1 ^ $2 ^ $3 }
 395       | op extends1 CP   { $1 ^ $2 ^ $3 }
 396    ;
 397    strict:
 398       | xstrict { $1 }
 399       | IDENT   { $1 }
 400       | SET     { $1 }
 401       | NOT     { $1 }
 402    ;
 403    restrict:
 404       | strict  { $1 }
 405       | IN      { $1 }
 406       | CP      { $1 }
 407    ;
 408    xre:
 409       | xstrict { $1 }
 410       | IN      { $1 }
 411       | CP      { $1 }
 412    ;
 413    restricts:
 414       | restrict spcs           { $1 ^ $2      }
 415       | restrict spcs restricts { $1 ^ $2 ^ $3 }
 416    ;
 417    xres:
 418       | xre spcs           { $1 ^ $2      }
 419       | xre spcs restricts { $1 ^ $2 ^ $3 }
 420    ;
 421    extend0:
 422       | strict { $1 }
 423       | DEF    { $1 }
 424    ;
 425    extends0:
 426       | extend0 spcs          { $1 ^ $2      }
 427       | extend0 spcs extends0 { $1 ^ $2 ^ $3 }
 428    ;
 429    extend1:
 430       | strict { $1 }
 431       | DEF    { $1 }
 432       | IN     { $1 }
 433    ;
 434    extends1:
 435       | extend1 spcs          { $1 ^ $2      }
 436       | extend1 spcs extends1 { $1 ^ $2 ^ $3 }
 437    ;
 438    unexport_ff:
 439       | IDENT          { $1 }
 440       | AC             { $1 }
 441       | STR            { $1 }
 442       | OP             { $1 }
 443       | ABBR           { $1 }
 444       | IN             { $1 }
 445       | CP             { $1 }
 446       | SET            { $1 }
 447    ;
 448    unexport_rr:
 449       | unexport_ff { $1 }
 450       | INT         { $1 }
 451       | EXTRA       { $1 }
 452       | CN          { $1 }
 453       | COE         { $1 }
 454       | DEF         { $1 }
 455    ;
 456    unexport_r:
 457       | unexport_rr       { $1, []                   }
 458       | oc fields CC      { $1 ^ fst $2 ^ $3, snd $2 }
 459       | oc unexport_ff CC { $1, []                   }
 460    ;
 461    unexports_r:
 462       | unexport_r spcs             { fst $1 ^ $2, snd $1                   }
 463       | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
 464    ;
 465    field:
 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) }
 472    ;
 473    fields:
 474       | field           { $1                                      }
 475       | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3   }
 476       | cnots           { $1, []                                  }
 477       | error           { out "ERROR" "fields"; failwith "fields" }
 478    ;
 479    unexport:
 480       | unexport_r { $1     }
 481       | SC         { $1, [] }
 482       | CC         { $1, [] }
 483       | IP         { $1, [] }
 484       | LET        { $1, [] }
 485       | VAR        { $1, [] }
 486
 487    ;
 488    unexports:
 489       | unexport spcs           { fst $1 ^ $2, snd $1                   }
 490       | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
 491    ;
 492    verbatim:
 493       | unexport_rr    { $1 }
 494       | reserved_ident { $1 }
 495       | comment        { $1 }
 496       | OC             { $1 }
 497       | CC             { $1 }
 498       | SC             { $1 }
 499       | XP             { $1 }
 500       | IP             { $1 }
 501       | FS             { $1 }
 502       | SPC            { $1 }
 503    ;
 504    verbatims:
 505       |                    { ""      }
 506       | verbatim verbatims { $1 ^ $2 }
 507    ;
 508    step:
 509       | macro_step   { $1 }
 510       | restricts FS { [] }
 511    ;
 512    steps:
 513       | step spcs       { []      }
 514       | step spcs steps { $1 @ $3 }
 515    ;
 516
 517    macro_step:
 518       | th ident restricts fs proof FS steps qed FS
 519          { out "TH" $2;
 520            $7 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
 521          }
 522       | th ident restricts fs proof restricts FS
 523          { out "TH" $2;
 524            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
 525          }
 526       | th ident restricts fs steps qed FS
 527          { out "TH" $2;
 528            $5 @ [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
 529          }
 530       | th ident restricts def restricts FS
 531          { out "TH" $2;
 532            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
 533          }
 534       | th ident def restricts FS
 535          { out "TH" $2;
 536            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
 537          }
 538       | gen ident def restricts FS
 539          { out "TH" $2;
 540            [T.Inline (false, T.Con, trim $2, "", mk_flavour $1)]
 541          }
 542       | xlet ident restricts fs proof FS steps qed FS
 543          { out "LET" $2;
 544            $7 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
 545          }
 546       | xlet ident restricts fs proof restricts FS
 547          { out "LET" $2;
 548            [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
 549          }
 550       | xlet ident restricts fs steps qed FS
 551          { out "LET" $2;
 552            $5 @ [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
 553          }
 554       | xlet ident restricts def restricts FS
 555          { out "LET" $2;
 556            [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
 557          }
 558       | xlet ident def restricts FS
 559          { out "LET" $2;
 560            [T.Inline (true, T.Con, trim $2, "", mk_flavour $1)]
 561          }
 562       | var idents xres FS
 563          { out "VAR" (cat $2); mk_vars true $2                      }
 564       | ax idents xres FS
 565          { out "AX" (cat $2); mk_vars false $2                      }
 566       | ind ident unexports FS
 567          { out "IND" $2;
 568            T.Inline (false, T.Ind, trim $2, "", None) :: snd $3
 569          }
 570       | sec ident FS
 571          { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)]       }
 572       | xend ident FS
 573          { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)]      }
 574       | unx unexports FS
 575          { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
 576       | req xp ident FS
 577          { out "REQ" $3; [T.Include (trim $3)]                      }
 578       | req ip ident FS
 579          { out "REQ" $3; [T.Include (trim $3)]                      }
 580       | req ident FS
 581          { out "REQ" $2; [T.Include (trim $2)]                      }
 582       | load str FS
 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)                   }
 588       | th ident error
 589          { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
 590       | ind ident error
 591          { out "ERROR" $2; failwith ("macro_step " ^ $2)            }
 592       | var idents error
 593          { let vs = cat $2 in
 594            out "ERROR" vs; failwith ("macro_step " ^ vs)            }
 595       | ax idents error
 596          { let vs = cat $2 in
 597            out "ERROR" vs; failwith ("macro_step " ^ vs)            }
 598    ;
 599    item:
 600       | OQ verbatims CQ       { [T.Comment $2]                       }
 601       | macro_step            { $1                                   }
 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"  }
 605     ;
 606     items:
 607       | rspcs EOF        { []      }
 608       | rspcs item items { $2 @ $3 }
 609     ;
 610 */