4a9c0f4 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Fix argument names in generated types for where blocks

commit4a9c0f4dc41c67775d19f921ac03695a31b68485 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 28 Nov 2012, 21:50 (14 years ago) parent979520b

4 files changed+21−12

compare with master

unifiedsplit

CHANGELOG+1−1 lib/Prelude/List.idr+5−5 src/Core/ProofState.hs+1 src/Idris/ElabTerm.hs+14−6

CHANGELOG+1−1

@@ -7,7 +7,7 @@ User visible changes:

77 - supporting induction recursion and mutually recursive data

88* Type inference of definitions in 'where' clauses

99 - Provided that the type can be completely determined from the first

10− application of the function

10+ application of the function (in the top level definition)

1111* 'mutual' blocks added

1212 - effect is to elaborate all types of declarations in the block before

1313 elaborating their definitions

lib/Prelude/List.idr+5−5

@@ -266,7 +266,7 @@ intersperse : a -> List a -> List a

266266intersperse sep [] = []

267267intersperse sep (x::xs) = x :: intersperse' sep xs

268268 where

269− intersperse' : a -> List a -> List a

269+-- intersperse' : a -> List a -> List a

270270 intersperse' sep [] = []

271271 intersperse' sep (y::ys) = sep :: y :: intersperse' sep ys

272272

@@ -324,9 +324,9 @@ find p (x::xs) =

324324 find p xs

325325

326326findIndex : (a -> Bool) -> List a -> Maybe Nat

327−findIndex = findIndex' 0

327+findIndex = findIndex' O

328328 where

329− findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat

329+-- findIndex' : Nat -> (a -> Bool) -> List a -> Maybe Nat

330330 findIndex' cnt p [] = Nothing

331331 findIndex' cnt p (x::xs) =

332332 if p x then

@@ -335,9 +335,9 @@ findIndex = findIndex' 0

335335 findIndex' (S cnt) p xs

336336

337337findIndices : (a -> Bool) -> List a -> List Nat

338−findIndices = findIndices' 0

338+findIndices = findIndices' O

339339 where

340− findIndices' : Nat -> (a -> Bool) -> List a -> List Nat

340+-- findIndices' : Nat -> (a -> Bool) -> List a -> List Nat

341341 findIndices' cnt p [] = []

342342 findIndices' cnt p (x::xs) =

343343 if p x then

src/Core/ProofState.hs+1

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

312312 where

313313 getP n = case lookup n env of

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

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

315316

316317regret :: RunTactic

317318regret ctxt env (Bind x (Hole t) sc) | noOccurrence x sc =

src/Idris/ElabTerm.hs+14−6

@@ -239,7 +239,8 @@ elab ist info pattern tcgen fn tm

239239 ctxt <- get_context

240240 -- make a function type a -> b -> c -> ... -> rty for the

241241 -- new function name

242− argTys <- claimArgTys args

242+ env <- get_env

243+ argTys <- claimArgTys env args

243244 fn <- unique_hole (MN 0 "inf_fn")

244245 let fty = fnTy argTys rty

245246-- trace (show (ptm, map fst argTys)) $ focus fn

@@ -248,20 +249,27 @@ elab ist info pattern tcgen fn tm

248249 -- elaborate the arguments, to unify their types. They all have to

249250 -- be explicit.

250251 mapM_ elabIArg (zip argTys args)

251− where claimArgTys [] = return []

252− claimArgTys (arg : xs) | PRef _ n <- getTm arg

252+ where claimArgTys env [] = return []

253+ claimArgTys env (arg : xs) | Just n <- localVar env (getTm arg)

253254 = do nty <- get_type (Var n)

254− ans <- claimArgTys xs

255+ ans <- claimArgTys env xs

255256 return ((n, (False, forget nty)) : ans)

256− claimArgTys (_ : xs) = do an <- unique_hole (MN 0 "inf_argTy")

257+ claimArgTys env (_ : xs)

258+ = do an <- unique_hole (MN 0 "inf_argTy")

257259 aval <- unique_hole (MN 0 "inf_arg")

258260 claim an RSet

259261 claim aval (Var an)

260− ans <- claimArgTys xs

262+ ans <- claimArgTys env xs

261263 return ((aval, (True, (Var an))) : ans)

262264 fnTy [] ret = forget ret

263265 fnTy ((x, (_, xt)) : xs) ret = RBind x (Pi xt) (fnTy xs ret)

264266

267+ localVar env (PRef _ x)

268+ = case lookup x env of

269+ Just _ -> Just x

270+ _ -> Nothing

271+ localVar env _ = Nothing

272+

265273 elabIArg ((n, (True, ty)), def) = do focus n; elabE ina (getTm def)

266274 elabIArg _ = return () -- already done, just a name

267275