0fbfeab · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Improve pruning of alternatives

0fbfeabEdwin Brady11 years ago

src/Idris/AbsSyntax.hs+3−1

compare with master

unifiedsplit

@@ -2120,6 +2120,7 @@ shadow n n' t = sm t where

2120 sm (PHidden x) = PHidden (sm x)

2121 sm (PUnifyLog x) = PUnifyLog (sm x)

2122 sm (PNoImplicits x) = PNoImplicits (sm x)

2123+ sm (PCoerced t) = PCoerced (sm t)

2123 sm x = x

2124 sm x = x

2124

2125

2125-- | Rename any binders which are repeated (so that we don't have to mess

2126-- | Rename any binders which are repeated (so that we don't have to mess

@@ -2231,7 +2232,8 @@ mkUniqueNames env shadows tm

2231 mkUniq nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT nmap) ts)

2232 mkUniq nmap (PTactics ts) = liftM PTactics (mapM (mkUniqT nmap) ts)

2232 mkUniq nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq nmap ts)

2233 mkUniq nmap (PRunElab fc ts ns) = liftM (\tm -> PRunElab fc tm ns) (mkUniq nmap ts)

2233 mkUniq nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq nmap tm)

2234 mkUniq nmap (PConstSugar fc tm) = liftM (PConstSugar fc) (mkUniq nmap tm)

2235+ mkUniq nmap (PCoerced tm) = liftM PCoerced (mkUniq nmap tm)

2234− mkUniq nmap t = return (shadowAll (M.toList nmap) t)

2236+ mkUniq nmap t = return $ shadowAll (M.toList nmap) t

2235 where

2237 where

2236 shadowAll [] t = t

2238 shadowAll [] t = t

2237 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)

2239 shadowAll ((n, n') : ns) t = shadow n n' (shadowAll ns t)

src/Idris/Elab/Term.hs+30−15

@@ -442,6 +442,7 @@ elab ist info emode opts fn tm

442-- trace (show (map showHd as')) $

443 ty <- goal

444 case as' of

445+ [] -> lift $ tfail $ NoValidAlts (map showHd as)

445 [x] -> elab' ina fc x

446 [x] -> elab' ina fc x

446 -- If there's options, try now, and if that fails, postpone

447 -- If there's options, try now, and if that fails, postpone

447 -- to later.

448 -- to later.

@@ -458,18 +459,24 @@ elab ist info emode opts fn tm

458 [x] -> elab' ina fc x

459 [x] -> elab' ina fc x

459 _ -> tryAll (zip (map (elab' ina fc) as'')

460 _ -> tryAll (zip (map (elab' ina fc) as'')

460 (map showHd as'')))

461 (map showHd as'')))

461− where showHd (PApp _ (PRef _ _ n) _) = n

462+ where showHd (PApp _ (PRef _ _ (UN l)) [_, _, arg])

463+ | l == txt "Delay" = showHd (getTm arg)

464+ showHd (PApp _ (PRef _ _ n) _) = n

462 showHd (PRef _ _ n) = n

465 showHd (PRef _ _ n) = n

463 showHd (PApp _ h _) = showHd h

466 showHd (PApp _ h _) = showHd h

464 showHd x = NErased -- We probably should do something better than this here

467 showHd x = NErased -- We probably should do something better than this here

465

468

466 doPrune as =

469 doPrune as =

467− do hnf_compute

470+ do compute

468 ty <- goal

471 ty <- goal

469− let (tc, _) = unApply ty

472+ let (tc, _) = unApply (unDelay ty)

470 env <- get_env

473 env <- get_env

471 return $ pruneByType env tc ist as

474 return $ pruneByType env tc ist as

472

475

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

477+ l == txt "Lazy'" = unDelay arg

478+ | otherwise = t

479+

473

480

474 isAmbiguous (CantResolveAlts _) = delayok

481 isAmbiguous (CantResolveAlts _) = delayok

475 isAmbiguous (Elaborating _ _ e) = isAmbiguous e

482 isAmbiguous (Elaborating _ _ e) = isAmbiguous e

@@ -492,20 +499,21 @@ elab ist info emode opts fn tm

492 solveAutos ist fn False) (trySeq' deferr xs) True

499 solveAutos ist fn False) (trySeq' deferr xs) True

493 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do

500 elab' ina fc (PAlternative ms TryImplicit (orig : alts)) = do

494 env <- get_env

501 env <- get_env

502+ compute

495 ty <- goal

503 ty <- goal

496 let doelab = elab' ina fc orig

504 let doelab = elab' ina fc orig

497 tryCatch doelab

505 tryCatch doelab

498 (\err ->

506 (\err ->

499 if recoverableErr err

507 if recoverableErr err

500 then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++

508 then -- trace ("NEED IMPLICIT! " ++ show orig ++ "\n" ++

501− -- show alts ++ "\n" ++

509+ -- show alts ++ "\n" ++

502− -- showQuick err) $

510+ -- showQuick err) $

503 -- Prune the coercions so that only the ones

511 -- Prune the coercions so that only the ones

504 -- with the right type to fix the error will be tried!

512 -- with the right type to fix the error will be tried!

505 case pruneAlts err alts env of

513 case pruneAlts err alts env of

506 [] -> lift $ tfail err

514 [] -> lift $ tfail err

507− alts' ->

515+ alts' -> do

508− try' (elab' ina fc (PAlternative [] (ExactlyOne False) alts'))

516+ try' (elab' ina fc (PAlternative ms (ExactlyOne False) alts'))

509 (lift $ tfail err) -- take error from original if all fail

517 (lift $ tfail err) -- take error from original if all fail

510 True

518 True

511 else lift $ tfail err)

519 else lift $ tfail err)

@@ -529,8 +537,8 @@ elab ist info emode opts fn tm

529 _ -> filter isLend alts -- special case hack for 'Borrowed'

537 _ -> filter isLend alts -- special case hack for 'Borrowed'

530 pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env

538 pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env

531 pruneAlts (At _ e) alts env = pruneAlts e alts env

539 pruneAlts (At _ e) alts env = pruneAlts e alts env

532− pruneAlts (NoValidAlts _) alts env = alts

540+ pruneAlts (NoValidAlts as) alts env = alts

533− pruneAlts _ alts _ = filter isLend alts

541+ pruneAlts err alts _ = filter isLend alts

534

542

535 hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'

543 hasArg n env ap | isLend ap = True -- special case hack for 'Borrowed'

536 hasArg n env (PApp _ (PRef _ _ a) _)

544 hasArg n env (PApp _ (PRef _ _ a) _)

@@ -538,7 +546,8 @@ elab ist info emode opts fn tm

538 Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in

546 Just ty -> let args = map snd (getArgTys (normalise (tt_ctxt ist) env ty)) in

539 any (fnIs n) args

547 any (fnIs n) args

540 Nothing -> False

548 Nothing -> False

541− hasArg n _ _ = False

549+ hasArg n env (PAlternative _ _ as) = any (hasArg n env) as

550+ hasArg n _ tm = False

542

551

543 isLend (PApp _ (PRef _ _ l) _) = l == sNS (sUN "lend") ["Ownership"]

552 isLend (PApp _ (PRef _ _ l) _) = l == sNS (sUN "lend") ["Ownership"]

544 isLend _ = False

553 isLend _ = False

@@ -1376,7 +1385,7 @@ elab ist info emode opts fn tm

1376 notImplicitable (PRef _ _ n)

1385 notImplicitable (PRef _ _ n)

1377 | [opts] <- lookupCtxt n (idris_flags ist)

1386 | [opts] <- lookupCtxt n (idris_flags ist)

1378 = NoImplicit `elem` opts

1387 = NoImplicit `elem` opts

1379− notImplicitable (PAlternative _ (ExactlyOne _) as) = any notImplicitable as

1388+ notImplicitable (PAlternative _ _ as) = any notImplicitable as

1380 -- case is tricky enough without implicit coercions! If they are needed,

1389 -- case is tricky enough without implicit coercions! If they are needed,

1381 -- they can go in the branches separately.

1390 -- they can go in the branches separately.

1382 notImplicitable (PCase _ _ _) = True

1391 notImplicitable (PCase _ _ _) = True

@@ -1420,9 +1429,11 @@ elab ist info emode opts fn tm

1420 (PCoerced tm, _) -> tm

1429 (PCoerced tm, _) -> tm

1421 (_, []) -> t

1430 (_, []) -> t

1422 (_, cs) -> PAlternative [] TryImplicit

1431 (_, cs) -> PAlternative [] TryImplicit

1423− (t : map (mkCoerce env t) cs)

1432+ (t : map (mkCoerce env t) cs)

1424 return t'

1433 return t'

1425 where

1434 where

1435+ mkCoerce env (PAlternative ms aty tms) n

1436+ = PAlternative ms aty (map (\t -> mkCoerce env t n) tms)

1426 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

1437 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

1427 addImplBound ist (map fst env)

1438 addImplBound ist (map fst env)

1428 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

1439 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

@@ -1520,6 +1531,8 @@ pruneByType env t c as

1520 n `elem` map fst env = Just t

1531 n `elem` map fst env = Just t

1521 | otherwise = locallyBound ts

1532 | otherwise = locallyBound ts

1522 getName (PRef _ _ n) = Just n

1533 getName (PRef _ _ n) = Just n

1534+ getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays

1535+ | l == txt "Delay" = getName (getTm arg)

1523 getName (PApp _ f _) = getName f

1536 getName (PApp _ f _) = getName f

1524 getName (PHidden t) = getName t

1537 getName (PHidden t) = getName t

1525 getName _ = Nothing

1538 getName _ = Nothing

@@ -1528,18 +1541,20 @@ pruneByType env t c as

1528pruneByType env (P _ n _) ist as

1541pruneByType env (P _ n _) ist as

1529-- if the goal type is polymorphic, keep everything

1542-- if the goal type is polymorphic, keep everything

1530 | Nothing <- lookupTyExact n ctxt = as

1543 | Nothing <- lookupTyExact n ctxt = as

1544+-- if the goal type is a ?metavariable, keep everything

1545+ | Just _ <- lookup n (idris_metavars ist) = as

1531 | otherwise

1546 | otherwise

1532 = let asV = filter (headIs True n) as

1547 = let asV = filter (headIs True n) as

1533 as' = filter (headIs False n) as in

1548 as' = filter (headIs False n) as in

1534 case as' of

1549 case as' of

1535− [] -> case asV of

1536− [] -> as

1537− _ -> asV

1550+ [] -> asV

1538 _ -> as'

1551 _ -> as'

1539 where

1552 where

1540 ctxt = tt_ctxt ist

1553 ctxt = tt_ctxt ist

1541

1554

1542 headIs var f (PRef _ _ f') = typeHead var f f'

1555 headIs var f (PRef _ _ f') = typeHead var f f'

1556+ headIs var f (PApp _ (PRef _ _ (UN l)) [_, _, arg])

1557+ | l == txt "Delay" = headIs var f (getTm arg)

1543 headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'

1558 headIs var f (PApp _ (PRef _ _ f') _) = typeHead var f f'

1544 headIs var f (PApp _ f' _) = headIs var f f'

1559 headIs var f (PApp _ f' _) = headIs var f f'

1545 headIs var f (PPi _ _ _ _ sc) = headIs var f sc

1560 headIs var f (PPi _ _ _ _ sc) = headIs var f sc

src/Idris/Elab/Type.hs+1

@@ -64,6 +64,7 @@ buildType info syn fc opts n ty' = do

64 let ty = addImpl (imp_methods syn) i ty'

66 logLvl 5 $ show n ++ " type pre-addimpl " ++ showTmImpls ty'

67+ logLvl 5 $ show "with methods " ++ show (imp_methods syn)

67 logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

68 logLvl 2 $ show n ++ " type " ++ show (using syn) ++ "\n" ++ showTmImpls ty

69 (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-

70 (ElabResult tyT' defer is ctxt' newDecls highlights, log) <-

test/effects001/test021.idr+2−1

@@ -23,7 +23,8 @@ readFile = readAcc [] where

24testFile : FileIO () ()

25testFile = do True <- open "testFile" Read | False => putStrLn "Error!"

26+ fcontents <- readFile

26− putStrLn (show !readFile)

27+ putStrLn (show fcontents)

27 close

28 close

28 putStrLn (show !(Count :- get))

29 putStrLn (show !(Count :- get))