refactor: reorder token kind constructors.

1 files changed, 104 insertions, 60 deletions

diff --git a/src/Obs/Parser.idr b/src/Obs/Parser.idr
index b00f5a8..bd4139c 100644
--- a/src/Obs/Parser.idr
+++ b/src/Obs/Parser.idr
@@ -16,39 +16,44 @@ import Text.Parser
 %default total
 
 data ObsTokenKind
+  -- Whitespace
   = OTNewlines
   | OTSpaces
+  -- Variables
   | OTIdent
-  -- Keywords
+  -- Universes
   | OTProp
   | OTSet
   | OTNat
-  | OTFst
-  | OTSnd
+  -- Term Forms
   | OTBool
   | OTTrue
   | OTFalse
-  | OTIf
+  | OTUnit
   | OTPoint
   | OTVoid
+  -- Head Forms
+  | OTFst
+  | OTSnd
   | OTAbsurd
   | OTRefl
   | OTTransp
   | OTCast
   | OTCastRefl
-  -- Special symbols
-  | OTUnit
-  -- Grouping symbols
+  -- Lambda Head Forms
+  | OTIf
+  -- Decl Forms
+  | OTThinArrow
+  | OTProduct
+  -- Lambda Form
+  | OTBackslash
+  | OTFatArrow
+  -- Grouping Symbols
   | OTPOpen
   | OTPClose
   | OTAOpen
   | OTAClose
-  -- Definition characters
-  | OTBackslash
-  | OTSlash
-  | OTThinArrow
-  | OTFatArrow
-  | OTProduct
+  -- Other Symbols
   | OTComma
   | OTTilde
   | OTEqual
@@ -57,69 +62,86 @@ data ObsTokenKind
 Eq ObsTokenKind where
   OTNewlines == OTNewlines = True
   OTSpaces == OTSpaces = True
+
   OTIdent == OTIdent = True
+
   OTProp == OTProp = True
   OTSet == OTSet = True
   OTNat == OTNat = True
-  OTFst == OTFst = True
-  OTSnd == OTSnd = True
+
   OTBool == OTBool = True
   OTTrue == OTTrue = True
   OTFalse == OTFalse = True
-  OTIf == OTIf = True
+  OTUnit == OTUnit = True
   OTPoint == OTPoint = True
   OTVoid == OTVoid = True
+
+  OTFst == OTFst = True
+  OTSnd == OTSnd = True
   OTAbsurd == OTAbsurd = True
   OTRefl == OTRefl = True
   OTTransp == OTTransp = True
   OTCast == OTCast = True
   OTCastRefl == OTCastRefl = True
-  OTUnit == OTUnit = True
+
+  OTIf == OTIf = True
+
+  OTThinArrow == OTThinArrow = True
+  OTProduct == OTProduct = True
+
+  OTBackslash == OTBackslash = True
+  OTFatArrow == OTFatArrow = True
+
   OTPOpen == OTPOpen = True
   OTPClose == OTPClose = True
   OTAOpen == OTAOpen = True
   OTAClose == OTAClose = True
-  OTBackslash == OTBackslash = True
-  OTSlash == OTSlash = True
-  OTThinArrow == OTThinArrow = True
-  OTFatArrow == OTFatArrow = True
-  OTProduct == OTProduct = True
+
   OTComma == OTComma = True
   OTTilde == OTTilde = True
   OTEqual == OTEqual = True
   OTColon == OTColon = True
+
   _ == _ = False
 
 Show ObsTokenKind where
   show OTNewlines = "\\n"
   show OTSpaces = " "
+
   show OTIdent = "ident"
+
   show OTProp = "Prop"
   show OTSet = "Set"
   show OTNat = "nat"
-  show OTFst = "fst"
-  show OTSnd = "snd"
+
   show OTBool = "Bool"
   show OTTrue = "True"
   show OTFalse = "False"
-  show OTIf = "if"
+  show OTUnit = "()"
   show OTPoint = "tt"
   show OTVoid = "Void"
+
+  show OTFst = "fst"
+  show OTSnd = "snd"
   show OTAbsurd = "absurd"
   show OTRefl = "refl"
   show OTTransp = "transp"
   show OTCast = "cast"
   show OTCastRefl = "castRefl"
-  show OTUnit = "()"
+
+  show OTIf = "if"
+
+  show OTThinArrow = "->"
+  show OTProduct = "**"
+
+  show OTBackslash = "\\"
+  show OTFatArrow = "=>"
+
   show OTPOpen = "("
   show OTPClose = ")"
   show OTAOpen = "<"
   show OTAClose = ">"
-  show OTBackslash = "\\"
-  show OTSlash = "/"
-  show OTThinArrow = "->"
-  show OTFatArrow = "=>"
-  show OTProduct = "**"
+
   show OTComma = ","
   show OTTilde = "~"
   show OTEqual = "="
@@ -132,33 +154,41 @@ TokenKind ObsTokenKind where
 
   tokValue OTNewlines s = ()
   tokValue OTSpaces s = ()
+
   tokValue OTIdent s = s
+
   tokValue OTProp s = ()
   tokValue OTSet s = ()
   tokValue OTNat s = stringToNatOrZ s
-  tokValue OTFst s = ()
-  tokValue OTSnd s = ()
+
   tokValue OTBool s = ()
   tokValue OTTrue s = ()
   tokValue OTFalse s = ()
-  tokValue OTIf s = ()
+  tokValue OTUnit s = ()
   tokValue OTPoint s = ()
   tokValue OTVoid s = ()
+
+  tokValue OTFst s = ()
+  tokValue OTSnd s = ()
   tokValue OTAbsurd s = ()
   tokValue OTRefl s = ()
   tokValue OTTransp s = ()
   tokValue OTCast s = ()
   tokValue OTCastRefl s = ()
-  tokValue OTUnit s = ()
+
+  tokValue OTIf s = ()
+
+  tokValue OTThinArrow s = ()
+  tokValue OTProduct s = ()
+
+  tokValue OTBackslash s = ()
+  tokValue OTFatArrow s = ()
+
   tokValue OTPOpen s = ()
   tokValue OTPClose s = ()
   tokValue OTAOpen s = ()
   tokValue OTAClose s = ()
-  tokValue OTBackslash s = ()
-  tokValue OTSlash s = ()
-  tokValue OTThinArrow s = ()
-  tokValue OTFatArrow s = ()
-  tokValue OTProduct s = ()
+
   tokValue OTComma s = ()
   tokValue OTTilde s = ()
   tokValue OTEqual s = ()
@@ -170,33 +200,41 @@ ObsToken = Token ObsTokenKind
 Show ObsToken where
   show (Tok OTNewlines s) = "\\n"
   show (Tok OTSpaces s) = " "
+
   show (Tok OTIdent s) = s
+
   show (Tok OTProp s) = "Prop"
   show (Tok OTSet s) = "Set"
   show (Tok OTNat s) = s
-  show (Tok OTFst s) = "fst"
-  show (Tok OTSnd s) = "snd"
+
   show (Tok OTBool s) = "Bool"
   show (Tok OTTrue s) = "True"
   show (Tok OTFalse s) = "False"
-  show (Tok OTIf s) = "if"
+  show (Tok OTUnit s) = "()"
   show (Tok OTPoint s) = "tt"
   show (Tok OTVoid s) = "Void"
+
+  show (Tok OTFst s) = "fst"
+  show (Tok OTSnd s) = "snd"
   show (Tok OTAbsurd s) = "absurd"
   show (Tok OTRefl s) = "refl"
   show (Tok OTTransp s) = "transp"
   show (Tok OTCast s) = "cast"
   show (Tok OTCastRefl s) = "castRefl"
-  show (Tok OTUnit s) = "()"
+
+  show (Tok OTIf s) = "if"
+
+  show (Tok OTThinArrow s) = "->"
+  show (Tok OTProduct s) = "**"
+
+  show (Tok OTBackslash s) = "\\"
+  show (Tok OTFatArrow s) = "=>"
+
   show (Tok OTPOpen s) = "("
   show (Tok OTPClose s) = ")"
   show (Tok OTAOpen s) = "<"
   show (Tok OTAClose s) = ">"
-  show (Tok OTBackslash s) = "\\"
-  show (Tok OTSlash s) = "/"
-  show (Tok OTThinArrow s) = "->"
-  show (Tok OTFatArrow s) = "=>"
-  show (Tok OTProduct s) = "**"
+
   show (Tok OTComma s) = ","
   show (Tok OTTilde s) = "~"
   show (Tok OTEqual s) = "="
@@ -207,21 +245,24 @@ identifier = alpha <+> many alphaNum
 
 keywords : List (String, ObsTokenKind)
 keywords =
-  [ ("Set", OTSet)
-  , ("Prop", OTProp)
-  , ("fst", OTFst)
-  , ("snd", OTSnd)
+  [ ("Prop", OTProp)
+  , ("Set", OTSet)
+
   , ("Bool", OTBool)
   , ("True", OTTrue)
   , ("False", OTFalse)
-  , ("if", OTIf)
   , ("tt", OTPoint)
   , ("Void", OTVoid)
+
+  , ("fst", OTFst)
+  , ("snd", OTSnd)
   , ("absurd", OTAbsurd)
   , ("refl", OTRefl)
   , ("transp", OTTransp)
   , ("cast", OTCast)
   , ("castRefl", OTCastRefl)
+
+  , ("if", OTIf)
   ]
 
 obsTokenMap : TokenMap ObsToken
@@ -232,15 +273,18 @@ obsTokenMap = toTokenMap [(newlines, OTNewlines), (spaces, OTSpaces)] ++
           Nothing => Tok OTIdent s)
   ] ++ toTokenMap
   [ (digits, OTNat)
+
+  , (exact "->", OTThinArrow)
+  , (exact "**", OTProduct)
+
+  , (exact "\\", OTBackslash)
+  , (exact "=>", OTFatArrow)
+
   , (exact "(", OTPOpen)
   , (exact ")", OTPClose)
   , (exact "<", OTAOpen)
   , (exact ">", OTAClose)
-  , (exact "=>", OTFatArrow)
-  , (exact "->", OTThinArrow)
-  , (exact "\\", OTBackslash)
-  , (exact "/", OTSlash)
-  , (exact "**", OTProduct)
+
   , (exact ",", OTComma)
   , (exact "~", OTTilde)
   , (exact "=", OTEqual)
@@ -260,9 +304,9 @@ termForms =
   [ (OTBool, Bool)
   , (OTTrue, True)
   , (OTFalse, False)
+  , (OTUnit, Top)
   , (OTPoint, Point)
   , (OTVoid, Bottom)
-  , (OTUnit, Top)
   ]
 
 headForms : List (ObsTokenKind, (n ** op (WithBounds Syntax) Syntax (S n)))