834bda8 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #976 from ahmadsalim/bug/inductionnamefix

834bda8Edwin Brady13 years ago

src/Idris/Core/ProofState.hs+9−3

compare with master

unifiedsplit

@@ -15,6 +15,7 @@ import Idris.Core.Unify

16import Control.Monad.State.Strict

17import Control.Applicative hiding (empty)

18+import Control.Arrow (first)

18import Data.List

19import Data.List

19import Debug.Trace

20import Debug.Trace

@@ -230,6 +231,10 @@ action :: Monad m => (ProofState -> ProofState) -> StateT TState m ()

230action a = do ps <- get

231action a = do ps <- get

231 put (a ps)

232 put (a ps)

232

233

234+query :: Monad m => (ProofState -> r) -> StateT TState m r

235+query q = do ps <- get

236+ return $ q ps

237+

233addLog :: Monad m => String -> StateT TState m ()

238addLog :: Monad m => String -> StateT TState m ()

234addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

239addLog str = action (\ps -> ps { plog = plog ps ++ str ++ "\n" })

235

240

@@ -638,10 +643,11 @@ induction nm ctxt env (Bind x (Hole t) (P _ x' _)) | x == x' = do

638 let scr = last $ tail args'

643 let scr = last $ tail args'

639 let indxnames = makeIndexNames indicies

644 let indxnames = makeIndexNames indicies

640 prop <- replaceIndicies indxnames indicies $ Bind nm (Lam tmt') t

645 prop <- replaceIndicies indxnames indicies $ Bind nm (Lam tmt') t

646+ consargs' <- query (\ps -> map (first $ flip (uniqueNameCtxt (context ps)) (holes ps)) consargs)

641− let res = flip (foldr substV) params $ (substV prop $ bindConsArgs consargs (mkApp (P Ref (SN (ElimN tnm)) (TType (UVal 0)))

647+ 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])))

648+ (params ++ [prop] ++ map makeConsArg consargs' ++ indicies ++ [tmv])))

643 action (\ps -> ps {holes = holes ps \\ [x]})

649 action (\ps -> ps {holes = holes ps \\ [x]})

644− mapM_ addConsHole (reverse consargs)

650+ mapM_ addConsHole (reverse consargs')

645 let res' = forget $ res

651 let res' = forget $ res

646 (scv, sct) <- lift $ check ctxt env res'

652 (scv, sct) <- lift $ check ctxt env res'

647 let scv' = specialise ctxt env [] scv

653 let scv' = specialise ctxt env [] scv