e3daf28 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Add RigCount to environment

commite3daf2882dc7125820a0c44fc9ca15ce5e04f6d0 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateSat 17 Dec 2016, 13:08 (10 years ago) parent17f0899

18 files changed+152−134

compare with master

unifiedsplit

src/Idris/Core/Elaborate.hs+7−7 src/Idris/Core/Evaluate.hs+7−7 src/Idris/Core/Execute.hs+1−1 src/Idris/Core/ProofState.hs+12−12 src/Idris/Core/ProofTerm.hs+7−7 src/Idris/Core/TT.hs+24−11 src/Idris/Core/Typecheck.hs+17−15 src/Idris/Core/Unify.hs+12−12 src/Idris/Core/WHNF.hs+6−5 src/Idris/Delaborate.hs+2−2 src/Idris/Elab/Clause.hs+3−3 src/Idris/Elab/Rewrite.hs+1−1 src/Idris/Elab/Term.hs+30−30 src/Idris/Elab/Utils.hs+2−2 src/Idris/ProofSearch.hs+4−4 src/Idris/Prover.hs+12−12 src/Idris/Reflection.hs+4−2 src/Idris/TypeSearch.hs+1−1

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

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

9999setNextName = do env <- get_env

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

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

102− initNextNameFrom (pargs ++ map fst env)

102+ initNextNameFrom (pargs ++ map fstEnv env)

103103

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

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

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

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

469469patvar n = do env <- get_env

470470 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

472472 else do n' <- case hs of

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

474474 else unique_hole n

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

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

482482patvar' n = do env <- get_env

483483 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

485485 else processTactic' (PatVar n)

486486

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

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

580580 then finalise ty

581581 else whnfArgs ctxt env (finalise ty)

582582 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)

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

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

586586 let n = length (filter not imps)

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

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

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

606606 env <- get_env

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

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

608608 when i (movelast n)

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

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

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

869869 case reverse ps' of

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

871871 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

873873 lift $ tfail $

874874 case err of

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

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

10131013 getHoleInfo h = do focus h

10141014 g <- goal

10151015 env <- get_env

1016− return (h, g, env)

1016+ return (h, g, envBinders env)

10171017

10181018qshow :: Fails -> String

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

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

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

197197

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

199199

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

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

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

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

202202

203203bindEnv :: EnvTT n -> TT n -> TT n

204204bindEnv [] tm = tm

205−bindEnv ((n, 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)

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

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

207207

208208unbindEnv :: EnvTT n -> TT n -> TT n

209209unbindEnv [] tm = tm

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

282282 | otherwise = cases_compiletime cd

283283

284284 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

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

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

288288 (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

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

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

339339 = 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)

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

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

343343 where vbind env t

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

11811181 _ -> []

11821182

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

1184−lookupTyEnv n env = li n 0 env where

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

11851185 li n i [] = Nothing

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

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

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

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

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

115115 return $ normalise ctxt env' tm

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

117− return (n, Let Erased v')

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

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

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

120120

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

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

129129 ") -------\n " ++

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

131131 where showPs env [] = ""

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

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

133133 = " " ++ show n ++ " : " ++

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

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

136136 "\n" ++ showPs env bs

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

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

138138 = " " ++ show n ++ " : " ++

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

140140 "\n" ++ showPs env bs

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

160160 prettyGoal ps b = prettyEnv ps $ binderTy b

161161

162162 prettyPs env [] = empty

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

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

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

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

166166 nest nestingSize (prettyPs env bs))

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

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

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

169169 nest nestingSize (prettyPs env bs))

170170

171171holeName i = sMN i "hole"

172172

173173qshow :: 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)

175175

176176match_unify' :: Context -> Env ->

177177 (TT Name, Maybe Provenance) ->

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

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

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

365365 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)

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

368368 cl env t = t

369369

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

463463

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

465465defer 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

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

468468 ps { usedns = n : usedns ps,

469469 holes = hs \\ [x] })

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

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

473473 where

474474 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)

476476

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

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

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

479479

480480-- 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' =

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

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

490490 where

491− getP n = case lookup n env of

491+ getP n = case lookupBinder n env of

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

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

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

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

914914

915915updateEnv [] e = e

916916updateEnv ns [] = []

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

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

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

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

919919

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

921921updateProv ns p = p

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

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

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

8585 fh' env path (Bind x b sc)

8686 | 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)

8888 fh' _ _ _ = Nothing

8989

9090 fhB env path (Let t v)

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

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

256256updateEnv [] e = e

257257updateEnv 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

259259

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

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

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

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

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

286286 = 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))

288288 (updateSolvedTerm xs sub)

289289 (ups ++ xs)

290290

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

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

298298 | same h n = return $ GD env b

299299 | otherwise

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

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

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

302302 | otherwise

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

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

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

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

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

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

338338 = do -- binder first

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

340340 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

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

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

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

345345 | 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

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

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

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

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

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

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

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

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

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

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

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

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

3737 , addAlist, addBinder, addDef, allTTNames, arity, bindAll

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

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

5050 , toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName

5151 , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm

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

5253 ) where

5354

5455import Util.Pretty hiding (Str)

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

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

10651066 pretty _ = text "test"

10661067

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

1068+data RigCount = Rig0 | Rig1 | RigW

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

1070+

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

10681081

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

10701083 d_typetag :: Int,

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

15721585 prettySe p env (V i) debug

15731586 | i < length env =

15741587 if debug then

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

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

15761589 else

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

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

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

15801593 | 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

15821595 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

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

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

15861599 prettySe p env (Proj x i) debug =

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

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

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

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

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

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

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

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

16261639 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

16281641 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

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

16311644 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

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

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

16351648 se p env (Constant c) = show c

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

16861699weakenEnv :: EnvTT n -> EnvTT n

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

16881701 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

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

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

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

16931706

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

16951708weakenTmEnv :: 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))

16971710

16981711refsIn :: TT Name -> [Name]

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

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

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

2525

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

2727convertsC ctxt env x y =

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

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

2929 c1 <- convEq ctxt hs x y

3030 if c1 then return ()

3131 else

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

3838

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

4040converts ctxt env x y

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

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

4242 case convEq' ctxt hs x y of

4343 OK True -> return ()

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

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

4848 (finalise (normalise ctxt env x))

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

5050

51−isHole (n, Hole _) = True

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

5252isHole _ = False

5353

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

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

5555

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

5757isType 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

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

114114 -- special case to reduce constraintss

115115 = 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

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

118− _ -> uniqueBinders (map fst env)

118+ _ -> uniqueBinders (map fstEnv env)

119119 $ case normalise ctxt env fty of

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

121121 _ -> normalise ctxt env fty

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

135135 t -> lift $ tfail $ NonFunctionType fv fty

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

137137 = 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

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

140− _ -> uniqueBinders (map fst env)

140+ _ -> uniqueBinders (map fstEnv env)

141141 $ case normalise ctxt env fty of

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

143143 _ -> normalise ctxt env fty

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

186186 let maxu = case lvl of

187187 Nothing -> UVar tcns v

188188 Just v' -> v'

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

189+ -- TODO: Get RigCount from Pi

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

190191

191192-- convertsC ctxt env st (TType maxu)

192193-- 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

200201 put (v, ULE su maxu :

201202 ULE tu maxu : cs)

202203 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')

204205 (pToV n tv), k')

205206 (un, un') ->

206207 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')

208209 (pToV n tv), k')

209210

210211 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

224225

225226 chk u lvl env (RBind n b sc)

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

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

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

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

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

229231 where checkBinder (Lam t)

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

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

316318 isVar _ = False

317319

318320 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))

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

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

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

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

336338 case b of

337339 Let t v -> chkBinders env v

338340 _ -> return ()

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

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

340342 chkBinders env t = return ()

341343

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

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

344346 chkBinderName env n b

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

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

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

347349 case kind of

348350 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 =

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

211211

212212renameBindersTm :: Env -> TT Name -> TT Name

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

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

214214 where

215215 uniqueBinders env (Bind n b sc)

216216 | n `elem` env

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

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

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

372372 _ -> 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

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

375375 envPos _ _ _ = 100000

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

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

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

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

426426 where rigid (V i) = True

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

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

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

429429 rigid _ = False

430430

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

450450 bindLams [] tm = tm

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

452452

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

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

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

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

455455 tm

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

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

458458

459459 substEnv [] tm = tm

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

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

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

462462

463463 -- remove any unnecessary lambdas (helps with interface

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

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

509509 | sameBinder bx by

510510 = 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

512512 combine env bnames h1 h2

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

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

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

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

607607 _ -> False

608608 inenv t = case t of

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

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

610610 _ -> False

611611

612612 notFn t = injective t || metavar t || inenv t

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

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

771771recoverable x y = True

772772

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

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

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

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

775775

776776holeIn :: Env -> Name -> Bool

777−holeIn env n = case lookup n env of

777+holeIn env n = case lookupBinder n env of

778778 Just (Hole _) -> True

779779 Just (Guess _ _) -> True

780780 _ -> False

781781

782782patIn :: Env -> Name -> Bool

783−patIn env n = case lookup n env of

783+patIn env n = case lookupBinder n env of

784784 Just (PVar _) -> True

785785 Just (PVTy _) -> True

786786 _ -> False

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

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

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

7474 -- the name

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

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

76+ -- TODO: Get RigCount from Pi

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

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

7879 res -> tm

7980

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

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

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

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

8283

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

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

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

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

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

9596 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

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

9899

99100 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

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

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

103104 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) =

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

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

529529

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

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

531531 ppHole (hn, goal, env) =

532532 ppAssumptions [] (reverse env) <>

533533 text "----------------------------------" <> line <>

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

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

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

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

537537 ppAssumptions ns [] = empty

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

539539 bindingOf n False <+>

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

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

644644

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

646646findUnique ctxt env (Bind n b sc)

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

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

648648 uniq = case check ctxt env rawTy of

649649 OK (_, UType UniqueType) -> True

650650 OK (_, UType NullType) -> True

651651 OK (_, UType AllTypes) -> True

652652 _ -> False in

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

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

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

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

655655findUnique _ _ _ = []

656656

657657getUnfolds (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

7777 let pred = PLam fc rname fc Placeholder

7878 (delab ist pred_tt)

7979 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)

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

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

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

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

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

227227 do ty <- goal

228228 case ty of

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

230− case lookup n env of

230+ case lookupBinder n env of

231231 Nothing -> return False

232232 _ -> return True

233233 _ -> return False

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

351351 notDelay _ = True

352352

353353 local f = do e <- get_env

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

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

355355

356356 -- | Is a constant a type?

357357 constType :: Const -> Bool

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

760760 (ivs' \\ ivs)

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

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

763− expandLet n (case lookup n env of

763+ expandLet n (case lookupBinder n env of

764764 Just (Let t v) -> v

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

766766 solve

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

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

814814

815815 localVar env (PRef _ _ x)

816− = case lookup x env of

816+ = case lookupBinder x env of

817817 Just _ -> Just x

818818 _ -> Nothing

819819 localVar env _ = Nothing

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

856856 && isTConName f (tt_ctxt ist)) $

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

858858-- 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)

860860 then -- simple app, as below

861861 do simple_app False

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

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

904904 imp <- if (e_isfn ina) then

905905 do guess <- get_guess

906906 env <- get_env

907− case safeForgetEnv (map fst env) guess of

907+ case safeForgetEnv (map fstEnv env) guess of

908908 Nothing ->

909909 return []

910910 Just rguess -> do

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

963963

964964 checkIfInjective n = do

965965 env <- get_env

966− case lookup n env of

966+ case lookupBinder n env of

967967 Nothing -> return ()

968968 Just b ->

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

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

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

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

10811081 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)

10831083

10841084 let argsDropped = filter (isUnique envU)

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

10861086 inOpts)

10871087

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

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

10891089

10901090 attack

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

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

11361136 Just u -> u

11371137 _ -> False

11381138

1139− getKind env (n, _)

1140− = case lookup n env of

1139+ getKind env (n, _, _)

1140+ = case lookupBinder n env of

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

11421142 Just b ->

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

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

12201220 loadState

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

12221222

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

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

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

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

12261226 _ -> False

12271227 case quoted of

12281228 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

12301230 if pattern

12311231 then if isRaw

12321232 then reflectRawQuotePattern unquoteNames (forget q')

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

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

12561256 do ctxt <- get_context

12571257 env <- get_env

1258− case lookup n env of

1258+ case lookupBinder n env of

12591259 Just _ -> do fill $ reflectName n

12601260 solve

12611261 highlightSource nfc (AnnBoundName n False)

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

13241324 env <- get_env

13251325 ctxt <- get_context

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

1327− (lookup n env)

1327+ (lookupBinder n env)

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

13291329 elab' ina fc tm

13301330 case v of

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

13471347 delayElab pri t

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

13491349

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

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

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

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

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

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

13531353

13541354 caseBlock :: FC -> Name

13551355 -> PTerm -- original scrutinee

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

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

14501450 mkDelay env t

14511451 = let fc = fileFC "Delay" in

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

1453− [pexp t])

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

1453+ [pexp t])

14541454

14551455

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

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

14751475 case fullApp tm of

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

14771477 -- 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 ->

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

14801480 return (mkPApp fc a ftm args)

14811481 _ -> return tm

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

15281528 mkCoerce env (PAlternative ms aty tms) n

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

15301530 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)

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

15331533

15341534 -- | Elaborate the arguments to a function

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

16471647 locallyBound [] = Nothing

16481648 locallyBound (t:ts)

16491649 | Just n <- getName t,

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

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

16511651 | otherwise = locallyBound ts

16521652 getName (PRef _ _ n) = Just n

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

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

18001800findHighlight :: Name -> ElabD OutputAnnotation

18011801findHighlight n = do ctxt <- get_context

18021802 env <- get_env

1803− case lookup n env of

1803+ case lookupBinder n env of

18041804 Just _ -> return $ AnnBoundName n False

18051805 Nothing -> case lookupTyExact n ctxt of

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

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

18201820 when (not isg) $

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

18221822 (lift $ Error (addLoc failc

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

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

18241824 return ()

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

18261826 = At fc (ElaboratingArg f x

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

18931893 focus valn

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

18951895 env <- get_env

1896− let (Just binding) = lookup letn env

1896+ let (Just binding) = lookupBinder letn env

18971897 let val = binderVal binding

18981898 if ind then induction (forget val)

18991899 else casetac (forget val)

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

24562456runTac autoSolve ist perhapsFC fn tac

24572457 = do env <- get_env

24582458 g <- goal

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

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

24602460 if autoSolve

24612461 then runT tac'

24622462 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)))

24642464 where

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

24662466 attack; intro (bname g)

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

24902490 tryAll tacs

24912491 when autoSolve solveAll

24922492 where envArgs n = do e <- get_env

2493− case lookup n e of

2493+ case lookupBinder n e of

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

24952495 (getArgTys (binderTy t))

24962496 _ -> return []

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

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

25092509 isImp _ = False

25102510 envArgs n = do e <- get_env

2511− case lookup n e of

2511+ case lookupBinder n e of

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

25132513 (getArgTys (binderTy t))

25142514 _ -> return []

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

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

292292 where

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

294294 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

296296 OK (_, UType UniqueType) -> True

297297 OK (_, UType NullType) -> True

298298 OK (_, UType AllTypes) -> True

299299 _ -> False in

300300 do getUniqB env us b

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

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

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

303303 getUniq env us (V i)

304304 | 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

4949 return ()) True

5050 where

5151 tryAll [] = fail "No trivial solution"

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

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

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

5454 hs <- get_holes

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

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

8585 return ()) True

8686 where

8787 tryAll [] = fail "No trivial solution"

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

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

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

9090 hs <- get_holes

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

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

123123cantSolveGoal = do g <- goal

124124 env <- get_env

125125 lift $ tfail $

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

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

127127

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

129129 -> 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

300300 tryLocals d locs tys env

301301

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

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

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

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

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

306306 (tryLocals d locs tys xs) True

src/Idris/Prover.hs+12−12

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

8282 = case envAtFocus (proof e) of

8383 OK env -> names env

8484 where names [] = []

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

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

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

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

8787

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

8989prove mode info opt ctxt lit n ty

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

174174 delab ist t

175175

176176 assumptionNames :: Env -> [Name]

177− assumptionNames = map fst

177+ assumptionNames = map fstEnv

178178

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

180180 prettyPs all g bnd [] = empty

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

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

182182 | 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)

184184 | 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) =

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

187187 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) =

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

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

191191

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

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

228228

229229 freeEnvNames :: Env -> [Name]

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

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

231231

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

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

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

468468 (ploop fn d prompt prf e h')

469469

470470

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

472472

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

474474checkNameType e prf n = do

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

478478 idrisCatch (do

479479 let OK env = envAtFocus (proof e)

480480 ctxt' = envCtxt env ctxt

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

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

482482 ist' = ist { tt_ctxt = ctxt' }

483483 putIState ist'

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

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

505505 action = case tm of

506506 TType _ ->

507507 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

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

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

511511 putIState ist

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

522522 let OK env = envAtFocus (proof e)

523523 ctxt' = envCtxt env ctxt

524524 ist' = ist { tt_ctxt = ctxt' }

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

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

526526 putIState ist'

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

528528 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)]

804804

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

806806reflectEnv :: Env -> Raw

807−reflectEnv = foldr consToEnvList emptyEnvList

807+reflectEnv = foldr consToEnvList emptyEnvList . envBinders

808808 where

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

810810 consToEnvList (n, b) l

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

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

824824 [envTupleType]

825825

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

826827reifyEnv :: 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

828830

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

830832rawBool :: Bool -> Raw

src/Idris/TypeSearch.hs+1−1

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

439439 unifyQueue state [] = return state

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

441441 --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]

443443 (ty1, Nothing)

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

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