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

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

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

6262 where get : IO (Ptr, msg)

6363 get = getMsg

6464

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

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

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

6767 return (MkPID ptr)

6868

libs/effects/Effects.idr+1−2

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

262262 = let env' = dropEnv env prf in

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

264264eff 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')

267266eff env (test prf l r) k

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

269268eff env (test_lbl prf l r) k

libs/neweffects/Effects.idr+1−2

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

237237 = let env' = dropEnv env prf in

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

239239eff 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)

242241eff env (catch prog handler) k

243242 = catch (eff env prog k)

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

libs/prelude/Builtins.idr+2−2

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

3939Force : Lazy a -> a

4040Force (Delay x) = x

4141

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

43−par x = x -- compiled specially

42+par : Lazy a -> a

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

4444

4545malloc : Int -> a -> a

4646malloc size x = x -- compiled specially

libs/prelude/IO.idr+2−2

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

131131

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

133133

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

134+prim_fork : PrimIO () -> PrimIO Ptr

135135prim_fork x = prim_io_return prim__vm -- compiled specially

136136

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

137+fork : IO () -> IO Ptr

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

139139 (prim_fork (prim_io_bind (f w)

140140 (\ x => prim_io_return x)))

libs/prelude/Prelude.idr+1−1

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

550550 return (not x)

551551

552552partial -- obviously

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

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

554554while t b = do v <- t

555555 if v then do b

556556 while t b

libs/prelude/Prelude/Bits.idr+1

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

22

33import Prelude.Strings

44import Prelude.Vect

5+import Prelude.Bool

56

67%access public

78%default total

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

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

44data Bool = False | True

55

66-- | Boolean elimination

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

8−boolElim True t e = force t

9−boolElim False t e = force e

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

8+boolElim True t e = t

9+boolElim False t e = e

1010

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

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

1313

1414-- 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)

1616

1717-- Boolean Operator Precedence

1818infixl 4 &&, ||

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

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

2828-- Misc

2929--------------------------------------------------------------------------------

3030

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

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

3232maybe n j Nothing = n

3333maybe n j (Just x) = j x

3434

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

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

3636fromMaybe def Nothing = def

3737fromMaybe def (Just j) = j

3838

libs/prelude/Prelude/Vect.idr+2

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

44import Prelude.Foldable

55import Prelude.Functor

66import Prelude.List

7+import Prelude.Classes

78import Prelude.Nat

9+import Prelude.Bool

810

911%access public

1012%default total

src/IRTS/Compiler.hs+12−1

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

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

179179 r == txt "replace"

180180 = ir' env arg

181+ -- Laziness, the old way

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

182183 l == txt "lazy"

183184 = do arg' <- ir' env arg

184− return $ LLazyExp arg'

185+ error "lazy has crept in somehow"

186+-- return $ LLazyExp arg'

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

186188 l == txt "force"

187189 = do arg' <- ir' env arg

188190 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'

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

190201 a == txt "assert_smaller"

191202 = ir' env arg

src/Idris/CaseSplit.hs+4

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

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

322322 = let n = getNameFrom i used ty in

323323 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)

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

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

326330 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

150150

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

152152

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

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

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

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

156156 ++ directUse t

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

158158directUse 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

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

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

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

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

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

575581 case alts' of

576582 [] -> ImpossibleCase

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

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

578584 | delay == txt "Delay"

579585 -> if proj then mkForce n arg sc

580586 else Case n as

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

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

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

631631try t1 t2 = try' t1 t2 False

632632

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+

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

634649try' t1 t2 proofSearch

635650 = do s <- get

636651 ps <- get_probs

637652 case prunStateT 999999 False ps t1 s of

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

639− return $! v

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

654+ return $! v

640655 Error e1 -> if recoverableErr e1 then

641656 do case runStateT t2 s of

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

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

658673

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

660675tryAll :: [(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

662677 where

663678 cantResolve :: Elab' aux a

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

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

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

667682 Int -> -- most problems

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

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

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

670685 Elab' aux a

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

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

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

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

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

675690 = do s <- get

676691 ps <- get_probs

677692 case prunStateT pmax True ps x s of

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

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

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

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

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

682697 tryAll' cs' newps f xs

683698 Error err -> do put s

684− if (score err) < 100

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

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

699+-- if (score err) < 100

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

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

687702

688703

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

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

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

699714 then case reverse (problems p) of

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

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

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

702717 Error e -> Error e

703718

704719qshow :: Fails -> String

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

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

251251 | holeIn env x || x `elem` holes

252252 = do UI s f <- get

253253 -- injectivity check

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

254255 if (notP tm && fn)

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

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

257258 then unifyTmpFail xtm tm

258259 else do sc 1

259− checkCycle bnames (x, tm)

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

260+ return x

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

262+ = do checkCycle bnames (x, tm)

263+ unifyTmpFail xtm tm

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

262265 | holeIn env y || y `elem` holes

263266 = do UI s f <- get

264267 -- injectivity check

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

265269 if (notP tm && fn)

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

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

268272 then unifyTmpFail tm ytm

269273 else do sc 1

270− checkCycle bnames (y, tm)

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

274+ return x

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

276+ = do checkCycle bnames (y, tm)

277+ unifyTmpFail tm ytm

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

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

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

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

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

528534-- rethink overloading properly...

529535

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

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

531541 | x == y = True

532542 | otherwise = False

src/Idris/Coverage.hs+20−11

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

222222-- and update the context accordingly

223223

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

225−checkPositive n (cn, ty)

226− = do let p = cp ty

225+checkPositive n (cn, ty')

226+ = do let ty = delazy ty'

227+ let p = cp ty

227228 i <- getIState

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

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

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

255256

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

257258 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)

259260

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

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

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

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

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

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

266265 let ctxt = tt_ctxt i

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

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

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

414413

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+

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

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

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

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

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

428+ rhs' = delazy rhs

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

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

419431

420432 findCalls ap@(App f a) pvs pargs

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

422− l == txt "lazy"

423− = findCalls arg pvs pargs

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

425434 -- that it is total.

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

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

480489 toJust (n, t) = Just t

481490

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

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

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

484493

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

486495 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)

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

859859

860860 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)

862865 mkLazy t = t

863866

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

868+ getTyName _ = False

869+

870+

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

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

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

src/Idris/ElabTerm.hs+38−10

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

165165-- ++ "\nproblems " ++ show ps

166166-- ++ "\n-----------\n") $

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

168− elab' ina t'

168+ let fc = fileFC "Force"

169+ handleError forceErr

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

169187

170188 local f = do e <- get_env

171189 return (f `elem` map fst e)

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

243261 ctxt <- get_context

244262 let (tc, _) = unApply ty

245263 let as' = pruneByType tc ctxt as

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

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

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

248267 showHd (PRef _ n) = show n

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

438457 let (ns', eargs) = unzip $

439458 sortBy cmpArg (zip ns args)

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

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

460+ [] fc False f ns'

461+ (f == sUN "Force")

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

442463 solve

443464 ivs' <- get_instances

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

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

610631 getFC d x = d

611632

612633 insertLazy :: PTerm -> ElabD PTerm

613−-- insertLazy t | pattern = return t

614634 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

615637 insertLazy t =

616638 do ty <- goal

617639 env <- get_env

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

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

619642 case tyh of

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

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

644+ -> return (PAlternative False tries)

622645 _ -> return t

623646 where

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

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

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

626650

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

650674 -> Bool

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

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

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

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

654679 -> ElabD ()

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

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

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

657682-- elabArgs ina [] False ns ts

658683 | otherwise = return ()

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

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

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

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

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

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

662687 | lazy && not pattern

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

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

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

668693 reflectFunctionErrors ist f argName $

669694 do hs <- get_holes

670695 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

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

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

673701 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

675703 False -> return failed

676− elabArgs ist ina failed fc r f ns args

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

677705

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

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

src/Idris/ParseExpr.hs+4−3

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

780780

781781pi :: SyntaxInfo -> IdrisParser PTerm

782782pi syn =

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

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

785− else return []

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

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

785+ -- else return []

786+ return []

786787 st <- static

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

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

test/dsl001/test001.idr+5−4

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

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

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

2828 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

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

3131 Expr G c

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

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

3838 index_first = stop

3939 index_next = pop

4040

41+ total

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

4243 interp env (Var i) = lookup i env

4344 interp env (Val x) = x

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

6263 eDouble : Expr G (TyFun TyInt TyInt)

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

6465

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

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

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

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

6768

6869 eFac : Expr G (TyFun TyInt TyInt)

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

7071 (Val 1)

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

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

7273

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

7475

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)

105105

106106{-- Control structures --}

107107

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

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

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

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

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

test/io001/test004.idr+1−1

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

11module Main

22

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

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

44mwhile t b = do v <- t

55 case v of

66 True => do b

test/io003/test018.idr+1−2

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

77recvMsg = getMsg

88

99pong : IO ()

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

11− (sender, x) <- recvMsg

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

1211 putStrLn x

1312 putStrLn "Received"

1413 sendToThread sender "Hello to you too!"

test/reg018/reg018c.idr+1−1

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

1010

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

1212take Z _ = []

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

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

1414

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

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