a41ca33 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

on master help sign in

Merge branch 'master' of https://github.com/idris-lang/Idris-dev into colin-adams-covering

a41ca33Ahmad Salim Al-Sibahi10 years ago

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]`.

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:

idris.cabal+6

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

614 test/interfaces002/*.idr

615 test/interfaces002/run

616 test/interfaces002/expected

617+ test/interfaces003/*.idr

618+ test/interfaces003/run

619+ test/interfaces003/expected

620+ test/interfaces004/*.idr

621+ test/interfaces004/run

622+ test/interfaces004/expected

617

623

618 test/io001/run

624 test/io001/run

619 test/io001/*.idr

625 test/io001/*.idr

src/Idris/AbsSyntax.hs+42−6

@@ -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 n ++ "_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,19 +1317,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)

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

1321+ = let cn' = case cn of

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

1323+ Nothing -> Nothing in

1294− = PInstance doc argDocs info f

1324+ PInstance doc argDocs info f

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

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

1296− acc opts n

1326+ pnames acc opts n

1297 nfc

1327 nfc

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

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

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

1299 (expandParams dec ps ns [] ty)

1330 (expandParams dec ps ns [] ty)

1300− cn

1331+ cn'

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

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

1302expandParamsD rhs ist dec ps ns d = d

1333expandParamsD rhs ist dec ps ns d = d

1303

1334

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

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

1305

1336

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

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

1339+ ty cn decls

1340+expandInstanceScope ist dec ps ns d = d

1341+

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

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

1343-- * 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)

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

src/Idris/AbsSyntaxTree.hs+27−7

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

196 idris_implicits :: Ctxt [PArg],

197 idris_statics :: Ctxt [Bool],

198 idris_classes :: Ctxt ClassInfo,

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

199 idris_records :: Ctxt RecordInfo,

200 idris_records :: Ctxt RecordInfo,

200 idris_dsls :: Ctxt DSL,

201 idris_dsls :: Ctxt DSL,

201 idris_optimisation :: Ctxt OptInfo,

202 idris_optimisation :: Ctxt OptInfo,

@@ -359,7 +360,7 @@ data IBCWrite = IBCFix FixDecl

359-- | The initial state for the compiler

360-- | The initial state for the compiler

360idrisInit :: IState

361idrisInit :: IState

361idrisInit = IState initContext S.empty []

362idrisInit = IState initContext S.empty []

362− emptyContext emptyContext emptyContext emptyContext

363+ emptyContext emptyContext emptyContext [] emptyContext

363 emptyContext emptyContext emptyContext emptyContext

364 emptyContext emptyContext emptyContext emptyContext

365 emptyContext emptyContext emptyContext emptyContext

366 emptyContext emptyContext emptyContext emptyContext

@@ -708,6 +709,7 @@ data PDecl' t

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

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

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

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

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

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

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

711 | PNamespace String FC [PDecl' t]

713 | PNamespace String FC [PDecl' t]

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

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

713 -- namespace in the file

715 -- namespace in the file

@@ -738,11 +740,13 @@ data PDecl' t

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

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

739 SyntaxInfo

741 SyntaxInfo

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

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

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

741 Accessibility

744 Accessibility

742 FnOpts

745 FnOpts

743 Name -- class

746 Name -- class

744 FC -- precise location of class

747 FC -- precise location of class

745 [t] -- parameters

748 [t] -- parameters

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

746 t -- full instance type

750 t -- full instance type

747 (Maybe Name) -- explicit name

751 (Maybe Name) -- explicit name

748 [PDecl' t]

752 [PDecl' t]

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

885 PParams (f fc)

889 PParams (f fc)

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

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

887 (map (mapPDeclFC f g) decls)

891 (map (mapPDeclFC f g) decls)

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

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

888mapPDeclFC f g (PNamespace ns fc decls) =

894mapPDeclFC f g (PNamespace ns fc decls) =

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

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

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

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

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

905 (map (mapPDeclFC f g) body)

911 (map (mapPDeclFC f g) body)

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

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

907 ctorDoc

913 ctorDoc

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

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

909 PInstance doc paramDocs syn (f fc)

915 PInstance doc paramDocs syn (f fc)

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

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

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

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

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

912 (mapPTermFC f g instTy)

919 (mapPTermFC f g instTy)

913 instN

920 instN

914 (map (mapPDeclFC f g) body)

921 (map (mapPDeclFC f g) body)

@@ -945,10 +952,14 @@ declared (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

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

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

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

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

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

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

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

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

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

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

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

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

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

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

959+declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

960+ = case mn of

961+ Nothing -> []

962+ Just n -> [n]

952declared (PDSL n _) = [n]

963declared (PDSL n _) = [n]

953declared (PSyntax _ _) = []

964declared (PSyntax _ _) = []

954declared (PMutual _ ds) = concatMap declared ds

965declared (PMutual _ ds) = concatMap declared ds

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

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

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

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

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

967tldeclared (PParams _ _ ds) = []

978tldeclared (PParams _ _ ds) = []

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

968tldeclared (PMutual _ ds) = concatMap tldeclared ds

980tldeclared (PMutual _ ds) = concatMap tldeclared ds

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

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

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

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

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

983+tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

984+ = case mn of

985+ Nothing -> []

986+ Just n -> [n]

972tldeclared _ = []

987tldeclared _ = []

973

988

974defined :: PDecl -> [Name]

989defined :: PDecl -> [Name]

@@ -981,10 +996,14 @@ defined (PData _ _ _ _ _ (PDatadecl n _ _ ts)) = n : map fstt ts

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1003+defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

1004+ = case mn of

1005+ Nothing -> []

1006+ Just n -> [n]

988defined (PDSL n _) = [n]

1007defined (PDSL n _) = [n]

989defined (PSyntax _ _) = []

1008defined (PSyntax _ _) = []

990defined (PMutual _ ds) = concatMap defined ds

1009defined (PMutual _ ds) = concatMap defined ds

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2177showDeclImp _ _ = text "..."

2197showDeclImp _ _ = text "..."

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

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

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

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

@@ -703,8 +704,8 @@ instance NFData IState where

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

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

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

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

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

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

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

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

707 = 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`

708 = 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`

708 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`

709 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`

709 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`

710 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`

710− 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` ()

711+ 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/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+73−30

@@ -55,15 +55,17 @@ 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

61 FC -> -- precise location of class name

62 FC -> -- precise location of class name

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

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

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

63 PTerm -> -- full instance type

65 PTerm -> -- full instance type

64 Maybe Name -> -- explicit name

66 Maybe Name -> -- explicit name

65 [PDecl] -> Idris ()

67 [PDecl] -> Idris ()

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

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

67 ist <- getIState

69 ist <- getIState

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

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

69 [c] -> return c

71 [c] -> return c

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

80 let emptyclass = null (class_methods ci)

82 let emptyclass = null (class_methods ci)

81 when (what /= EDefns) $ do

83 when (what /= EDefns) $ do

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

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

85+ (piBindp expl_param pextra t)

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

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

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

85 case expn of

88 case expn of

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

88 addInstance intInst True n iname

91 addInstance intInst True n iname

89 Just _ -> addInstance intInst False n iname

92 Just _ -> addInstance intInst False n iname

90 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+

91 let ips = zip (class_params ci) ps

97 let ips = zip (class_params ci) ps

92 let ns = case n of

98 let ns = case n of

93 NS n ns' -> ns'

99 NS n ns' -> ns'

@@ -105,14 +111,27 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

105 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

111 let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

106 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances

112 undefinedSuperclassInstances <- filterM (fmap not . isOverlapping ist) superclassInstances

107 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

113 mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

114+

115+ ist <- getIState

116+ -- Bring variables in instance head into scope when building the

117+ -- dictionary

118+ let headVars = nub $ concatMap getHeadVars ps

119+ let (headVarTypes, ty)

120+ = case lookupTyExact iname (tt_ctxt ist) of

121+ Just ty -> (map (\n -> (n, getTypeIn ist n ty)) headVars, ty)

122+ _ -> (zip headVars (repeat Placeholder), Erased)

123+ logElab 3 $ "Head var types " ++ show headVarTypes ++ " from " ++ show ty

124+

108 let all_meths = map (nsroot . fst) (class_methods ci)

125 let all_meths = map (nsroot . fst) (class_methods ci)

109 let mtys = map (\ (n, (op, t)) ->

126 let mtys = map (\ (n, (op, t)) ->

110 let t_in = substMatchesShadow ips pnames t

127 let t_in = substMatchesShadow ips pnames t

128+ mnamemap =

111− mnamemap = map (\n -> (n, PRef fc [] (decorate ns iname n)))

129+ map (\n -> (n, PApp fc (PRef fc [] (decorate ns iname n))

130+ (map (toImp fc) headVars)))

112 all_meths

131 all_meths

113 t' = substMatchesShadow mnamemap pnames t_in in

132 t' = substMatchesShadow mnamemap pnames t_in in

114 (decorate ns iname n,

133 (decorate ns iname n,

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

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

116 (class_methods ci)

135 (class_methods ci)

117 logElab 3 (show (mtys, ips))

136 logElab 3 (show (mtys, ips))

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

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

@@ -123,19 +142,19 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

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

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

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

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

125 let wbTys = map mkTyDecl mtys

144 let wbTys = map mkTyDecl mtys

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

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

146+ ist <- getIState

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

127 let wb = wbTys ++ wbVals

148 let wb = wbTys ++ wbVals

149+

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

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

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

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

130 show (concat (nub wparams))

152 show (concat (nub wparams))

131

153

132− -- Bring variables in instance head into scope when building the

154+

133− -- dictionary

134− let headVars = nub $ concatMap getHeadVars ps

135−

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

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

137

156

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

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

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

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

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

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

141

160

@@ -144,12 +163,13 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

144

163

145 push_estack iname True

164 push_estack iname True

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

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

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

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

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

148

168

149 let idecls = [PClauses fc totopts iname

169 let idecls = [PClauses fc totopts iname

150 [PClause fc iname lhs [] rhs []]]

170 [PClause fc iname lhs [] rhs []]]

151

171

152− mapM_ (rec_elabDecl info EAll info) (map (impBind headVars) wbTys)

172+ mapM_ (rec_elabDecl info EAll info) (map (impBind headVarTypes) wbTys)

153 mapM_ (rec_elabDecl info EAll info) idecls

173 mapM_ (rec_elabDecl info EAll info) idecls

154

174

155 ctxt <- getContext

175 ctxt <- getContext

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

169 mapM_ (rec_elabDecl info EAll info) wbVals'

189 mapM_ (rec_elabDecl info EAll info) wbVals'

170

190

171 pop_estack

191 pop_estack

192+

193+ setOpenImpl oldOpen

172-- totalityCheckBlock

194-- totalityCheckBlock

173

195

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

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

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

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

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

187 Just nm -> nm

209 Just nm -> nm

188

210

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

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

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

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

213+ (map (substMatchesShadow ips pnames) ps)

214+ pextra

215+ (substMatchesShadow ips pnames t) expn ds

191

216

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

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

193 = case lookupCtxtName n (idris_classes i) of

218 = case lookupCtxtName n (idris_classes i) of

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

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

195 case lookupTy iname (tt_ctxt i) of

220 case lookupTy iname (tt_ctxt i) of

@@ -246,9 +271,15 @@ elabInstance info syn doc argDocs what fc cs acc opts n nfc ps t expn ds = do

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

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

247 keepDets dets t = t

272 keepDets dets t = t

248

273

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

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

276+

249− mkMethApp ps (n, _, _, ty)

277+ mkMethApp ps (n, _, _, ty)

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

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

251− (ps ++ methArgs 0 ty))

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

280+ where

281+ needed is p = pname p `elem` map pname is

282+

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

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

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

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

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

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

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

275 _ -> return ps'

306 _ -> return ps'

276 getWParams (_ : ps) = getWParams ps

307 getWParams (_ : ps) = getWParams ps

277

308

278− decorate ns iname (UN nm)

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

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

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

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

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

311+ decorate ns iname nm

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

282

313

283 mkTyDecl (n, op, t, _)

314 mkTyDecl (n, op, t, _)

284 = PTy emptyDocstring [] syn fc op n NoFC

315 = PTy emptyDocstring [] syn fc op n NoFC

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

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

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

289 conbind [] x = x

320 conbind [] x = x

290

321

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

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

324+ extrabind [] x = x

325+

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

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

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

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

293− coninsert cs sc = conbind cs sc

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

294

329

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

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

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

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

@@ -346,19 +381,28 @@ getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars

346getHeadVars _ = []

381getHeadVars _ = []

347

382

348-- Implicitly bind variables from the instance head in method types

383-- Implicitly bind variables from the instance head in method types

349−impBind :: [Name] -> PDecl -> PDecl

384+impBind :: [(Name, PTerm)] -> PDecl -> PDecl

350impBind vs (PTy d ds syn fc opts n fc' t)

385impBind vs (PTy d ds syn fc opts n fc' t)

351− = PTy d ds syn fc opts n fc' (doImpBind (vs \\ boundIn t) t)

386+ = PTy d ds syn fc opts n fc'

387+ (doImpBind (filter (\(n, ty) -> n `notElem` boundIn t) vs) t)

352 where

388 where

353 doImpBind [] ty = ty

389 doImpBind [] ty = ty

390+ doImpBind ((n, argty) : ns) ty

354− doImpBind (n : ns) ty = PPi impl n NoFC Placeholder (doImpBind ns ty)

391+ = PPi impl n NoFC argty (doImpBind ns ty)

355

392

356 boundIn (PPi _ n _ _ sc) = n : boundIn sc

393 boundIn (PPi _ n _ _ sc) = n : boundIn sc

357 boundIn _ = []

394 boundIn _ = []

358

395

396+getTypeIn :: IState -> Name -> Type -> PTerm

397+getTypeIn ist n (Bind x b sc)

398+ | n == x = delab ist (binderTy b)

399+ | otherwise = getTypeIn ist n (substV (P Ref x Erased) sc)

400+getTypeIn ist n tm = Placeholder

401+

402+toImp fc n = pimp n (PRef fc [] n) True

359

403

360-- Propagate class parameters to method bodies, if they're not already

404-- Propagate class parameters to method bodies, if they're not already

361−-- there

405+-- there, and they are needed (i.e. appear in method's type)

362addParams :: [Name] -> PDecl -> PDecl

406addParams :: [Name] -> PDecl -> PDecl

363addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)

407addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)

364 where

408 where

@@ -369,13 +413,12 @@ addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)

369 (map (addParams ps) ds)

413 (map (addParams ps) ds)

370 addCParams c = c

414 addCParams c = c

371

415

416+ addTmParams ps (PRef fc hls n)

372− addTmParams ps (PRef fc hls n) = PApp fc (PRef fc hls n) (map toImp ps)

417+ = PApp fc (PRef fc hls n) (map (toImp fc) ps)

373 addTmParams ps (PApp fc ap@(PRef fc' hls n) args)

418 addTmParams ps (PApp fc ap@(PRef fc' hls n) args)

374− = PApp fc ap (mergePs (map toImp ps) args)

419+ = PApp fc ap (mergePs (map (toImp fc) ps) args)

375 addTmParams ps tm = tm

420 addTmParams ps tm = tm

376

421

377− toImp n = pimp n (PRef fc [] n) True

378−

379 mergePs [] args = args

422 mergePs [] args = args

380 mergePs (p : ps) args

423 mergePs (p : ps) args

381 | isImplicit p,

424 | isImplicit p,

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 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 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+15−3

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

40import Codec.Archive.Zip

42ibcVersion :: Word16

43−ibcVersion = 138

43+ibcVersion = 140

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

1375 do putWord8 8

1376 put x1

1377 put x2

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

1386 put x11

1387 put x12

1388 put x13

1389+ put x14

1390+ put x15

1389 PDSL x1 x2 -> do putWord8 9

1391 PDSL x1 x2 -> do putWord8 9

1390 put x1

1392 put x1

1391 put x2

1393 put x2

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

1427 put x1

1429 put x1

1428 put x2

1430 put x2

1429 put x3

1431 put x3

1432+ POpenInterfaces x1 x2 x3 -> do putWord8 18

1433+ put x1

1434+ put x2

1435+ put x3

1430 get

1436 get

1431 = do i <- getWord8

1437 = do i <- getWord8

1432 case i of

1438 case i of

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

1502 x11 <- get

1508 x11 <- get

1503 x12 <- get

1509 x12 <- get

1504 x13 <- get

1510 x13 <- get

1511+ x14 <- get

1512+ x15 <- get

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

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

1506 9 -> do x1 <- get

1514 9 -> do x1 <- get

1507 x2 <- get

1515 x2 <- get

1508 return (PDSL x1 x2)

1516 return (PDSL x1 x2)

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

1542 x2 <- get

1550 x2 <- get

1543 x3 <- get

1551 x3 <- get

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

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

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

1546

1558

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

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

src/Idris/Parser.hs+32−4

@@ -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,9 +338,9 @@ 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 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 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)

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

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

@@ -780,6 +781,26 @@ params syn =

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

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

781 <?> "parameters declaration"

782 <?> "parameters declaration"

782

783

784+{- | Parses an open block

785+

786+-}

787+

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

789+openInterface syn =

790+ do reservedHL "using"

791+ reservedHL "implementation"

792+ fc <- getFC

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

794+

795+ openBlock

796+ ds <- many (decl syn)

797+ closeBlock

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

799+ <?> "open interface declaration"

800+

801+

802+

803+

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

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

784

805

785@

806@

@@ -946,8 +967,9 @@ instance_ kwopt syn

946 args <- many (simpleExpr syn)

967 args <- many (simpleExpr syn)

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

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

948 let t = bindList (PPi constraint) cs sc

969 let t = bindList (PPi constraint) cs sc

970+ pnames <- instanceUsing

949 ds <- instanceBlock syn

971 ds <- instanceBlock syn

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

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

951 <?> "implementation declaration"

973 <?> "implementation declaration"

952 where instanceName :: IdrisParser Name

974 where instanceName :: IdrisParser Name

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

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

@@ -960,6 +982,12 @@ instance_ kwopt syn

960 fc <- getFC

982 fc <- getFC

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

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

962

984

985+ instanceUsing :: IdrisParser [Name]

986+ instanceUsing = do reservedHL "using"

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

988+ return (map fst ns)

989+ <|> return []

990+

963-- | Parse a docstring

991-- | Parse a docstring

964docstring :: SyntaxInfo

992docstring :: SyntaxInfo

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

993 -> 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 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 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 = idris_openimpls ist ++ findInstances ist t

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 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 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/interfaces002/expected−4

@@ -1,5 +1 @@

1−WARNING: There are incomplete holes:

2− [Main.prf]

3−

4−Evaluation of any of these will crash at run time.

541

141

test/interfaces002/interfaces002.idr+1−1

@@ -34,6 +34,6 @@ testSum : Array n Int -> Int

34testSum = sumArray

36main : IO ()

37−main = printLn (testSum (upd 11 2 ?prf (create 4 10)))

37+main = printLn (testSum (upd 11 1 (LTESucc (LTESucc LTEZero)) (create 4 10)))

test/interfaces003/expectednew file+2

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

1+10

2+9

test/interfaces003/interfaces003.idrnew file+22

@@ -0,0 +1,22 @@

1+interface NumMod where

2+ number : Bool -> Int

4+implementation [Five] NumMod where

5+ number b = 5

7+foo : NumMod => Int

8+foo = number True + number False

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+using implementation Five

20+ main : IO ()

21+ main = do printLn foo

22+ 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

test/interfaces004/expectednew file+4

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

1+12

2+36

3+True

4+False

test/interfaces004/interfaces004.idrnew file+35

@@ -0,0 +1,35 @@

2+[PlusNatSemi] Semigroup Nat where

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

5+[MultNatSemi] Semigroup Nat where

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

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+[CmpLess] Ord Int where

18+ compare x y = if (x == y) then EQ else

19+ if (boolOp prim__sltInt x y) then GT else LT

20+

21+foo : Int -> Int -> Bool

22+foo x y = x < y

23+

24+using implementation CmpLess

25+ foo' : Int -> Int -> Bool

26+ foo' x y = x < y

27+

28+using implementation PlusNatMonoid

29+ main : IO ()

30+ main = do printLn (test (the Nat 6))

31+ printLn (test @{MultNatMonoid} 6)

32+

33+ printLn (foo 3 4)

34+ printLn (foo' 3 4)

35+

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