0659508 · Idris-dev · git.iko.soy

libs/contrib/Text/Lexer.idr+10−23

compare with master

unifiedsplit

@@ -3,6 +3,7 @@ module Text.Lexer

3import Data.Bool.Extra

4

5import public Text.Lexer.Core

6+import public Text.Quantity

6

7

7%default total

8%default total

8%access export

9%access export

@@ -109,29 +110,15 @@ manyTill l end = end <|> opt (l <+> manyTill l end)

109%deprecate manyTill

110%deprecate manyTill

110 "Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."

111 "Prefer `lineComment`, or `manyUntil`/`manyThen` (argument order is flipped)."

111

112

112−||| Recognise a sub-lexer at least `min` times. Consumes input unless

113+||| Recognise a sub-lexer repeated as specified by `q`. Fails if `q` has

113−||| min is zero.

114−atLeast : (min : Nat) -> (l : Lexer) -> Recognise (min > 0)

115−atLeast Z l = many l

116−atLeast (S min) l = l <+> atLeast min l

117−

118−||| Recognise a sub-lexer at most `max` times. Not guaranteed to

119−||| consume input.

120−atMost : (max : Nat) -> (l : Lexer) -> Recognise False

121−atMost Z _ = empty

122−atMost (S k) l = atMost k l <+> opt l

123−

124−||| Recognise a sub-lexer repeated between `min` and `max` times. Fails

125−||| if the inputs are out of order. Consumes input unless min is zero.

114+||| `min` and `max` in the wrong order. Consumes input unless `min q` is zero.

126−between : (min : Nat) -> (max : Nat) -> (l : Lexer) -> Recognise (min > 0)

115+count : (q : Quantity) -> (l : Lexer) -> Recognise (isSucc (min q))

116+count (Qty Z Nothing) l = many l

117+count (Qty Z (Just Z)) _ = empty

127−between Z max l = atMost max l

118+count (Qty Z (Just (S max))) l = opt $ l <+> count (atMost max) l

119+count (Qty (S min) Nothing) l = l <+> count (atLeast min) l

128−between (S min) Z _ = fail

120+count (Qty (S min) (Just Z)) _ = fail

129−between (S min) (S max) l = l <+> between min max l

121+count (Qty (S min) (Just (S max))) l = l <+> count (between min max) l

130−

131−||| Recognise exactly `count` repeated occurrences of a sub-lexer.

132−||| Consumes input unless count is zero.

133−exactly : (count : Nat) -> (l : Lexer) -> Recognise (count > 0)

134−exactly n l = between n n l

135

122

136||| Recognise a single digit 0-9

123||| Recognise a single digit 0-9

137digit : Lexer

124digit : Lexer

libs/contrib/Text/Parser.idr+23−2

@@ -3,6 +3,7 @@ module Text.Parser

3import Data.Bool.Extra

4

5import public Text.Parser.Core

6+import public Text.Quantity

6

7

7%access export

8%access export

8%default total

9%default total

@@ -12,8 +13,8 @@ import public Text.Parser.Core

12option : {c : Bool} ->

13option : {c : Bool} ->

13 (def : a) -> (p : Grammar tok c a) ->

14 (def : a) -> (p : Grammar tok c a) ->

14 Grammar tok False a

15 Grammar tok False a

15−option {c} def p = rewrite sym (andFalseFalse c) in

16+option {c = False} def p = p <|> pure def

16− p <|> pure def

17+option {c = True} def p = p <|> pure def

17

18

18||| Optionally parse a thing.

19||| Optionally parse a thing.

19||| To provide a default value, use `option` instead.

20||| To provide a default value, use `option` instead.

@@ -63,6 +64,26 @@ some' : (p : Grammar tok True a) ->

63 Grammar tok True (xs : List a ** NonEmpty xs)

64 Grammar tok True (xs : List a ** NonEmpty xs)

64some' p = pure (!p :: !(many p) ** IsNonEmpty)

65some' p = pure (!p :: !(many p) ** IsNonEmpty)

65

66

67+mutual

68+ private

69+ count1 : (q : Quantity) ->

70+ (p : Grammar tok True a) ->

71+ Grammar tok True (List a)

72+ count1 q p = do x <- p

73+ seq (count q p)

74+ (\xs => pure (x :: xs))

75+

76+ ||| Parse `p`, repeated as specified by `q`, returning the list of values.

77+ count : (q : Quantity) ->

78+ (p : Grammar tok True a) ->

79+ Grammar tok (isSucc (min q)) (List a)

80+ count (Qty Z Nothing) p = many p

81+ count (Qty Z (Just Z)) _ = pure []

82+ count (Qty Z (Just (S max))) p = option [] $ count1 (atMost max) p

83+ count (Qty (S min) Nothing) p = count1 (atLeast min) p

84+ count (Qty (S min) (Just Z)) _ = fail "Quantity out of order"

85+ count (Qty (S min) (Just (S max))) p = count1 (between (S min) max) p

86+

66mutual

87mutual

67 ||| Parse one or more instances of `p` until `end` succeeds, returning the

88 ||| Parse one or more instances of `p` until `end` succeeds, returning the

68 ||| list of values from `p`. Guaranteed to consume input.

89 ||| list of values from `p`. Guaranteed to consume input.

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

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

1+module Text.Quantity

2+

3+%access public export

4+%default total

5+

6+record Quantity where

7+ constructor Qty

8+ min : Nat

9+ max : Maybe Nat

10+

11+Show Quantity where

12+ show (Qty Z Nothing) = "*"

13+ show (Qty Z (Just (S Z))) = "?"

14+ show (Qty (S Z) Nothing) = "+"

15+ show (Qty min max) = "{" ++ show min ++ showMax ++ "}"

16+ where

17+ showMax : String

18+ showMax = case max of

19+ Nothing => ","

20+ Just max' => if min == max'

21+ then ""

22+ else "," ++ show max'

23+

24+between : Nat -> Nat -> Quantity

25+between min max = Qty min (Just max)

26+

27+atLeast : Nat -> Quantity

28+atLeast min = Qty min Nothing

29+

30+atMost : Nat -> Quantity

31+atMost max = Qty 0 (Just max)

32+

33+exactly : Nat -> Quantity

34+exactly n = Qty n (Just n)

35+

36+inOrder : Quantity -> Bool

37+inOrder (Qty min Nothing) = True

38+inOrder (Qty min (Just max)) = min <= max

libs/contrib/contrib.ipkg+1

@@ -61,3 +61,4 @@ modules = CFFI

61 , Text.PrettyPrint.WL.Characters

62 , Text.PrettyPrint.WL.Combinators

63 , Text.PrettyPrint.WL.Core

64+ , Text.Quantity