git.iko.soy/Idris-dev
on master help sign in
Add 'force' (opposite of 'lazy')

Used now in boolElim to ensure that thunks don't build up unnecessarily (and this is the intended semantics of if...then...else anyway).

commit57af98500595c673d12ce8bb5b073d25f0ad707d authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 12 Feb 2014, 12:30 (13 years ago) parent6bb7f86
4 files changed+11−2
compare with master
unifiedsplit
libs/prelude/Builtins.idr+3 libs/prelude/Prelude/Bool.idr+2−2 src/IRTS/Compiler.hs+4 src/Idris/Core/Evaluate.hs+2
libs/prelude/Builtins.idr+3
@@ -30,6 +30,9 @@ trans refl refl = refl
3030lazy : a -> a
3131lazy x = x -- compiled specially
3232
33+force : a -> a
34+force x = x -- compiled specially
35+
3336par : |(thunk:a) -> a
3437par x = x -- compiled specially
3538
libs/prelude/Prelude/Bool.idr+2−2
@@ -5,8 +5,8 @@ data Bool = False | True
55
66-- | Boolean elimination
77boolElim : Bool -> |(t : a) -> |(f : a) -> a
8−boolElim True t e = t
9−boolElim False t e = e
8+boolElim True t e = force t
9+boolElim False t e = force e
1010
1111-- | Defines a predicate on Bool which guarantees that the value is true.
1212data so : Bool -> Type where oh : so True
src/IRTS/Compiler.hs+4
@@ -182,6 +182,10 @@ instance ToIR (TT Name) where
182182 l == txt "lazy"
183183 = do arg' <- ir' env arg
184184 return $ LLazyExp arg'
185+ | (P _ (UN l) _, [_, arg]) <- unApply tm,
186+ l == txt "force"
187+ = do arg' <- ir' env arg
188+ return $ LForce arg'
185189 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,
186190 a == txt "assert_smaller"
187191 = ir' env arg
src/Idris/Core/Evaluate.hs+2
@@ -100,6 +100,7 @@ specialise ctxt env limits t
100100simplify :: Context -> Env -> TT Name -> TT Name
101101simplify ctxt env t
102102 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
103+ (sUN "force", 0),
103104 (sUN "assert_smaller", 0),
104105 (sUN "assert_total", 0),
105106 (sUN "par", 0),
@@ -113,6 +114,7 @@ simplify ctxt env t
113114rt_simplify :: Context -> Env -> TT Name -> TT Name
114115rt_simplify ctxt env t
115116 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
117+ (sUN "force", 0),
116118 (sUN "par", 0),
117119 (sUN "prim__syntactic_eq", 0),
118120 (sUN "prim_fork", 0)]