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

src/Core/Elaborate.hs+10−13

compare with master

unifiedsplit

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

501 solve

502 focus f

503

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

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

505−simple_app fun arg =

505+simple_app fun arg appstr =

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

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

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

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

514 start_unify s

515 claim s (Var a)

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

523 focus f; fun

517 focus f; fun

524 focus s; arg

518 focus s; arg

525 tm <- get_term

519 tm <- get_term

526 ps <- get_probs

520 ps <- get_probs

527 complete_fill

521 complete_fill

528 hs <- get_holes

522 hs <- get_holes

523+ env <- get_env

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

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

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

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

531− -- regret will fail

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

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

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

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

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

534 end_unify

529 end_unify

530+ where regretWith err = try regret

531+ (lift $ tfail err)

535

532

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

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

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

534-- 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 =

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

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

365 return sc

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

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

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

367

368

368exact :: Raw -> RunTactic

369exact :: Raw -> RunTactic

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

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

src/Core/TT.hs+2

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

60 -- unification succeed

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

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

63+ | CantInferType String

63 | NonFunctionType Term Term

64 | NonFunctionType Term Term

64 | CantIntroduce Term

65 | CantIntroduce Term

65 | NoSuchVariable Name

66 | NoSuchVariable Name

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

103score (CantResolve _) = 20

104score (CantResolve _) = 20

104score (NoSuchVariable _) = 1000

105score (NoSuchVariable _) = 1000

105score (ProofSearchFail _) = 10000

106score (ProofSearchFail _) = 10000

107+score (InternalMsg _) = -1

106score _ = 0

108score _ = 0

107

109

108instance Show Err where

110instance Show Err where

src/Idris/Delaborate.hs+2

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

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

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

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

115+pshow i (CantInferType t)

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

115pshow i (NonFunctionType f ty)

117pshow i (NonFunctionType f ty)

116 = let imps = opt_showimp (idris_options i) in

118 = let imps = opt_showimp (idris_options i) in

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

119 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

349 then -- simple app, as below

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

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

352+ (show tm)

352 solve

353 solve

353 else

354 else

354 do ivs <- get_instances

355 do ivs <- get_instances

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

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

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

402 setInjective _ = return ()

403 setInjective _ = return ()

403

404

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

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

405 = erun fc $

406 = erun fc $

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

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

408+ (show tm)

407 solve

409 solve

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

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

409 movelast h

411 movelast h