matita/matita/contribs/lambdadelta/bin/recomm/recommLexer.mll

   1 {
   2   module EP = RecommParser
   3
   4   let debug = ref false
   5
   6   let keys = [|
   7     "Note";
   8     "NOTE";
   9   |]
  10
  11   let heads = [|
  12     "Advanced";
  13     "Alternative";
  14     "Basic";
  15     "Constructions";
  16     "Forward";
  17     "Destructions";
  18     "Eliminations";
  19     "Eliminators";
  20     "Equalities";
  21     "Helper";
  22     "Inversion";
  23     "Inversions";
  24     "Iterators";
  25     "Main";
  26     "Properties";
  27   |]
  28
  29   let str c = String.make 1 c
  30
  31   let nl lexbuf = Lexing.new_line lexbuf
  32
  33   let is_uppercase_ascii s =
  34     let rec aux i =
  35        if i < 0 then true else
  36        if 'a' <= s.[i] && s.[i] <= 'z' then false else
  37        aux (pred i)
  38     in
  39     aux (String.length s - 1)
  40
  41   let disambiguate_word s =
  42     if Array.mem s keys then EP.KW s else
  43     if Array.mem s heads then EP.HW s else
  44     if is_uppercase_ascii s then EP.CW s else
  45     EP.SW s
  46
  47   let log s =
  48     if !debug then Printf.eprintf "lezer: %s\n" s
  49
  50   let log_s s =
  51     if !debug then Printf.eprintf "lexer: %S\n" s
  52
  53   let log_c c =
  54     if !debug then Printf.eprintf "lexer: %C\n" c
  55 }
  56
  57 let CR = "\r"
  58 let SP = " "
  59 let NL = "\n"
  60 let SR = "*"
  61 let OP = "(*"
  62 let CP = SR* "*)"
  63 let PP = CP SP* OP
  64 let WF = ['A'-'Z' 'a'-'z']
  65 let WB = ['A'-'Z' 'a'-'z' '_' '-']*
  66 let WD = WF WB
  67
  68 rule src_token = parse
  69   | CR       { src_token lexbuf                   }
  70   | NL  as c { log "NL"; nl lexbuf; EP.NL (str c) }
  71   | SP+ as s { log "SP"; EP.SP s                  }
  72   | PP  as s { log "PP"; EP.PP s                  }
  73   | OP  as s { log "OP"; EP.OP s                  }
  74   | CP  as s { log "CP"; EP.CP s                  }
  75   | SR  as c { log "SR"; EP.SR (str c)            }
  76   | WD  as s { log_s s ; disambiguate_word s      }
  77   | _   as c { log_c c ; EP.OT (str c)            }
  78   | eof      { log "EF"; EP.EF                    }