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

docs/reference/compilation.rst+1−1

compare with master

unifiedsplit

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

68

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

70+ 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,

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

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

74+ 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.)

163* function arguments

164

165* data constructor fields (including record fields and dictionary

166− fields of class instances)

166+ fields of interface implementations)

167

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

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

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

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

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

297

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

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

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

301in the program.

docs/reference/misc.rst+1−1

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

275Existence of an instance

276========================

277

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

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

280

281.. code:: idris

docs/reference/repl.rst+27−17

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

240 Idris> :t plus 4

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

242

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

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

244

245::

246

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

268::

269

270 Idris> :doc (+)

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

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

272

273 infixl 8

274

275− Arguments:

275+ The function is Total

276− Class constraint Prelude.Classes.Num a

277− __pi_arg : a

278− __pi_arg1 : a

279

276

280::

277::

281

278

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

302::

299::

303

300

304 Idris> :doc Monad

301 Idris> :doc Monad

305− Interface Prelude.Monad.Monad

302+ Interface Monad

306− Methods:

303+

304+ Parameters:

305+ m

307

306

307+ Methods:

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

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

309+ Also called bind.

310+ infixl 5

309

311

310− infixl 5

312+ The function is Total

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

314+ Also called flatten or mu

311

315

312− Arguments:

316+ The function is Total

313− Class constraint Prelude.Monad.Monad m

317+ Implementations:

314− __pi_arg : m a

318+ Monad (IO' ffi)

315− __pi_arg1 : a -> m b

319+ Monad Stream

320+ Monad Provider

321+ Monad Elab

322+ Monad PrimIO

323+ Monad Maybe

324+ Monad (Either e)

325+ Monad List

316

326

317Finding things

327Finding things

318~~~~~~~~~~~~~~

328~~~~~~~~~~~~~~

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

382

392

383

393

384 Eq : Type -> Type

394 Eq : Type -> Type

385− The Eq class defines inequality and equality.

395+ The Eq interface defines inequality and equality.

386

396

387 GTE : Nat -> Nat -> Type

397 GTE : Nat -> Nat -> Type

388 Greater than or equal to

398 Greater than or equal to

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

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

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

427

437

428

438

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

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

430

440

431

441

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

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

433 ... (More results)

443 ... (More results)

434

444

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

445``: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

27 plus_i = User 6

28

29

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

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

31-- we can do:

32{-

33implementation 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,

2||| and Complex number types.

3module Control.Algebra.NumericInstances

4

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

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

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

3||| and `Control.Algebra.VectorSpace`.

4module Data.Matrix.Algebraic

5

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

23infixr 7 <&> -- matrix tensor product

24

25-----------------------------------------------------------------------

26−-- Vectors as members of algebraic classes

26+-- Vectors as members of algebraic interfaces

27-----------------------------------------------------------------------

28

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

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

146-- Matrix Algebra Properties

147-----------------------------------------------------------------------

148

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

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

3module Data.Matrix.Numeric

4

5import public Data.Matrix

libs/effects/Effects.idr+1−1

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

366 = let env' = unlabel env in

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

368

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

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

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

371-- so just brute force it.

372syntax MkDefaultEnv = with Env

libs/oldeffects/Effects.idr+2−2

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

24data EFFECT : Type where

25 MkEff : Type -> Effect -> EFFECT

26

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

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

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

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

30 ||| How to handle the effect.

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

235 = let env' = unlabel env in

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

237

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

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

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

240-- so just brute force it.

241syntax MkDefaultEnv = with Env

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

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

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

198

199--------------------------------------------------------------------------------

200−-- Type class implementations

200+-- Interface implementations

201--------------------------------------------------------------------------------

202

203Eq Nat where

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

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

49 getProof = snd

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

51

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

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

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

src/Idris/AbsSyntax.hs+5−5

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

434 where ptail [] = []

435 ptail (x : xs) = xs

436

437−-- | Add a class instance function.

437+-- | Add an interface implementation function.

438--

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

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

440--

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

442-- resolved by default.

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

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

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

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

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

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

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

449 -> Idris ()

450addInstance int res n i

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

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

1477 concatMap freeNames args

1478

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

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

1481 -- resolved by searching.

1482 searchArg (Constraint _ _) = True

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

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

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

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

1779−-- dependent type classes).

1779+-- dependent interfaces).

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

1781addImpl = addImpl' False [] []

1782

src/Idris/AbsSyntaxTree.hs+12−12

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

647 | TotalFn | PartialFn | CoveringFn

648 | Coinductive | AssertTotal

649

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

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

651 -- argument, and further evaluation results.

652 | Dictionary

653 | Implicit -- ^ implicit coercion

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

684type ProvideWhat = ProvideWhat' PTerm

685

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

687−-- datatypes and typeclasses.

687+-- datatypes and interfaces.

688data PDecl' t

689 -- | Fixity declaration

690 = PFix FC Fixity [String]

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

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

718 SyntaxInfo -- Constructor SyntaxInfo

719

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

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

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

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

722 -- parameters, method declarations, optional constructor name

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

724 [(Name, t)] -- constraints

725− Name -- class name

725+ Name -- interface name

726− FC -- accurate location of class name

726+ FC -- accurate location of interface name

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

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

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

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

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

733

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

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

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

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

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

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

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

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

742 Accessibility

743 FnOpts

744− Name -- class

744+ Name -- interface

745− FC -- precise location of class

745+ FC -- precise location of interface

746 [t] -- parameters

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

748 t -- full instance type

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

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

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

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

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

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

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

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

1073 -- optional result type

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

1408highestFC (PConstSugar fc _) = Just fc

1409highestFC (PAppImpl t _) = highestFC t

1410

1411−-- Type class data

1411+-- Interface data

1412

1413data InterfaceInfo = CI {

1414 instanceCtorName :: Name

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

1581 , syn_namespace :: [String]

1582 , no_imp :: [Name]

1583 , imp_methods :: [Name]

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

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

1585 -- expanded even under binders

1586 , decoration :: Name -> Name

1587 , inPattern :: Bool

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

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

50 problems :: Fails,

51 injective :: [Name],

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

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

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

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

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

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

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

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

598mapCtxt = fmap . fmap

599

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

601−-- typeclass.

601+-- interface.

602tcname (UN xs) = False

603tcname (NS n _) = tcname n

604tcname (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 =

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

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

462

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

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

464 -- resolution later).

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

466 eta ks t = rebind ks t

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

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

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

490

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

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

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

492+ -- interface resolution for interfaces over functions.

493

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

495 | noOccurrence n y && injectiveApp f

src/Idris/Docs.hs+9−9

@@ -45,18 +45,18 @@ 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− | InterfaceDoc Name d -- class docs

48+ | InterfaceDoc Name d -- interface docs

49− [FunDoc' d] -- method docs

49+ [FunDoc' d] -- method docs

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

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

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

52− [PTerm] -- subclasses

52+ [PTerm] -- sub interfaces

53− [PTerm] -- superclasses

53+ [PTerm] -- super interfaces

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

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

55 | RecordDoc Name d -- record docs

56 (FunDoc' d) -- data constructor docs

57 [FunDoc' d] -- projection docs

58 [(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

60 | ModDoc [String] -- Module name

61 d

62 deriving Functor

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

101 <+> pprintPTerm ppo bnd [] infixes ty

102 <> showDoc ist d

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

105 text "Class constraint"

106 <+> pprintPTerm ppo bnd [] infixes ty

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

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

1110 addResolves ty tm = tm

1111

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

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

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

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

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

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

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

68 -> Accessibility

69 -> FnOpts

70− -> Name -- ^ the class

70+ -> Name -- ^ the interface

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

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

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

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

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

74 -> PTerm -- ^ full instance type

75 -> Maybe Name -- ^ explicit name

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

233 case lookupTy iname (tt_ctxt i) of

234 [] -> elabFindOverlapping i ci iname syn t

235 (_:_) -> 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

237

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

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

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

342

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

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

346 -- respected)

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

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

414

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

416

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

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

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

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

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

449

450addParams ps d = d

451

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

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

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

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

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

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

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

1{-|

2−Module : Idris.Elab.Class

2+Module : Idris.Elab.Interface

3Description : Code to elaborate interfaces.

4Copyright :

5License : BSD3

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

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

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

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

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

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

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

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

77 -> Idris ()

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

88

89 -- build data declaration

90 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

92 mapM_ checkDefaultSuperInterfaceInstance idecls

93 let mnames = map getMName mdecls

94 ist <- getIState

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

153 pibind [] x = x

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

155

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

157 -- uniqueness hierarchy

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

159 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

260

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

262 -- dictionary (this is inlinable, always)

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

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

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

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

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

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

267 -- ^ The present declaration

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

313 where

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

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

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

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

319

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

322 | otherwise = m

323 addC _ _ tm = tm

324

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

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

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

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

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

92 hs <- get_holes

93 ivs <- get_instances

94 ptm <- get_term

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

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

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

97 when (not pattern) $

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

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

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

153 [] -> return ()

154

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

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

156--

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

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

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

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

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

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

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

398 elab' ina fc (PResolveTC fc')

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

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

620 let defined = case lookupTy n ctxt of

621 [] -> False

622 _ -> True

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

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

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

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

626 then erun fc $

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

863 else

864 do ivs <- get_instances

865 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

867 -- function or default definition.

868 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

870 -- we can unify with them

871 case lookupCtxt f (idris_interfaces ist) of

872 [] -> return ()

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

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

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

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

880− -- mark any type class arguments as injective

880+ -- mark any interface arguments as injective

881-- when (not pattern) $

882 mapM_ checkIfInjective (map snd ns)

883 unifyProblems -- try again with the new information,

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

914 _ -> do solve

915 hs <- get_holes

916 ivs' <- get_instances

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

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

918 -- i.e. no holes in them

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

920 mapM_ (\n -> do focus n

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

963 (P _ c _, args) ->

964 case lookupCtxtExact c (idris_interfaces ist) of

965 Nothing -> return ()

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

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

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

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

969 ulog <- getUnifyLog

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

1738pruneByType _ t _ _ as = as

1739

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

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

1743-- Otherwise, yes

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

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

1809 = do autos <- get_autos

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

1811

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

1813-- recoverable

1814tcRecoverable :: ElabMode -> Err -> Bool

1815tcRecoverable ERHS (CantResolve f g _) = f

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

2820 -- TODO: inaccessible

2821

2822 RAddInstance interfaceName instName ->

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

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

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

2825 " for " ++ show interfaceName

2826 addInstance False True interfaceName instName

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

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

185 dappname t = t

186

187

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

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

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

191 = do attack; patbind n

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

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

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

195 [] -> return ()

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

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

197 mapM_ setinjArg args

198 _ -> return ()

199 pbinds i sc

src/Idris/IdrisDoc.hs+2−2

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

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

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

167

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

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

169-- leaving them documented only under their parent.

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

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

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

577

578

579-- | Generates HTML documentation for any Docs type

580−-- TODO: Generate actual signatures for typeclasses

580+-- TODO: Generate actual signatures for interfaces

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

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

583 -> H.Html -- ^ Resulting HTML

src/Idris/Interactive.hs+1−1

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

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

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

428 -- or at the top level themselves.

429− -- Also, make type class instances implicit

429+ -- Also, make interface implementations implicit

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

431 -- machine names aren't lifted

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

src/Idris/Parser.hs+9−9

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

179 | Params

180 | Mutual

181 | Namespace

182− | Class

182+ | Interface

183 | Instance

184 | DSL

185 | Directive

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

316

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

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

320 -- record declarations, not including pattern variables)

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

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

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

846 return (concat ds)

847 <?> "implementation block"

848

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

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

850

851@

852MethodOrInstance ::=

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

856@

857

858@

859−ClassBlock ::=

859+InterfaceBlock ::=

860 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock

861 ;

862@

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

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

887 annotate syn ist = annotCode $ tryFullExpr syn ist

888

889−{-| Parses a type class declaration

889+{-| Parses an interface declaration

890

891@

892−ClassArgument ::=

892+InterfaceArgument ::=

893 Name

894 | '(' Name ':' Expr ')'

895 ;

896@

897

898@

899−Class ::=

899+Interface ::=

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

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

901 ;

902@

903-}

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

935 fc <- getFC

936 return (i, ifc, PType fc)

937

938−{-| Parses a type class instance declaration

938+{-| Parses an interface implementation declaration

939

940@

941 Instance ::=

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

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

740 return (pimp n v True)

741 <?> "implicit function argument"

742

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

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

744

745> ConstraintArg ::=

746> '@{' Expr '}'

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

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

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

677

678{- | 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) -}

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

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

682 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

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

161 gen tm = return tm

162

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

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

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

165interfaceConstraint ist v

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

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

168 _ -> False

169 | otherwise = False

170

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

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

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

174concreteInterface ist v

src/Idris/REPL.hs+1−1

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

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

930 undefine' names already

931 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

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

934 fputState (ctxt_lookup n . known_interfaces) Nothing

935 fmodifyState repl_definitions (delete n)

src/Idris/TypeSearch.hs+10−10

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

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

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

254

255−-- | A list of typeclass constraints

255+-- | A list of interface constraints

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

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

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

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

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

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

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

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

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

265 } deriving Show

266

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

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

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

478 nextSteps :: State -> [State]

479

480− -- Stage 3 - match typeclasses

480+ -- Stage 3 - match interfaces

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

482 if null results3 then results4 else results3

483 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

485 results3 =

486 catMaybes [ unifyQueue (State []

487 (Sided ([], deleteFromArgList n1 c1)

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

489 scoreAcc usedns) [(ty1, ty2)]

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

491

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

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

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

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

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

530

531

532

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

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

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

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

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

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

537 where

test/meta002/AgdaStyleReflection.idr+1−1

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

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

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

4||| the Idris elaborator itself.

5|||