a41ca33 · 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+6

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

614614 test/interfaces002/*.idr

615615 test/interfaces002/run

616616 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

617623

618624 test/io001/run

619625 test/io001/*.idr

src/Idris/AbsSyntax.hs+42−6

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

1294− = PInstance doc argDocs info f

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

1324+ PInstance doc argDocs info f

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

1296− acc opts n

1326+ pnames acc opts n

12971327 nfc

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

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

12991330 (expandParams dec ps ns [] ty)

1300− cn

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

1331+ cn'

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

13021333expandParamsD rhs ist dec ps ns d = d

13031334

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

13051336

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+

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

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

13081344-- * 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 {

196196 idris_implicits :: Ctxt [PArg],

197197 idris_statics :: Ctxt [Bool],

198198 idris_classes :: Ctxt ClassInfo,

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

199200 idris_records :: Ctxt RecordInfo,

200201 idris_dsls :: Ctxt DSL,

201202 idris_optimisation :: Ctxt OptInfo,

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

359360-- | The initial state for the compiler

360361idrisInit :: IState

361362idrisInit = IState initContext S.empty []

362− emptyContext emptyContext emptyContext emptyContext

363+ emptyContext emptyContext emptyContext [] emptyContext

363364 emptyContext emptyContext emptyContext emptyContext

364365 emptyContext emptyContext emptyContext emptyContext

365366 emptyContext emptyContext emptyContext emptyContext

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

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

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

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

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

711713 | PNamespace String FC [PDecl' t]

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

713715 -- namespace in the file

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

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

739741 SyntaxInfo

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

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

741744 Accessibility

742745 FnOpts

743746 Name -- class

744747 FC -- precise location of class

745748 [t] -- parameters

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

746750 t -- full instance type

747751 (Maybe Name) -- explicit name

748752 [PDecl' t]

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

885889 PParams (f fc)

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

887891 (map (mapPDeclFC f g) decls)

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

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

888894mapPDeclFC f g (PNamespace ns fc decls) =

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

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

905911 (map (mapPDeclFC f g) body)

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

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

909915 PInstance doc paramDocs syn (f fc)

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

912919 (mapPTermFC f g instTy)

913920 instN

914921 (map (mapPDeclFC f g) body)

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

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

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

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

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

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

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

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

952963declared (PDSL n _) = [n]

953964declared (PSyntax _ _) = []

954965declared (PMutual _ ds) = concatMap declared ds

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

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

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

967978tldeclared (PParams _ _ ds) = []

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

968980tldeclared (PMutual _ ds) = concatMap tldeclared ds

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

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

972987tldeclared _ = []

973988

974989defined :: PDecl -> [Name]

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

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

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

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

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

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

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

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

9881007defined (PDSL n _) = [n]

9891008defined (PSyntax _ _) = []

9901009defined (PMutual _ ds) = concatMap defined ds

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

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

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

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

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

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

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

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

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

21772197showDeclImp _ _ = text "..."

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

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

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

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

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

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

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

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

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

709710 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

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/Clause.hs+2−1

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

629629

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

631631 let wb = map (mkStatic static_names) $

632+ map (expandInstanceScope ist decorate newargs defs) $

632633 map (expandParamsD False ist decorate newargs defs) whereblock

633634

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

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

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

637638 let (wbefore, wafter) = sepBlocks wb

638639

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

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

640641 mapM_ (rec_elabDecl info EAll winfo) wbefore

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

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

src/Idris/Elab/Instance.hs+73−30

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

6162 FC -> -- precise location of class name

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

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

6365 PTerm -> -- full instance type

6466 Maybe Name -> -- explicit name

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

6769 ist <- getIState

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

6971 [c] -> return c

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

7981

8082 let emptyclass = null (class_methods ci)

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

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

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

8588 case expn of

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

8891 addInstance intInst True n iname

8992 Just _ -> addInstance intInst False n iname

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

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

95+ oldOpen <- addOpenImpl parents

96+

9197 let ips = zip (class_params ci) ps

9298 let ns = case n of

9399 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

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

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

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

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

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

110127 let t_in = substMatchesShadow ips pnames t

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

128+ mnamemap =

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

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

112131 all_meths

113132 t' = substMatchesShadow mnamemap pnames t_in in

114133 (decorate ns iname n,

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

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

116135 (class_methods ci)

117136 logElab 3 (show (mtys, ips))

118137 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

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

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

125144 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

127148 let wb = wbTys ++ wbVals

149+

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

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

130152 show (concat (nub wparams))

131153

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

133− -- dictionary

134− let headVars = nub $ concatMap getHeadVars ps

135−

154+

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

137156

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

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

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

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

141160

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

144163

145164 push_estack iname True

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

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

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

148168

149169 let idecls = [PClauses fc totopts iname

150170 [PClause fc iname lhs [] rhs []]]

151171

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

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

153173 mapM_ (rec_elabDecl info EAll info) idecls

154174

155175 ctxt <- getContext

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

169189 mapM_ (rec_elabDecl info EAll info) wbVals'

170190

171191 pop_estack

192+

193+ setOpenImpl oldOpen

172194-- totalityCheckBlock

173195

174196 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

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

187209 Just nm -> nm

188210

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

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

213+ (map (substMatchesShadow ips pnames) ps)

214+ pextra

215+ (substMatchesShadow ips pnames t) expn ds

191216

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

193218 = case lookupCtxtName n (idris_classes i) of

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

195220 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

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

247272 keepDets dets t = t

248273

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

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

251− (ps ++ methArgs 0 ty))

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

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

276+

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

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

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

280+ where

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

282+

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

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

254285 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

275306 _ -> return ps'

276307 getWParams (_ : ps) = getWParams ps

277308

278− decorate ns iname (UN nm)

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

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

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

282313

283314 mkTyDecl (n, op, t, _)

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

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

289320 conbind [] x = x

290321

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

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

293− coninsert cs sc = conbind cs sc

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+

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

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

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

294329

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

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

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

346381getHeadVars _ = []

347382

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

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

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

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

352388 where

353389 doImpBind [] ty = ty

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

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

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

355392

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

357394 boundIn _ = []

358395

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

359403

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

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

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

364408 where

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

369413 (map (addParams ps) ds)

370414 addCParams c = c

371415

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

416+ addTmParams ps (PRef fc hls n)

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

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

375420 addTmParams ps tm = tm

376421

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

378−

379422 mergePs [] args = args

380423 mergePs (p : ps) args

381424 | isImplicit p,

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

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

4040import Codec.Archive.Zip

4141

4242ibcVersion :: Word16

43−ibcVersion = 138

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

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

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

13861386 put x11

13871387 put x12

13881388 put x13

1389+ put x14

1390+ put x15

13891391 PDSL x1 x2 -> do putWord8 9

13901392 put x1

13911393 put x2

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

14271429 put x1

14281430 put x2

14291431 put x3

1432+ POpenInterfaces x1 x2 x3 -> do putWord8 18

1433+ put x1

1434+ put x2

1435+ put x3

14301436 get

14311437 = do i <- getWord8

14321438 case i of

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

15021508 x11 <- get

15031509 x12 <- get

15041510 x13 <- get

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

1511+ x14 <- get

1512+ x15 <- get

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

15061514 9 -> do x1 <- get

15071515 x2 <- get

15081516 return (PDSL x1 x2)

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

15421550 x2 <- get

15431551 x3 <- get

15441552 return (PRunElabDecl x1 x2 x3)

1553+ 18 -> do x1 <- get

1554+ x2 <- get

1555+ x3 <- get

1556+ return (POpenInterfaces x1 x2 x3)

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

15461558

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

src/Idris/Parser.hs+32−4

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

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

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

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'

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

343344 (map (updateNs ns) ds)

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

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

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

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

781782 <?> "parameters declaration"

782783

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+

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

784805

785806@

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

946967 args <- many (simpleExpr syn)

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

948969 let t = bindList (PPi constraint) cs sc

970+ pnames <- instanceUsing

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

951973 <?> "implementation declaration"

952974 where instanceName :: IdrisParser Name

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

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

960982 fc <- getFC

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

962984

985+ instanceUsing :: IdrisParser [Name]

986+ instanceUsing = do reservedHL "using"

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

988+ return (map fst ns)

989+ <|> return []

990+

963991-- | Parse a docstring

964992docstring :: SyntaxInfo

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

695− = PInstance doc argDocs f s cs acc opts n nfc ps 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 = idris_openimpls ist ++ findInstances ist t

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

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

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

5141

test/interfaces002/interfaces002.idr+1−1

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

3434testSum = sumArray

3535

3636main : 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)))

3838

3939

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

3+

4+implementation [Five] NumMod where

5+ number b = 5

6+

7+foo : NumMod => Int

8+foo = number True + number False

9+

10+Increment : Int -> NumMod -> NumMod

11+Increment inc x = AddOne

12+ where

13+ foo : NumMod

14+ foo = x

15+

16+ implementation [AddOne] NumMod where

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

18+

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

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