helm/software/components/binaries/transcript/grafiteLexer.mll

   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 O = Options
  28    module P = GrafiteParser
  29
  30    let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s)
  31 }
  32
  33 let SPC   = [' ' '\t' '\n' '\r']+
  34 let ALPHA = ['A'-'Z' 'a'-'z']
  35 let FIG   = ['0'-'9']
  36 let DECOR = "?" | "'" | "`"
  37 let IDENT = ALPHA (ALPHA | '_' | FIG )* DECOR*
  38
  39 rule token = parse
  40    | "(*"              { let s = Lexing.lexeme lexbuf in out "OK" s; P.OK s   }
  41    | "*)"              { let s = Lexing.lexeme lexbuf in out "CK" s; P.CK s   }
  42    | SPC               { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s }
  43    | "axiom"           { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  44    | "definition"      { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  45    | "theorem"         { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  46    | "lemma"           { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  47 (*
  48    | "fact"            { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  49 *)
  50    | "remark"          { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  51    | "variant"         { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  52    | "inductive"       { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  53    | "coinductive"     { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  54    | "record"          { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  55    | "let rec"         { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  56    | "let corec"       { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s   }
  57    | "notation"        { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
  58    | "interpretation"  { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
  59    | "alias"           { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
  60    | "coercion"        { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
  61    | "prefer coercion" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
  62    | "default"         { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
  63    | "include"         { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
  64    | "inline"          { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
  65    | "pump"            { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s }
  66    | "qed"             { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s }
  67    | "elim"            { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
  68    | "apply"           { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
  69    | "intros"          { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
  70    | "assume"          { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
  71    | "the"             { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
  72    | "rewrite"         { let s = Lexing.lexeme lexbuf in out "PS" s; P.PS s   }
  73    | IDENT             { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s   }
  74    | "." SPC           { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s   }
  75    | "."               { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s   }
  76    | _                 { let s = Lexing.lexeme lexbuf in out "RAW" s; P.RAW s }
  77    | eof               { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF   }