helm/software/helena/src/automath/autLexer.mll

   1 (*
   2     ||M||  This file is part of HELM, an Hypertextual, Electronic
   3     ||A||  Library of Mathematics, developed at the Computer Science
   4     ||T||  Department, University of Bologna, Italy.
   5     ||I||
   6     ||T||  HELM is free software; you can redistribute it and/or
   7     ||A||  modify it under the terms of the GNU General Public License
   8     \   /  version 2 or (at your option) any later version.
   9      \ /   This software is distributed as is, NO WARRANTY.
  10       V_______________________________________________________________ *)
  11
  12 {
  13    module KT = String
  14
  15    module L  = Log
  16    module G  = Options
  17    module AP = AutParser
  18
  19    let level = 0
  20
  21 IFDEF LEXER THEN
  22    let out s = if !G.debug_lexer then L.warn level s else ()
  23 END
  24
  25 IFDEF QUOTE THEN
  26 (* This turns an Automath identifier into an XML nmtoken *)
  27    let quote id =
  28       let map = function
  29          | '\''
  30          | '`' -> '_';
  31          | c   -> c
  32       in
  33       KT.map map id
  34
  35 END
  36 }
  37
  38 let LC  = ['#' '%']
  39 let OC  = "{"
  40 let CC  = "}"
  41 let SPC = [' ' '\t' '\n']+
  42 let NL  = "\n"
  43 let ID  = ['0'-'9' 'A'-'Z' 'a'-'z' '_' '\'' '`']+
  44
  45 rule line_comment = parse
  46    | NL  { () }
  47    | OC  { block_comment lexbuf; line_comment lexbuf }
  48    | _   { line_comment lexbuf }
  49    | eof { () }
  50 and block_comment = parse
  51    | CC  { () }
  52    | OC  { block_comment lexbuf; block_comment lexbuf }
  53    | LC  { line_comment lexbuf; block_comment lexbuf  }
  54    | _   { block_comment lexbuf }
  55 and token = parse
  56    | SPC      { token lexbuf }
  57    | LC       { line_comment lexbuf; token lexbuf  }
  58    | OC       { block_comment lexbuf; token lexbuf }
  59    | "_E"     { IFDEF LEXER THEN out "E" ELSE () END; AP.E         }
  60    | "'_E'"   { IFDEF LEXER THEN out "E" ELSE () END; AP.E         }
  61    | "---"    { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
  62    | "'eb'"   { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
  63    | "EB"     { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
  64    | "--"     { IFDEF LEXER THEN out "EXIT" ELSE () END; AP.EXIT   }
  65    | "PN"     { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
  66    | "'pn'"   { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
  67    | "PRIM"   { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
  68    | "'prim'" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
  69    | "???"    { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
  70    | "PROP"   { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP   }
  71    | "'prop'" { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP   }
  72    | "TYPE"   { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE   }
  73    | "'type'" { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE   }
  74    | ID       { IFDEF LEXER THEN out "ID" ELSE () END;
  75                    let s = Lexing.lexeme lexbuf in
  76 IFDEF QUOTE THEN
  77                    if !G.quote then AP.IDENT (quote s) else AP.IDENT s
  78 ELSE
  79                    AP.IDENT s
  80 END
  81               }
  82    | ":="     { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF     }
  83    | "("      { IFDEF LEXER THEN out "OP" ELSE () END; AP.OP       }
  84    | ")"      { IFDEF LEXER THEN out "CP" ELSE () END; AP.CP       }
  85    | "["      { IFDEF LEXER THEN out "OB" ELSE () END; AP.OB       }
  86    | "]"      { IFDEF LEXER THEN out "CB" ELSE () END; AP.CB       }
  87    | "<"      { IFDEF LEXER THEN out "OA" ELSE () END; AP.OA       }
  88    | ">"      { IFDEF LEXER THEN out "CA" ELSE () END; AP.CA       }
  89    | "@"      { IFDEF LEXER THEN out "AT" ELSE () END; AP.AT       }
  90    | "~"      { IFDEF LEXER THEN out "TD" ELSE () END; AP.TD       }
  91    | "\""     { IFDEF LEXER THEN out "QT" ELSE () END; AP.QT       }
  92    | ":"      { IFDEF LEXER THEN out "CN" ELSE () END; AP.CN       }
  93    | ","      { IFDEF LEXER THEN out "CM" ELSE () END; AP.CM       }
  94    | ";"      { IFDEF LEXER THEN out "SC" ELSE () END; AP.SC       }
  95    | "."      { IFDEF LEXER THEN out "FS" ELSE () END; AP.FS       }
  96    | "+"      { IFDEF LEXER THEN out "PLUS" ELSE () END; AP.PLUS   }
  97    | "-"      { IFDEF LEXER THEN out "MINUS" ELSE () END; AP.MINUS }
  98    | "*"      { IFDEF LEXER THEN out "TIMES" ELSE () END; AP.TIMES }
  99    | "="      { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF     }
 100    | eof      { IFDEF LEXER THEN out "EOF" ELSE () END; AP.EOF     }