helm/software/lambda-delta/src/text/txtLexer.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 TP = TxtParser
  16
  17    let out s = if !G.debug_lexer then L.warn s else ()
  18 }
  19
  20 let BS    = "\\"
  21 let SPC   = [' ' '\t' '\n']+
  22 let OC    = "\\*"
  23 let CC    = "*\\"
  24 let FIG   = ['0'-'9']
  25 let ALPHA = ['A'-'Z' 'a'-'z' '_']
  26 let QT    = '"'
  27 let ID    = ALPHA+ (ALPHA | FIG)*
  28 let IX    = FIG+
  29
  30 rule block_comment = parse
  31    | CC  { () }
  32    | OC  { block_comment lexbuf; block_comment lexbuf }
  33    | _   { block_comment lexbuf }
  34 and qstring = parse
  35    | QT    { ""                                }
  36    | SPC   { " " ^ qstring lexbuf              }
  37    | BS BS { "\\" ^ qstring lexbuf             }
  38    | BS QT { "\"" ^ qstring lexbuf             }
  39    | _ as c { String.make 1 c ^ qstring lexbuf }
  40 and token = parse
  41    | SPC          { token lexbuf                                         }
  42    | OC           { block_comment lexbuf; token lexbuf                   }
  43    | ID as id     { out ("ID " ^ id); TP.ID id                           }
  44    | IX as ix     { out ("IX " ^ ix); TP.IX (int_of_string ix)           }
  45    | QT           { let s = qstring lexbuf in out ("STR " ^ s); TP.STR s }
  46    | "\\graph"    { out "GRAPH"; TP.GRAPH }
  47    | "\\main"     { out "MAIN"; TP.MAIN   }
  48    | "\\decl"     { out "DECL"; TP.DECL   }
  49    | "\\ax"       { out "AX"; TP.AX       }
  50    | "\\cong"     { out "CONG"; TP.CONG   }
  51    | "\\def"      { out "DEF"; TP.DEF     }
  52    | "\\th"       { out "TH"; TP.TH       }
  53    | "\\generate" { out "GEN"; TP.GEN     }
  54    | "\\require"  { out "REQ"; TP.REQ     }
  55    | "\\open"     { out "OPEN"; TP.OPEN   }
  56    | "\\close"    { out "CLOSE"; TP.CLOSE }
  57    | "\\sorts"    { out "SORTS"; TP.SORTS }
  58    | "("          { out "OP"; TP.OP       }
  59    | ")"          { out "CP"; TP.CP       }
  60    | "["          { out "OB"; TP.OB       }
  61    | "]"          { out "CB"; TP.CB       }
  62    | "<"          { out "OA"; TP.OA       }
  63    | ">"          { out "CA"; TP.CA       }
  64    | "."          { out "FS"; TP.FS       }
  65    | ":"          { out "CN"; TP.CN       }
  66    | ","          { out "CM"; TP.CM       }
  67    | "="          { out "EQ"; TP.EQ       }
  68    | "*"          { out "STAR"; TP.STAR   }
  69    | "#"          { out "HASH"; TP.HASH   }
  70    | "+"          { out "PLUS"; TP.PLUS   }
  71    | "~"          { out "TE"; TP.TE       }
  72    | "->"         { out "WTO"; TP.WTO     }
  73    | "=>"         { out "STO"; TP.STO     }
  74    | "^"          { out "CT"; TP.CT       }
  75    | eof          { out "EOF"; TP.EOF     }