helm/software/components/binaries/transcript/gallina8Lexer.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 = Gallina8Parser
  29
  30    let out t s = if !O.verbose_lexer then prerr_endline (t ^ " " ^ s)
  31
  32    let check s =
  33       let c = Char.code s.[0] in
  34       if c <= 127 then s else
  35       let escaped = Printf.sprintf "\\%3u\\" c in
  36       begin
  37          if !O.verbose_escape then Printf.eprintf "ESCAPED: %s %s\n" s escaped;
  38          escaped
  39       end
  40 }
  41
  42 let QT    = '"'
  43 let SPC   = [' ' '\t' '\n' '\r']+
  44 let ALPHA = ['A'-'Z' 'a'-'z' '_']
  45 let FIG   = ['0'-'9']
  46 let ID    = ALPHA (ALPHA | FIG | "\'")*
  47 let RAWID = QT [^ '"']* QT
  48 let NUM   = "-"? FIG+
  49
  50 rule token = parse
  51    | "Let"         { let s = Lexing.lexeme lexbuf in out "LET" s; P.LET s    }
  52    | "Remark"      { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s      }
  53    | "Lemma"       { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s      }
  54    | "Theorem"     { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s      }
  55    | "Definition"  { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s      }
  56    | "Fixpoint"    { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s      }
  57    | "CoFixpoint"  { let s = Lexing.lexeme lexbuf in out "TH" s; P.TH s      }
  58    | "Qed"         { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s    }
  59    | "Save"        { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s    }
  60    | "Defined"     { let s = Lexing.lexeme lexbuf in out "QED" s; P.QED s    }
  61    | "Proof"       { let s = Lexing.lexeme lexbuf in out "PRF" s; P.PROOF s  }
  62    | "Variable"    { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s    }
  63    | "Variables"   { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s    }
  64    | "Hypothesis"  { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s    }
  65    | "Hypotheses"  { let s = Lexing.lexeme lexbuf in out "VAR" s; P.VAR s    }
  66    | "Axiom"       { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s      }
  67    | "Parameter"   { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s      }
  68    | "Parameters"  { let s = Lexing.lexeme lexbuf in out "AX" s; P.AX s      }
  69    | "Inductive"   { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s    }
  70    | "CoInductive" { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s    }
  71    | "Record"      { let s = Lexing.lexeme lexbuf in out "IND" s; P.IND s    }
  72    | "Scheme"      { let s = Lexing.lexeme lexbuf in out "GEN" s; P.GEN s    }
  73    | "Section"     { let s = Lexing.lexeme lexbuf in out "SEC" s; P.SEC s    }
  74    | "End"         { let s = Lexing.lexeme lexbuf in out "END" s; P.END s    }
  75    | "Hint"        { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s    }
  76    | "Hints"       { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s    }
  77    | "Unset"       { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s    }
  78    | "Print"       { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s    }
  79    | "Opaque"      { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s    }
  80    | "Transparent" { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s    }
  81    | "Ltac"        { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s    }
  82    | "Tactic"      { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s    }
  83    | "Declare"     { let s = Lexing.lexeme lexbuf in out "UNX" s; P.UNX s    }
  84    | "Require"     { let s = Lexing.lexeme lexbuf in out "REQ" s; P.REQ s    }
  85    | "Export"      { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s      }
  86    | "Import"      { let s = Lexing.lexeme lexbuf in out "XP" s; P.XP s      }
  87    | "Load"        { let s = Lexing.lexeme lexbuf in out "LOAD" s; P.LOAD s  }
  88    | "Set"         { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s    }
  89    | "Reset"       { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s    }
  90    | "Implicit"    { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s    }
  91    | "Delimit"     { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s    }
  92    | "Bind"        { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s    }
  93    | "Arguments"   { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s    }
  94    | "Open"        { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s    }
  95    | "V7only"      { let s = Lexing.lexeme lexbuf in out "SET" s; P.SET s    }
  96    | "Notation"    { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s    }
  97    | "Reserved"    { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s    }
  98    | "Infix"       { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s    }
  99    | "Grammar"     { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s    }
 100    | "Syntax"      { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s    }
 101    | "Add" SPC "Morphism"
 102       { let s = Lexing.lexeme lexbuf in out "MOR" s; P.MOR s }
 103    | "Add"         { let s = Lexing.lexeme lexbuf in out "NOT" s; P.NOT s    }
 104    | "Identity"    { let s = Lexing.lexeme lexbuf in out "ID" s; P.ID s      }
 105    | "Coercion"    { let s = Lexing.lexeme lexbuf in out "CO" s; P.COERC s   }
 106    | "let"         { let s = Lexing.lexeme lexbuf in out "ABBR" s; P.ABBR s  }
 107    | "in"          { let s = Lexing.lexeme lexbuf in out "IN" s; P.IN s      }
 108    | "with"        { let s = Lexing.lexeme lexbuf in out "WITH" s; P.WITH s  }
 109    | SPC           { let s = Lexing.lexeme lexbuf in out "SPC" s; P.SPC s    }
 110    | ID            { let s = Lexing.lexeme lexbuf in out "ID" s; P.IDENT s   }
 111    | RAWID         { let s = Lexing.lexeme lexbuf in out "STR" s; P.STR s    }
 112    | NUM           { let s = Lexing.lexeme lexbuf in out "INT" s; P.INT s    }
 113    | ":="          { let s = Lexing.lexeme lexbuf in out "DEF" s; P.DEF s    }
 114    | ":>"          { let s = Lexing.lexeme lexbuf in out "COE" s; P.COE s    }
 115    | "." ID        { let s = Lexing.lexeme lexbuf in out "AC" s; P.AC s      }
 116    | "." SPC       { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s      }
 117    | "." eof       { let s = Lexing.lexeme lexbuf in out "FS" s; P.FS s      }
 118    | "(*"          { let s = Lexing.lexeme lexbuf in out "OQ" s; P.OQ s      }
 119    | "*)"          { let s = Lexing.lexeme lexbuf in out "CQ" s; P.CQ s      }
 120    | "("           { let s = Lexing.lexeme lexbuf in out "OP" s; P.OP s      }
 121    | ")"           { let s = Lexing.lexeme lexbuf in out "CP" s; P.CP s      }
 122    | "{"           { let s = Lexing.lexeme lexbuf in out "OC" s; P.OC s      }
 123    | "}"           { let s = Lexing.lexeme lexbuf in out "CC" s; P.CC s      }
 124    | ";"           { let s = Lexing.lexeme lexbuf in out "SC" s; P.SC s      }
 125    | ":"           { let s = Lexing.lexeme lexbuf in out "CN" s; P.CN s      }
 126    | ","           { let s = Lexing.lexeme lexbuf in out "CM" s; P.CM s      }
 127    | _
 128       { let s = check (Lexing.lexeme lexbuf) in out "SPEC" s; P.EXTRA s }
 129    | eof           { let s = Lexing.lexeme lexbuf in out "EOF" s; P.EOF      }