ec631d7 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix default arguments in pattern context

commitec631d73706b317bb6202f7669cc3d537dbf6aa1 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 4 May 2012, 13:45 (14 years ago) parent1f95beb

3 files changed+12−10

compare with master

unifiedsplit

lib/io.idr+1−1 src/Idris/AbsSyntax.hs+8−8 src/Idris/Compiler.hs+3−1

lib/io.idr+1−1

@@ -9,7 +9,7 @@ io_bind : IO a -> (a -> IO b) -> IO b

99io_bind (prim__IO v) k = k v

1010

1111unsafePerformIO : IO a -> a

12−unsafePerformIO (prim__IO x) = x

12+-- compiled as primitive

1313

1414abstract

1515io_return : a -> IO a

src/Idris/AbsSyntax.hs+8−8

@@ -1575,9 +1575,9 @@ addImpl' :: Bool -> [Name] -> IState -> PTerm -> PTerm

15751575addImpl' inpat env ist ptm = ai env ptm

15761576 where

15771577 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 []

15791579 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 []

15811581 ai env (PEq fc l r) = let l' = ai env l

15821582 r' = ai env r in

15831583 PEq fc l' r'

@@ -1596,7 +1596,7 @@ addImpl' inpat env ist ptm = ai env ptm

15961596 ai env (PApp fc (PRef _ f) as)

15971597 | not (f `elem` env)

15981598 = 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'

16001600 ai env (PApp fc f as) = let f' = ai env f

16011601 as' = map (fmap (ai env)) as in

16021602 mkPApp fc 1 f' as'

@@ -1625,18 +1625,18 @@ addImpl' inpat env ist ptm = ai env ptm

16251625-- if in a pattern, and there are no arguments, and there's no possible

16261626-- names with zero explicit arguments, don't add implicits.

16271627

1628−aiFn :: Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm

1629−aiFn True ist fc f []

1628+aiFn :: Bool -> Bool -> IState -> FC -> Name -> [PArg] -> Either Err PTerm

1629+aiFn inpat True ist fc f []

16301630 = case lookupCtxt Nothing f (idris_implicits ist) of

16311631 [] -> Right $ PRef fc f

16321632 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

16341634 else Right $ PRef fc f

16351635 where imp (PExp _ _ _) = False

16361636 imp _ = True

1637−aiFn inpat ist fc f as

1637+aiFn inpat expat ist fc f as

16381638 | 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

16401640 -- This is where namespaces get resolved by adding PAlternative

16411641 = case lookupCtxtName Nothing f (idris_implicits ist) of

16421642 [(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

2121import Epic.Epic hiding (Term, Type, Name, fn, compile)

2222import qualified Epic.Epic as E

2323

24−primDefs = [UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]

24+primDefs = [UN "unsafePerformIO", UN "mkLazyForeign", UN "mkForeign", UN "FalseElim"]

2525

2626compile :: FilePath -> Term -> Idris ()

2727compile f tm

@@ -105,6 +105,8 @@ instance ToEpic (TT Name) where

105105 = doForeign False args

106106 | (P _ (UN "mkLazyForeign") _, args) <- unApply tm

107107 = doForeign True args

108+ | (P _ (UN "unsafePerformIO") _, [_, arg]) <- unApply tm

109+ = epic' env arg

108110 | (P _ (UN "lazy") _, [_,arg]) <- unApply tm

109111 = do arg' <- epic' env arg

110112 return $ lazy_ arg'