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

git.iko.soy/Idris-dev

Improve mid-do-block cases

By assuming that any missing type is () (which is probably what was intended anyway). This works by filling any holes with () if they happen to be patterns in generated case blocks.

commit1b53cc58fb33fb451ba348e2f19d057bfaf69934 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 6 Jan 2014, 22:58 (13 years ago) parent7e2c212

2 files changed+24−1

compare with master

unifiedsplit

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

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

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

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

269269 return (doProj t' (getValArgs t'))

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

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

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

272272 doProj t' _ = VProj t' i

273273

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

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

12751275 errAt "right hand side of " fname

12761276 (erun fc $ psolve lhs_tm)

1277+ hs <- get_holes

1278+ aux <- getAux

1279+ mapM_ (elabCaseHole aux) hs

12771280 tt <- get_term

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

12791282 return (tm, ds, is))

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

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

13721375 propagateParams ps x = x

13731376

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+

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

13751398 = do let tcgen = Dictionary `elem` opts

13761399 ctxt <- getContext