f9a0008 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Added 'believe_me'

commitf9a0008ca64b5e9b2054602260d2367c02ef5166 authorEdwin Brady <eb@cs.st-andrews.ac.uk> dateFri 18 Nov 2011, 11:16 (15 years ago) parentae3ad10

2 files changed+5−1

unifiedsplit

lib/builtins.idr+2

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

1919lazy : a -> a;

2020lazy x = x; -- compiled specially

2121

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

23+

2224id : a -> a;

2325id x = x;

2426

src/Idris/Compiler.hs+3−1

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

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

1414import qualified Epic.Epic as E

1515

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

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

1717

1818compile :: FilePath -> Idris ()

1919compile f = do ds <- mkDecls

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

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

6262 = do arg' <- epic' env arg

6363 return $ lazy_ arg'

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

65+ = epic' env arg

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

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

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