pieuvre/lexer.mll

{
  open Parser
  exception Eof
}

let lowercase = ['a'-'z']
let uppercase = ['A'-'Z']
let digit = ['0'-'9'] 
let word = (lowercase | uppercase)*

let var_id = lowercase lowercase* digit*
let ty_id = uppercase uppercase* digit*

rule token = parse
  | [' ' '\t' '\n']      { token lexbuf }
  | '.'             { DOT }
  | ','             { COMMA }
  | "False"         { BOT }
  | '('             { LPAREN }
  | ')'             { RPAREN }
  | "fun"           { FUN }
  | ':'             { COLON }
  | "=>"            { ARR }
  | "->"            { TARR }
  | '~'             { TILDE }
  | "exf"           { EXFALSO }
  | "/\\"           { AND }
  | "\\/"           { OR }
  | "l"             { L }
  | "r"             { R }

  | "Goal"          { GOAL }
  | "Undo"          { UNDO }
  | "Qed"           { QED }
  | "Check"          { CHECK }
  | "exact"         { EXACT }
  | "assumption"    { ASSUMPTION }
  | "intros"        { INTROS }
  | "intro"         { INTRO }
  | "cut"           { CUT }
  | "apply"         { APPLY }
  | "left"          { LEFT }
  | "right"         { RIGHT }
  | "split"         { SPLIT }
  | "try"           { TRY }

  | var_id as s     { VARID(s) }
  | ty_id as s      { TYID(s) }
  | eof             { EOF }