e3daf28 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Add RigCount to environment

e3daf28Edwin Brady10 years ago

src/Idris/Core/Elaborate.hs+7−7

compare with master

unifiedsplit

@@ -99,7 +99,7 @@ setNextName :: Elab' aux ()

99setNextName = do env <- get_env

100 ES (p, a) s e <- get

101 let pargs = map fst (getArgTys (ptype p))

102− initNextNameFrom (pargs ++ map fst env)

102+ initNextNameFrom (pargs ++ map fstEnv env)

103

104initNextNameFrom :: [Name] -> Elab' aux ()

105initNextNameFrom ns = do ES (p, a) s e <- get

@@ -468,7 +468,7 @@ patvar :: Name -> Elab' aux ()

468patvar n@(SN _) = do apply (Var n) []; solve

469patvar n = do env <- get_env

470 hs <- get_holes

471− if (n `elem` map fst env) then do apply (Var n) []; solve

471+ if (n `elem` map fstEnv env) then do apply (Var n) []; solve

472 else do n' <- case hs of

473 (h : hs) -> if n == h then return n

474 else unique_hole n

@@ -481,7 +481,7 @@ patvar' :: Name -> Elab' aux ()

481patvar' n@(SN _) = do apply (Var n) [] ; solve

482patvar' n = do env <- get_env

483 hs <- get_holes

484− if (n `elem` map fst env) then do apply (Var n) [] ; solve

484+ if (n `elem` map fstEnv env) then do apply (Var n) [] ; solve

485 else processTactic' (PatVar n)

486

487patbind :: Name -> Elab' aux ()

@@ -580,7 +580,7 @@ prepare_apply fn imps =

580 then finalise ty

581 else whnfArgs ctxt env (finalise ty)

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

583− mkClaims usety imps [] (map fst env)

583+ mkClaims usety imps [] (map fstEnv env)

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

585 -- reverse the claims we made so that args go left to right

586 let n = length (filter not imps)

@@ -604,7 +604,7 @@ prepare_apply fn imps =

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

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

606 env <- get_env

607− claim n (forgetEnv (map fst env) t)

607+ claim n (forgetEnv (map fstEnv env) t)

608 when i (movelast n)

609 mkClaims sc' is ((n', n) : claims) hs

610 mkClaims t [] claims _ = return $! (reverse claims)

@@ -869,7 +869,7 @@ no_errors tac err

869 case reverse ps' of

870 ((x, y, _, env, inerr, while, _) : _) ->

871 let (xp, yp) = getProvenance inerr

872− env' = map (\(x, b) -> (x, binderTy b)) env in

872+ env' = map (\(x, rig, b) -> (x, binderTy b)) env in

873 lift $ tfail $

874 case err of

875 Nothing -> CantUnify False (x, xp) (y, yp) inerr env' 0

@@ -1013,7 +1013,7 @@ debugElaborator msg = do ps <- fmap proof get

1013 getHoleInfo h = do focus h

1014 g <- goal

1015 env <- get_env

1016− return (h, g, env)

1016+ return (h, g, envBinders env)

1017

1018qshow :: Fails -> String

1019qshow fs = show (map (\ (x, y, _, _, _, _, _) -> (x, y)) fs)

src/Idris/Core/Evaluate.hs+7−7

@@ -197,13 +197,13 @@ unfold ctxt env ns t

197

198-- unbindEnv env (quote 0 (eval ctxt (bindEnv env t)))

199

200−finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))

200+finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))

201−finalEntry (n, b) = (n, fmap finalise b)

201+finalEntry (n, r, b) = (n, r, fmap finalise b)

202

203bindEnv :: EnvTT n -> TT n -> TT n

204bindEnv [] tm = tm

205−bindEnv ((n, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)

205+bindEnv ((n, r, Let t v):bs) tm = Bind n (NLet t v) (bindEnv bs tm)

206−bindEnv ((n, b):bs) tm = Bind n b (bindEnv bs tm)

206+bindEnv ((n, r, b):bs) tm = Bind n b (bindEnv bs tm)

207

208unbindEnv :: EnvTT n -> TT n -> TT n

209unbindEnv [] tm = tm

@@ -282,7 +282,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

282 | otherwise = cases_compiletime cd

283

284 ev ntimes stk top env (P _ n ty)

285− | Just (Let t v) <- lookup n genv = ev ntimes stk top env v

285+ | Just (Let t v) <- lookupBinder n genv = ev ntimes stk top env v

286 ev ntimes_in stk top env (P Ref n ty)

287 = do let limit = if simpl then 100 else 10000

288 (u, ntimes) <- usable spec unfold limit n ntimes_in

@@ -337,7 +337,7 @@ eval traceon ctxt ntimes genv tm opts = ev ntimes [] True [] tm where

337 return $ VBind True n (Let t' v') (\x -> return sc')

338 ev ntimes stk top env (Bind n b sc)

339 = do b' <- vbind env b

340− let n' = uniqueName n (map fst genv ++ map fst env)

340+ let n' = uniqueName n (map fstEnv genv ++ map fst env)

341 return $ VBind True -- (vinstances 0 sc < 2)

342 n' b' (\x -> ev ntimes stk False ((n', x):env) sc)

343 where vbind env t

@@ -1181,7 +1181,7 @@ lookupVal n ctxt

1181 _ -> []

1182

1183lookupTyEnv :: Name -> Env -> Maybe (Int, Type)

1184−lookupTyEnv n env = li n 0 env where

1184+lookupTyEnv n env = li n 0 (envBinders env) where

1185 li n i [] = Nothing

1186 li n i ((x, b): xs)

1187 | n == x = Just (i, binderTy b)

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

@@ -114,7 +114,7 @@ toTT (EConstant c) = return (Constant c)

114toTT (EThunk ctxt env tm) = do env' <- mapM toBinder env

115 return $ normalise ctxt env' tm

116 where toBinder (n, v) = do v' <- toTT v

117− return (n, Let Erased v')

117+ return (n, Rig0, Let Erased v')

118toTT (EHandle _) = execFail $ Msg "Can't convert handles back to TT after execution."

119toTT (EPtr ptr) = execFail $ Msg "Can't convert pointers back to TT after execution."

120

src/Idris/Core/ProofState.hs+12−12

@@ -129,12 +129,12 @@ instance Show ProofState where

129 ") -------\n " ++

130 show h ++ " : " ++ showG wkenv (goalType g) ++ "\n"

131 where showPs env [] = ""

132− showPs env ((n, Let t v):bs)

132+ showPs env ((n, _, Let t v):bs)

133 = " " ++ show n ++ " : " ++

134 showEnv env ({- normalise ctxt env -} t) ++ " = " ++

135 showEnv env ({- normalise ctxt env -} v) ++

136 "\n" ++ showPs env bs

137− showPs env ((n, b):bs)

137+ showPs env ((n, _, b):bs)

138 = " " ++ show n ++ " : " ++

139 showEnv env ({- normalise ctxt env -} (binderTy b)) ++

140 "\n" ++ showPs env bs

@@ -160,18 +160,18 @@ instance Pretty ProofState OutputAnnotation where

160 prettyGoal ps b = prettyEnv ps $ binderTy b

161

162 prettyPs env [] = empty

163− prettyPs env ((n, Let t v):bs) =

163+ prettyPs env ((n, _, Let t v):bs) =

164 nest nestingSize (pretty n <+> colon <+>

165 prettyEnv env t <+> text "=" <+> prettyEnv env v <+>

166 nest nestingSize (prettyPs env bs))

167− prettyPs env ((n, b):bs) =

167+ prettyPs env ((n, _, b):bs) =

168 nest nestingSize (pretty n <+> colon <+> prettyEnv env (binderTy b) <+>

169 nest nestingSize (prettyPs env bs))

170

171holeName i = sMN i "hole"

172

173qshow :: Fails -> String

174−qshow fs = show (map (\ (x, y, hs, env, _, _, t) -> (t, map fst env, x, y, hs)) fs)

174+qshow fs = show (map (\ (x, y, hs, env, _, _, t) -> (t, map fstEnv env, x, y, hs)) fs)

175

176match_unify' :: Context -> Env ->

177 (TT Name, Maybe Provenance) ->

@@ -363,7 +363,7 @@ computeLet ctxt n tm = cl [] tm where

363 cl env (Bind n' (Let t v) sc)

364 | n' == n = let v' = normalise ctxt env v in

365 Bind n' (Let t v') sc

366− cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, b):env) sc)

366+ cl env (Bind n' b sc) = Bind n' (fmap (cl env) b) (cl ((n, Rig0, b):env) sc)

367 cl env (App s f a) = App s (cl env f) (cl env a)

368 cl env t = t

369

@@ -463,7 +463,7 @@ setinj n ctxt env (Bind x b sc)

463

464defer :: [Name] -> Name -> RunTactic

465defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

466− do let env' = filter (\(n, t) -> n `notElem` dropped) env

466+ do let env' = filter (\(n, _, t) -> n `notElem` dropped) env

467 action (\ps -> let hs = holes ps in

468 ps { usedns = n : usedns ps,

469 holes = hs \\ [x] })

@@ -472,9 +472,9 @@ defer dropped n ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

472 (mkApp (P Ref n ty) (map getP (reverse env'))))

473 where

474 mkTy [] t = t

475− mkTy ((n,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar [] 0))) (mkTy bs t)

475+ mkTy ((n,rig,b) : bs) t = Bind n (Pi Nothing (binderTy b) (TType (UVar [] 0))) (mkTy bs t)

476

477− getP (n, b) = P Bound n (binderTy b)

477+ getP (n, rig, b) = P Bound n (binderTy b)

478defer dropped n ctxt env _ = fail "Can't defer a non-hole focus."

479

480-- as defer, but build the type and application explicitly

@@ -488,7 +488,7 @@ deferType n fty_in args ctxt env (Bind x (Hole t) (P nt x' ty)) | x == x' =

488 return (Bind n (GHole 0 [] fty)

489 (mkApp (P Ref n ty) (map getP args)))

490 where

491− getP n = case lookup n env of

491+ getP n = case lookupBinder n env of

492 Just b -> P Bound n (binderTy b)

493 Nothing -> error ("deferType can't find " ++ show n)

494deferType _ _ _ _ _ _ = fail "Can't defer a non-hole focus."

@@ -914,8 +914,8 @@ keepGiven du (u : us) hs = keepGiven du us hs

914

915updateEnv [] e = e

916updateEnv ns [] = []

917−updateEnv ns ((n, b) : env)

917+updateEnv ns ((n, rig, b) : env)

918− = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

918+ = (n, rig, fmap (updateSolvedTerm ns) b) : updateEnv ns env

919

920updateProv ns (SourceTerm t) = SourceTerm $ updateSolvedTerm ns t

921updateProv ns p = p

src/Idris/Core/ProofTerm.hs+7−7

@@ -84,7 +84,7 @@ findHole n env t = fh' env Top t where

84 | Just (p, env', tm) <- fh' env path f = Just (AppL s p a, env', tm)

85 fh' env path (Bind x b sc)

86 | Just (bp, env', tm) <- fhB env path b = Just (InBind x bp sc, env', tm)

87− | Just (p, env', tm) <- fh' ((x,b):env) path sc = Just (InScope x b p, env', tm)

87+ | Just (p, env', tm) <- fh' ((x,Rig0,b):env) path sc = Just (InScope x b p, env', tm)

88 fh' _ _ _ = Nothing

90 fhB env path (Let t v)

@@ -255,7 +255,7 @@ updsubst n v tm = fst $ subst' 0 tm

255updateEnv :: [(Name, Term)] -> Env -> Env

256updateEnv [] e = e

257updateEnv ns [] = []

258−updateEnv ns ((n, b) : env) = (n, fmap (updateSolvedTerm ns) b) : updateEnv ns env

258+updateEnv ns ((n, r, b) : env) = (n, r, fmap (updateSolvedTerm ns) b) : updateEnv ns env

259

260-- | Fill out solved holes in a term zipper.

261updateSolvedPath :: [(Name, Term)] -> TermPath -> TermPath

@@ -284,7 +284,7 @@ updateSolvedPath ns (InScope n b sc)

284updateSolved :: [(Name, Term)] -> ProofTerm -> ProofTerm

285updateSolved xs pt@(PT path env sub ups)

286 = PT path -- (updateSolvedPath xs path)

287− (updateEnv xs (filter (\(n, t) -> n `notElem` map fst xs) env))

287+ (updateEnv xs (filter (\(n, r, t) -> n `notElem` map fst xs) env))

288 (updateSolvedTerm xs sub)

289 (ups ++ xs)

290

@@ -297,10 +297,10 @@ goal h pt@(PT path env sub ups)

297 g env (Bind n b@(Guess _ _) sc)

298 | same h n = return $ GD env b

299 | otherwise

300− = gb env b `mplus` g ((n, b):env) sc

300+ = gb env b `mplus` g ((n, Rig0, b):env) sc

301 g env (Bind n b sc) | hole b && same h n = return $ GD env b

302 | otherwise

303− = g ((n, b):env) sc `mplus` gb env b

303+ = g ((n, Rig0, b):env) sc `mplus` gb env b

304 g env (App Complete f a) = fail "Can't find hole"

305 g env (App _ f a) = g env a `mplus` g env f

306 g env t = fail "Can't find hole"

@@ -338,12 +338,12 @@ atHole h f c e pt -- @(PT path env sub)

338 = do -- binder first

339 (b', u) <- ulift2 f c env Guess t v

340 if u then return (Bind n b' sc, True)

341− else do (sc', u) <- atH f c ((n, b) : env) sc

341+ else do (sc', u) <- atH f c ((n, Rig0, b) : env) sc

342 return (Bind n b' sc', u)

343 atH f c env binder@(Bind n b sc)

344 | hole b && same h n = updated (f c env binder)

345 | otherwise -- scope first

346− = do (sc', u) <- atH f c ((n, b) : env) sc

346+ = do (sc', u) <- atH f c ((n, Rig0, b) : env) sc

347 if u then return (Bind n b sc', True)

348 else do (b', u) <- atHb f c env b

349 return (Bind n b' sc', u)

src/Idris/Core/TT.hs+24−11

@@ -31,7 +31,7 @@ module Idris.Core.TT(

31 , Env(..), EnvTT(..), Err(..), Err'(..), ErrorReportPart(..)

32 , FC(..), FC'(..), ImplicitInfo(..), IntTy(..), Name(..)

33 , NameOutput(..), NameType(..), NativeTy(..), OutputAnnotation(..)

34− , Provenance(..), Raw(..), SpecialName(..), TC(..), Term(..)

34+ , Provenance(..), Raw(..), RigCount(..), SpecialName(..), TC(..), Term(..)

35 , TermSize(..), TextFormatting(..), TT(..),Type(..), TypeInfo(..)

36 , UConstraint(..), UCs(..), UExp(..), Universe(..)

37 , addAlist, addBinder, addDef, allTTNames, arity, bindAll

@@ -49,6 +49,7 @@ module Idris.Core.TT(

49 , substV, sUN, tcname, termSmallerThan, tfail, thead, tnull

50 , toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName

51 , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm

52+ , fstEnv, rigEnv, sndEnv, lookupBinder, envBinders

52 ) where

53 ) where

54import Util.Pretty hiding (Str)

55import Util.Pretty hiding (Str)

@@ -1064,7 +1065,19 @@ instance Sized a => Sized (TT a) where

1064instance Pretty a o => Pretty (TT a) o where

1065instance Pretty a o => Pretty (TT a) o where

1065 pretty _ = text "test"

1066 pretty _ = text "test"

1066

1067

1068+data RigCount = Rig0 | Rig1 | RigW

1069+ deriving (Show, Eq, Ord, Data, Generic, Typeable)

1070+

1067−type EnvTT n = [(n, Binder (TT n))]

1071+type EnvTT n = [(n, RigCount, Binder (TT n))]

1072+

1073+fstEnv (n, c, b) = n

1074+rigEnv (n, c, b) = c

1075+sndEnv (n, c, b) = b

1076+

1077+envBinders = map (\(n, _, b) -> (n, b))

1078+

1079+lookupBinder :: Eq n => n -> EnvTT n -> Maybe (Binder (TT n))

1080+lookupBinder n = lookup n . envBinders

1068

1081

1069data Datatype n = Data { d_typename :: n,

1082data Datatype n = Data { d_typename :: n,

1070 d_typetag :: Int,

1083 d_typetag :: Int,

@@ -1572,15 +1585,15 @@ prettyEnv env t = prettyEnv' env t False

1572 prettySe p env (V i) debug

1585 prettySe p env (V i) debug

1573 | i < length env =

1586 | i < length env =

1574 if debug then

1587 if debug then

1575− text . show . fst $ env!!i

1588+ text . show . fstEnv $ env!!i

1576 else

1589 else

1577 lbracket <+> text (show i) <+> rbracket

1590 lbracket <+> text (show i) <+> rbracket

1578 | otherwise = text "unbound" <+> text (show i) <+> text "!"

1591 | otherwise = text "unbound" <+> text (show i) <+> text "!"

1579 prettySe p env (Bind n b@(Pi _ t _) sc) debug

1592 prettySe p env (Bind n b@(Pi _ t _) sc) debug

1580 | noOccurrence n sc && not debug =

1593 | noOccurrence n sc && not debug =

1581− bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

1594+ bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, Rig0, b):env) sc debug

1582 prettySe p env (Bind n b sc) debug =

1595 prettySe p env (Bind n b sc) debug =

1583− bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, b):env) sc debug

1596+ bracket p 2 $ prettySb env n b debug <> prettySe 10 ((n, Rig0, b):env) sc debug

1584 prettySe p env (App _ f a) debug =

1597 prettySe p env (App _ f a) debug =

1585 bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug

1598 bracket p 1 $ prettySe 1 env f debug <+> prettySe 0 env a debug

1586 prettySe p env (Proj x i) debug =

1599 prettySe p env (Proj x i) debug =

@@ -1620,16 +1633,16 @@ showEnv' env t dbg = se 10 env t where

1620 se p env (P nt n t) = show n

1633 se p env (P nt n t) = show n

1621 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

1634 ++ if dbg then "{" ++ show nt ++ " : " ++ se 10 env t ++ "}" else ""

1622 se p env (V i) | i < length env && i >= 0

1635 se p env (V i) | i < length env && i >= 0

1623− = (show $ fst $ env!!i) ++

1636+ = (show $ fstEnv $ env!!i) ++

1624 if dbg then "{" ++ show i ++ "}" else ""

1637 if dbg then "{" ++ show i ++ "}" else ""

1625 | otherwise = "!!V " ++ show i ++ "!!"

1638 | otherwise = "!!V " ++ show i ++ "!!"

1626 se p env (Bind n b@(Pi (Just _) t k) sc)

1639 se p env (Bind n b@(Pi (Just _) t k) sc)

1627− = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

1640+ = bracket p 2 $ sb env n b ++ se 10 ((n,Rig0,b):env) sc

1628 se p env (Bind n b@(Pi _ t k) sc)

1641 se p env (Bind n b@(Pi _ t k) sc)

1629− | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow k ++ se 10 ((n,b):env) sc

1642+ | noOccurrence n sc && not dbg = bracket p 2 $ se 1 env t ++ arrow k ++ se 10 ((n,Rig0,b):env) sc

1630 where arrow (TType _) = " -> "

1643 where arrow (TType _) = " -> "

1631 arrow u = " [" ++ show u ++ "] -> "

1644 arrow u = " [" ++ show u ++ "] -> "

1632− se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,b):env) sc

1645+ se p env (Bind n b sc) = bracket p 2 $ sb env n b ++ se 10 ((n,Rig0,b):env) sc

1633 se p env (App _ f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

1646 se p env (App _ f a) = bracket p 1 $ se 1 env f ++ " " ++ se 0 env a

1634 se p env (Proj x i) = se 1 env x ++ "!" ++ show i

1647 se p env (Proj x i) = se 1 env x ++ "!" ++ show i

1635 se p env (Constant c) = show c

1648 se p env (Constant c) = show c

@@ -1686,14 +1699,14 @@ weakenTm i t = wk i 0 t

1686weakenEnv :: EnvTT n -> EnvTT n

1699weakenEnv :: EnvTT n -> EnvTT n

1687weakenEnv env = wk (length env - 1) env

1700weakenEnv env = wk (length env - 1) env

1688 where wk i [] = []

1701 where wk i [] = []

1689− wk i ((n, b) : bs) = (n, weakenTmB i b) : wk (i - 1) bs

1702+ wk i ((n, c, b) : bs) = (n, c, weakenTmB i b) : wk (i - 1) bs

1690 weakenTmB i (Let t v) = Let (weakenTm i t) (weakenTm i v)

1703 weakenTmB i (Let t v) = Let (weakenTm i t) (weakenTm i v)

1691 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)

1704 weakenTmB i (Guess t v) = Guess (weakenTm i t) (weakenTm i v)

1692 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }

1705 weakenTmB i t = t { binderTy = weakenTm i (binderTy t) }

1693

1706

1694-- | Weaken every term in the environment by the given amount

1707-- | Weaken every term in the environment by the given amount

1695weakenTmEnv :: Int -> EnvTT n -> EnvTT n

1708weakenTmEnv :: Int -> EnvTT n -> EnvTT n

1696−weakenTmEnv i = map (\ (n, b) -> (n, fmap (weakenTm i) b))

1709+weakenTmEnv i = map (\ (n, c, b) -> (n, c, fmap (weakenTm i) b))

1697

1710

1698refsIn :: TT Name -> [Name]

1711refsIn :: TT Name -> [Name]

1699refsIn (P _ n _) = [n]

1712refsIn (P _ n _) = [n]

src/Idris/Core/Typecheck.hs+17−15

@@ -25,7 +25,7 @@ import Debug.Trace

26convertsC :: Context -> Env -> Term -> Term -> StateT UCs TC ()

27convertsC ctxt env x y =

28− do let hs = map fst (filter isHole env)

28+ do let hs = map fstEnv (filter isHole env)

29 c1 <- convEq ctxt hs x y

30 if c1 then return ()

31 else

@@ -38,7 +38,7 @@ convertsC ctxt env x y =

39converts :: Context -> Env -> Term -> Term -> TC ()

40converts ctxt env x y

41− = let hs = map fst (filter isHole env) in

41+ = let hs = map fstEnv (filter isHole env) in

42 case convEq' ctxt hs x y of

43 OK True -> return ()

44 _ -> case convEq' ctxt hs (finalise (normalise ctxt env x))

@@ -48,10 +48,10 @@ converts ctxt env x y

48 (finalise (normalise ctxt env x))

49 (finalise (normalise ctxt env y)) (errEnv env))

51−isHole (n, Hole _) = True

51+isHole (n, _, Hole _) = True

52isHole _ = False

54−errEnv = map (\(x, b) -> (x, binderTy b))

54+errEnv = map (\(x, _, b) -> (x, binderTy b))

56isType :: Context -> Env -> Term -> TC ()

57isType ctxt env tm = isType' (normalise ctxt env tm)

@@ -113,9 +113,9 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

113 chk u lvl env ap@(RApp f RType) | not holes

114 -- special case to reduce constraintss

115 = do (fv, fty) <- chk u Nothing env f

116− let fty' = case uniqueBinders (map fst env) (finalise fty) of

116+ let fty' = case uniqueBinders (map fstEnv env) (finalise fty) of

117 ty@(Bind x (Pi i s k) t) -> ty

118− _ -> uniqueBinders (map fst env)

118+ _ -> uniqueBinders (map fstEnv env)

119 $ case normalise ctxt env fty of

120 ty@(Bind x (Pi i s k) t) -> ty

121 _ -> normalise ctxt env fty

@@ -135,9 +135,9 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

135 t -> lift $ tfail $ NonFunctionType fv fty

136 chk u lvl env ap@(RApp f a)

137 = do (fv, fty) <- chk u Nothing env f

138− let fty' = case uniqueBinders (map fst env) (finalise fty) of

138+ let fty' = case uniqueBinders (map fstEnv env) (finalise fty) of

139 ty@(Bind x (Pi i s k) t) -> ty

140− _ -> uniqueBinders (map fst env)

140+ _ -> uniqueBinders (map fstEnv env)

141 $ case normalise ctxt env fty of

142 ty@(Bind x (Pi i s k) t) -> ty

143 _ -> normalise ctxt env fty

@@ -186,7 +186,8 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

186 let maxu = case lvl of

187 Nothing -> UVar tcns v

188 Just v' -> v'

189+ -- TODO: Get RigCount from Pi

189− (tv, tt) <- chk st (Just maxu) ((n, Pi i sv kv) : env) t

190+ (tv, tt) <- chk st (Just maxu) ((n, Rig0, Pi i sv kv) : env) t

190

191

191-- convertsC ctxt env st (TType maxu)

192-- convertsC ctxt env st (TType maxu)

192-- convertsC ctxt env tt (TType maxu)

193-- convertsC ctxt env tt (TType maxu)

@@ -200,11 +201,11 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

200 put (v, ULE su maxu :

201 put (v, ULE su maxu :

201 ULE tu maxu : cs)

202 ULE tu maxu : cs)

202 let k' = TType (UVar tcns v) `smaller` st `smaller` kv `smaller` u

203 let k' = TType (UVar tcns v) `smaller` st `smaller` kv `smaller` u

203− return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')

204+ return (Bind n (Pi i (uniqueBinders (map fstEnv env) sv) k')

204 (pToV n tv), k')

205 (pToV n tv), k')

205 (un, un') ->

206 (un, un') ->

206 let k' = st `smaller` kv `smaller` un `smaller` un' `smaller` u in

207 let k' = st `smaller` kv `smaller` un `smaller` un' `smaller` u in

207− return (Bind n (Pi i (uniqueBinders (map fst env) sv) k')

208+ return (Bind n (Pi i (uniqueBinders (map fstEnv env) sv) k')

208 (pToV n tv), k')

209 (pToV n tv), k')

209

210

210 where mkUniquePi kv (Bind n (Pi i s k) sc)

211 where mkUniquePi kv (Bind n (Pi i s k) sc)

@@ -224,7 +225,8 @@ check' holes tcns ctxt env top = chk (TType (UVar tcns (-5))) Nothing env top wh

224

225

225 chk u lvl env (RBind n b sc)

226 chk u lvl env (RBind n b sc)

226 = do (b', bt') <- checkBinder b

227 = do (b', bt') <- checkBinder b

228+ -- TODO: Get RigCount from binder (Pi or Pattern?)

227− (scv, sct) <- chk (smaller bt' u) Nothing ((n, b'):env) sc

229+ (scv, sct) <- chk (smaller bt' u) Nothing ((n, Rig0, b'):env) sc

228 discharge n b' bt' (pToV n scv) (pToV n sct)

230 discharge n b' bt' (pToV n scv) (pToV n sct)

229 where checkBinder (Lam t)

231 where checkBinder (Lam t)

230 = do (tv, tt) <- chk u Nothing env t

232 = do (tv, tt) <- chk u Nothing env t

@@ -316,7 +318,7 @@ checkUnique borrowed ctxt env tm

316 isVar _ = False

318 isVar _ = False

317

319

318 chkBinders :: Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()

320 chkBinders :: Env -> Term -> StateT [(Name, (UniqueUse, Universe))] TC ()

319− chkBinders env (V i) | length env > i = chkName (fst (env!!i))

321+ chkBinders env (V i) | length env > i = chkName (fstEnv (env!!i))

320 chkBinders env (P _ n _) = chkName n

322 chkBinders env (P _ n _) = chkName n

321 -- 'lending' a unique or nulltype variable doesn't count as a use,

323 -- 'lending' a unique or nulltype variable doesn't count as a use,

322 -- but we still can't lend something that's already been used.

324 -- but we still can't lend something that's already been used.

@@ -336,13 +338,13 @@ checkUnique borrowed ctxt env tm

336 case b of

338 case b of

337 Let t v -> chkBinders env v

339 Let t v -> chkBinders env v

338 _ -> return ()

340 _ -> return ()

339− chkBinders ((n, b) : env) t

341+ chkBinders ((n, Rig0, b) : env) t

340 chkBinders env t = return ()

342 chkBinders env t = return ()

341

343

342 chkBinderName :: Env -> Name -> Binder Term ->

344 chkBinderName :: Env -> Name -> Binder Term ->

343 StateT [(Name, (UniqueUse, Universe))] TC ()

345 StateT [(Name, (UniqueUse, Universe))] TC ()

344 chkBinderName env n b

346 chkBinderName env n b

345− = do let rawty = forgetEnv (map fst env) (binderTy b)

347+ = do let rawty = forgetEnv (map fstEnv env) (binderTy b)

346 (_, kind) <- lift $ check ctxt env rawty

348 (_, kind) <- lift $ check ctxt env rawty

347 case kind of

349 case kind of

348 UType UniqueType -> do ns <- get

350 UType UniqueType -> do ns <- get

src/Idris/Core/Unify.hs+12−12

@@ -210,7 +210,7 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

210renameBinders env (x, t) = (x, renameBindersTm env t)

211

212renameBindersTm :: Env -> TT Name -> TT Name

213−renameBindersTm env tm = uniqueBinders (map fst env) tm

213+renameBindersTm env tm = uniqueBinders (map fstEnv env) tm

214 where

215 uniqueBinders env (Bind n b sc)

216 | n `elem` env

@@ -370,7 +370,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

370 = case compare (envPos 0 x env) (envPos 0 y env) of

371 LT -> do sc 1; checkCycle bnames (x, ty)

372 _ -> do sc 1; checkCycle bnames (y, tx)

373− where envPos i n ((n',_):env) | n == n' = i

373+ where envPos i n ((n',_,_):env) | n == n' = i

374 envPos i n (_:env) = envPos (i+1) n env

375 envPos _ _ _ = 100000

376 un' env fn bnames xtm@(P _ x _) tm

@@ -424,7 +424,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

424 = -- trace ("PATTERN RULE SOLVE: " ++ show (mv, tm, env, bindLams args (substEnv env tm))) $

425 checkCycle bnames (mv, eta [] $ bindLams args (substEnv env tm))

426 where rigid (V i) = True

427− rigid (P _ t _) = t `elem` map fst env &&

427+ rigid (P _ t _) = t `elem` map fstEnv env &&

428 not (holeIn env t || t `elem` holes)

429 rigid _ = False

430

@@ -450,14 +450,14 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

450 bindLams [] tm = tm

451 bindLams (a : as) tm = bindLam a (bindLams as tm)

452

453− bindLam (V i) tm = Bind (fst (env !! i))

453+ bindLam (V i) tm = Bind (fstEnv (env !! i))

454− (Lam (binderTy (snd (env !! i))))

454+ (Lam (binderTy (sndEnv (env !! i))))

455 tm

456 bindLam (P _ n ty) tm = Bind n (Lam ty) tm

457 bindLam _ tm = error "Can't happen [non rigid bindLam]"

458

459 substEnv [] tm = tm

460− substEnv ((n, t) : env) tm

460+ substEnv ((n, _, t) : env) tm

461 = substEnv env (substV (P Bound n (binderTy t)) tm)

462

463 -- remove any unnecessary lambdas (helps with interface

@@ -508,7 +508,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

508 un' env fn bnames (Bind x bx sx) (Bind y by sy)

509 | sameBinder bx by

510 = do h1 <- uB env bnames bx by

511− h2 <- un' ((x, bx) : env) False (((x,y),binderTy bx):bnames) sx sy

511+ h2 <- un' ((x, Rig0, bx) : env) False (((x,y),binderTy bx):bnames) sx sy

512 combine env bnames h1 h2

513 where sameBinder (Lam _) (Lam _) = True

514 sameBinder (Pi i _ _) (Pi i' _ _) = True

@@ -606,7 +606,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

606 P _ x _ -> x `elem` holes || patIn env x

607 _ -> False

608 inenv t = case t of

609− P _ x _ -> x `elem` (map fst env)

609+ P _ x _ -> x `elem` (map fstEnv env)

610 _ -> False

611

612 notFn t = injective t || metavar t || inenv t

@@ -770,17 +770,17 @@ recoverable (Bind _ (Lam _) sc) f = recoverable sc f

770recoverable f (Bind _ (Lam _) sc) = recoverable f sc

771recoverable x y = True

772

773−errEnv :: [(a, Binder b)] -> [(a, b)]

773+errEnv :: [(a, r, Binder b)] -> [(a, b)]

774−errEnv = map (\(x, b) -> (x, binderTy b))

774+errEnv = map (\(x, _, b) -> (x, binderTy b))

775

776holeIn :: Env -> Name -> Bool

777−holeIn env n = case lookup n env of

777+holeIn env n = case lookupBinder n env of

778 Just (Hole _) -> True

779 Just (Guess _ _) -> True

780 _ -> False

781

782patIn :: Env -> Name -> Bool

783−patIn env n = case lookup n env of

783+patIn env n = case lookupBinder n env of

784 Just (PVar _) -> True

785 Just (PVTy _) -> True

786 _ -> False

src/Idris/Core/WHNF.hs+6−5

@@ -73,12 +73,13 @@ whnfArgs' ctxt env tm

73 -- (so not in the external environment) so we need to instantiate

74 -- the name

75 Bind n b@(Pi _ ty _) sc ->

76+ -- TODO: Get RigCount from Pi

76− Bind n b (whnfArgs' ctxt ((n,b):env)

77+ Bind n b (whnfArgs' ctxt ((n,Rig0,b):env)

77 (subst n (P Bound n ty) sc))

78 (subst n (P Bound n ty) sc))

78 res -> tm

79 res -> tm

80−finalEntry :: (Name, Binder (TT Name)) -> (Name, Binder (TT Name))

81+finalEntry :: (Name, RigCount, Binder (TT Name)) -> (Name, RigCount, Binder (TT Name))

81−finalEntry (n, b) = (n, fmap finalise b)

82+finalEntry (n, r, b) = (n, r, fmap finalise b)

83do_whnf :: Context -> Env -> Term -> WHNF

84do_whnf :: Context -> Env -> Term -> WHNF

84do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

85do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

@@ -93,11 +94,11 @@ do_whnf ctxt genv tm = eval (WEnv 0 []) [] tm

93 eval (WEnv d env) ((tm, tenv) : stk) (Bind n b@(Lam _) sc)

94 eval (WEnv d env) ((tm, tenv) : stk) (Bind n b@(Lam _) sc)

94 = eval (WEnv d ((tm, tenv) : env)) stk sc

95 = eval (WEnv d ((tm, tenv) : env)) stk sc

95 eval wenv@(WEnv d env) stk (Bind n b sc) -- stk must be empty if well typed

96 eval wenv@(WEnv d env) stk (Bind n b sc) -- stk must be empty if well typed

96− =let n' = uniqueName n (map fst genv) in

97+ =let n' = uniqueName n (map fstEnv genv) in

97 WBind n' (fmap (\t -> (t, wenv)) b) (sc, WEnv (d + 1) env)

98 WBind n' (fmap (\t -> (t, wenv)) b) (sc, WEnv (d + 1) env)

99 eval env stk (P nt n ty)

100 eval env stk (P nt n ty)

100− | Just (Let t v) <- lookup n genv = eval env stk v

101+ | Just (Let t v) <- lookupBinder n genv = eval env stk v

101 eval env stk (P nt n ty) = apply env nt n ty stk

102 eval env stk (P nt n ty) = apply env nt n ty stk

102 eval env stk (App _ f a) = eval env ((a, env) : stk) f

103 eval env stk (App _ f a) = eval env ((a, env) : stk) f

103 eval env stk (Constant c) = unload (WConstant c) stk

104 eval env stk (Constant c) = unload (WConstant c) stk

src/Idris/Delaborate.hs+2−2

@@ -527,13 +527,13 @@ pprintErr' i (ElabScriptDebug msg tm holes) =

527 indented (vsep (map ppHole holes)) <> line <> line <>

528 text "Term: " <> indented (pprintTT [] tm)

529

530− where ppHole :: (Name, Type, Env) -> Doc OutputAnnotation

530+ where ppHole :: (Name, Type, [(Name, Binder Type)]) -> Doc OutputAnnotation

531 ppHole (hn, goal, env) =

532 ppAssumptions [] (reverse env) <>

533 text "----------------------------------" <> line <>

534 bindingOf hn False <+> text ":" <+>

535 pprintTT (map fst (reverse env)) goal <> line

536− ppAssumptions :: [Name] -> Env -> Doc OutputAnnotation

536+ ppAssumptions :: [Name] -> [(Name, Binder Type)] -> Doc OutputAnnotation

537 ppAssumptions ns [] = empty

538 ppAssumptions ns ((n, b) : rest) =

539 bindingOf n False <+>

src/Idris/Elab/Clause.hs+3−3

@@ -644,14 +644,14 @@ checkPossibles _ _ _ _ [] = return []

644

645findUnique :: Context -> Env -> Term -> [Name]

646findUnique ctxt env (Bind n b sc)

647− = let rawTy = forgetEnv (map fst env) (binderTy b)

647+ = let rawTy = forgetEnv (map fstEnv env) (binderTy b)

648 uniq = case check ctxt env rawTy of

649 OK (_, UType UniqueType) -> True

650 OK (_, UType NullType) -> True

651 OK (_, UType AllTypes) -> True

652 _ -> False in

653− if uniq then n : findUnique ctxt ((n, b) : env) sc

653+ if uniq then n : findUnique ctxt ((n, Rig0, b) : env) sc

654− else findUnique ctxt ((n, b) : env) sc

654+ else findUnique ctxt ((n, Rig0, b) : env) sc

655findUnique _ _ _ = []

656

657getUnfolds (UnfoldIface n ns : _) = Just (n, ns)

src/Idris/Elab/Rewrite.hs+1−1

@@ -77,7 +77,7 @@ elabRewrite elab ist fc substfn_in rule sc_in newg

77 let pred = PLam fc rname fc Placeholder

78 (delab ist pred_tt)

79 let rewrite = stripImpls $

80− addImplBound ist (map fst env) (PApp fc (PRef fc [] substfn)

80+ addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] substfn)

81 [pexp pred, pexp rule, pexp sc])

82-- trace ("LHS: " ++ show l ++ "\n" ++

83-- "RHS: " ++ show r ++ "\n" ++

src/Idris/Elab/Term.hs+30−30

@@ -227,7 +227,7 @@ goal_polymorphic =

227 do ty <- goal

228 case ty of

229 P _ n _ -> do env <- get_env

230− case lookup n env of

230+ case lookupBinder n env of

231 Nothing -> return False

232 _ -> return True

233 _ -> return False

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

351 notDelay _ = True

352

353 local f = do e <- get_env

354− return (f `elem` map fst e)

354+ return (f `elem` map fstEnv e)

355

356 -- | Is a constant a type?

357 constType :: Const -> Bool

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

760 (ivs' \\ ivs)

761 -- HACK: If the name leaks into its type, it may leak out of

762 -- scope outside, so substitute in the outer scope.

763− expandLet n (case lookup n env of

763+ expandLet n (case lookupBinder n env of

764 Just (Let t v) -> v

765 other -> error ("Value not a let binding: " ++ show other))

766 solve

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

813 fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi Nothing xt RType) (fnTy xs ret)

814

815 localVar env (PRef _ _ x)

816− = case lookup x env of

816+ = case lookupBinder x env of

817 Just _ -> Just x

818 _ -> Nothing

819 localVar env _ = Nothing

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

856 && isTConName f (tt_ctxt ist)) $

857 lift $ tfail $ Msg ("No explicit types on left hand side: " ++ show tm)

858-- trace (show (f, args_in, args)) $

859− if (f `elem` map fst env && length args == 1 && length args_in == 1)

859+ if (f `elem` map fstEnv env && length args == 1 && length args_in == 1)

860 then -- simple app, as below

861 do simple_app False

862 (elabE (ina { e_isfn = True }) (Just fc) (PRef ffc hls f))

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

904 imp <- if (e_isfn ina) then

905 do guess <- get_guess

906 env <- get_env

907− case safeForgetEnv (map fst env) guess of

907+ case safeForgetEnv (map fstEnv env) guess of

908 Nothing ->

909 return []

910 Just rguess -> do

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

963

964 checkIfInjective n = do

965 env <- get_env

966− case lookup n env of

966+ case lookupBinder n env of

967 Nothing -> return ()

968 Just b ->

969 case unApply (whnf (tt_ctxt ist) env (binderTy b)) of

@@ -1079,13 +1079,13 @@ elab ist info emode opts fn tm

1079 -- unnecessarily (can only do this for unique things, since we

1080 -- assume they don't appear implicitly in types)

1081 ptm <- get_term

1082− let inOpts = (filter (/= scvn) (map fst args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

1082+ let inOpts = (filter (/= scvn) (map fstEnv args)) \\ (concatMap (\x -> allNamesIn (snd x)) opts)

1083

1084 let argsDropped = filter (isUnique envU)

1085 (nub $ allNamesIn scr ++ inApp ptm ++

1086 inOpts)

1087

1088− let args' = filter (\(n, _) -> n `notElem` argsDropped) args

1088+ let args' = filter (\(n, _, _) -> n `notElem` argsDropped) args

1089

1090 attack

1091 cname' <- defer argsDropped (mkN (mkCaseName fc fn))

@@ -1136,8 +1136,8 @@ elab ist info emode opts fn tm

1136 Just u -> u

1137 _ -> False

1138

1139− getKind env (n, _)

1139+ getKind env (n, _, _)

1140− = case lookup n env of

1140+ = case lookupBinder n env of

1141 Nothing -> return (n, False) -- can't happen, actually...

1142 Just b ->

1143 do ty <- get_type (forget (binderTy b))

@@ -1220,13 +1220,13 @@ elab ist info emode opts fn tm

1220 loadState

1221 updateAux (\aux -> aux { highlighting = hs })

1222

1223− let quoted = fmap (explicitNames . binderVal) $ lookup nTm env

1223+ let quoted = fmap (explicitNames . binderVal) $ lookupBinder nTm env

1224 isRaw = case unApply (normaliseAll ctxt env finalTy) of

1225 (P _ n _, []) | n == reflm "Raw" -> True

1226 _ -> False

1227 case quoted of

1228 Just q -> do ctxt <- get_context

1229− (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, Lam Erased) | uq <- unquoteNames] (forget q) q

1229+ (q', _, _) <- lift $ recheck (constraintNS info) ctxt [(uq, Rig0, Lam Erased) | uq <- unquoteNames] (forget q) q

1230 if pattern

1231 then if isRaw

1232 then reflectRawQuotePattern unquoteNames (forget q')

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

1255 elab' ina fc (PQuoteName n True nfc) =

1256 do ctxt <- get_context

1257 env <- get_env

1258− case lookup n env of

1258+ case lookupBinder n env of

1259 Just _ -> do fill $ reflectName n

1260 solve

1261 highlightSource nfc (AnnBoundName n False)

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

1324 env <- get_env

1325 ctxt <- get_context

1326 let v = fmap (normaliseAll ctxt env . finalise . binderVal)

1327− (lookup n env)

1327+ (lookupBinder n env)

1328 loadState -- we have the highlighting - re-elaborate the value

1329 elab' ina fc tm

1330 case v of

@@ -1347,9 +1347,9 @@ elab ist info emode opts fn tm

1347 delayElab pri t

1348 = updateAux (\e -> e { delayed_elab = delayed_elab e ++ [(pri, t)] })

1349

1350− isScr :: PTerm -> (Name, Binder Term) -> (Name, (Bool, Binder Term))

1350+ isScr :: PTerm -> (Name, RigCount, Binder Term) -> (Name, (Bool, Binder Term))

1351− isScr (PRef _ _ n) (n', b) = (n', (n == n', b))

1351+ isScr (PRef _ _ n) (n', _, b) = (n', (n == n', b))

1352− isScr _ (n', b) = (n', (False, b))

1352+ isScr _ (n', _, b) = (n', (False, b))

1353

1354 caseBlock :: FC -> Name

1355 -> PTerm -- original scrutinee

@@ -1449,8 +1449,8 @@ elab ist info emode opts fn tm

1449 mkDelay env (PAlternative ms b xs) = PAlternative ms b (map (mkDelay env) xs)

1450 mkDelay env t

1451 = let fc = fileFC "Delay" in

1452− addImplBound ist (map fst env) (PApp fc (PRef fc [] (sUN "Delay"))

1452+ addImplBound ist (map fstEnv env) (PApp fc (PRef fc [] (sUN "Delay"))

1453− [pexp t])

1453+ [pexp t])

1454

1455

1456 -- Don't put implicit coercions around applications which are marked

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

1475 case fullApp tm of

1476 -- if f is global, leave it alone because we've already

1477 -- expanded it to the right arity

1478− PApp fc ftm@(PRef _ _ f) args | Just aty <- lookup f env ->

1478+ PApp fc ftm@(PRef _ _ f) args | Just aty <- lookupBinder f env ->

1479 do let a = length (getArgTys (normalise (tt_ctxt ist) env (binderTy aty)))

1480 return (mkPApp fc a ftm args)

1481 _ -> return tm

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

1528 mkCoerce env (PAlternative ms aty tms) n

1529 = PAlternative ms aty (map (\t -> mkCoerce env t n) tms)

1530 mkCoerce env t n = let fc = maybe (fileFC "Coercion") id (highestFC t) in

1531− addImplBound ist (map fst env)

1531+ addImplBound ist (map fstEnv env)

1532 (PApp fc (PRef fc [] n) [pexp (PCoerced t)])

1533

1534 -- | Elaborate the arguments to a function

@@ -1647,7 +1647,7 @@ pruneByType imp env t goalty c as

1647 locallyBound [] = Nothing

1648 locallyBound (t:ts)

1649 | Just n <- getName t,

1650− n `elem` map fst env = Just t

1650+ n `elem` map fstEnv env = Just t

1651 | otherwise = locallyBound ts

1652 getName (PRef _ _ n) = Just n

1653 getName (PApp _ (PRef _ _ (UN l)) [_, _, arg]) -- ignore Delays

@@ -1800,7 +1800,7 @@ isPlausible ist var env n ty

1800findHighlight :: Name -> ElabD OutputAnnotation

1801findHighlight n = do ctxt <- get_context

1802 env <- get_env

1803− case lookup n env of

1803+ case lookupBinder n env of

1804 Just _ -> return $ AnnBoundName n False

1805 Nothing -> case lookupTyExact n ctxt of

1806 Just _ -> return $ AnnName n Nothing Nothing Nothing

@@ -1820,7 +1820,7 @@ solveAuto ist fn ambigok (n, failc)

1820 when (not isg) $

1821 proofSearch' ist True ambigok 100 True Nothing fn [] [])

1822 (lift $ Error (addLoc failc

1823− (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env))))

1823+ (CantSolveGoal g (map (\(n, _, b) -> (n, binderTy b)) env))))

1824 return ()

1825 where addLoc (FailContext fc f x : prev) err

1826 = At fc (ElaboratingArg f x

@@ -1893,7 +1893,7 @@ case_ ind autoSolve ist fn tm = do

1893 focus valn

1894 elab ist toplevel ERHS [] (sMN 0 "tac") tm

1895 env <- get_env

1896− let (Just binding) = lookup letn env

1896+ let (Just binding) = lookupBinder letn env

1897 let val = binderVal binding

1898 if ind then induction (forget val)

1899 else casetac (forget val)

@@ -2456,11 +2456,11 @@ runTac :: Bool -> IState -> Maybe FC -> Name -> PTactic -> ElabD ()

2456runTac autoSolve ist perhapsFC fn tac

2457 = do env <- get_env

2458 g <- goal

2459− let tac' = fmap (addImplBound ist (map fst env)) tac

2459+ let tac' = fmap (addImplBound ist (map fstEnv env)) tac

2460 if autoSolve

2461 then runT tac'

2462 else no_errors (runT tac')

2463− (Just (CantSolveGoal g (map (\(n, b) -> (n, binderTy b)) env)))

2463+ (Just (CantSolveGoal g (map (\(n, _, b) -> (n, binderTy b)) env)))

2464 where

2465 runT (Intro []) = do g <- goal

2466 attack; intro (bname g)

@@ -2490,7 +2490,7 @@ runTac autoSolve ist perhapsFC fn tac

2490 tryAll tacs

2491 when autoSolve solveAll

2492 where envArgs n = do e <- get_env

2493− case lookup n e of

2493+ case lookupBinder n e of

2494 Just t -> return $ map (const False)

2495 (getArgTys (binderTy t))

2496 _ -> return []

@@ -2508,7 +2508,7 @@ runTac autoSolve ist perhapsFC fn tac

2508 where isImp (PImp _ _ _ _ _) = True

2509 isImp _ = False

2510 envArgs n = do e <- get_env

2511− case lookup n e of

2511+ case lookupBinder n e of

2512 Just t -> return $ map (const False)

2513 (getArgTys (binderTy t))

2514 _ -> return []

src/Idris/Elab/Utils.hs+2−2

@@ -292,13 +292,13 @@ getUniqueUsed ctxt tm = execState (getUniq [] [] tm) []

292 where

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

294 getUniq env us (Bind n b sc)

295− = let uniq = case check ctxt env (forgetEnv (map fst env) (binderTy b)) of

295+ = let uniq = case check ctxt env (forgetEnv (map fstEnv env) (binderTy b)) of

296 OK (_, UType UniqueType) -> True

297 OK (_, UType NullType) -> True

298 OK (_, UType AllTypes) -> True

299 _ -> False in

300 do getUniqB env us b

301− getUniq ((n,b):env) ((n, uniq):us) sc

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

302 getUniq env us (App _ f a) = do getUniq env us f; getUniq env us a

303 getUniq env us (V i)

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

src/Idris/ProofSearch.hs+4−4

@@ -49,7 +49,7 @@ trivialHoles psnames ok elab ist

49 return ()) True

50 where

51 tryAll [] = fail "No trivial solution"

52− tryAll ((x, b):xs)

52+ tryAll ((x, _, b):xs)

53 = do -- if type of x has any holes in it, move on

54 hs <- get_holes

55 let badhs = hs -- filter (flip notElem holesOK) hs

@@ -85,7 +85,7 @@ trivialTCs ok elab ist

85 return ()) True

86 where

87 tryAll [] = fail "No trivial solution"

88− tryAll ((x, b):xs)

88+ tryAll ((x, _, b):xs)

89 = do -- if type of x has any holes in it, move on

90 hs <- get_holes

91 let badhs = hs -- filter (flip notElem holesOK) hs

@@ -123,7 +123,7 @@ cantSolveGoal :: ElabD a

123cantSolveGoal = do g <- goal

124 env <- get_env

125 lift $ tfail $

126− CantSolveGoal g (map (\(n,b) -> (n, binderTy b)) env)

126+ CantSolveGoal g (map (\(n,_,b) -> (n, binderTy b)) env)

127

128proofSearch :: Bool -- ^ recursive search (False for 'refine')

129 -> Bool -- ^ invoked from a tactic proof. If so, making new metavariables is meaningless, and there should be an error reported instead.

@@ -300,7 +300,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

300 tryLocals d locs tys env

301

302 tryLocals d locs tys [] = fail "Locals failed"

303− tryLocals d locs tys ((x, t) : xs)

303+ tryLocals d locs tys ((x, _, t) : xs)

304 | x `elem` locs || x `notElem` psnames = tryLocals d locs tys xs

305 | otherwise = try' (tryLocal d (x : locs) tys x t)

306 (tryLocals d locs tys xs) True

src/Idris/Prover.hs+12−12

@@ -82,8 +82,8 @@ assumptionNames e

82 = case envAtFocus (proof e) of

83 OK env -> names env

84 where names [] = []

85− names ((MN _ _, _) : bs) = names bs

85+ names ((MN _ _, _, _) : bs) = names bs

86− names ((n, _) : bs) = show n : names bs

86+ names ((n, _, _) : bs) = show n : names bs

88prove :: Bool -> ElabInfo -> Ctxt OptInfo -> Context -> Bool -> Name -> Type -> Idris ()

89prove mode info opt ctxt lit n ty

@@ -174,18 +174,18 @@ dumpState ist inElab menv ps | (h : hs) <- holes ps = do

174 delab ist t

175

176 assumptionNames :: Env -> [Name]

177− assumptionNames = map fst

177+ assumptionNames = map fstEnv

178

179 prettyPs :: Bool -> Binder Type -> [(Name, Bool)] -> Env -> Doc OutputAnnotation

180 prettyPs all g bnd [] = empty

181− prettyPs all g bnd ((n@(MN _ r), _) : bs)

181+ prettyPs all g bnd ((n@(MN _ r), _, _) : bs)

182 | not all && r == txt "rewrite_rule" = prettyPs all g ((n, False):bnd) bs

183− prettyPs all g bnd ((n@(MN _ _), _) : bs)

183+ prettyPs all g bnd ((n@(MN _ _), _, _) : bs)

184 | not (all || n `elem` freeEnvNames bs || n `elem` goalNames g) = prettyPs all g bnd bs

185− prettyPs all g bnd ((n, Let t v) : bs) =

185+ prettyPs all g bnd ((n, _, Let t v) : bs) =

186 line <> bindingOf n False <+> text "=" <+> tPretty bnd v <+> colon <+>

187 align (tPretty bnd t) <> prettyPs all g ((n, False):bnd) bs

188− prettyPs all g bnd ((n, b) : bs) =

188+ prettyPs all g bnd ((n, _, b) : bs) =

189 line <> bindingOf n False <+> colon <+>

190 align (tPretty bnd (binderTy b)) <> prettyPs all g ((n, False):bnd) bs

191

@@ -227,7 +227,7 @@ dumpState ist inElab menv ps | (h : hs) <- holes ps = do

227 nest nestingSize (align . cat . punctuate (text ",") . map (`bindingOf` False) $ hs)

228

229 freeEnvNames :: Env -> [Name]

230− freeEnvNames = concatMap (\(n, b) -> freeNames (Bind n b Erased))

230+ freeEnvNames = concatMap (\(n, _, b) -> freeNames (Bind n b Erased))

231

232lifte :: ElabState EState -> ElabD a -> Idris a

233lifte st e = do (v, _) <- elabStep st e

@@ -468,7 +468,7 @@ ploop fn d prompt prf e h

468 (ploop fn d prompt prf e h')

469

470

471−envCtxt env ctxt = foldl (\c (n, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

471+envCtxt env ctxt = foldl (\c (n, _, b) -> addTyDecl n Bound (binderTy b) c) ctxt env

472

473checkNameType :: ElabState EState -> [String] -> Name -> Idris (Bool, ElabState EState, Bool, [String], Either Err (Idris ()))

474checkNameType e prf n = do

@@ -478,7 +478,7 @@ checkNameType e prf n = do

478 idrisCatch (do

479 let OK env = envAtFocus (proof e)

480 ctxt' = envCtxt env ctxt

481− bnd = map (\x -> (fst x, False)) env

481+ bnd = map (\x -> (fstEnv x, False)) env

482 ist' = ist { tt_ctxt = ctxt' }

483 putIState ist'

484 -- Unlike the REPL, metavars have no special treatment, to

@@ -505,7 +505,7 @@ checkType e prf t = do

505 action = case tm of

506 TType _ ->

507 iPrintTermWithType (prettyImp ppo (PType emptyFC)) type1Doc

508− _ -> let bnd = map (\x -> (fst x, False)) env in

508+ _ -> let bnd = map (\x -> (fstEnv x, False)) env in

509 iPrintTermWithType (pprintPTerm ppo bnd [] infixes (delab ist tm))

510 (pprintPTerm ppo bnd [] infixes (delab ist ty))

511 putIState ist

@@ -522,7 +522,7 @@ evalTerm e prf t = withErrorReflection $

522 let OK env = envAtFocus (proof e)

523 ctxt' = envCtxt env ctxt

524 ist' = ist { tt_ctxt = ctxt' }

525− bnd = map (\x -> (fst x, False)) env

525+ bnd = map (\x -> (fstEnv x, False)) env

526 putIState ist'

527 (tm, ty) <- elabVal (recinfo proverfc) ERHS t

528 let tm' = force (normaliseAll ctxt' env tm)

src/Idris/Reflection.hs+4−2

@@ -804,7 +804,7 @@ reflectUExp (UVal i) = reflCall "UVal" [RConstant (I i)]

804

805-- | Reflect the environment of a proof into a List (TTName, Binder TT)

806reflectEnv :: Env -> Raw

807−reflectEnv = foldr consToEnvList emptyEnvList

807+reflectEnv = foldr consToEnvList emptyEnvList . envBinders

808 where

809 consToEnvList :: (Name, Binder Term) -> Raw -> Raw

810 consToEnvList (n, b) l

@@ -823,8 +823,10 @@ reflectEnv = foldr consToEnvList emptyEnvList

823 emptyEnvList = raw_apply (Var (sNS (sUN "Nil") ["List", "Prelude"]))

824 [envTupleType]

825

826+-- Reflected environments don't get the RigCount (for the moment, at least)

826reifyEnv :: Term -> ElabD Env

827reifyEnv :: Term -> ElabD Env

827−reifyEnv = reifyList (reifyPair reifyTTName (reifyTTBinder reifyTT (reflm "TT")))

828+reifyEnv tm = do preEnv <- reifyList (reifyPair reifyTTName (reifyTTBinder reifyTT (reflm "TT"))) tm

829+ return $ map (\(n, b) -> (n, Rig0, b)) preEnv

828

830

829-- | Reflect an error into the internal datatype of Idris -- TODO

831-- | Reflect an error into the internal datatype of Idris -- TODO

830rawBool :: Bool -> Raw

832rawBool :: Bool -> Raw

src/Idris/TypeSearch.hs+1−1

@@ -439,7 +439,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

439 unifyQueue state [] = return state

440 unifyQueue state ((ty1, ty2) : queue) = do

441 --trace ("go: \n" ++ show state) True `seq` return ()

442− res <- tcToMaybe $ match_unify ctxt [ (n, Pi Nothing ty (TType (UVar [] 0))) | (n, ty) <- holes state]

442+ res <- tcToMaybe $ match_unify ctxt [ (n, Rig0, Pi Nothing ty (TType (UVar [] 0))) | (n, ty) <- holes state]

443 (ty1, Nothing)

444 (ty2, Nothing) [] (map fst $ holes state) []

445 (state', queueAdditions) <- resolveUnis res state