git.iko.soy/Idris-dev
on master help sign in
Add 'Lazy' type for capturing delayed computations
commitf9684d6d9ad5983619aea4ed1a545bc600ed6726 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateThu 13 Feb 2014, 11:38 (13 years ago) parent57af985
6 files changed+59−2
compare with master
unifiedsplit
libs/prelude/Builtins.idr+6 src/Idris/CaseSplit.hs+2 src/Idris/Core/CaseTree.hs+29 src/Idris/Core/Evaluate.hs+2 src/Idris/ElabDecls.hs+2−1 src/Idris/ElabTerm.hs+18−1
libs/prelude/Builtins.idr+6
@@ -33,6 +33,12 @@ lazy x = x -- compiled specially
3333force : a -> a
3434force x = x -- compiled specially
3535
36+data Lazy : Type -> Type where
37+ Delay : (val : a) -> Lazy a
38+
39+Force : Lazy a -> a
40+Force (Delay x) = x
41+
3642par : |(thunk:a) -> a
3743par x = x -- compiled specially
3844
src/Idris/CaseSplit.hs+2
@@ -94,6 +94,8 @@ inventName ist ty n =
9494 MN i n | not (tnull n) && thead n == '_'
9595 -> mkSupply (supp ++ varlist)
9696 MN i n -> mkSupply (UN n : supp ++ varlist)
97+ UN n | thead n == '_'
98+ -> mkSupply (supp ++ varlist)
9799 x -> mkSupply (x : supp)
98100 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++
99101 explicit ms
src/Idris/Core/CaseTree.hs+29
@@ -574,6 +574,10 @@ prune proj (Case n alts)
574574 = let alts' = filter notErased (map pruneAlt alts) in
575575 case alts' of
576576 [] -> ImpossibleCase
577+ as@[ConCase (UN delay) i [arg] sc]
578+ | delay == txt "Delay"
579+ -> if proj then mkForce n arg sc
580+ else Case n as
577581 as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc
578582 else Case n as
579583 as@[SucCase cn sc] -> if proj then mkProj n (-1) [cn] sc
@@ -594,6 +598,31 @@ prune proj (Case n alts)
594598 notErased (DefaultCase ImpossibleCase) = False
595599 notErased _ = True
596600
601+ mkForce n arg (Case x alts)
602+ | x == arg = ProjCase (forceArg n)
603+ (map (mkForceAlt n arg) alts)
604+ | otherwise = Case x (map (mkForceAlt n arg) alts)
605+ mkForce n arg (ProjCase t alts)
606+ = ProjCase (forceTm n arg t) (map (mkForceAlt n arg) alts)
607+ mkForce n arg (STerm t) = STerm (forceTm n arg t)
608+ mkForce n arg c = c
609+
610+ mkForceAlt n arg (ConCase cn t args rhs)
611+ = ConCase cn t args (mkForce n arg rhs)
612+ mkForceAlt n arg (FnCase cn args rhs)
613+ = FnCase cn args (mkForce n arg rhs)
614+ mkForceAlt n arg (ConstCase t rhs)
615+ = ConstCase t (mkForce n arg rhs)
616+ mkForceAlt n arg (SucCase sn rhs)
617+ = SucCase sn (mkForce n arg rhs)
618+ mkForceAlt n arg (DefaultCase rhs)
619+ = DefaultCase (mkForce n arg rhs)
620+
621+ forceTm n arg t = subst arg (forceArg n) t
622+
623+ forceArg n = App (App (P Ref (sUN "Force") Erased) Erased)
624+ (P Bound n Erased)
625+
597626 mkProj n i [] sc = prune proj sc
598627 mkProj n i (x : xs) sc = mkProj n (i + 1) xs (projRep x n i sc)
599628
src/Idris/Core/Evaluate.hs+2
@@ -101,6 +101,7 @@ simplify :: Context -> Env -> TT Name -> TT Name
101101simplify ctxt env t
102102 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
103103 (sUN "force", 0),
104+ (sUN "Force", 0),
104105 (sUN "assert_smaller", 0),
105106 (sUN "assert_total", 0),
106107 (sUN "par", 0),
@@ -115,6 +116,7 @@ rt_simplify :: Context -> Env -> TT Name -> TT Name
115116rt_simplify ctxt env t
116117 = evalState (do val <- eval False ctxt [(sUN "lazy", 0),
117118 (sUN "force", 0),
119+ (sUN "Force", 0),
118120 (sUN "par", 0),
119121 (sUN "prim__syntactic_eq", 0),
120122 (sUN "prim_fork", 0)]
src/Idris/ElabDecls.hs+2−1
@@ -250,7 +250,8 @@ elabData info syn doc fc opts (PDatadecl n t_in dcons)
250250 addIBC (IBCDoc n)
251251 let metainf = DataMI params
252252 addIBC (IBCMetaInformation n metainf)
253− collapseCons n cons
253+ -- TMP HACK! Make this a data option
254+ when (n /= sUN "Lazy") $ collapseCons n cons
254255 updateContext (addDatatype (Data n ttag cty cons))
255256 updateContext (setMetaInformation n metainf)
256257 mapM_ (checkPositive n) cons
src/Idris/ElabTerm.hs+18−1
@@ -153,7 +153,8 @@ elab ist info pattern opts fn tm
153153 tm <- get_term
154154 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)
155155 $ -}
156− do t' <- insertCoerce ina t
156+ do ct <- insertCoerce ina t
157+ t' <- insertLazy ct
157158 g <- goal
158159 tm <- get_term
159160 ps <- get_probs
@@ -608,6 +609,22 @@ elab ist info pattern opts fn tm
608609 getFC d (PAlternative _ (x:_)) = getFC d x
609610 getFC d x = d
610611
612+ insertLazy :: PTerm -> ElabD PTerm
613+-- insertLazy t | pattern = return t
614+ insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t
615+ insertLazy t =
616+ do ty <- goal
617+ env <- get_env
618+ let (tyh, _) = unApply (normalise (tt_ctxt ist) env ty)
619+ case tyh of
620+ P _ (UN l) _ | l == txt "Lazy"
621+ -> return (PAlternative False [t, mkDelay t])
622+ _ -> return t
623+ where
624+ mkDelay t = let fc = fileFC "Delay" in
625+ addImpl ist (PApp fc (PRef fc (sUN "Delay")) [pexp t])
626+
627+
611628 insertCoerce ina t =
612629 do ty <- goal
613630 -- Check for possible coercions to get to the goal