130f437 · Idris-dev · git.iko.soy

libs/base/System/Concurrency/Process.idr+1−1

compare with master

unifiedsplit

@@ -62,7 +62,7 @@ recvWithSender {msg}

62 where get : IO (Ptr, msg)

63 get = getMsg

64

65−create : |(thread : Process msg ()) -> Process msg (ProcID msg)

65+create : Process msg () -> Process msg (ProcID msg)

66create (lift p) = do ptr <- lift (fork p)

67 return (MkPID ptr)

68

libs/effects/Effects.idr+1−2

@@ -262,8 +262,7 @@ eff env (lift prf effP) k

262 = let env' = dropEnv env prf in

263 eff env' effP (\envk, p' => k (rebuildEnv envk prf env) p')

264eff env (new r prog) k

265− = let env' = r :: env in

266− eff env' prog (\(v :: envk), p' => k envk p')

265+ = eff (r :: env) prog (\(v :: envk), p' => k envk p')

267eff env (test prf l r) k

266eff env (test prf l r) k

268 = testEff env prf (\envk => eff envk l k) (\envk => eff envk r k)

267 = testEff env prf (\envk => eff envk l k) (\envk => eff envk r k)

269eff env (test_lbl prf l r) k

268eff env (test_lbl prf l r) k

libs/neweffects/Effects.idr+1−2

@@ -237,8 +237,7 @@ eff env (lift prf effP) k

237 = let env' = dropEnv env prf in

238 eff env' effP (\p', envk => k p' (rebuildEnv envk prf env))

239eff env (new r prog) k

240− = let env' = r :: env in

241− eff env' prog (\p' => \ (v :: envk) => k p' envk)

240+ = eff (r :: env) prog (\p' => \ (v :: envk) => k p' envk)

242eff env (catch prog handler) k

241eff env (catch prog handler) k

243 = catch (eff env prog k)

242 = catch (eff env prog k)

244 (\e => eff env (handler e) k)

243 (\e => eff env (handler e) k)

libs/prelude/Builtins.idr+2−2

@@ -39,8 +39,8 @@ data Lazy : Type -> Type where

39Force : Lazy a -> a

40Force (Delay x) = x

41

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

42+par : Lazy a -> a

43−par x = x -- compiled specially

43+par (Delay x) = x -- compiled specially

44

45malloc : Int -> a -> a

46malloc size x = x -- compiled specially

libs/prelude/IO.idr+2−2

@@ -131,10 +131,10 @@ run__provider (MkIO f) = prim_io_bind (f TheWorld)

131

132-- io_bind v (\v' => io_return v')

133

134−prim_fork : |(thread:PrimIO ()) -> PrimIO Ptr

134+prim_fork : PrimIO () -> PrimIO Ptr

135prim_fork x = prim_io_return prim__vm -- compiled specially

136

137−fork : |(thread:IO ()) -> IO Ptr

137+fork : IO () -> IO Ptr

138fork (MkIO f) = MkIO (\w => prim_io_bind

139 (prim_fork (prim_io_bind (f w)

140 (\ x => prim_io_return x)))

libs/prelude/Prelude.idr+1−1

@@ -550,7 +550,7 @@ validFile (FHandle h) = do x <- nullPtr h

550 return (not x)

551

552partial -- obviously

553−while : |(test : IO Bool) -> |(body : IO ()) -> IO ()

553+while : (test : IO Bool) -> (body : IO ()) -> IO ()

554while t b = do v <- t

555 if v then do b

556 while t b

libs/prelude/Prelude/Bits.idr+1

@@ -2,6 +2,7 @@ module Prelude.Bits

2

3import Prelude.Strings

4import Prelude.Vect

5+import Prelude.Bool

5

6

6%access public

7%access public

7%default total

8%default total

libs/prelude/Prelude/Bool.idr+4−4

@@ -4,15 +4,15 @@ module Prelude.Bool

4data Bool = False | True

5

6-- | Boolean elimination

7−boolElim : Bool -> |(t : a) -> |(f : a) -> a

7+boolElim : Bool -> (t : Lazy a) -> (e : Lazy a) -> a

8−boolElim True t e = force t

8+boolElim True t e = t

9−boolElim False t e = force e

9+boolElim False t e = e

10

11-- | Defines a predicate on Bool which guarantees that the value is true.

12data so : Bool -> Type where oh : so True

13

14-- Syntaxtic sugar for boolean elimination.

15−syntax if [test] then [t] else [e] = boolElim test t e

15+syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

16

17-- Boolean Operator Precedence

18infixl 4 &&, ||

libs/prelude/Prelude/Maybe.idr+2−2

@@ -28,11 +28,11 @@ isJust (Just j) = True

28-- Misc

29--------------------------------------------------------------------------------

30

31−maybe : |(def : b) -> (a -> b) -> Maybe a -> b

31+maybe : Lazy b -> (a -> b) -> Maybe a -> b

32maybe n j Nothing = n

33maybe n j (Just x) = j x

34

35−fromMaybe : |(def: a) -> Maybe a -> a

35+fromMaybe : (Lazy a) -> Maybe a -> a

36fromMaybe def Nothing = def

37fromMaybe def (Just j) = j

38

libs/prelude/Prelude/Vect.idr+2

@@ -4,7 +4,9 @@ import Prelude.Fin

4import Prelude.Foldable

5import Prelude.Functor

6import Prelude.List

7+import Prelude.Classes

7import Prelude.Nat

8import Prelude.Nat

9+import Prelude.Bool

8

10

9%access public

11%access public

10%default total

12%default total

src/IRTS/Compiler.hs+12−1

@@ -178,14 +178,25 @@ instance ToIR (TT Name) where

178 | (P _ (UN r) _, [_, _, _, _, _, arg]) <- unApply tm,

179 r == txt "replace"

180 = ir' env arg

181+ -- Laziness, the old way

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

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

182 l == txt "lazy"

183 l == txt "lazy"

183 = do arg' <- ir' env arg

184 = do arg' <- ir' env arg

185+ error "lazy has crept in somehow"

184− return $ LLazyExp arg'

186+-- return $ LLazyExp arg'

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

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

186 l == txt "force"

188 l == txt "force"

187 = do arg' <- ir' env arg

189 = do arg' <- ir' env arg

188 return $ LForce arg'

190 return $ LForce arg'

191+ -- Laziness, the new way

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

193+ l == txt "Delay"

194+ = do arg' <- ir' env arg

195+ return $ LLazyExp arg'

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

197+ l == txt "Force"

198+ = do arg' <- ir' env arg

199+ return $ LForce arg'

189 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,

200 | (P _ (UN a) _, [_, _, arg]) <- unApply tm,

190 a == txt "assert_smaller"

201 a == txt "assert_smaller"

191 = ir' env arg

202 = ir' env arg

src/Idris/CaseSplit.hs+4

@@ -321,6 +321,10 @@ getClause l fn fp = do ty <- getInternalApp fp l

321 where mkApp i (PPi (Exp _ _ _ False) (MN _ _) ty sc) used

322 = let n = getNameFrom i used ty in

323 show n ++ " " ++ mkApp i sc (n : used)

324+ mkApp i (PPi (Exp _ _ _ False) (UN n) ty sc) used

325+ | thead n == '_'

326+ = let n = getNameFrom i used ty in

327+ show n ++ " " ++ mkApp i sc (n : used)

324 mkApp i (PPi (Exp _ _ _ False) n _ sc) used

328 mkApp i (PPi (Exp _ _ _ False) n _ sc) used

325 = show n ++ " " ++ mkApp i sc (n : used)

329 = show n ++ " " ++ mkApp i sc (n : used)

326 mkApp i (PPi _ _ _ sc) used = mkApp i sc used

330 mkApp i (PPi _ _ _ sc) used = mkApp i sc used

src/Idris/Core/CaseTree.hs+8−2

@@ -150,12 +150,18 @@ findCalls sc topargs = nub $ nu' topargs sc where

150

151-- Find names which are used directly (i.e. not in a function call) in a term

152

153−directUse :: Eq n => TT n -> [n]

153+directUse :: TT Name -> [Name]

154directUse (P _ n _) = [n]

155directUse (Bind n (Let t v) sc) = nub $ directUse v ++ (directUse sc \\ [n])

156 ++ directUse t

157directUse (Bind n b sc) = nub $ directUse (binderTy b) ++ (directUse sc \\ [n])

158directUse fn@(App f a)

159+ | (P Ref (UN pfk) _, [App e w]) <- unApply fn,

160+ pfk == txt "prim_fork"

161+ = directUse e ++ directUse w -- HACK so that fork works

162+ | (P Ref (UN fce) _, [_, a]) <- unApply fn,

163+ fce == txt "Force"

164+ = directUse a -- forcing a value counts as a use

159 | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them

165 | (P Ref n _, args) <- unApply fn = [] -- need to know what n does with them

160 | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime

166 | (P (TCon _ _) n _, args) <- unApply fn = [] -- type constructors not used at runtime

161 | otherwise = nub $ directUse f ++ directUse a

167 | otherwise = nub $ directUse f ++ directUse a

@@ -574,7 +580,7 @@ prune proj (Case n alts)

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

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

575 case alts' of

581 case alts' of

576 [] -> ImpossibleCase

582 [] -> ImpossibleCase

577− as@[ConCase (UN delay) i [arg] sc]

583+ as@(ConCase (UN delay) i [arg] sc : _)

578 | delay == txt "Delay"

584 | delay == txt "Delay"

579 -> if proj then mkForce n arg sc

585 -> if proj then mkForce n arg sc

580 else Case n as

586 else Case n as

src/Idris/Core/Elaborate.hs+25−10

@@ -630,13 +630,28 @@ no_errors tac err

630try :: Elab' aux a -> Elab' aux a -> Elab' aux a

631try t1 t2 = try' t1 t2 False

632

633+handleError :: (Err -> Bool) -> Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

634+handleError p t1 t2 proofSearch

635+ = do s <- get

636+ ps <- get_probs

637+ case runStateT t1 s of

638+ OK (v, s') -> do put s'

639+ return $! v

640+ Error e1 -> if p e1 then

641+ do case runStateT t2 s of

642+ OK (v, s') -> do put s'; return $! v

643+ Error e2 -> if score e1 >= score e2

644+ then lift (tfail e1)

645+ else lift (tfail e2)

646+ else lift (tfail e1)

647+

633try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

648try' :: Elab' aux a -> Elab' aux a -> Bool -> Elab' aux a

634try' t1 t2 proofSearch

649try' t1 t2 proofSearch

635 = do s <- get

650 = do s <- get

636 ps <- get_probs

651 ps <- get_probs

637 case prunStateT 999999 False ps t1 s of

652 case prunStateT 999999 False ps t1 s of

638− OK ((v, _), s') -> do put s'

653+ OK ((v, _, _), s') -> do put s'

639− return $! v

654+ return $! v

640 Error e1 -> if recoverableErr e1 then

655 Error e1 -> if recoverableErr e1 then

641 do case runStateT t2 s of

656 do case runStateT t2 s of

642 OK (v, s') -> do put s'; return $! v

657 OK (v, s') -> do put s'; return $! v

@@ -658,7 +673,7 @@ tryWhen False a b = a

658

673

659-- Try a selection of tactics. Exactly one must work, all others must fail

674-- Try a selection of tactics. Exactly one must work, all others must fail

660tryAll :: [(Elab' aux a, String)] -> Elab' aux a

675tryAll :: [(Elab' aux a, String)] -> Elab' aux a

661−tryAll xs = tryAll' [] 999999 (cantResolve, 0) (map fst xs)

676+tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

662 where

677 where

663 cantResolve :: Elab' aux a

678 cantResolve :: Elab' aux a

664 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

679 cantResolve = lift $ tfail $ CantResolveAlts (map snd xs)

@@ -666,24 +681,24 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) (map fst xs)

666 tryAll' :: [Elab' aux a] -> -- successes

681 tryAll' :: [Elab' aux a] -> -- successes

667 Int -> -- most problems

682 Int -> -- most problems

668 (Elab' aux a, Int) -> -- smallest failure

683 (Elab' aux a, Int) -> -- smallest failure

669− [Elab' aux a] -> -- still to try

684+ [(Elab' aux a, String)] -> -- still to try

670 Elab' aux a

685 Elab' aux a

671 tryAll' [res] pmax _ [] = res

686 tryAll' [res] pmax _ [] = res

672 tryAll' (_:_) pmax _ [] = cantResolve

687 tryAll' (_:_) pmax _ [] = cantResolve

673 tryAll' [] pmax (f, _) [] = f

688 tryAll' [] pmax (f, _) [] = f

674− tryAll' cs pmax f (x:xs)

689+ tryAll' cs pmax f ((x, msg):xs)

675 = do s <- get

690 = do s <- get

676 ps <- get_probs

691 ps <- get_probs

677 case prunStateT pmax True ps x s of

692 case prunStateT pmax True ps x s of

678− OK ((v, newps), s') ->

693+ OK ((v, newps, probs), s') ->

679 do let cs' = if (newps < pmax)

694 do let cs' = if (newps < pmax)

680 then [do put s'; return $! v]

695 then [do put s'; return $! v]

681 else (do put s'; return $! v) : cs

696 else (do put s'; return $! v) : cs

682 tryAll' cs' newps f xs

697 tryAll' cs' newps f xs

683 Error err -> do put s

698 Error err -> do put s

684− if (score err) < 100

699+-- if (score err) < 100

685− then tryAll' cs pmax (better err f) xs

700+ tryAll' cs pmax (better err f) xs

686− else tryAll' [] pmax (better err f) xs -- give up

701+-- else tryAll' [] pmax (better err f) xs -- give up

687

702

688

703

689 better err (f, i) = let s = score err in

704 better err (f, i) = let s = score err in

@@ -698,7 +713,7 @@ prunStateT pmax zok ps x s

698 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

713 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

699 then case reverse (problems p) of

714 then case reverse (problems p) of

700 ((_,_,_,e):_) -> Error e

715 ((_,_,_,e):_) -> Error e

701− else OK ((v, newpmax), s')

716+ else OK ((v, newpmax, problems p), s')

702 Error e -> Error e

717 Error e -> Error e

703

718

704qshow :: Fails -> String

719qshow :: Fails -> String

src/Idris/Core/Unify.hs+14−4

@@ -251,24 +251,30 @@ unify ctxt env topx topy dont holes =

251 | holeIn env x || x `elem` holes

252 = do UI s f <- get

253 -- injectivity check

254+ x <- checkCycle bnames (x, tm)

254 if (notP tm && fn)

255 if (notP tm && fn)

255-- trace (show (x, tm, normalise ctxt env tm)) $

256-- trace (show (x, tm, normalise ctxt env tm)) $

256-- put (UI s ((tm, topx, topy) : i) f)

257-- put (UI s ((tm, topx, topy) : i) f)

257 then unifyTmpFail xtm tm

258 then unifyTmpFail xtm tm

258 else do sc 1

259 else do sc 1

259− checkCycle bnames (x, tm)

260+ return x

260− | not (injective xtm) && injective tm = unifyTmpFail xtm tm

261+ | not (injective xtm) && injective tm

262+ = do checkCycle bnames (x, tm)

263+ unifyTmpFail xtm tm

261 un' fn bnames tm ytm@(P _ y _)

264 un' fn bnames tm ytm@(P _ y _)

262 | holeIn env y || y `elem` holes

265 | holeIn env y || y `elem` holes

263 = do UI s f <- get

266 = do UI s f <- get

264 -- injectivity check

267 -- injectivity check

268+ x <- checkCycle bnames (y, tm)

265 if (notP tm && fn)

269 if (notP tm && fn)

266-- trace (show (y, tm, normalise ctxt env tm)) $

270-- trace (show (y, tm, normalise ctxt env tm)) $

267-- put (UI s ((tm, topx, topy) : i) f)

271-- put (UI s ((tm, topx, topy) : i) f)

268 then unifyTmpFail tm ytm

272 then unifyTmpFail tm ytm

269 else do sc 1

273 else do sc 1

270− checkCycle bnames (y, tm)

274+ return x

271− | not (injective ytm) && injective tm = unifyTmpFail tm ytm

275+ | not (injective ytm) && injective tm

276+ = do checkCycle bnames (y, tm)

277+ unifyTmpFail tm ytm

272 un' fn bnames (V i) (P _ x _)

278 un' fn bnames (V i) (P _ x _)

273 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

279 | fst (bnames!!i) == x || snd (bnames!!i) == x = do sc 1; return []

274 un' fn bnames (P _ x _) (V i)

280 un' fn bnames (P _ x _) (V i)

@@ -527,6 +533,10 @@ envPos x i ((y, _) : ys) | x == y = i

527-- FIXME: Depending on how overloading gets used, this may cause problems. Better

533-- FIXME: Depending on how overloading gets used, this may cause problems. Better

528-- rethink overloading properly...

534-- rethink overloading properly...

529

535

536+recoverable t@(App _ _) _

537+ | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False

538+recoverable _ t@(App _ _)

539+ | (P _ (UN l) _, _) <- unApply t, l == txt "Lazy" = False

530recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)

540recoverable (P (DCon _ _) x _) (P (DCon _ _) y _)

531 | x == y = True

541 | x == y = True

532 | otherwise = False

542 | otherwise = False

src/Idris/Coverage.hs+20−11

@@ -222,8 +222,9 @@ upd p' p = p { getTm = p' }

222-- and update the context accordingly

223

224checkPositive :: Name -> (Name, Type) -> Idris ()

225−checkPositive n (cn, ty)

225+checkPositive n (cn, ty')

226+ = do let ty = delazy ty'

226− = do let p = cp ty

227+ let p = cp ty

227 i <- getIState

228 i <- getIState

228 let tot = if p then Total (args ty) else Partial NotPositive

229 let tot = if p then Total (args ty) else Partial NotPositive

229 let ctxt' = setTotal cn tot (tt_ctxt i)

230 let ctxt' = setTotal cn tot (tt_ctxt i)

@@ -255,12 +256,10 @@ calcProd i fc topn pats

255

256

256 prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool

257 prodRec :: Name -> [Name] -> ([Name], Term, Term) -> Idris Bool

257 prodRec n done _ | n `elem` done = return True

258 prodRec n done _ | n `elem` done = return True

258− prodRec n done (_, _, tm) = prod n done False tm

259+ prodRec n done (_, _, tm) = prod n done False (delazy tm)

259

260

260 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool

261 prod :: Name -> [Name] -> Bool -> Term -> Idris Bool

261 prod n done ok ap@(App _ _)

262 prod n done ok ap@(App _ _)

262− | (P _ (UN l) _, [_, arg]) <- unApply ap,

263− l == txt "lazy" = prod n done ok arg

264 | (P nt f _, args) <- unApply ap

263 | (P nt f _, args) <- unApply ap

265 = do recOK <- checkProdRec (n:done) f

264 = do recOK <- checkProdRec (n:done) f

266 let ctxt = tt_ctxt i

265 let ctxt = tt_ctxt i

@@ -412,15 +411,25 @@ buildSCG (_, n) = do

412 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"

411 [] -> logLvl 5 $ "Could not build SCG for " ++ show n ++ "\n"

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

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

414

413

414+delazy t@(App f a)

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

416+ l == txt "Force" = delazy arg

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

418+ l == txt "Delay" = delazy arg

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

420+ l == txt "Lazy" = delazy arg

421+delazy (App f a) = App (delazy f) (delazy a)

422+delazy (Bind n b sc) = Bind n (fmap delazy b) (delazy sc)

423+delazy t = t

424+

415buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]

425buildSCG' :: IState -> [(Term, Term)] -> [Name] -> [SCGEntry]

416buildSCG' ist pats args = nub $ concatMap scgPat pats where

426buildSCG' ist pats args = nub $ concatMap scgPat pats where

427+ scgPat (lhs, rhs) = let lhs' = delazy lhs

428+ rhs' = delazy rhs

417− scgPat (lhs, rhs) = let (f, pargs) = unApply (dePat lhs) in

429+ (f, pargs) = unApply (dePat lhs') in

418− findCalls (dePat rhs) (patvars lhs) pargs

430+ findCalls (dePat rhs') (patvars lhs') pargs

419

431

420 findCalls ap@(App f a) pvs pargs

432 findCalls ap@(App f a) pvs pargs

421− | (P _ (UN l) _, [_, arg]) <- unApply ap,

422− l == txt "lazy"

423− = findCalls arg pvs pargs

424 -- under a call to "assert_total", don't do any checking, just believe

433 -- under a call to "assert_total", don't do any checking, just believe

425 -- that it is total.

434 -- that it is total.

426 | (P _ (UN at) _, [_, _]) <- unApply ap,

435 | (P _ (UN at) _, [_, _]) <- unApply ap,

@@ -480,7 +489,7 @@ buildSCG' ist pats args = nub $ concatMap scgPat pats where

480 toJust (n, t) = Just t

489 toJust (n, t) = Just t

481

490

482 getType n = case lookupTy n (tt_ctxt ist) of

491 getType n = case lookupTy n (tt_ctxt ist) of

483− [ty] -> ty -- must exist

492+ [ty] -> delazy ty -- must exist

484

493

485 isInductive (P _ nty _) (P _ nty' _) =

494 isInductive (P _ nty _) (P _ nty' _) =

486 let co = case lookupCtxt nty (idris_datatypes ist) of

495 let co = case lookupCtxt nty (idris_datatypes ist) of

src/Idris/ElabDecls.hs+8−1

@@ -858,9 +858,16 @@ elabCon info syn tn codata (doc, n, t_in, fc, forcenames)

858 tyIs t = tclift $ tfail (At fc (Msg (show t ++ " is not " ++ show tn)))

859

860 mkLazy (PPi pl n ty sc)

861− = PPi (pl { pargopts = nub (Lazy : pargopts pl) }) n ty (mkLazy sc)

861+ = let ty' = if getTyName ty

862+ then PApp fc (PRef fc (sUN "Lazy")) [pexp ty]

863+ else ty in

864+ PPi pl n ty' (mkLazy sc)

862 mkLazy t = t

865 mkLazy t = t

863

866

867+ getTyName (PApp _ (PRef _ n) _) = n == nsroot tn

868+ getTyName _ = False

869+

870+

864 getNamePos :: Int -> PTerm -> Name -> Maybe Int

871 getNamePos :: Int -> PTerm -> Name -> Maybe Int

865 getNamePos i (PPi _ n _ sc) x | n == x = Just i

872 getNamePos i (PPi _ n _ sc) x | n == x = Just i

866 | otherwise = getNamePos (i + 1) sc x

873 | otherwise = getNamePos (i + 1) sc x

src/Idris/ElabTerm.hs+38−10

@@ -165,7 +165,25 @@ elab ist info pattern opts fn tm

165-- ++ "\nproblems " ++ show ps

166-- ++ "\n-----------\n") $

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

168+ let fc = fileFC "Force"

169+ handleError forceErr

168− elab' ina t'

170+ (elab' ina t')

171+ (elab' ina (PApp fc (PRef fc (sUN "Force"))

172+ [pimp (sUN "a") Placeholder True,

173+ pexp ct])) True

174+

175+ forceErr (CantUnify _ t t' _ _ _)

176+ | (P _ (UN ht) _, _) <- unApply t,

177+ ht == txt "Lazy" = True

178+ forceErr (CantUnify _ t t' _ _ _)

179+ | (P _ (UN ht) _, _) <- unApply t',

180+ ht == txt "Lazy" = True

181+ forceErr (InfiniteUnify _ t _)

182+ | (P _ (UN ht) _, _) <- unApply t,

183+ ht == txt "Lazy" = True

184+ forceErr (Elaborating _ _ t) = forceErr t

185+ forceErr (At _ t) = forceErr t

186+ forceErr t = False

169

187

170 local f = do e <- get_env

188 local f = do e <- get_env

171 return (f `elem` map fst e)

189 return (f `elem` map fst e)

@@ -243,6 +261,7 @@ elab ist info pattern opts fn tm

243 ctxt <- get_context

261 ctxt <- get_context

244 let (tc, _) = unApply ty

262 let (tc, _) = unApply ty

245 let as' = pruneByType tc ctxt as

263 let as' = pruneByType tc ctxt as

264+-- trace (show as ++ "\n ==> " ++ showSep ", " (map showTmImpls as')) $

246 tryAll (zip (map (elab' ina) as') (map showHd as'))

265 tryAll (zip (map (elab' ina) as') (map showHd as'))

247 where showHd (PApp _ (PRef _ n) _) = show n

266 where showHd (PApp _ (PRef _ n) _) = show n

248 showHd (PRef _ n) = show n

267 showHd (PRef _ n) = show n

@@ -438,7 +457,9 @@ elab ist info pattern opts fn tm

438 let (ns', eargs) = unzip $

457 let (ns', eargs) = unzip $

439 sortBy cmpArg (zip ns args)

458 sortBy cmpArg (zip ns args)

440 elabArgs ist (ina || not isinf, guarded, inty)

459 elabArgs ist (ina || not isinf, guarded, inty)

460+ [] fc False f ns'

461+ (f == sUN "Force")

441− [] fc False f ns' (map (\x -> (lazyarg x, getTm x)) eargs)

462+ (map (\x -> (lazyarg x, getTm x)) eargs)

442 solve

463 solve

443 ivs' <- get_instances

464 ivs' <- get_instances

444 -- Attempt to resolve any type classes which have 'complete' types,

465 -- Attempt to resolve any type classes which have 'complete' types,

@@ -610,17 +631,20 @@ elab ist info pattern opts fn tm

610 getFC d x = d

631 getFC d x = d

611

632

612 insertLazy :: PTerm -> ElabD PTerm

633 insertLazy :: PTerm -> ElabD PTerm

613−-- insertLazy t | pattern = return t

614 insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t

634 insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Delay" = return t

635+ insertLazy t@(PApp _ (PRef _ (UN l)) _) | l == txt "Force" = return t

636+ insertLazy (PCoerced t) = return t

615 insertLazy t =

637 insertLazy t =

616 do ty <- goal

638 do ty <- goal

617 env <- get_env

639 env <- get_env

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

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

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

619 case tyh of

642 case tyh of

620 P _ (UN l) _ | l == txt "Lazy"

643 P _ (UN l) _ | l == txt "Lazy"

621− -> return (PAlternative False [t, mkDelay t])

644+ -> return (PAlternative False tries)

622 _ -> return t

645 _ -> return t

623 where

646 where

647+ mkDelay (PAlternative b xs) = PAlternative b (map mkDelay xs)

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

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

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

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

626

650

@@ -650,15 +674,16 @@ elab ist info pattern opts fn tm

650 -> Bool

674 -> Bool

651 -> Name -- ^ Name of the function being applied

675 -> Name -- ^ Name of the function being applied

652 -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

676 -> [(Name, Name)] -- ^ (Argument Name, Hole Name)

677+ -> Bool -- ^ under a 'force'

653 -> [(Bool, PTerm)] -- ^ (Laziness, argument)

678 -> [(Bool, PTerm)] -- ^ (Laziness, argument)

654 -> ElabD ()

679 -> ElabD ()

655− elabArgs ist ina failed fc retry f [] _

680+ elabArgs ist ina failed fc retry f [] force _

656-- | retry = let (ns, ts) = unzip (reverse failed) in

681-- | retry = let (ns, ts) = unzip (reverse failed) in

657-- elabArgs ina [] False ns ts

682-- elabArgs ina [] False ns ts

658 | otherwise = return ()

683 | otherwise = return ()

659− elabArgs ist ina failed fc r f (n:ns) ((_, Placeholder) : args)

684+ elabArgs ist ina failed fc r f (n:ns) force ((_, Placeholder) : args)

660− = elabArgs ist ina failed fc r f ns args

685+ = elabArgs ist ina failed fc r f ns force args

661− elabArgs ist ina failed fc r f ((argName, holeName):ns) ((lazy, t) : args)

686+ elabArgs ist ina failed fc r f ((argName, holeName):ns) force ((lazy, t) : args)

662 | lazy && not pattern

687 | lazy && not pattern

663 = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))

688 = elabArg argName holeName (PApp bi (PRef bi (sUN "lazy"))

664 [pimp (sUN "a") Placeholder True,

689 [pimp (sUN "a") Placeholder True,

@@ -668,12 +693,15 @@ elab ist info pattern opts fn tm

668 reflectFunctionErrors ist f argName $

693 reflectFunctionErrors ist f argName $

669 do hs <- get_holes

694 do hs <- get_holes

670 tm <- get_term

695 tm <- get_term

696+ -- No coercing under an explicit Force (or it can Force/Delay

697+ -- recursively!)

698+ let elab = if force then elab' else elabE

671 failed' <- -- trace (show (n, t, hs, tm)) $

699 failed' <- -- trace (show (n, t, hs, tm)) $

672 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

700 -- traceWhen (not (null cs)) (show ty ++ "\n" ++ showImp True t) $

673 case holeName `elem` hs of

701 case holeName `elem` hs of

674− True -> do focus holeName; elabE ina t; return failed

702+ True -> do focus holeName; elab ina t; return failed

675 False -> return failed

703 False -> return failed

676− elabArgs ist ina failed fc r f ns args

704+ elabArgs ist ina failed fc r f ns force args

677

705

678-- | Perform error reflection for function applicaitons with specific error handlers

706-- | Perform error reflection for function applicaitons with specific error handlers

679reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD a

707reflectFunctionErrors :: IState -> Name -> Name -> ElabD a -> ElabD a

src/Idris/ParseExpr.hs+4−3

@@ -780,9 +780,10 @@ Pi ::=

780

781pi :: SyntaxInfo -> IdrisParser PTerm

782pi syn =

783− do opts <- if implicitAllowed syn -- laziness is top level only

783+ do opts <- -- if implicitAllowed syn -- laziness is top level only

784− then option [] (do lchar '|'; return [Lazy])

784+ -- then option [] (do lchar '|'; return [Lazy])

785− else return []

785+ -- else return []

786+ return []

786 st <- static

787 st <- static

787 (do try(lchar '('); xt <- typeDeclList syn; lchar ')'

788 (do try(lchar '('); xt <- typeDeclList syn; lchar ')'

788 doc <- option "" (docComment '^')

789 doc <- option "" (docComment '^')

test/dsl001/test001.idr+5−4

@@ -26,7 +26,7 @@ using (G : Vect n Ty)

26 Var : HasType i G t -> Expr G t

27 Val : (x : Int) -> Expr G TyInt

28 Lam : Expr (a :: G) t -> Expr G (TyFun a t)

29− App : Expr G (TyFun a t) -> Expr G a -> Expr G t

29+ App : Lazy (Expr G (TyFun a t)) -> Expr G a -> Expr G t

30 Op : (interpTy a -> interpTy b -> interpTy c) -> Expr G a -> Expr G b ->

31 Expr G c

32 If : Expr G TyBool -> Expr G a -> Expr G a -> Expr G a

@@ -38,6 +38,7 @@ using (G : Vect n Ty)

38 index_first = stop

39 index_next = pop

40

41+ total

41 interp : Env G -> [static] (e : Expr G t) -> interpTy t

42 interp : Env G -> [static] (e : Expr G t) -> interpTy t

42 interp env (Var i) = lookup i env

43 interp env (Var i) = lookup i env

43 interp env (Val x) = x

44 interp env (Val x) = x

@@ -62,13 +63,13 @@ using (G : Vect n Ty)

62 eDouble : Expr G (TyFun TyInt TyInt)

63 eDouble : Expr G (TyFun TyInt TyInt)

63 eDouble = expr (\x => App (App eAdd x) (Var stop))

64 eDouble = expr (\x => App (App eAdd x) (Var stop))

64

65

65− app : |(f : Expr G (TyFun a t)) -> Expr G a -> Expr G t

66+-- app : Lazy (Expr G (TyFun a t)) -> Expr G a -> Expr G t

66− app = \f, a => App f a

67+-- app = \f, a => App (Force f) a

67

68

68 eFac : Expr G (TyFun TyInt TyInt)

69 eFac : Expr G (TyFun TyInt TyInt)

69 eFac = expr (\x => If (Op (==) x (Val 0))

70 eFac = expr (\x => If (Op (==) x (Val 0))

70 (Val 1)

71 (Val 1)

71− (Op (*) (app eFac (Op (-) x (Val 1))) x))

72+ (Op (*) (App eFac (Op (-) x (Val 1))) x))

72

73

73 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

74 -- Exercise elaborator: Complicated way of doing \x y => x*4 + y*2

74

75

test/dsl002/Resimp.idr+1−1

@@ -105,7 +105,7 @@ using (i: Fin n, gam : Vect n Ty, gam' : Vect n Ty, gam'' : Vect n Ty)

105

106{-- Control structures --}

107

108− Lift : |(action:IO a) -> Res gam gam (R a)

108+ Lift : IO a -> Res gam gam (R a)

109 Check : (p:HasType gam i (Choice (interpTy a) (interpTy b))) ->

110 (failure:Res (update gam p a) (update gam p c) t) ->

111 (success:Res (update gam p b) (update gam p c) t) ->

test/io001/test004.idr+1−1

@@ -1,6 +1,6 @@

1module Main

2

3−mwhile : |(test : IO Bool) -> |(body : IO ()) -> IO ()

3+mwhile : (test : IO Bool) -> (body : IO ()) -> IO ()

4mwhile t b = do v <- t

5 case v of

6 True => do b

test/io003/test018.idr+1−2

@@ -7,8 +7,7 @@ recvMsg : IO (Ptr, String)

7recvMsg = getMsg

8

9pong : IO ()

10−pong = do -- putStrLn "Waiting for ping"

11− (sender, x) <- recvMsg

10+pong = do (sender, x) <- recvMsg

12 putStrLn x

11 putStrLn x

13 putStrLn "Received"

12 putStrLn "Received"

14 sendToThread sender "Hello to you too!"

13 sendToThread sender "Hello to you too!"

test/reg018/reg018c.idr+1−1

@@ -10,7 +10,7 @@ codata InfStream a = (::) a (InfStream a)

10

11take : (n: Nat) -> InfStream a -> Vect n a

12take Z _ = []

13−take (S n) (x :: xs) = x :: take n xs

13+take (S n) (x :: xs) = x :: CodataTest.take n xs

14

15hdtl : InfStream a -> (a, InfStream a)

16hdtl (x :: xs) = (x, xs)