f9684d6 · Idris-dev · git.iko.soy

libs/prelude/Builtins.idr+6

compare with master

unifiedsplit

@@ -33,6 +33,12 @@ lazy x = x -- compiled specially

33force : a -> a

34force x = x -- compiled specially

35

36+data Lazy : Type -> Type where

37+ Delay : (val : a) -> Lazy a

38+

39+Force : Lazy a -> a

40+Force (Delay x) = x

41+

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

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

37par x = x -- compiled specially

43par x = x -- compiled specially

38

44

src/Idris/CaseSplit.hs+2

@@ -94,6 +94,8 @@ inventName ist ty n =

94 MN i n | not (tnull n) && thead n == '_'

95 -> mkSupply (supp ++ varlist)

96 MN i n -> mkSupply (UN n : supp ++ varlist)

97+ UN n | thead n == '_'

98+ -> mkSupply (supp ++ varlist)

97 x -> mkSupply (x : supp)

99 x -> mkSupply (x : supp)

98 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++

100 let badnames = map snd (namemap ms) ++ map snd (invented ms) ++

99 explicit ms

101 explicit ms

src/Idris/Core/CaseTree.hs+29

@@ -574,6 +574,10 @@ prune proj (Case n alts)

574 = let alts' = filter notErased (map pruneAlt alts) in

575 case alts' of

576 [] -> 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

577 as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc

581 as@[ConCase cn i args sc] -> if proj then mkProj n 0 args sc

578 else Case n as

582 else Case n as

579 as@[SucCase cn sc] -> if proj then mkProj n (-1) [cn] sc

583 as@[SucCase cn sc] -> if proj then mkProj n (-1) [cn] sc

@@ -594,6 +598,31 @@ prune proj (Case n alts)

594 notErased (DefaultCase ImpossibleCase) = False

598 notErased (DefaultCase ImpossibleCase) = False

595 notErased _ = True

599 notErased _ = True

596

600

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+

597 mkProj n i [] sc = prune proj sc

626 mkProj n i [] sc = prune proj sc

598 mkProj n i (x : xs) sc = mkProj n (i + 1) xs (projRep x n i sc)

627 mkProj n i (x : xs) sc = mkProj n (i + 1) xs (projRep x n i sc)

599

628

src/Idris/Core/Evaluate.hs+2

@@ -101,6 +101,7 @@ simplify :: Context -> Env -> TT Name -> TT Name

101simplify ctxt env t

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

103 (sUN "force", 0),

104+ (sUN "Force", 0),

104 (sUN "assert_smaller", 0),

105 (sUN "assert_smaller", 0),

105 (sUN "assert_total", 0),

106 (sUN "assert_total", 0),

106 (sUN "par", 0),

107 (sUN "par", 0),

@@ -115,6 +116,7 @@ rt_simplify :: Context -> Env -> TT Name -> TT Name

115rt_simplify ctxt env t

116rt_simplify ctxt env t

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

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

117 (sUN "force", 0),

118 (sUN "force", 0),

119+ (sUN "Force", 0),

118 (sUN "par", 0),

120 (sUN "par", 0),

119 (sUN "prim__syntactic_eq", 0),

121 (sUN "prim__syntactic_eq", 0),

120 (sUN "prim_fork", 0)]

122 (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)

250 addIBC (IBCDoc n)

251 let metainf = DataMI params

252 addIBC (IBCMetaInformation n metainf)

253+ -- TMP HACK! Make this a data option

253− collapseCons n cons

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

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

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

255 updateContext (setMetaInformation n metainf)

256 updateContext (setMetaInformation n metainf)

256 mapM_ (checkPositive n) cons

257 mapM_ (checkPositive n) cons

src/Idris/ElabTerm.hs+18−1

@@ -153,7 +153,8 @@ elab ist info pattern opts fn tm

153 tm <- get_term

154 trace ("Elaborating " ++ show t ++ " : " ++ show g ++ "\n\tin " ++ show tm)

155 $ -}

156− do t' <- insertCoerce ina t

156+ do ct <- insertCoerce ina t

157+ t' <- insertLazy ct

157 g <- goal

158 g <- goal

158 tm <- get_term

159 tm <- get_term

159 ps <- get_probs

160 ps <- get_probs

@@ -608,6 +609,22 @@ elab ist info pattern opts fn tm

608 getFC d (PAlternative _ (x:_)) = getFC d x

609 getFC d (PAlternative _ (x:_)) = getFC d x

609 getFC d x = d

610 getFC d x = d

610

611

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+

611 insertCoerce ina t =

628 insertCoerce ina t =

612 do ty <- goal

629 do ty <- goal

613 -- Check for possible coercions to get to the goal

630 -- Check for possible coercions to get to the goal