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

idris.cabal+3

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

611611 test/interfaces002/*.idr

612612 test/interfaces002/run

613613 test/interfaces002/expected

614+ test/interfaces003/*.idr

615+ test/interfaces003/run

616+ test/interfaces003/expected

614617

615618 test/io001/run

616619 test/io001/*.idr

src/Idris/AbsSyntax.hs+14−5

@@ -1249,7 +1249,7 @@ expandParamsD rhsonly ist dec ps ns (PClauses fc opts n cs)

12491249 updateps yn nm [] = []

12501250 updateps yn nm (((a, t), i):as)

12511251 | (a `elem` nm) == yn = (a, t) : updateps yn nm as

1252− | otherwise = (sMN i ('_' : show n ++ "_u"), t) : updateps yn nm as

1252+ | otherwise = (sMN i (show a ++ "_u"), t) : updateps yn nm as

12531253

12541254 removeBound lhs ns = ns \\ nub (bnames lhs)

12551255

@@ -1290,19 +1290,28 @@ expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds dec

12901290 (map (expandParamsD rhs ist dec ps ns) decls)

12911291 cn

12921292 cd

1293−expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs acc opts n nfc params ty cn decls)

1294− = PInstance doc argDocs info f

1293+expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs acc opts n nfc params pextra ty cn decls)

1294+ = let cn' = case cn of

1295+ Just n -> if n `elem` ns then Just (dec n) else Just n

1296+ Nothing -> Nothing in

1297+ PInstance doc argDocs info f

12951298 (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) cs)

12961299 acc opts n

12971300 nfc

12981301 (map (expandParams dec ps ns []) params)

1302+ (map (\ (n, t) -> (n, expandParams dec ps ns [] t)) pextra)

12991303 (expandParams dec ps ns [] ty)

1300− cn

1301− (map (expandParamsD rhs ist dec ps ns) decls)

1304+ cn'

1305+ (map (expandParamsD True ist dec ps ns) decls)

13021306expandParamsD rhs ist dec ps ns d = d

13031307

13041308mapsnd f (x, t) = (x, f t)

13051309

1310+expandInstanceScope ist dec ps ns (PInstance doc argDocs info f cs acc opts n nfc params pextra ty cn decls)

1311+ = PInstance doc argDocs info f cs acc opts n nfc params (ps ++ pextra)

1312+ ty cn decls

1313+expandInstanceScope ist dec ps ns d = d

1314+

13061315-- Calculate a priority for a type, for deciding elaboration order

13071316-- * if it's just a type variable or concrete type, do it early (0)

13081317-- * if there's only type variables and injective constructors, do it next (1)

src/Idris/AbsSyntaxTree.hs+16−5

@@ -738,6 +738,7 @@ data PDecl' t

738738 Name -- class

739739 FC -- precise location of class

740740 [t] -- parameters

741+ [(Name, t)] -- Extra names in scope in the body

741742 t -- full instance type

742743 (Maybe Name) -- explicit name

743744 [PDecl' t]

@@ -900,10 +901,11 @@ mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor c

900901 (map (mapPDeclFC f g) body)

901902 (fmap (\(n, nfc) -> (n, g nfc)) ctor)

902903 ctorDoc

903−mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn acc opts cnfc params instTy instN body) =

904+mapPDeclFC f g (PInstance doc paramDocs syn fc constrs cn acc opts cnfc params pextra instTy instN body) =

904905 PInstance doc paramDocs syn (f fc)

905906 (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)

906907 cn acc opts (g cnfc) (map (mapPTermFC f g) params)

908+ (map (\(en, et) -> (en, mapPTermFC f g et)) pextra)

907909 (mapPTermFC f g instTy)

908910 instN

909911 (map (mapPDeclFC f g) body)

@@ -943,7 +945,10 @@ declared (PParams _ _ ds) = concatMap declared ds

943945declared (PNamespace _ _ ds) = concatMap declared ds

944946declared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

945947declared (PClass _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)

946−declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []

948+declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ mn _)

949+ = case mn of

950+ Nothing -> []

951+ Just n -> [n]

947952declared (PDSL n _) = [n]

948953declared (PSyntax _ _) = []

949954declared (PMutual _ ds) = concatMap declared ds

@@ -963,7 +968,10 @@ tldeclared (PParams _ _ ds) = []

963968tldeclared (PMutual _ ds) = concatMap tldeclared ds

964969tldeclared (PNamespace _ _ ds) = concatMap tldeclared ds

965970tldeclared (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)

966−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []

971+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ mn _)

972+ = case mn of

973+ Nothing -> []

974+ Just n -> [n]

967975tldeclared _ = []

968976

969977defined :: PDecl -> [Name]

@@ -979,7 +987,10 @@ defined (PParams _ _ ds) = concatMap defined ds

979987defined (PNamespace _ _ ds) = concatMap defined ds

980988defined (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

981989defined (PClass _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)

982−defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = []

990+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ mn _)

991+ = case mn of

992+ Nothing -> []

993+ Just n -> [n]

983994defined (PDSL n _) = [n]

984995defined (PSyntax _ _) = []

985996defined (PMutual _ ds) = concatMap defined ds

@@ -2167,7 +2178,7 @@ showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (lin

21672178showDeclImp _ (PSyntax _ syn) = text "syntax" <+> text (show syn)

21682179showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)

21692180 = text "interface" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

2170−showDeclImp o (PInstance _ _ _ _ cs acc _ n _ _ t _ ds)

2181+showDeclImp o (PInstance _ _ _ _ cs acc _ n _ _ _ t _ ds)

21712182 = text "implementation" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

21722183showDeclImp _ _ = text "..."

21732184-- showDeclImp (PImport o) = "import " ++ o

src/Idris/DeepSeq.hs+2−2

@@ -468,7 +468,7 @@ instance (NFData t) => NFData (PDecl' t) where

468468 rnf x9 `seq`

469469 rnf x10 `seq`

470470 rnf x11 `seq` rnf x12 `seq` ()

471− rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

471+ rnf (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

472472 = rnf x1 `seq`

473473 rnf x2 `seq`

474474 rnf x3 `seq`

@@ -477,7 +477,7 @@ instance (NFData t) => NFData (PDecl' t) where

477477 rnf x6 `seq`

478478 rnf x7 `seq`

479479 rnf x8 `seq`

480− rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` ()

480+ rnf x9 `seq` rnf x10 `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` ()

481481 rnf (PDSL x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

482482 rnf (PSyntax x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

483483 rnf (PMutual x1 x2) = rnf x1 `seq` rnf x2 `seq` ()

src/Idris/Docs.hs+2−2

@@ -319,8 +319,8 @@ docClass n ci

319319 namedInst n@(UN _) = Just n

320320 namedInst _ = Nothing

321321

322− getDInst (PInstance _ _ _ _ _ _ _ _ _ _ t _ _) = Just t

323− getDInst _ = Nothing

322+ getDInst (PInstance _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t

323+ getDInst _ = Nothing

324324

325325 isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))

326326 = nm == n && map getTm args == map getTm args'

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

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

144144

145145 -- TODO: probably should normalise

146146 checkDefaultSuperclassInstance :: PDecl -> Idris ()

147− checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ _ n _ ps _ _ _)

147+ checkDefaultSuperclassInstance (PInstance _ _ _ fc cs _ _ n _ ps _ _ _ _)

148148 = do when (not $ null cs) . tclift

149149 $ tfail (At fc (Msg $ "Default superclass instances can't have constraints."))

150150 i <- getIState

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

198198

199199 tydecl (PTy _ _ _ _ _ _ _ _) = True

200200 tydecl _ = False

201− instdecl (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _) = True

201+ instdecl (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ _) = True

202202 instdecl _ = False

203203 clause (PClauses _ _ _ _) = True

204204 clause _ = False

src/Idris/Elab/Clause.hs+2−1

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

629629

630630 let winfo = (pinfo info newargs defs windex) { elabFC = Just fc }

631631 let wb = map (mkStatic static_names) $

632+ map (expandInstanceScope ist decorate newargs defs) $

632633 map (expandParamsD False ist decorate newargs defs) whereblock

633634

634635 -- Split the where block into declarations with a type, and those

@@ -636,7 +637,7 @@ elabClause info opts (cnum, PClause fc fname lhs_in_as withs rhs_in_as wherebloc

636637 -- Elaborate those with a type *before* RHS, those without *after*

637638 let (wbefore, wafter) = sepBlocks wb

638639

639− logElab 2 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

640+ logElab 5 $ "Where block:\n " ++ show wbefore ++ "\n" ++ show wafter

640641 mapM_ (rec_elabDecl info EAll winfo) wbefore

641642 -- Now build the RHS, using the type of the LHS as the goal.

642643 i <- getIState -- new implicits from where block

src/Idris/Elab/Instance.hs+31−14

@@ -60,10 +60,11 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

6060 Name -> -- the class

6161 FC -> -- precise location of class name

6262 [PTerm] -> -- class parameters (i.e. instance)

63+ [(Name, PTerm)] -> -- Extra arguments in scope (e.g. instance in where block)

6364 PTerm -> -- full instance type

6465 Maybe Name -> -- explicit name

6566 [PDecl] -> Idris ()

66−elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

67+elabInstance info syn doc argDocs what fc cs acc opts n nfc ps pextra t expn ds = do

6768 ist <- getIState

6869 (n, ci) <- case lookupCtxtName n (idris_classes ist) of

6970 [c] -> return c

@@ -79,7 +80,8 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

7980

8081 let emptyclass = null (class_methods ci)

8182 when (what /= EDefns) $ do

82− nty <- elabType' True info syn doc argDocs fc totopts iname NoFC t

83+ nty <- elabType' True info syn doc argDocs fc totopts iname NoFC

84+ (piBindp expl_param pextra t)

8385 -- if the instance type matches any of the instances we have already,

8486 -- and it's not a named instance, then it's overlapping, so report an error

8587 case expn of

@@ -125,7 +127,7 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

125127 all_meths

126128 t' = substMatchesShadow mnamemap pnames t_in in

127129 (decorate ns iname n,

128− op, coninsert cs t', t'))

130+ op, coninsert cs pextra t', t'))

129131 (class_methods ci)

130132 logElab 3 (show (mtys, ips))

131133 logElab 5 ("Before defaults: " ++ show ds ++ "\n" ++ show (map fst (class_methods ci)))

@@ -136,8 +138,11 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

136138 mapM_ (warnMissing ds' ns iname) (map fst (class_methods ci))

137139 mapM_ (checkInClass (map fst (class_methods ci))) (concatMap defined ds')

138140 let wbTys = map mkTyDecl mtys

139− let wbVals = map (decorateid (decorate ns iname)) ds'

141+ let wbVals_orig = map (decorateid (decorate ns iname)) ds'

142+ ist <- getIState

143+ let wbVals = map (expandParamsD False ist id pextra (map methName mtys)) wbVals_orig

140144 let wb = wbTys ++ wbVals

145+

141146 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

142147 logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++

143148 show (concat (nub wparams))

@@ -145,7 +150,7 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

145150

146151 let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars

147152

148− let lhs = PApp fc (PRef fc [] iname) lhsImps

153+ let lhs = PApp fc (PRef fc [] iname) (lhsImps ++ map (toExp .fst) pextra)

149154 let rhs = PApp fc (PRef fc [] (instanceCtorName ci))

150155 (map (pexp . (mkMethApp lhsImps)) mtys)

151156

@@ -154,6 +159,7 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

154159

155160 push_estack iname True

156161 logElab 3 ("Method types: " ++ show wbTys)

162+ logElab 3 ("Method bodies (before params): " ++ show wbVals_orig)

157163 logElab 3 ("Method bodies: " ++ show wbVals)

158164

159165 let idecls = [PClauses fc totopts iname

@@ -196,10 +202,13 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

196202 Just m -> sNS (SN (sInstanceN n' (map show ps'))) m

197203 Just nm -> nm

198204

199− substInstance ips pnames (PInstance doc argDocs syn _ cs acc opts n nfc ps t expn ds)

200− = PInstance doc argDocs syn fc cs acc opts n nfc (map (substMatchesShadow ips pnames) ps) (substMatchesShadow ips pnames t) expn ds

205+ substInstance ips pnames (PInstance doc argDocs syn _ cs acc opts n nfc ps pextra t expn ds)

206+ = PInstance doc argDocs syn fc cs acc opts n nfc

207+ (map (substMatchesShadow ips pnames) ps)

208+ pextra

209+ (substMatchesShadow ips pnames t) expn ds

201210

202− isOverlapping i (PInstance doc argDocs syn _ _ _ _ n nfc ps t expn _)

211+ isOverlapping i (PInstance doc argDocs syn _ _ _ _ n nfc ps pextra t expn _)

203212 = case lookupCtxtName n (idris_classes i) of

204213 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

205214 case lookupTy iname (tt_ctxt i) of

@@ -256,11 +265,15 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

256265 map snd (filter (\(i, _) -> i `elem` dets) a')

257266 keepDets dets t = t

258267

268+ methName (n, _, _, _) = n

269+ toExp n = pexp (PRef fc [] n)

270+

259271 mkMethApp ps (n, _, _, ty)

260272 = lamBind 0 ty (papp fc (PRef fc [] n)

261− (ps ++ methArgs 0 ty))

273+ (ps ++ map (toExp . fst) pextra ++ methArgs 0 ty))

262274 where

263275 needed is p = pname p `elem` map pname is

276+

264277 lamBind i (PPi (Constraint _ _) _ _ _ sc) sc'

265278 = PLam fc (sMN i "meth") NoFC Placeholder (lamBind (i+1) sc sc')

266279 lamBind i (PPi _ n _ ty sc) sc'

@@ -287,10 +300,10 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

287300 _ -> return ps'

288301 getWParams (_ : ps) = getWParams ps

289302

290− decorate ns iname (UN nm)

291− = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns

292303 decorate ns iname (NS (UN nm) s)

293304 = NS (SN (WhereN 0 iname (SN (MethodN (UN nm))))) ns

305+ decorate ns iname nm

306+ = NS (SN (WhereN 0 iname (SN (MethodN nm)))) ns

294307

295308 mkTyDecl (n, op, t, _)

296309 = PTy emptyDocstring [] syn fc op n NoFC

@@ -300,9 +313,13 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

300313 conbind ((c,ty) : ns) x = PPi constraint c NoFC ty (conbind ns x)

301314 conbind [] x = x

302315

303− coninsert :: [(Name, PTerm)] -> PTerm -> PTerm

304− coninsert cs (PPi p@(Imp _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs sc)

305− coninsert cs sc = conbind cs sc

316+ extrabind :: [(Name, PTerm)] -> PTerm -> PTerm

317+ extrabind ((c,ty) : ns) x = PPi expl c NoFC ty (extrabind ns x)

318+ extrabind [] x = x

319+

320+ coninsert :: [(Name, PTerm)] -> [(Name, PTerm)] -> PTerm -> PTerm

321+ coninsert cs ex (PPi p@(Imp _ _ _ _ _) n fc t sc) = PPi p n fc t (coninsert cs ex sc)

322+ coninsert cs ex sc = conbind cs (extrabind ex sc)

306323

307324 -- Reorder declarations to be in the same order as defined in the

308325 -- class declaration (important so that we insert default definitions

src/Idris/ElabDecls.hs+2−2

@@ -251,9 +251,9 @@ elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)

251251 | what /= EDefns

252252 = do logElab 1 $ "Elaborating class " ++ show n

253253 elabClass info (s { syn_params = [] }) doc f cs n nfc ps pdocs fds ds cn cd

254−elabDecl' what info (PInstance doc argDocs s f cs acc fnopts n nfc ps t expn ds)

254+elabDecl' what info (PInstance doc argDocs s f cs acc fnopts n nfc ps pextra t expn ds)

255255 = do logElab 1 $ "Elaborating instance " ++ show n

256− elabInstance info s doc argDocs what f cs acc fnopts n nfc ps t expn ds

256+ elabInstance info s doc argDocs what f cs acc fnopts n nfc ps pextra t expn ds

257257elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)

258258 = do logElab 1 $ "Elaborating record " ++ show name

259259 elabRecord info what doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn

src/Idris/IBC.hs+5−3

@@ -40,7 +40,7 @@ import System.Directory

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 138

43+ibcVersion = 139

4444

4545-- When IBC is being loaded - we'll load different things (and omit different

4646-- structures/definitions) depending on which phase we're in

@@ -1371,7 +1371,7 @@ instance (Binary t) => Binary (PDecl' t) where

13711371 put x10

13721372 put x11

13731373 put x12

1374− PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 ->

1374+ PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 ->

13751375 do putWord8 8

13761376 put x1

13771377 put x2

@@ -1386,6 +1386,7 @@ instance (Binary t) => Binary (PDecl' t) where

13861386 put x11

13871387 put x12

13881388 put x13

1389+ put x14

13891390 PDSL x1 x2 -> do putWord8 9

13901391 put x1

13911392 put x2

@@ -1502,7 +1503,8 @@ instance (Binary t) => Binary (PDecl' t) where

15021503 x11 <- get

15031504 x12 <- get

15041505 x13 <- get

1505− return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13)

1506+ x14 <- get

1507+ return (PInstance x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14)

15061508 9 -> do x1 <- get

15071509 x2 <- get

15081510 return (PDSL x1 x2)

src/Idris/Parser.hs+3−3

@@ -337,9 +337,9 @@ declExtension syn ns rules =

337337 (map (updateNs ns) ds)

338338 (updateRecCon ns cname)

339339 cdocs

340− updateNs ns (PInstance docs pdocs s fc cs acc opts cn fc' ps ity ni ds)

340+ updateNs ns (PInstance docs pdocs s fc cs acc opts cn fc' ps pextra ity ni ds)

341341 = PInstance docs pdocs s fc cs acc opts (updateB ns cn) fc'

342− ps ity (fmap (updateB ns) ni)

342+ ps pextra ity (fmap (updateB ns) ni)

343343 (map (updateNs ns) ds)

344344 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)

345345 updateNs ns (PProvider docs s fc fc' pw n)

@@ -941,7 +941,7 @@ instance_ kwopt syn

941941 let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

942942 let t = bindList (PPi constraint) cs sc

943943 ds <- instanceBlock syn

944− return [PInstance doc argDocs syn fc cs' acc opts' cn cnfc args t en ds]

944+ return [PInstance doc argDocs syn fc cs' acc opts' cn cnfc args [] t en ds]

945945 <?> "implementation declaration"

946946 where instanceName :: IdrisParser Name

947947 instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

src/Idris/Parser/Helpers.hs+2−2

@@ -691,7 +691,7 @@ collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

691691collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds

692692collect (PClass doc f s cs n nfc ps pdocs fds ds cn cd : ds')

693693 = PClass doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'

694−collect (PInstance doc argDocs f s cs acc opts n nfc ps t en ds : ds')

695− = PInstance doc argDocs f s cs acc opts n nfc ps t en (collect ds) : collect ds'

694+collect (PInstance doc argDocs f s cs acc opts n nfc ps pextra t en ds : ds')

695+ = PInstance doc argDocs f s cs acc opts n nfc ps pextra t en (collect ds) : collect ds'

696696collect (d : ds) = d : collect ds

697697collect [] = []

src/Idris/REPL.hs+2−2

@@ -903,8 +903,8 @@ process fn (NewDefn decls) = do

903903 fixClauses :: PDecl' t -> PDecl' t

904904 fixClauses (PClauses fc opts _ css@(clause:cs)) =

905905 PClauses fc opts (getClauseName clause) css

906− fixClauses (PInstance doc argDocs syn fc constraints acc opts cls nfc parms ty instName decls) =

907− PInstance doc argDocs syn fc constraints acc opts cls nfc parms ty instName (map fixClauses decls)

906+ fixClauses (PInstance doc argDocs syn fc constraints acc opts cls nfc parms pextra ty instName decls) =

907+ PInstance doc argDocs syn fc constraints acc opts cls nfc parms pextra ty instName (map fixClauses decls)

908908 fixClauses decl = decl

909909

910910process fn (Undefine names) = undefine names

test/interfaces003/expectednew file+2

@@ -0,0 +1,2 @@

1+10

2+9

test/interfaces003/interfaces003.idrnew file+21

@@ -0,0 +1,21 @@

1+interface NumMod where

2+ number : Bool -> Int

3+

4+implementation [five] NumMod where

5+ number b = 5

6+

7+foo : NumMod => Int

8+foo = number True + number False

9+

10+increment : Int -> NumMod -> NumMod

11+increment inc x = addOne

12+ where

13+ foo : NumMod

14+ foo = x

15+

16+ implementation [addOne] NumMod where

17+ number x = if x then number@{foo} x + inc else inc

18+

19+main : IO ()

20+main = do printLn (foo @{five})

21+ printLn (foo @{increment 2 five})

test/interfaces003/runnew file+4

@@ -0,0 +1,4 @@

1+#!/usr/bin/env bash

2+${IDRIS:-idris} $@ --nocolour --consolewidth 70 interfaces003.idr -o interfaces003

3+./interfaces003

4+rm -f interfaces003 *.ibc