02003d7 · Idris-dev · git.iko.soy

lib/builtins.idr+6

@@ -21,6 +21,12 @@ sym refl = refl

21lazy : a -> a

22lazy x = x -- compiled specially

23

24+malloc : Int -> a -> a

25+malloc size x = x -- compiled specially

26+

27+trace_malloc : a -> a

28+trace_malloc x = x -- compiled specially

29+

24believe_me : a -> b -- compiled specially as id, use with care!

30believe_me : a -> b -- compiled specially as id, use with care!

25believe_me x = prim__believe_me _ _ x

31believe_me x = prim__believe_me _ _ x

26

32

samples/interp.idr+1−1

@@ -92,5 +92,5 @@ testFac : Int

92testFac = interp [] eFac 4

93

94main : IO ()

95−main = print testFac

95+main = malloc 79856 (print testFac)

96

src/Idris/Compiler.hs+7

@@ -102,6 +102,13 @@ instance ToEpic (TT Name) where

102 = do v' <- epic' env v

103 k' <- epic' env k

104 return (k' @@ (effect_ v'))

105+ | (P _ (UN "malloc") _, [_,size,t]) <- unApply tm

106+ = do size' <- epic' env size

107+ t' <- epic' env t

108+ return $ malloc_ size' t'

109+ | (P _ (UN "trace_malloc") _, [_,t]) <- unApply tm

110+ = do t' <- epic' env t

111+ return $ mallocTrace_ t'

105 | (P (DCon t a) n _, args) <- unApply tm

112 | (P (DCon t a) n _, args) <- unApply tm

106 = epicCon env t a n args

113 = epicCon env t a n args

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

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