@@ -0,0 +1,184 @@
1+module Parsing
2+
3+import prelude
4+import builtins
5+
6+infixr 5 |||
7+
8+{-
9+The monad of parsers
10+--------------------
11+-}
12+
13+data Parser a = P (String -> Either String (a,String))
14+
15+parse : Parser a -> String ->Either String (a,String)
16+parse (P p) inp = p inp
17+
18+instance Monad Parser where
19+ return v = P (\inp => Right (v,inp))
20+ p >>= f = P (\inp => case parse p inp of
21+ Left err => Left err
22+ Right (v,rest) => parse (f v) rest)
23+
24+
25+instance MonadPlus Parser where
26+ mzero = P (\inp => Left "Parse Error")
27+ mplus p q = P (\inp => case parse p inp of
28+ Left msg => parse q inp
29+ Right (v,out) => Right(v,out))
30+
31+
32+
33+{-
34+Basic parsers
35+-------------
36+-}
37+
38+failure : String -> Parser a
39+failure msg = P (\inp => Left msg)
40+
41+item : Parser Char
42+item = P (\inp => case unpack inp of
43+ [] => Left "Error! Parsing empty list."
44+ (x::xs) => Right (x, pack xs))
45+
46+
47+{-
48+Choice
49+--------
50+---}
51+
52+(|||) : Parser a -> Parser a -> Parser a
53+p ||| q = p `mplus` q
54+
55+
56+--{-
57+--Derived primitives
58+---}
59+
60+sat : (Char -> Bool) -> Parser Char
61+sat p = item >>= (\x => if p x then return x else failure "failed")
62+
63+oneof : List Char -> Parser Char
64+oneof xs = sat (\x => elem x xs)
65+
66+digit : Parser Char
67+digit = sat isDigit
68+
69+lower : Parser Char
70+lower = sat isLower
71+
72+upper : Parser Char
73+upper = sat isUpper
74+
75+letter : Parser Char
76+letter = sat isAlpha
77+
78+alphanum : Parser Char
79+alphanum = sat isAlphaNum
80+
81+char : Char -> Parser Char
82+char x = sat (== x)
83+
84+string : String -> Parser String
85+helper : List Char -> Parser (List Char)
86+string s = do result <- helper (unpack s)
87+ return (pack result)
88+
89+helper [] = return []
90+helper (x::xs) = do char x
91+ string (cast xs)
92+ return (x :: xs)
93+
94+many1 : Parser a -> Parser (List a)
95+many : Parser a -> Parser (List a)
96+many1 p = do v <- p
97+ vs <- many p
98+ return (v::vs)
99+
100+
101+many p = many1 p `mplus` return []
102+
103+
104+
105+ident : Parser String
106+ident = do x <- letter
107+ xs <- many1 alphanum
108+ return (pack(x::xs))
109+
110+
111+nat : Parser Int
112+nat = do xs <- many digit
113+ return (cast (cast xs))
114+
115+
116+int : Parser Int
117+int = do char '-'
118+ n <- nat
119+ return (-n)
120+ `mplus` nat
121+
122+space : Parser ()
123+space = do many (sat isSpace)
124+ return ()
125+--{-
126+--Ignoring spacing
127+---}
128+
129+token : Parser a -> Parser a
130+token p = do space
131+ v <- p
132+ space
133+ return v
134+
135+identifier : Parser String
136+identifier = token ident
137+
138+natural : Parser Int
139+natural = token nat
140+
141+integer : Parser Int
142+integer = token int
143+
144+symbol : String -> Parser String
145+symbol xs = token (string xs)
146+
147+--apply : Parser a -> String -> List (a,String)
148+--apply p = parse (space >>= (\_ => p))
149+
150+--{-
151+-- Expressions
152+---}
153+
154+factor : Parser Int
155+term : Parser Int
156+expr : Parser Int
157+expr = do t <- term
158+ do symbol "+"
159+ e <- expr
160+ Right (t+e)
161+ ||| Right t
162+
163+
164+factor = do symbol "("
165+ e <- expr
166+ symbol ")"
167+ return e
168+ ||| natural
169+
170+term = do f <- factor
171+ symbol "*"
172+ t <- term
173+ return (f * t)
174+ ||| return f
175+
176+
177+
178+eval : String -> Maybe Int
179+eval xs = case (parse expr xs) of
180+ Right (n,rest) => if rest == "" then Just n else Nothing
181+ Left msg => Nothing
182+
183+
184+