809683b · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Don't allow unification problems to be introduced in :p mode

809683bEdwin Brady14 years ago

src/Core/Elaborate.hs+13

compare with master

unifiedsplit

@@ -525,6 +525,19 @@ arg n tyhole = do ty <- unique_hole tyhole

525 claim ty RType

526 forall n (Var ty)

527

528+-- try a tactic, if it adds any unification problem, return an error

529+no_errors :: Elab' aux () -> Elab' aux ()

530+no_errors tac

531+ = do ps <- get_probs

532+ tac

533+ ps' <- get_probs

534+ if (length ps' > length ps) then

535+ case reverse ps' of

536+ ((x,y,env,err) : _) ->

537+ let env' = map (\(x, b) -> (x, binderTy b)) env in

538+ lift $ tfail $ CantUnify False x y err env' 0

539+ else return ()

540+

528-- Try a tactic, if it fails, try another

541-- Try a tactic, if it fails, try another

529try :: Elab' aux a -> Elab' aux a -> Elab' aux a

542try :: Elab' aux a -> Elab' aux a -> Elab' aux a

530try t1 t2 = try' t1 t2 False

543try t1 t2 = try' t1 t2 False

src/Idris/ElabTerm.hs+4−2

@@ -695,10 +695,12 @@ collectDeferred (App f a) = liftM2 App (collectDeferred f) (collectDeferred a)

695collectDeferred t = return t

696

697-- Running tactics directly

698+-- if a tactic adds unification problems, return an error

698

699

699runTac :: Bool -> IState -> PTactic -> ElabD ()

700runTac :: Bool -> IState -> PTactic -> ElabD ()

700−runTac autoSolve ist tac = do env <- get_env

701+runTac autoSolve ist tac

702+ = do env <- get_env

701− runT (fmap (addImplBound ist (map fst env)) tac)

703+ no_errors $ runT (fmap (addImplBound ist (map fst env)) tac)

702 where

704 where

703 runT (Intro []) = do g <- goal

705 runT (Intro []) = do g <- goal

704 attack; intro (bname g)

706 attack; intro (bname g)