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

git.iko.soy/Idris-dev

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

commit809683bf0fd94e785bf41b7702d19854b614cbb4 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSun 14 Apr 2013, 14:12 (14 years ago) parent4f63881

2 files changed+17−2

unifiedsplit

src/Core/Elaborate.hs+13

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

525525 claim ty RType

526526 forall n (Var ty)

527527

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+

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

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

530543try 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)

695695collectDeferred t = return t

696696

697697-- Running tactics directly

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

698699

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

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

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

701+runTac autoSolve ist tac

702+ = do env <- get_env

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

702704 where

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

704706 attack; intro (bname g)