ca684b6 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix pToV scoping bug

commitca684b65e3f22d44ef7e2627b09e22abeb79bb30 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateTue 13 Nov 2012, 14:30 (14 years ago) parentf91a45a

3 files changed+7−3

unifiedsplit

src/Core/ProofState.hs+2−1

@@ -358,7 +358,8 @@ solve ctxt env (Bind x (Guess ty val) sc)

358358 -- dontunify = dontunify ps \\ [x],

359359 -- unified = (uh, uns ++ [(x, val)]),

360360 instances = instances ps \\ [x] })

361− return $ {- Bind x (Let ty val) sc -} instantiate val (pToV x sc)

361+ return $ {- Bind x (Let ty val) sc -}

362+ instantiate val (pToV x sc)

362363 | otherwise = lift $ tfail $ IncompleteTerm val

363364solve _ _ h = do ps <- get

364365 fail $ "Not a guess " ++ show h ++ "\n" ++ show (holes ps, pterm ps)

src/Core/TT.hs+3−1

@@ -515,7 +515,9 @@ pToV :: Eq n => n -> TT n -> TT n

515515pToV n = pToV' n 0

516516pToV' n i (P _ x _) | n == x = V i

517517pToV' n i (Bind x b sc)

518− | n == x = Bind x (fmap (pToV' n i) b) sc

518+-- We can assume the inner scope has been pToVed already, so continue to

519+-- resolve names from the *outer* scope which may happen to have the same id.

520+-- | n == x = Bind x (fmap (pToV' n i) b) sc

519521 | otherwise = Bind x (fmap (pToV' n i) b) (pToV' n (i+1) sc)

520522pToV' n i (App f a) = App (pToV' n i f) (pToV' n i a)

521523pToV' n i (Proj t idx) = Proj (pToV' n i t) idx

src/Idris/ElabDecls.hs+2−1

@@ -57,7 +57,8 @@ elabType info syn doc fc opts n ty' = {- let ty' = piBind (params info) ty_in

5757 ctxt <- getContext

5858 (cty, _) <- recheckC fc [] tyT

5959 addStatics n cty ty'

60− logLvl 2 $ "---> " ++ show cty

60+ logLvl 6 $ "Elaborated to " ++ showEnvDbg [] tyT

61+ logLvl 2 $ "Rechecked to " ++ show cty

6162 let nty = cty -- normalise ctxt [] cty

6263 -- if the return type is something coinductive, freeze the definition

6364 let nty' = normalise ctxt [] nty