helm/software/components/tptp_grafite/lexer.mll

   1 {
   2   open Parser
   3   exception BadToken of string
   4
   5   let incr_linenum lexbuf =
   6     let pos = lexbuf.Lexing.lex_curr_p in
   7     lexbuf.Lexing.lex_curr_p <- { pos with
   8       Lexing.pos_lnum = pos.Lexing.pos_lnum + 1;
   9       Lexing.pos_bol = pos.Lexing.pos_cnum;
  10     }
  11   ;;
  12
  13 }
  14
  15 let dust = ' ' | '\t'
  16 let comment = '%' [^ '\n' ] * '\n'
  17 let lname =
  18   ['a'-'z'] ['a'-'z''A'-'Z''0'-'9''_']*
  19 let uname =
  20   ['A'-'Z'] ['a'-'z''A'-'Z''0'-'9''_']*
  21 let qstring = ''' [^ ''' ]+ '''
  22 let type_ =
  23   "axiom" | "hypothesis" | "definition" | "lemma" | "theorem" |
  24   "conjecture" | "lemma_conjecture" | "negated_conjecture" |
  25   "plain" | "unknown"
  26
  27 let ieq = "="
  28 let peq = "equal"
  29 let nieq = "!="
  30
  31 rule yylex = parse
  32    | dust { yylex lexbuf }
  33    | '\n' { incr_linenum lexbuf; yylex lexbuf }
  34    | comment { incr_linenum lexbuf; COMMENT (Lexing.lexeme lexbuf) }
  35    | "include" { INCLUSION }
  36    | type_ { TYPE (Lexing.lexeme lexbuf) }
  37    | "cnf" { CNF }
  38    | "$true" { TRUE }
  39    | "$false" { FALSE }
  40    | "equal" { PEQ }
  41
  42    | lname { LNAME (Lexing.lexeme lexbuf) }
  43    | uname { UNAME (Lexing.lexeme lexbuf) }
  44    | ['0' - '9']+ { NUM (int_of_string (Lexing.lexeme lexbuf)) }
  45    | ',' { COMMA }
  46    | '.' { DOT }
  47    | '(' { LPAREN }
  48    | ')' { RPAREN }
  49    | '|' { IOR }
  50    | '~' { NOT }
  51    | '=' { IEQ }
  52    | "!=" { NIEQ }
  53    | qstring { QSTRING (Lexing.lexeme lexbuf) }
  54    | eof { EOF }
  55    | _ { raise (BadToken (Lexing.lexeme lexbuf)) }
  56
  57 { (* trailer *) }