3cef609 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Annotate 'Lazy' with reason for laziness

3cef609Edwin Brady13 years ago

libs/prelude/Builtins.idr+14−5

compare with master

unifiedsplit

@@ -43,14 +43,23 @@ lazy x = x -- compiled specially

43force : a -> a

44force x = x -- compiled specially

46−data Lazy : Type -> Type where

46+data LazyType = LazyCodata | LazyEval

47− Delay : (val : a) -> Lazy a

48+data Lazy' : LazyType -> Type -> Type where

49+ Delay : {t, a : _} -> (val : a) -> Lazy' t a

50+

49−Force : Lazy a -> a

51+Force : {t, a : _} -> Lazy' t a -> a

50Force (Delay x) = x

52Force (Delay x) = x

52−par : Lazy a -> a

54+Lazy : Type -> Type

55+Lazy t = Lazy' LazyEval t

56+

57+Inf : Type -> Type

58+Inf t = Lazy' LazyCodata t

59+

60+par : Lazy a -> a -- Doesn't actually do anything yet. Maybe a 'Par a' type

61+ -- is better in any case?

53−par (Delay x) = x -- compiled specially

62+par (Delay x) = x

55malloc : Int -> a -> a

64malloc : Int -> a -> a

56malloc size x = x -- compiled specially

65malloc size x = x -- compiled specially

libs/prelude/Prelude/Bool.idr+2

@@ -1,5 +1,7 @@

1module Prelude.Bool

3+import Builtins

3||| Boolean Data Type

5||| Boolean Data Type

4data Bool = False | True

6data Bool = False | True

src/IRTS/Compiler.hs+1−1

@@ -193,7 +193,7 @@ instance ToIR (TT Name) where

193 l == txt "Delay"

194 = do arg' <- ir' env arg

195 return $ LLazyExp arg'

196− | (P _ (UN l) _, [_, arg]) <- unApply tm,

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

197 l == txt "Force"

198 = do arg' <- ir' env arg

199 return $ LForce arg'

src/Idris/Coverage.hs+4−4

@@ -402,12 +402,12 @@ buildSCG (_, n) = do

402 x -> error $ "buildSCG: " ++ show (n, x)

403

404delazy t@(App f a)

405− | (P _ (UN l) _, [_, arg]) <- unApply t,

405+ | (P _ (UN l) _, [_, _, arg]) <- unApply t,

406 l == txt "Force" = delazy arg

407− | (P _ (UN l) _, [_, arg]) <- unApply t,

407+ | (P _ (UN l) _, [_, _, arg]) <- unApply t,

408 l == txt "Delay" = delazy arg

409− | (P _ (UN l) _, [arg]) <- unApply t,

409+ | (P _ (UN l) _, [_, arg]) <- unApply t,

410− l == txt "Lazy" = delazy arg

410+ l == txt "Lazy'" = delazy arg

411delazy (App f a) = App (delazy f) (delazy a)

412delazy (Bind n b sc) = Bind n (fmap delazy b) (delazy sc)

413delazy t = t

src/Idris/ElabDecls.hs+4−2

@@ -255,7 +255,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)

255 let metainf = DataMI params

256 addIBC (IBCMetaInformation n metainf)

257 -- TMP HACK! Make this a data option

258− when (n /= sUN "Lazy") $ collapseCons n cons

258+ when (n /= sUN "Lazy'") $ collapseCons n cons

259 updateContext (addDatatype (Data n ttag cty cons))

260 updateContext (setMetaInformation n metainf)

261 mapM_ (checkPositive n) cons

@@ -875,7 +875,9 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)

875

876 mkLazy (PPi pl n ty sc)

877 = let ty' = if getTyName ty

878− then PApp fc (PRef fc (sUN "Lazy")) [pexp ty]

878+ then PApp fc (PRef fc (sUN "Lazy'"))

879+ [pexp (PRef fc (sUN "LazyCodata")),

880+ pexp ty]

879 else ty in

881 else ty in

880 PPi pl n ty' (mkLazy sc)

882 PPi pl n ty' (mkLazy sc)

881 mkLazy t = t

883 mkLazy t = t

src/Idris/ElabTerm.hs+20−17

@@ -173,25 +173,27 @@ elab ist info pattern opts fn tm

173 -- ++ "\n-----------\n") $

174 --trace ("ELAB " ++ show t') $

175 let fc = fileFC "Force"

176+ env <- get_env

176− handleError forceErr

177+ handleError (forceErr env)

177 (elab' ina t')

178 (elab' ina t')

178 (elab' ina (PApp fc (PRef fc (sUN "Force"))

179 (elab' ina (PApp fc (PRef fc (sUN "Force"))

180+ [pimp (sUN "t") Placeholder True,

179− [pimp (sUN "a") Placeholder True,

181+ pimp (sUN "a") Placeholder True,

180 pexp ct])) True

182 pexp ct])) True

181

183

182− forceErr (CantUnify _ t t' _ _ _)

184+ forceErr env (CantUnify _ t t' _ _ _)

183− | (P _ (UN ht) _, _) <- unApply t,

185+ | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

184− ht == txt "Lazy" = True

186+ ht == txt "Lazy'" = True

185− forceErr (CantUnify _ t t' _ _ _)

187+ forceErr env (CantUnify _ t t' _ _ _)

186− | (P _ (UN ht) _, _) <- unApply t',

188+ | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),

187− ht == txt "Lazy" = True

189+ ht == txt "Lazy'" = True

188− forceErr (InfiniteUnify _ t _)

190+ forceErr env (InfiniteUnify _ t _)

189− | (P _ (UN ht) _, _) <- unApply t,

191+ | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),

190− ht == txt "Lazy" = True

192+ ht == txt "Lazy'" = True

191− forceErr (Elaborating _ _ t) = forceErr t

193+ forceErr env (Elaborating _ _ t) = forceErr env t

192− forceErr (ElaboratingArg _ _ t) = forceErr t

194+ forceErr env (ElaboratingArg _ _ t) = forceErr env t

193− forceErr (At _ t) = forceErr t

195+ forceErr env (At _ t) = forceErr env t

194− forceErr t = False

196+ forceErr env t = False

195

197

196 local f = do e <- get_env

198 local f = do e <- get_env

197 return (f `elem` map fst e)

199 return (f `elem` map fst e)

@@ -688,13 +690,14 @@ elab ist info pattern opts fn tm

688 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)

690 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)

689 let tries = if pattern then [t, mkDelay t] else [mkDelay t, t]

691 let tries = if pattern then [t, mkDelay t] else [mkDelay t, t]

690 case tyh of

692 case tyh of

691− P _ (UN l) _ | l == txt "Lazy"

693+ P _ (UN l) _ | l == txt "Lazy'"

692 -> return (PAlternative False tries)

694 -> return (PAlternative False tries)

693 _ -> return t

695 _ -> return t

694 where

696 where

695 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

697 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

696 mkDelay t = let fc = fileFC "Delay" in

698 mkDelay t = let fc = fileFC "Delay" in

697− addImpl ist (PApp fc (PRef fc (sUN "Delay")) [pexp t])

699+ addImpl ist (PApp fc (PRef fc (sUN "Delay"))

700+ [pexp t])

698

701

699 insertCoerce ina t =

702 insertCoerce ina t =

700 do ty <- goal

703 do ty <- goal