diff options
author | Csaba Hruska <csaba.hruska@gmail.com> | 2017-06-13 23:54:58 +0100 |
---|---|---|
committer | Csaba Hruska <csaba.hruska@gmail.com> | 2017-06-13 23:54:58 +0100 |
commit | 30792e3d67a11787a691493683c703a4767ce96d (patch) | |
tree | 5a0542984e84268f9628269d8279715b7b45b731 | |
parent | 07bd8babb6b9991884ac2d1ca50436ce861b06c8 (diff) |
add type signatures
-rw-r--r-- | refactor.plan | 2 | ||||
-rw-r--r-- | src/LambdaCube/Compiler/Parser.hs | 107 |
2 files changed, 98 insertions, 11 deletions
diff --git a/refactor.plan b/refactor.plan index 25b6fbfc..9d08dc97 100644 --- a/refactor.plan +++ b/refactor.plan | |||
@@ -10,7 +10,7 @@ typesig - import LambdaCube.Compiler.Lexer | |||
10 | typesig - import LambdaCube.Compiler.DesugaredSource | 10 | typesig - import LambdaCube.Compiler.DesugaredSource |
11 | typesig - import LambdaCube.Compiler.Patterns | 11 | typesig - import LambdaCube.Compiler.Patterns |
12 | typesig - import LambdaCube.Compiler.Statements | 12 | typesig - import LambdaCube.Compiler.Statements |
13 | import LambdaCube.Compiler.Parser | 13 | typesig - import LambdaCube.Compiler.Parser |
14 | 14 | ||
15 | stage 2: | 15 | stage 2: |
16 | import LambdaCube.Compiler.Core | 16 | import LambdaCube.Compiler.Core |
diff --git a/src/LambdaCube/Compiler/Parser.hs b/src/LambdaCube/Compiler/Parser.hs index 69f1b7a4..1ed8ac8c 100644 --- a/src/LambdaCube/Compiler/Parser.hs +++ b/src/LambdaCube/Compiler/Parser.hs | |||
@@ -85,19 +85,24 @@ trackSI p = do | |||
85 | addFixity :: BodyParser SIName -> BodyParser SIName | 85 | addFixity :: BodyParser SIName -> BodyParser SIName |
86 | addFixity p = f <$> asks (fixityMap . desugarInfo) <*> p | 86 | addFixity p = f <$> asks (fixityMap . desugarInfo) <*> p |
87 | where | 87 | where |
88 | f :: Map.Map SName Fixity -> SIName -> SIName | ||
88 | f fm sn@(SIName_ si _ n) = SIName_ si (Just $ defaultFixity $ Map.lookup n fm) n | 89 | f fm sn@(SIName_ si _ n) = SIName_ si (Just $ defaultFixity $ Map.lookup n fm) n |
89 | 90 | ||
90 | addFixity' :: BodyParser SIName -> BodyParser SIName | 91 | addFixity' :: BodyParser SIName -> BodyParser SIName |
91 | addFixity' p = f <$> asks (fixityMap . desugarInfo) <*> p | 92 | addFixity' p = f <$> asks (fixityMap . desugarInfo) <*> p |
92 | where | 93 | where |
94 | f :: Map.Map SName Fixity -> SIName -> SIName | ||
93 | f fm sn@(SIName_ si _ n) = SIName_ si (Map.lookup n fm) n | 95 | f fm sn@(SIName_ si _ n) = SIName_ si (Map.lookup n fm) n |
94 | 96 | ||
97 | addConsInfo :: BodyParser SIName -> BodyParser (SIName, ConsInfo) | ||
95 | addConsInfo p = join $ f <$> asks (consMap . desugarInfo) <*> p | 98 | addConsInfo p = join $ f <$> asks (consMap . desugarInfo) <*> p |
96 | where | 99 | where |
100 | f :: Map.Map String ConsInfo -> SIName -> BodyParser (SIName, ConsInfo) | ||
97 | f adts s = do | 101 | f adts s = do |
98 | tell [Left $ either (Just . UndefinedConstructor) (const Nothing) x] | 102 | tell [Left $ either (Just . UndefinedConstructor) (const Nothing) x] |
99 | return $ either (const $ error "impossible @ Parser 826") id x | 103 | return $ either (const $ error "impossible @ Parser 826") id x |
100 | where | 104 | where |
105 | x :: Either SIName (SIName, ConsInfo) | ||
101 | x = case Map.lookup (sName s) adts of | 106 | x = case Map.lookup (sName s) adts of |
102 | Nothing -> throwError s | 107 | Nothing -> throwError s |
103 | Just i -> return (s, i) | 108 | Just i -> return (s, i) |
@@ -105,6 +110,7 @@ addConsInfo p = join $ f <$> asks (consMap . desugarInfo) <*> p | |||
105 | addForalls' :: BodyParser SExp -> BodyParser SExp | 110 | addForalls' :: BodyParser SExp -> BodyParser SExp |
106 | addForalls' p = addForalls_ mempty <*> p | 111 | addForalls' p = addForalls_ mempty <*> p |
107 | 112 | ||
113 | addForalls_ :: [SIName] -> BodyParser (SExp -> SExp) | ||
108 | addForalls_ s = addForalls . (Set.fromList (sName <$> s) <>) <$> asks (definedSet . desugarInfo) | 114 | addForalls_ s = addForalls . (Set.fromList (sName <$> s) <>) <$> asks (definedSet . desugarInfo) |
109 | 115 | ||
110 | -------------------------------------------------------------------------------- desugar info | 116 | -------------------------------------------------------------------------------- desugar info |
@@ -131,8 +137,10 @@ mkDesugarInfo ss = DesugarInfo | |||
131 | , definedSet = Set.singleton "'Type" <> foldMap defined ss | 137 | , definedSet = Set.singleton "'Type" <> foldMap defined ss |
132 | } | 138 | } |
133 | where | 139 | where |
140 | pars :: SExp' a -> Int | ||
134 | pars (UncurryS l _) = length $ filter ((== Visible) . fst) l -- todo | 141 | pars (UncurryS l _) = length $ filter ((== Visible) . fst) l -- todo |
135 | 142 | ||
143 | defined :: Stmt -> Set.Set SName | ||
136 | defined = \case | 144 | defined = \case |
137 | StLet sn _ _ -> Set.singleton $ sName sn | 145 | StLet sn _ _ -> Set.singleton $ sName sn |
138 | Data sn _ _ cs -> Set.fromList $ sName sn: map (sName . fst) cs | 146 | Data sn _ _ cs -> Set.fromList $ sName sn: map (sName . fst) cs |
@@ -140,27 +148,37 @@ mkDesugarInfo ss = DesugarInfo | |||
140 | 148 | ||
141 | -------------------------------------------------------------------------------- expression parsing | 149 | -------------------------------------------------------------------------------- expression parsing |
142 | 150 | ||
151 | hiddenTerm :: BodyParser a -> BodyParser a -> BodyParser (Visibility, a) | ||
143 | hiddenTerm p q = (,) Hidden <$ reservedOp "@" <*> typeNS p <|> (,) Visible <$> q | 152 | hiddenTerm p q = (,) Hidden <$ reservedOp "@" <*> typeNS p <|> (,) Visible <$> q |
144 | 153 | ||
154 | parseType :: Maybe SExp -> BodyParser SExp | ||
145 | parseType mb = maybe id option mb (reservedOp "::" *> typeNS (setR parseTermLam)) | 155 | parseType mb = maybe id option mb (reservedOp "::" *> typeNS (setR parseTermLam)) |
146 | 156 | ||
157 | typedIds :: DeBruijnify SIName a => (BodyParser SExp -> BodyParser a) -> [SIName] -> BodyParser [(SIName, a)] | ||
147 | typedIds f ds = (\ns t -> (,) <$> ns <*> pure t) <$> commaSep1 upperLower <*> (deBruijnify (ds :: [SIName]) <$> f (parseType Nothing)) | 158 | typedIds f ds = (\ns t -> (,) <$> ns <*> pure t) <$> commaSep1 upperLower <*> (deBruijnify (ds :: [SIName]) <$> f (parseType Nothing)) |
148 | 159 | ||
160 | telescope :: Maybe SExp -> BodyParser ([SIName], [(Visibility, SExp)]) | ||
149 | telescope mb = fmap mkTelescope $ many $ hiddenTerm | 161 | telescope mb = fmap mkTelescope $ many $ hiddenTerm |
150 | (typedId <|> maybe empty (tvar . pure) mb) | 162 | (typedId <|> maybe empty (tvar . pure) mb) |
151 | (try_ "::" typedId <|> maybe ((,) (SIName mempty "") <$> typeNS (setR parseTermAtom)) (tvar . pure) mb) | 163 | (try_ "::" typedId <|> maybe ((,) (SIName mempty "") <$> typeNS (setR parseTermAtom)) (tvar . pure) mb) |
152 | where | 164 | where |
165 | tvar :: BodyParser SExp -> BodyParser (SIName, SExp) | ||
153 | tvar x = (,) <$> patVar <*> x | 166 | tvar x = (,) <$> patVar <*> x |
167 | |||
168 | typedId :: BodyParser (SIName, SExp) | ||
154 | typedId = parens $ tvar $ parseType mb | 169 | typedId = parens $ tvar $ parseType mb |
155 | 170 | ||
171 | mkTelescope :: [(Visibility,(SIName,SExp))] -> ([SIName],[(Visibility,SExp)]) | ||
156 | mkTelescope (unzip -> (vs, ns)) = second (zip vs) $ mkTelescope' $ first (:[]) <$> ns | 172 | mkTelescope (unzip -> (vs, ns)) = second (zip vs) $ mkTelescope' $ first (:[]) <$> ns |
157 | 173 | ||
174 | mkTelescope' :: DeBruijnify SIName a => [([SIName],a)] -> ([SIName],[a]) | ||
158 | mkTelescope' = go [] | 175 | mkTelescope' = go [] |
159 | where | 176 | where |
177 | go :: DeBruijnify SIName a => [SIName] -> [([SIName],a)] -> ([SIName],[a]) | ||
160 | go ns [] = (ns, []) | 178 | go ns [] = (ns, []) |
161 | go ns ((n, e): ts) = second (deBruijnify ns e:) $ go (n ++ ns) ts | 179 | go ns ((n, e): ts) = second (deBruijnify ns e:) $ go (n ++ ns) ts |
162 | 180 | ||
163 | --parseTerm... :: BodyParser SExp | 181 | parseTermLam :: BodyParser SExp |
164 | parseTermLam = | 182 | parseTermLam = |
165 | do level parseTermAnn $ \t -> | 183 | do level parseTermAnn $ \t -> |
166 | mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> setR parseTermLam | 184 | mkPi <$> (Visible <$ reservedOp "->" <|> Hidden <$ reservedOp "=>") <*> pure t <*> setR parseTermLam |
@@ -179,75 +197,100 @@ parseTermLam = | |||
179 | (fe, p) <- longPattern | 197 | (fe, p) <- longPattern |
180 | (,) p . deBruijnify fe <$> parseRHS "->" | 198 | (,) p . deBruijnify fe <$> parseRHS "->" |
181 | where | 199 | where |
200 | mkIf :: SExp -> SExp -> SExp -> SExp | ||
182 | mkIf b t f = SBuiltin FprimIfThenElse `SAppV` b `SAppV` t `SAppV` f | 201 | mkIf b t f = SBuiltin FprimIfThenElse `SAppV` b `SAppV` t `SAppV` f |
183 | 202 | ||
203 | mkPi :: Visibility -> SExp -> SExp -> SExp | ||
184 | mkPi Hidden xs b = foldr (\a b -> SPi Hidden a $ up1 b) b $ map SCW $ getTTuple xs | 204 | mkPi Hidden xs b = foldr (\a b -> SPi Hidden a $ up1 b) b $ map SCW $ getTTuple xs |
185 | mkPi Visible a b = SPi Visible a $ up1 b | 205 | mkPi Visible a b = SPi Visible a $ up1 b |
186 | 206 | ||
207 | parseTermAnn :: BodyParser SExp | ||
187 | parseTermAnn = level parseTermOp $ \t -> SAnn t <$> parseType Nothing | 208 | parseTermAnn = level parseTermOp $ \t -> SAnn t <$> parseType Nothing |
188 | 209 | ||
210 | parseTermOp :: BodyParser SExp | ||
189 | parseTermOp = (notOp False <|> notExp) >>= calculatePrecs | 211 | parseTermOp = (notOp False <|> notExp) >>= calculatePrecs |
190 | where | 212 | where |
213 | notExp :: BodyParser [Either SIName SExp] | ||
191 | notExp = (++) <$> ope <*> notOp True | 214 | notExp = (++) <$> ope <*> notOp True |
215 | |||
216 | notOp :: Bool -> BodyParser [Either SIName SExp] | ||
192 | notOp x = (++) <$> try_ "expression" ((++) <$> ex parseTermApp <*> option [] ope) <*> notOp True | 217 | notOp x = (++) <$> try_ "expression" ((++) <$> ex parseTermApp <*> option [] ope) <*> notOp True |
193 | <|> if x then option [] (try_ "lambda" $ ex parseTermLam) else mzero | 218 | <|> if x then option [] (try_ "lambda" $ ex parseTermLam) else mzero |
219 | |||
220 | ope :: BodyParser [Either SIName SExp] | ||
194 | ope = pure . Left <$> addFixity (rhsOperator <|> appRange (flip SIName "'EqCTt" <$ reservedOp "~")) | 221 | ope = pure . Left <$> addFixity (rhsOperator <|> appRange (flip SIName "'EqCTt" <$ reservedOp "~")) |
222 | |||
223 | ex :: BodyParser SExp -> BodyParser [Either SIName SExp] | ||
195 | ex pr = pure . Right <$> setR pr | 224 | ex pr = pure . Right <$> setR pr |
196 | 225 | ||
197 | calculatePrecs :: [Either SIName SExp] -> BodyParser SExp | 226 | calculatePrecs :: [Either SIName SExp] -> BodyParser SExp |
198 | calculatePrecs = go where | 227 | calculatePrecs = go where |
199 | 228 | ||
229 | go :: [Either SIName SExp] -> BodyParser SExp | ||
200 | go (Right e: xs) = waitOp False e [] xs | 230 | go (Right e: xs) = waitOp False e [] xs |
201 | go xs@(Left (sName -> "-"): _) = waitOp False (mkLit $ LInt 0) [] xs | 231 | go xs@(Left (sName -> "-"): _) = waitOp False (mkLit $ LInt 0) [] xs |
202 | go (Left op: xs) = Section . SLamV <$> waitExp True (sVar "leftSection" 0) [] op xs | 232 | go (Left op: xs) = Section . SLamV <$> waitExp True (sVar "leftSection" 0) [] op xs |
203 | go _ = error "impossible @ Parser 479" | 233 | go _ = error "impossible @ Parser 479" |
204 | 234 | ||
235 | waitExp :: Bool -> SExp -> [(SIName, SExp)] -> SIName -> [Either SIName SExp] -> BodyParser SExp | ||
205 | waitExp lsec e acc op (Right t: xs) = waitOp lsec e ((op, if lsec then up 1 t else t): acc) xs | 236 | waitExp lsec e acc op (Right t: xs) = waitOp lsec e ((op, if lsec then up 1 t else t): acc) xs |
206 | waitExp lsec e acc op [] | lsec = fail "two-sided section is not allowed" | 237 | waitExp lsec e acc op [] | lsec = fail "two-sided section is not allowed" |
207 | | otherwise = fmap (Section . SLamV) . calcPrec' e $ (op, sVar "rightSection" 0): map (second (up 1)) acc | 238 | | otherwise = fmap (Section . SLamV) . calcPrec' e $ (op, sVar "rightSection" 0): map (second (up 1)) acc |
208 | waitExp _ _ _ _ _ = fail "two operator is not allowed next to each-other" | 239 | waitExp _ _ _ _ _ = fail "two operator is not allowed next to each-other" |
209 | 240 | ||
241 | waitOp :: Bool -> SExp -> [(SIName, SExp)] -> [Either SIName SExp] -> BodyParser SExp | ||
210 | waitOp lsec e acc (Left op: xs) = waitExp lsec e acc op xs | 242 | waitOp lsec e acc (Left op: xs) = waitExp lsec e acc op xs |
211 | waitOp lsec e acc [] = calcPrec' e acc | 243 | waitOp lsec e acc [] = calcPrec' e acc |
212 | waitOp lsec e acc _ = error "impossible @ Parser 488" | 244 | waitOp lsec e acc _ = error "impossible @ Parser 488" |
213 | 245 | ||
246 | calcPrec' :: SExp -> [(SIName, SExp)] -> BodyParser SExp | ||
214 | calcPrec' e = postponedCheck id . calcPrec (\op x y -> SGlobal op `SAppV` x `SAppV` y) (fromJust . nameFixity) e . reverse | 247 | calcPrec' e = postponedCheck id . calcPrec (\op x y -> SGlobal op `SAppV` x `SAppV` y) (fromJust . nameFixity) e . reverse |
215 | 248 | ||
249 | parseTermApp :: BodyParser SExp | ||
216 | parseTermApp = | 250 | parseTermApp = |
217 | AppsS <$> try_ "record" (SGlobal <$> upperCase <* symbol "{") | 251 | AppsS <$> try_ "record" (SGlobal <$> upperCase <* symbol "{") |
218 | <*> commaSep ((,) Visible <$ lowerCase{-TODO-} <* reservedOp "=" <*> setR parseTermLam) | 252 | <*> commaSep ((,) Visible <$ lowerCase{-TODO-} <* reservedOp "=" <*> setR parseTermLam) |
219 | <* symbol "}" | 253 | <* symbol "}" |
220 | <|> AppsS <$> setR parseTermSwiz <*> many (hiddenTerm (setR parseTermSwiz) $ setR parseTermSwiz) | 254 | <|> AppsS <$> setR parseTermSwiz <*> many (hiddenTerm (setR parseTermSwiz) $ setR parseTermSwiz) |
221 | 255 | ||
256 | parseTermSwiz :: BodyParser SExp | ||
222 | parseTermSwiz = level parseTermProj $ \t -> | 257 | parseTermSwiz = level parseTermProj $ \t -> |
223 | mkSwizzling t <$> lexeme (try_ "swizzling" $ char '%' *> count' 1 4 (satisfy (`elem` ("xyzwrgba" :: String)))) | 258 | mkSwizzling t <$> lexeme (try_ "swizzling" $ char '%' *> count' 1 4 (satisfy (`elem` ("xyzwrgba" :: String)))) |
224 | where | 259 | where |
260 | mkSwizzling :: SExp -> String -> SExp | ||
225 | mkSwizzling term = swizzcall . map (SBuiltin . sc . synonym) | 261 | mkSwizzling term = swizzcall . map (SBuiltin . sc . synonym) |
226 | where | 262 | where |
263 | swizzcall :: [SExp] -> SExp | ||
227 | swizzcall [] = error "impossible: swizzling parsing returned empty pattern" | 264 | swizzcall [] = error "impossible: swizzling parsing returned empty pattern" |
228 | swizzcall [x] = SBuiltin Fswizzscalar `SAppV` term `SAppV` x | 265 | swizzcall [x] = SBuiltin Fswizzscalar `SAppV` term `SAppV` x |
229 | swizzcall xs = SBuiltin Fswizzvector `SAppV` term `SAppV` foldl SAppV (SBuiltin $ f (length xs)) xs | 266 | swizzcall xs = SBuiltin Fswizzvector `SAppV` term `SAppV` foldl SAppV (SBuiltin $ f (length xs)) xs |
230 | 267 | ||
268 | sc :: Char -> FNameTag | ||
231 | sc 'x' = FSx | 269 | sc 'x' = FSx |
232 | sc 'y' = FSy | 270 | sc 'y' = FSy |
233 | sc 'z' = FSz | 271 | sc 'z' = FSz |
234 | sc 'w' = FSw | 272 | sc 'w' = FSw |
235 | 273 | ||
274 | f :: Int -> FNameTag | ||
236 | f 2 = FV2 | 275 | f 2 = FV2 |
237 | f 3 = FV3 | 276 | f 3 = FV3 |
238 | f 4 = FV4 | 277 | f 4 = FV4 |
239 | 278 | ||
279 | synonym :: Char -> Char | ||
240 | synonym 'r' = 'x' | 280 | synonym 'r' = 'x' |
241 | synonym 'g' = 'y' | 281 | synonym 'g' = 'y' |
242 | synonym 'b' = 'z' | 282 | synonym 'b' = 'z' |
243 | synonym 'a' = 'w' | 283 | synonym 'a' = 'w' |
244 | synonym c = c | 284 | synonym c = c |
245 | 285 | ||
286 | parseTermProj :: BodyParser SExp | ||
246 | parseTermProj = level parseTermAtom $ \t -> | 287 | parseTermProj = level parseTermAtom $ \t -> |
247 | try_ "projection" $ mkProjection t <$ char '.' <*> sepBy1 lowerCase (char '.') | 288 | try_ "projection" $ mkProjection t <$ char '.' <*> sepBy1 lowerCase (char '.') |
248 | where | 289 | where |
290 | mkProjection :: SExp -> [SIName] -> SExp | ||
249 | mkProjection = foldl $ \exp field -> SBuiltin Fproject `SAppV` litString field `SAppV` exp | 291 | mkProjection = foldl $ \exp field -> SBuiltin Fproject `SAppV` litString field `SAppV` exp |
250 | 292 | ||
293 | parseTermAtom :: BodyParser SExp | ||
251 | parseTermAtom = | 294 | parseTermAtom = |
252 | mkLit <$> try_ "literal" parseLit | 295 | mkLit <$> try_ "literal" parseLit |
253 | <|> Wildcard (Wildcard SType) <$ reserved "_" | 296 | <|> Wildcard (Wildcard SType) <$ reserved "_" |
@@ -258,6 +301,7 @@ parseTermAtom = | |||
258 | <|> char '\'' *> ppa switchNamespace | 301 | <|> char '\'' *> ppa switchNamespace |
259 | <|> ppa id | 302 | <|> ppa id |
260 | where | 303 | where |
304 | ppa :: (Namespace -> Namespace) -> BodyParser SExp | ||
261 | ppa tick = | 305 | ppa tick = |
262 | brackets ( (setR parseTermLam >>= \e -> | 306 | brackets ( (setR parseTermLam >>= \e -> |
263 | mkDotDot e <$ reservedOp ".." <*> setR parseTermLam | 307 | mkDotDot e <$ reservedOp ".." <*> setR parseTermLam |
@@ -267,6 +311,7 @@ parseTermAtom = | |||
267 | <|> parens (SGlobal <$> try_ "opname" (symbols <* lookAhead (symbol ")")) | 311 | <|> parens (SGlobal <$> try_ "opname" (symbols <* lookAhead (symbol ")")) |
268 | <|> mkTuple . tick <$> asks namespace <*> commaSep (setR parseTermLam)) | 312 | <|> mkTuple . tick <$> asks namespace <*> commaSep (setR parseTermLam)) |
269 | 313 | ||
314 | mkTuple :: Namespace -> [SExp] -> SExp | ||
270 | mkTuple _ [Section e] = e | 315 | mkTuple _ [Section e] = e |
271 | mkTuple ExpNS [Parens e] = HCons e HNil | 316 | mkTuple ExpNS [Parens e] = HCons e HNil |
272 | mkTuple TypeNS [Parens e] = HList $ BCons e BNil | 317 | mkTuple TypeNS [Parens e] = HList $ BCons e BNil |
@@ -274,15 +319,19 @@ parseTermAtom = | |||
274 | mkTuple ExpNS xs = foldr HCons HNil xs | 319 | mkTuple ExpNS xs = foldr HCons HNil xs |
275 | mkTuple TypeNS xs = HList $ foldr BCons BNil xs | 320 | mkTuple TypeNS xs = HList $ foldr BCons BNil xs |
276 | 321 | ||
322 | mkList :: Namespace -> [SExp] -> SExp | ||
277 | mkList TypeNS [x] = BList x | 323 | mkList TypeNS [x] = BList x |
278 | mkList _ xs = foldr BCons BNil xs | 324 | mkList _ xs = foldr BCons BNil xs |
279 | 325 | ||
280 | -- Creates: RecordCons @[("x", _), ("y", _), ("z", _)] (1.0, 2.0, 3.0))) | 326 | -- Creates: RecordCons @[("x", _), ("y", _), ("z", _)] (1.0, 2.0, 3.0))) |
327 | mkRecord :: [(SIName, SExp)] -> SExp | ||
281 | mkRecord (unzip -> (names, values)) | 328 | mkRecord (unzip -> (names, values)) |
282 | = SBuiltin FRecordCons `SAppH` foldr BCons BNil (mkRecItem <$> names) `SAppV` foldr HCons HNil values | 329 | = SBuiltin FRecordCons `SAppH` foldr BCons BNil (mkRecItem <$> names) `SAppV` foldr HCons HNil values |
283 | 330 | ||
331 | mkRecItem :: SIName -> SExp | ||
284 | mkRecItem l = SBuiltin FRecItem `SAppV` litString l `SAppV` Wildcard SType | 332 | mkRecItem l = SBuiltin FRecItem `SAppV` litString l `SAppV` Wildcard SType |
285 | 333 | ||
334 | mkDotDot :: SExp -> SExp -> SExp | ||
286 | mkDotDot e f = SBuiltin FfromTo `SAppV` e `SAppV` f | 335 | mkDotDot e f = SBuiltin FfromTo `SAppV` e `SAppV` f |
287 | 336 | ||
288 | generator, letdecl, boolExpression :: BodyParser (SExp -> ErrorFinder SExp) | 337 | generator, letdecl, boolExpression :: BodyParser (SExp -> ErrorFinder SExp) |
@@ -300,40 +349,54 @@ parseTermAtom = | |||
300 | boolExpression = (\pred e -> return $ SBuiltin FprimIfThenElse `SAppV` pred `SAppV` e `SAppV` BNil) <$> setR parseTermLam | 349 | boolExpression = (\pred e -> return $ SBuiltin FprimIfThenElse `SAppV` pred `SAppV` e `SAppV` BNil) <$> setR parseTermLam |
301 | 350 | ||
302 | 351 | ||
352 | level :: BodyParser SExp -> (SExp -> BodyParser SExp) -> BodyParser SExp | ||
303 | level pr f = pr >>= \t -> option t $ f t | 353 | level pr f = pr >>= \t -> option t $ f t |
304 | 354 | ||
355 | litString :: SIName -> SExp | ||
305 | litString (SIName si n) = SLit si $ LString n | 356 | litString (SIName si n) = SLit si $ LString n |
306 | 357 | ||
358 | mkLit :: Lit -> SExp | ||
307 | mkLit n@LInt{} = SBuiltin FfromInt `SAppV` sLit n | 359 | mkLit n@LInt{} = SBuiltin FfromInt `SAppV` sLit n |
308 | mkLit l = sLit l | 360 | mkLit l = sLit l |
309 | 361 | ||
310 | -------------------------------------------------------------------------------- pattern parsing | 362 | -------------------------------------------------------------------------------- pattern parsing |
311 | 363 | ||
364 | setR :: SetSourceInfo a => BodyParser a -> BodyParser a | ||
312 | setR p = appRange $ flip setSI <$> p | 365 | setR p = appRange $ flip setSI <$> p |
313 | 366 | ||
314 | --parsePat... :: BodyParser ParPat | 367 | parsePatAnn :: BodyParser ParPat |
315 | parsePatAnn = patType <$> setR parsePatOp <*> parseType (Just $ Wildcard SType) | 368 | parsePatAnn = patType <$> setR parsePatOp <*> parseType (Just $ Wildcard SType) |
316 | where | 369 | where |
370 | patType :: ParPat -> SExp -> ParPat | ||
317 | patType p (Wildcard SType) = p | 371 | patType p (Wildcard SType) = p |
318 | patType p t = PatTypeSimp p t | 372 | patType p t = PatTypeSimp p t |
319 | 373 | ||
374 | parsePatOp :: BodyParser ParPat | ||
320 | parsePatOp = join $ calculatePatPrecs <$> setR parsePatApp <*> option [] (oper >>= p) | 375 | parsePatOp = join $ calculatePatPrecs <$> setR parsePatApp <*> option [] (oper >>= p) |
321 | where | 376 | where |
377 | oper :: BodyParser (SIName, ConsInfo) | ||
322 | oper = addConsInfo $ addFixity colonSymbols | 378 | oper = addConsInfo $ addFixity colonSymbols |
379 | |||
380 | p :: (SIName,ConsInfo) -> BodyParser [((SIName, ConsInfo), ParPat)] | ||
323 | p op = do (exp, op') <- try_ "pattern" $ (,) <$> setR parsePatApp <*> oper | 381 | p op = do (exp, op') <- try_ "pattern" $ (,) <$> setR parsePatApp <*> oper |
324 | ((op, exp):) <$> p op' | 382 | ((op, exp):) <$> p op' |
325 | <|> pure . (,) op <$> setR parsePatAnn | 383 | <|> pure . (,) op <$> setR parsePatAnn |
326 | 384 | ||
385 | calculatePatPrecs :: ParPat -> [((SIName, ConsInfo), ParPat)] -> BodyParser ParPat | ||
327 | calculatePatPrecs e xs = postponedCheck fst $ calcPrec (\op x y -> PConSimp op [x, y]) (fromJust . nameFixity . fst) e xs | 386 | calculatePatPrecs e xs = postponedCheck fst $ calcPrec (\op x y -> PConSimp op [x, y]) (fromJust . nameFixity . fst) e xs |
328 | 387 | ||
388 | parsePatApp :: BodyParser ParPat | ||
329 | parsePatApp = | 389 | parsePatApp = |
330 | PConSimp <$> addConsInfo upperCase_ <*> many (setR parsePatAt) | 390 | PConSimp <$> addConsInfo upperCase_ <*> many (setR parsePatAt) |
331 | <|> parsePatAt | 391 | <|> parsePatAt |
332 | 392 | ||
393 | parsePatAt :: BodyParser ParPat | ||
333 | parsePatAt = concatParPats <$> sepBy1 (setR parsePatAtom) (noSpaceBefore $ reservedOp "@") | 394 | parsePatAt = concatParPats <$> sepBy1 (setR parsePatAtom) (noSpaceBefore $ reservedOp "@") |
334 | where | 395 | where |
396 | concatParPats :: [ParPat] -> ParPat | ||
335 | concatParPats ps = ParPat $ concat [p | ParPat p <- ps] | 397 | concatParPats ps = ParPat $ concat [p | ParPat p <- ps] |
336 | 398 | ||
399 | parsePatAtom :: BodyParser ParPat | ||
337 | parsePatAtom = | 400 | parsePatAtom = |
338 | mkLit <$> asks namespace <*> try_ "literal" parseLit | 401 | mkLit <$> asks namespace <*> try_ "literal" parseLit |
339 | <|> flip PConSimp [] <$> addConsInfo upperCase_ | 402 | <|> flip PConSimp [] <$> addConsInfo upperCase_ |
@@ -341,18 +404,21 @@ parsePatAtom = | |||
341 | <|> char '\'' *> ppa switchNamespace | 404 | <|> char '\'' *> ppa switchNamespace |
342 | <|> ppa id | 405 | <|> ppa id |
343 | where | 406 | where |
407 | mkLit :: Namespace -> Lit -> ParPat | ||
344 | mkLit TypeNS (LInt n) = iterateN (fromIntegral n) cSucc cZero -- todo: elim this alternative | 408 | mkLit TypeNS (LInt n) = iterateN (fromIntegral n) cSucc cZero -- todo: elim this alternative |
345 | mkLit _ n@LInt{} = litP (SBuiltin FfromInt `SAppV` sLit n) | 409 | mkLit _ n@LInt{} = litP (SBuiltin FfromInt `SAppV` sLit n) |
346 | mkLit _ n = litP (sLit n) | 410 | mkLit _ n = litP (sLit n) |
347 | 411 | ||
412 | ppa :: (Namespace -> Namespace) -> BodyParser ParPat | ||
348 | ppa tick = | 413 | ppa tick = |
349 | brackets (mkListPat . tick <$> asks namespace <*> patlist) | 414 | brackets (mkListPat . tick <$> asks namespace <*> patlist) |
350 | <|> parens (parseViewPat <|> mkTupPat . tick <$> asks namespace <*> patlist) | 415 | <|> parens (parseViewPat <|> mkTupPat . tick <$> asks namespace <*> patlist) |
351 | 416 | ||
417 | mkListPat :: Namespace -> [ParPat] -> ParPat | ||
352 | mkListPat TypeNS [p] = cList p | 418 | mkListPat TypeNS [p] = cList p |
353 | mkListPat ns ps = foldr cCons cNil ps | 419 | mkListPat ns ps = foldr cCons cNil ps |
354 | 420 | ||
355 | --mkTupPat :: [Pat] -> Pat | 421 | mkTupPat :: Namespace -> [ParPat] -> ParPat |
356 | mkTupPat TypeNS [PParens x] = mkTTup [x] | 422 | mkTupPat TypeNS [PParens x] = mkTTup [x] |
357 | mkTupPat ns [PParens x] = mkTup [x] | 423 | mkTupPat ns [PParens x] = mkTup [x] |
358 | mkTupPat _ [x] = PParens x | 424 | mkTupPat _ [x] = PParens x |
@@ -362,22 +428,29 @@ parsePatAtom = | |||
362 | mkTTup = cHList . mkListPat ExpNS | 428 | mkTTup = cHList . mkListPat ExpNS |
363 | mkTup ps = foldr cHCons cHNil ps | 429 | mkTup ps = foldr cHCons cHNil ps |
364 | 430 | ||
431 | parseViewPat :: BodyParser ParPat | ||
365 | parseViewPat = ViewPatSimp <$> try_ "view pattern" (setR parseTermOp <* reservedOp "->") <*> setR parsePatAnn | 432 | parseViewPat = ViewPatSimp <$> try_ "view pattern" (setR parseTermOp <* reservedOp "->") <*> setR parsePatAnn |
366 | 433 | ||
434 | mkPVar :: SIName -> ParPat | ||
367 | mkPVar (SIName si "") = PWildcard si | 435 | mkPVar (SIName si "") = PWildcard si |
368 | mkPVar s = PVarSimp s | 436 | mkPVar s = PVarSimp s |
369 | 437 | ||
438 | litP :: SExp -> ParPat | ||
370 | litP = flip ViewPatSimp cTrue . SAppV (SGlobal $ SIName_ mempty (Just $ Infix 4) "==") | 439 | litP = flip ViewPatSimp cTrue . SAppV (SGlobal $ SIName_ mempty (Just $ Infix 4) "==") |
371 | 440 | ||
441 | patlist :: BodyParser [ParPat] | ||
372 | patlist = commaSep $ setR parsePatAnn | 442 | patlist = commaSep $ setR parsePatAnn |
373 | 443 | ||
444 | longPattern :: BodyParser ([SIName], ParPat) | ||
374 | longPattern = setR parsePatAnn <&> (reverse . getPVars &&& id) | 445 | longPattern = setR parsePatAnn <&> (reverse . getPVars &&& id) |
375 | 446 | ||
447 | telescopePat :: BodyParser ([SIName], [((Visibility,SExp),ParPat)]) | ||
376 | telescopePat = do | 448 | telescopePat = do |
377 | (a, b) <- fmap (reverse . foldMap (getPVars . snd) &&& id) $ many $ uncurry f <$> hiddenTerm (setR parsePatAt) (setR parsePatAt) | 449 | (a, b) <- fmap (reverse . foldMap (getPVars . snd) &&& id) $ many $ uncurry f <$> hiddenTerm (setR parsePatAt) (setR parsePatAt) |
378 | checkPattern a | 450 | checkPattern a |
379 | return (a, b) | 451 | return (a, b) |
380 | where | 452 | where |
453 | f :: Visibility -> ParPat -> ((Visibility,SExp),ParPat) | ||
381 | f h (PParens p) = second PParens $ f h p | 454 | f h (PParens p) = second PParens $ f h p |
382 | f h (PatTypeSimp p t) = ((h, t), p) | 455 | f h (PatTypeSimp p t) = ((h, t), p) |
383 | f h p = ((h, Wildcard SType), p) | 456 | f h p = ((h, Wildcard SType), p) |
@@ -388,7 +461,7 @@ checkPattern ns = tell $ pure $ Left $ | |||
388 | [] -> Nothing | 461 | [] -> Nothing |
389 | xs -> Just $ MultiplePatternVars xs | 462 | xs -> Just $ MultiplePatternVars xs |
390 | 463 | ||
391 | --postponedCheck :: _ | 464 | postponedCheck :: (a -> SIName) -> Either (a,a) b -> BodyParser b |
392 | postponedCheck pr x = do | 465 | postponedCheck pr x = do |
393 | tell [Left $ either (\(a, b) -> Just $ OperatorMismatch (pr a) (pr b)) (const Nothing) x] | 466 | tell [Left $ either (\(a, b) -> Just $ OperatorMismatch (pr a) (pr b)) (const Nothing) x] |
394 | return $ either (const $ error "impossible @ Parser 725") id x | 467 | return $ either (const $ error "impossible @ Parser 725") id x |
@@ -404,7 +477,8 @@ parseDef = | |||
404 | (npsd, ts) <- telescope (Just SType) | 477 | (npsd, ts) <- telescope (Just SType) |
405 | t <- deBruijnify npsd <$> parseType (Just SType) | 478 | t <- deBruijnify npsd <$> parseType (Just SType) |
406 | adf <- addForalls_ npsd | 479 | adf <- addForalls_ npsd |
407 | let mkConTy mk (nps', ts') = | 480 | let mkConTy :: Bool -> ([SIName], [(Visibility, SExp)]) -> (Maybe [SIName], SExp) |
481 | mkConTy mk (nps', ts') = | ||
408 | ( if mk then Just $ reverse nps' else Nothing | 482 | ( if mk then Just $ reverse nps' else Nothing |
409 | , deBruijnify npsd $ foldr (uncurry SPi) (foldl SAppV (SGlobal x) $ SGlobal <$> reverse npsd) ts' | 483 | , deBruijnify npsd $ foldr (uncurry SPi) (foldl SAppV (SGlobal x) $ SGlobal <$> reverse npsd) ts' |
410 | ) | 484 | ) |
@@ -453,9 +527,11 @@ parseDef = | |||
453 | telescopeDataFields :: BodyParser ([SIName], [(Visibility, SExp)]) | 527 | telescopeDataFields :: BodyParser ([SIName], [(Visibility, SExp)]) |
454 | telescopeDataFields = mkTelescope <$> commaSep ((,) Visible <$> ((,) <$> lowerCase <*> parseType Nothing)) | 528 | telescopeDataFields = mkTelescope <$> commaSep ((,) Visible <$> ((,) <$> lowerCase <*> parseType Nothing)) |
455 | 529 | ||
530 | mkData :: SIName -> [(Visibility, SExp)] -> SExp -> [(SIName, (Maybe [SIName], SExp))] -> BodyParser [PreStmt] | ||
456 | mkData x ts t cs | 531 | mkData x ts t cs |
457 | = (Stmt (Data x ts t (second snd <$> cs)):) . concat <$> traverse mkProj (nub $ concat [fs | (_, (Just fs, _)) <- cs]) | 532 | = (Stmt (Data x ts t (second snd <$> cs)):) . concat <$> traverse mkProj (nub $ concat [fs | (_, (Just fs, _)) <- cs]) |
458 | where | 533 | where |
534 | mkProj :: SIName -> BodyParser [PreStmt] | ||
459 | mkProj fn = sequence | 535 | mkProj fn = sequence |
460 | [ do | 536 | [ do |
461 | cn' <- addConsInfo $ pure cn | 537 | cn' <- addConsInfo $ pure cn |
@@ -474,20 +550,25 @@ parseRHS tok = do | |||
474 | f <- option id $ mkLets <$ reserved "where" <*> parseDefs sLHS | 550 | f <- option id $ mkLets <$ reserved "where" <*> parseDefs sLHS |
475 | noGuards <$> trackSI (pure $ f rhs) | 551 | noGuards <$> trackSI (pure $ f rhs) |
476 | where | 552 | where |
553 | guard :: BodyParser ([(ParPat, SExp)], SExp) | ||
477 | guard = do | 554 | guard = do |
478 | (nps, ps) <- mkTelescope' <$> commaSep1 guardPiece <* reservedOp tok | 555 | (nps, ps) <- mkTelescope' <$> commaSep1 guardPiece <* reservedOp tok |
479 | e <- trackSI $ setR parseTermLam | 556 | e <- trackSI $ setR parseTermLam |
480 | return (ps, deBruijnify nps e) | 557 | return (ps, deBruijnify nps e) |
481 | 558 | ||
559 | guardPiece :: BodyParser ([SIName], (ParPat, SExp)) | ||
482 | guardPiece = getVars <$> option cTrue (try_ "pattern guard" $ setR parsePatOp <* reservedOp "<-") <*> setR parseTermOp | 560 | guardPiece = getVars <$> option cTrue (try_ "pattern guard" $ setR parsePatOp <* reservedOp "<-") <*> setR parseTermOp |
483 | where | 561 | where |
562 | getVars :: ParPat -> SExp -> ([SIName], (ParPat, SExp)) | ||
484 | getVars p e = (reverse $ getPVars p, (p, e)) | 563 | getVars p e = (reverse $ getPVars p, (p, e)) |
485 | 564 | ||
565 | mkGuards :: [([(ParPat, SExp)], SExp)] -> [Stmt] -> GuardTrees | ||
486 | mkGuards gs wh = mkLets_ lLet wh $ mconcat [foldr (uncurry guardNode') (noGuards e) ge | (ge, e) <- gs] | 566 | mkGuards gs wh = mkLets_ lLet wh $ mconcat [foldr (uncurry guardNode') (noGuards e) ge | (ge, e) <- gs] |
487 | 567 | ||
568 | parseDefs :: (SIName -> SExp -> SExp) -> BodyParser [Stmt] | ||
488 | parseDefs lhs = identation True parseDef >>= runCheck . compileStmt'_ lhs SRHS SRHS . concat | 569 | parseDefs lhs = identation True parseDef >>= runCheck . compileStmt'_ lhs SRHS SRHS . concat |
489 | 570 | ||
490 | --funAltDef :: BodyParser _ -> BodyParser _ -> BodyParser _ | 571 | funAltDef :: Maybe (BodyParser SIName) -> BodyParser SIName -> BodyParser PreStmt |
491 | funAltDef parseOpName parseName = do | 572 | funAltDef parseOpName parseName = do |
492 | (n, (fee, tss)) <- | 573 | (n, (fee, tss)) <- |
493 | case parseOpName of | 574 | case parseOpName of |
@@ -496,7 +577,8 @@ funAltDef parseOpName parseName = do | |||
496 | (e', a1) <- longPattern | 577 | (e', a1) <- longPattern |
497 | n <- opName | 578 | n <- opName |
498 | (e'', a2) <- longPattern <* lookAhead (reservedOp "=" <|> reservedOp "|") | 579 | (e'', a2) <- longPattern <* lookAhead (reservedOp "=" <|> reservedOp "|") |
499 | let fee = e'' <> e' | 580 | let fee :: [SIName] |
581 | fee = e'' <> e' | ||
500 | checkPattern fee | 582 | checkPattern fee |
501 | return (n, (fee, (,) (Visible, Wildcard SType) <$> [a1, deBruijnify e' a2])) | 583 | return (n, (fee, (,) (Visible, Wildcard SType) <$> [a1, deBruijnify e' a2])) |
502 | <|> do try_ "lhs" $ (,) <$> parseName <*> telescopePat <* lookAhead (reservedOp "=" <|> reservedOp "|") | 584 | <|> do try_ "lhs" $ (,) <$> parseName <*> telescopePat <* lookAhead (reservedOp "=" <|> reservedOp "|") |
@@ -543,8 +625,10 @@ parseModule = do | |||
543 | modn <- reserved "module" *> moduleName | 625 | modn <- reserved "module" *> moduleName |
544 | exps <- optional (parens $ commaSep parseExport) <* reserved "where" | 626 | exps <- optional (parens $ commaSep parseExport) <* reserved "where" |
545 | return (modn, exps) | 627 | return (modn, exps) |
546 | let mkIDef _ n i h _ = (n, f i h) | 628 | let mkIDef :: Maybe SI -> SIName -> Maybe [SIName] -> Maybe [SIName] -> Maybe SIName -> (SIName, ImportItems) |
629 | mkIDef _ n i h _ = (n, f i h) | ||
547 | where | 630 | where |
631 | f :: Maybe [SIName] -> Maybe [SIName] -> ImportItems | ||
548 | f Nothing Nothing = ImportAllBut [] | 632 | f Nothing Nothing = ImportAllBut [] |
549 | f (Just h) Nothing = ImportAllBut h | 633 | f (Just h) Nothing = ImportAllBut h |
550 | f Nothing (Just i) = ImportJust i | 634 | f Nothing (Just i) = ImportJust i |
@@ -571,13 +655,16 @@ runDefParser :: (MonadFix m, MonadError LCParseError m) => DesugarInfo -> DefPar | |||
571 | runDefParser ds_ dp = do | 655 | runDefParser ds_ dp = do |
572 | 656 | ||
573 | (defs, dns, ds) <- mfix $ \ ~(_, _, ds) -> do | 657 | (defs, dns, ds) <- mfix $ \ ~(_, _, ds) -> do |
574 | let x = dp (ds <> ds_) | 658 | let x :: Either ParseError ([Stmt], [PostponedCheck]) |
659 | x = dp (ds <> ds_) | ||
575 | (defs, dns) <- either (throwError . ParseError) return x | 660 | (defs, dns) <- either (throwError . ParseError) return x |
576 | return (defs, dns, mkDesugarInfo defs) | 661 | return (defs, dns, mkDesugarInfo defs) |
577 | 662 | ||
578 | mapM_ throwError [x | Left (Just x) <- dns] | 663 | mapM_ throwError [x | Left (Just x) <- dns] |
579 | 664 | ||
580 | let ism = Set.fromList [is | Right (Reachable is) <- dns] | 665 | let ism :: Set.Set Range |
666 | ism = Set.fromList [is | Right (Reachable is) <- dns] | ||
667 | f :: ParseCheck -> Maybe ParseWarning | ||
581 | f (TrackedCode is) | is `Set.notMember` ism = Just $ Unreachable is | 668 | f (TrackedCode is) | is `Set.notMember` ism = Just $ Unreachable is |
582 | f (Uncovered' si x) | not $ null $ filter (not . null . fst) x = Just $ Uncovered si x | 669 | f (Uncovered' si x) | not $ null $ filter (not . null . fst) x = Just $ Uncovered si x |
583 | f _ = Nothing | 670 | f _ = Nothing |