62a3eba · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Improve the "...is not solved" internal error to display something useful

Fixes #361 Fixes #321

commit62a3eba03304e6fdd4d680f05c2e27172fd488cc authorEdwin Brady <ecb10@st-andrews.ac.uk> dateMon 8 Jul 2013, 01:23 (13 years ago) parent006c8f2

5 files changed+19−15

compare with master

unifiedsplit

src/Core/Elaborate.hs+10−13 src/Core/ProofState.hs+2−1 src/Core/TT.hs+2 src/Idris/Delaborate.hs+2 src/Idris/ElabTerm.hs+3−1

src/Core/Elaborate.hs+10−13

@@ -501,8 +501,8 @@ checkPiGoal n

501501 solve

502502 focus f

503503

504−simple_app :: Elab' aux () -> Elab' aux () -> Elab' aux ()

505−simple_app fun arg =

504+simple_app :: Elab' aux () -> Elab' aux () -> String -> Elab' aux ()

505+simple_app fun arg appstr =

506506 do a <- unique_hole (MN 0 "argTy")

507507 b <- unique_hole (MN 0 "retTy")

508508 f <- unique_hole (MN 0 "f")

@@ -514,24 +514,21 @@ simple_app fun arg =

514514 start_unify s

515515 claim s (Var a)

516516 prep_fill f [s]

517− -- try elaborating in both orders, since we might learn something useful

518− -- either way

519−-- try (do focus s; arg

520−-- focus f; fun)

521−-- (do focus f; fun

522−-- focus s; arg)

523517 focus f; fun

524518 focus s; arg

525519 tm <- get_term

526520 ps <- get_probs

527521 complete_fill

528522 hs <- get_holes

529− -- We don't need a and b in the hole queue any more since they were just for

530− -- checking f, so discard them if they are still there. If they haven't been solved,

531− -- regret will fail

532− when (a `elem` hs) $ do focus a; regret

533− when (b `elem` hs) $ do focus b; regret

523+ env <- get_env

524+ -- We don't need a and b in the hole queue any more since they were

525+ -- just for checking f, so discard them if they are still there.

526+ -- If they haven't been solved, regret will fail

527+ when (a `elem` hs) $ do focus a; regretWith (CantInferType appstr)

528+ when (b `elem` hs) $ do focus b; regretWith (CantInferType appstr)

534529 end_unify

530+ where regretWith err = try regret

531+ (lift $ tfail err)

535532

536533-- Abstract over an argument of unknown type, giving a name for the hole

537534-- which we'll fill with the argument type too.

src/Core/ProofState.hs+2−1

@@ -363,7 +363,8 @@ regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

363363 do action (\ps -> let hs = holes ps in

364364 ps { holes = hs \\ [x] })

365365 return sc

366−regret ctxt env (Bind x (Hole t) _) = fail $ show x ++ " : " ++ show t ++ " is not solved"

366+regret ctxt env (Bind x (Hole t) _)

367+ = fail $ show x ++ " : " ++ show t ++ " is not solved..."

367368

368369exact :: Raw -> RunTactic

369370exact guess ctxt env (Bind x (Hole ty) sc) =

src/Core/TT.hs+2

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

6060 -- unification succeed

6161 | InfiniteUnify Name Term [(Name, Type)]

6262 | CantConvert Term Term [(Name, Type)]

63+ | CantInferType String

6364 | NonFunctionType Term Term

6465 | CantIntroduce Term

6566 | NoSuchVariable Name

@@ -103,6 +104,7 @@ score (CantUnify _ _ _ m _ s) = s + score m

103104score (CantResolve _) = 20

104105score (NoSuchVariable _) = 1000

105106score (ProofSearchFail _) = 10000

107+score (InternalMsg _) = -1

106108score _ = 0

107109

108110instance Show Err where

src/Idris/Delaborate.hs+2

@@ -112,6 +112,8 @@ pshow i (CantConvert x y env)

112112 "Can't convert " ++ showImp imps (delab i x) ++ " with "

113113 ++ showImp imps (delab i y) ++

114114 if (opt_errContext (idris_options i)) then showSc i env else ""

115+pshow i (CantInferType t)

116+ = "Can't infer type for " ++ t

115117pshow i (NonFunctionType f ty)

116118 = let imps = opt_showimp (idris_options i) in

117119 showImp imps (delab i f) ++ " does not have a function type ("

src/Idris/ElabTerm.hs+3−1

@@ -349,6 +349,7 @@ elab ist info pattern tcgen fn tm

349349 then -- simple app, as below

350350 do simple_app (elabE (ina, g) (PRef fc f))

351351 (elabE (True, g) (getTm (head args')))

352+ (show tm)

352353 solve

353354 else

354355 do ivs <- get_instances

@@ -401,9 +402,10 @@ elab ist info pattern tcgen fn tm

401402 setInjective (PApp _ (PRef _ n) _) = setinj n

402403 setInjective _ = return ()

403404

404− elab' ina@(_, a) (PApp fc f [arg])

405+ elab' ina@(_, a) tm@(PApp fc f [arg])

405406 = erun fc $

406407 do simple_app (elabE ina f) (elabE (True, a) (getTm arg))

408+ (show tm)

407409 solve

408410 elab' ina Placeholder = do (h : hs) <- get_holes

409411 movelast h