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