/
Parsing.hs
179 lines (142 loc) · 4.33 KB
/
Parsing.hs
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
{-# language RankNTypes #-}
module Parsing where
import Control.Applicative
import Control.Monad.Fix
import Data.Functor
import Text.Megaparsec
import qualified Text.Megaparsec.Lexer as L
import Text.Megaparsec.String
import Text.Printf
import Term.RawTerm
import Term
type Parser1 a = Parser a -> Parser a
type Parser2 a = Parser a -> Parser1 a
data Associativity = LeftAssociative | RightAssociative | NonAssociative
data ModularParser a
= SelfNextParser (Parser2 a)
| BinaryOpParser Associativity String (a -> a -> a)
| AtomParser (Parser a)
binOpL, binOpR, binOpN :: String -> (a -> a -> a) -> ModularParser a
binOpL = BinaryOpParser LeftAssociative
binOpR = BinaryOpParser RightAssociative
binOpN = BinaryOpParser NonAssociative
parser :: [[ModularParser RawTerm]]
parser =
-- low precedence
[ [SelfNextParser letP, SelfNextParser lamP]
, [binOpN "∷" (Annot ())]
, [SelfNextParser namedPiP, binOpR "→" (Pi () (Binder Nothing))]
, [binOpL "" (App ())]
, [AtomParser holeP, AtomParser typeP, AtomParser varP]
]
-- high precedence
unModularP :: ModularParser a -> Parser2 a
unModularP (SelfNextParser p) = p
unModularP (BinaryOpParser LeftAssociative s p) = binOpLP s p
unModularP (BinaryOpParser RightAssociative s p) = binOpRP s p
unModularP (BinaryOpParser NonAssociative s p) = binOpNP s p
unModularP (AtomParser p) = \ _selfP _nextP -> p
choiceOrNextP :: [ModularParser a] -> Parser1 a
choiceOrNextP ps nextP =
fix $ \ selfP -> choice $ map (\ p -> unModularP p selfP nextP) ps ++ [nextP]
foldP :: [[ModularParser a]] -> Parser a
foldP ps = fix $ \ self -> foldr ($) (parens self) (map choiceOrNextP ps)
termP :: Parser RawTerm
termP = foldP parser
-- Binary operator parsers
binOpLP :: String -> (a -> a -> a) -> Parser2 a
binOpLP s k _selfP nextP = chainl1 nextP (symbol s *> return k)
binOpRP :: String -> (a -> a -> a) -> Parser2 a
binOpRP s k selfP nextP = do
l <- try $ do
l <- nextP
symbol s
return l
r <- selfP
return $ k l r
binOpNP :: String -> (a -> a -> a) -> Parser2 a
binOpNP s k _selfP nextP = binOpRP s k nextP nextP
-- Individual parsers (alphabetically)
binderP :: Parser Binder
binderP = Binder <$> ((Nothing <$ symbol "_") <|> (Just <$> identifier))
holeP :: Parser RawTerm
holeP = Hole () <$ symbol "_"
lamP :: Parser2 RawTerm
lamP selfP _nextP = do
try $ do
symbol "λ"
bs <- some binderP
symbol "."
t <- selfP
return $ lams bs t
where
lams :: [Binder] -> RawTerm -> RawTerm
lams [] t = t
lams (b : bs) t = Lam () b $ lams bs t
letP :: Parser2 RawTerm
letP selfP _nextP = do
try $ do
rword "let"
b <- binderP
symbol "="
t1 <- termP
rword "in"
t2 <- selfP
return $ Let () b t1 t2
namedPiP :: Parser2 RawTerm
namedPiP selfP _nextP = do
(x, τ1) <- try $ do
symbol "("
x <- identifier
symbol ":"
τ1 <- termP
symbol ")"
symbol "→"
return (x, τ1)
τ2 <- selfP
return $ Pi () (Binder (Just x)) τ1 τ2
typeP :: Parser RawTerm
typeP = Type () <$ rword "Type"
varP :: Parser RawTerm
varP = Var () <$> identifier
-- Running parsers
langP :: Parser RawTerm
langP = termP <* eof
runParserTerm :: String -> Either (ParseError Char Dec) RawTerm
runParserTerm = runParser langP "runParserTerm"
parseMaybeTerm :: String -> Maybe RawTerm
parseMaybeTerm = parseMaybe langP
-- Utilities
sc :: Parser ()
sc = L.space (void spaceChar) lineCmnt blockCmnt
where
lineCmnt = empty -- L.skipLineComment "//"
blockCmnt = L.skipBlockComment "(*" "*)"
lexeme :: Parser a -> Parser a
lexeme = L.lexeme sc
symbol :: String -> Parser ()
symbol = void . L.symbol sc
parens :: Parser a -> Parser a
parens = between (symbol "(") (symbol ")")
rword :: String -> Parser ()
rword w = string w *> notFollowedBy alphaNumChar *> sc
reservedWords :: [String] -- list of reserved words
reservedWords =
[ "let"
, "in"
, "λ"
]
identifier :: Parser String
identifier = (lexeme . try) (p >>= check)
where
p = (:) <$> letterChar <*> many alphaNumChar
check x =
if x `elem` reservedWords
then fail $ printf "keyword %s cannot be an identifier" (show x)
else return x
chainl1 :: (Alternative m, Monad m) => m a -> m (a -> a -> a) -> m a
chainl1 p op = do
x <- p
rest x
where
rest x = do { f <- op ; y <- p ; rest (f x y) } <|> return x