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

git.iko.soy/Idris-dev

on master help sign in

Restrict (and speed up) implicit coercions

0dd2f06Edwin Brady11 years ago

src/Idris/AbsSyntaxTree.hs+1

compare with master

unifiedsplit

@@ -877,6 +877,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the high-level langua

877

878data PAltType = ExactlyOne Bool -- ^ flag sets whether delay is allowed

879 | FirstSuccess

880+ | TryImplicit

880 deriving (Eq, Data, Typeable)

881 deriving (Eq, Data, Typeable)

881

882

882-- | Transform the FCs in a PTerm. The first function transforms the

883-- | Transform the FCs in a PTerm. The first function transforms the

src/Idris/Core/Elaborate.hs+5−3

@@ -812,9 +812,10 @@ tryCatch t1 t2

812 = do s <- get

813 ps <- get_probs

814 ulog <- getUnifyLog

815− case prunStateT 999999 False ps t1 s of

815+-- case prunStateT 999999 False ps t1 s of

816+ case runStateT t1 s of

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

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

817− return $! v

818+ return $! v

818 Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

819 Error e1 -> traceWhen ulog ("tryCatch failed " ++ show e1) $

819 case runStateT (t2 e1) s of

820 case runStateT (t2 e1) s of

820 OK (v, s') -> do put s'

821 OK (v, s') -> do put s'

@@ -863,6 +864,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

863 if (s >= i) then (lift (tfail err), s)

864 if (s >= i) then (lift (tfail err), s)

864 else (f, i)

865 else (f, i)

865

866

867+-- Run an elaborator, and fail if any problems are introduced

866prunStateT

868prunStateT

867 :: Int

869 :: Int

868 -> Bool

870 -> Bool

src/Idris/Elab/Term.hs+62−3

@@ -479,6 +479,66 @@ elab ist info emode opts fn tm

479 trySeq' deferr (x : xs)

480 = try' (do elab' ina fc x

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

482+ elab' ina fc (PAlternative TryImplicit (orig : alts)) = do

483+ env <- get_env

484+ let doelab = elab' ina fc orig

485+ tryCatch doelab

486+ (\err ->

487+ if recoverableErr err

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

489+ -- show alts ++ "\n" ++

490+ -- showQuick err) $

491+ -- Prune the coercions so that only the ones

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

493+ case pruneAlts err alts env of

494+ [] -> lift $ tfail err

495+ alts' ->

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

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

498+ True

499+ else lift $ tfail err)

500+ where

501+ recoverableErr (CantUnify _ _ _ _ _ _) = True

502+ recoverableErr (CantSolveGoal _ _) = False

503+ recoverableErr (CantResolveAlts _) = False

504+ recoverableErr (ProofSearchFail (Msg _)) = True

505+ recoverableErr (ProofSearchFail _) = False

506+ recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

507+ recoverableErr (At _ e) = recoverableErr e

508+ recoverableErr (ElabScriptDebug _ _ _) = False

509+ recoverableErr _ = True

510+

511+ pruneAlts (CantUnify _ (inc, _) (outc, _) _ _ _) alts env

512+ = case unApply (normalise (tt_ctxt ist) env inc) of

513+ (P (TCon _ _) n _, _) -> filter (hasArg n env) alts

514+ (Constant _, _) -> alts

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

516+ pruneAlts (ElaboratingArg _ _ _ e) alts env = pruneAlts e alts env

517+ pruneAlts (At _ e) alts env = pruneAlts e alts env

518+ pruneAlts _ alts _ = filter isLend alts

519+

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

521+ hasArg n env (PApp _ (PRef _ a) _)

522+ = case lookupTyExact a (tt_ctxt ist) of

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

524+ any (fnIs n) args

525+ Nothing -> False

526+ hasArg n _ _ = False

527+

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

529+ isLend _ = False

530+

531+ fnIs n ty = case unApply ty of

532+ (P _ n' _, _) -> n == n'

533+ _ -> False

534+

535+ showQuick (CantUnify _ (l, _) (r, _) _ _ _)

536+ = show (l, r)

537+ showQuick (ElaboratingArg _ _ _ e) = showQuick e

538+ showQuick (At _ e) = showQuick e

539+ showQuick (ProofSearchFail (Msg _)) = "search fail"

540+ showQuick _ = "No chance"

541+

482 elab' ina _ (PPatvar fc n) | bindfree

542 elab' ina _ (PPatvar fc n) | bindfree

483 = do patvar n

543 = do patvar n

484 update_term liftPats

544 update_term liftPats

@@ -1299,9 +1359,8 @@ elab ist info emode opts fn tm

1299 let t' = case (t, cs) of

1359 let t' = case (t, cs) of

1300 (PCoerced tm, _) -> tm

1360 (PCoerced tm, _) -> tm

1301 (_, []) -> t

1361 (_, []) -> t

1302− (_, cs) -> PAlternative FirstSuccess [t ,

1362+ (_, cs) -> PAlternative TryImplicit

1303− PAlternative (ExactlyOne False)

1304− (map (mkCoerce env t) cs)]

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

1305 return t'

1364 return t'

1306 where

1365 where

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

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

src/Idris/IBC.hs+2

@@ -1801,12 +1801,14 @@ instance Binary PAltType where

1801 ExactlyOne x1 -> do putWord8 0

1802 put x1

1803 FirstSuccess -> putWord8 1

1804+ TryImplicit -> putWord8 2

1804 get

1805 get

1805 = do i <- getWord8

1806 = do i <- getWord8

1806 case i of

1807 case i of

1807 0 -> do x1 <- get

1808 0 -> do x1 <- get

1808 return (ExactlyOne x1)

1809 return (ExactlyOne x1)

1809 1 -> return FirstSuccess

1810 1 -> return FirstSuccess

1811+ 2 -> return TryImplicit

1810 _ -> error "Corrupted binary data for PAltType"

1812 _ -> error "Corrupted binary data for PAltType"

1811

1813

1812

1814