From 2d7110b9c64aba41c9ded4161494169bf2933e63 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Wed, 4 May 2022 15:30:08 +0200
Subject: [PATCH] tokens in separate file

---
 sirdi.json         |  2 ++
 src/Quox/Lexer.idr | 30 +-----------------------------
 src/Quox/Token.idr | 45 +++++++++++++++++++++++++++++++++++++++++++++
 3 files changed, 48 insertions(+), 29 deletions(-)
 create mode 100644 src/Quox/Token.idr

diff --git a/sirdi.json b/sirdi.json
index 0a192c5..c84ae65 100644
--- a/sirdi.json
+++ b/sirdi.json
@@ -39,6 +39,8 @@
         "Quox.Syntax.Term.Subst",
         "Quox.Syntax.Universe",
         "Quox.Syntax.Var",
+
+        "Quox.Token",
         "Quox.Lexer",
 
         "Quox.Context",
diff --git a/src/Quox/Lexer.idr b/src/Quox/Lexer.idr
index 3b8d924..46a1cae 100644
--- a/src/Quox/Lexer.idr
+++ b/src/Quox/Lexer.idr
@@ -1,6 +1,7 @@
 module Quox.Lexer
 
 import Quox.Error
+import public Quox.Token
 
 import Data.String
 import Data.String.Extra
@@ -19,35 +20,6 @@ record Error where
   line, col : Int
   char      : Char
 
-public export
-data Punc
-= LParen  | RParen
-| LSquare | RSquare
-| LBrace  | RBrace
-| Comma
-| Colon | DblColon
-| Arrow | DblArrow
-| Times | Triangle
-| Wild
-
-%runElab derive "Punc" [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
-| Name String | Symbol String
-| N Number
-
-%runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]
 
 
 nameStart = pred $ \c => isAlpha c || c == '_'
diff --git a/src/Quox/Token.idr b/src/Quox/Token.idr
new file mode 100644
index 0000000..4d51b37
--- /dev/null
+++ b/src/Quox/Token.idr
@@ -0,0 +1,45 @@
+module Quox.Token
+
+import Generics.Derive
+
+%default total
+%language ElabReflection
+
+
+public export
+data Punc
+= LParen  | RParen
+| LSquare | RSquare
+| LBrace  | RBrace
+| Comma
+| Colon | DblColon
+| Arrow | DblArrow
+| Times | Triangle
+| Wild
+
+%runElab derive "Punc" [Generic, Meta, Eq, Ord, DecEq, Show]
+
+
+public export
+data Keyword
+= Fun | Let | In | Case | Of
+
+%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
+| Name String | Symbol String
+| N Number
+| K Keyword
+
+%runElab derive "Token" [Generic, Meta, Eq, Ord, DecEq, Show]