git.iko.soy/Idris-dev
on master help sign in
Annotate 'Lazy' with reason for laziness

i.e. is it just for evaluation, or is it for codata? This will be useful for mixed induction/coinduction and allow the productivity checker to be cleverer.

commit3cef6094b9937f64d737ef4de6d866c690e14b38 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateFri 21 Mar 2014, 17:55 (13 years ago) parent7f3d436
6 files changed+45−29
compare with master
unifiedsplit
libs/prelude/Builtins.idr+14−5 libs/prelude/Prelude/Bool.idr+2 src/IRTS/Compiler.hs+1−1 src/Idris/Coverage.hs+4−4 src/Idris/ElabDecls.hs+4−2 src/Idris/ElabTerm.hs+20−17
libs/prelude/Builtins.idr+14−5
@@ -43,14 +43,23 @@ lazy x = x -- compiled specially
4343force : a -> a
4444force x = x -- compiled specially
4545
46−data Lazy : Type -> Type where
47− Delay : (val : a) -> Lazy a
46+data LazyType = LazyCodata | LazyEval
4847
49−Force : Lazy a -> a
48+data Lazy' : LazyType -> Type -> Type where
49+ Delay : {t, a : _} -> (val : a) -> Lazy' t a
50+
51+Force : {t, a : _} -> Lazy' t a -> a
5052Force (Delay x) = x
5153
52−par : Lazy a -> a
53−par (Delay x) = x -- compiled specially
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?
62+par (Delay x) = x
5463
5564malloc : Int -> a -> a
5665malloc size x = x -- compiled specially
libs/prelude/Prelude/Bool.idr+2
@@ -1,5 +1,7 @@
11module Prelude.Bool
22
3+import Builtins
4+
35||| Boolean Data Type
46data Bool = False | True
57
src/IRTS/Compiler.hs+1−1
@@ -193,7 +193,7 @@ instance ToIR (TT Name) where
193193 l == txt "Delay"
194194 = do arg' <- ir' env arg
195195 return $ LLazyExp arg'
196− | (P _ (UN l) _, [_, arg]) <- unApply tm,
196+ | (P _ (UN l) _, [_, _, arg]) <- unApply tm,
197197 l == txt "Force"
198198 = do arg' <- ir' env arg
199199 return $ LForce arg'
src/Idris/Coverage.hs+4−4
@@ -402,12 +402,12 @@ buildSCG (_, n) = do
402402 x -> error $ "buildSCG: " ++ show (n, x)
403403
404404delazy t@(App f a)
405− | (P _ (UN l) _, [_, arg]) <- unApply t,
405+ | (P _ (UN l) _, [_, _, arg]) <- unApply t,
406406 l == txt "Force" = delazy arg
407− | (P _ (UN l) _, [_, arg]) <- unApply t,
407+ | (P _ (UN l) _, [_, _, arg]) <- unApply t,
408408 l == txt "Delay" = delazy arg
409− | (P _ (UN l) _, [arg]) <- unApply t,
410− l == txt "Lazy" = delazy arg
409+ | (P _ (UN l) _, [_, arg]) <- unApply t,
410+ l == txt "Lazy'" = delazy arg
411411delazy (App f a) = App (delazy f) (delazy a)
412412delazy (Bind n b sc) = Bind n (fmap delazy b) (delazy sc)
413413delazy t = t
src/Idris/ElabDecls.hs+4−2
@@ -255,7 +255,7 @@ elabData info syn doc argDocs fc opts (PDatadecl n t_in dcons)
255255 let metainf = DataMI params
256256 addIBC (IBCMetaInformation n metainf)
257257 -- TMP HACK! Make this a data option
258− when (n /= sUN "Lazy") $ collapseCons n cons
258+ when (n /= sUN "Lazy'") $ collapseCons n cons
259259 updateContext (addDatatype (Data n ttag cty cons))
260260 updateContext (setMetaInformation n metainf)
261261 mapM_ (checkPositive n) cons
@@ -875,7 +875,9 @@ elabCon info syn tn codata (doc, argDocs, n, t_in, fc, forcenames)
875875
876876 mkLazy (PPi pl n ty sc)
877877 = 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]
879881 else ty in
880882 PPi pl n ty' (mkLazy sc)
881883 mkLazy t = t
src/Idris/ElabTerm.hs+20−17
@@ -173,25 +173,27 @@ elab ist info pattern opts fn tm
173173 -- ++ "\n-----------\n") $
174174 --trace ("ELAB " ++ show t') $
175175 let fc = fileFC "Force"
176− handleError forceErr
176+ env <- get_env
177+ handleError (forceErr env)
177178 (elab' ina t')
178179 (elab' ina (PApp fc (PRef fc (sUN "Force"))
179− [pimp (sUN "a") Placeholder True,
180+ [pimp (sUN "t") Placeholder True,
181+ pimp (sUN "a") Placeholder True,
180182 pexp ct])) True
181183
182− forceErr (CantUnify _ t t' _ _ _)
183− | (P _ (UN ht) _, _) <- unApply t,
184− ht == txt "Lazy" = True
185− forceErr (CantUnify _ t t' _ _ _)
186− | (P _ (UN ht) _, _) <- unApply t',
187− ht == txt "Lazy" = True
188− forceErr (InfiniteUnify _ t _)
189− | (P _ (UN ht) _, _) <- unApply t,
190− ht == txt "Lazy" = True
191− forceErr (Elaborating _ _ t) = forceErr t
192− forceErr (ElaboratingArg _ _ t) = forceErr t
193− forceErr (At _ t) = forceErr t
194− forceErr t = False
184+ forceErr env (CantUnify _ t t' _ _ _)
185+ | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
186+ ht == txt "Lazy'" = True
187+ forceErr env (CantUnify _ t t' _ _ _)
188+ | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t'),
189+ ht == txt "Lazy'" = True
190+ forceErr env (InfiniteUnify _ t _)
191+ | (P _ (UN ht) _, _) <- unApply (normalise (tt_ctxt ist) env t),
192+ ht == txt "Lazy'" = True
193+ forceErr env (Elaborating _ _ t) = forceErr env t
194+ forceErr env (ElaboratingArg _ _ t) = forceErr env t
195+ forceErr env (At _ t) = forceErr env t
196+ forceErr env t = False
195197
196198 local f = do e <- get_env
197199 return (f `elem` map fst e)
@@ -688,13 +690,14 @@ elab ist info pattern opts fn tm
688690 let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
689691 let tries = if pattern then [t, mkDelay t] else [mkDelay t, t]
690692 case tyh of
691− P _ (UN l) _ | l == txt "Lazy"
693+ P _ (UN l) _ | l == txt "Lazy'"
692694 -> return (PAlternative False tries)
693695 _ -> return t
694696 where
695697 mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)
696698 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])
698701
699702 insertCoerce ina t =
700703 do ty <- goal