b7cf1ec · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Fix delab of scoped implicits

b7cf1ecEdwin Brady10 years ago

src/Idris/AbsSyntaxTree.hs+5

compare with master

unifiedsplit

@@ -1871,12 +1871,17 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

1871 depth d . bracket p startPrec $

1872 lbrace <> showRig rig n <+> colon <+> prettySe (decD d) startPrec bnd ty <> rbrace <+>

1873 st <> text "->" </> prettySe (decD d) startPrec ((n, True):bnd) sc

1874+ | isPi sc = depth d . bracket p startPrec $ prettySe (decD d) startPrec ((n, True):bnd) sc

1874 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc

1875 | otherwise = depth d $ prettySe (decD d) startPrec ((n, True):bnd) sc

1875 where

1876 where

1876 showRig Rig0 n = text "0" <+> prettyBindingOf n True

1877 showRig Rig0 n = text "0" <+> prettyBindingOf n True

1877 showRig Rig1 n = text "1" <+> prettyBindingOf n True

1878 showRig Rig1 n = text "1" <+> prettyBindingOf n True

1878 showRig _ n = prettyBindingOf n True

1879 showRig _ n = prettyBindingOf n True

1879

1880

1881+ isPi (PPi (Exp{}) _ _ _ _) = True

1882+ isPi (PPi _ _ _ _ sc) = isPi sc

1883+ isPi _ = False

1884+

1880 st =

1885 st =

1881 case s of

1886 case s of

1882 Static -> text "%static" <> space

1887 Static -> text "%static" <> space

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

@@ -611,9 +611,7 @@ prepare_apply fn imps =

611 mkClaims _ _ _ _

612 | Var n <- fn

613 = do ctxt <- get_context

614− case lookupTy n ctxt of

615− [] -> lift $ tfail $ NoSuchVariable n

616− _ -> lift $ tfail $ TooManyArguments n

614+ lift $ tfail $ TooManyArguments n

617 | otherwise = fail $ "Too many arguments for " ++ show fn

615 | otherwise = fail $ "Too many arguments for " ++ show fn

618

616

619 doClaim ((i, _), n, t) = do claim n t

617 doClaim ((i, _), n, t) = do claim n t

src/Idris/Delaborate.hs+101−76

@@ -8,7 +8,7 @@ Maintainer : The Idris Community.

8{-# LANGUAGE PatternGuards #-}

9{-# OPTIONS_GHC -fwarn-incomplete-patterns #-}

10module Idris.Delaborate (

11− annName, bugaddr, delab, delabDirect, delab', delabMV, delabSugared

11+ annName, bugaddr, delab, delabWithEnv, delabDirect, delab', delabMV, delabSugared

12 , delabTy, delabTy', fancifyAnnots, pprintDelab, pprintNoDelab

13 , pprintDelabTy, pprintErr, resugar

14 ) where

@@ -82,6 +82,9 @@ delabSugared ist tm = resugar ist $ delab ist tm

82delab :: IState -> Term -> PTerm

83delab i tm = delab' i tm False False

85+delabWithEnv :: IState -> [(Name, Type)] -> Term -> PTerm

86+delabWithEnv i tys tm = delabWithEnv' i tys tm False False

87+

85delabMV :: IState -> Term -> PTerm

88delabMV :: IState -> Term -> PTerm

86delabMV i tm = delab' i tm False True

89delabMV i tm = delab' i tm False True

@@ -89,26 +92,31 @@ delabMV i tm = delab' i tm False True

89-- We need this for interactive case splitting, where we need access to the

92-- We need this for interactive case splitting, where we need access to the

90-- underlying function in a delaborated form, to generate the right patterns

93-- underlying function in a delaborated form, to generate the right patterns

91delabDirect :: IState -> Term -> PTerm

94delabDirect :: IState -> Term -> PTerm

92−delabDirect i tm = delabTy' i [] tm False False False

95+delabDirect i tm = delabTy' i [] [] tm False False False

94delabTy :: IState -> Name -> PTerm

97delabTy :: IState -> Name -> PTerm

95delabTy i n

98delabTy i n

96 = case lookupTy n (tt_ctxt i) of

99 = case lookupTy n (tt_ctxt i) of

97 (ty:_) -> case lookupCtxt n (idris_implicits i) of

100 (ty:_) -> case lookupCtxt n (idris_implicits i) of

98− (imps:_) -> delabTy' i imps ty False False True

101+ (imps:_) -> delabTy' i imps [] ty False False True

99− _ -> delabTy' i [] ty False False True

102+ _ -> delabTy' i [] [] ty False False True

100 [] -> error "delabTy: got non-existing name"

103 [] -> error "delabTy: got non-existing name"

101

104

102delab' :: IState -> Term -> Bool -> Bool -> PTerm

105delab' :: IState -> Term -> Bool -> Bool -> PTerm

103−delab' i t f mvs = delabTy' i [] t f mvs True

106+delab' i t f mvs = delabTy' i [] [] t f mvs True

107+

108+delabWithEnv' :: IState -> [(Name, Type)] -> Term -> Bool -> Bool -> PTerm

109+delabWithEnv' i tys t f mvs = delabTy' i [] tys t f mvs True

104

110

105delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

111delabTy' :: IState -> [PArg] -- ^ implicit arguments to type, if any

112+ -> [(Name, Type)] -- ^ Names and types in environment

113+ -- (for properly hiding scoped implicits)

106 -> Term

114 -> Term

107 -> Bool -- ^ use full names

115 -> Bool -- ^ use full names

108 -> Bool -- ^ Don't treat metavariables specially

116 -> Bool -- ^ Don't treat metavariables specially

109 -> Bool -- ^ resugar cases

117 -> Bool -- ^ resugar cases

110 -> PTerm

118 -> PTerm

111−delabTy' ist imps tm fullname mvs docases = de [] imps tm

119+delabTy' ist imps genv tm fullname mvs docases = de genv [] imps tm

112 where

120 where

113 un = fileFC "(val)"

121 un = fileFC "(val)"

114

122

@@ -118,64 +126,71 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

118 -- the last argument,

126 -- the last argument,

119 -- although that's not always the thing that gets pattern matched

127 -- although that's not always the thing that gets pattern matched

120 -- in the elaborated block)

128 -- in the elaborated block)

121− de env imps sc

129+ de tys env imps sc

122 | docases

130 | docases

123 , isCaseApp sc

131 , isCaseApp sc

124 , (P _ cOp _, args@(_:_)) <- unApply sc

132 , (P _ cOp _, args@(_:_)) <- unApply sc

125− , Just caseblock <- delabCase env imps (last args) cOp args

133+ , Just caseblock <- delabCase tys env imps (last args) cOp args

126 = caseblock

134 = caseblock

127

135

128− de env _ (App _ f a) = deFn env f [a]

136+ de tys env _ (App _ f a) = deFn tys env f [a]

129− de env _ (V i) | i < length env = PRef un [] (snd (env!!i))

137+ de tys env _ (V i) | i < length env = PRef un [] (snd (env!!i))

130 | otherwise = PRef un [] (sUN ("v" ++ show i ++ ""))

138 | otherwise = PRef un [] (sUN ("v" ++ show i ++ ""))

131− de env _ (P _ n _) | n == unitTy = PTrue un IsType

139+ de tys env _ (P _ n _) | n == unitTy = PTrue un IsType

132− | n == unitCon = PTrue un IsTerm

140+ | n == unitCon = PTrue un IsTerm

133− | Just n' <- lookup n env = PRef un [] n'

141+ | Just n' <- lookup n env = PRef un [] n'

134− | otherwise

142+ | otherwise

135− = case lookup n (idris_metavars ist) of

143+ = case lookup n (idris_metavars ist) of

136− Just (Just _, mi, _, _, _) -> mkMVApp n []

144+ Just (Just _, mi, _, _, _) -> mkMVApp n []

137− _ -> PRef un [] n

145+ _ -> PRef un [] n

138− de env _ (Bind n (Lam _ ty) sc)

146+ de tys env _ (Bind n (Lam _ ty) sc)

139− = PLam un n NoFC (de env [] ty) (de ((n,n):env) [] sc)

147+ = PLam un n NoFC (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) [] sc)

140− de env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)

148+ de tys env (_ : is) (Bind n (Pi rig (Just impl) ty _) sc)

141 | toplevel_imp impl -- information in 'imps' repeated

149 | toplevel_imp impl -- information in 'imps' repeated

142− = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)

150+ = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC

151+ (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)

143− de env is (Bind n (Pi rig (Just impl) ty _) sc)

152+ de tys env is (Bind n (Pi rig (Just impl) ty _) sc)

144 | tcimplementation impl

153 | tcimplementation impl

145− = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

154+ = PPi constraint n NoFC (de tys env [] ty)

155+ (de ((n, ty) : tys) ((n,n):env) is sc)

146 | otherwise

156 | otherwise

147− = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)

157+ = PPi (Imp [] Dynamic False (Just impl) False rig) n NoFC (de tys env [] ty) (de tys ((n,n):env) is sc)

148− de env ((PImp { argopts = opts }):is) (Bind n (Pi rig _ ty _) sc)

158+ de tys env ((PImp { argopts = opts }):is) (Bind n (Pi rig _ ty _) sc)

149− = PPi (Imp opts Dynamic False Nothing False rig) n NoFC (de env [] ty) (de ((n,n):env) is sc)

159+ = PPi (Imp opts Dynamic False Nothing False rig) n NoFC

160+ (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)

150− de env (PConstraint _ _ _ _:is) (Bind n (Pi rig _ ty _) sc)

161+ de tys env (PConstraint _ _ _ _:is) (Bind n (Pi rig _ ty _) sc)

151− = PPi (constraint { pcount = rig}) n NoFC (de env [] ty) (de ((n,n):env) is sc)

162+ = PPi (constraint { pcount = rig}) n NoFC

163+ (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)

152− de env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi rig _ ty _) sc)

164+ de tys env (PTacImplicit _ _ _ tac _:is) (Bind n (Pi rig _ ty _) sc)

153− = PPi ((tacimpl tac) { pcount = rig }) n NoFC (de env [] ty) (de ((n,n):env) is sc)

165+ = PPi ((tacimpl tac) { pcount = rig }) n NoFC

166+ (de tys env [] ty) (de ((n, ty) : tys) ((n,n):env) is sc)

154− de env (plic:is) (Bind n (Pi rig _ ty _) sc)

167+ de tys env (plic:is) (Bind n (Pi rig _ ty _) sc)

155 = PPi (Exp (argopts plic) Dynamic False rig)

168 = PPi (Exp (argopts plic) Dynamic False rig)

156 n NoFC

169 n NoFC

157− (de env [] ty)

170+ (de tys env [] ty)

158− (de ((n,n):env) is sc)

171+ (de ((n, ty) : tys) ((n,n):env) is sc)

159− de env [] (Bind n (Pi rig _ ty _) sc)

172+ de tys env [] (Bind n (Pi rig _ ty _) sc)

160− = PPi (expl { pcount = rig }) n NoFC (de env [] ty) (de ((n,n):env) [] sc)

173+ = PPi (expl { pcount = rig }) n NoFC (de tys env [] ty)

174+ (de ((n, ty) : tys) ((n,n):env) [] sc)

161

175

162− de env imps (Bind n (Let ty val) sc)

176+ de tys env imps (Bind n (Let ty val) sc)

163 | docases

177 | docases

164 , isCaseApp sc

178 , isCaseApp sc

165 , (P _ cOp _, args) <- unApply sc

179 , (P _ cOp _, args) <- unApply sc

166− , Just caseblock <- delabCase env imps val cOp args = caseblock

180+ , Just caseblock <- delabCase tys env imps val cOp args = caseblock

167 | otherwise =

181 | otherwise =

168− PLet un n NoFC (de env [] ty) (de env [] val) (de ((n,n):env) [] sc)

182+ PLet un n NoFC (de tys env [] ty)

183+ (de tys env [] val) (de ((n, ty) : tys) ((n,n):env) [] sc)

169− de env _ (Bind n (Hole ty) sc) = de ((n, sUN "[__]"):env) [] sc

184+ de tys env _ (Bind n (Hole ty) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc

170− de env _ (Bind n (Guess ty val) sc) = de ((n, sUN "[__]"):env) [] sc

185+ de tys env _ (Bind n (Guess ty val) sc) = de ((n, ty) : tys) ((n, sUN "[__]"):env) [] sc

171− de env plic (Bind n bb sc) = de ((n,n):env) [] sc

186+ de tys env plic (Bind n bb sc) = de ((n, binderTy bb) : tys) ((n,n):env) [] sc

172− de env _ (Constant i) = PConstant NoFC i

187+ de tys env _ (Constant i) = PConstant NoFC i

173− de env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"

188+ de tys env _ (Proj _ _) = error "Delaboration got run-time-only Proj!"

174− de env _ Erased = Placeholder

189+ de tys env _ Erased = Placeholder

175− de env _ Impossible = Placeholder

190+ de tys env _ Impossible = Placeholder

176− de env _ (Inferred t) = Placeholder

191+ de tys env _ (Inferred t) = Placeholder

177− de env _ (TType i) = PType un

192+ de tys env _ (TType i) = PType un

178− de env _ (UType u) = PUniverse un u

193+ de tys env _ (UType u) = PUniverse un u

179

194

180 dens x | fullname = x

195 dens x | fullname = x

181 dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

196 dens ns@(NS n _) = case lookupCtxt n (idris_implicits ist) of

@@ -184,38 +199,48 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

184 _ -> ns

199 _ -> ns

185 dens n = n

200 dens n = n

186

201

187− deFn env (App _ f a) args = deFn env f (a:args)

202+ deFn tys env (App _ f a) args = deFn tys env f (a:args)

188− deFn env (P _ n _) [l,r]

203+ deFn tys env (P _ n _) [l,r]

189− | n == pairTy = PPair un [] IsType (de env [] l) (de env [] r)

204+ | n == pairTy = PPair un [] IsType (de tys env [] l) (de tys env [] r)

190− | n == sUN "lazy" = de env [] r -- TODO: Fix string based matching

191− deFn env (P _ n _) [ty, Bind x (Lam _ _) r]

205+ deFn tys env (P _ n _) [ty, Bind x (Lam _ _) r]

192 | n == sigmaTy

206 | n == sigmaTy

193− = PDPair un [] IsType (PRef un [] x) (de env [] ty)

207+ = PDPair un [] IsType (PRef un [] x) (de tys env [] ty)

194− (de ((x,x):env) [] (instantiate (P Bound x ty) r))

208+ (de tys ((x,x):env) [] (instantiate (P Bound x ty) r))

195− deFn env (P _ n _) [lt,rt,l,r]

209+ deFn tys env (P _ n _) [lt,rt,l,r]

196− | n == pairCon = PPair un [] IsTerm (de env [] l) (de env [] r)

210+ | n == pairCon = PPair un [] IsTerm (de tys env [] l) (de tys env [] r)

197− | n == sigmaCon = PDPair un [] IsTerm (de env [] l) Placeholder

211+ | n == sigmaCon = PDPair un [] IsTerm (de tys env [] l) Placeholder

198− (de env [] r)

212+ (de tys env [] r)

199− deFn env f@(P _ n _) args

213+-- deFn tys env f@(P _ n _) args

200− | n `elem` map snd env

214+-- | n `elem` map snd env

201− = PApp un (de env [] f) (map pexp (map (de env []) args))

215+-- = PApp un (de tys env [] f) (map pexp (map (de tys env []) args))

202− deFn env (P _ n _) args

216+ deFn tys env (P _ n _) args

203 | not mvs = case lookup n (idris_metavars ist) of

217 | not mvs = case lookup n (idris_metavars ist) of

204 Just (Just _, mi, _, _, _) ->

218 Just (Just _, mi, _, _, _) ->

205− mkMVApp n (drop mi (map (de env []) args))

219+ mkMVApp n (drop mi (map (de tys env []) args))

206− _ -> mkPApp n (map (de env []) args)

220+ _ -> mkPApp tys n (map (de tys env []) args)

207− | otherwise = mkPApp n (map (de env []) args)

221+ | otherwise = mkPApp tys n (map (de tys env []) args)

222+ deFn tys env (V i) args

223+ | i < length env = mkPApp tys (fst (env!!i)) (map (de tys env []) args)

208− deFn env f args = PApp un (de env [] f) (map pexp (map (de env []) args))

224+ deFn tys env f args = PApp un (de tys env [] f) (map pexp (map (de tys env []) args))

209

225

210 mkMVApp n []

226 mkMVApp n []

211 = PMetavar NoFC n

227 = PMetavar NoFC n

212 mkMVApp n args

228 mkMVApp n args

213 = PApp un (PMetavar NoFC n) (map pexp args)

229 = PApp un (PMetavar NoFC n) (map pexp args)

230+

214− mkPApp n args

231+ mkPApp tys n args

232+ | Just ty <- lookup n tys

233+ = let imps = findImp ty in

234+ PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

215 | Just imps <- lookupCtxtExact n (idris_implicits ist)

235 | Just imps <- lookupCtxtExact n (idris_implicits ist)

216 = PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

236 = PApp un (PRef un [] n) (zipWith imp (imps ++ repeat (pexp undefined)) args)

217 | otherwise = PApp un (PRef un [] n) (map pexp args)

237 | otherwise = PApp un (PRef un [] n) (map pexp args)

218−

238+ where

239+ findImp (Bind n (Pi _ im@(Just i) _ _) sc)

240+ = pimp n Placeholder True : findImp sc

241+ findImp (Bind n (Pi _ _ _ _) sc)

242+ = pexp Placeholder : findImp sc

243+ findImp _ = []

219 imp (PImp p m l n _) arg = PImp p m l n arg

244 imp (PImp p m l n _) arg = PImp p m l n arg

220 imp (PExp p l n _) arg = PExp p l n arg

245 imp (PExp p l n _) arg = PExp p l n arg

221 imp (PConstraint p l n _) arg = PConstraint p l n arg

246 imp (PConstraint p l n _) arg = PConstraint p l n arg

@@ -227,14 +252,14 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

227 isCN (SN (CaseN _ _)) = True

252 isCN (SN (CaseN _ _)) = True

228 isCN _ = False

253 isCN _ = False

229

254

230− delabCase :: [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm

255+ delabCase :: [(Name, Type)] -> [(Name, Name)] -> [PArg] -> Term -> Name -> [Term] -> Maybe PTerm

231− delabCase env imps scrutinee caseName caseArgs =

256+ delabCase tys env imps scrutinee caseName caseArgs =

232 do cases <- case lookupCtxt caseName (idris_patdefs ist) of

257 do cases <- case lookupCtxt caseName (idris_patdefs ist) of

233 [(cases, _)] -> return cases

258 [(cases, _)] -> return cases

234 _ -> Nothing

259 _ -> Nothing

235− return $ PCase un (de env imps scrutinee)

260+ return $ PCase un (de tys env imps scrutinee)

236− [ (de (env ++ map (\(n, _) -> (n, n)) vars) imps (splitArg lhs),

261+ [ (de tys (env ++ map (\(n, _) -> (n, n)) vars) imps (splitArg lhs),

237− de (env ++ map (\(n, _) -> (n, n)) vars) imps rhs)

262+ de tys (env ++ map (\(n, _) -> (n, n)) vars) imps rhs)

238 | (vars, lhs, rhs) <- cases

263 | (vars, lhs, rhs) <- cases

239 ]

264 ]

240 where splitArg tm | (_, args) <- unApply tm = nonVar (reverse args)

265 where splitArg tm | (_, args) <- unApply tm = nonVar (reverse args)

@@ -268,8 +293,8 @@ pprintDelabTy i n

268 = case lookupTy n (tt_ctxt i) of

293 = case lookupTy n (tt_ctxt i) of

269 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $

294 (ty:_) -> annotate (AnnTerm [] ty) . prettyIst i $

270 case lookupCtxt n (idris_implicits i) of

295 case lookupCtxt n (idris_implicits i) of

271− (imps:_) -> resugar i $ delabTy' i imps ty False False True

296+ (imps:_) -> resugar i $ delabTy' i imps [] ty False False True

272− _ -> resugar i $ delabTy' i [] ty False False True

297+ _ -> resugar i $ delabTy' i [] [] ty False False True

273 [] -> error "pprintDelabTy got a name that doesn't exist"

298 [] -> error "pprintDelabTy got a name that doesn't exist"

274

299

275pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

300pprintTerm :: IState -> PTerm -> Doc OutputAnnotation

src/Idris/Elab/Clause.hs−3

@@ -753,9 +753,6 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

753

754 -- These are the names we're not allowed to use on the RHS, because

755 -- they're UniqueTypes and borrowed from another function.

756− -- FIXME: There is surely a nicer way than this...

757− -- Issue #1615 on the Issue Tracker.

758− -- https://github.com/idris-lang/Idris-dev/issues/1615

759 when (not (null borrowed)) $

756 when (not (null borrowed)) $

760 logElab 5 ("Borrowed names on LHS: " ++ show borrowed)

757 logElab 5 ("Borrowed names on LHS: " ++ show borrowed)

761

758

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

@@ -212,7 +212,7 @@ elabInterface info_in syn_in doc what fc constraints tn tnfc ps pDocs fds ds mcn

212 Just i -> i

213 Nothing -> []

214 case lookupTyExact n (tt_ctxt ist) of

215− Just ty -> return (delabTy' ist impls ty False False False)

215+ Just ty -> return (delabTy' ist impls [] ty False False False)

216 Nothing -> tclift $ tfail (At fc (InternalMsg "Can't happen, elabMethTy"))

217

218 -- Find the argument position of the current interface in a method type

src/Idris/Elab/Term.hs+3−1

@@ -2659,8 +2659,10 @@ runTac autoSolve ist perhapsFC fn tac

2659 letbind scriptvar scriptTy (Var script)

2660 focus script

2661 ptm <- get_term

2662+ env <- get_env

2663+ let denv = map (\(n, _, b) -> (n, binderTy b)) env

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

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

2663− (PApp emptyFC tm [pexp (delabTy' ist [] tgoal True True True)])

2665+ (PApp emptyFC tm [pexp (delabTy' ist [] denv tgoal True True True)])

2664 (script', _) <- get_type_val (Var scriptvar)

2666 (script', _) <- get_type_val (Var scriptvar)

2665 -- now that we have the script apply

2667 -- now that we have the script apply

2666 -- it to the reflected goal

2668 -- it to the reflected goal

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

@@ -209,8 +209,11 @@ getPBtys _ = []

209psolve (Bind n (PVar _ t) sc) = do solve; psolve sc

210psolve tm = return ()

211

212+pvars ist tm = pv' [] tm

213+ where

212−pvars ist (Bind n (PVar _ t) sc) = (n, delab ist t) : pvars ist sc

214+ pv' env (Bind n (PVar _ t) sc)

213−pvars ist _ = []

215+ = (n, delabWithEnv ist env t) : pv' ((n, t) : env) sc

216+ pv' env _ = []

214

217

215getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi _ _ t _) sc)

218getFixedInType i env (PExp _ _ _ _ : is) (Bind n (Pi _ _ t _) sc)

216 = nub $ getFixedInType i env [] t ++

219 = nub $ getFixedInType i env [] t ++

src/Idris/REPL.hs+10−7

@@ -93,6 +93,8 @@ import Util.Pretty hiding ((</>))

93import Util.System

94import Version_idris (gitHash)

96+import Debug.Trace

97+

96-- | Run the REPL

98-- | Run the REPL

97repl :: IState -- ^ The initial state

99repl :: IState -- ^ The initial state

98 -> [FilePath] -- ^ The loaded modules

100 -> [FilePath] -- ^ The loaded modules

@@ -422,9 +424,9 @@ runIdeModeCommand h id orig fn mods (IdeMode.Metavariables cols) =

422 splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

424 splitPi :: IState -> Int -> Type -> ([(Name, Type, PTerm)], Type, PTerm)

423 splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =

425 splitPi ist i (Bind n (Pi _ _ t _) rest) | i > 0 =

424 let (hs, c, pc) = splitPi ist (i - 1) rest in

426 let (hs, c, pc) = splitPi ist (i - 1) rest in

425− ((n, t, delabTy' ist [] t False False True):hs,

427+ ((n, t, delabTy' ist [] [] t False False True):hs,

426− c, delabTy' ist [] c False False True)

428+ c, delabTy' ist [] [] c False False True)

427− splitPi ist i tm = ([], tm, delabTy' ist [] tm False False True)

429+ splitPi ist i tm = ([], tm, delabTy' ist [] [] tm False False True)

428

430

429 -- | Get the types of a list of metavariable names

431 -- | Get the types of a list of metavariable names

430 mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]

432 mvTys :: IState -> [(Name, Int)] -> [(Name, Int, Type)]

@@ -1511,15 +1513,16 @@ pprintDef asCore n =

1511 ppDef amb ist (n, (clauses, missing)) =

1513 ppDef amb ist (n, (clauses, missing)) =

1512 prettyName True amb [] n <+> colon <+>

1514 prettyName True amb [] n <+> colon <+>

1513 align (pprintDelabTy ist n) <$>

1515 align (pprintDelabTy ist n) <$>

1514− ppClauses ist (map (\(ns, lhs, rhs) -> (map fst ns, lhs, rhs)) clauses) <> ppMissing missing

1516+ ppClauses ist clauses <> ppMissing missing

1515 ppClauses ist [] = text "No clauses."

1517 ppClauses ist [] = text "No clauses."

1516 ppClauses ist cs = vsep (map pp cs)

1518 ppClauses ist cs = vsep (map pp cs)

1517− where pp (vars, lhs, rhs) =

1519+ where pp (varTys, lhs, rhs) =

1520+ let vars = map fst varTys

1518− let ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .

1521+ ppTm t = annotate (AnnTerm (zip vars (repeat False)) t) .

1519 pprintPTerm (ppOptionIst ist)

1522 pprintPTerm (ppOptionIst ist)

1520 (zip vars (repeat False))

1523 (zip vars (repeat False))

1521 [] (idris_infixes ist) .

1524 [] (idris_infixes ist) .

1522− delab ist $

1525+ delabWithEnv ist varTys $

1523 t

1526 t

1524 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)

1527 in group $ ppTm lhs <+> text "=" <$> (group . align . hang 2 $ ppTm rhs)

1525 ppMissing _ = empty

1528 ppMissing _ = empty