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

CHANGELOG.md+32

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

66 dependent types

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

88 `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+

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

1042 in a with block directly. For example:

1143

idris.cabal+3

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

614614 test/interfaces003/*.idr

615615 test/interfaces003/run

616616 test/interfaces003/expected

617+ test/interfaces004/*.idr

618+ test/interfaces004/run

619+ test/interfaces004/expected

617620

618621 test/io001/run

619622 test/io001/*.idr

src/Idris/AbsSyntax.hs+32−5

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

446446 chaser (NS n _) = chaser n

447447 chaser _ = False

448448

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+

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

450477addClass n i

451478 = do ist <- getIState

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

12491276 updateps yn nm [] = []

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

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

12531280

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

12551282

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

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

12911318 cn

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

12941321 = let cn' = case cn of

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

12961323 Nothing -> Nothing in

12971324 PInstance doc argDocs info f

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

1299− acc opts n

1326+ pnames acc opts n

13001327 nfc

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

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

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

13071334

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

13091336

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

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

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)

13121339 ty cn decls

13131340expandInstanceScope ist dec ps ns d = d

13141341

src/Idris/AbsSyntaxTree.hs+16−7

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

191191 idris_implicits :: Ctxt [PArg],

192192 idris_statics :: Ctxt [Bool],

193193 idris_classes :: Ctxt ClassInfo,

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

194195 idris_records :: Ctxt RecordInfo,

195196 idris_dsls :: Ctxt DSL,

196197 idris_optimisation :: Ctxt OptInfo,

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

354355-- | The initial state for the compiler

355356idrisInit :: IState

356357idrisInit = IState initContext S.empty []

357− emptyContext emptyContext emptyContext emptyContext

358+ emptyContext emptyContext emptyContext [] emptyContext

358359 emptyContext emptyContext emptyContext emptyContext

359360 emptyContext emptyContext emptyContext emptyContext

360361 emptyContext emptyContext emptyContext emptyContext

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

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

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

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

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

706708 | PNamespace String FC [PDecl' t]

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

708710 -- namespace in the file

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

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

734736 SyntaxInfo

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

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

736739 Accessibility

737740 FnOpts

738741 Name -- class

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

881884 PParams (f fc)

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

883886 (map (mapPDeclFC f g) decls)

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

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

884889mapPDeclFC f g (PNamespace ns fc decls) =

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

886891mapPDeclFC 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

901906 (map (mapPDeclFC f g) body)

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

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

905910 PInstance doc paramDocs syn (f fc)

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

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

909914 (mapPTermFC f g instTy)

910915 instN

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

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

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

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

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

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

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

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

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

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

949955 = case mn of

950956 Nothing -> []

951957 Just n -> [n]

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

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

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

967973tldeclared (PParams _ _ ds) = []

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

968975tldeclared (PMutual _ ds) = concatMap tldeclared ds

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

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

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

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

972979 = case mn of

973980 Nothing -> []

974981 Just n -> [n]

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

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

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

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

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

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

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

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

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

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

991999 = case mn of

9921000 Nothing -> []

9931001 Just n -> [n]

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

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

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

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

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

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

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

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

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

21832192showDeclImp _ _ = text "..."

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

src/Idris/DeepSeq.hs+5−4

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

444444 rnf x2 `seq`

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

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

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

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

449450 = rnf x1 `seq`

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

468469 rnf x9 `seq`

469470 rnf x10 `seq`

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

472473 = rnf x1 `seq`

473474 rnf x2 `seq`

474475 rnf x3 `seq`

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

477478 rnf x6 `seq`

478479 rnf x7 `seq`

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

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

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

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

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

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

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

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

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

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

705706 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

319319 namedInst n@(UN _) = Just n

320320 namedInst _ = Nothing

321321

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

323− getDInst _ = Nothing

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

323+ getDInst _ = Nothing

324324

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

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

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

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

144144

145145 -- TODO: probably should normalise

146146 checkDefaultSuperclassInstance :: PDecl -> Idris ()

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

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

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

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

150150 i <- getIState

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

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

197197 defaultdec (NS n ns) = NS (defaultdec n) ns

198198

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

199+ tydecl (PTy{}) = True

200200 tydecl _ = False

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

201+ instdecl (PInstance{}) = True

202202 instdecl _ = False

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

203+ clause (PClauses{}) = True

204204 clause _ = False

205205

206206 -- Generate a function for chasing a dictionary constraint

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

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

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

5656 ElabWhat -> -- phase

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

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

5859 Accessibility ->

5960 FnOpts ->

6061 Name -> -- the class

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

6465 PTerm -> -- full instance type

6566 Maybe Name -> -- explicit name

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

6869 ist <- getIState

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

7071 [c] -> return c

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

9091 addInstance intInst True n iname

9192 Just _ -> addInstance intInst False n iname

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

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

95+ oldOpen <- addOpenImpl parents

96+

9397 let ips = zip (class_params ci) ps

9498 let ns = case n of

9599 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

185189 mapM_ (rec_elabDecl info EAll info) wbVals'

186190

187191 pop_estack

192+

193+ setOpenImpl oldOpen

188194-- totalityCheckBlock

189195

190196 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

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

203209 Just nm -> nm

204210

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

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

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

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

207213 (map (substMatchesShadow ips pnames) ps)

208214 pextra

209215 (substMatchesShadow ips pnames t) expn ds

210216

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

212218 = case lookupCtxtName n (idris_classes i) of

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

214220 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

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

8686 do focus n

8787 g <- goal

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

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

8989 (movelast n)) ivs

9090 ivs <- get_instances

9191 hs <- get_holes

src/Idris/ElabDecls.hs+7−2

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

239239 pblock i = map (expandParamsD False i id ns

240240 (concatMap tldeclared ps)) ps

241241

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

243+ = do open <- addOpenImpl ns

244+ mapM_ (elabDecl' what info) ds

245+ setOpenImpl open

246+

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

243248 do mapM_ (elabDecl' what ninfo) ps

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

251256 | what /= EDefns

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

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

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

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

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

259264 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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 139

43+ibcVersion = 140

4444

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

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

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

13711371 put x10

13721372 put x11

13731373 put x12

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

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

13751375 do putWord8 8

13761376 put x1

13771377 put x2

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

13871387 put x12

13881388 put x13

13891389 put x14

1390+ put x15

13901391 PDSL x1 x2 -> do putWord8 9

13911392 put x1

13921393 put x2

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

14281429 put x1

14291430 put x2

14301431 put x3

1432+ POpenInterfaces x1 x2 x3 -> do putWord8 18

1433+ put x1

1434+ put x2

1435+ put x3

14311436 get

14321437 = do i <- getWord8

14331438 case i of

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

15041509 x12 <- get

15051510 x13 <- get

15061511 x14 <- get

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

1512+ x15 <- get

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

15081514 9 -> do x1 <- get

15091515 x2 <- get

15101516 return (PDSL x1 x2)

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

15441550 x2 <- get

15451551 x3 <- get

15461552 return (PRunElabDecl x1 x2 x3)

1553+ 18 -> do x1 <- get

1554+ x2 <- get

1555+ x3 <- get

1556+ return (POpenInterfaces x1 x2 x3)

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

15481558

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

src/Idris/Parser.hs+31−3

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

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

214214 declBody b =

215215 try (instance_ True syn)

216+ <|> try (openInterface syn)

216217 <|> declBody' b

217218 <|> using_ syn

218219 <|> params syn

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

337338 (map (updateNs ns) ds)

338339 (updateRecCon ns cname)

339340 cdocs

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

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

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

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

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

343344 (map (updateNs ns) ds)

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

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

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

768769 <?> "parameters declaration"

769770

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+

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

771792

772793@

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

940961 args <- many (simpleExpr syn)

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

942963 let t = bindList (PPi constraint) cs sc

964+ pnames <- instanceUsing

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

945967 <?> "implementation declaration"

946968 where instanceName :: IdrisParser Name

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

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

954976 fc <- getFC

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

956978

979+ instanceUsing :: IdrisParser [Name]

980+ instanceUsing = do reservedHL "using"

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

982+ return (map fst ns)

983+ <|> return []

984+

957985-- | Parse a docstring

958986docstring :: SyntaxInfo

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

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

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

687687 fcOf :: PDecl -> FC

688688 fcOf (PClauses fc _ _ _) = fc

689689collect (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

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

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

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

693694 = 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− = PInstance doc argDocs f s cs acc opts n nfc ps pextra t en (collect ds) : collect ds'

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

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

696697collect (d : ds) = d : collect ds

697698collect [] = []

src/Idris/ProofSearch.hs+23−11

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

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

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

341341resolveTC :: Bool -- ^ using default Int

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

342+ -> Bool -- ^ allow open implementations

343343 -> Int -- ^ depth

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

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

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

347347 -> IState -> ElabD ()

348−resolveTC def mvok depth top fn elab ist

349− = do hs <- get_holes

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

348+resolveTC def openOK depth top fn elab ist

349+ = do hs <- get_holes

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

351351

352−resTC' tcs def 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

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

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

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 openOK topholes depth topg fn elab ist

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

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

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

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

360371 -- those holes and no others.

372+ g <- goal

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

362374 Nothing -> (False, [])

363375 Just hs -> (True, hs)

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

380392 try' (trivialTCs okholes elab ist)

381393 (do addDefault t tc ttypes

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

383− let insts = findInstances ist t

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

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

385− where

397+

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

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

388400 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

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

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

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

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

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

497509 hs <- get_holes

src/Idris/REPL.hs+2−2

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

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

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

905905 PClauses fc opts (getClauseName clause) css

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

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

908908 fixClauses decl = decl

909909

910910process fn (Undefine names) = undefine names

test/interfaces003/interfaces003.idr+8−7

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

11interface NumMod where

22 number : Bool -> Int

33

4−implementation [five] NumMod where

4+implementation [Five] NumMod where

55 number b = 5

66

77foo : NumMod => Int

88foo = number True + number False

99

10−increment : Int -> NumMod -> NumMod

11−increment inc x = addOne

10+Increment : Int -> NumMod -> NumMod

11+Increment inc x = AddOne

1212 where

1313 foo : NumMod

1414 foo = x

1515

16− implementation [addOne] NumMod where

16+ implementation [AddOne] NumMod where

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

1818

19−main : IO ()

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

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

19+using implementation Five

20+ main : IO ()

21+ main = do printLn foo

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