160eb14 · Idris-dev · git.iko.soy

idris.cabal+1−1

compare with master

unifiedsplit

@@ -151,7 +151,7 @@ Library

151 , Idris.Elab.Clause

152 , Idris.Elab.Data

153 , Idris.Elab.Record

154− , Idris.Elab.Class

154+ , Idris.Elab.Interface

155 , Idris.Elab.Instance

156 , Idris.Elab.Provider

157 , Idris.Elab.RunElab

libs/base/System/Concurrency/Channels.idr → libs/base/System/Concurrency/Sessions.idrrenamed

The content is the same.

libs/contrib/Classes/Verified.idr → libs/contrib/Interfaces/Verified.idrrenamed+1−1

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

1−module Classes.Verified

1+module Interfaces.Verified

2

3import Control.Algebra

4import Control.Algebra.Lattice

libs/contrib/contrib.ipkg+1−1

@@ -9,7 +9,7 @@ modules = CFFI, CFFI.Types, CFFI.Memory,

9 Control.Isomorphism.Primitives,

10 Control.Partial,

11

12− Classes.Verified,

12+ Interfaces.Verified,

13

14 Data.Fun, Data.Rel,

15 Data.Hash,

libs/oldeffects/Effect/Default.idr+1−1

@@ -1,6 +1,6 @@

1module Default

2

3−class Default a where

3+interface Default a where

4 default : a

5

6instance Default Int where

libs/oldeffects/Effects.idr+1−1

@@ -26,7 +26,7 @@ data EFFECT : Type where

26

27||| Handler classes describe how an effect `e` is translated to the

28||| underlying computation context `m` for execution.

29−class Handler (e : Effect) (m : Type -> Type) where

29+interface Handler (e : Effect) (m : Type -> Type) where

30 ||| How to handle the effect.

31 |||

32 ||| @ r The resource being handled.

src/IRTS/Compiler.hs+1−1

@@ -628,7 +628,7 @@ irAlt top vs _ (ConCase n t args sc) = do

628 LConCase (-1) n usedArgs <$> irSC top (methodVars `M.union` vs) sc

629 where

630 methodVars = case n of

631− SN (InstanceCtorN className)

631+ SN (InstanceCtorN interfaceName)

632 -> M.fromList [(v, VI

633 { viMethod = Just $ mkFieldName n i

634 }) | (v,i) <- zip args [0..]]

src/Idris/ASTUtils.hs+3−3

@@ -40,7 +40,7 @@ f = do

40module Idris.ASTUtils(

41 Field(), cg_usedpos, ctxt_lookup, fgetState, fmodifyState

42 , fputState, idris_fixities, ist_callgraph, ist_optimisation

43− , known_classes, known_terms, opt_detaggable, opt_inaccessible

43+ , known_interfaces, known_terms, opt_detaggable, opt_inaccessible

44 , opts_idrisCmdline, repl_definitions

45 ) where

46

@@ -148,8 +148,8 @@ known_terms :: Field IState (Ctxt (Def, Injectivity, Accessibility, Totality, Me

148known_terms = Field (definitions . tt_ctxt)

149 (\v state -> state {tt_ctxt = (tt_ctxt state) {definitions = v}})

150

151−known_classes :: Field IState (Ctxt ClassInfo)

151+known_interfaces :: Field IState (Ctxt InterfaceInfo)

152−known_classes = Field idris_classes (\v state -> state {idris_classes = idris_classes state})

152+known_interfaces = Field idris_interfaces (\v state -> state {idris_interfaces = idris_interfaces state})

153

154

155-- | Names defined at the repl

src/Idris/AbsSyntax.hs+12−12

@@ -449,12 +449,12 @@ addInstance :: Bool -- ^ whether the name is an Integer instance

449 -> Idris ()

450addInstance int res n i

451 = do ist <- getIState

452− case lookupCtxt n (idris_classes ist) of

452+ case lookupCtxt n (idris_interfaces ist) of

453 [CI a b c d e ins fds] ->

454− do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_classes ist)

454+ do let cs = addDef n (CI a b c d e (addI i ins) fds) (idris_interfaces ist)

455− putIState $ ist { idris_classes = cs }

455+ putIState $ ist { idris_interfaces = cs }

456− _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_classes ist)

456+ _ -> do let cs = addDef n (CI (sMN 0 "none") [] [] [] [] [(i, res)] []) (idris_interfaces ist)

457− putIState $ ist { idris_classes = cs }

457+ putIState $ ist { idris_interfaces = cs }

458 where addI, insI :: Name -> [(Name, Bool)] -> [(Name, Bool)]

459 addI i ins | int = (i, res) : ins

460 | chaser n = ins ++ [(i, res)]

@@ -493,13 +493,13 @@ getOpenImpl :: Idris [Name]

493getOpenImpl = do ist <- getIState

494 return (idris_openimpls ist)

495

496−addClass :: Name -> ClassInfo -> Idris ()

496+addInterface :: Name -> InterfaceInfo -> Idris ()

497−addClass n i

497+addInterface n i

498 = do ist <- getIState

499− let i' = case lookupCtxt n (idris_classes ist) of

499+ let i' = case lookupCtxt n (idris_interfaces ist) of

500− [c] -> c { class_instances = class_instances i }

500+ [c] -> c { interface_instances = interface_instances i }

501 _ -> i

502− putIState $ ist { idris_classes = addDef n i' (idris_classes ist) }

502+ putIState $ ist { idris_interfaces = addDef n i' (idris_interfaces ist) }

503

504addRecord :: Name -> RecordInfo -> Idris ()

505addRecord n ri = do ist <- getIState

@@ -1353,8 +1353,8 @@ expandParamsD rhs ist dec ps ns (PParams f params pds)

1353-- (map (expandParamsD ist dec ps ns) pds)

1354expandParamsD rhs ist dec ps ns (PMutual f pds)

1355 = PMutual f (map (expandParamsD rhs ist dec ps ns) pds)

1356−expandParamsD rhs ist dec ps ns (PClass doc info f cs n nfc params pDocs fds decls cn cd)

1356+expandParamsD rhs ist dec ps ns (PInterface doc info f cs n nfc params pDocs fds decls cn cd)

1357− = PClass doc info f

1357+ = PInterface doc info f

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

1359 n nfc

1360 (map (\(n, fc, t) -> (n, fc, expandParams dec ps ns [] t)) params)

src/Idris/AbsSyntaxTree.hs+19−19

@@ -216,7 +216,7 @@ data IState = IState {

216 , idris_infixes :: [FixDecl] -- ^ Currently defined infix operators

217 , idris_implicits :: Ctxt [PArg]

218 , idris_statics :: Ctxt [Bool]

219− , idris_classes :: Ctxt ClassInfo

219+ , idris_interfaces :: Ctxt InterfaceInfo

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

221 , idris_records :: Ctxt RecordInfo

222 , idris_dsls :: Ctxt DSL

@@ -347,7 +347,7 @@ primDefs = [ sUN "unsafePerformPrimIO"

347data IBCWrite = IBCFix FixDecl

348 | IBCImp Name

349 | IBCStatic Name

350− | IBCClass Name

350+ | IBCInterface Name

351 | IBCRecord Name

352 | IBCInstance Bool Bool Name Name

353 | IBCDSL Name

@@ -720,7 +720,7 @@ data PDecl' t

720 -- | Type class: arguments are documentation, syntax info, source

721 -- location, constraints, class name, class name location,

722 -- parameters, method declarations, optional constructor name

723− | PClass (Docstring (Either Err t)) SyntaxInfo FC

723+ | PInterface (Docstring (Either Err t)) SyntaxInfo FC

724 [(Name, t)] -- constraints

725 Name -- class name

726 FC -- accurate location of class name

@@ -913,8 +913,8 @@ mapPDeclFC f g (PRecord doc syn fc opts n nfc params paramdocs fields ctor ctorD

913 (fmap (\(ctorN, ctorNFC) -> (ctorN, g ctorNFC)) ctor)

914 ctorDoc

915 syn'

916−mapPDeclFC f g (PClass doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =

916+mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ctor ctorDoc) =

917− PClass doc syn (f fc)

917+ PInterface doc syn (f fc)

918 (map (\(constrn, constr) -> (constrn, mapPTermFC f g constr)) constrs)

919 n (g nfc) (map (\(n, nfc, pty) -> (n, g nfc, mapPTermFC f g pty)) params)

920 paramDocs (map (\(dn, dnfc) -> (dn, g dnfc)) det)

@@ -965,7 +965,7 @@ declared (PParams _ _ ds) = concatMap declared ds

965declared (POpenInterfaces _ _ ds) = concatMap declared ds

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

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

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

968+declared (PInterface _ _ _ _ n _ _ _ _ ms cn cd) = n : (map fst (maybeToList cn) ++ concatMap declared ms)

969declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

970 = case mn of

971 Nothing -> []

@@ -989,7 +989,7 @@ tldeclared (PParams _ _ ds) = []

989tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds

990tldeclared (PMutual _ ds) = concatMap tldeclared ds

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

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

992+tldeclared (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap tldeclared ms)

993tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

994 = case mn of

995 Nothing -> []

@@ -1009,7 +1009,7 @@ defined (PParams _ _ ds) = concatMap defined ds

1009defined (POpenInterfaces _ _ ds) = concatMap defined ds

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

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

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

1012+defined (PInterface _ _ _ _ n _ _ _ _ ms cn _) = n : (map fst (maybeToList cn) ++ concatMap defined ms)

1013defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

1014 = case mn of

1015 Nothing -> []

@@ -1413,18 +1413,18 @@ highestFC (PAppImpl t _) = highestFC t

1413

1414-- Type class data

1415

1416−data ClassInfo = CI {

1416+data InterfaceInfo = CI {

1417− instanceCtorName :: Name

1417+ instanceCtorName :: Name

1418− , class_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method

1418+ , interface_methods :: [(Name, (Bool, FnOpts, PTerm))] -- ^ flag whether it's a "data" method

1419− , class_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl

1419+ , interface_defaults :: [(Name, (Name, PDecl))] -- ^ method name -> default impl

1420− , class_default_superclasses :: [PDecl]

1420+ , interface_default_super_interfaces :: [PDecl]

1421− , class_params :: [Name]

1421+ , interface_params :: [Name]

1422− , class_instances :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded

1422+ , interface_instances :: [(Name, Bool)] -- ^ the Bool is whether to include in instance search, so named instances are excluded

1423− , class_determiners :: [Int]

1423+ , interface_determiners :: [Int]

1424 } deriving (Show, Generic)

1425{-!

1426−deriving instance Binary ClassInfo

1426+deriving instance Binary InterfaceInfo

1427−deriving instance NFData ClassInfo

1427+deriving instance NFData InterfaceInfo

1428!-}

1429

1430-- Record data

@@ -2242,7 +2242,7 @@ showDeclImp o (PParams _ ns ps) = text "params" <+> braces (text (show ns) <

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

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

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

2245−showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)

2245+showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)

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

2247showDeclImp o (PInstance _ _ _ _ cs _ acc _ n _ _ _ t _ ds)

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

src/Idris/CaseSplit.hs+4−4

@@ -401,8 +401,8 @@ getClause :: Int -- ^ line number that the type is declared on

401 -> Idris String

402getClause l fn un fp

403 = do i <- getIState

404− case lookupCtxt un (idris_classes i) of

404+ case lookupCtxt un (idris_interfaces i) of

405− [c] -> return (mkClassBodies i (class_methods c))

405+ [c] -> return (mkInterfaceBodies i (interface_methods c))

406 _ -> do ty_in <- getInternalApp fp l

407 let ty = case ty_in of

408 PTyped n t -> t

@@ -436,8 +436,8 @@ getClause l fn un fp

436 sUN "z"]) used

437

438 -- write method declarations, indent with 4 spaces

439− mkClassBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String

439+ mkInterfaceBodies :: IState -> [(Name, (Bool, FnOpts, PTerm))] -> String

440− mkClassBodies i ns

440+ mkInterfaceBodies i ns

441 = showSep "\n"

442 (zipWith (\(n, (_, _, ty)) m -> " " ++

443 def (show (nsroot n)) ++ " "

src/Idris/DeepSeq.hs+1−1

@@ -91,7 +91,7 @@ instance NFData PAltType

91instance (NFData t) => NFData (PTactic' t)

92instance (NFData t) => NFData (PDo' t)

93instance (NFData t) => NFData (PArg' t)

94−instance NFData ClassInfo

94+instance NFData InterfaceInfo

95instance NFData RecordInfo

96instance NFData OptInfo

97instance NFData TypeInfo

src/Idris/Docs.hs+34−34

@@ -45,7 +45,7 @@ type FunDoc = FunDoc' (Docstring DocTerm)

45data Docs' d = FunDoc (FunDoc' d)

46 | DataDoc (FunDoc' d) -- type constructor docs

47 [FunDoc' d] -- data constructor docs

48− | ClassDoc Name d -- class docs

48+ | InterfaceDoc Name d -- class docs

49 [FunDoc' d] -- method docs

50 [(Name, Maybe d)] -- parameters and their docstrings

51 [(Maybe Name, PTerm, (d, [(Name, d)]))] -- instances: name for named instances, the constraint term, the docs

@@ -139,7 +139,7 @@ pprintDocs ist (DataDoc t args)

139 if null args then text "No constructors."

140 else nest 4 (text "Constructors:" <> line <>

141 vsep (map (pprintFDWithoutTotality ist False) args))

142−pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ctor)

142+pprintDocs ist (InterfaceDoc n doc meths params instances sub_interfaces super_interfaces ctor)

143 = nest 4 (text "Interface" <+> prettyName True (ppopt_impl ppo) [] n <>

144 if nullDocstring doc

145 then empty

@@ -164,13 +164,13 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct

164 else line <$> nest 4 (text "Named implementations:" <$>

165 vsep (map pprintInstance namedInstances)))

166 <>

167− (if null subclasses then empty

167+ (if null sub_interfaces then empty

168 else line <$> nest 4 (text "Child interfaces:" <$>

169− vsep (map (dumpInstance . prettifySubclasses) subclasses)))

169+ vsep (map (dumpInstance . prettifySubInterfaces) sub_interfaces)))

170 <>

171− (if null superclasses then empty

171+ (if null super_interfaces then empty

172 else line <$> nest 4 (text "Default parent implementations:" <$>

173− vsep (map dumpInstance superclasses)))

173+ vsep (map dumpInstance super_interfaces)))

174 where

175 params' = zip pNames (repeat False)

176

@@ -213,10 +213,10 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct

213 dumpInstance :: PTerm -> Doc OutputAnnotation

214 dumpInstance = pprintPTerm ppo params' [] infixes

215

216− prettifySubclasses (PPi (Constraint _ _) _ _ tm _) = prettifySubclasses tm

216+ prettifySubInterfaces (PPi (Constraint _ _) _ _ tm _) = prettifySubInterfaces tm

217− prettifySubclasses (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubclasses t1) (prettifySubclasses t2)

217+ prettifySubInterfaces (PPi plcity nm fc t1 t2) = PPi plcity (safeHead nm pNames) NoFC (prettifySubInterfaces t1) (prettifySubInterfaces t2)

218− prettifySubclasses (PApp fc ref args) = PApp fc ref $ updateArgs pNames args

218+ prettifySubInterfaces (PApp fc ref args) = PApp fc ref $ updateArgs pNames args

219− prettifySubclasses tm = tm

219+ prettifySubInterfaces tm = tm

220

221 safeHead _ (y:_) = y

222 safeHead x [] = x

@@ -228,9 +228,9 @@ pprintDocs ist (ClassDoc n doc meths params instances subclasses superclasses ct

228 updateRef nm (PRef fc _ _) = PRef fc [] nm

229 updateRef _ pt = pt

230

231− isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'

231+ isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args')) = nm == n && map getTm args == map getTm args'

232− isSubclass (PPi _ _ _ _ pt) = isSubclass pt

232+ isSubInterface (PPi _ _ _ _ pt) = isSubInterface pt

233− isSubclass _ = False

233+ isSubInterface _ = False

234

235 prettyParameters =

236 if any (isJust . snd) params

@@ -287,24 +287,24 @@ getDocs n@(NS n' ns) w | n' == modDocName

287 " do not exist! This shouldn't have happened and is a bug."

288getDocs n w

289 = do i <- getIState

290− docs <- if | Just ci <- lookupCtxtExact n (idris_classes i)

290+ docs <- if | Just ci <- lookupCtxtExact n (idris_interfaces i)

291− -> docClass n ci

291+ -> docInterface n ci

292 | Just ri <- lookupCtxtExact n (idris_records i)

293 -> docRecord n ri

294 | Just ti <- lookupCtxtExact n (idris_datatypes i)

295 -> docData n ti

296− | Just class_ <- classNameForInst i n

296+ | Just interface_ <- interfaceNameForInst i n

297 -> do fd <- docFun n

298− return $ NamedInstanceDoc class_ fd

298+ return $ NamedInstanceDoc interface_ fd

299 | otherwise

300 -> do fd <- docFun n

301 return (FunDoc fd)

302 return $ fmap (howMuch w) docs

303− where classNameForInst :: IState -> Name -> Maybe Name

303+ where interfaceNameForInst :: IState -> Name -> Maybe Name

304− classNameForInst ist n =

304+ interfaceNameForInst ist n =

305 listToMaybe [ cn

306− | (cn, ci) <- toAlist (idris_classes ist)

306+ | (cn, ci) <- toAlist (idris_interfaces ist)

307− , n `elem` map fst (class_instances ci)

307+ , n `elem` map fst (interface_instances ci)

308 ]

309

310docData :: Name -> TypeInfo -> Idris Docs

@@ -313,30 +313,30 @@ docData n ti

313 cdocs <- mapM docFun (con_names ti)

314 return (DataDoc tdoc cdocs)

315

316−docClass :: Name -> ClassInfo -> Idris Docs

316+docInterface :: Name -> InterfaceInfo -> Idris Docs

317−docClass n ci

317+docInterface n ci

318 = do i <- getIState

319 let docStrings = listToMaybe $ lookupCtxt n $ idris_docstrings i

320 docstr = maybe emptyDocstring fst docStrings

321 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd)))

322− (class_params ci)

322+ (interface_params ci)

323 docsForInstance inst = fromMaybe (emptyDocstring, []) .

324 flip lookupCtxtExact (idris_docstrings i) $

325 inst

326 instances = map (\inst -> (namedInst inst,

327 delabTy i inst,

328 docsForInstance inst))

329− (nub (map fst (class_instances ci)))

329+ (nub (map fst (interface_instances ci)))

330− (subclasses, instances') = partition (isSubclass . (\(_,tm,_) -> tm)) instances

330+ (sub_interfaces, instances') = partition (isSubInterface . (\(_,tm,_) -> tm)) instances

331− superclasses = catMaybes $ map getDInst (class_default_superclasses ci)

331+ super_interfaces = catMaybes $ map getDInst (interface_default_super_interfaces ci)

332− mdocs <- mapM (docFun . fst) (class_methods ci)

332+ mdocs <- mapM (docFun . fst) (interface_methods ci)

333 let ctorN = instanceCtorName ci

334 ctorDocs <- case basename ctorN of

335 SN _ -> return Nothing

336 _ -> fmap Just $ docFun ctorN

337− return $ ClassDoc

337+ return $ InterfaceDoc

338 n docstr mdocs params

339− instances' (map (\(_,tm,_) -> tm) subclasses) superclasses

339+ instances' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces

340 ctorDocs

341 where

342 namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)

@@ -346,11 +346,11 @@ docClass n ci

346 getDInst (PInstance _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t

347 getDInst _ = Nothing

348

349− isSubclass (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))

349+ isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))

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

351− isSubclass (PPi _ _ _ _ pt)

351+ isSubInterface (PPi _ _ _ _ pt)

352− = isSubclass pt

352+ = isSubInterface pt

353− isSubclass _

353+ isSubInterface _

354 = False

355

356docRecord :: Name -> RecordInfo -> Idris Docs

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

@@ -1117,7 +1117,7 @@ elabClause info opts (_, PWith fc fname lhs_in withs wval_in pn_in withblock)

1117 addResolvesArgs fc (Bind n (Pi _ ty _) sc) (a : args)

1118 | (P _ cn _, _) <- unApply ty,

1119 getTm a == Placeholder

1120− = case lookupCtxtExact cn (idris_classes ist) of

1120+ = case lookupCtxtExact cn (idris_interfaces ist) of

1121 Just _ -> a { getTm = PResolveTC fc } : addResolvesArgs fc sc args

1122 Nothing -> a : addResolvesArgs fc sc args

1123 addResolvesArgs fc (Bind n (Pi _ ty _) sc) (a : args)

src/Idris/Elab/Instance.hs+21−21

@@ -77,7 +77,7 @@ elabInstance :: ElabInfo

77 -> Idris ()

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

79 ist <- getIState

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

80+ (n, ci) <- case lookupCtxtName n (idris_interfaces ist) of

81 [c] -> return c

82 [] -> ifail $ show fc ++ ":" ++ show n ++ " is not an interface"

83 cs -> tclift $ tfail $ At fc

@@ -89,22 +89,22 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

89

90 let totopts = Dictionary : Inlinable : opts

91

92− let emptyclass = null (class_methods ci)

92+ let emptyinterface = null (interface_methods ci)

93 when (what /= EDefns) $ do

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

95 (piBindp expl_param pextra t)

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

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

98 case expn of

99− Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping ist (class_determiners ci) (delab ist nty))

99+ Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty))

100− (map fst $ class_instances ci)

100+ (map fst $ interface_instances ci)

101 addInstance intInst True n iname

102 Just _ -> addInstance intInst False n iname

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

103+ when (what /= ETypes && (not (null ds && not emptyinterface))) $ do

104 -- Add the parent implementation names to the privileged set

105 oldOpen <- addOpenImpl parents

106

107− let ips = zip (class_params ci) ps

107+ let ips = zip (interface_params ci) ps

108 let ns = case n of

109 NS n ns' -> ns'

110 _ -> []

@@ -118,9 +118,9 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

118 let pnames = nub $ map pname (concat (nub wparams)) ++

119 concatMap (namesIn [] ist) ps

120

121− let superclassInstances = map (substInstance ips pnames) (class_default_superclasses ci)

121+ let superInterfaceInstances = map (substInstance ips pnames) (interface_default_super_interfaces ci)

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

122+ undefinedSuperInterfaceInstances <- filterM (fmap not . isOverlapping ist) superInterfaceInstances

123− mapM_ (rec_elabDecl info EAll info) undefinedSuperclassInstances

123+ mapM_ (rec_elabDecl info EAll info) undefinedSuperInterfaceInstances

124

125 ist <- getIState

126 -- Bring variables in instance head into scope when building the

@@ -132,7 +132,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

132 _ -> (zip headVars (repeat Placeholder), Erased)

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

134

135− let all_meths = map (nsroot . fst) (class_methods ci)

135+ let all_meths = map (nsroot . fst) (interface_methods ci)

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

137 let t_in = substMatchesShadow ips pnames t

138 mnamemap =

@@ -142,16 +142,16 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

142 t' = substMatchesShadow mnamemap pnames t_in in

143 (decorate ns iname n,

144 op, coninsert cs pextra t', t'))

145− (class_methods ci)

145+ (interface_methods ci)

146 logElab 3 (show (mtys, ips))

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

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

148− let ds_defs = insertDefaults ist iname (class_defaults ci) ns ds

148+ let ds_defs = insertDefaults ist iname (interface_defaults ci) ns ds

149 logElab 3 ("After defaults: " ++ show ds_defs ++ "\n")

150− let ds' = reorderDefs (map fst (class_methods ci)) ds_defs

150+ let ds' = reorderDefs (map fst (interface_methods ci)) ds_defs

151 logElab 1 ("Reordered: " ++ show ds' ++ "\n")

152

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

153+ mapM_ (warnMissing ds' ns iname) (map fst (interface_methods ci))

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

154+ mapM_ (checkInInterface (map fst (interface_methods ci))) (concatMap defined ds')

155 let wbTys = map mkTyDecl mtys

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

157 ist <- getIState

@@ -199,14 +199,14 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

199

200 mapM_ (rec_elabDecl info EAll info) wbVals'

201

202− mapM_ (checkInjectiveDef fc (class_methods ci)) (zip ds' wbVals')

202+ mapM_ (checkInjectiveDef fc (interface_methods ci)) (zip ds' wbVals')

203

204 pop_estack

205

206 setOpenImpl oldOpen

207-- totalityCheckBlock

208

209− checkInjectiveArgs fc n (class_determiners ci) (lookupTyExact iname (tt_ctxt ist))

209+ checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))

210 addIBC (IBCInstance intInst (isNothing expn) n iname)

211

212 where

@@ -228,7 +228,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

228 (substMatchesShadow ips pnames t) expn ds

229

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

231− = case lookupCtxtName n (idris_classes i) of

231+ = case lookupCtxtName n (idris_interfaces i) of

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

233 case lookupTy iname (tt_ctxt i) of

234 [] -> elabFindOverlapping i ci iname syn t

@@ -255,7 +255,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

255 ctxt <- getContext

256 (cty, _) <- recheckC (constraintNS info) fc id [] tyT

257 let nty = normalise ctxt [] cty

258− return $ any (isJust . findOverlapping i (class_determiners ci) (delab i nty)) (map fst $ class_instances ci)

258+ return $ any (isJust . findOverlapping i (interface_determiners ci) (delab i nty)) (map fst $ interface_instances ci)

259

260 findOverlapping i dets t n

261 | SN (ParentN _ _) <- n = Nothing

@@ -375,7 +375,7 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

375 = iWarn fc . text $ "method " ++ show meth ++ " not defined"

376 | otherwise = return ()

377

378− checkInClass ns meth

378+ checkInInterface ns meth

379 | any (eqRoot meth) ns = return ()

380 | otherwise = tclift $ tfail (At fc (Msg $

381 show meth ++ " not a method of class " ++ show n))

src/Idris/Elab/Class.hs → src/Idris/Elab/Interface.hsrenamed+10−10

@@ -7,7 +7,7 @@ Maintainer : The Idris Community.

7-}

8{-# LANGUAGE PatternGuards #-}

9{-# OPTIONS_GHC -fwarn-missing-signatures #-}

10−module Idris.Elab.Class(elabClass) where

10+module Idris.Elab.Interface(elabInterface) where

11

12import Idris.AbsSyntax

13import Idris.ASTUtils

@@ -61,7 +61,7 @@ import Util.Pretty(pretty, text)

61

62data MArgTy = IA Name | EA Name | CA deriving Show

63

64−elabClass :: ElabInfo

64+elabInterface :: ElabInfo

65 -> SyntaxInfo

66 -> Docstring (Either Err PTerm)

67 -> FC

@@ -75,7 +75,7 @@ elabClass :: ElabInfo

75 -> Maybe (Name, FC) -- ^ instance ctor name and location

76 -> Docstring (Either Err PTerm) -- ^ instance ctor docs

77 -> Idris ()

78−elabClass info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

78+elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

79 = do let cn = fromMaybe (SN (InstanceCtorN tn)) (fst <$> mcn)

80 let tty = pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)

81 let constraint = PApp fc (PRef fc [] tn)

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

89 -- build data declaration

90 let mdecls = filter tydecl ds -- method declarations

91 let idecls = filter instdecl ds -- default superclass instance declarations

92− mapM_ checkDefaultSuperclassInstance idecls

92+ mapM_ checkDefaultSuperInterfaceInstance idecls

93 let mnames = map getMName mdecls

94 ist <- getIState

95 let constraintNames = nub $

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

119 elabData info (syn { no_imp = no_imp syn ++ mnames,

120 imp_methods = mnames }) doc pDocs fc [] ddecl

121 dets <- findDets cn (map fst fds)

122− addClass tn (CI cn (map nodoc imethods) defaults idecls (map (\(n, _, _) -> n) ps) [] dets)

122+ addInterface tn (CI cn (map nodoc imethods) defaults idecls (map (\(n, _, _) -> n) ps) [] dets)

123

124 -- for each constraint, build a top level function to chase it

125 cfns <- mapM (cfun cn constraint syn (map fst imethods)) constraints

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

139

140 -- add the default definitions

141 mapM_ (rec_elabDecl info EAll info) (concatMap (snd.snd) defs)

142− addIBC (IBCClass tn)

142+ addIBC (IBCInterface tn)

143

144 sendHighlighting $

145 [(tnfc, AnnName tn Nothing Nothing Nothing)] ++

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

161 chkUniq _ t = t

162

163 -- TODO: probably should normalise

164− checkDefaultSuperclassInstance :: PDecl -> Idris ()

164+ checkDefaultSuperInterfaceInstance :: PDecl -> Idris ()

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

165+ checkDefaultSuperInterfaceInstance (PInstance _ _ _ fc cs _ _ _ n _ ps _ _ _ _)

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

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

168 i <- getIState

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

249 let conn = case con of

250 PRef _ _ n -> n

251 PApp _ (PRef _ _ n) _ -> n

252− let conn' = case lookupCtxtName conn (idris_classes i) of

252+ let conn' = case lookupCtxtName conn (idris_interfaces i) of

253 [(n, _)] -> n

254 _ -> conn

255 addInstance False True conn' cfn

@@ -341,7 +341,7 @@ memberDocs (PTy d _ _ _ _ n _ _) = Just (basename n, d)

341memberDocs (PPostulate _ d _ _ _ _ n _) = Just (basename n, d)

342memberDocs (PData d _ _ _ _ pdata) = Just (basename $ d_name pdata, d)

343memberDocs (PRecord d _ _ _ n _ _ _ _ _ _ _ ) = Just (basename n, d)

344−memberDocs (PClass d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)

344+memberDocs (PInterface d _ _ _ n _ _ _ _ _ _ _) = Just (basename n, d)

345memberDocs _ = Nothing

346

347

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

@@ -868,7 +868,7 @@ elab ist info emode opts fn tm

868 let isinf = f == inferCon || tcname f

869 -- if f is a type class, we need to know its arguments so that

870 -- we can unify with them

871− case lookupCtxt f (idris_classes ist) of

871+ case lookupCtxt f (idris_interfaces ist) of

872 [] -> return ()

873 _ -> do mapM_ setInjective (map getTm args)

874 -- maybe more things are solvable now

@@ -961,10 +961,10 @@ elab ist info emode opts fn tm

961 Just b ->

962 case unApply (normalise (tt_ctxt ist) env (binderTy b)) of

963 (P _ c _, args) ->

964− case lookupCtxtExact c (idris_classes ist) of

964+ case lookupCtxtExact c (idris_interfaces ist) of

965 Nothing -> return ()

966 Just ci -> -- type class, set as injective

967− do mapM_ setinjArg (getDets 0 (class_determiners ci) args)

967+ do mapM_ setinjArg (getDets 0 (interface_determiners ci) args)

968 -- maybe we can solve more things now...

969 ulog <- getUnifyLog

970 probs <- get_probs

@@ -1137,7 +1137,7 @@ elab ist info emode opts fn tm

1137 _ -> return (n, False)

1138

1139 tcName tm | (P _ n _, _) <- unApply tm

1140− = case lookupCtxt n (idris_classes ist) of

1140+ = case lookupCtxt n (idris_interfaces ist) of

1141 [_] -> True

1142 _ -> False

1143 tcName _ = False

@@ -1745,18 +1745,18 @@ pruneByType _ t _ _ as = as

1745-- to it later - just returns 'var' for now. EB)

1746isPlausible :: IState -> Bool -> Env -> Name -> Type -> Bool

1747isPlausible ist var env n ty

1748− = let (hvar, classes) = collectConstraints [] [] ty in

1748+ = let (hvar, interfaces) = collectConstraints [] [] ty in

1749 case hvar of

1750 Nothing -> True

1751− Just rth -> var -- trace (show (rth, classes)) var

1751+ Just rth -> var -- trace (show (rth, interfaces)) var

1752 where

1753 collectConstraints :: [Name] -> [(Term, [Name])] -> Type ->

1754 (Maybe Name, [(Term, [Name])])

1755 collectConstraints env tcs (Bind n (Pi _ ty _) sc)

1756 = let tcs' = case unApply ty of

1757 (P _ c _, _) ->

1758− case lookupCtxtExact c (idris_classes ist) of

1758+ case lookupCtxtExact c (idris_interfaces ist) of

1759− Just tc -> ((ty, map fst (class_instances tc))

1759+ Just tc -> ((ty, map fst (interface_instances tc))

1760 : tcs)

1761 Nothing -> tcs

1762 _ -> tcs

@@ -2321,15 +2321,15 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

2321 returnUnit

2322 | n == tacN "Prim__AddInstance"

2323 = do ~[cls, inst] <- tacTmArgs 2 tac args

2324− className <- reifyTTName cls

2324+ interfaceName <- reifyTTName cls

2325 instName <- reifyTTName inst

2326− updateAux $ \e -> e { new_tyDecls = RAddInstance className instName :

2326+ updateAux $ \e -> e { new_tyDecls = RAddInstance interfaceName instName :

2327 new_tyDecls e }

2328 returnUnit

2329 | n == tacN "Prim__IsTCName"

2330 = do ~[n] <- tacTmArgs 1 tac args

2331 n' <- reifyTTName n

2332− case lookupCtxtExact n' (idris_classes ist) of

2332+ case lookupCtxtExact n' (idris_interfaces ist) of

2333 Just _ -> fmap fst . checkClosed $ Var (sNS (sUN "True") ["Bool", "Prelude"])

2334 Nothing -> fmap fst . checkClosed $ Var (sNS (sUN "False") ["Bool", "Prelude"])

2335 | n == tacN "Prim__ResolveTC"

@@ -2819,12 +2819,12 @@ processTacticDecls info steps =

2819 _ -> return ()

2820 -- TODO: inaccessible

2821

2822− RAddInstance className instName ->

2822+ RAddInstance interfaceName instName ->

2823 do -- The type class resolution machinery relies on a special

2824 logElab 2 $ "Adding elab script instance " ++ show instName ++

2825− " for " ++ show className

2825+ " for " ++ show interfaceName

2826− addInstance False True className instName

2826+ addInstance False True interfaceName instName

2827− addIBC (IBCInstance False True className instName)

2827+ addIBC (IBCInstance False True interfaceName instName)

2828 RClausesInstrs n cs ->

2829 do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n

2830 solveDeferred emptyFC n

src/Idris/Elab/Utils.hs+2−2

@@ -191,7 +191,7 @@ pbinds i (Bind n (PVar t) sc)

191 = do attack; patbind n

192 env <- get_env

193 case unApply (normalise (tt_ctxt i) env t) of

194− (P _ c _, args) -> case lookupCtxt c (idris_classes i) of

194+ (P _ c _, args) -> case lookupCtxt c (idris_interfaces i) of

195 [] -> return ()

196 _ -> -- type class, set as injective

197 mapM_ setinjArg args

@@ -270,7 +270,7 @@ getTCinj i ap@(App _ f a)

270 isTCName n = mapMaybe getInjName args

271 | otherwise = []

272 where

273− isTCName n = case lookupCtxtExact n (idris_classes i) of

273+ isTCName n = case lookupCtxtExact n (idris_interfaces i) of

274 Just _ -> True

275 _ -> False

276 getInjName t | (P _ x _, _) <- unApply t = Just x

src/Idris/ElabDecls.hs+3−3

@@ -34,7 +34,7 @@ import Idris.Elab.Type

34import Idris.Elab.Clause

35import Idris.Elab.Data

36import Idris.Elab.Record

37−import Idris.Elab.Class

37+import Idris.Elab.Interface

38import Idris.Elab.Instance

39import Idris.Elab.Provider

40import Idris.Elab.RunElab

@@ -271,10 +271,10 @@ elabDecl' what info (PNamespace n nfc ps) =

271 newNS = n : namespace info

272 ninfo = info { namespace = newNS }

273

274−elabDecl' what info (PClass doc s f cs n nfc ps pdocs fds ds cn cd)

274+elabDecl' what info (PInterface doc s f cs n nfc ps pdocs fds ds cn cd)

275 | what /= EDefns

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

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

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

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

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

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

src/Idris/Erasure.hs+5−5

@@ -79,7 +79,7 @@ performUsageAnalysis startNames = do

79 case startNames of

80 [] -> return [] -- no main -> not compiling -> reachability irrelevant

81 main -> do

82− ci <- idris_classes <$> getIState

82+ ci <- idris_interfaces <$> getIState

83 cg <- idris_callgraph <$> getIState

84 opt <- idris_optimisation <$> getIState

85 used <- idris_erasureUsed <$> getIState

@@ -170,7 +170,7 @@ forwardChain deps

170

171-- | Build the dependency graph, starting the depth-first search from

172-- a list of Names.

173−buildDepMap :: Ctxt ClassInfo -> [(Name, Int)] -> [(Name, Int)] ->

173+buildDepMap :: Ctxt InterfaceInfo -> [(Name, Int)] -> [(Name, Int)] ->

174 Context -> [Name] -> Deps

175buildDepMap ci used externs ctx startNames

176 = addPostulates used $ dfs S.empty M.empty startNames

@@ -252,7 +252,7 @@ buildDepMap ci used externs ctx startNames

252

253 -- get Deps for a Name

254 getDeps :: Name -> Deps

255− getDeps (SN (WhereN i (SN (InstanceCtorN classN)) (MN i' field)))

255+ getDeps (SN (WhereN i (SN (InstanceCtorN interfaceN)) (MN i' field)))

256 = M.empty -- these deps are created when applying instance ctors

257 getDeps n = case lookupDefExact n ctx of

258 Just def -> getDepsDef n def

@@ -338,7 +338,7 @@ buildDepMap ci used externs ctx startNames

338

339 -- generate metamethod names, "n" is the instance ctor

340 meth :: Int -> Maybe Name

341− meth | SN (InstanceCtorN className) <- n = \j -> Just (mkFieldName n j)

341+ meth | SN (InstanceCtorN interfaceName) <- n = \j -> Just (mkFieldName n j)

342 | otherwise = \j -> Nothing

343

344 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps

@@ -381,7 +381,7 @@ buildDepMap ci used externs ctx startNames

381 getDepsTerm vs bs cd app@(App _ _ _)

382 | (fun, args) <- unApply app = case fun of

383 -- instance constructors -> create metamethod deps

384− P (DCon _ _ _) ctorName@(SN (InstanceCtorN className)) _

384+ P (DCon _ _ _) ctorName@(SN (InstanceCtorN interfaceName)) _

385 -> conditionalDeps ctorName args -- regular data ctor stuff

386 `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff

387

src/Idris/IBC.hs+12−12

@@ -67,7 +67,7 @@ data IBCFile = IBCFile {

67 , ibc_implicits :: ![(Name, [PArg])]

68 , ibc_fixes :: ![FixDecl]

69 , ibc_statics :: ![(Name, [Bool])]

70− , ibc_classes :: ![(Name, ClassInfo)]

70+ , ibc_classes :: ![(Name, InterfaceInfo)]

71 , ibc_records :: ![(Name, RecordInfo)]

72 , ibc_instances :: ![(Bool, Bool, Name, Name)]

73 , ibc_dsls :: ![(Name, DSL)]

@@ -268,8 +268,8 @@ ibc i (IBCStatic n) f

268 = case lookupCtxtExact n (idris_statics i) of

269 Just v -> return f { ibc_statics = (n,v): ibc_statics f }

270 _ -> ifail "IBC write failed"

271−ibc i (IBCClass n) f

271+ibc i (IBCInterface n) f

272− = case lookupCtxtExact n (idris_classes i) of

272+ = case lookupCtxtExact n (idris_interfaces i) of

273 Just v -> return f { ibc_classes = (n,v): ibc_classes f }

274 _ -> ifail "IBC write failed"

275ibc i (IBCRecord n) f

@@ -390,7 +390,7 @@ process reexp phase archive fn = do

390 processImplicits archive

391 processInfix archive

392 processStatics archive

393− processClasses archive

393+ processInterfaces archive

394 processRecords archive

395 processInstances archive

396 processDSLs archive

@@ -545,18 +545,18 @@ processStatics ar = do

545 mapM_ (\ (n, s) ->

546 updateIState (\i -> i { idris_statics = addDef n s (idris_statics i) })) ss

547

548−processClasses :: Archive -> Idris ()

548+processInterfaces :: Archive -> Idris ()

549−processClasses ar = do

549+processInterfaces ar = do

550 cs <- getEntry [] "ibc_classes" ar

551 mapM_ (\ (n, c) -> do

552 i <- getIState

553 -- Don't lose instances from previous IBCs, which

554 -- could have loaded in any order

555− let is = case lookupCtxtExact n (idris_classes i) of

555+ let is = case lookupCtxtExact n (idris_interfaces i) of

556 Just (CI _ _ _ _ _ ins _) -> ins

557 _ -> []

558− let c' = c { class_instances = class_instances c ++ is }

558+ let c' = c { interface_instances = interface_instances c ++ is }

559− putIState (i { idris_classes = addDef n c' (idris_classes i) })) cs

559+ putIState (i { idris_interfaces = addDef n c' (idris_interfaces i) })) cs

560

561processRecords :: Archive -> Idris ()

562processRecords ar = do

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

1410 put x10

1411 put x11

1412 put x12

1413− PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12

1413+ PInterface x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12

1414 -> do putWord8 7

1415 put x1

1416 put x2

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

1547 x10 <- get

1548 x11 <- get

1549 x12 <- get

1550− return (PClass x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

1550+ return (PInterface x1 x2 x3 x4 x5 x6 x7 x8 x9 x10 x11 x12)

1551 8 -> do x1 <- get

1552 x2 <- get

1553 x3 <- get

@@ -2357,7 +2357,7 @@ instance (Binary t) => Binary (PArg' t) where

2357 _ -> error "Corrupted binary data for PArg'"

2358

2359

2360−instance Binary ClassInfo where

2360+instance Binary InterfaceInfo where

2361 put (CI x1 x2 x3 x4 x5 _ x6)

2362 = do put x1

2363 put x2

src/Idris/IdrisDoc.hs+12−12

@@ -173,9 +173,9 @@ removeOrphans list =

173 let children = S.fromList $ concatMap (names . (\(_, d, _) -> d)) list

174 in filter ((flip S.notMember children) . (\(n, _, _) -> n)) list

175

176− where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

176+ where names (Just (DataDoc _ fds)) = map (\(FD n _ _ _ _) -> n) fds

177− names (Just (ClassDoc _ _ fds _ _ _ _ c)) = map (\(FD n _ _ _ _) -> n) fds ++ map (\(FD n _ _ _ _) -> n) (maybeToList c)

177+ names (Just (InterfaceDoc _ _ fds _ _ _ _ c)) = map (\(FD n _ _ _ _) -> n) fds ++ map (\(FD n _ _ _ _) -> n) (maybeToList c)

178− names _ = []

178+ names _ = []

179

180-- | Whether a Name names something which should be documented

181filterName :: Name -- ^ Name to check

@@ -222,14 +222,14 @@ referredNss (n, Just d, _) =

222 names = concatMap (extractPTermNames) ts

223 in S.map getNs $ S.fromList names

224

225− where getFunDocs (FunDoc f) = [f]

225+ where getFunDocs (FunDoc f) = [f]

226− getFunDocs (DataDoc f fs) = f:fs

226+ getFunDocs (DataDoc f fs) = f:fs

227− getFunDocs (ClassDoc _ _ fs _ _ _ _ _) = fs

227+ getFunDocs (InterfaceDoc _ _ fs _ _ _ _ _) = fs

228− getFunDocs (RecordDoc _ _ f fs _) = f:fs

228+ getFunDocs (RecordDoc _ _ f fs _) = f:fs

229− getFunDocs (NamedInstanceDoc _ fd) = [fd]

229+ getFunDocs (NamedInstanceDoc _ fd) = [fd]

230− getFunDocs (ModDoc _ _) = []

230+ getFunDocs (ModDoc _ _) = []

231− types (FD _ _ args t _) = t:(map second args)

231+ types (FD _ _ args t _) = t:(map second args)

232− second (_, x, _, _) = x

232+ second (_, x, _, _) = x

233

234

235-- | Returns an NsDict of containing all known namespaces and their contents

@@ -583,7 +583,7 @@ createOtherDoc :: IState -- ^ Needed to determine the types of names

583 -> H.Html -- ^ Resulting HTML

584createOtherDoc ist (FunDoc fd) = createFunDoc ist fd

585

586−createOtherDoc ist (ClassDoc n docstring fds _ _ _ _ c) = do

586+createOtherDoc ist (InterfaceDoc n docstring fds _ _ _ _ c) = do

587 H.dt ! (A.id $ toValue $ show n) $ do

588 H.span ! class_ "word" $ do "interface"; nbsp

589 H.span ! class_ "name type"

src/Idris/Interactive.hs+14−14

@@ -349,10 +349,10 @@ makeLemma fn updatefile l n

349 if (not isProv) then do

350 let skip = guessImps i (tt_ctxt i) mty

351 let impty = stripMNBind skip margs (delab i mty)

352− let classes = guessClasses i (tt_ctxt i) [] (allNamesIn impty) mty

352+ let interfaces = guessInterfaces i (tt_ctxt i) [] (allNamesIn impty) mty

353

354 let lem = show n ++ " : " ++

355− constraints i classes mty ++

355+ constraints i interfaces mty ++

356 showTmOpts (defaultPPOption { ppopt_pinames = True })

357 impty

358 let lem_app = guessBrackets False tyline (show n) (show n ++ appArgs skip margs mty)

@@ -434,7 +434,7 @@ makeLemma fn updatefile l n

434 guessImps ist ctxt (Bind n (Pi _ ty _) sc)

435 | guarded ctxt n (substV (P Bound n Erased) sc)

436 = n : guessImps ist ctxt sc

437− | isClass ist ty

437+ | isInterface ist ty

438 = n : guessImps ist ctxt sc

439 | paramty ty = n : guessImps ist ctxt sc

440 | ignoreName n = n : guessImps ist ctxt sc

@@ -450,13 +450,13 @@ makeLemma fn updatefile l n

450 "_aX" -> True

451 _ -> False

452

453− guessClasses :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]

453+ guessInterfaces :: IState -> Context -> [Name] -> [Name] -> Term -> [Name]

454− guessClasses ist ctxt binders usednames (Bind n (Pi _ ty _) sc)

454+ guessInterfaces ist ctxt binders usednames (Bind n (Pi _ ty _) sc)

455− | isParamClass ist ty && any (\x -> elem x usednames)

455+ | isParamInterface ist ty && any (\x -> elem x usednames)

456− (paramNames binders ty)

456+ (paramNames binders ty)

457− = n : guessClasses ist ctxt (n : binders) usednames sc

457+ = n : guessInterfaces ist ctxt (n : binders) usednames sc

458− | otherwise = guessClasses ist ctxt (n : binders) usednames sc

458+ | otherwise = guessInterfaces ist ctxt (n : binders) usednames sc

459− guessClasses ist ctxt _ _ _ = []

459+ guessInterfaces ist ctxt _ _ _ = []

460

461 paramNames bs ty | (P _ _ _, args) <- unApply ty

462 = vnames args

@@ -464,16 +464,16 @@ makeLemma fn updatefile l n

464 vnames (V i : xs) | i < length bs = bs !! i : vnames xs

465 vnames (_ : xs) = vnames xs

466

467− isClass ist t

467+ isInterface ist t

468 | (P _ n _, args) <- unApply t

469− = case lookupCtxtExact n (idris_classes ist) of

469+ = case lookupCtxtExact n (idris_interfaces ist) of

470 Just _ -> True

471 _ -> False

472 | otherwise = False

473

474− isParamClass ist t

474+ isParamInterface ist t

475 | (P _ n _, args) <- unApply t

476− = case lookupCtxtExact n (idris_classes ist) of

476+ = case lookupCtxtExact n (idris_interfaces ist) of

477 Just _ -> any isV args

478 _ -> False

479 | otherwise = False

src/Idris/Parser.hs+40−40

@@ -226,7 +226,7 @@ internalDecl syn

226 <|> params syn

227 <|> mutual syn

228 <|> namespace syn

229− <|> class_ syn

229+ <|> interface_ syn

230 <|> do d <- dsl syn; return [d]

231 <|> directive syn

232 <|> provider syn

@@ -340,8 +340,8 @@ declExtension syn ns rules =

340 (updateRecCon ns cname)

341 cdoc

342 s

343− updateNs ns (PClass docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)

343+ updateNs ns (PInterface docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)

344− = PClass docs s fc cs (updateB ns cn) fc' ps pdocs pdets

344+ = PInterface docs s fc cs (updateB ns cn) fc' ps pdocs pdets

345 (map (updateNs ns) ds)

346 (updateRecCon ns cname)

347 cdocs

@@ -861,23 +861,23 @@ ClassBlock ::=

861 ;

862@

863-}

864−classBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])

864+interfaceBlock :: SyntaxInfo -> IdrisParser (Maybe (Name, FC), Docstring (Either Err PTerm), [PDecl])

865−classBlock syn = do reservedHL "where"

865+interfaceBlock syn = do reservedHL "where"

866− openBlock

866+ openBlock

867− (cn, cd) <- option (Nothing, emptyDocstring) $

867+ (cn, cd) <- option (Nothing, emptyDocstring) $

868− try (do (doc, _) <- option noDocs docComment

868+ try (do (doc, _) <- option noDocs docComment

869− n <- constructor

869+ n <- constructor

870− return (Just n, doc))

870+ return (Just n, doc))

871− ist <- get

871+ ist <- get

872− let cd' = annotate syn ist cd

872+ let cd' = annotate syn ist cd

873−

873+

874− ds <- many (notEndBlock >> try (instance_ True syn)

874+ ds <- many (notEndBlock >> try (instance_ True syn)

875− <|> do x <- data_ syn

875+ <|> do x <- data_ syn

876− return [x]

876+ return [x]

877− <|> fnDecl syn)

877+ <|> fnDecl syn)

878− closeBlock

878+ closeBlock

879− return (cn, cd', concat ds)

879+ return (cn, cd', concat ds)

880− <?> "class block"

880+ <?> "class block"

881

882 where

883 constructor :: IdrisParser (Name, FC)

@@ -901,29 +901,29 @@ Class ::=

901 ;

902@

903-}

904−class_ :: SyntaxInfo -> IdrisParser [PDecl]

904+interface_ :: SyntaxInfo -> IdrisParser [PDecl]

905−class_ syn = do (doc, argDocs, acc)

905+interface_ syn = do (doc, argDocs, acc)

906− <- try (do (doc, argDocs) <- docstring syn

906+ <- try (do (doc, argDocs) <- docstring syn

907− acc <- accessibility

907+ acc <- accessibility

908− classKeyword

908+ interfaceKeyword

909− return (doc, argDocs, acc))

909+ return (doc, argDocs, acc))

910− fc <- getFC

910+ fc <- getFC

911− cons <- constraintList syn

911+ cons <- constraintList syn

912− let cons' = [(c, ty) | (c, _, ty) <- cons]

912+ let cons' = [(c, ty) | (c, _, ty) <- cons]

913− (n_in, nfc) <- fnName

913+ (n_in, nfc) <- fnName

914− let n = expandNS syn n_in

914+ let n = expandNS syn n_in

915− cs <- many carg

915+ cs <- many carg

916− fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps

916+ fds <- option [(cn, NoFC) | (cn, _, _) <- cs] fundeps

917− (cn, cd, ds) <- option (Nothing, fst noDocs, []) (classBlock syn)

917+ (cn, cd, ds) <- option (Nothing, fst noDocs, []) (interfaceBlock syn)

918− accData acc n (concatMap declared ds)

918+ accData acc n (concatMap declared ds)

919− return [PClass doc syn fc cons' n nfc cs argDocs fds ds cn cd]

919+ return [PInterface doc syn fc cons' n nfc cs argDocs fds ds cn cd]

920− <?> "type-class declaration"

920+ <?> "type-class declaration"

921 where

922 fundeps :: IdrisParser [(Name, FC)]

923 fundeps = do lchar '|'; sepBy name (lchar ',')

924

925− classKeyword :: IdrisParser ()

925+ interfaceKeyword :: IdrisParser ()

926− classKeyword = reservedHL "interface"

926+ interfaceKeyword = reservedHL "interface"

927 <|> do reservedHL "class"

928 fc <- getFC

929 parserWarning fc Nothing (Msg "The 'class' keyword is deprecated. Use 'interface' instead.")

@@ -1866,7 +1866,7 @@ loadSource lidr f toline

1866 toMutual x = let r = PMutual (fileFC "single mutual") [x] in

1867 case x of

1868 PClauses{} -> r

1869− PClass{} -> r

1869+ PInterface{} -> r

1870 PData{} -> r

1871 PInstance{} -> r

1872 _ -> x

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

@@ -713,8 +713,8 @@ collect (PParams f ns ps : ds) = PParams f ns (collect ps) : collect ds

713collect (POpenInterfaces f ns ps : ds) = POpenInterfaces f ns (collect ps) : collect ds

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

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

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

716+collect (PInterface doc f s cs n nfc ps pdocs fds ds cn cd : ds')

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

717+ = PInterface doc f s cs n nfc ps pdocs fds (collect ds) cn cd : collect ds'

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

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

720collect (d : ds) = d : collect ds

src/Idris/PartialEval.hs+8−8

@@ -141,8 +141,8 @@ mkPE_TyDecl ist args ty = mkty args ty

141 mkty ((ExplicitD, v) : xs) (Bind n (Pi _ t k) sc)

142 = PPi expl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

143 mkty ((ImplicitD, v) : xs) (Bind n (Pi _ t k) sc)

144− | concreteClass ist t = mkty xs sc

144+ | concreteInterface ist t = mkty xs sc

145− | classConstraint ist t

145+ | interfaceConstraint ist t

146 = PPi constraint n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

147 | otherwise = PPi impl n NoFC (delab ist (generaliseIn t)) (mkty xs sc)

148

@@ -161,18 +161,18 @@ mkPE_TyDecl ist args ty = mkty args ty

161 gen tm = return tm

162

163-- | Checks if a given argument is a type class constraint argument

164−classConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool

164+interfaceConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool

165−classConstraint ist v

165+interfaceConstraint ist v

166− | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_classes ist) of

166+ | (P _ c _, args) <- unApply v = case lookupCtxt c (idris_interfaces ist) of

167 [_] -> True

168 _ -> False

169 | otherwise = False

170

171-- | Checks if the given arguments of a type class constraint are all either constants

172-- or references (i.e. that it doesn't contain any complex terms).

173−concreteClass :: IState -> TT Name -> Bool

173+concreteInterface :: IState -> TT Name -> Bool

174−concreteClass ist v

174+concreteInterface ist v

175− | not (classConstraint ist v) = False

175+ | not (interfaceConstraint ist v) = False

176 | (P _ c _, args) <- unApply v = all concrete args

177 | otherwise = False

178 where concrete (Constant _) = True

src/Idris/ProofSearch.hs+7−7

@@ -101,7 +101,7 @@ trivialTCs ok elab ist

101

102 tcArg env ty

103 | (P _ n _, args) <- unApply (getRetTy (normalise (tt_ctxt ist) env ty))

104− = case lookupCtxtExact n (idris_classes ist) of

104+ = case lookupCtxtExact n (idris_interfaces ist) of

105 Just _ -> True

106 _ -> False

107 | otherwise = False

@@ -412,13 +412,13 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

412

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

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

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

415+ tcArgsOK ty hs | (P _ nc _, as) <- unApply (getRetTy ty), nc == numinterface && defaultOn

416 = Just []

417 tcArgsOK ty hs -- if any determining arguments are metavariables, postpone

418 = let (f, as) = unApply (getRetTy ty) in

419 case f of

420− P _ cn _ -> case lookupCtxtExact cn (idris_classes ist) of

420+ P _ cn _ -> case lookupCtxtExact cn (idris_interfaces ist) of

421− Just ci -> tcDetArgsOK 0 (class_determiners ci) hs as

421+ Just ci -> tcDetArgsOK 0 (interface_determiners ci) hs as

422 Nothing -> if any (isMeta hs) as

423 then Nothing

424 else Just []

@@ -451,9 +451,9 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

451 | Constant _ <- c = not (n `elem` hs)

452 notHole _ _ = True

453

454− numclass = sNS (sUN "Num") ["Interfaces","Prelude"]

454+ numinterface = sNS (sUN "Num") ["Interfaces","Prelude"]

455

456− addDefault t num@(P _ nc _) [P Bound a _] | nc == numclass && defaultOn

456+ addDefault t num@(P _ nc _) [P Bound a _] | nc == numinterface && defaultOn

457 = do focus a

458 fill (RConstant (AType (ATInt ITBig))) -- default Integer

459 solve

@@ -525,7 +525,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

525findInstances :: IState -> Term -> [Name]

526findInstances ist t

527 | (P _ n _, _) <- unApply (getRetTy t)

528− = case lookupCtxt n (idris_classes ist) of

528+ = case lookupCtxt n (idris_interfaces ist) of

529 [CI _ _ _ _ _ ins _] ->

530 [n | (n, True) <- ins, accessible n]

531 _ -> []

src/Idris/REPL.hs+2−2

@@ -868,7 +868,7 @@ process fn (NewDefn decls) = do

868 getName (PTy docs argdocs syn fc opts name _ ty) = Just name

869 getName (PClauses fc opts name (clause:clauses)) = Just (getClauseName clause)

870 getName (PData doc argdocs syn fc opts dataDecl) = Just (d_name dataDecl)

871− getName (PClass doc syn fc constraints name nfc parms parmdocs fds decls _ _) = Just name

871+ getName (PInterface doc syn fc constraints name nfc parms parmdocs fds decls _ _) = Just name

872 getName _ = Nothing

873 -- getClauseName is partial and I am not sure it's used safely! -- trillioneyes

874 getClauseName (PClause fc name whole with rhs whereBlock) = name

@@ -943,7 +943,7 @@ process fn (Undefine names) = undefine names

943 undefOne n = do fputState (ctxt_lookup n . known_terms) Nothing

944 -- for now just assume it's a class. Eventually we'll want some kind of

945 -- smart detection of exactly what kind of name we're undefining.

946− fputState (ctxt_lookup n . known_classes) Nothing

946+ fputState (ctxt_lookup n . known_interfaces) Nothing

947 fmodifyState repl_definitions (delete n)

948 undefClosure n =

949 do replDefs <- idris_repl_defs `fmap` get

src/Idris/TypeSearch.hs+52−52

@@ -30,8 +30,8 @@ import qualified Data.Text as T (pack, isPrefixOf)

30import Data.Traversable (traverse)

31

32import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)

33−import Idris.AbsSyntaxTree (class_instances, ClassInfo, defaultSyntax, eqTy, Idris

33+import Idris.AbsSyntaxTree (interface_instances, InterfaceInfo, defaultSyntax, eqTy, Idris

34− , IState (idris_classes, idris_docstrings, tt_ctxt, idris_outputmode),

34+ , IState (idris_interfaces, idris_docstrings, tt_ctxt, idris_outputmode),

35 implicitAllowed, OutputMode(..), PTerm, toplevel)

36import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

37import Idris.Core.TT hiding (score)

@@ -173,8 +173,8 @@ deleteFromArgList n = filter ((/= n) . fst)

173-- | Asymmetric modifications to keep track of

174data AsymMods = Mods

175 { argApp :: !Int

176− , typeClassApp :: !Int

176+ , interfaceApp :: !Int

177− , typeClassIntro :: !Int

177+ , interfaceIntro :: !Int

178 } deriving (Eq, Show)

179

180

@@ -253,18 +253,18 @@ instance Monoid Score where

253type ArgsDAG = [((Name, Type), (Int, Set Name))]

254

255-- | A list of typeclass constraints

256−type Classes = [(Name, Type)]

256+type Interfaces = [(Name, Type)]

257

258-- | The state corresponding to an attempted match of two types.

259data State = State

260 { holes :: ![(Name, Type)] -- ^ names which have yet to be resolved

261− , argsAndClasses :: !(Sided (ArgsDAG, Classes))

261+ , argsAndInterfaces :: !(Sided (ArgsDAG, Interfaces))

262 -- ^ arguments and typeclass constraints for each type which have yet to be resolved

263 , score :: !Score -- ^ the score so far

264 , usedNames :: ![Name] -- ^ all names that have been used

265 } deriving Show

266

267−modifyTypes :: (Type -> Type) -> (ArgsDAG, Classes) -> (ArgsDAG, Classes)

267+modifyTypes :: (Type -> Type) -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)

268modifyTypes f = modifyDag *** modifyList

269 where

270 modifyDag = map (first (second f))

@@ -273,11 +273,11 @@ modifyTypes f = modifyDag *** modifyList

273findNameInArgsDAG :: Name -> ArgsDAG -> Maybe (Type, Maybe Int)

274findNameInArgsDAG name = fmap ((snd . fst) &&& (Just . fst . snd)) . find ((name ==) . fst . fst)

275

276−findName :: Name -> (ArgsDAG, Classes) -> Maybe (Type, Maybe Int)

276+findName :: Name -> (ArgsDAG, Interfaces) -> Maybe (Type, Maybe Int)

277−findName n (args, classes) = findNameInArgsDAG n args <|> ((,) <$> lookup n classes <*> Nothing)

277+findName n (args, interfaces) = findNameInArgsDAG n args <|> ((,) <$> lookup n interfaces <*> Nothing)

278

279−deleteName :: Name -> (ArgsDAG, Classes) -> (ArgsDAG, Classes)

279+deleteName :: Name -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)

280−deleteName n (args, classes) = (deleteFromDag n args, filter ((/= n) . fst) classes)

280+deleteName n (args, interfaces) = (deleteFromDag n args, filter ((/= n) . fst) interfaces)

281

282tcToMaybe :: TC a -> Maybe a

283tcToMaybe (OK x) = Just x

@@ -287,8 +287,8 @@ inArgTys :: (Type -> Type) -> ArgsDAG -> ArgsDAG

287inArgTys = map . first . second

288

289

290−typeclassUnify :: Ctxt ClassInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]

290+interfaceUnify :: Ctxt InterfaceInfo -> Context -> Type -> Type -> Maybe [(Name, Type)]

291−typeclassUnify classInfo ctxt ty tyTry = do

291+interfaceUnify interfaceInfo ctxt ty tyTry = do

292 res <- tcToMaybe $ match_unify ctxt [] (ty, Nothing) (retTy, Nothing) [] theHoles []

293 guard $ null (theHoles \\ map fst res)

294 let argTys' = map (second $ foldr (.) id [ subst n t | (n, t) <- res ]) tcArgs

@@ -297,13 +297,13 @@ typeclassUnify classInfo ctxt ty tyTry = do

297 tyTry' = vToP tyTry

298 theHoles = map fst nonTcArgs

299 retTy = getRetTy tyTry'

300− (tcArgs, nonTcArgs) = partition (isTypeClassArg classInfo . snd) $ getArgTys tyTry'

300+ (tcArgs, nonTcArgs) = partition (isInterfaceArg interfaceInfo . snd) $ getArgTys tyTry'

301

302−isTypeClassArg :: Ctxt ClassInfo -> Type -> Bool

302+isInterfaceArg :: Ctxt InterfaceInfo -> Type -> Bool

303−isTypeClassArg classInfo ty = not (null (getClassName clss >>= flip lookupCtxt classInfo)) where

303+isInterfaceArg interfaceInfo ty = not (null (getInterfaceName clss >>= flip lookupCtxt interfaceInfo)) where

304 (clss, args) = unApply ty

305− getClassName (P (TCon _ _) className _) = [className]

305+ getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]

306− getClassName _ = []

306+ getInterfaceName _ = []

307

308

309-- | Compute the power set

@@ -345,12 +345,12 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

345 <$> flipEqualities ty <*> flipEqualitiesDag xs

346 startStates (numEqFlips, sndDag, sndRetTy) = do

347 state <- unifyQueue (State startingHoles

348− (Sided (dag1, typeClassArgs1) (sndDag, typeClassArgs2))

348+ (Sided (dag1, interfaceArgs1) (sndDag, interfaceArgs2))

349 (mempty { equalityFlips = numEqFlips }) usedns) [(retTy1, sndRetTy)]

350 return (score state, state)

351

352

353− (dag2, typeClassArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)

353+ (dag2, interfaceArgs2, retTy2) = makeDag (uniqueBinders (map fst argNames1) type2)

354 argNames2 = map fst dag2

355 usedns = map fst startingHoles

356 startingHoles = argNames1 ++ argNames2

@@ -376,13 +376,13 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

376

377

378 ctxt = tt_ctxt istate

379− classInfo = idris_classes istate

379+ interfaceInfo = idris_interfaces istate

380

381− (dag1, typeClassArgs1, retTy1) = makeDag type1

381+ (dag1, interfaceArgs1, retTy1) = makeDag type1

382 argNames1 = map fst dag1

383− makeDag :: Type -> (ArgsDAG, Classes, Type)

383+ makeDag :: Type -> (ArgsDAG, Interfaces, Type)

384 makeDag = first3 (zipWith (\i (ty, deps) -> (ty, (i, deps))) [0..] . reverseDag) .

385− computeDagP (isTypeClassArg classInfo) . vToP . unLazy

385+ computeDagP (isInterfaceArg interfaceInfo) . vToP . unLazy

386 first3 f (a,b,c) = (f a, b, c)

387

388 -- update our state with the unification resolutions

@@ -396,14 +396,14 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

396 let transScore = fromMaybe 0 (abs <$> ((-) <$> ix1 <*> ix2))

397 return (inScore (\s -> s { transposition = transposition s + transScore }) state'', (ty1, ty2) : queue)

398 where

399− unresolved = argsAndClasses state

399+ unresolved = argsAndInterfaces state

400 inScore f stat = stat { score = f (score stat) }

401 findArgs = ((,) <$> findName name (left unresolved) <*> findName name2 (right unresolved)) <|>

402 ((,) <$> findName name2 (left unresolved) <*> findName name (right unresolved))

403 matchnames = [name, name2]

404 deleteArgs = deleteName name . deleteName name2

405 state' = state { holes = filter (not . (`elem` matchnames) . fst) (holes state)

406− , argsAndClasses = both (modifyTypes (subst name term) . deleteArgs) unresolved}

406+ , argsAndInterfaces = both (modifyTypes (subst name term) . deleteArgs) unresolved}

407

408 resolveUnis ((name, term) : xs)

409 state@(State hs unresolved _ _) = case both (findName name) unresolved of

@@ -427,7 +427,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

427 addScore additions theState = theState { score = let s = score theState in

428 s { asymMods = asymMods s `mappend` additions } }

429 state' = state { holes = filter (not . (`elem` toDelete) . fst) hs

430− , argsAndClasses = both (modifyTypes (subst name term) . deleteMany) (argsAndClasses state) }

430+ , argsAndInterfaces = both (modifyTypes (subst name term) . deleteMany) (argsAndInterfaces state) }

431 nextStep = resolveUnis xs state'

432

433

@@ -443,19 +443,19 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

443 guard $ scoreCriterion (score state')

444 unifyQueue state' (queue ++ queueAdditions)

445

446− possClassInstances :: [Name] -> Type -> [Type]

446+ possInterfaceInstances :: [Name] -> Type -> [Type]

447− possClassInstances usedns ty = do

447+ possInterfaceInstances usedns ty = do

448− className <- getClassName clss

448+ interfaceName <- getInterfaceName clss

449− classDef <- lookupCtxt className classInfo

449+ interfaceDef <- lookupCtxt interfaceName interfaceInfo

450− n <- class_instances classDef

450+ n <- interface_instances interfaceDef

451 def <- lookupCtxt (fst n) (definitions ctxt)

452 nty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])

453 let ty' = vToP (uniqueBinders usedns nty)

454 return ty'

455 where

456 (clss, _) = unApply ty

457− getClassName (P (TCon _ _) className _) = [className]

457+ getInterfaceName (P (TCon _ _) interfaceName _) = [interfaceName]

458− getClassName _ = []

458+ getInterfaceName _ = []

459

460 -- 'Just' if the computation hasn't totally failed yet, 'Nothing' if it has

461 -- 'Left' if we haven't found a terminal state, 'Right' if we have

@@ -496,24 +496,24 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

496 | sds <- allMods ]

497 where

498 allMods = parallel defMod mods

499− mods :: Sided [( Classes, AsymMods, [Name] )]

499+ mods :: Sided [( Interfaces, AsymMods, [Name] )]

500 mods = both (instanceMods . snd) unresolved

501− defMod :: Sided (Classes, AsymMods, [Name])

501+ defMod :: Sided (Interfaces, AsymMods, [Name])

502 defMod = both (\(_, cs) -> (cs, mempty , [])) unresolved

503 parallel :: Sided a -> Sided [a] -> [Sided a]

504 parallel (Sided l r) (Sided ls rs) = map (flip Sided r) ls ++ map (Sided l) rs

505− instanceMods :: Classes -> [( Classes , AsymMods, [Name] )]

505+ instanceMods :: Interfaces -> [( Interfaces , AsymMods, [Name] )]

506− instanceMods classes = [ ( newClassArgs, mempty { typeClassApp = 1 }, newHoles )

506+ instanceMods interfaces = [ ( newInterfaceArgs, mempty { interfaceApp = 1 }, newHoles )

507− | (_, ty) <- classes

507+ | (_, ty) <- interfaces

508− , inst <- possClassInstances usedns ty

508+ , inst <- possInterfaceInstances usedns ty

509− , newClassArgs <- maybeToList $ typeclassUnify classInfo ctxt ty inst

509+ , newInterfaceArgs <- maybeToList $ interfaceUnify interfaceInfo ctxt ty inst

510− , let newHoles = map fst newClassArgs ]

510+ , let newHoles = map fst newInterfaceArgs ]

511

512

513 -- Stage 1 - match arguments

514 nextSteps (State hs (Sided (dagL, c1) (dagR, c2)) scoreAcc usedns) = results where

515

516− results = concatMap takeSomeClasses results1

516+ results = concatMap takeSomeInterfaces results1

517

518 -- we only try to match arguments whose names don't appear in the types

519 -- of any other arguments

@@ -532,18 +532,18 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

532

533 -- Stage 2 - simply introduce a subset of the typeclasses

534 -- we've finished, so take some classes

535− takeSomeClasses (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =

535+ takeSomeInterfaces (State [] unresolved@(Sided ([], _) ([], _)) scoreAcc usedns) =

536− map statesFromMods . prod $ both (classMods . snd) unresolved

536+ map statesFromMods . prod $ both (interfaceMods . snd) unresolved

537 where

538 swap (Sided l r) = Sided r l

539− statesFromMods :: Sided (Classes, AsymMods) -> State

539+ statesFromMods :: Sided (Interfaces, AsymMods) -> State

540− statesFromMods sides = let classes = both (\(c, _) -> ([], c)) sides

540+ statesFromMods sides = let interfaces = both (\(c, _) -> ([], c)) sides

541 mods = swap (both snd sides) in

542− State [] classes (scoreAcc `mappend` (mempty { asymMods = mods })) usedns

542+ State [] interfaces (scoreAcc `mappend` (mempty { asymMods = mods })) usedns

543− classMods :: Classes -> [(Classes, AsymMods)]

543+ interfaceMods :: Interfaces -> [(Interfaces, AsymMods)]

544− classMods cs = let lcs = length cs in

544+ interfaceMods cs = let lcs = length cs in

545− [ (cs', mempty { typeClassIntro = lcs - length cs' }) | cs' <- subsets cs ]

545+ [ (cs', mempty { interfaceIntro = lcs - length cs' }) | cs' <- subsets cs ]

546 prod :: Sided [a] -> [Sided a]

547 prod (Sided ls rs) = [Sided l r | l <- ls, r <- rs]

548 -- still have arguments to match, so just be the identity

549− takeSomeClasses s = [s]

549+ takeSomeInterfaces s = [s]

test/idrisdoc004/TestTypeclasses.idr → test/idrisdoc004/TestInterfaces.idrrenamed+1−1

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

1−module TestTypeclasses

1+module TestInterfaces

2

3||| This is a test

4|||

test/idrisdoc004/expected+1−1

@@ -1 +1 @@

1−Typeclasses are documented

1+Interfaces are documented

test/idrisdoc004/run+3−3

@@ -1,5 +1,5 @@

1#!/usr/bin/env bash

2−# Tests that documentation is generated for typeclasses

2+# Tests that documentation is generated for interfaces

3−${IDRIS:-idris} $@ --mkdoc test_typeclasses.ipkg

3+${IDRIS:-idris} $@ --mkdoc test_interfaces.ipkg

4−[ -d test_typeclasses_doc ] && echo "Typeclasses are documented"

4+[ -d test_interfaces_doc ] && echo "Interfaces are documented"

5rm -rf *.ibc *_doc

test/idrisdoc004/test_interfaces.ipkgnew file+6

@@ -0,0 +1,6 @@

1+package test_interfaces

2+

3+opts = "--quiet"

4+

5+modules = TestInterfaces

6+

test/idrisdoc004/test_typeclasses.ipkgdeleted−6

@@ -1,6 +0,0 @@

1−package test_typeclasses

2−

3−opts = "--quiet"

4−

5−modules = TestTypeclasses

6−

test/interfaces001/ClassName.idr → test/interfaces001/InterfaceName.idrrenamed+2−2

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

1−module ClassName

1+module InterfaceName

2

3||| A fancy shower with a constructor

4||| @ a the thing to be shown

@@ -21,7 +21,7 @@ badShow = MkMyShow (const "hej")

21test1 : twiceAString 2 = "22"

22test1 = Refl

23

24−test2 : twiceAString @{ClassName.badShow} 2 = "hejhej"

24+test2 : twiceAString @{InterfaceName.badShow} 2 = "hejhej"

25test2 = Refl

26

27

test/interfaces001/run+1−1

@@ -1,3 +1,3 @@

1#!/usr/bin/env bash

2−${IDRIS:-idris} $@ --quiet --nocolour --consolewidth 70 ClassName.idr < input

2+${IDRIS:-idris} $@ --quiet --nocolour --consolewidth 70 InterfaceName.idr < input

3rm -f *.ibc

test/regression001/reg065.idr+1−1

@@ -2,7 +2,7 @@

2|||

3||| Fixes a regression where previous methods used in a later method's

4||| type would lead to "can't find interface" errors

5−module TypeClassDep

5+module InterfaceDep

6

7import Data.Vect

8