f9a0008 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Added 'believe_me'

f9a0008Edwin Brady15 years ago

lib/builtins.idr+2

@@ -19,6 +19,8 @@ sym refl = refl;

19lazy : a -> a;

20lazy x = x; -- compiled specially

22+believe_me : a -> b; -- compiled specially as id, use with care!

23+

22id : a -> a;

24id : a -> a;

23id x = x;

25id x = x;

src/Idris/Compiler.hs+3−1

@@ -13,7 +13,7 @@ import Control.Monad.State

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

14import qualified Epic.Epic as E

16−primDefs = [UN ["mkForeign"], UN ["FalseElim"]]

16+primDefs = [UN ["mkForeign"], UN ["FalseElim"], UN ["believe_me"]]

18compile :: FilePath -> Idris ()

19compile f = do ds <- mkDecls

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

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

62 = do arg' <- epic' env arg

63 return $ lazy_ arg'

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

65+ = epic' env arg

64 epic' env (P (DCon t a) n _) = return $ con_ t

66 epic' env (P (DCon t a) n _) = return $ con_ t

65 epic' env (P (TCon t a) n _) = return $ con_ t

67 epic' env (P (TCon t a) n _) = return $ con_ t

66 epic' env (P _ n _) = return $ ref (ename n)

68 epic' env (P _ n _) = return $ ref (ename n)