]> matita.cs.unibo.it Git - helm.git/blob - helm/software/components/tptp_grafite/lexer.mll
Trick: the refiner always subst-expands the outtype, so that the beta-redex
[helm.git] / 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 *) }