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 map ident = T.Inline (local, T.Var, trim ident, "") in
  39       List.map map idents
  40
  41    let strip2 s =
  42       String.sub s 1 (String.length s - 2)
  43
  44    let strip1 s =
  45       String.sub s 1 (String.length s - 1)
  46
  47    let coercion str =
  48       [T.Coercion (false, str); T.Coercion (true, str)]
  49
  50    let notation str =
  51       [T.Notation (false, str); T.Notation (true, str)]
  52 %}
  53    %token <string> SPC STR IDENT INT EXTRA AC OP CP OC CC OQ CQ DEF FS COE CN SC
  54    %token <string> ABBR IN LET TH PROOF QED VAR AX IND SEC END UNX REQ XP IP SET NOT LOAD ID COERC
  55    %token EOF
  56
  57    %start items
  58    %type <Types.items> items
  59 %%
  60    comment:
  61       | OQ verbatims CQ { $1 ^ $2 ^ $3 }
  62    ;
  63    spc:
  64       | SPC     { $1 }
  65       | comment { $1 }
  66    ;
  67    spcs:
  68      |          { ""      }
  69      | spc spcs { $1 ^ $2 }
  70    ;
  71    rspcs:
  72      |           { ""      }
  73      | SPC rspcs { $1 ^ $2 }
  74    ;
  75    xident:
  76       | IDENT { $1 }
  77       | LET   { $1 }
  78       | TH    { $1 }
  79       | QED   { $1 }
  80       | PROOF { $1 }
  81       | VAR   { $1 }
  82       | AX    { $1 }
  83       | IND   { $1 }
  84       | SEC   { $1 }
  85       | END   { $1 }
  86       | UNX   { $1 }
  87       | REQ   { $1 }
  88       | LOAD  { $1 }
  89       | NOT   { $1 }
  90       | ID    { $1 }
  91       | COERC { $1 }
  92    ;
  93    fs: FS spcs { $1 ^ $2 };
  94    ident: xident spcs { $1 ^ $2 };
  95    th: TH spcs { $1 ^ $2 };
  96    xlet: LET spcs { $1 ^ $2 };
  97    proof: PROOF spcs { $1 ^ $2 };
  98    qed: QED spcs { $1 ^ $2 };
  99    sec: SEC spcs { $1 ^ $2 };
 100    xend: END spcs { $1 ^ $2 };
 101    unx: UNX spcs { $1 ^ $2 };
 102    def: DEF spcs { $1 ^ $2 };
 103    op: OP spcs { $1 ^ $2 };
 104    abbr: ABBR spcs { $1 ^ $2 };
 105    var: VAR spcs { $1 ^ $2 };
 106    ax: AX spcs { $1 ^ $2 };
 107    req: REQ spcs { $1 ^ $2 };
 108    load: LOAD spcs { $1 ^ $2 };
 109    xp: XP spcs { $1 ^ $2 };
 110    ip: IP spcs { $1 ^ $2 };
 111    ind: IND spcs { $1 ^ $2 };
 112    set: SET spcs { $1 ^ $2 };
 113    notation: NOT spcs { $1 ^ $2 };
 114    oc: OC spcs { $1 ^ $2 };
 115    coe: COE spcs { $1 ^ $2 };
 116    cn: CN spcs { $1 ^ $2 };
 117    sc: SC spcs { $1 ^ $2 };
 118    str: STR spcs { $1 ^ $2 };
 119    id: ID spcs { $1 ^ $2 };
 120    coerc: COERC spcs { $1 ^ $2 };
 121
 122    idents:
 123       | ident        { [$1]     }
 124       | ident idents { $1 :: $2 }
 125    ;
 126
 127    cnot:
 128       | EXTRA { $1 }
 129       | INT   { $1 }
 130    ;
 131    cnots:
 132       | cnot spcs       { $1 ^ $2      }
 133       | cnot spcs cnots { $1 ^ $2 ^ $3 }
 134    ;
 135
 136    xstrict:
 137       | AC               { $1           }
 138       | INT              { $1           }
 139       | EXTRA            { $1           }
 140       | CN               { $1           }
 141       | SC               { $1           }
 142       | OC               { $1           }
 143       | CC               { $1           }
 144       | COE              { $1           }
 145       | STR              { $1           }
 146       | abbr extends0 IN { $1 ^ $2 ^ $3 }
 147       | op extends1 CP   { $1 ^ $2 ^ $3 }
 148
 149    ;
 150    strict:
 151       | xstrict { $1 }
 152       | IDENT   { $1 }
 153       | SET     { $1 }
 154       | NOT     { $1 }
 155    ;
 156    restrict:
 157       | strict  { $1 }
 158       | IN      { $1 }
 159       | CP      { $1 }
 160    ;
 161    xre:
 162       | xstrict { $1 }
 163       | IN      { $1 }
 164       | CP      { $1 }
 165    ;
 166    restricts:
 167       | restrict spcs           { $1 ^ $2      }
 168       | restrict spcs restricts { $1 ^ $2 ^ $3 }
 169    ;
 170    xres:
 171       | xre spcs           { $1 ^ $2      }
 172       | xre spcs restricts { $1 ^ $2 ^ $3 }
 173    ;
 174    extend0:
 175       | strict { $1 }
 176       | DEF    { $1 }
 177    ;
 178    extends0:
 179       | extend0 spcs          { $1 ^ $2      }
 180       | extend0 spcs extends0 { $1 ^ $2 ^ $3 }
 181    ;
 182    extend1:
 183       | strict { $1 }
 184       | DEF    { $1 }
 185       | IN     { $1 }
 186    ;
 187    extends1:
 188       | extend1 spcs          { $1 ^ $2      }
 189       | extend1 spcs extends1 { $1 ^ $2 ^ $3 }
 190    ;
 191    unexport_rr:
 192       | AC    { $1 }
 193       | INT   { $1 }
 194       | IDENT { $1 }
 195       | EXTRA { $1 }
 196       | CN    { $1 }
 197       | COE   { $1 }
 198       | STR   { $1 }
 199       | OP    { $1 }
 200       | ABBR  { $1 }
 201       | IN    { $1 }
 202       | CP    { $1 }
 203       | DEF   { $1 }
 204       | SET   { $1 }
 205       | NOT   { $1 }
 206       | LOAD  { $1 }
 207       | ID    { $1 }
 208       | COERC { $1 }
 209    ;
 210    unexport_r:
 211       | unexport_rr  { $1, []                   }
 212       | oc fields CC { $1 ^ fst $2 ^ $3, snd $2 }
 213    ;
 214    unexports_r:
 215       | unexport_r spcs             { fst $1 ^ $2, snd $1                   }
 216       | unexport_r spcs unexports_r { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
 217    ;
 218    field:
 219       | ident cn unexports_r
 220          { $1 ^ $2 ^ fst $3, snd $3                      }
 221       | ident coe unexports_r
 222          { $1 ^ $2 ^ fst $3, snd $3 @ coercion (trim $1) }
 223    ;
 224    fields:
 225       | field           { $1                                      }
 226       | field sc fields { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3   }
 227       | cnots           { $1, []                                  }
 228       | error           { out "ERROR" "fields"; failwith "fields" }
 229    ;
 230    unexport:
 231       | unexport_r { $1     }
 232       | SC         { $1, [] }
 233       | CC         { $1, [] }
 234    ;
 235    unexports:
 236       | unexport spcs           { fst $1 ^ $2, snd $1                   }
 237       | unexport spcs unexports { fst $1 ^ $2 ^ fst $3, snd $1 @ snd $3 }
 238    ;
 239    verbatim:
 240       | unexport_rr { $1 }
 241       | OC          { $1 }
 242       | CC          { $1 }
 243       | SC          { $1 }
 244       | TH          { $1 }
 245       | LET         { $1 }
 246       | VAR         { $1 }
 247       | AX          { $1 }
 248       | IND         { $1 }
 249       | SEC         { $1 }
 250       | END         { $1 }
 251       | UNX         { $1 }
 252       | REQ         { $1 }
 253       | XP          { $1 }
 254       | IP          { $1 }
 255       | QED         { $1 }
 256       | PROOF       { $1 }
 257       | FS          { $1 }
 258       | SPC         { $1 }
 259    ;
 260    verbatims:
 261       |                    { ""      }
 262       | verbatim verbatims { $1 ^ $2 }
 263    ;
 264    step:
 265       | macro_step   { $1 }
 266       | restricts FS { [] }
 267    ;
 268    steps:
 269       | step spcs       { []      }
 270       | step spcs steps { $1 @ $3 }
 271    ;
 272
 273    qid:
 274       | xident { [$1]            }
 275       | qid AC { strip1 $2 :: $1 }
 276    ;
 277
 278    macro_step:
 279       | th ident restricts fs proof FS steps qed FS
 280          { out "TH" $2; $7 @ [T.Inline (false, T.Con, trim $2, "")]     }
 281       | th ident restricts fs proof restricts FS
 282          { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")]          }
 283       | th ident restricts fs steps qed FS
 284          { out "TH" $2; $5 @ [T.Inline (false, T.Con, trim $2, "")]     }
 285       | th ident restricts def restricts FS
 286          { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")]          }
 287       | th ident def restricts FS
 288          { out "TH" $2; [T.Inline (false, T.Con, trim $2, "")]          }
 289       | xlet ident restricts fs proof FS steps qed FS
 290          { out "LET" $2; $7 @ [T.Inline (true, T.Con, trim $2, "")]     }
 291       | xlet ident restricts fs proof restricts FS
 292          { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")]          }
 293       | xlet ident restricts fs steps qed FS
 294          { out "LET" $2; $5 @ [T.Inline (true, T.Con, trim $2, "")]     }
 295       | xlet ident restricts def restricts FS
 296          { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")]          }
 297       | xlet ident def restricts FS
 298          { out "LET" $2; [T.Inline (true, T.Con, trim $2, "")]          }
 299       | var idents xres FS
 300          { out "VAR" (cat $2); mk_vars true $2                          }
 301       | ax idents xres FS
 302          { out "AX" (cat $2); mk_vars false $2                          }
 303       | ind ident unexports FS
 304          { out "IND" $2; T.Inline (false, T.Ind, trim $2, "") :: snd $3 }
 305       | sec ident FS
 306          { out "SEC" $2; [T.Section (true, trim $2, $1 ^ $2)]           }
 307       | xend ident FS
 308          { out "END" $2; [T.Section (false, trim $2, $1 ^ $2)]          }
 309       | unx unexports FS
 310          { out "UNX" (fst $2); [T.Unexport ($1 ^ fst $2 ^ trim $3)]     }
 311       | req xp ident FS
 312          { out "REQ" $3; [T.Include (trim $3)]                          }
 313       | req ip ident FS
 314          { out "REQ" $3; [T.Include (trim $3)]                          }
 315       | req ident FS
 316          { out "REQ" $2; [T.Include (trim $2)]                          }
 317       | load str FS
 318          { out "REQ" $2; [T.Include (strip2 (trim $2))]                 }
 319       | coerc qid spcs cn unexports FS
 320          { out "COERCE" (hd $2); coercion (hd $2)                       }
 321       | id coerc qid spcs cn unexports FS
 322          { out "COERCE" (hd $3); coercion (hd $3)                       }
 323       | th ident error
 324          { out "ERROR" $2; failwith ("macro_step " ^ $2)                }
 325       | ind ident error
 326          { out "ERROR" $2; failwith ("macro_step " ^ $2)                }
 327       | var idents error
 328          { let vs = cat $2 in
 329            out "ERROR" vs; failwith ("macro_step " ^ vs)                }
 330       | ax idents error
 331          { let vs = cat $2 in
 332            out "ERROR" vs; failwith ("macro_step " ^ vs)                }
 333    ;
 334    item:
 335       | OQ verbatims CQ       { [T.Comment $2]                       }
 336       | macro_step            { $1                                   }
 337       | set unexports FS      { [T.Unexport ($1 ^ fst $2 ^ trim $3)] }
 338       | notation unexports FS { notation ($1 ^ fst $2 ^ trim $3)     }
 339       | error                 { out "ERROR" "item"; failwith "item"  }
 340     ;
 341     items:
 342       | rspcs EOF        { []      }
 343       | rspcs item items { $2 @ $3 }
 344     ;