less prototype, less bad code implementation of CCHM type theory
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.

90 lines
1.4 KiB

  1. module Presyntax.Tokens where
  2. import qualified Data.Text as T
  3. import Data.Text (Text)
  4. data TokenClass
  5. = TokVar Text
  6. | TokEof
  7. | TokLambda
  8. | TokArrow
  9. | TokOParen
  10. | TokOBrace
  11. | TokOSquare
  12. | TokCParen
  13. | TokCBrace
  14. | TokCSquare
  15. -- {-# #-}
  16. | TokOPragma
  17. | TokCPragma
  18. | TokPrim
  19. | TokReplLet
  20. | TokReplT Text
  21. | TokStar
  22. | TokColon
  23. | TokEqual
  24. | TokComma
  25. | TokPi1
  26. | TokPi2
  27. | TokLet
  28. | TokIn
  29. | TokLStart
  30. | TokLEnd
  31. | TokAnd
  32. | TokOr
  33. | TokAs
  34. | TokWhere
  35. | TokPostulate
  36. | TokSemi
  37. deriving (Eq, Show, Ord)
  38. tokSize :: TokenClass -> Int
  39. tokSize (TokVar x) = T.length x
  40. tokSize TokEof = 0
  41. tokSize TokLambda = 1
  42. tokSize TokOParen = 1
  43. tokSize TokOBrace = 1
  44. tokSize TokOSquare = 1
  45. tokSize TokCBrace = 1
  46. tokSize TokCParen = 1
  47. tokSize TokCSquare = 1
  48. tokSize TokCPragma = 3
  49. tokSize TokOPragma = 3
  50. tokSize TokPrim = length "PRIMITIVE"
  51. tokSize TokStar = 1
  52. tokSize TokColon = 1
  53. tokSize TokEqual = 1
  54. tokSize TokComma = 1
  55. tokSize TokSemi = 1
  56. tokSize TokArrow = 2
  57. tokSize TokPi1 = 2
  58. tokSize TokPi2 = 2
  59. tokSize TokReplLet = 4
  60. tokSize TokAnd = 2
  61. tokSize TokOr = 2
  62. tokSize TokAs = 2
  63. tokSize (TokReplT s) = T.length s
  64. tokSize TokLet = 3
  65. tokSize TokIn = 2
  66. tokSize TokLStart = 0
  67. tokSize TokLEnd = 0
  68. tokSize TokWhere = length "where"
  69. tokSize TokPostulate = length "postulate"
  70. data Token
  71. = Token { tokenClass :: TokenClass
  72. , tokStartLine :: !Int
  73. , tokStartCol :: !Int
  74. }
  75. deriving (Eq, Show, Ord)