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