42a1719 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge pull request #2303 from david-christiansen/issue/2302

42a1719Niklas Larsson11 years ago

idris.cabal+3

compare with master

unifiedsplit

@@ -314,6 +314,9 @@ Extra-source-files:

314 test/reg064/run

315 test/reg064/*.idr

316 test/reg064/expected

317+ test/reg065/run

318+ test/reg065/*.idr

319+ test/reg065/expected

317

320

318 test/basic001/run

321 test/basic001/run

319 test/basic001/*.idr

322 test/basic001/*.idr

src/Idris/AbsSyntax.hs+6−6

@@ -1623,12 +1623,12 @@ addImpl' inpat env infns imp_meths ist ptm

1623-- names with zero explicit arguments, don't add implicits.

1624

1625aiFn :: Bool -> Bool -> Bool

1626− -> [Name]

1626+ -> [Name]

1627− -> IState -> FC

1627+ -> IState -> FC

1628− -> Name -- ^ function being applied

1628+ -> Name -- ^ function being applied

1629− -> FC -> [[T.Text]]

1629+ -> FC -> [[T.Text]]

1630− -> [PArg] -> -- ^ initial arguments

1630+ -> [PArg] -- ^ initial arguments

1631− Either Err PTerm

1631+ -> Either Err PTerm

1632aiFn inpat True qq imp_meths ist fc f ffc ds []

1633 = case lookupDef f (tt_ctxt ist) of

1634 [] -> Right $ PPatvar ffc f

src/Idris/Elab/Class.hs+44−16

@@ -1,4 +1,5 @@

1{-# LANGUAGE PatternGuards #-}

2+{-# OPTIONS_GHC -fwarn-missing-signatures #-}

2module Idris.Elab.Class(elabClass) where

3module Idris.Elab.Class(elabClass) where

4import Idris.AbsSyntax

5import Idris.AbsSyntax

@@ -47,6 +48,7 @@ import qualified Data.Set as S

47import qualified Data.Text as T

48import qualified Data.Text as T

48import Data.Char(isLetter, toLower)

49import Data.Char(isLetter, toLower)

49import Data.List.Split (splitOn)

50import Data.List.Split (splitOn)

51+import Data.Generics.Uniplate.Data (transform)

51import Util.Pretty(pretty, text)

53import Util.Pretty(pretty, text)

@@ -83,6 +85,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

83 let (methods, imethods)

85 let (methods, imethods)

84 = unzip (map (\ (x, y, z) -> (x, y)) ims)

86 = unzip (map (\ (x, y, z) -> (x, y)) ims)

85 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

87 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

88+

86 -- build instance constructor type

89 -- build instance constructor type

87 let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints

90 let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints

88 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

91 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

@@ -92,6 +95,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

92 let ddecl = PDatadecl tn NoFC tty cons

95 let ddecl = PDatadecl tn NoFC tty cons

94 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

97 logLvl 5 $ "Class data " ++ show (showDImp verbosePPOption ddecl)

98+

95 -- Elaborate the data declaration

99 -- Elaborate the data declaration

96 elabData info (syn { no_imp = no_imp syn ++ mnames,

100 elabData info (syn { no_imp = no_imp syn ++ mnames,

97 imp_methods = mnames }) doc pDocs fc [] ddecl

101 imp_methods = mnames }) doc pDocs fc [] ddecl

@@ -118,7 +122,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

118 [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++

122 [(pnfc, AnnBoundName pn False) | (pn, pnfc, _) <- ps] ++

119 [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++

123 [(fdfc, AnnBoundName fc False) | (fc, fdfc) <- fds] ++

120 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

124 maybe [] (\(conN, conNFC) -> [(conNFC, AnnName conN Nothing Nothing Nothing)]) mcn

121−

125+

122 where

126 where

123 nodoc (n, (_, _, o, t)) = (n, (o, t))

127 nodoc (n, (_, _, o, t)) = (n, (o, t))

124

128

@@ -132,11 +136,6 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

132 chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t

136 chkUniq (PPi _ _ _ _ sc) t = chkUniq sc t

133 chkUniq _ t = t

137 chkUniq _ t = t

134

138

135− mdec :: Name -> Name

136− mdec (UN n) = SN (MethodN (UN n))

137− mdec (NS x n) = NS (mdec x) n

138− mdec x = x

139−

140 -- TODO: probably should normalise

139 -- TODO: probably should normalise

141 checkDefaultSuperclassInstance :: PDecl -> Idris ()

140 checkDefaultSuperclassInstance :: PDecl -> Idris ()

142 checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n _ ps _ _ _)

141 checkDefaultSuperclassInstance (PInstance _ _ _ fc cs n _ ps _ _ _)

@@ -171,7 +170,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

171 defdecl mtys c d@(PClauses fc opts n cs) =

170 defdecl mtys c d@(PClauses fc opts n cs) =

172 case lookup n mtys of

171 case lookup n mtys of

173 Just (nfc, syn, o, ty) ->

172 Just (nfc, syn, o, ty) ->

174− do let ty' = insertConstraint c ty

173+ do let ty' = insertConstraint c (map fst mtys) ty

175 let ds = map (decorateid defaultdec)

174 let ds = map (decorateid defaultdec)

176 [PTy emptyDocstring [] syn fc [] n nfc ty',

175 [PTy emptyDocstring [] syn fc [] n nfc ty',

177 PClauses fc (o ++ opts) n cs]

176 PClauses fc (o ++ opts) n cs]

@@ -215,10 +214,16 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

215 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,

214 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,

216 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

215 PClauses fc [Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

217

216

218− -- Generate a top level function which looks up a method in a given

217+ -- | Generate a top level function which looks up a method in a given

219 -- dictionary (this is inlinable, always)

218 -- dictionary (this is inlinable, always)

219+ tfun :: Name -- ^ The name of the class

220+ -> PTerm -- ^ A constraint for the class, to be inserted under the implicit bindings

221+ -> SyntaxInfo -> [Name] -- ^ All the method names

222+ -> (Name, (FC, Docstring (Either Err PTerm), FnOpts, PTerm))

223+ -- ^ The present declaration

224+ -> Idris [PDecl]

220 tfun cn c syn all (m, (mfc, doc, o, ty))

225 tfun cn c syn all (m, (mfc, doc, o, ty))

221− = do let ty' = expandMethNS syn (insertConstraint c ty)

226+ = do let ty' = expandMethNS syn (insertConstraint c all ty)

222 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

227 let mnames = take (length all) $ map (\x -> sMN x "meth") [0..]

223 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

228 let capp = PApp fc (PRef fc cn) (map (pexp . PRef fc) mnames)

224 let margs = getMArgs ty

229 let margs = getMArgs ty

@@ -236,6 +241,7 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

236 getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc

241 getMArgs (PPi (Constraint _ _) n _ ty sc) = CA : getMArgs sc

237 getMArgs _ = []

242 getMArgs _ = []

238

243

244+ getMeth :: [Name] -> [Name] -> Name -> PTerm

239 getMeth (m:ms) (a:as) x | x == a = PRef fc m

245 getMeth (m:ms) (a:as) x | x == a = PRef fc m

240 | otherwise = getMeth ms as x

246 | otherwise = getMeth ms as x

241

247

@@ -249,10 +255,24 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

249 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

255 rhsArgs (CA : xs) ns = pconst (PResolveTC fc) : rhsArgs xs ns

250 rhsArgs [] _ = []

256 rhsArgs [] _ = []

251

257

258+ insertConstraint :: PTerm -> [Name] -> PTerm -> PTerm

252− insertConstraint c (PPi p@(Imp _ _ _ _) n fc ty sc)

259+ insertConstraint c all (PPi p@(Imp _ _ _ _) n fc ty sc)

253− = PPi p n fc ty (insertConstraint c sc)

260+ = PPi p n fc ty (insertConstraint c all sc)

261+ insertConstraint c all sc = let dictN = sMN 0 "class"

254− insertConstraint c sc = PPi (constraint { pstatic = Static })

262+ in PPi (constraint { pstatic = Static })

255− (sMN 0 "class") NoFC c sc

263+ dictN NoFC c

264+ (constrainMeths (map basename all)

265+ dictN sc)

266+ where

267+ -- After we insert the constraint into the lookup, we need to

268+ -- ensure that the same dictionary is used to resolve lookups

269+ -- to the other methods in the class

270+ constrainMeths :: [Name] -> Name -> PTerm -> PTerm

271+ constrainMeths allM dictN tm = transform (addC allM dictN) tm

272+ addC allM dictN m@(PRef fc n)

273+ | n `elem` allM = PApp NoFC m [pconst (PRef NoFC dictN)]

274+ | otherwise = m

275+ addC _ _ tm = tm

256

276

257 -- make arguments explicit and don't bind class parameters

277 -- make arguments explicit and don't bind class parameters

258 toExp ns e (PPi (Imp l s p _) n fc ty sc)

278 toExp ns e (PPi (Imp l s p _) n fc ty sc)

@@ -261,6 +281,13 @@ elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

261 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

281 toExp ns e (PPi p n fc ty sc) = PPi p n fc ty (toExp ns e sc)

262 toExp ns e sc = sc

282 toExp ns e sc = sc

263

283

284+-- | Get the method declaration name corresponding to a user-provided name

285+mdec :: Name -> Name

286+mdec (UN n) = SN (MethodN (UN n))

287+mdec (NS x n) = NS (mdec x) n

288+mdec x = x

289+

290+-- | Get the docstring corresponding to a member, if one exists

264memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

291memberDocs :: PDecl -> Maybe (Name, Docstring (Either Err PTerm))

265memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

292memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

266memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)

293memberDocs (PPostulate _ d _ _ _ n _) = Just (basename n, d)

@@ -270,17 +297,18 @@ memberDocs (PClass d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)

270memberDocs _ = Nothing

297memberDocs _ = Nothing

271

298

272

299

273−-- In a top level type for a method, expand all the method names namespaces

300+-- | In a top level type for a method, expand all the method names' namespaces

274-- so that we don't have to disambiguate later

301-- so that we don't have to disambiguate later

275−expandMethNS :: SyntaxInfo

302+expandMethNS :: SyntaxInfo

276 -> PTerm -> PTerm

303 -> PTerm -> PTerm

277expandMethNS syn = mapPT expand

304expandMethNS syn = mapPT expand

278 where

305 where

279 expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n

306 expand (PRef fc n) | n `elem` imp_methods syn = PRef fc $ expandNS syn n

280 expand t = t

307 expand t = t

281

308

309+-- | Find the determining parameter locations

282findDets :: Name -> [Name] -> Idris [Int]

310findDets :: Name -> [Name] -> Idris [Int]

283−findDets n ns =

311+findDets n ns =

284 do i <- getIState

312 do i <- getIState

285 return $ case lookupTyExact n (tt_ctxt i) of

313 return $ case lookupTyExact n (tt_ctxt i) of

286 Just ty -> getDetPos 0 ns ty

314 Just ty -> getDetPos 0 ns ty

test/reg065/expectednew file

No changes to the content.

test/reg065/reg065.idrnew file+26

@@ -0,0 +1,26 @@

1+||| Test that dependent type class definitions work.

2+|||

3+||| Fixes a regression where previous methods used in a later method's

4+||| type would lead to "can't resolve type class" errors

5+module TypeClassDep

7+import Data.Vect

10+class Foo a where

11+ getLen : Nat

12+ item : a -> Vect getLen a

13+

14+instance Foo () where

15+ getLen = 3

16+ item () = [(), (), ()]

17+

18+instance Foo String where

19+ getLen = 1

20+ item str = [str]

21+

22+check1 : item () = with Vect [(),(),()]

23+check1 = Refl

24+

25+check2 : item "halløjsa" = with Vect ["halløjsa"]

26+check2 = Refl

test/reg065/runnew file+3

@@ -0,0 +1,3 @@

1+#!/usr/bin/env bash

2+idris $@ reg065.idr --check

3+rm -f *.ibc