e1c79ef · Idris-dev · git.iko.soy

libs/base/Language/Reflection/Utils.idr+1

compare with master

unifiedsplit

@@ -302,6 +302,7 @@ instance Show Err where

302 showPrec d (CantResolve tm) = showCon d "CantResolve" $ showArg tm

303 showPrec d (InvalidTCArg n tm) = showCon d "InvalidTCName" $ showArg n ++ showArg tm

304 showPrec d (CantResolveAlts xs) = showCon d "CantResolveAlts" $ showArg xs

305+ showPrec d (NoValidAlts xs) = showCon d "NoValidAlts" $ showArg xs

305 showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm

306 showPrec d (IncompleteTerm tm) = showCon d "IncompleteTerm" $ showArg tm

306 showPrec d (NoEliminator s tm) = showCon d "NoEliminator" $ showArg s ++ showArg tm

307 showPrec d (NoEliminator s tm) = showCon d "NoEliminator" $ showArg s ++ showArg tm

307 showPrec d UniverseError = "UniverseError"

308 showPrec d UniverseError = "UniverseError"

libs/prelude/Language/Reflection/Errors.idr+1

@@ -31,6 +31,7 @@ data Err = Msg String

31 | CantResolve TT

32 | InvalidTCArg TTName TT

33 | CantResolveAlts (List TTName)

34+ | NoValidAlts (List TTName)

34 | IncompleteTerm TT

35 | IncompleteTerm TT

35 | NoEliminator String TT

36 | NoEliminator String TT

36 | UniverseError

37 | UniverseError

src/Idris/Core/Binary.hs+3

@@ -184,6 +184,8 @@ instance Binary a => Binary (Err' a) where

184 put (UnknownImplicit n f) = do putWord8 40

185 put n

186 put f

187+ put (NoValidAlts ns) = do putWord8 41

188+ put ns

187

189

188 get = do i <- getWord8

190 get = do i <- getWord8

189 case i of

191 case i of

@@ -253,6 +255,7 @@ instance Binary a => Binary (Err' a) where

253 return (ElabScriptStuck x1)

255 return (ElabScriptStuck x1)

254 40 -> do x <- get ; y <- get

256 40 -> do x <- get ; y <- get

255 return $ UnknownImplicit x y

257 return $ UnknownImplicit x y

258+ 41 -> fmap NoValidAlts get

256 _ -> error "Corrupted binary data for Err'"

259 _ -> error "Corrupted binary data for Err'"

257----- Generated by 'derive'

260----- Generated by 'derive'

258

261

src/Idris/Core/DeepSeq.hs+1

@@ -93,6 +93,7 @@ instance NFData Err where

93 rnf (CantResolve x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

94 rnf (InvalidTCArg x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

95 rnf (CantResolveAlts x1) = rnf x1 `seq` ()

96+ rnf (NoValidAlts x1) = rnf x1 `seq` ()

96 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

97 rnf (IncompleteTerm x1) = rnf x1 `seq` ()

97 rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

98 rnf (NoEliminator x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

98 rnf (UniverseError x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

99 rnf (UniverseError x1 x2 x3 x4 x5) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` ()

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

@@ -806,7 +806,7 @@ try' t1 t2 proofSearch

806 = -- traceWhen r (show err) $

807 r || proofSearch

808 recoverableErr (CantSolveGoal _ _) = False

809− recoverableErr (CantResolveAlts _) = False

809+ recoverableErr (CantResolveAlts _) = proofSearch

810 recoverableErr (ProofSearchFail (Msg _)) = True

811 recoverableErr (ProofSearchFail _) = False

812 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

@@ -844,6 +844,9 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

844 cantResolve :: Elab' aux a

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

846

847+ noneValid :: Elab' aux a

848+ noneValid = lift $ tfail $ NoValidAlts (map snd xs)

849+

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

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

848 Int -> -- most problems

851 Int -> -- most problems

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

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

@@ -851,7 +854,7 @@ tryAll xs = tryAll' [] 999999 (cantResolve, 0) xs

851 Elab' aux a

854 Elab' aux a

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

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

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

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

854− tryAll' [] pmax (f, _) [] = f

857+ tryAll' [] pmax (f, _) [] = noneValid

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

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

856 = do s <- get

859 = do s <- get

857 ps <- get_probs

860 ps <- get_probs

src/Idris/Core/TT.hs+2

@@ -266,6 +266,7 @@ data Err' t

266 t

267 | InvalidTCArg Name t

268 | CantResolveAlts [Name]

269+ | NoValidAlts [Name]

269 | IncompleteTerm t

270 | IncompleteTerm t

270 | NoEliminator String t

271 | NoEliminator String t

271 | UniverseError FC UExp (Int, Int) (Int, Int) [ConstraintFC]

272 | UniverseError FC UExp (Int, Int) (Int, Int) [ConstraintFC]

@@ -360,6 +361,7 @@ instance Sized Err where

360score :: Err -> Int

361score :: Err -> Int

361score (CantUnify _ _ _ m _ s) = 1 + s + score m

362score (CantUnify _ _ _ m _ s) = 1 + s + score m

362score (CantResolve _ _) = 20

363score (CantResolve _ _) = 20

364+score (NoValidAlts _) = 0

363score (NoSuchVariable _) = 1000

365score (NoSuchVariable _) = 1000

364score (ProofSearchFail e) = score e

366score (ProofSearchFail e) = score e

365score (CantSolveGoal _ _) = 100000

367score (CantSolveGoal _ _) = 100000

src/Idris/Delaborate.hs+2

@@ -344,6 +344,8 @@ pprintErr' i (InvalidTCArg n t)

344 text "(Type class arguments must be injective)"

345pprintErr' i (CantResolveAlts as) = text "Can't disambiguate name:" <+>

346 align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i True) . annName) as)))

347+pprintErr' i (NoValidAlts as) = text "Can't disambiguate since no alternative is valid:" <+>

348+ indented (align (cat (punctuate (comma <> space) (map (fmap (fancifyAnnots i True) . annName) as))))

347pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

349pprintErr' i (NoTypeDecl n) = text "No type declaration for" <+> annName n

348pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

350pprintErr' i (NoSuchVariable n) = text "No such variable" <+> annName n

349pprintErr' i (WithFnType ty) =

351pprintErr' i (WithFnType ty) =

src/Idris/Elab/Term.hs+8

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

512 recoverableErr (TooManyArguments _) = False

513 recoverableErr (CantSolveGoal _ _) = False

514 recoverableErr (CantResolveAlts _) = False

515+ recoverableErr (NoValidAlts _) = True

515 recoverableErr (ProofSearchFail (Msg _)) = True

516 recoverableErr (ProofSearchFail (Msg _)) = True

516 recoverableErr (ProofSearchFail _) = False

517 recoverableErr (ProofSearchFail _) = False

517 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

518 recoverableErr (ElaboratingArg _ _ _ e) = recoverableErr e

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

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

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

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

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

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

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

530+ pruneAlts (NoValidAlts _) alts env = alts

529 pruneAlts _ alts _ = filter isLend alts

531 pruneAlts _ alts _ = filter isLend alts

530

532

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

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

@@ -1377,6 +1379,12 @@ elab ist info emode opts fn tm

1377 (t : map (mkCoerce env t) cs)

1379 (t : map (mkCoerce env t) cs)

1378 return t'

1380 return t'

1379 where

1381 where

1382+-- mkCoerce env (PAlternative ns aty alts@(a : as)) n

1383+-- = let fc = maybe (fileFC "Coercion") id (highestFC a) in

1384+-- addImplBound ist (map fst env)

1385+-- (PAlternative ns aty

1386+-- (map (\t -> PApp fc (PRef fc n) [pexp (PCoerced t)])

1387+-- alts))

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

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

1381 addImplBound ist (map fst env)

1389 addImplBound ist (map fst env)

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

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

test/dsl004/Door1.idr+2−2

@@ -30,8 +30,8 @@ action : DoorCmd a -> DoorLang a

30action = Action

31

32testProg : DoorH CLOSED -> DoorLang ()

33−testProg h = do h <- Knock h

33+testProg h = with Main, Show do -- h <- Knock h

34 h <- Open h

35− h <- Close h

35+ -- h <- Close h

36 Return ()

37