@@ -15,6 +15,7 @@ import Idris.Core.Unify
1515
1616import Control.Monad.State.Strict
1717import Control.Applicative hiding (empty)
18+import Control.Arrow (first)
1819import Data.List
1920import Debug.Trace
2021
@@ -230,6 +231,10 @@ action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()
230231action a = do ps <- get
231232 put (a ps)
232233
234+query :: Monad m => (ProofState -> r) -> StateT TState m r
235+query q = do ps <- get
236+ return $ q ps
237+
233238addLog :: Monad m => String -> StateT TState m ()
234239addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })
235240
@@ -638,10 +643,11 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do
638643 let scr = last $ tail args'
639644 let indxnames = makeIndexNames indicies
640645 prop <- replaceIndicies indxnames indicies $ Bind nm (Lam tmt') t
641− let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0)))
642− (params ++ [prop] ++ map makeConsArg consargs ++ indicies ++ [tmv])))
646+ consargs' <- query (\ps -> map (first $ flip (uniqueNameCtxt (context ps)) (holes ps)) consargs)
647+ let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs' (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0)))
648+ (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))
643649 action (\ps -> ps {holes = holes ps \\ [x]})
644− mapM_ addConsHole (reverse consargs)
650+ mapM_ addConsHole (reverse consargs')
645651 let res' = forget $ res
646652 (scv, sct) <- lift $ check ctxt env res'
647653 let scv' = specialise ctxt env [] scv