Skip to content

Commit

Permalink
Revert "Do-Notation desugars to Block type"
Browse files Browse the repository at this point in the history
I'm reverting this commit because I think the extra block type will be
annoying to deal with. I'll think about an alternative approach that
avoids it, while still making it possible for the bidirectinal type
checker to infer the return type.
  • Loading branch information
VictorTaelin committed Oct 18, 2024
1 parent 1b752d9 commit 6198eaa
Showing 1 changed file with 74 additions and 19 deletions.
93 changes: 74 additions & 19 deletions src/Kind/Parse.hs
Original file line number Diff line number Diff line change
Expand Up @@ -410,36 +410,91 @@ expandUses uses name =
(short, long):_ -> long ++ drop (length short) name
[] -> name

-- Syntax Sugars
-- -------------

-- TODO: implement a parser for Kind's do-notation:
-- do Name { // this starts a do-block
-- ask x = exp0 // this is parsed as a monadic binder
-- ask exp1 // this is parsed as a monadic sequencer
-- ret-val // this is the monadic return
-- } // this ends a do block

-- The do-notation above is desugared to:
-- (Name/Monad/bind _ _ exp0 λx
-- (Name/Monad/bind _ _ exp1 λ_
-- ret-val))
-- Note this is just a series of applications:
-- (App (App (App (App (Ref "Name/Monad/bind") (Met 0 [])) (Met 0 [])) exp0) (Lam "x" λx ...

-- To make the code cleaner, create a DoBlock type.
-- Then, create a 'parseDoSugar' parser, that returns a DoBlock.
-- Then, create a 'desugarDo' function, that converts a DoBlock into a Term.
-- Finally, create a 'parseDo' parser, that parses a do-block as a Term.

-- actually, let's add another option:
-- - optionally, the user can end the block in 'wrap value'
-- - if they do, the end value will be `((Name/Monad/bind _) value)` instead of just `value`
-- rewrite the commented out code above to add this feature. keep all else the same. do it now:

-- this 'isDoWrap' logic is ugly. clean up the code above to avoid pattern-matching on (App (App ...)) like that. implement the wrap functionality in a more elegant fashion. rewrite the code now.

-- TODO: rewrite the code above to apply the expand-uses functionality to the generated refs. also, append just "bind" and "pure" (instad of "/Monad/bind" etc.)

-- Do-Notation:
-- ------------

-- FIXME: will only work on Base/ monads for now
parseDo :: Parser Term
parseDo = withSrc $ do
data DoBlck = DoBlck String [DoStmt] Bool Term -- bool used for wrap
data DoStmt = DoBind String Term | DoSeq Term

parseDoSugar :: Parser DoBlck
parseDoSugar = do
string "do "
name <- parseName
char '{'
parseTrivia
stmts <- parseDoStmts
stmts <- P.many (P.try parseDoStmt)
(wrap, ret) <- parseDoReturn
char '}'
return stmts
return $ DoBlck name stmts wrap ret

parseDoStmts :: Parser Term
parseDoStmts = P.choice [ parseDoAsk , parseDoRet , parseTerm ]
parseDoStmt :: Parser DoStmt
parseDoStmt = P.try parseDoBind <|> parseDoSeq

parseDoAsk :: Parser Term
parseDoAsk = do
P.try $ string "ask "
nam <- parseName
parseDoBind :: Parser DoStmt
parseDoBind = do
string "ask "
name <- parseName
char '='
val <- parseTerm
bod <- parseDoStmts
return $ Con "Ask" [(Nothing, Met 0 []), (Nothing, val), (Nothing, Lam nam (\x -> bod))]
exp <- parseTerm
return $ DoBind name exp

parseDoSeq :: Parser DoStmt
parseDoSeq = do
string "ask "
exp <- parseTerm
return $ DoSeq exp

parseDoReturn :: Parser (Bool, Term)
parseDoReturn = do
wrap <- P.optionMaybe (P.try (string "ret "))
term <- parseTerm
return (maybe False (const True) wrap, term)

desugarDo :: DoBlck -> Parser Term
desugarDo (DoBlck name stmts wrap ret) = do
(_, uses) <- P.getState
let exName = expandUses uses name
let mkBind = \ x exp acc -> App (App (App (App (Ref (exName ++ "bind")) (Met 0 [])) (Met 0 [])) exp) (Lam x (\_ -> acc))
let mkWrap = \ ret -> App (App (Ref (exName ++ "pure")) (Met 0 [])) ret
return $ foldr (\stmt acc ->
case stmt of
DoBind x exp -> mkBind x exp acc
DoSeq exp -> mkBind "_" exp acc
) (if wrap then mkWrap ret else ret) stmts

parseDoRet :: Parser Term
parseDoRet = do
P.try $ string "ret "
val <- parseTerm
return $ Con "Ret" [(Nothing, val)]
parseDo :: Parser Term
parseDo = parseDoSugar >>= desugarDo

-- Match
-- -----
Expand Down

0 comments on commit 6198eaa

Please sign in to comment.