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 L  = Log
  14    module G  = Options
  15    module AP = AutParser
  16
  17    let level = 0
  18
  19 IFDEF LEXER THEN
  20    let out s = if !G.debug_lexer then L.warn level s else ()
  21 END
  22
  23 IFDEF QUOTE THEN
  24 (* This turns an Automath identifier into an XML nmtoken *)
  25    let quote id =
  26       let l = String.length id in
  27       let rec aux i =
  28          if i < l then begin
  29             if id.[i] = '\'' || id.[i] = '`' then id.[i] <- '_';
  30             aux (succ i)
  31          end else
  32             id
  33       in
  34       aux 0
  35
  36 END
  37 }
  38
  39 let LC  = ['#' '%']
  40 let OC  = "{"
  41 let CC  = "}"
  42 let SPC = [' ' '\t' '\n']+
  43 let NL  = "\n"
  44 let ID  = ['0'-'9' 'A'-'Z' 'a'-'z' '_' '\'' '`']+
  45
  46 rule line_comment = parse
  47    | NL  { () }
  48    | OC  { block_comment lexbuf; line_comment lexbuf }
  49    | _   { line_comment lexbuf }
  50    | eof { () }
  51 and block_comment = parse
  52    | CC  { () }
  53    | OC  { block_comment lexbuf; block_comment lexbuf }
  54    | LC  { line_comment lexbuf; block_comment lexbuf  }
  55    | _   { block_comment lexbuf }
  56 and token = parse
  57    | SPC      { token lexbuf }
  58    | LC       { line_comment lexbuf; token lexbuf  }
  59    | OC       { block_comment lexbuf; token lexbuf }
  60    | "_E"     { IFDEF LEXER THEN out "E" ELSE () END; AP.E         }
  61    | "'_E'"   { IFDEF LEXER THEN out "E" ELSE () END; AP.E         }
  62    | "---"    { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
  63    | "'eb'"   { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
  64    | "EB"     { IFDEF LEXER THEN out "EB" ELSE () END; AP.EB       }
  65    | "--"     { IFDEF LEXER THEN out "EXIT" ELSE () END; AP.EXIT   }
  66    | "PN"     { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
  67    | "'pn'"   { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
  68    | "PRIM"   { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
  69    | "'prim'" { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
  70    | "???"    { IFDEF LEXER THEN out "PN" ELSE () END; AP.PN       }
  71    | "PROP"   { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP   }
  72    | "'prop'" { IFDEF LEXER THEN out "PROP" ELSE () END; AP.PROP   }
  73    | "TYPE"   { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE   }
  74    | "'type'" { IFDEF LEXER THEN out "TYPE" ELSE () END; AP.TYPE   }
  75    | ID       { IFDEF LEXER THEN out "ID" ELSE () END;
  76                    let s = Lexing.lexeme lexbuf in
  77 IFDEF QUOTE THEN
  78                    if !G.quote then AP.IDENT (quote s) else AP.IDENT s
  79 ELSE
  80                    AP.IDENT s
  81 END
  82               }
  83    | ":="     { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF     }
  84    | "("      { IFDEF LEXER THEN out "OP" ELSE () END; AP.OP       }
  85    | ")"      { IFDEF LEXER THEN out "CP" ELSE () END; AP.CP       }
  86    | "["      { IFDEF LEXER THEN out "OB" ELSE () END; AP.OB       }
  87    | "]"      { IFDEF LEXER THEN out "CB" ELSE () END; AP.CB       }
  88    | "<"      { IFDEF LEXER THEN out "OA" ELSE () END; AP.OA       }
  89    | ">"      { IFDEF LEXER THEN out "CA" ELSE () END; AP.CA       }
  90    | "@"      { IFDEF LEXER THEN out "AT" ELSE () END; AP.AT       }
  91    | "~"      { IFDEF LEXER THEN out "TD" ELSE () END; AP.TD       }
  92    | "\""     { IFDEF LEXER THEN out "QT" ELSE () END; AP.QT       }
  93    | ":"      { IFDEF LEXER THEN out "CN" ELSE () END; AP.CN       }
  94    | ","      { IFDEF LEXER THEN out "CM" ELSE () END; AP.CM       }
  95    | ";"      { IFDEF LEXER THEN out "SC" ELSE () END; AP.SC       }
  96    | "."      { IFDEF LEXER THEN out "FS" ELSE () END; AP.FS       }
  97    | "+"      { IFDEF LEXER THEN out "PLUS" ELSE () END; AP.PLUS   }
  98    | "-"      { IFDEF LEXER THEN out "MINUS" ELSE () END; AP.MINUS }
  99    | "*"      { IFDEF LEXER THEN out "TIMES" ELSE () END; AP.TIMES }
 100    | "="      { IFDEF LEXER THEN out "DEF" ELSE () END; AP.DEF     }
 101    | eof      { IFDEF LEXER THEN out "EOF" ELSE () END; AP.EOF     }