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