254a227 · Idris-dev · git.iko.soy

CHANGELOG.md+32

compare with master

unifiedsplit

@@ -6,6 +6,38 @@

6 dependent types

7* `rewrite` can now be given an optional rewriting lemma, with the syntax

8 `rewrite [rule] using [rewrite_lemma] in [scope]`.

9+

10+* Reorganised elaboration of `implementation`, so that interfaces with

11+ dependencies between methods now work more smoothly

12+

13+* Allow naming of parent implementations when defining an implementation.

14+ For example:

15+

16+ ```

17+ [PlusNatSemi] Semigroup Nat where

18+ (<+>) x y = x + y

19+

20+ [MultNatSemi] Semigroup Nat where

21+ (<+>) x y = x * y

22+

23+ -- use PlusNatSemi as the parent implementation

24+ [PlusNatMonoid] Monoid Nat using PlusNatSemi where

25+ neutral = 0

26+

27+ -- use MultNatSemi as the parent implementation

28+ [MultNatMonoid] Monoid Nat using MultNatSemi where

29+ neutral = 1

30+ ```

31+

32+* Experimentally, allow named implementations to be available by default in a

33+ block of declarations with `using` notation. For example:

34+

35+ ```

36+ using implementation PlusNatMonoid

37+ test : Nat -> Nat

38+ test x = x <+> x <+> neutral

39+ ```

40+

9* Experimental extended `with` syntax, which allows calling functions defined

41* Experimental extended `with` syntax, which allows calling functions defined

10 in a with block directly. For example:

42 in a with block directly. For example:

11

43

idris.cabal+3

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

614 test/interfaces003/*.idr

615 test/interfaces003/run

616 test/interfaces003/expected

617+ test/interfaces004/*.idr

618+ test/interfaces004/run

619+ test/interfaces004/expected

617

620

618 test/io001/run

621 test/io001/run

619 test/io001/*.idr

622 test/io001/*.idr

src/Idris/AbsSyntax.hs+32−5

@@ -446,6 +446,33 @@ addInstance int res n i

446 chaser (NS n _) = chaser n

447 chaser _ = False

448

449+-- Add a privileged implementation - one which instance search will happily

450+-- resolve immediately if it is type correct

451+-- This is used for naming parent implementations when defining an

452+-- implementation with constraints.

453+-- Returns the old list, so we can revert easily at the end of a block

454+

455+addOpenImpl :: [Name] -> Idris [Name]

456+addOpenImpl ns = do ist <- getIState

457+ ns' <- mapM (checkValid ist) ns

458+ let open = idris_openimpls ist

459+ putIState $ ist { idris_openimpls = nub (ns' ++ open) }

460+ return open

461+ where

462+ checkValid ist n

463+ = case lookupCtxtName n (idris_implicits ist) of

464+ [(n', _)] -> return n'

465+ [] -> throwError (NoSuchVariable n)

466+ more -> throwError (CantResolveAlts (map fst more))

467+

468+setOpenImpl :: [Name] -> Idris ()

469+setOpenImpl ns = do ist <- getIState

470+ putIState $ ist { idris_openimpls = ns }

471+

472+getOpenImpl :: Idris [Name]

473+getOpenImpl = do ist <- getIState

474+ return (idris_openimpls ist)

475+

449addClass :: Name -> ClassInfo -> Idris ()

476addClass :: Name -> ClassInfo -> Idris ()

450addClass n i

477addClass n i

451 = do ist <- getIState

478 = do ist <- getIState

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

1249 updateps yn nm [] = []

1276 updateps yn nm [] = []

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

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

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

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

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

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

1253

1280

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

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

1255

1282

@@ -1290,13 +1317,13 @@ 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)

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

1291 cn

1318 cn

1292 cd

1319 cd

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

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

1294 = let cn' = case cn of

1321 = let cn' = case cn of

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

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

1296 Nothing -> Nothing in

1323 Nothing -> Nothing in

1297 PInstance doc argDocs info f

1324 PInstance doc argDocs info f

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

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

1299− acc opts n

1326+ pnames acc opts n

1300 nfc

1327 nfc

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

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

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

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

@@ -1307,8 +1334,8 @@ expandParamsD rhs ist dec ps ns d = d

1307

1334

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

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

1309

1336

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

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

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

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

1312 ty cn decls

1339 ty cn decls

1313expandInstanceScope ist dec ps ns d = d

1340expandInstanceScope ist dec ps ns d = d

1314

1341

src/Idris/AbsSyntaxTree.hs+16−7

@@ -191,6 +191,7 @@ data IState = IState {

191 idris_implicits :: Ctxt [PArg],

192 idris_statics :: Ctxt [Bool],

193 idris_classes :: Ctxt ClassInfo,

194+ idris_openimpls :: [Name], -- ^ Privileged implementations, will resolve immediately

194 idris_records :: Ctxt RecordInfo,

195 idris_records :: Ctxt RecordInfo,

195 idris_dsls :: Ctxt DSL,

196 idris_dsls :: Ctxt DSL,

196 idris_optimisation :: Ctxt OptInfo,

197 idris_optimisation :: Ctxt OptInfo,

@@ -354,7 +355,7 @@ data IBCWrite = IBCFix FixDecl

354-- | The initial state for the compiler

355-- | The initial state for the compiler

355idrisInit :: IState

356idrisInit :: IState

356idrisInit = IState initContext S.empty []

357idrisInit = IState initContext S.empty []

357− emptyContext emptyContext emptyContext emptyContext

358+ emptyContext emptyContext emptyContext [] emptyContext

358 emptyContext emptyContext emptyContext emptyContext

359 emptyContext emptyContext emptyContext emptyContext

360 emptyContext emptyContext emptyContext emptyContext

361 emptyContext emptyContext emptyContext emptyContext

@@ -703,6 +704,7 @@ data PDecl' t

703 | PCAF FC Name t -- ^ Top level constant

704 | PCAF FC Name t -- ^ Top level constant

704 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

705 | PData (Docstring (Either Err t)) [(Name, Docstring (Either Err t))] SyntaxInfo FC DataOpts (PData' t) -- ^ Data declaration.

705 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

706 | PParams FC [(Name, t)] [PDecl' t] -- ^ Params block

707+ | POpenInterfaces FC [Name] [PDecl' t] -- ^ Open block/declaration

706 | PNamespace String FC [PDecl' t]

708 | PNamespace String FC [PDecl' t]

707 -- ^ New namespace, where FC is accurate location of the

709 -- ^ New namespace, where FC is accurate location of the

708 -- namespace in the file

710 -- namespace in the file

@@ -733,6 +735,7 @@ data PDecl' t

733 [(Name, Docstring (Either Err t))] -- Parameter docs

735 [(Name, Docstring (Either Err t))] -- Parameter docs

734 SyntaxInfo

736 SyntaxInfo

735 FC [(Name, t)] -- constraints

737 FC [(Name, t)] -- constraints

738+ [Name] -- parent dictionaries to search for constraints

736 Accessibility

739 Accessibility

737 FnOpts

740 FnOpts

738 Name -- class

741 Name -- class

@@ -881,6 +884,8 @@ mapPDeclFC f g (PParams fc params decls) =

881 PParams (f fc)

884 PParams (f fc)

882 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)

885 (map (\(n, ty) -> (n, mapPTermFC f g ty)) params)

883 (map (mapPDeclFC f g) decls)

886 (map (mapPDeclFC f g) decls)

887+mapPDeclFC f g (POpenInterfaces fc ifs decls) =

888+ POpenInterfaces (f fc) ifs (map (mapPDeclFC f g) decls)

884mapPDeclFC f g (PNamespace ns fc decls) =

889mapPDeclFC f g (PNamespace ns fc decls) =

885 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)

890 PNamespace ns (f fc) (map (mapPDeclFC f g) decls)

886mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =

891mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorDoc syn') =

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

901 (map (mapPDeclFC f g) body)

906 (map (mapPDeclFC f g) body)

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

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

903 ctorDoc

908 ctorDoc

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

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

905 PInstance doc paramDocs syn (f fc)

910 PInstance doc paramDocs syn (f fc)

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

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

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

912+ pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)

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

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

909 (mapPTermFC f g instTy)

914 (mapPTermFC f g instTy)

910 instN

915 instN

@@ -942,10 +947,11 @@ declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

942 where fstt (_, _, a, _, _, _, _) = a

947 where fstt (_, _, a, _, _, _, _) = a

943declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]

948declared (PData _ _ _ _ _ (PLaterdecl n _ _)) = [n]

944declared (PParams _ _ ds) = concatMap declared ds

949declared (PParams _ _ ds) = concatMap declared ds

950+declared (POpenInterfaces _ _ ds) = concatMap declared ds

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

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

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

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

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

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

948−declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ mn _)

954+declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

949 = case mn of

955 = case mn of

950 Nothing -> []

956 Nothing -> []

951 Just n -> [n]

957 Just n -> [n]

@@ -965,10 +971,11 @@ tldeclared (PRecord _ _ _ _ n _ _ _ _ cn _ _) = n : map fst (maybeToList cn)

965tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

971tldeclared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

966 where fstt (_, _, a, _, _, _, _) = a

972 where fstt (_, _, a, _, _, _, _) = a

967tldeclared (PParams _ _ ds) = []

973tldeclared (PParams _ _ ds) = []

974+tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds

968tldeclared (PMutual _ ds) = concatMap tldeclared ds

975tldeclared (PMutual _ ds) = concatMap tldeclared ds

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

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

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

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

971−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ mn _)

978+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

972 = case mn of

979 = case mn of

973 Nothing -> []

980 Nothing -> []

974 Just n -> [n]

981 Just n -> [n]

@@ -984,10 +991,11 @@ defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

984 where fstt (_, _, a, _, _, _, _) = a

991 where fstt (_, _, a, _, _, _, _) = a

985defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []

992defined (PData _ _ _ _ _ (PLaterdecl n _ _)) = []

986defined (PParams _ _ ds) = concatMap defined ds

993defined (PParams _ _ ds) = concatMap defined ds

994+defined (POpenInterfaces _ _ ds) = concatMap defined ds

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

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

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

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

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

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

990−defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ mn _)

998+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

991 = case mn of

999 = case mn of

992 Nothing -> []

1000 Nothing -> []

993 Just n -> [n]

1001 Just n -> [n]

@@ -2174,11 +2182,12 @@ showDeclImp o (PClauses _ _ n cs) = text "pat" <+> text (showCG n) <+> text "\

2174 indent 2 (vsep (map (showCImp o) cs))

2182 indent 2 (vsep (map (showCImp o) cs))

2175showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

2183showDeclImp o (PData _ _ _ _ _ d) = showDImp o { ppopt_impl = True } d

2176showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

2184showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

2185+showDeclImp o (POpenInterfaces _ ns ps) = text "open" <+> braces (text (show ns) <> line <> showDecls o ps <> line)

2177showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

2186showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (line <> showDecls o ps <> line)

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

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

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

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

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

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

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

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

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

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

2183showDeclImp _ _ = text "..."

2192showDeclImp _ _ = text "..."

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

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

src/Idris/DeepSeq.hs+5−4

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

444 rnf x2 `seq`

445 rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` ()

446 rnf (PParams x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

447+ rnf (POpenInterfaces x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

447 rnf (PNamespace x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

448 rnf (PNamespace x1 x2 x3) = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` ()

448 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

449 rnf (PRecord x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

449 = rnf x1 `seq`

450 = rnf x1 `seq`

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

468 rnf x9 `seq`

469 rnf x9 `seq`

469 rnf x10 `seq`

470 rnf x10 `seq`

470 rnf x11 `seq` rnf x12 `seq` ()

471 rnf x11 `seq` rnf x12 `seq` ()

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

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

472 = rnf x1 `seq`

473 = rnf x1 `seq`

473 rnf x2 `seq`

474 rnf x2 `seq`

474 rnf x3 `seq`

475 rnf x3 `seq`

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

477 rnf x6 `seq`

478 rnf x6 `seq`

478 rnf x7 `seq`

479 rnf x7 `seq`

479 rnf x8 `seq`

480 rnf x8 `seq`

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

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

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

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

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

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

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

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

@@ -699,8 +700,8 @@ instance NFData IState where

699 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

700 rnf (IState x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12 x13 x14 x15 x16 x17 x18 x19 x20

700 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40

701 x21 x22 x23 x24 x25 x26 x27 x28 x29 x30 x31 x32 x33 x34 x35 x36 x37 x38 x39 x40

701 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60

702 x41 x42 x43 x44 x45 x46 x47 x48 x49 x50 x51 x52 x53 x54 x55 x56 x57 x58 x59 x60

702− x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76)

703+ x61 x62 x63 x64 x65 x66 x67 x68 x69 x70 x71 x72 x73 x74 x75 x76 x77)

703 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq`

704 = rnf x1 `seq` rnf x2 `seq` rnf x3 `seq` rnf x4 `seq` rnf x5 `seq` rnf x6 `seq` rnf x7 `seq` rnf x8 `seq` rnf x9 `seq` rnf x10 `seq` () `seq` rnf x11 `seq` rnf x12 `seq` rnf x13 `seq` rnf x14 `seq` rnf x15 `seq` rnf x16 `seq` rnf x17 `seq` rnf x18 `seq` rnf x19 `seq` rnf x20 `seq`

704 rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq`

705 rnf x21 `seq` rnf x22 `seq` rnf x23 `seq` rnf x24 `seq` rnf x25 `seq` rnf x26 `seq` rnf x27 `seq` rnf x28 `seq` rnf x29 `seq` rnf x30 `seq` rnf x31 `seq` rnf x32 `seq` rnf x33 `seq` rnf x34 `seq` rnf x35 `seq` rnf x36 `seq` rnf x37 `seq` rnf x38 `seq` rnf x39 `seq` rnf x40 `seq`

705 rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`

706 rnf x41 `seq` rnf x42 `seq` rnf x43 `seq` rnf x44 `seq` rnf x45 `seq` rnf x46 `seq` rnf x47 `seq` rnf x48 `seq` rnf x49 `seq` rnf x50 `seq` rnf x51 `seq` rnf x52 `seq` rnf x53 `seq` rnf x54 `seq` rnf x55 `seq` rnf x56 `seq` rnf x57 `seq` rnf x58 `seq` rnf x59 `seq` rnf x60 `seq`

706− rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` rnf x75 `seq` rnf x76 `seq` ()

707+ rnf x61 `seq` rnf x62 `seq` rnf x63 `seq` rnf x64 `seq` rnf x65 `seq` rnf x66 `seq` rnf x67 `seq` rnf x68 `seq` rnf x69 `seq` rnf x70 `seq` rnf x71 `seq` rnf x72 `seq` rnf x73 `seq` rnf x74 `seq` rnf x75 `seq` rnf x76 `seq` rnf x77 `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+4−4

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

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

196 defaultdec (UN n) = sUN ("default#" ++ str n)

197 defaultdec (NS n ns) = NS (defaultdec n) ns

198

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

199+ tydecl (PTy{}) = True

200 tydecl _ = False

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

201+ instdecl (PInstance{}) = True

202 instdecl _ = False

203− clause (PClauses _ _ _ _) = True

203+ clause (PClauses{}) = True

204 clause _ = False

205

206 -- Generate a function for chasing a dictionary constraint

src/Idris/Elab/Instance.hs+10−4

@@ -55,6 +55,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

55 [(Name, Docstring (Either Err PTerm))] ->

56 ElabWhat -> -- phase

57 FC -> [(Name, PTerm)] -> -- constraints

58+ [Name] -> -- parent dictionary names (optionally)

58 Accessibility ->

59 Accessibility ->

59 FnOpts ->

60 FnOpts ->

60 Name -> -- the class

61 Name -> -- the class

@@ -64,7 +65,7 @@ elabInstance :: ElabInfo -> SyntaxInfo ->

64 PTerm -> -- full instance type

65 PTerm -> -- full instance type

65 Maybe Name -> -- explicit name

66 Maybe Name -> -- explicit name

66 [PDecl] -> Idris ()

67 [PDecl] -> Idris ()

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

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

68 ist <- getIState

69 ist <- getIState

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

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

70 [c] -> return c

71 [c] -> return c

@@ -90,6 +91,9 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps pextra t expn ds

90 addInstance intInst True n iname

91 addInstance intInst True n iname

91 Just _ -> addInstance intInst False n iname

92 Just _ -> addInstance intInst False n iname

92 when (what /= ETypes && (not (null ds && not emptyclass))) $ do

93 when (what /= ETypes && (not (null ds && not emptyclass))) $ do

94+ -- Add the parent implementation names to the privileged set

95+ oldOpen <- addOpenImpl parents

96+

93 let ips = zip (class_params ci) ps

97 let ips = zip (class_params ci) ps

94 let ns = case n of

98 let ns = case n of

95 NS n ns' -> ns'

99 NS n ns' -> ns'

@@ -185,6 +189,8 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps pextra t expn ds

185 mapM_ (rec_elabDecl info EAll info) wbVals'

189 mapM_ (rec_elabDecl info EAll info) wbVals'

186

190

187 pop_estack

191 pop_estack

192+

193+ setOpenImpl oldOpen

188-- totalityCheckBlock

194-- totalityCheckBlock

189

195

190 checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))

196 checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))

@@ -202,13 +208,13 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps pextra t expn ds

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

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

203 Just nm -> nm

209 Just nm -> nm

204

210

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

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

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

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

207 (map (substMatchesShadow ips pnames) ps)

213 (map (substMatchesShadow ips pnames) ps)

208 pextra

214 pextra

209 (substMatchesShadow ips pnames t) expn ds

215 (substMatchesShadow ips pnames t) expn ds

210

216

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

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

212 = case lookupCtxtName n (idris_classes i) of

218 = case lookupCtxtName n (idris_classes i) of

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

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

214 case lookupTy iname (tt_ctxt i) of

220 case lookupTy iname (tt_ctxt i) of

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

@@ -85,7 +85,7 @@ build ist info emode opts fn tm

85 mapM_ (\n -> when (n `elem` hs) $

86 do focus n

87 g <- goal

88− try (resolveTC' True False 10 g fn ist)

88+ try (resolveTC' True True 10 g fn ist)

89 (movelast n)) ivs

90 ivs <- get_instances

91 hs <- get_holes

src/Idris/ElabDecls.hs+7−2

@@ -239,6 +239,11 @@ elabDecl' what info (PParams f ns ps)

239 pblock i = map (expandParamsD False i id ns

240 (concatMap tldeclared ps)) ps

241

242+elabDecl' what info (POpenInterfaces f ns ds)

243+ = do open <- addOpenImpl ns

244+ mapM_ (elabDecl' what info) ds

245+ setOpenImpl open

246+

242elabDecl' what info (PNamespace n nfc ps) =

247elabDecl' what info (PNamespace n nfc ps) =

243 do mapM_ (elabDecl' what ninfo) ps

248 do mapM_ (elabDecl' what ninfo) ps

244 let ns = reverse (map T.pack newNS)

249 let ns = reverse (map T.pack newNS)

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

251 | what /= EDefns

256 | what /= EDefns

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

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

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

258 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 pextra t expn ds)

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

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

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

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

261+ elabInstance info s doc argDocs what f cs pnames 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)

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

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

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

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

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

src/Idris/IBC.hs+13−3

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

40import Codec.Archive.Zip

41

42ibcVersion :: Word16

43−ibcVersion = 139

43+ibcVersion = 140

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

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

1375 do putWord8 8

1376 put x1

1377 put x2

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

1387 put x12

1388 put x13

1389 put x14

1390+ put x15

1390 PDSL x1 x2 -> do putWord8 9

1391 PDSL x1 x2 -> do putWord8 9

1391 put x1

1392 put x1

1392 put x2

1393 put x2

@@ -1428,6 +1429,10 @@ instance (Binary t) => Binary (PDecl' t) where

1428 put x1

1429 put x1

1429 put x2

1430 put x2

1430 put x3

1431 put x3

1432+ POpenInterfaces x1 x2 x3 -> do putWord8 18

1433+ put x1

1434+ put x2

1435+ put x3

1431 get

1436 get

1432 = do i <- getWord8

1437 = do i <- getWord8

1433 case i of

1438 case i of

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

1504 x12 <- get

1509 x12 <- get

1505 x13 <- get

1510 x13 <- get

1506 x14 <- get

1511 x14 <- get

1512+ x15 <- get

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

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

1508 9 -> do x1 <- get

1514 9 -> do x1 <- get

1509 x2 <- get

1515 x2 <- get

1510 return (PDSL x1 x2)

1516 return (PDSL x1 x2)

@@ -1544,6 +1550,10 @@ instance (Binary t) => Binary (PDecl' t) where

1544 x2 <- get

1550 x2 <- get

1545 x3 <- get

1551 x3 <- get

1546 return (PRunElabDecl x1 x2 x3)

1552 return (PRunElabDecl x1 x2 x3)

1553+ 18 -> do x1 <- get

1554+ x2 <- get

1555+ x3 <- get

1556+ return (POpenInterfaces x1 x2 x3)

1547 _ -> error "Corrupted binary data for PDecl'"

1557 _ -> error "Corrupted binary data for PDecl'"

1548

1558

1549instance Binary t => Binary (ProvideWhat' t) where

1559instance Binary t => Binary (ProvideWhat' t) where

src/Idris/Parser.hs+31−3

@@ -213,6 +213,7 @@ internalDecl syn

213 where declBody :: Bool -> IdrisParser [PDecl]

214 declBody b =

215 try (instance_ True syn)

216+ <|> try (openInterface syn)

216 <|> declBody' b

217 <|> declBody' b

217 <|> using_ syn

218 <|> using_ syn

218 <|> params syn

219 <|> params syn

@@ -337,8 +338,8 @@ declExtension syn ns rules =

337 (map (updateNs ns) ds)

338 (map (updateNs ns) ds)

338 (updateRecCon ns cname)

339 (updateRecCon ns cname)

339 cdocs

340 cdocs

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

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

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

342+ = PInstance docs pdocs s fc cs pnames acc opts (updateB ns cn) fc'

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

343 ps pextra ity (fmap (updateB ns) ni)

343 (map (updateNs ns) ds)

344 (map (updateNs ns) ds)

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

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

@@ -767,6 +768,26 @@ params syn =

767 return [PParams fc ns' (concat ds)]

768 return [PParams fc ns' (concat ds)]

768 <?> "parameters declaration"

769 <?> "parameters declaration"

769

770

771+{- | Parses an open block

772+

773+-}

774+

775+openInterface :: SyntaxInfo -> IdrisParser [PDecl]

776+openInterface syn =

777+ do reservedHL "using"

778+ reservedHL "implementation"

779+ fc <- getFC

780+ ns <- sepBy1 fnName (lchar ',')

781+

782+ openBlock

783+ ds <- many (decl syn)

784+ closeBlock

785+ return [POpenInterfaces fc (map fst ns) (concat ds)]

786+ <?> "open interface declaration"

787+

788+

789+

790+

770{- | Parses a mutual declaration (for mutually recursive functions)

791{- | Parses a mutual declaration (for mutually recursive functions)

771

792

772@

793@

@@ -940,8 +961,9 @@ instance_ kwopt syn

940 args <- many (simpleExpr syn)

961 args <- many (simpleExpr syn)

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

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

942 let t = bindList (PPi constraint) cs sc

963 let t = bindList (PPi constraint) cs sc

964+ pnames <- instanceUsing

943 ds <- instanceBlock syn

965 ds <- instanceBlock syn

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

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

945 <?> "implementation declaration"

967 <?> "implementation declaration"

946 where instanceName :: IdrisParser Name

968 where instanceName :: IdrisParser Name

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

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

@@ -954,6 +976,12 @@ instance_ kwopt syn

954 fc <- getFC

976 fc <- getFC

955 parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")

977 parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")

956

978

979+ instanceUsing :: IdrisParser [Name]

980+ instanceUsing = do reservedHL "using"

981+ ns <- sepBy1 fnName (lchar ',')

982+ return (map fst ns)

983+ <|> return []

984+

957-- | Parse a docstring

985-- | Parse a docstring

958docstring :: SyntaxInfo

986docstring :: SyntaxInfo

959 -> IdrisParser (Docstring (Either Err PTerm),

987 -> IdrisParser (Docstring (Either Err PTerm),

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

@@ -687,11 +687,12 @@ collect (c@(PClauses _ o _ _) : ds)

687 fcOf :: PDecl -> FC

688 fcOf (PClauses fc _ _ _) = fc

689collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

690+collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds

690collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

691collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

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

692collect (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')

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

695+collect (PInstance doc argDocs f s cs pnames 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'

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

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

697collect (d : ds) = d : collect ds

697collect [] = []

698collect [] = []

src/Idris/ProofSearch.hs+23−11

@@ -339,25 +339,37 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

339-- | Resolve interfaces. This will only pick up 'normal' implementations, never

340-- named implementations (which is enforced by 'findInstances').

341resolveTC :: Bool -- ^ using default Int

342− -> Bool -- ^ allow metavariables in the goal

342+ -> Bool -- ^ allow open implementations

343 -> Int -- ^ depth

344 -> Term -- ^ top level goal, for error messages

345 -> Name -- ^ top level function name, to prevent loops

346 -> (PTerm -> ElabD ()) -- ^ top level elaborator

347 -> IState -> ElabD ()

348−resolveTC def mvok depth top fn elab ist

348+resolveTC def openOK depth top fn elab ist

349− = do hs <- get_holes

349+ = do hs <- get_holes

350− resTC' [] def hs depth top fn elab ist

350+ resTC' [] def openOK hs depth top fn elab ist

351

352−resTC' tcs def topholes 0 topg fn elab ist = fail $ "Can't resolve interface"

352+resTC' tcs def openOK topholes 0 topg fn elab ist = fail $ "Can't resolve interface"

353−resTC' tcs def topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True

353+resTC' tcs def openOK topholes 1 topg fn elab ist = try' (trivial elab ist) (resolveTC def False 0 topg fn elab ist) True

354−resTC' tcs defaultOn topholes depth topg fn elab ist

354+resTC' tcs defaultOn openOK topholes depth topg fn elab ist

355 = do compute

356− g <- goal

356+ if openOK

357+ then try' (resolveOpen (idris_openimpls ist))

358+ resolveNormal

359+ True

360+ else resolveNormal

361+

362+ where

363+ -- try all the Open implementations first

364+ resolveOpen open = do t <- goal

365+ blunderbuss t depth [] open

366+

367+ resolveNormal = do

357 -- Resolution can proceed only if there is something concrete in the

368 -- Resolution can proceed only if there is something concrete in the

358 -- determining argument positions. Keep track of the holes in the

369 -- determining argument positions. Keep track of the holes in the

359 -- non-determining position, because it's okay for 'trivial' to solve

370 -- non-determining position, because it's okay for 'trivial' to solve

360 -- those holes and no others.

371 -- those holes and no others.

372+ g <- goal

361 let (argsok, okholePos) = case tcArgsOK g topholes of

373 let (argsok, okholePos) = case tcArgsOK g topholes of

362 Nothing -> (False, [])

374 Nothing -> (False, [])

363 Just hs -> (True, hs)

375 Just hs -> (True, hs)

@@ -380,9 +392,9 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

380 try' (trivialTCs okholes elab ist)

392 try' (trivialTCs okholes elab ist)

381 (do addDefault t tc ttypes

393 (do addDefault t tc ttypes

382 let stk = map fst (filter snd $ elab_stack ist)

394 let stk = map fst (filter snd $ elab_stack ist)

383− let insts = findInstances ist t

395+ let insts = findInstances ist t ++ idris_openimpls ist

384 blunderbuss t depth stk (stk ++ insts)) True

396 blunderbuss t depth stk (stk ++ insts)) True

385− where

397+

386 -- returns Just hs if okay, where hs are holes which are okay in the

398 -- returns Just hs if okay, where hs are holes which are okay in the

387 -- goal, or Nothing if not okay to proceed

399 -- goal, or Nothing if not okay to proceed

388 tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn

400 tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numclass && defaultOn

@@ -491,7 +503,7 @@ resTC' tcs defaultOn topholes depth topg fn elab ist

491 let got = fst (unApply (getRetTy t))

503 let got = fst (unApply (getRetTy t))

492 let depth' = if tc' `elem` tcs

504 let depth' = if tc' `elem` tcs

493 then depth - 1 else depth

505 then depth - 1 else depth

494− resTC' (got : tcs) defaultOn topholes depth' topg fn elab ist)

506+ resTC' (got : tcs) defaultOn openOK topholes depth' topg fn elab ist)

495 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

507 (filter (\ (x, y) -> not x) (zip (map fst imps) args))

496 -- if there's any arguments left, we've failed to resolve

508 -- if there's any arguments left, we've failed to resolve

497 hs <- get_holes

509 hs <- get_holes

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 pextra ty instName decls) =

906+ fixClauses (PInstance doc argDocs syn fc constraints pnames 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)

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

908 fixClauses decl = decl

909

910process fn (Undefine names) = undefine names

test/interfaces003/interfaces003.idr+8−7

@@ -1,21 +1,22 @@

1interface NumMod where

2 number : Bool -> Int

3

4−implementation [five] NumMod where

4+implementation [Five] NumMod where

5 number b = 5

6

7foo : NumMod => Int

8foo = number True + number False

9

10−increment : Int -> NumMod -> NumMod

10+Increment : Int -> NumMod -> NumMod

11−increment inc x = addOne

11+Increment inc x = AddOne

12 where

13 foo : NumMod

14 foo = x

15

16− implementation [addOne] NumMod where

16+ implementation [AddOne] NumMod where

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

18

19+using implementation Five

19−main : IO ()

20+ main : IO ()

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

21+ main = do printLn foo

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

22+ printLn (foo @{Increment 2 Five})

test/interfaces004/expectednew file+2

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

1+12

2+36

test/interfaces004/interfaces004.idrnew file+19

@@ -0,0 +1,19 @@

1+

2+[PlusNatSemi] Semigroup Nat where

3+ (<+>) x y = x + y

4+

5+[MultNatSemi] Semigroup Nat where

6+ (<+>) x y = x * y

7+

8+[PlusNatMonoid] Monoid Nat using PlusNatSemi where

9+ neutral = 0

10+

11+[MultNatMonoid] Monoid Nat using MultNatSemi where

12+ neutral = 1

13+

14+test : Monoid a => a -> a

15+test x = x <+> x <+> neutral

16+

17+main : IO ()

18+main = do printLn (test @{PlusNatMonoid} 6)

19+ printLn (test @{MultNatMonoid} 6)

test/interfaces004/runnew file+4

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

1+#!/usr/bin/env bash

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

3+./interfaces004

4+rm -f interfaces004 *.ibc