helm/software/components/binaries/transcript/grafiteParser.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    module O = Options
  29
  30    let out t s = if !O.verbose_parser then prerr_endline ("-- " ^ t ^ " " ^ s)
  31
  32    let mk_flavour str =
  33       match str with
  34         | "record"      -> T.Ind, None
  35         | "inductive"   -> T.Ind, None
  36         | "coinductive" -> T.Ind, None
  37         | "axiom"       -> T.Con, None
  38         | "definition"  -> T.Con, Some `Definition
  39         | "let rec"     -> T.Con, Some `Definition
  40         | "let corec"   -> T.Con, Some `Definition
  41         | "theorem"     -> T.Con, Some `Theorem
  42         | "lemma"       -> T.Con, Some `Lemma
  43         | "fact"        -> T.Con, Some `Fact
  44         | "remark"      -> T.Con, Some `Remark
  45         | "variant"     -> T.Con, Some `Variant
  46         | _             -> assert false
  47
  48 %}
  49    %token <string> SPC OK CK FS QED TH UNX PS ID RAW
  50    %token EOF
  51
  52    %start items
  53    %type <Types.items> items
  54 %%
  55
  56 /* LINES ITEMS ***************************************************************/
  57
  58    extra:
  59       | ID           { $1           }
  60       | QED          { $1           }
  61       | RAW          { $1           }
  62    ;
  63    text:
  64       | extra   { $1 }
  65       | TH      { $1 }
  66       | UNX     { $1 }
  67       | PS      { $1 }
  68       | comment { $1 }
  69    ;
  70    texts:
  71       |            { ""      }
  72       | text texts { $1 ^ $2 }
  73    ;
  74    line:
  75       | texts FS { $1 ^ $2 }
  76    ;
  77    drop:
  78       | extra line { $1 ^ $2 }
  79    ;
  80    drops:
  81       |            { ""      }
  82       | drop drops { $1 ^ $2 }
  83    ;
  84
  85 /* SPACE ITEMS  *************************************************************/
  86
  87    verbatim:
  88       | text    { $1 }
  89       | FS      { $1 }
  90    ;
  91    verbatims:
  92       |                    { ""      }
  93       | verbatim verbatims { $1 ^ $2 }
  94    ;
  95    comment:
  96       | SPC             { $1 }
  97       | OK verbatims CK { $1 ^ $2 ^ $3 }
  98    ;
  99
 100 /* STEPS ********************************************************************/
 101
 102    step:
 103       | comment { $1 }
 104       | FS      { $1 }
 105       | TH      { $1 }
 106       | UNX     { $1 }
 107       | PS      { $1 }
 108       | ID      { $1 }
 109       | RAW     { $1 }
 110    ;
 111    steps:
 112       | QED FS     { $1 ^ $2 }
 113       | step steps { $1 ^ $2 }
 114    ;
 115
 116 /* ITEMS ********************************************************************/
 117
 118    id:
 119       | ID  { $1 }
 120       | TH  { $1 }
 121       | UNX { $1 }
 122       | PS  { $1 }
 123    ;
 124
 125    item:
 126       | comment
 127          { out "OK" $1; [T.Verbatim $1] }
 128       | TH SPC id line drops
 129          { out "TH" $3;
 130            let a, b = mk_flavour $1 in [T.Inline (false, a, $3, "", b, [])]
 131          }
 132       | UNX line drops { out "UNX" $1; [T.Verbatim ($1 ^ $2 ^ $3)] }
 133       | PS steps       { out "PS" $2; [] }
 134       | QED FS         { [] }
 135    ;
 136    items:
 137       | EOF        { []      }
 138       | item items { $1 @ $2 }
 139 /*      | error      { out "ERROR" ""; failwith ("item id " ^ "") } */
 140   ;