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