git.iko.soy/Idris-dev
on master help sign in
Fix default arguments in pattern context
ec631d7Edwin Brady
lib/io.idr+1−1
compare with master
unifiedsplit
@@ -9,7 +9,7 @@ io_bind : IO a -> (a -> IO b) -> IO b
9io_bind (prim__IO v) k = k v
9io_bind (prim__IO v) k = k v
10
10
11unsafePerformIO : IO a -> a
11unsafePerformIO : IO a -> a
12−unsafePerformIO (prim__IO x) = x
12+-- compiled as primitive
13
13
14abstract
14abstract
15io_return : a -> IO a
15io_return : a -> IO a
src/Idris/AbsSyntax.hs+8−8
@@ -1575,9 +1575,9 @@ addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm
1575addImpl' inpat env ist ptm = ai env ptm
1575addImpl' inpat env ist ptm = ai env ptm
1576 where
1576 where
1577 ai env (PRef fc f)
1577 ai env (PRef fc f)
1578− | not (f `elem` env) = handleErr $ aiFn inpat ist fc f []
1578+ | not (f `elem` env) = handleErr $ aiFn inpat inpat ist fc f []
1579 ai env (PHidden (PRef fc f))
1579 ai env (PHidden (PRef fc f))
1580− | not (f `elem` env) = handleErr $ aiFn False ist fc f []
1580+ | not (f `elem` env) = handleErr $ aiFn inpat False ist fc f []
1581 ai env (PEq fc l r) = let l' = ai env l
1581 ai env (PEq fc l r) = let l' = ai env l
1582 r' = ai env r in
1582 r' = ai env r in
1583 PEq fc l' r'
1583 PEq fc l' r'
@@ -1596,7 +1596,7 @@ addImpl' inpat env ist ptm = ai env ptm
1596 ai env (PApp fc (PRef _ f) as)
1596 ai env (PApp fc (PRef _ f) as)
1597 | not (f `elem` env)
1597 | not (f `elem` env)
1598 = let as' = map (fmap (ai env)) as in
1598 = let as' = map (fmap (ai env)) as in
1599− handleErr $ aiFn False ist fc f as'
1599+ handleErr $ aiFn inpat False ist fc f as'
1600 ai env (PApp fc f as) = let f' = ai env f
1600 ai env (PApp fc f as) = let f' = ai env f
1601 as' = map (fmap (ai env)) as in
1601 as' = map (fmap (ai env)) as in
1602 mkPApp fc 1 f' as'
1602 mkPApp fc 1 f' as'
@@ -1625,18 +1625,18 @@ addImpl' inpat env ist ptm = ai env ptm
1625-- if in a pattern, and there are no arguments, and there's no possible
1625-- if in a pattern, and there are no arguments, and there's no possible
1626-- names with zero explicit arguments, don't add implicits.
1626-- names with zero explicit arguments, don't add implicits.
1627
1627
1628−aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1628+aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm
1629−aiFn True ist fc f []
1629+aiFn inpat True ist fc f []
1630 = case lookupCtxt Nothing f (idris_implicits ist) of
1630 = case lookupCtxt Nothing f (idris_implicits ist) of
1631 [] -> Right $ PRef fc f
1631 [] -> Right $ PRef fc f
1632 alts -> if (any (all imp) alts)
1632 alts -> if (any (all imp) alts)
1633− then aiFn False ist fc f [] -- use it as a constructor
1633+ then aiFn inpat False ist fc f [] -- use it as a constructor
1634 else Right $ PRef fc f
1634 else Right $ PRef fc f
1635 where imp (PExp _ _ _) = False
1635 where imp (PExp _ _ _) = False
1636 imp _ = True
1636 imp _ = True
1637−aiFn inpat ist fc f as
1637+aiFn inpat expat ist fc f as
1638 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1638 | f `elem` primNames = Right $ PApp fc (PRef fc f) as
1639−aiFn inpat ist fc f as
1639+aiFn inpat expat ist fc f as
1640 -- This is where namespaces get resolved by adding PAlternative
1640 -- This is where namespaces get resolved by adding PAlternative
1641 = case lookupCtxtName Nothing f (idris_implicits ist) of
1641 = case lookupCtxtName Nothing f (idris_implicits ist) of
1642 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
1642 [(f',ns)] -> Right $ mkPApp fc (length ns) (PRef fc f') (insertImpl ns as)
src/Idris/Compiler.hs+3−1
@@ -21,7 +21,7 @@ import Paths_idris
21import Epic.Epic hiding (Term, Type, Name, fn, compile)
21import Epic.Epic hiding (Term, Type, Name, fn, compile)
22import qualified Epic.Epic as E
22import qualified Epic.Epic as E
23
23
24−primDefs = [UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]
24+primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]
25
25
26compile :: FilePath -> Term -> Idris ()
26compile :: FilePath -> Term -> Idris ()
27compile f tm
27compile f tm
@@ -105,6 +105,8 @@ instance ToEpic (TT Name) where
105 = doForeign False args
105 = doForeign False args
106 | (P _ (UN "mkLazyForeign") _, args) <- unApply tm
106 | (P _ (UN "mkLazyForeign") _, args) <- unApply tm
107 = doForeign True args
107 = doForeign True args
108+ | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm
109+ = epic' env arg
108 | (P _ (UN "lazy") _, [_,arg]) <- unApply tm
110 | (P _ (UN "lazy") _, [_,arg]) <- unApply tm
109 = do arg' <- epic' env arg
111 = do arg' <- epic' env arg
110 return $ lazy_ arg'
112 return $ lazy_ arg'