1b53cc5 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improve mid-do-block cases

1b53cc5Edwin Brady13 years ago

src/Idris/Core/Evaluate.hs+1−1

compare with master

unifiedsplit

@@ -268,7 +268,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

268-- tfull' <- reapply ntimes stk top env t' []

269 return (doProj t' (getValArgs t'))

270 where doProj t' (VP (DCon _ _) _ _, args)

271− | i >=0 && i < length args = args!!i

271+ | i >= 0 && i < length args = args!!i

272 doProj t' _ = VProj t' i

273

274 ev ntimes stk top env (Constant c) = return $ VConstant c

src/Idris/ElabDecls.hs+23

@@ -1274,6 +1274,9 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1274 (erun fc (build i info False fname rhs))

1275 errAt "right hand side of " fname

1276 (erun fc $ psolve lhs_tm)

1277+ hs <- get_holes

1278+ aux <- getAux

1279+ mapM_ (elabCaseHole aux) hs

1277 tt <- get_term

1280 tt <- get_term

1278 let (tm, ds) = runState (collectDeferred (Just fname) tt) []

1281 let (tm, ds) = runState (collectDeferred (Just fname) tt) []

1279 return (tm, ds, is))

1282 return (tm, ds, is))

@@ -1371,6 +1374,26 @@ elabClause info opts (cnum, PClause fc fname lhs_in withs rhs_in whereblock)

1371 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

1374 = PApp fc (PRef fc n) (map (\x -> pimp x (PRef fc x) True) ps)

1372 propagateParams ps x = x

1375 propagateParams ps x = x

1373

1376

1377+ -- if a hole is just an argument/result of a case block, treat it as

1378+ -- the unit type. Hack to help elaborate case in do blocks.

1379+ elabCaseHole aux h = do

1380+ focus h

1381+ g <- goal

1382+ case g of

1383+ TType _ -> when (any (isArg h) aux) $ do apply (Var unitTy) []; solve

1384+ _ -> return ()

1385+

1386+ -- Is the name a pattern argument in the declaration

1387+ isArg :: Name -> PDecl -> Bool

1388+ isArg n (PClauses _ _ _ cs) = any isArg' cs

1389+ where

1390+ isArg' (PClause _ _ (PApp _ _ args) _ _ _)

1391+ = any (\x -> case x of

1392+ PRef _ n' -> n == n'

1393+ _ -> False) (map getTm args)

1394+ isArg' _ = False

1395+ isArg _ _ = False

1396+

1374elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1397elabClause info opts (_, PWith fc fname lhs_in withs wval_in withblock)

1375 = do let tcgen = Dictionary `elem` opts

1398 = do let tcgen = Dictionary `elem` opts

1376 ctxt <- getContext

1399 ctxt <- getContext