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