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