09bb6fc · 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+--------------------------------------------------------------------------------

19−The monad of parsers

18+-- The monad of parsers

20−--------------------

19+--------------------------------------------------------------------------------

21−-}

22

20

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

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

24

22

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

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

26−parse (P p) inp = p inp

24+parse (P p) inp = p inp

27

25

28−instance Functor Parser where

26+instance Functor Parser where

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

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

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

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

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

33− (Left err) => Left err

28+ Left err => Left err

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

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

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

36−

37

30

38−instance Applicative Parser where

31+instance Applicative Parser where

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

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

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

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

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

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

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

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

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

44

36

45instance Monad Parser where

37instance Monad Parser where

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

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

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

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

49− (Left err) => Left err

39+ Left err => Left err

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

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

51−

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

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

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

55− Left msg => parse q inp

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

57

41

42+instance Alternative Parser where

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

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

45+ Left msg => parse q inp

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

58

47

59−{-

60−Basic parsers

61−-------------

62−-}

63

48

64−failure : String -> Parser a

49+--------------------------------------------------------------------------------

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

50+-- Basic parsers

51+--------------------------------------------------------------------------------

66

52

67−item : Parser Char

53+failure : String -> Parser a

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

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

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

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

71−

72

55

73−{-

56+item : Parser Char

74−Choice

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

75−--------

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

76−---}

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

77

60

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

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

80

61

62+--------------------------------------------------------------------------------

63+-- Derived primitives

64+--------------------------------------------------------------------------------

81

65

82−--{-

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

83−--Derived primitives

67+sat p = do x <- item

84−---}

68+ guard (p x)

69+ pure x

85

70

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

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

88−

89−oneof : List Char -> Parser Char

71+oneof : List Char -> Parser Char

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

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

91

73

92−digit : Parser Char

74+digit : Parser Char

93−digit = sat isDigit

75+digit = sat isDigit

94

76

95−lower : Parser Char

77+lower : Parser Char

96−lower = sat isLower

78+lower = sat isLower

97

79

98−upper : Parser Char

80+upper : Parser Char

99−upper = sat isUpper

81+upper = sat isUpper

100

82

101−letter : Parser Char

83+letter : Parser Char

102−letter = sat isAlpha

84+letter = sat isAlpha

103

85

104−alphanum : Parser Char

86+alphanum : Parser Char

105−alphanum = sat isAlphaNum

87+alphanum = sat isAlphaNum

106

88

107−char : Char -> Parser Char

89+char : Char -> Parser Char

108−char x = sat (== x)

90+char x = sat (== x)

109

91

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

111−string : String -> Parser String

92+string : String -> Parser String

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

93+string s = fmap pack (traverse char (unpack s))

113− pure (pack result)

114−

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

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

117− string (cast xs)

118− pure (x :: xs)

119

94

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

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

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

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

122−many1 p = do v <- p

123− vs <- many p

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

125

97

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

99+

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

126

101

127bool : Parser Bool

102bool : Parser Bool

128−bool = parseTrue ||| parseFalse

103+bool = parseTrue <|> parseFalse

129 where parseTrue : Parser Bool

104 where parseTrue : Parser Bool

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

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

131 string "rue"

106 string "rue"

134 string "alse"

109 string "alse"

135 pure False

110 pure False

136

111

112+ident : Parser String

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

137

114

115+nat : Parser Int

116+nat = do xs <- many digit

117+ pure (cast (cast xs))

138

118

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

119+int : Parser Int

150−nat = do xs <- many digit

151− pure (cast (cast xs))

152−

153−

154−int : Parser Int

155−int = neg ||| nat

120+int = neg <|> nat

156 where neg : Parser Int

121 where neg : Parser Int

157 neg = do char '-'

122 neg = do char '-'

158 n <- nat

123 n <- nat

159 pure (-n)

124 pure (-n)

160

125

161−space : Parser ()

126+space : Parser ()

162−space = do many (sat isSpace)

127+space = do many (sat isSpace)

163− pure ()

128+ pure ()

164−--{-

129+

165−--Ignoring spacing

166−---}

167

130

168−token : Parser a -> Parser a

131+--------------------------------------------------------------------------------

169−token p = do space

132+-- Ignoring spacing

170− v <- p

133+--------------------------------------------------------------------------------

171− space

172− pure v

173

134

174−identifier : Parser String

135+token : Parser a -> Parser a

175−identifier = token ident

136+token p = space $> p <$ space

176

137

177−natural : Parser Int

138+identifier : Parser String

178−natural = token nat

139+identifier = token ident

179

140

180−integer : Parser Int

141+natural : Parser Int

181−integer = token int

142+natural = token nat

182

143

144+integer : Parser Int

145+integer = token int

146+

183−symbol : String -> Parser String

147+symbol : String -> Parser String

184−symbol xs = token (string xs)

148+symbol xs = token (string xs)

185

149

186strToken : Parser String

150strToken : Parser String

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

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

188

152

189−--apply : Parser a -> String -> List (a,String)

190−--apply p = parse (space >>= (\_ => p))

191

153

192−--{-

154+--------------------------------------------------------------------------------

193-- Expressions

155-- Expressions

194−---}

156+--------------------------------------------------------------------------------

195−

157+

196−factor : Parser Int

158+expr : Parser Int

197−term : Parser Int

159+factor : Parser Int

198−expr : Parser Int

160+term : Parser Int

161+

199−expr = do t <- term

162+expr = do t <- term

200− do symbol "+"

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

201− e <- expr

164+

202− pure $ t + e

203− `mplus` pure t

204−

205−

206−factor = do symbol "("

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

207− do e <- expr

166+

208− symbol ")"

209− pure e

210− `mplus` natural

211−

212−term = do f <- factor

167+term = do f <- factor

213− do symbol "*"

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

214− t <- term

169+

215− pure (f * t)

216− `mplus` pure f

217−

218−

219−

220−eval : String -> Maybe Int

170+eval : String -> Maybe Int

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

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

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

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

223− Left msg => Nothing

173+ Left msg => Nothing