942f55e · Idris-dev · git.iko.soy

1{-

2− Simple monadic parser module, based heavily on that by

2+ Simple monadic parser module, based heavily on that by

3 Graham Hutton.

4-}

5

13

14%access public

15

16−infixr 5 |||

17

16

18{-

17{-

19The monad of parsers

18The monad of parsers

20--------------------

19--------------------

21-}

20-}

22

21

23−data Parser a = P (String -> Either String (a, String))

22+data Parser a = P (String -> Either String (a, String))

24

23

25−parse : Parser a -> String -> Either String (a, String)

24+parse : Parser a -> String -> Either String (a, String)

26−parse (P p) inp = p inp

25+parse (P p) inp = p inp

27

26

28−instance Functor Parser where

27+instance Functor Parser where

29− -- fmap : (a -> b) -> f a -> f b

28+ -- fmap : (a -> b) -> f a -> f b

30− -- fmap : (a -> b) -> Parser a -> Parser b

29+ -- fmap : (a -> b) -> Parser a -> Parser b

31− -- Given a function (a -> b), and a parser a, make a parser b

30+ -- Given a function (a -> b), and a parser a, make a parser b

32− fmap f p = P (\inp => case parse p inp of

31+ fmap f p = P (\inp => case parse p inp of

33− (Left err) => Left err

32+ Left err => Left err

34− -- Apply f to the v that we got from parsing

33+ -- Apply f to the v that we got from parsing

35− (Right (v, rest)) => Right ((f v), rest))

34+ Right (v, rest) => Right ((f v), rest))

36−

37

35

38−instance Applicative Parser where

36+instance Applicative Parser where

39− pure v = P (\inp => Right (v, inp))

37+ pure v = P (\inp => Right (v, inp))

40− -- Parse to get the function, then parse to get the first argument

38+ -- Parse to get the function, then parse to get the first argument

41− a <$> b = P (\inp => do (f, rest) <- parse a inp

39+ a <$> b = P (\inp => do (f, rest) <- parse a inp

42− (x, rest') <- parse b rest

40+ (x, rest') <- parse b rest

43− pure ((f x), rest'))

41+ pure ((f x), rest'))

44

42

45instance Monad Parser where

43instance Monad Parser where

46−-- pure v = P (\inp => Right (v,inp))

47− -- m a -> (a -> m b) -> m b

44+ -- m a -> (a -> m b) -> m b

48− p >>= f = P (\inp => case parse p inp of

45+ p >>= f = P (\inp => case parse p inp of

49− (Left err) => Left err

46+ Left err => Left err

50− (Right (v,rest)) => parse (f v) rest)

47+ Right (v,rest) => parse (f v) rest)

51−

48+

52−--mplus : Monad m => m a -> m a -> m a

49+instance Alternative Parser where

53−mplus : Parser a -> Parser a -> Parser a

50+ empty = P (const (Left "empty"))

54−mplus p q = P (\inp => case parse p inp of

51+ p <|> q = P (\inp => case parse p inp of

55− Left msg => parse q inp

52+ Left msg => parse q inp

56− Right (v,out) => Right(v,out))

53+ Right (v,out) => Right (v,out))

57

54

58

55

59{-

56{-

61-------------

58-------------

62-}

59-}

63

60

64−failure : String -> Parser a

61+failure : String -> Parser a

65−failure msg = P (\inp => Left msg)

62+failure msg = P (\inp => Left msg)

66−

67−item : Parser Char

68−item = P (\inp => case unpack inp of

69− [] => Left "Error! Parsing empty list."

70− (x::xs) => Right (x, pack xs))

71−

72−

73−{-

74−Choice

75−--------

76−---}

77

63

78−(|||) : Parser a -> Parser a -> Parser a

64+item : Parser Char

79−p ||| q = p `mplus` q

65+item = P (\inp => case unpack inp of

66+ [] => Left "Error! Parsing empty list."

67+ (x::xs) => Right (x, pack xs))

80

68

81

69

82--{-

70--{-

83--Derived primitives

71--Derived primitives

84---}

72---}

85

73

86−sat : (Char -> Bool) -> Parser Char

74+sat : (Char -> Bool) -> Parser Char

87−sat p = item >>= (\x => if p x then pure x else failure "failed")

75+sat p = item >>= (\x => if p x then pure x else failure "failed")

88−

89−oneof : List Char -> Parser Char

90−oneof xs = sat (\x => elem x xs)

91

76

92−digit : Parser Char

77+oneof : List Char -> Parser Char

93−digit = sat isDigit

78+oneof xs = sat (\x => elem x xs)

94

79

95−lower : Parser Char

80+digit : Parser Char

96−lower = sat isLower

81+digit = sat isDigit

97

82

98−upper : Parser Char

83+lower : Parser Char

99−upper = sat isUpper

84+lower = sat isLower

100

85

101−letter : Parser Char

86+upper : Parser Char

102−letter = sat isAlpha

87+upper = sat isUpper

103

88

104−alphanum : Parser Char

89+letter : Parser Char

105−alphanum = sat isAlphaNum

90+letter = sat isAlpha

106

91

107−char : Char -> Parser Char

92+alphanum : Parser Char

108−char x = sat (== x)

93+alphanum = sat isAlphaNum

109

94

110−helper : List Char -> Parser (List Char)

95+char : Char -> Parser Char

111−string : String -> Parser String

112−string s = do result <- helper (unpack s)

113− pure (pack result)

114−

115−helper [] = pure Prelude.List.Nil

116−helper (x::xs) = do char x

96+char x = sat (== x)

117− string (cast xs)

118− pure (x :: xs)

119

97

120−many : Parser a -> Parser (List a)

98+string : String -> Parser String

121−many1 : Parser a -> Parser (List a)

99+string s = [| pack (traverse char (unpack s)) |]

122−many1 p = do v <- p

123− vs <- many p

124− pure $ Prelude.List.(::) v vs

125

100

101+many1 : Parser a -> Parser (List a)

102+many : Parser a -> Parser (List a)

103+

104+many1 p = [| p :: many p |]

105+

106+many p = many1 p <|> pure []

126

107

127bool : Parser Bool

108bool : Parser Bool

128−bool = parseTrue ||| parseFalse

109+bool = parseTrue <|> parseFalse

129 where parseTrue : Parser Bool

110 where parseTrue : Parser Bool

130 parseTrue = do oneof ['T', 't']

111 parseTrue = do oneof ['T', 't']

131 string "rue"

112 string "rue"

134 string "alse"

115 string "alse"

135 pure False

116 pure False

136

117

118+ident : Parser String

119+ident = fmap pack [| letter :: many1 alphanum |]

137

120

121+nat : Parser Int

122+nat = do xs <- many digit

123+ pure (cast (cast xs))

138

124

139−

140−many p = many1 p `mplus` pure Prelude.List.Nil

141−

142−

143−

144−ident : Parser String

145−ident = do x <- letter

146− xs <- many1 alphanum

147− pure (pack(x::xs))

148−

149−nat : Parser Int

125+int : Parser Int

150−nat = do xs <- many digit

151− pure (cast (cast xs))

152−

153−

154−int : Parser Int

155−int = neg ||| nat

126+int = neg <|> nat

156 where neg : Parser Int

127 where neg : Parser Int

157 neg = do char '-'

128 neg = do char '-'

158 n <- nat

129 n <- nat

159 pure (-n)

130 pure (-n)

160

131

161−space : Parser ()

132+space : Parser ()

162−space = do many (sat isSpace)

133+space = do many (sat isSpace)

163− pure ()

134+ pure ()

164--{-

135--{-

165--Ignoring spacing

136--Ignoring spacing

166---}

137---}

167

138

168−token : Parser a -> Parser a

139+token : Parser a -> Parser a

169−token p = do space

140+token p = do space

170− v <- p

141+ v <- p

171− space

142+ space

172− pure v

143+ pure v

173

144

174−identifier : Parser String

145+identifier : Parser String

175−identifier = token ident

146+identifier = token ident

176

147

177−natural : Parser Int

148+natural : Parser Int

178−natural = token nat

149+natural = token nat

179

150

180−integer : Parser Int

151+integer : Parser Int

181−integer = token int

152+integer = token int

182

153

183−symbol : String -> Parser String

154+symbol : String -> Parser String

184−symbol xs = token (string xs)

155+symbol xs = token (string xs)

185

156

186strToken : Parser String

157strToken : Parser String

187strToken = fmap pack (token (many1 alphanum))

158strToken = fmap pack (token (many1 alphanum))

193-- Expressions

164-- Expressions

194---}

165---}

195

166

196−factor : Parser Int

167+expr : Parser Int

197−term : Parser Int

168+factor : Parser Int

198−expr : Parser Int

169+term : Parser Int

170+

199−expr = do t <- term

171+expr = do t <- term

200− do symbol "+"

172+ fmap (t+) (symbol "+" $> expr) <|> pure t

201− e <- expr

173+

202− pure $ t + e

203− `mplus` pure t

204−

205−

206−factor = do symbol "("

174+factor = (symbol "(" $> expr <$ symbol ")") <|> natural

207− do e <- expr

175+

208− symbol ")"

209− pure e

210− `mplus` natural

211−

212−term = do f <- factor

176+term = do f <- factor

213− do symbol "*"

177+ fmap (f*) (symbol "*" $> term) <|> pure f

214− t <- term

178+

215− pure (f * t)

216− `mplus` pure f

217−

218−

219−

220−eval : String -> Maybe Int

179+eval : String -> Maybe Int

221−eval xs = case (parse expr xs) of

180+eval xs = case (parse expr xs) of

222− Right (n,rest) => if rest == "" then Just n else Nothing

181+ Right (n,rest) => if rest == "" then Just n else Nothing

223− Left msg => Nothing

182+ Left msg => Nothing