50 lines
887 B
Idris
50 lines
887 B
Idris
module Quox.Token
|
|
|
|
import Generics.Derive
|
|
import Text.Lexer
|
|
|
|
%default total
|
|
%language ElabReflection
|
|
|
|
|
|
public export
|
|
data Punc
|
|
= LParen | RParen
|
|
| LSquare | RSquare
|
|
| LBrace | RBrace
|
|
| Comma
|
|
| Colon | DblColon
|
|
| Dot
|
|
| Arrow | DblArrow
|
|
| Times | Triangle
|
|
| Wild
|
|
%runElab derive "Punc" [Generic, Meta, Eq, Ord, DecEq, Show]
|
|
|
|
|
|
public export
|
|
data Keyword
|
|
= Lam | Let | In | Case | Of | Omega
|
|
| Pi | Sigma | W
|
|
%runElab derive "Keyword" [Generic, Meta, Eq, Ord, DecEq, Show]
|
|
|
|
|
|
||| zero and one are separate because they are
|
|
||| quantity & dimension constants
|
|
public export
|
|
data Number = Zero | One | Other Nat
|
|
%runElab derive "Number" [Generic, Meta, Eq, Ord, DecEq, Show]
|
|
|
|
|
|
public export
|
|
data Token
|
|
= P Punc
|
|
| K Keyword
|
|
| Name String | Symbol String
|
|
| N Number | TYPE Nat
|
|
%runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]
|
|
|
|
|
|
public export
|
|
BToken : Type
|
|
BToken = WithBounds Token
|