06d9db6 · Idris-dev · git.iko.soy

docs/reference/compilation.rst+1−1

@@ -68,7 +68,7 @@ logging level between: 1 to 10 using the command-line option: ``--log

6868

6969+ Level 0: Show no logging output. Default level

7070+ Level 1: High level details of the compilation process.

71−+ Level 2: Provides details of the coverage checking, and further details the elaboration process specifically: Class, Clauses, Data, Term, and Types,

71++ Level 2: Provides details of the coverage checking, and further details the elaboration process specifically: Interface, Clauses, Data, Term, and Types,

7272+ Level 3: Provides details of compilation of the IRTS, erasure, parsing, case splitting, and further details elaboration of: Instances, Providers, and Values.

7373+ Level 4: Provides further details on: Erasure, Coverage Checking, Case splitting, and elaboration of clauses.

7474+ Level 5: Provides details on the prover, and further details elaboration (adding declarations) and compilation of the IRTS.

docs/reference/erasure.rst+2−2

@@ -163,7 +163,7 @@ analysis algorithm.)

163163* function arguments

164164

165165* data constructor fields (including record fields and dictionary

166− fields of class instances)

166+ fields of interface implementations)

167167

168168For example, ``Either`` often compiles to the same runtime

169169representation as ``Bool``. Constructor field removal sometimes

@@ -295,7 +295,7 @@ considered to be using all their arguments. To work around this, you

295295can force erasure via the type system, using the ``Erased`` wrapper:

296296https://github.com/idris-lang/Idris-dev/blob/master/libs/base/Data/Erased.idr

297297

298−Typeclass methods are considered to be using the union of all their

298+Interface methods are considered to be using the union of all their

299299implementations. In other words, an argument of a method is unused

300300only if it is unused in every implementation of the method that occurs

301301in the program.

docs/reference/misc.rst+1−1

@@ -275,7 +275,7 @@ That is, ``{x}`` behaves like ``{x=x}``.

275275Existence of an instance

276276========================

277277

278−In order to show that an instance of some typeclass is defined for some

278+In order to show that an instance of some interface is defined for some

279279type, one could use the ``%instance`` keyword:

280280

281281.. code:: idris

docs/reference/repl.rst+27−17

@@ -240,7 +240,7 @@ surround it in parentheses.

240240 Idris> :t plus 4

241241 plus (Builtins.fromInteger 4) : Nat -> Nat

242242

243−You can also ask for basic information about typeclasses with ``:doc``:

243+You can also ask for basic information about interfaces with ``:doc``:

244244

245245::

246246

@@ -268,14 +268,11 @@ Other documentation is also available from ``:doc``:

268268::

269269

270270 Idris> :doc (+)

271− Prelude.Classes.+ : (a : Type) -> (Num a) -> a -> a -> a

271+ Prelude.Interfaces.(+) : Num ty => ty -> ty -> ty

272272

273273 infixl 8

274274

275− Arguments:

276− Class constraint Prelude.Classes.Num a

277− __pi_arg : a

278− __pi_arg1 : a

275+ The function is Total

279276

280277::

281278

@@ -302,17 +299,30 @@ Other documentation is also available from ``:doc``:

302299::

303300

304301 Idris> :doc Monad

305− Interface Prelude.Monad.Monad

306− Methods:

302+ Interface Monad

303+

304+ Parameters:

305+ m

307306

308− Prelude.Monad.>>= : (m : Type -> Type) -> (a : Type) -> (b : Type) -> (Monad m) -> (m a) -> (a -> m b) -> m b

307+ Methods:

308+ (>>=) : Monad m => m a -> (a -> m b) -> m b

309+ Also called bind.

310+ infixl 5

309311

310− infixl 5

312+ The function is Total

313+ join : Monad m => m (m a) -> m a

314+ Also called flatten or mu

311315

312− Arguments:

313− Class constraint Prelude.Monad.Monad m

314− __pi_arg : m a

315− __pi_arg1 : a -> m b

316+ The function is Total

317+ Implementations:

318+ Monad (IO' ffi)

319+ Monad Stream

320+ Monad Provider

321+ Monad Elab

322+ Monad PrimIO

323+ Monad Maybe

324+ Monad (Either e)

325+ Monad List

316326

317327Finding things

318328~~~~~~~~~~~~~~

@@ -382,7 +392,7 @@ some string, and prints the results. For example:

382392

383393

384394 Eq : Type -> Type

385− The Eq class defines inequality and equality.

395+ The Eq interface defines inequality and equality.

386396

387397 GTE : Nat -> Nat -> Type

388398 Greater than or equal to

@@ -426,10 +436,10 @@ some string, and prints the results. For example:

426436 > Prelude.pow : Num a => a -> Nat -> a

427437

428438

429− > Prelude.Classes.(*) : Num a => a -> a -> a

439+ > Prelude.Interfaces.(*) : Num a => a -> a -> a

430440

431441

432− > Prelude.Classes.(+) : Num a => a -> a -> a

442+ > Prelude.Interfaces.(+) : Num a => a -> a -> a

433443 ... (More results)

434444

435445``:search`` can also look for dependent types:

libs/base/Data/Complex.idr+1−1

@@ -27,7 +27,7 @@ implementation Show a => Show (Complex a) where

2727 plus_i = User 6

2828

2929

30−-- when we have a type class 'Fractional' (which contains Double),

30+-- when we have an interface 'Fractional' (which contains Double),

3131-- we can do:

3232{-

3333implementation Fractional a => Fractional (Complex a) where

libs/contrib/Control/Algebra/NumericInstances.idr+1−1

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

1−||| Instances of algebraic classes (group, ring, etc) for numeric data types,

1+||| Instances of algebraic interfaces (group, ring, etc) for numeric data types,

22||| and Complex number types.

33module Control.Algebra.NumericInstances

44

libs/contrib/Data/Matrix/Algebraic.idr+3−3

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

11||| Matrix operations with vector space dimensionalities enforced

2−||| at the type level. Uses operations from classes in `Control.Algebra`

2+||| at the type level. Uses operations from interfaces in `Control.Algebra`

33||| and `Control.Algebra.VectorSpace`.

44module Data.Matrix.Algebraic

55

@@ -23,7 +23,7 @@ infixr 7 \&\ -- vector tensor product

2323infixr 7 <&> -- matrix tensor product

2424

2525-----------------------------------------------------------------------

26−-- Vectors as members of algebraic classes

26+-- Vectors as members of algebraic interfaces

2727-----------------------------------------------------------------------

2828

2929implementation Semigroup a => Semigroup (Vect n a) where

@@ -146,4 +146,4 @@ det {n} m = case n of

146146-- Matrix Algebra Properties

147147-----------------------------------------------------------------------

148148

149−-- TODO: Prove properties of matrix algebra for 'Verified' algebraic classes

149+-- TODO: Prove properties of matrix algebra for 'Verified' algebraic interfaces

libs/contrib/Data/Matrix/Numeric.idr+1−1

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

11||| Matrix operations with vector space dimensionalities enforced

2−||| at the type level. Uses operations from the Num type class.

2+||| at the type level. Uses operations from the Num interface.

33module Data.Matrix.Numeric

44

55import public Data.Matrix

libs/effects/Effects.idr+1−1

@@ -366,7 +366,7 @@ eff env (l :- prog) k

366366 = let env' = unlabel env in

367367 eff env' prog (\p', envk => k p' (relabel l envk))

368368

369−-- yuck :) Haven't got interface instances working nicely in tactic

369+-- yuck :) Haven't got interface implementations working nicely in tactic

370370-- proofs yet, and 'search' can't be told about any hints yet,

371371-- so just brute force it.

372372syntax MkDefaultEnv = with Env

libs/oldeffects/Effects.idr+2−2

@@ -24,7 +24,7 @@ Effect = (x : Type) -> Type -> (x -> Type) -> Type

2424data EFFECT : Type where

2525 MkEff : Type -> Effect -> EFFECT

2626

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

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

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

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

3030 ||| How to handle the effect.

@@ -235,7 +235,7 @@ eff {xs = [l ::: x]} env (l :- prog) k

235235 = let env' = unlabel env in

236236 eff env' prog (\p', envk => k p' (relabel l envk))

237237

238−-- yuck :) Haven't got type class instances working nicely in tactic

238+-- yuck :) Haven't got interface implementations working nicely in tactic

239239-- proofs yet, and 'search' can't be told about any hints yet,

240240-- so just brute force it.

241241syntax MkDefaultEnv = with Env

libs/prelude/Prelude/Nat.idr+1−1

@@ -197,7 +197,7 @@ toIntNat n = toIntNat' n 0 where

197197(-) m n {smaller} = minus m n

198198

199199--------------------------------------------------------------------------------

200−-- Type class implementations

200+-- Interface implementations

201201--------------------------------------------------------------------------------

202202

203203Eq Nat where

libs/prelude/Prelude/Pairs.idr+1−1

@@ -49,5 +49,5 @@ using (a : Type, P : a -> Type)

4949 getProof = snd

5050 %deprecate DPair.getProof "This is being deprecated in favour of `snd`."

5151

52− -- Polymorphic (class-based) projections have been removed

52+ -- Polymorphic (interface-based) projections have been removed

5353 -- because type-directed name disambiguation works better.

src/Idris/AbsSyntax.hs+5−5

@@ -434,9 +434,9 @@ pop_estack = do i <- getIState

434434 where ptail [] = []

435435 ptail (x : xs) = xs

436436

437−-- | Add a class instance function.

437+-- | Add an interface implementation function.

438438--

439−-- Precondition: the instance should have the correct type.

439+-- Precondition: the implementation should have the correct type.

440440--

441441-- Dodgy hack 1: Put integer instances first in the list so they are

442442-- resolved by default.

@@ -444,7 +444,7 @@ pop_estack = do i <- getIState

444444-- Dodgy hack 2: put constraint chasers (ParentN) last

445445addInstance :: Bool -- ^ whether the name is an Integer instance

446446 -> Bool -- ^ whether to include the instance in instance search

447− -> Name -- ^ the name of the class

447+ -> Name -- ^ the name of the interface

448448 -> Name -- ^ the name of the instance

449449 -> Idris ()

450450addInstance int res n i

@@ -1476,7 +1476,7 @@ addStatics n tm ptm =

14761476 freeArgNames tm = let (_, args) = unApply tm in

14771477 concatMap freeNames args

14781478

1479− -- if a name appears in a type class or tactic implicit index, it doesn't

1479+ -- if a name appears in an interface or tactic implicit index, it doesn't

14801480 -- affect its 'uniquely inferrable' from a static status since these are

14811481 -- resolved by searching.

14821482 searchArg (Constraint _ _) = True

@@ -1776,7 +1776,7 @@ addImplBoundInf ist ns inf = addImpl' False ns inf [] ist

17761776-- | Add the implicit arguments to applications in the term [Name]

17771777-- gives the names to always expend, even when under a binder of that

17781778-- name (this is to expand methods with implicit arguments in

1779−-- dependent type classes).

1779+-- dependent interfaces).

17801780addImpl :: [Name] -> IState -> PTerm -> PTerm

17811781addImpl = addImpl' False [] []

17821782

src/Idris/AbsSyntaxTree.hs+12−12

@@ -647,7 +647,7 @@ data FnOpt = Inlinable -- ^ always evaluate when simplifying

647647 | TotalFn | PartialFn | CoveringFn

648648 | Coinductive | AssertTotal

649649

650− -- | type class dictionary, eval only when a function

650+ -- | interface dictionary, eval only when a function

651651 -- argument, and further evaluation results.

652652 | Dictionary

653653 | Implicit -- ^ implicit coercion

@@ -684,7 +684,7 @@ data ProvideWhat' t = ProvTerm t t -- ^ the first is the goal type, the seco

684684type ProvideWhat = ProvideWhat' PTerm

685685

686686-- | Top-level declarations such as compiler directives, definitions,

687−-- datatypes and typeclasses.

687+-- datatypes and interfaces.

688688data PDecl' t

689689 -- | Fixity declaration

690690 = PFix FC Fixity [String]

@@ -717,13 +717,13 @@ data PDecl' t

717717 (Docstring (Either Err t)) -- Constructor doc

718718 SyntaxInfo -- Constructor SyntaxInfo

719719

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

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

720+ -- | Interface: arguments are documentation, syntax info, source

721+ -- location, constraints, interface name, interface name location,

722722 -- parameters, method declarations, optional constructor name

723723 | PInterface (Docstring (Either Err t)) SyntaxInfo FC

724724 [(Name, t)] -- constraints

725− Name -- class name

726− FC -- accurate location of class name

725+ Name -- interface name

726+ FC -- accurate location of interface name

727727 [(Name, FC, t)] -- parameters and precise locations

728728 [(Name, Docstring (Either Err t))] -- parameter docstrings

729729 [(Name, FC)] -- determining parameters and precise locations

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

732732 (Docstring (Either Err t)) -- instance constructor docs

733733

734734 -- | Instance declaration: arguments are documentation, syntax

735− -- info, source location, constraints, class name, parameters, full

735+ -- info, source location, constraints, interface name, parameters, full

736736 -- instance type, optional explicit name, and definitions

737737 | PInstance (Docstring (Either Err t)) -- Instance docs

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

@@ -741,8 +741,8 @@ data PDecl' t

741741 [Name] -- parent dictionaries to search for constraints

742742 Accessibility

743743 FnOpts

744− Name -- class

745− FC -- precise location of class

744+ Name -- interface

745+ FC -- precise location of interface

746746 [t] -- parameters

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

748748 t -- full instance type

@@ -1067,7 +1067,7 @@ data PTerm = PQuote Raw -- ^ Inclusion of a core term into the

10671067 | PIfThenElse FC PTerm PTerm PTerm -- ^ Conditional expressions - elaborated to an overloading of ifThenElse

10681068 | PCase FC PTerm [(PTerm, PTerm)] -- ^ A case expression. Args are source location, scrutinee, and a list of pattern/RHS pairs

10691069 | PTrue FC PunInfo -- ^ Unit type..?

1070− | PResolveTC FC -- ^ Solve this dictionary by type class resolution

1070+ | PResolveTC FC -- ^ Solve this dictionary by interface resolution

10711071 | PRewrite FC (Maybe Name) PTerm PTerm (Maybe PTerm)

10721072 -- ^ "rewrite" syntax, with optional rewriting function and

10731073 -- optional result type

@@ -1408,7 +1408,7 @@ highestFC (PRunElab fc _ _) = Just fc

14081408highestFC (PConstSugar fc _) = Just fc

14091409highestFC (PAppImpl t _) = highestFC t

14101410

1411−-- Type class data

1411+-- Interface data

14121412

14131413data InterfaceInfo = CI {

14141414 instanceCtorName :: Name

@@ -1581,7 +1581,7 @@ data SyntaxInfo = Syn {

15811581 , syn_namespace :: [String]

15821582 , no_imp :: [Name]

15831583 , imp_methods :: [Name]

1584− -- ^ class methods. When expanding implicits, these should be

1584+ -- ^ interface methods. When expanding implicits, these should be

15851585 -- expanded even under binders

15861586 , decoration :: Name -> Name

15871587 , inPattern :: Bool

src/Idris/Core/ProofState.hs+1−1

@@ -50,7 +50,7 @@ data ProofState = PS { thname :: Name,

5050 problems :: Fails,

5151 injective :: [Name],

5252 deferred :: [Name], -- ^ names we'll need to define

53− instances :: [Name], -- ^ instance arguments (for type classes)

53+ instances :: [Name], -- ^ instance arguments (for interfaces)

5454 autos :: [(Name, ([FailContext], [Name]))], -- ^ unsolved 'auto' implicits with their holes

5555 psnames :: [Name], -- ^ Local names okay to use in proof search

5656 previous :: Maybe ProofState, -- ^ for undo

src/Idris/Core/TT.hs+1−1

@@ -598,7 +598,7 @@ mapCtxt :: (a -> b) -> Ctxt a -> Ctxt b

598598mapCtxt = fmap . fmap

599599

600600-- |Return True if the argument 'Name' should be interpreted as the name of a

601−-- typeclass.

601+-- interface.

602602tcname (UN xs) = False

603603tcname (NS n _) = tcname n

604604tcname (SN (InstanceN _ _)) = True

src/Idris/Core/Unify.hs+3−3

@@ -460,7 +460,7 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

460460 substEnv ((n, t) : env) tm

461461 = substEnv env (substV (P Bound n (binderTy t)) tm)

462462

463− -- remove any unnecessary lambdas (helps with type class

463+ -- remove any unnecessary lambdas (helps with interface

464464 -- resolution later).

465465 eta ks (Bind n (Lam ty) sc) = eta ((n, ty) : ks) sc

466466 eta ks t = rebind ks t

@@ -488,8 +488,8 @@ unify ctxt env (topx, xfrom) (topy, yfrom) inj holes usersupp from =

488488-- un' env fn bnames (Bind x (PVTy _) sx) (Bind y (PVTy _) sy)

489489-- = un' env False ((x,y):bnames) sx sy

490490

491− -- f D unifies with t -> D. This is dubious, but it helps with type

492− -- class resolution for type classes over functions.

491+ -- f D unifies with t -> D. This is dubious, but it helps with

492+ -- interface resolution for interfaces over functions.

493493

494494 un' env fn bnames (App _ f x) (Bind n (Pi i t k) y)

495495 | noOccurrence n y && injectiveApp f

src/Idris/Docs.hs+9−9

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

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

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

4747 [FunDoc' d] -- data constructor 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

52− [PTerm] -- subclasses

53− [PTerm] -- superclasses

54− (Maybe (FunDoc' d)) -- explicit constructor

48+ | InterfaceDoc Name d -- interface 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

52+ [PTerm] -- sub interfaces

53+ [PTerm] -- super interfaces

54+ (Maybe (FunDoc' d)) -- explicit constructor

5555 | RecordDoc Name d -- record docs

5656 (FunDoc' d) -- data constructor docs

5757 [FunDoc' d] -- projection docs

5858 [(Name, PTerm, Maybe d)] -- parameters with type and doc

59− | NamedInstanceDoc Name (FunDoc' d) -- name is class

59+ | NamedInstanceDoc Name (FunDoc' d) -- name is interface

6060 | ModDoc [String] -- Module name

6161 d

6262 deriving Functor

@@ -101,7 +101,7 @@ pprintFD ist totalityFlag nsFlag (FD n doc args ty f) =

101101 <+> pprintPTerm ppo bnd [] infixes ty

102102 <> showDoc ist d

103103 <> line : showArgs args ((n, False):bnd)

104− showArgs ((n, ty, Constraint {}, Just d):args) bnd = -- Class constraints.

104+ showArgs ((n, ty, Constraint {}, Just d):args) bnd = -- Interface constraints.

105105 text "Class constraint"

106106 <+> pprintPTerm ppo bnd [] infixes ty

107107 <> showDoc ist d

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

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

11091109 addResolves ty (PApp fc f args) = PApp fc f (addResolvesArgs fc ty args)

11101110 addResolves ty tm = tm

11111111

1112− -- if an argument's type is a type class, and is otherwise to

1112+ -- if an argument's type is an interface, and is otherwise to

11131113 -- be inferred, then resolve it with instance search

11141114 -- This is something of a hack, because matching on the top level

11151115 -- application won't find this information for us

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

@@ -67,9 +67,9 @@ elabInstance :: ElabInfo

6767 -> [Name] -- ^ parent dictionary names (optionally)

6868 -> Accessibility

6969 -> FnOpts

70− -> Name -- ^ the class

71− -> FC -- ^ precise location of class name

72− -> [PTerm] -- ^ class parameters (i.e. instance)

70+ -> Name -- ^ the interface

71+ -> FC -- ^ precise location of interface name

72+ -> [PTerm] -- ^ interface parameters (i.e. instance)

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

7474 -> PTerm -- ^ full instance type

7575 -> Maybe Name -- ^ explicit name

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

233233 case lookupTy iname (tt_ctxt i) of

234234 [] -> elabFindOverlapping i ci iname syn t

235235 (_:_) -> return True

236− _ -> return False -- couldn't find class, just let elabInstance fail later

236+ _ -> return False -- couldn't find interface, just let elabInstance fail later

237237

238238 -- TODO: largely based upon elabType' - should try to abstract

239239 -- Issue #1614 in the issue tracker:

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

341341 coninsert cs ex sc = conbind cs (extrabind ex sc)

342342

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

344− -- class declaration (important so that we insert default definitions

344+ -- interface declaration (important so that we insert default definitions

345345 -- in the right place, and so that dependencies between methods are

346346 -- respected)

347347 reorderDefs :: [Name] -> [PDecl] -> [PDecl]

@@ -414,7 +414,7 @@ getTypeIn ist n tm = Placeholder

414414

415415toImp fc n = pimp n (PRef fc [] n) True

416416

417−-- | Propagate class parameters to method bodies, if they're not

417+-- | Propagate interface parameters to method bodies, if they're not

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

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

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

@@ -449,7 +449,7 @@ addParams ps (PClauses fc opts n cs) = PClauses fc opts n (map addCParams cs)

449449

450450addParams ps d = d

451451

452−-- | Check a given method definition is injective, if the class info

452+-- | Check a given method definition is injective, if the interface info

453453-- says it needs to be. Takes originally written decl and the one

454454-- with name decoration, so we know which name to look up.

455455checkInjectiveDef :: FC -> [(Name, (Bool, FnOpts, PTerm))] ->

src/Idris/Elab/Interface.hs+8−8

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

11{-|

2−Module : Idris.Elab.Class

2+Module : Idris.Elab.Interface

33Description : Code to elaborate interfaces.

44Copyright :

55License : BSD3

@@ -71,7 +71,7 @@ elabInterface :: ElabInfo

7171 -> [(Name, FC, PTerm)]

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

7373 -> [(Name, FC)] -- ^ determining params

74− -> [PDecl] -- ^ class body

74+ -> [PDecl] -- ^ interface body

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

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

7777 -> Idris ()

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

8888

8989 -- build data declaration

9090 let mdecls = filter tydecl ds -- method declarations

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

91+ let idecls = filter instdecl ds -- default super interface implementation declarations

9292 mapM_ checkDefaultSuperInterfaceInstance idecls

9393 let mnames = map getMName mdecls

9494 ist <- getIState

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

153153 pibind [] x = x

154154 pibind ((n, ty): ns) x = PPi expl n NoFC ty (pibind ns (chkUniq ty x))

155155

156− -- To make sure the type constructor of the class is in the appropriate

156+ -- To make sure the type constructor of the interface is in the appropriate

157157 -- uniqueness hierarchy

158158 chkUniq u@(PUniverse _ _) (PType _) = u

159159 chkUniq (PUniverse _ l) (PUniverse _ r) = PUniverse NoFC (min l r)

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

260260

261261 -- | Generate a top level function which looks up a method in a given

262262 -- dictionary (this is inlinable, always)

263− tfun :: Name -- ^ The name of the class

264− -> PTerm -- ^ A constraint for the class, to be inserted under the implicit bindings

263+ tfun :: Name -- ^ The name of the interface

264+ -> PTerm -- ^ A constraint for the interface, to be inserted under the implicit bindings

265265 -> SyntaxInfo -> [Name] -- ^ All the method names

266266 -> (Name, (Bool, FC, Docstring (Either Err PTerm), FnOpts, PTerm))

267267 -- ^ The present declaration

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

313313 where

314314 -- After we insert the constraint into the lookup, we need to

315315 -- ensure that the same dictionary is used to resolve lookups

316− -- to the other methods in the class

316+ -- to the other methods in the interface

317317 constrainMeths :: [Name] -> Name -> PTerm -> PTerm

318318 constrainMeths allM dictN tm = transform (addC allM dictN) tm

319319

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

322322 | otherwise = m

323323 addC _ _ tm = tm

324324

325− -- make arguments explicit and don't bind class parameters

325+ -- make arguments explicit and don't bind interface parameters

326326 toExp ns e (PPi (Imp l s p _ _) n fc ty sc)

327327 | n `elem` ns = toExp ns e sc

328328 | otherwise = PPi (e l s p) n fc ty (toExp ns e sc)

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

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

9292 hs <- get_holes

9393 ivs <- get_instances

9494 ptm <- get_term

95− -- Resolve remaining type classes. Two passes - first to get the

95+ -- Resolve remaining interfaces. Two passes - first to get the

9696 -- default Num instances, second to clean up the rest

9797 when (not pattern) $

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

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

152152 (h: hs) -> do patvar h; mkPat

153153 [] -> return ()

154154

155−-- | Build a term autogenerated as a typeclass method definition.

155+-- | Build a term autogenerated as an interface method definition.

156156--

157157-- (Separate, so we don't go overboard resolving things that we don't

158158-- know about yet on the LHS of a pattern def)

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

393393 TType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

394394 UType _ -> elab' ina (Just fc) (PRef fc [] unitTy)

395395 _ -> elab' ina (Just fc) (PRef fc [] unitCon)

396− elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent classes

396+ elab' ina fc (PResolveTC (FC "HACK" _ _)) -- for chasing parent interfaces

397397 = do g <- goal; resolveTC False False 5 g fn elabRec ist

398398 elab' ina fc (PResolveTC fc')

399399 = do c <- getNameFrom (sMN 0 "__class")

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

620620 let defined = case lookupTy n ctxt of

621621 [] -> False

622622 _ -> True

623− -- this is to stop us resolve type classes recursively

623+ -- this is to stop us resolve interfaces recursively

624624 -- trace (show (n, guarded)) $

625625 if (tcname n && ina && not intransform)

626626 then erun fc $

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

863863 else

864864 do ivs <- get_instances

865865 ps <- get_probs

866− -- HACK: we shouldn't resolve type classes if we're defining an instance

866+ -- HACK: we shouldn't resolve interfaces if we're defining an instance

867867 -- function or default definition.

868868 let isinf = f == inferCon || tcname f

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

869+ -- if f is an interface, we need to know its arguments so that

870870 -- we can unify with them

871871 case lookupCtxt f (idris_interfaces ist) of

872872 [] -> return ()

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

877877-- trace ("args is " ++ show args) $ return ()

878878 ns <- apply (Var f) (map isph args)

879879-- trace ("ns is " ++ show ns) $ return ()

880− -- mark any type class arguments as injective

880+ -- mark any interface arguments as injective

881881-- when (not pattern) $

882882 mapM_ checkIfInjective (map snd ns)

883883 unifyProblems -- try again with the new information,

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

914914 _ -> do solve

915915 hs <- get_holes

916916 ivs' <- get_instances

917− -- Attempt to resolve any type classes which have 'complete' types,

917+ -- Attempt to resolve any interfaces which have 'complete' types,

918918 -- i.e. no holes in them

919919 when (not pattern || (e_inarg ina && not tcgen)) $

920920 mapM_ (\n -> do focus n

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

963963 (P _ c _, args) ->

964964 case lookupCtxtExact c (idris_interfaces ist) of

965965 Nothing -> return ()

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

966+ Just ci -> -- interface, set as injective

967967 do mapM_ setinjArg (getDets 0 (interface_determiners ci) args)

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

969969 ulog <- getUnifyLog

@@ -1738,7 +1738,7 @@ pruneByType env (P _ n _) goalty ist as

17381738pruneByType _ t _ _ as = as

17391739

17401740-- Could the name feasibly be the return type?

1741−-- If there is a type class constraint on the return type, and no instance

1741+-- If there is an interface constraint on the return type, and no instance

17421742-- in the environment or globally for that name, then no

17431743-- Otherwise, yes

17441744-- (FIXME: This isn't complete, but I'm leaving it here and coming back

@@ -1809,7 +1809,7 @@ solveAutos ist fn ambigok

18091809 = do autos <- get_autos

18101810 mapM_ (solveAuto ist fn ambigok) (map (\(n, (fc, _)) -> (n, fc)) autos)

18111811

1812−-- Return true if the given error suggests a type class failure is

1812+-- Return true if the given error suggests an interface failure is

18131813-- recoverable

18141814tcRecoverable :: ElabMode -> Err -> Bool

18151815tcRecoverable ERHS (CantResolve f g _) = f

@@ -2820,7 +2820,7 @@ processTacticDecls info steps =

28202820 -- TODO: inaccessible

28212821

28222822 RAddInstance interfaceName instName ->

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

2823+ do -- The interface resolution machinery relies on a special

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

28252825 " for " ++ show interfaceName

28262826 addInstance False True interfaceName instName

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

@@ -185,7 +185,7 @@ decorateid decorate (PClauses f o n cs)

185185 dappname t = t

186186

187187

188−-- if 't' is a type class application, assume its arguments are injective

188+-- if 't' is an interface application, assume its arguments are injective

189189pbinds :: IState -> Term -> ElabD ()

190190pbinds i (Bind n (PVar t) sc)

191191 = do attack; patbind n

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

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

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

195195 [] -> return ()

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

196+ _ -> -- interface, set as injective

197197 mapM_ setinjArg args

198198 _ -> return ()

199199 pbinds i sc

src/Idris/IdrisDoc.hs+2−2

@@ -165,7 +165,7 @@ fetchInfo ist nss =

165165 filterContents p (NsInfo md ns) = NsInfo md (filter p ns)

166166 updateContents f x = x { nsContents = f (nsContents x) }

167167

168−-- | Removes loose class methods and data constructors,

168+-- | Removes loose interface methods and data constructors,

169169-- leaving them documented only under their parent.

170170removeOrphans :: [NsItem] -- ^ List to remove orphans from

171171 -> [NsItem] -- ^ Orphan-free list

@@ -577,7 +577,7 @@ createFunDoc ist fd@(FD name docstring args ftype fixity) = do

577577

578578

579579-- | Generates HTML documentation for any Docs type

580−-- TODO: Generate actual signatures for typeclasses

580+-- TODO: Generate actual signatures for interfaces

581581createOtherDoc :: IState -- ^ Needed to determine the types of names

582582 -> Docs -- ^ Namespace item to generate HTML block for

583583 -> H.Html -- ^ Resulting HTML

src/Idris/Interactive.hs+1−1

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

426426 -- Guess which binders should be implicits in the generated lemma.

427427 -- Make them implicit if they appear guarded by a top level constructor,

428428 -- or at the top level themselves.

429− -- Also, make type class instances implicit

429+ -- Also, make interface implementations implicit

430430 guessImps :: IState -> Context -> Term -> [Name]

431431 -- machine names aren't lifted

432432 guessImps ist ctxt (Bind n@(MN _ _) (Pi _ ty _) sc)

src/Idris/Parser.hs+9−9

@@ -179,7 +179,7 @@ Decl ::=

179179 | Params

180180 | Mutual

181181 | Namespace

182− | Class

182+ | Interface

183183 | Instance

184184 | DSL

185185 | Directive

@@ -316,7 +316,7 @@ declExtension syn ns rules =

316316

317317 -- Below is a lot of tedious boilerplate which updates any top level

318318 -- names in the declaration. It will only change names which are bound in

319− -- the declaration (including method names in classes and field names in

319+ -- the declaration (including method names in interfaces and field names in

320320 -- record declarations, not including pattern variables)

321321 updateB :: [(Name, SynMatch)] -> Name -> Name

322322 updateB ns (NS n mods) = NS (updateB ns n) mods

@@ -846,7 +846,7 @@ instanceBlock syn = do reservedHL "where"

846846 return (concat ds)

847847 <?> "implementation block"

848848

849−{-| Parses a methods and instances block (for type classes)

849+{-| Parses a methods and instances block (for interfaces)

850850

851851@

852852MethodOrInstance ::=

@@ -856,7 +856,7 @@ MethodOrInstance ::=

856856@

857857

858858@

859−ClassBlock ::=

859+InterfaceBlock ::=

860860 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock

861861 ;

862862@

@@ -886,18 +886,18 @@ interfaceBlock syn = do reservedHL "where"

886886 annotate :: SyntaxInfo -> IState -> Docstring () -> Docstring (Either Err PTerm)

887887 annotate syn ist = annotCode $ tryFullExpr syn ist

888888

889−{-| Parses a type class declaration

889+{-| Parses an interface declaration

890890

891891@

892−ClassArgument ::=

892+InterfaceArgument ::=

893893 Name

894894 | '(' Name ':' Expr ')'

895895 ;

896896@

897897

898898@

899−Class ::=

900− DocComment_t? Accessibility? 'class' ConstraintList? Name ClassArgument* ClassBlock?

899+Interface ::=

900+ DocComment_t? Accessibility? 'interface' ConstraintList? Name InterfaceArgument* InterfaceBlock?

901901 ;

902902@

903903-}

@@ -935,7 +935,7 @@ interface_ syn = do (doc, argDocs, acc)

935935 fc <- getFC

936936 return (i, ifc, PType fc)

937937

938−{-| Parses a type class instance declaration

938+{-| Parses an interface implementation declaration

939939

940940@

941941 Instance ::=

src/Idris/Parser/Expr.hs+1−1

@@ -740,7 +740,7 @@ implicitArg syn = do lchar '{'

740740 return (pimp n v True)

741741 <?> "implicit function argument"

742742

743−{-| Parses a constraint argument (for selecting a named type class instance)

743+{-| Parses a constraint argument (for selecting a named interface implementation)

744744

745745> ConstraintArg ::=

746746> '@{' Expr '}'

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

@@ -676,7 +676,7 @@ addAcc n a = do i <- get

676676 put (i { hide_list = addDef n a (hide_list i) })

677677

678678{- | Add accessbility option for data declarations

679− (works for classes too - 'abstract' means the data/class is visible but members not) -}

679+ (works for interfaces too - 'abstract' means the data/interface is visible but members not) -}

680680accData :: Accessibility -> Name -> [Name] -> IdrisParser ()

681681accData Frozen n ns = do addAcc n Public -- so that it can be used in public definitions

682682 mapM_ (\n -> addAcc n Private) ns -- so that they are invisible

src/Idris/PartialEval.hs+2−2

@@ -160,7 +160,7 @@ mkPE_TyDecl ist args ty = mkty args ty

160160 gen (App s f a) = App s <$> gen f <*> gen a

161161 gen tm = return tm

162162

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

163+-- | Checks if a given argument is an interface constraint argument

164164interfaceConstraint :: Idris.AbsSyntax.IState -> TT Name -> Bool

165165interfaceConstraint ist v

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

@@ -168,7 +168,7 @@ interfaceConstraint ist v

168168 _ -> False

169169 | otherwise = False

170170

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

171+-- | Checks if the given arguments of an interface constraint are all either constants

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

173173concreteInterface :: IState -> TT Name -> Bool

174174concreteInterface ist v

src/Idris/REPL.hs+1−1

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

929929 else do tclift $ tfail $ Msg ("Can't undefine " ++ show n ++ " because it wasn't defined at the repl")

930930 undefine' names already

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

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

932+ -- for now just assume it's an interface. Eventually we'll want some kind of

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

934934 fputState (ctxt_lookup n . known_interfaces) Nothing

935935 fmodifyState repl_definitions (delete n)

src/Idris/TypeSearch.hs+10−10

@@ -252,16 +252,16 @@ instance Monoid Score where

252252-- The 'Int' represents the position of the argument (1st argument, 2nd, etc.)

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

254254

255−-- | A list of typeclass constraints

255+-- | A list of interface constraints

256256type Interfaces = [(Name, Type)]

257257

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

259259data State = State

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

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

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

262+ -- ^ arguments and interface 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

265265 } deriving Show

266266

267267modifyTypes :: (Type -> Type) -> (ArgsDAG, Interfaces) -> (ArgsDAG, Interfaces)

@@ -477,11 +477,11 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

477477 -- the search tree. Once we advance in a phase, there should be no going back.

478478 nextSteps :: State -> [State]

479479

480− -- Stage 3 - match typeclasses

480+ -- Stage 3 - match interfaces

481481 nextSteps (State [] unresolved@(Sided ([], c1) ([], c2)) scoreAcc usedns) =

482482 if null results3 then results4 else results3

483483 where

484− -- try to match a typeclass argument from the left with a typeclass argument from the right

484+ -- try to match an interface argument from the left with an interface argument from the right

485485 results3 =

486486 catMaybes [ unifyQueue (State []

487487 (Sided ([], deleteFromArgList n1 c1)

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

489489 scoreAcc usedns) [(ty1, ty2)]

490490 | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

491491

492− -- try to hunt match a typeclass constraint by replacing it with an instance

492+ -- try to hunt match an interface constraint by replacing it with an instance

493493 results4 = [ State [] (both (\(cs, _, _) -> ([], cs)) sds)

494494 (scoreAcc `mappend` Score 0 0 (both (\(_, amods, _) -> amods) sds))

495495 (usedns ++ sided (++) (both (\(_, _, hs) -> hs) sds))

@@ -530,8 +530,8 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

530530

531531

532532

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

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

533+ -- Stage 2 - simply introduce a subset of the interfaces

534+ -- we've finished, so take some interfaces

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

536536 map statesFromMods . prod $ both (interfaceMods . snd) unresolved

537537 where

test/meta002/AgdaStyleReflection.idr+1−1

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

11||| Implement an Agda-style reflection system as a DSL inside of

2−||| Idris's reflected elaboration. Requires handling type class

2+||| Idris's reflected elaboration. Requires handling interface

33||| resolution and implicit arguments - some of the same features as

44||| the Idris elaborator itself.

55|||