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

idris.cabal+3

compare with master

unifiedsplit

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

611 test/interfaces002/*.idr

612 test/interfaces002/run

613 test/interfaces002/expected

614+ test/interfaces003/*.idr

615+ test/interfaces003/run

616+ test/interfaces003/expected

614

617

615 test/io001/run

618 test/io001/run

616 test/io001/*.idr

619 test/io001/*.idr

src/Idris/AbsSyntax.hs+14−5

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

1249 updateps yn nm [] = []

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

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

1253

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

1255

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

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

1291 cn

1292 cd

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

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

1294− = PInstance doc argDocs info f

1297+ PInstance doc argDocs info f

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

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

1296 acc opts n

1299 acc opts n

1297 nfc

1300 nfc

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

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

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

1299 (expandParams dec ps ns [] ty)

1303 (expandParams dec ps ns [] ty)

1300− cn

1304+ cn'

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

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

1302expandParamsD rhs ist dec ps ns d = d

1306expandParamsD rhs ist dec ps ns d = d

1303

1307

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

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

1305

1309

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+

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

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

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

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

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

1317-- * 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

738 Name -- class

739 FC -- precise location of class

740 [t] -- parameters

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

741 t -- full instance type

742 t -- full instance type

742 (Maybe Name) -- explicit name

743 (Maybe Name) -- explicit name

743 [PDecl' t]

744 [PDecl' t]

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

900 (map (mapPDeclFC f g) body)

901 (map (mapPDeclFC f g) body)

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

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

902 ctorDoc

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

904 PInstance doc paramDocs syn (f fc)

905 PInstance doc paramDocs syn (f fc)

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

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

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

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

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

907 (mapPTermFC f g instTy)

909 (mapPTermFC f g instTy)

908 instN

910 instN

909 (map (mapPDeclFC f g) body)

911 (map (mapPDeclFC f g) body)

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

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

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

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

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

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

947declared (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]

947declared (PDSL n _) = [n]

952declared (PDSL n _) = [n]

948declared (PSyntax _ _) = []

953declared (PSyntax _ _) = []

949declared (PMutual _ ds) = concatMap declared ds

954declared (PMutual _ ds) = concatMap declared ds

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

963tldeclared (PMutual _ ds) = concatMap tldeclared ds

968tldeclared (PMutual _ ds) = concatMap tldeclared ds

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

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

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

970tldeclared (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]

967tldeclared _ = []

975tldeclared _ = []

968

976

969defined :: PDecl -> [Name]

977defined :: PDecl -> [Name]

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

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

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

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

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

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

989defined (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]

983defined (PDSL n _) = [n]

994defined (PDSL n _) = [n]

984defined (PSyntax _ _) = []

995defined (PSyntax _ _) = []

985defined (PMutual _ ds) = concatMap defined ds

996defined (PMutual _ ds) = concatMap defined ds

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

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

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

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

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

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

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

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

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

2172showDeclImp _ _ = text "..."

2183showDeclImp _ _ = text "..."

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

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

src/Idris/DeepSeq.hs+2−2

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

468 rnf x9 `seq`

469 rnf x10 `seq`

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

472 = rnf x1 `seq`

473 rnf x2 `seq`

474 rnf x3 `seq`

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

477 rnf x6 `seq`

478 rnf x7 `seq`

479 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` ()

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

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

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

src/Idris/Docs.hs+2−2

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

319 namedInst n@(UN _) = Just n

320 namedInst _ = Nothing

321

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

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

323− getDInst _ = Nothing

323+ getDInst _ = Nothing

324

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

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

144

145 -- TODO: probably should normalise

146 checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

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

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

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

150 i <- getIState

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

198

199 tydecl (PTy _ _ _ _ _ _ _ _) = True

200 tydecl _ = False

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

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

202 instdecl _ = False

203 clause (PClauses _ _ _ _) = True

204 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

629

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

631 let wb = map (mkStatic static_names) $

632+ map (expandInstanceScope ist decorate newargs defs) $

632 map (expandParamsD False ist decorate newargs defs) whereblock

633 map (expandParamsD False ist decorate newargs defs) whereblock

633

634

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

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

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

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

637 let (wbefore, wafter) = sepBlocks wb

638 let (wbefore, wafter) = sepBlocks wb

638

639

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

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

640 mapM_ (rec_elabDecl info EAll winfo) wbefore

641 mapM_ (rec_elabDecl info EAll winfo) wbefore

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

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

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

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

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

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

60 Name -> -- the class

61 FC -> -- precise location of class name

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

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

63 PTerm -> -- full instance type

64 PTerm -> -- full instance type

64 Maybe Name -> -- explicit name

65 Maybe Name -> -- explicit name

65 [PDecl] -> Idris ()

66 [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

67 ist <- getIState

68 ist <- getIState

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

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

69 [c] -> return c

70 [c] -> return c

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

79

80

80 let emptyclass = null (class_methods ci)

81 let emptyclass = null (class_methods ci)

81 when (what /= EDefns) $ do

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

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

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

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

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

85 case expn of

87 case expn of

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

125 all_meths

127 all_meths

126 t' = substMatchesShadow mnamemap pnames t_in in

128 t' = substMatchesShadow mnamemap pnames t_in in

127 (decorate ns iname n,

129 (decorate ns iname n,

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

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

129 (class_methods ci)

131 (class_methods ci)

130 logElab 3 (show (mtys, ips))

132 logElab 3 (show (mtys, ips))

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

133 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

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

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

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

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

138 let wbTys = map mkTyDecl mtys

140 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

140 let wb = wbTys ++ wbVals

144 let wb = wbTys ++ wbVals

145+

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

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

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

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

143 show (concat (nub wparams))

148 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

145

150

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

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

147

152

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

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

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

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

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

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

151

156

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

154

159

155 push_estack iname True

160 push_estack iname True

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

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

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

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

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

158

164

159 let idecls = [PClauses fc totopts iname

165 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

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

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

197 Just nm -> nm

203 Just nm -> nm

198

204

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

205+ substInstance ips pnames (PInstance doc argDocs syn _ cs acc opts n nfc ps pextra 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

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

201

210

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

203 = case lookupCtxtName n (idris_classes i) of

212 = case lookupCtxtName n (idris_classes i) of

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

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

205 case lookupTy iname (tt_ctxt i) of

214 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

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

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

257 keepDets dets t = t

266 keepDets dets t = t

258

267

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

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

270+

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

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

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

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

261− (ps ++ methArgs 0 ty))

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

262 where

274 where

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

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

276+

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

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

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

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

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

279 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

287 _ -> return ps'

300 _ -> return ps'

288 getWParams (_ : ps) = getWParams ps

301 getWParams (_ : ps) = getWParams ps

289

302

290− decorate ns iname (UN nm)

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

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

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

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

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

294

307

295 mkTyDecl (n, op, t, _)

308 mkTyDecl (n, op, t, _)

296 = PTy emptyDocstring [] syn fc op n NoFC

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

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

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

301 conbind [] x = x

314 conbind [] x = x

302

315

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+

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

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

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

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

305− coninsert cs sc = conbind cs sc

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

306

323

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

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

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

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

251 | what /= EDefns

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

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

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

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

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

259 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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 138

43+ibcVersion = 139

44

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

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

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

1371 put x10

1372 put x11

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

1375 do putWord8 8

1376 put x1

1377 put x2

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

1386 put x11

1387 put x12

1388 put x13

1389+ put x14

1389 PDSL x1 x2 -> do putWord8 9

1390 PDSL x1 x2 -> do putWord8 9

1390 put x1

1391 put x1

1391 put x2

1392 put x2

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

1502 x11 <- get

1503 x11 <- get

1503 x12 <- get

1504 x12 <- get

1504 x13 <- get

1505 x13 <- get

1506+ x14 <- get

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

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

1506 9 -> do x1 <- get

1508 9 -> do x1 <- get

1507 x2 <- get

1509 x2 <- get

1508 return (PDSL x1 x2)

1510 return (PDSL x1 x2)

src/Idris/Parser.hs+3−3

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

337 (map (updateNs ns) ds)

338 (updateRecCon ns cname)

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

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

343 (map (updateNs ns) ds)

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

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

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

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

942 let t = bindList (PPi constraint) cs sc

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

945 <?> "implementation declaration"

946 where instanceName :: IdrisParser Name

947 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

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

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

693 = 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')

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 t en (collect ds) : collect ds'

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

696collect (d : ds) = d : collect ds

697collect [] = []

src/Idris/REPL.hs+2−2

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

903 fixClauses :: PDecl' t -> PDecl' t

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

905 PClauses fc opts (getClauseName clause) css

906− fixClauses (PInstance doc argDocs syn fc constraints acc opts cls nfc parms ty instName 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 ty instName (map fixClauses decls)

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

908 fixClauses decl = decl

909

910process 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