57af985 · Idris-dev · git.iko.soy

libs/prelude/Builtins.idr+3

compare with master

unifiedsplit

@@ -30,6 +30,9 @@ trans refl refl = refl

30lazy : a -> a

31lazy x = x -- compiled specially

32

33+force : a -> a

34+force x = x -- compiled specially

35+

33par : |(thunk:a) -> a

36par : |(thunk:a) -> a

34par x = x -- compiled specially

37par x = x -- compiled specially

35

38

libs/prelude/Prelude/Bool.idr+2−2

@@ -5,8 +5,8 @@ data Bool = False | True

5

6-- | Boolean elimination

7boolElim : Bool -> |(t : a) -> |(f : a) -> a

8−boolElim True t e = t

8+boolElim True t e = force t

9−boolElim False t e = e

9+boolElim False t e = force e

10

11-- | Defines a predicate on Bool which guarantees that the value is true.

12data so : Bool -> Type where oh : so True

src/IRTS/Compiler.hs+4

@@ -182,6 +182,10 @@ instance ToIR (TT Name) where

182 l == txt "lazy"

183 = do arg' <- ir' env arg

184 return $ LLazyExp arg'

185+ | (P _ (UN l) _, [_, arg]) <- unApply tm,

186+ l == txt "force"

187+ = do arg' <- ir' env arg

188+ return $ LForce arg'

185 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,

189 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,

186 a == txt "assert_smaller"

190 a == txt "assert_smaller"

187 = ir' env arg

191 = ir' env arg

src/Idris/Core/Evaluate.hs+2

@@ -100,6 +100,7 @@ specialise ctxt env limits t

100simplify :: Context -> Env -> TT Name -> TT Name

101simplify ctxt env t

102 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),

103+ (sUN "force", 0),

103 (sUN "assert_smaller", 0),

104 (sUN "assert_smaller", 0),

104 (sUN "assert_total", 0),

105 (sUN "assert_total", 0),

105 (sUN "par", 0),

106 (sUN "par", 0),

@@ -113,6 +114,7 @@ simplify ctxt env t

113rt_simplify :: Context -> Env -> TT Name -> TT Name

114rt_simplify :: Context -> Env -> TT Name -> TT Name

114rt_simplify ctxt env t

115rt_simplify ctxt env t

115 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),

116 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),

117+ (sUN "force", 0),

116 (sUN "par", 0),

118 (sUN "par", 0),

117 (sUN "prim__syntactic_eq", 0),

119 (sUN "prim__syntactic_eq", 0),

118 (sUN "prim_fork", 0)]

120 (sUN "prim_fork", 0)]