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