2c609ae · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Environment fix in prepare_apply

2c609aeEdwin Brady11 years ago

src/Idris/Core/Elaborate.hs+4−3

compare with master

unifiedsplit

@@ -501,7 +501,8 @@ prepare_apply fn imps =

501 env <- get_env

502 -- let claims = getArgs ty imps

503 -- claims <- mkClaims (normalise ctxt env ty) imps []

504+ claims <- -- trace (show (fn, imps, ty, map fst env, normalise ctxt env (finalise ty))) $

504− claims <- mkClaims (finalise ty)

505+ mkClaims (finalise ty)

505 (normalise ctxt env (finalise ty))

506 (normalise ctxt env (finalise ty))

506 imps [] (map fst env)

507 imps [] (map fst env)

507 ES (p, a) s prev <- get

508 ES (p, a) s prev <- get

@@ -522,8 +523,8 @@ prepare_apply fn imps =

522 n <- getNameFrom (mkMN n')

523 n <- getNameFrom (mkMN n')

523-- when (null claims) (start_unify n)

524-- when (null claims) (start_unify n)

524 let sc' = instantiate (P Bound n t) sc

525 let sc' = instantiate (P Bound n t) sc

525−-- trace ("CLAIMING " ++ show (n, t) ++ " with " ++ show (fn, hs)) $

526+ env <- get_env

526− claim n (forget t)

527+ claim n (forgetEnv (map fst env) t)

527 when i (movelast n)

528 when i (movelast n)

528 mkClaims sc' scn is ((n', n) : claims) hs

529 mkClaims sc' scn is ((n', n) : claims) hs

529 -- if we run out of arguments, we need the normalised version...

530 -- if we run out of arguments, we need the normalised version...

src/Idris/Core/TT.hs+1−1

@@ -1258,7 +1258,7 @@ safeForget tm = safeForgetEnv [] tm

1258forgetEnv :: [Name] -> TT Name -> Raw

1259forgetEnv env tm = case safeForgetEnv env tm of

1260 Just t' -> t'

1261− Nothing -> error $ "Scope error in " ++ show tm

1261+ Nothing -> error $ "Scope error in " ++ show tm ++ show env

1262

1263

1264safeForgetEnv :: [Name] -> TT Name -> Maybe Raw

src/Idris/Elab/Term.hs+8−4

@@ -757,10 +757,14 @@ elab ist info emode opts fn tm

757 (map (\x -> getTm x) args) -- TODO: remove this False arg

758 imp <- if (e_isfn ina) then

759 do guess <- get_guess

760− gty <- get_type (forget guess)

761 env <- get_env

760 env <- get_env

761+ case safeForgetEnv (map fst env) guess of

762+ Nothing ->

763+ return []

764+ Just rguess -> do

765+ gty <- get_type rguess

762− let ty_n = normalise ctxt env gty

766+ let ty_n = normalise ctxt env gty

763− return $ getReqImps ty_n

767+ return $ getReqImps ty_n

764 else return []

768 else return []

765 -- Now we find out how many implicits we needed at the

769 -- Now we find out how many implicits we needed at the

766 -- end of the application by looking at the goal again

770 -- end of the application by looking at the goal again

@@ -1250,7 +1254,7 @@ elab ist info emode opts fn tm

1250 where

1254 where

1251 -- just one level at a time

1255 -- just one level at a time

1252 addLam (Bind n (Pi (Just _) _ _) sc) t =

1256 addLam (Bind n (Pi (Just _) _ _) sc) t =

1253− do impn <- unique_hole (sMN 0 "imp")

1257+ do impn <- unique_hole n -- (sMN 0 "scoped_imp")

1254 if e_isfn ina -- apply to an implicit immediately

1258 if e_isfn ina -- apply to an implicit immediately

1255 then return (PApp emptyFC

1259 then return (PApp emptyFC

1256 (PLam emptyFC impn NoFC Placeholder t)

1260 (PLam emptyFC impn NoFC Placeholder t)