4064dcf · Idris-dev · git.iko.soy

libs/contrib/Text/Lexer.idr+5−1

compare with master

unifiedsplit

@@ -4,9 +4,13 @@ import Data.Bool.Extra

4

5import public Text.Lexer.Core

6import public Text.Quantity

7+import public Text.Token

7

8

8−%default total

9%access export

10+%default total

11+

12+toTokenMap : List (Lexer, k) -> TokenMap (Token k)

13+toTokenMap = map $ \(l, kind) => (l, Tok kind)

10

14

11||| Recognise any character

15||| Recognise any character

12any : Lexer

16any : Lexer

libs/contrib/Text/Parser.idr+10

@@ -4,10 +4,20 @@ import Data.Bool.Extra

4

5import public Text.Parser.Core

6import public Text.Quantity

7+import public Text.Token

7

8

8%access export

9%access export

9%default total

10%default total

10

11

12+||| Parse a terminal based on a kind of token.

13+match : (Eq k, TokenKind k) =>

14+ (kind : k) ->

15+ Grammar (Token k) True (TokType kind)

16+match kind = terminal $

17+ \(Tok kind' text) => if kind' == kind

18+ then Just $ tokValue kind text

19+ else Nothing

20+

11||| Optionally parse a thing, with a default value if the grammar doesn't

21||| Optionally parse a thing, with a default value if the grammar doesn't

12||| match. May match the empty input.

22||| match. May match the empty input.

13option : {c : Bool} ->

23option : {c : Bool} ->

libs/contrib/Text/Parser/Core.idr+14

@@ -109,6 +109,20 @@ export

109 Grammar tok (c1 || c2) b

110(*>) x y = map (const id) x <*> y

111

112+||| Produce a grammar that can parse a different type of token by providing a

113+||| function converting the new token type into the original one.

114+export

115+mapToken : (a -> b) -> Grammar b c ty -> Grammar a c ty

116+mapToken f (Empty val) = Empty val

117+mapToken f (Terminal g) = Terminal (g . f)

118+mapToken f (NextIs g) = SeqEmpty (NextIs (g . f)) (Empty . f)

119+mapToken f EOF = EOF

120+mapToken f (Fail msg) = Fail msg

121+mapToken f Commit = Commit

122+mapToken f (SeqEat act next) = SeqEat (mapToken f act) (\x => mapToken f (next x))

123+mapToken f (SeqEmpty act next) = SeqEmpty (mapToken f act) (\x => mapToken f (next x))

124+mapToken f (Alt x y) = Alt (mapToken f x) (mapToken f y)

125+

112||| Always succeed with the given value.

126||| Always succeed with the given value.

113export

127export

114pure : (val : ty) -> Grammar tok False ty

128pure : (val : ty) -> Grammar tok False ty

libs/contrib/Text/Token.idrnew file+38

@@ -0,0 +1,38 @@

1+module Text.Token

2+

3+%access public export

4+%default total

5+

6+||| For a type `kind`, specify a way of converting the recognised

7+||| string into a value.

8+|||

9+||| ```idris example

10+||| data SimpleKind = SKString | SKInt | SKComma

11+|||

12+||| TokenKind SimpleKind where

13+||| TokType SKString = String

14+||| TokType SKInt = Int

15+||| TokType SKComma = ()

16+|||

17+||| tokValue SKString x = x

18+||| tokValue SKInt x = cast x

19+||| tokValue SKComma x = ()

20+||| ```

21+interface TokenKind (k : Type) where

22+ ||| The type that a token of this kind converts to.

23+ TokType : k -> Type

24+

25+ ||| Convert a recognised string into a value. The type is determined

26+ ||| by the kind of token.

27+ tokValue : (kind : k) -> String -> TokType kind

28+

29+||| A token of a particular kind and the text that was recognised.

30+record Token k where

31+ constructor Tok

32+ kind : k

33+ text : String

34+

35+||| Get the value of a `Token k`. The resulting type depends upon

36+||| the kind of token.

37+value : TokenKind k => (t : Token k) -> TokType (kind t)

38+value (Tok k x) = tokValue k x

libs/contrib/contrib.ipkg+7−6

@@ -65,6 +65,12 @@ modules = CFFI

65

66 , System.Concurrency.Process

67

68+ , Test.Unit.Display

69+ , Test.Unit.Runners

70+ , Test.Unit.Generic

71+ , Test.Unit.Assertions

72+ , Test.Unit

73+

68 , Text.Lexer

74 , Text.Lexer

69 , Text.Lexer.Core

75 , Text.Lexer.Core

70

76

@@ -79,9 +85,4 @@ modules = CFFI

79 , Text.PrettyPrint.WL

85 , Text.PrettyPrint.WL

80

86

81 , Text.Quantity

87 , Text.Quantity

82−

88+ , Text.Token

83− , Test.Unit.Display

84− , Test.Unit.Runners

85− , Test.Unit.Generic

86− , Test.Unit.Assertions

87− , Test.Unit