edwinb/Idris2-boot
1
1
Fork 0
mirror of https://github.com/edwinb/Idris2-boot.git synced 2025-01-06 21:28:25 +03:00
Code Issues Projects Releases Wiki Activity

Lift ! out of 'let' in do blocks

Browse Source
This commit is contained in:
Edwin Brady 2020-02-01 13:54:10 +00:00
parent cf27bbed66
commit 8d8d281fb4
2 changed files with 7 additions and 3 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

7
src/Idris/Desugar.idr
View File

@ -388,10 +388,13 @@ mutual
(PatClause fc bpat rest' (PatClause fc bpat rest'
:: alts'))) :: alts')))
expandDo side ps topfc (DoLet fc n rig ty tm :: rest) expandDo side ps topfc (DoLet fc n rig ty tm :: rest)
= do tm' <- desugar side ps tm = do b <- newRef Bang initBangs
tm' <- desugarB side ps tm
ty' <- desugar side ps ty ty' <- desugar side ps ty
rest' <- expandDo side ps topfc rest rest' <- expandDo side ps topfc rest
pure $ ILet fc rig n ty' tm' rest' let bind = ILet fc rig n ty' tm' rest'
bd <- get Bang
pure $ bindBangs (bangNames bd) bind
expandDo side ps topfc (DoLetPat fc pat ty tm alts :: rest) expandDo side ps topfc (DoLetPat fc pat ty tm alts :: rest)
= do pat' <- desugar LHS ps pat = do pat' <- desugar LHS ps pat
ty' <- desugar side ps ty ty' <- desugar side ps ty

3
src/Idris/Parser.idr
View File

@ -159,7 +159,8 @@ mutual
arg <- implicitArg fname indents arg <- implicitArg fname indents
pure (ImpArg (fst arg) (snd arg)) pure (ImpArg (fst arg) (snd arg))
<|> if withOK q <|> if withOK q
then do symbol "|" then do continue indents
symbol "|"
arg <- expr (record { withOK = False} q) fname indents arg <- expr (record { withOK = False} q) fname indents
pure (WithArg arg) pure (WithArg arg)
else fail "| not allowed here" else fail "| not allowed here"