1d0f14d · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Some combinators for Lexing and Parsing.

1d0f14dJan de Muijnck-Hughes9 years ago

libs/contrib/Text/Lexer.idr+27−17

compare with master

unifiedsplit

@@ -23,11 +23,11 @@ public export

23inf : Bool -> Type -> Type

24inf True t = Inf t

25inf False t = t

26−

26+

27||| Sequence two recognisers. If either consumes a character, the sequence

28||| is guaranteed to consume a character.

29export %inline

30−(<+>) : {c1 : Bool} ->

30+(<+>) : {c1 : Bool} ->

31 Recognise c1 -> inf c1 (Recognise c2) -> Recognise (c1 || c2)

32(<+>) {c1 = False} = SeqEmpty

33(<+>) {c1 = True} = SeqEat

@@ -59,6 +59,17 @@ export

59many : Lexer -> Recognise False

60many l = some l <|> Empty

62+||| Recognise many instances of `l` until an instance of `end` is

63+||| encountered.

64+|||

65+||| Useful for defining comments.

66+export

67+manyTill : (l : Lexer)

68+ -> (end : Lexer) -> Recognise False

69+manyTill l end = end

70+ <|> (l <+> manyTill l end)

71+ <|> Empty

72+

62||| Recognise any character

73||| Recognise any character

63export

74export

64any : Lexer

75any : Lexer

@@ -86,7 +97,7 @@ getString : StrLen -> String

86getString (MkStrLen str n) = str

97getString (MkStrLen str n) = str

88strIndex : StrLen -> Nat -> Maybe Char

99strIndex : StrLen -> Nat -> Maybe Char

89−strIndex (MkStrLen str len) i

100+strIndex (MkStrLen str len) i

90 = if i >= len then Nothing

101 = if i >= len then Nothing

91 else Just (assert_total (prim__strIndex str (cast i)))

102 else Just (assert_total (prim__strIndex str (cast i)))

103

@@ -102,25 +113,25 @@ strTail start (MkStrLen str len)

102scan : Recognise c -> Nat -> StrLen -> Maybe Nat

113scan : Recognise c -> Nat -> StrLen -> Maybe Nat

103scan Empty idx str = pure idx

114scan Empty idx str = pure idx

104scan Fail idx str = Nothing

115scan Fail idx str = Nothing

105−scan (Pred f) idx str

116+scan (Pred f) idx str

106 = do c <- strIndex str idx

117 = do c <- strIndex str idx

107 if f c

118 if f c

108 then Just (idx + 1)

119 then Just (idx + 1)

109 else Nothing

120 else Nothing

110−scan (SeqEat r1 r2) idx str

121+scan (SeqEat r1 r2) idx str

111 = do idx' <- scan r1 idx str

122 = do idx' <- scan r1 idx str

112 -- TODO: Can we prove totality instead by showing idx has increased?

123 -- TODO: Can we prove totality instead by showing idx has increased?

113 assert_total (scan r2 idx' str)

124 assert_total (scan r2 idx' str)

114−scan (SeqEmpty r1 r2) idx str

125+scan (SeqEmpty r1 r2) idx str

115 = do idx' <- scan r1 idx str

126 = do idx' <- scan r1 idx str

116 scan r2 idx' str

127 scan r2 idx' str

117−scan (Alt r1 r2) idx str

128+scan (Alt r1 r2) idx str

118 = case scan r1 idx str of

129 = case scan r1 idx str of

119 Nothing => scan r2 idx str

130 Nothing => scan r2 idx str

120 Just idx => Just idx

131 Just idx => Just idx

121

132

122takeToken : Lexer -> StrLen -> Maybe (String, StrLen)

133takeToken : Lexer -> StrLen -> Maybe (String, StrLen)

123−takeToken lex str

134+takeToken lex str

124 = do i <- scan lex 0 str -- i must be > 0 if successful

135 = do i <- scan lex 0 str -- i must be > 0 if successful

125 pure (substr 0 i (getString str), strTail i str)

136 pure (substr 0 i (getString str), strTail i str)

126

137

@@ -134,7 +145,7 @@ export

134exact : String -> Lexer

145exact : String -> Lexer

135exact str with (unpack str)

146exact str with (unpack str)

136 exact str | [] = Fail -- Not allowed, Lexer has to consume

147 exact str | [] = Fail -- Not allowed, Lexer has to consume

137− exact str | (x :: xs)

148+ exact str | (x :: xs)

138 = foldl SeqEmpty (is x) (map is xs)

149 = foldl SeqEmpty (is x) (map is xs)

139

150

140||| Recognise a whitespace character

151||| Recognise a whitespace character

@@ -185,8 +196,8 @@ record TokenData a where

185

196

186fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)

197fspanEnd : Nat -> (Char -> Bool) -> String -> (Nat, String)

187fspanEnd k p "" = (k, "")

198fspanEnd k p "" = (k, "")

188−fspanEnd k p xxs

199+fspanEnd k p xxs

189− = assert_total $

200+ = assert_total $

190 let x = prim__strHead xxs

201 let x = prim__strHead xxs

191 xs = prim__strTail xxs in

202 xs = prim__strTail xxs in

192 if p x then fspanEnd (S k) p xs

203 if p x then fspanEnd (S k) p xs

@@ -195,14 +206,14 @@ fspanEnd k p xxs

195-- Faster version of 'span' from the prelude (avoids unpacking)

206-- Faster version of 'span' from the prelude (avoids unpacking)

196export

207export

197fspan : (Char -> Bool) -> String -> (String, String)

208fspan : (Char -> Bool) -> String -> (String, String)

198−fspan p xs

209+fspan p xs

199 = let (end, rest) = fspanEnd 0 p xs in

210 = let (end, rest) = fspanEnd 0 p xs in

200 (substr 0 end xs, rest)

211 (substr 0 end xs, rest)

201

212

202tokenise : (line : Int) -> (col : Int) ->

213tokenise : (line : Int) -> (col : Int) ->

203− List (TokenData a) -> TokenMap a ->

214+ List (TokenData a) -> TokenMap a ->

204 StrLen -> (List (TokenData a), (Int, Int, StrLen))

215 StrLen -> (List (TokenData a), (Int, Int, StrLen))

205−tokenise line col acc tmap str

216+tokenise line col acc tmap str

206 = case getFirstToken tmap str of

217 = case getFirstToken tmap str of

207 Just (tok, line', col', rest) =>

218 Just (tok, line', col', rest) =>

208 -- assert total because getFirstToken must consume something

219 -- assert total because getFirstToken must consume something

@@ -213,7 +224,7 @@ tokenise line col acc tmap str

213 countNLs str = List.length (filter (== '\n') str)

224 countNLs str = List.length (filter (== '\n') str)

214

225

215 getCols : String -> Int -> Int

226 getCols : String -> Int -> Int

216− getCols x c

227+ getCols x c

217 = case fspan (/= '\n') (reverse x) of

228 = case fspan (/= '\n') (reverse x) of

218 (incol, "") => c + cast (length incol)

229 (incol, "") => c + cast (length incol)

219 (incol, _) => cast (length incol)

230 (incol, _) => cast (length incol)

@@ -223,7 +234,7 @@ tokenise line col acc tmap str

223 getFirstToken ((lex, fn) :: ts) str

234 getFirstToken ((lex, fn) :: ts) str

224 = case takeToken lex str of

235 = case takeToken lex str of

225 Just (tok, rest) => Just (MkToken line col (fn tok),

236 Just (tok, rest) => Just (MkToken line col (fn tok),

226− line + cast (countNLs (unpack tok)),

237+ line + cast (countNLs (unpack tok)),

227 getCols tok col, rest)

238 getCols tok col, rest)

228 Nothing => getFirstToken ts str

239 Nothing => getFirstToken ts str

229

240

@@ -235,4 +246,3 @@ export

235lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))

246lex : TokenMap a -> String -> (List (TokenData a), (Int, Int, String))

236lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in

247lex tmap str = let (ts, (l, c, str')) = tokenise 0 0 [] tmap (mkStr str) in

237 (ts, (l, c, getString str'))

248 (ts, (l, c, getString str'))

238−

libs/contrib/Text/Parser.idr+67−26

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

3%default total

5-- TODO: Add some primitives for helping with error messages.

6−-- e.g. perhaps set a string to state what we're currently trying to

6+-- e.g. perhaps set a string to state what we're currently trying to

7-- parse, or to say what the next expected token is in words

9||| Description of a language's grammar. The `tok` parameter is the type

@@ -26,14 +26,14 @@ data Grammar : (tok : Type) -> (consumes : Bool) -> Type -> Type where

26 Grammar tok c1 a -> (a -> Grammar tok c2 b) ->

27 Grammar tok (c1 || c2) b

28 Alt : {c1, c2 : Bool} ->

29− Grammar tok c1 ty -> Grammar tok c2 ty ->

29+ Grammar tok c1 ty -> Grammar tok c2 ty ->

30 Grammar tok (c1 && c2) ty

32public export

33inf : Bool -> Type -> Type

34inf True t = Inf t

35inf False t = t

36−

36+

37||| Sequence two grammars. If either consumes some input, the sequence is

38||| guaranteed to consume some input. If the first one consumes input, the

39||| second is allowed to be recursive (because it means some input has been

@@ -44,11 +44,11 @@ export %inline

44 Grammar tok (c1 || c2) b

45(>>=) {c1 = False} = SeqEmpty

46(>>=) {c1 = True} = SeqEat

47−

47+

48||| Give two alternative grammars. If both consume, the combination is

49||| guaranteed to consume.

50export

51−(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->

51+(<|>) : Grammar tok c1 ty -> Grammar tok c2 ty ->

52 Grammar tok (c1 && c2) ty

53(<|>) = Alt

@@ -82,21 +82,21 @@ export

82eof : Grammar tok False ()

83eof = EOF

85−||| Commit to an alternative; if the current branch of an alternative

85+||| Commit to an alternative; if the current branch of an alternative

86||| fails to parse, no more branches will be tried

87export

88commit : Grammar tok False ()

89commit = Commit

91data ParseResult : List tok -> (consumes : Bool) -> Type -> Type where

92− Failure : {xs : List tok} ->

92+ Failure : {xs : List tok} ->

93 (committed : Bool) ->

94 (err : String) -> (rest : List tok) -> ParseResult xs c ty

95 EmptyRes : (committed : Bool) ->

96 (val : ty) -> (more : List tok) -> ParseResult more False ty

97 NonEmptyRes : (committed : Bool) ->

98 (val : ty) -> (more : List tok) ->

99− ParseResult (x :: xs ++ more) c ty

99+ ParseResult (x :: xs ++ more) c ty

100

101weakenRes : {whatever, c : Bool} -> {xs : List tok} ->

102 ParseResult xs c ty -> ParseResult xs (whatever && c) ty

@@ -105,13 +105,13 @@ weakenRes {whatever=True} (EmptyRes com val xs) = EmptyRes com val xs

105weakenRes {whatever=False} (EmptyRes com val xs) = EmptyRes com val xs

106weakenRes (NonEmptyRes com val more) = NonEmptyRes com val more

107

108−shorter : (more : List tok) -> .(ys : List tok) ->

108+shorter : (more : List tok) -> .(ys : List tok) ->

109 LTE (S (length more)) (S (length (ys ++ more)))

110shorter more [] = lteRefl

111shorter more (x :: xs) = LTESucc (lteSuccLeft (shorter more xs))

112

113doParse : {c : Bool} ->

114− (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->

114+ (commit : Bool) -> (xs : List tok) -> (act : Grammar tok c ty) ->

115 ParseResult xs c ty

116doParse com xs act with (sizeAccessible xs)

117 doParse com xs (Empty val) | sml = EmptyRes com val xs

@@ -120,17 +120,17 @@ doParse com xs act with (sizeAccessible xs)

120 doParse com xs Commit | sml = EmptyRes True () xs

121

122 doParse com [] (Terminal f) | sml = Failure com "End of input" []

123− doParse com (x :: xs) (Terminal f) | sml

123+ doParse com (x :: xs) (Terminal f) | sml

124 = maybe

125 (Failure com "Unrecognised token" (x :: xs))

126 (\a => NonEmptyRes com {xs=[]} a xs)

127 (f x)

128 doParse com [] EOF | sml = EmptyRes com () []

129− doParse com (x :: xs) EOF | sml

129+ doParse com (x :: xs) EOF | sml

130 = Failure com "Expected end of input" (x :: xs)

131 doParse com [] (NextIs f) | sml = Failure com "End of input" []

132− doParse com (x :: xs) (NextIs f) | sml

132+ doParse com (x :: xs) (NextIs f) | sml

133− = if f x

133+ = if f x

134 then EmptyRes com x (x :: xs)

135 else Failure com "Unrecognised token" (x :: xs)

136 doParse com xs (Alt x y) | sml with (doParse False xs x | sml)

@@ -140,19 +140,19 @@ doParse com xs act with (sizeAccessible xs)

140 then Failure com msg ts

141 else weakenRes (doParse False xs y | sml)

142 -- Successfully parsed the first option, so use the outer commit flag

143− doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)

143+ doParse com xs (Alt x y) | sml | (EmptyRes _ val xs)

144 = EmptyRes com val xs

145− doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)

145+ doParse com (z :: (ys ++ more)) (Alt x y) | sml | (NonEmptyRes _ val more)

146 = NonEmptyRes com val more

147 doParse com xs (SeqEmpty act next) | (Access morerec)

148 = case doParse com xs act | Access morerec of

149 Failure com msg ts => Failure com msg ts

150− EmptyRes com val xs =>

150+ EmptyRes com val xs =>

151 case doParse com xs (next val) | (Access morerec) of

152 Failure com' msg ts => Failure com' msg ts

153 EmptyRes com' val xs => EmptyRes com' val xs

154 NonEmptyRes com' val more => NonEmptyRes com' val more

155− NonEmptyRes {x} {xs=ys} com val more =>

155+ NonEmptyRes {x} {xs=ys} com val more =>

156 case (doParse com more (next val) | morerec _ (shorter more ys)) of

157 Failure com' msg ts => Failure com' msg ts

158 EmptyRes com' val _ => NonEmptyRes com' val more

@@ -160,13 +160,13 @@ doParse com xs act with (sizeAccessible xs)

160 rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in

161 NonEmptyRes com' val more'

162 doParse com xs (SeqEat act next) | sml with (doParse com xs act | sml)

163− doParse com xs (SeqEat act next) | sml | Failure com' msg ts

163+ doParse com xs (SeqEat act next) | sml | Failure com' msg ts

164 = Failure com' msg ts

165− doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)

165+ doParse com (x :: (ys ++ more)) (SeqEat act next) | (Access morerec) | (NonEmptyRes com' val more)

166 = case doParse com' more (next val) | morerec _ (shorter more ys) of

167 Failure com' msg ts => Failure com' msg ts

168 EmptyRes com' val _ => NonEmptyRes com' val more

169− NonEmptyRes {x=x1} {xs=xs1} com' val more' =>

169+ NonEmptyRes {x=x1} {xs=xs1} com' val more' =>

170 rewrite appendAssociative (x :: ys) (x1 :: xs1) more' in

171 NonEmptyRes com' val more'

172 -- This next line is not strictly necessary, but it stops the coverage

@@ -180,7 +180,7 @@ data ParseError tok = Error String (List tok)

180||| returns a pair of the parse result and the unparsed tokens (the remaining

181||| input).

182export

183−parse : (xs : List tok) -> (act : Grammar tok c ty) ->

183+parse : (xs : List tok) -> (act : Grammar tok c ty) ->

184 Either (ParseError tok) (ty, List tok)

185parse xs act

186 = case doParse False xs act of

@@ -190,7 +190,7 @@ parse xs act

190

191||| Parse one or more things

192export

193−some : Grammar tok True a ->

193+some : Grammar tok True a ->

194 Grammar tok True (List a)

195some p = do x <- p

196 (do xs <- some p

@@ -198,14 +198,14 @@ some p = do x <- p

198

199||| Parse zero or more things (may match the empty input)

200export

201−many : Grammar tok True a ->

201+many : Grammar tok True a ->

202 Grammar tok False (List a)

203many p = some p

204 <|> pure []

205

206||| Parse one or more things, separated by another thing

207export

208−sepBy1 : Grammar tok True () -> Grammar tok True a ->

208+sepBy1 : Grammar tok True () -> Grammar tok True a ->

209 Grammar tok True (List a)

210sepBy1 sep p = do x <- p

211 (do sep

@@ -215,7 +215,7 @@ sepBy1 sep p = do x <- p

215||| Parse zero or more things, separated by another thing. May

216||| match the empty input.

217export

218−sepBy : Grammar tok True () -> Grammar tok True a ->

218+sepBy : Grammar tok True () -> Grammar tok True a ->

219 Grammar tok False (List a)

220sepBy sep p = sepBy1 sep p <|> pure []

221

@@ -227,3 +227,44 @@ optional : Grammar tok True a -> (ifNothing : a) ->

227optional p def = p <|> pure def

228

229

230+||| Parse an instance of `p` that is between `left` and `right`.

231+export

232+between : (left : Grammar tok True ())

233+ -> (right : Grammar tok True ())

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

235+ -> Grammar tok True a

236+between left right contents = do

237+ left

238+ res <- contents

239+ right

240+ pure res

241+

242+||| Parse one or more instances of `p` separated by `s`, returning the

243+||| parsed items and proof the resulting list is non-empty.

244+export

245+sepBy1' : (sep : Grammar tok True ())

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

247+ -> Grammar tok True (xs : List a ** NonEmpty xs)

248+sepBy1' sep p

249+ = do x <- p

250+ (do sep

251+ xs <- sepBy1 sep p

252+ pure (x :: xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)

253+

254+||| Parse one or more instances of `p`, returning the parsed items and proof the resulting list is non-empty.

255+export

256+some' : (p : Grammar tok True a)

257+ -> Grammar tok True (xs : List a ** NonEmpty xs)

258+some' p = do

259+ x <- p

260+ (do xs <- some p

261+ pure (x::xs ** IsNonEmpty)) <|> pure ([x] ** IsNonEmpty)

262+

263+

264+||| Optionally parse a thing. If the grammar provides a default use `optional` instead.

265+export

266+maybe : Grammar tok True a

267+ -> Grammar tok False (Maybe a)

268+maybe p =

269+ (do res <- p; pure $ Just res)

270+ <|> pure Nothing