47 lines
1.5 KiB
OCaml
47 lines
1.5 KiB
OCaml
{
|
|
open Parser
|
|
}
|
|
|
|
rule token = parse
|
|
| [' ' '\t' '\n'] { token lexbuf }
|
|
| eof { EOF }
|
|
|
|
| '(' { LPAREN }
|
|
| ')' { RPAREN }
|
|
| "->" { RARROW }
|
|
| '~' { TILDE }
|
|
| "/\\" { LAND } (* logical and *)
|
|
| "\\/" { LOR } (* logical or *)
|
|
| ',' { COMMA }
|
|
|
|
| "intro" { INTRO }
|
|
| "intros" { INTROS }
|
|
| "assumption" { ASSUMPTION }
|
|
| "apply" { APPLY }
|
|
| "elim" { ELIM }
|
|
| "cut" { CUT }
|
|
| "split" { SPLIT }
|
|
| "left" { LEFT }
|
|
| "right" { RIGHT }
|
|
| "exact" { EXACT }
|
|
|
|
| "False" { FALSE }
|
|
| "True" { TRUE }
|
|
|
|
| "fun" { FUN }
|
|
| "=>" { MAPS_TO }
|
|
| ':' { COLON }
|
|
| "exf" { EXF }
|
|
| "fst" { FST }
|
|
| "snd" { SND }
|
|
| "ig" { IG }
|
|
| "id" { ID }
|
|
| "case" { CASE }
|
|
| 'I' { I }
|
|
|
|
| '&' { AMPERSAND }
|
|
|
|
| ['A'-'Z']+['0'-'9']* as s { TYPE_NAME s }
|
|
| ['a'-'z']+['0'-'9']* as s { VAR_NAME s }
|
|
| '.' { DOT }
|