helm/software/lambda-delta/automath/autLexer.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 P = AutParser
  28
  29    let debug = false
  30    let out s = if debug then print_endline s else ()
  31 }
  32
  33 let LC  = ['#' '%']
  34 let OC  = "{"
  35 let CC  = "}"
  36 let SPC = [' ' '\t' '\n']+
  37 let NL  = "\n"
  38 let ID  = ['0'-'9' 'A'-'Z' 'a'-'z' '_' '\'' '`']+
  39
  40 rule line_comment = parse
  41    | NL  { () }
  42    | OC  { block_comment lexbuf; line_comment lexbuf }
  43    | _   { line_comment lexbuf }
  44    | eof  { () }
  45 and block_comment = parse
  46    | CC  { () }
  47    | OC  { block_comment lexbuf; block_comment lexbuf }
  48    | LC  { line_comment lexbuf; block_comment lexbuf  }
  49    | _   { block_comment lexbuf }
  50    | eof { () }
  51 and token = parse
  52    | SPC      { token lexbuf }
  53    | LC       { line_comment lexbuf; token lexbuf  }
  54    | OC       { block_comment lexbuf; token lexbuf }
  55    | "_E"     { out "E"; P.E         }
  56    | "'_E'"   { out "E"; P.E         }
  57    | "---"    { out "EB"; P.EB       }
  58    | "'eb'"   { out "EB"; P.EB       }
  59    | "EB"     { out "EB"; P.EB       }
  60    | "--"     { out "EXIT"; P.EXIT   }
  61    | "PN"     { out "PN"; P.PN       }
  62    | "'pn'"   { out "PN"; P.PN       }
  63    | "PRIM"   { out "PN"; P.PN       }
  64    | "'prim'" { out "PN"; P.PN       }
  65    | "???"    { out "PN"; P.PN       }
  66    | "PROP"   { out "PROP"; P.PROP   }
  67    | "'prop'" { out "PROP"; P.PROP   }
  68    | "TYPE"   { out "TYPE"; P.TYPE   }
  69    | "'type'" { out "TYPE"; P.TYPE   }
  70    | ID       { out "ID"; P.IDENT (Lexing.lexeme lexbuf) }
  71    | ":="     { out "DEF"; P.DEF     }
  72    | "("      { out "OP"; P.OP       }
  73    | ")"      { out "CP"; P.CP       }
  74    | "["      { out "OB"; P.OB       }
  75    | "]"      { out "CB"; P.CB       }
  76    | "<"      { out "OA"; P.OA       }
  77    | ">"      { out "CA"; P.CA       }
  78    | "@"      { out "AT"; P.AT       }
  79    | "~"      { out "TD"; P.TD       }
  80    | "\""     { out "QT"; P.QT       }
  81    | ":"      { out "CN"; P.CN       }
  82    | ","      { out "CM"; P.CM       }
  83    | ";"      { out "SC"; P.SC       }
  84    | "."      { out "FS"; P.FS       }
  85    | "+"      { out "PLUS"; P.PLUS   }
  86    | "-"      { out "MINUS"; P.MINUS }
  87    | "*"      { out "TIMES"; P.TIMES }
  88    | "="      { out "DEF"; P.DEF     }
  89    | eof      { out "EOF"; P.EOF     }