d3660ed · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Don't pass used unique variables to metavars

d3660edEdwin Brady12 years ago

src/Idris/Elab/Utils.hs+31

compare with master

unifiedsplit

@@ -13,6 +13,7 @@ import Idris.Core.Evaluate

13import Idris.Core.Typecheck

15import Control.Applicative hiding (Const)

16+import Control.Monad.State

16import Control.Monad

17import Control.Monad

17import Data.List

18import Data.List

@@ -205,3 +206,33 @@ paramNames args env (p : ps)

205 else paramNames args env ps

206 else paramNames args env ps

206 _ -> paramNames args env ps

207 _ -> paramNames args env ps

207 | otherwise = paramNames args env ps

208 | otherwise = paramNames args env ps

209+

210+getUniqueUsed :: Context -> Term -> [Name]

211+getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

212+ where

213+ getUniq :: Env -> [(Name, Bool)] -> Term -> State [Name] ()

214+ getUniq env us (Bind n b sc)

215+ = let uniq = case check ctxt env (forgetEnv (map fst env) (binderTy b)) of

216+ OK (_, UType UniqueType) -> True

217+ OK (_, UType NullType) -> True

218+ OK (_, UType AllTypes) -> True

219+ _ -> False in

220+ do getUniqB env us b

221+ getUniq ((n,b):env) ((n, uniq):us) sc

222+ getUniq env us (App f a) = do getUniq env us f; getUniq env us a

223+ getUniq env us (V i)

224+ | i < length us = if snd (us!!i) then use (fst (us!!i)) else return ()

225+ getUniq env us (P _ n _)

226+ | Just u <- lookup n us = if u then use n else return ()

227+ getUniq env us _ = return ()

228+

229+ use n = do ns <- get; put (n : ns)

230+

231+ getUniqB env us (Let t v) = do getUniq env us t; getUniq env us v

232+ getUniqB env us (Guess t v) = do getUniq env us t; getUniq env us v

233+ getUniqB env us (Pi t v) = do getUniq env us t; getUniq env us v

234+ getUniqB env us (NLet t v) = do getUniq env us t; getUniq env us v

235+ getUniqB env us b = getUniq env us (binderTy b)

236+

237+

238+

src/Idris/ElabTerm.hs+11−2

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

17import Idris.Core.Typecheck (check, recheck)

18import Idris.ErrReverse (errReverse)

19import Idris.ElabQuasiquote (extractUnquotes)

20+import Idris.Elab.Utils

20import qualified Util.Pretty as U

21import qualified Util.Pretty as U

22import Control.Applicative ((<$>))

23import Control.Applicative ((<$>))

@@ -629,8 +630,16 @@ elab ist info emode opts fn tm

629 solve

630 solve

630 elab' ina Placeholder = do (h : hs) <- get_holes

631 elab' ina Placeholder = do (h : hs) <- get_holes

631 movelast h

632 movelast h

632− elab' ina (PMetavar n) = let n' = mkN n in

633+ elab' ina (PMetavar n) =

634+ do ptm <- get_term

635+ -- When building the metavar application, leave out the unique

636+ -- names which have been used elsewhere in the term, since we

637+ -- won't be able to use them in the resulting application.

638+ let unique_used = getUniqueUsed (tt_ctxt ist) ptm

639+ let n' = mkN n

633− do attack; defer [] n'; solve

640+ attack

641+ defer unique_used n'

642+ solve

634 where mkN n@(NS _ _) = n

643 where mkN n@(NS _ _) = n

635 mkN n = case namespace info of

644 mkN n = case namespace info of

636 Just xs@(_:_) -> sNS n xs

645 Just xs@(_:_) -> sNS n xs