helm/software/components/tptp_grafite/lexerTHF.mll

   1 {
   2   open ParserTHF
   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" | "type"
  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    | "thf" { THF }
  38    | "$true" { TRUE }
  39    | "$false" { FALSE }
  40    | "equal" { PEQ }
  41
  42    | "$i" { TYPE_I }
  43    | "$o" { TYPE_O }
  44    | "$tType" { TYPE_U }
  45    | ">" { TO }
  46
  47    | lname { LNAME (Lexing.lexeme lexbuf) }
  48    | uname { UNAME (Lexing.lexeme lexbuf) }
  49
  50    | ['0' - '9']+ { NUM (int_of_string (Lexing.lexeme lexbuf)) }
  51    | ',' { COMMA }
  52    | '.' { DOT }
  53    | '(' { LPAREN }
  54    | ')' { RPAREN }
  55    | '|' { IOR }
  56    | '&' { IAND }
  57    | '~' { NOT }
  58    | '=' { IEQ }
  59    | "=>" { IMPLY }
  60    | "<=" { IMPLYLR }
  61    | "<=>" { COIMPLY }
  62    | "<~>" { XOR }
  63    | "!=" { NIEQ }
  64    | "!" { FORALL }
  65    | "?" { EXISTS }
  66    | "!" { FORALL }
  67    | "^" { LAMBDA }
  68    | "[" { BEGINVARLIST }
  69    | "]" { ENDVARLIST }
  70    | ":" { COLON }
  71    | "," { COMMA }
  72    | "@" { APPLY }
  73    | qstring { QSTRING (Lexing.lexeme lexbuf) }
  74    | eof { EOF }
  75    | _ { raise (BadToken (Lexing.lexeme lexbuf)) }
  76
  77 { (* trailer *) }