0df1270 · Idris-dev · git.iko.soy

CHANGELOG.md+5−1

@@ -27,8 +27,12 @@

2727 `Prelude.File` and to provide a 'better' API.

2828* `natEnumFromThen` and `natEnumFromTo` have been updated to correctly calculate reverse ranges. Range syntax `[a,b..c]` now can be used again to generate reverse ranges.

2929* `divBN` and `modBN` now can only be used for unsigned numbers.

30−

3130* `return`, which has been an alias for `pure` for many releases, is now deprecated.

31+* Replace instance with implementation:

32+ + `InstanceN` is deprecated, use `ImplementationN` instead.

33+ + `InstanceCtorN` is deprecated, use `ImplementationCtorN` instead.

34+ + `addInstance` is deprecated, use `addImplementation` instead.

35+ + `%instance` keyword is deprecated, use `%implementation` instead.

3236

3337* Idris packages are now installed within a sub-directory `libs` of Idris' data directory, before they were installed in the directory's root.

3438

CONTRIBUTORS+1

@@ -53,3 +53,4 @@ Daniel Waterworth

5353Eric Weinstein

5454Jonas Westerlund

5555Björn Aili

56+Zheng Jihui

docs/guides/type-providers-ffi.rst+1−1

@@ -209,7 +209,7 @@ Next, an Idris file to define our providers:

209209 -- stat types.

210210 data BitWidth = B8 | B16 | B32 | B64

211211

212− instance Show BitWidth where

212+ implementation Show BitWidth where

213213 show B8 = "8 bits"

214214 show B16 = "16 bits"

215215 show B32 = "32 bits"

docs/proofs/pluscomm.rst+1−1

@@ -53,7 +53,7 @@ as follows:

5353.. code-block:: idris

5454

5555 data (=) : a -> b -> Type where

56− Refl : x = x

56+ Refl : x = x

5757

5858Note that this must be built-in, rather than defined in the library,

5959because ``=`` is a reserved operator — you cannot define this directly

docs/reference/compilation.rst+1−1

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

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

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

7171+ 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.

72++ Level 3: Provides details of compilation of the IRTS, erasure, parsing, case splitting, and further details elaboration of: Implementations, 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.

7575+ Level 6: Further details elaboration and coverage checking.

docs/reference/elaborator-reflection.rst+2−2

@@ -130,7 +130,7 @@ Some tactics may *fail*.

130130For example, ``intro`` will fail if the focused hole does not have a function type, ``solve`` will fail if the current hole does not contain a guess, and ``fill`` will fail if the term to be filled in has the wrong type.

131131Scripts can also fail explicitly using the ``fail`` tactic.

132132

133−To account for failure, there is an ``Alternative`` instance for ``Elab``.

133+To account for failure, there is an ``Alternative`` implementation for ``Elab``.

134134The ``<|>`` operator first tries the script to its left.

135135If that script fails, any changes that it made to the state are undone and the right argument is executed.

136136If the first argument succeeds, then the second argument is not executed.

@@ -172,7 +172,7 @@ Changing the Global Context

172172``Elab`` scripts can modify the global context during execution.

173173Just as the Idris elaborator produces auxiliary definitions to implement features such as ``where``-blocks and ``case`` expressions, user elaboration scripts may need to define functions.

174174Furthermore, this allows ``Elab`` reflection to be used to implement features such as interface deriving.

175−The operations ``declareType``, ``defineFunction``, and ``addInstance`` allow ``Elab`` scripts to modify the global context.

175+The operations ``declareType``, ``defineFunction``, and ``addImplementation`` allow ``Elab`` scripts to modify the global context.

176176

177177Using Idris's Features

178178======================

docs/reference/ffi.rst+1−1

@@ -47,7 +47,7 @@ the C FFI and ``JS_IO`` to use the JavaScript FFI:

4747 JS_IO a = IO' FFI_JS a

4848

4949As before, the entry point to an Idris program is ``main``, but the

50−type of ``main`` can now be any instance of ``IO'``, e.g. the

50+type of ``main`` can now be any implementation of ``IO'``, e.g. the

5151following are both valid:

5252

5353.. code-block:: idris

docs/reference/misc.rst+4−4

@@ -272,16 +272,16 @@ The latter could be shortened to the following:

272272That is, ``{x}`` behaves like ``{x=x}``.

273273

274274

275−Existence of an instance

275+Existence of an implementation

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

277277

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

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

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

279+type, one could use the ``%implementation`` keyword:

280280

281281.. code:: idris

282282

283283 foo : Num Nat

284− foo = %instance

284+ foo = %implementation

285285

286286'match' application

287287===================

idris.cabal+1−1

@@ -152,7 +152,7 @@ Library

152152 , Idris.Elab.Data

153153 , Idris.Elab.Record

154154 , Idris.Elab.Interface

155− , Idris.Elab.Instance

155+ , Idris.Elab.Implementation

156156 , Idris.Elab.Provider

157157 , Idris.Elab.RunElab

158158 , Idris.Elab.Transform

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

@@ -24,5 +24,5 @@ fromList l = SetWrapper (Data.SortedMap.fromList (map (\i => (i, ())) l))

2424toList : SortedSet k -> List k

2525toList (SetWrapper m) = map (\(i, _) => i) (Data.SortedMap.toList m)

2626

27−instance Foldable SortedSet where

27+implementation Foldable SortedSet where

2828 foldr f e xs = foldr f e (Data.SortedSet.toList xs)

libs/base/Language/Reflection/Utils.idr+13−13

@@ -87,12 +87,12 @@ mutual

8787 showPrec d (WhereN i n1 n2) = showCon d "WhereN" $ showArg i ++

8888 showArg n1 ++ showArg n2

8989 showPrec d (WithN i n) = showCon d "WithN" $ showArg i ++ showArg n

90− showPrec d (InstanceN i ss) = showCon d "InstanceN" $ showArg i ++ showArg ss

90+ showPrec d (ImplementationN i ss) = showCon d "ImplementationN" $ showArg i ++ showArg ss

9191 showPrec d (ParentN n s) = showCon d "ParentN" $ showArg n ++ showArg s

9292 showPrec d (MethodN n) = showCon d "MethodN" $ showArg n

9393 showPrec d (CaseN fc n) = showCon d "CaseN" $ showArg fc ++ showArg n

9494 showPrec d (ElimN n) = showCon d "ElimN" $ showArg n

95− showPrec d (InstanceCtorN n) = showCon d "InstanceCtorN" $ showArg n

95+ showPrec d (ImplementationCtorN n) = showCon d "ImplementationCtorN" $ showArg n

9696 showPrec d (MetaN parent meta) = showCon d "MetaN" $ showArg parent ++ showArg meta

9797

9898 implementation Show TTName where

@@ -110,16 +110,16 @@ mutual

110110 x == y = False

111111

112112 implementation Eq SpecialName where

113− (WhereN i n1 n2) == (WhereN i' n1' n2') = i == i' && n1 == n1' && n2 == n2'

114− (WithN i n) == (WithN i' n') = i == i' && n == n'

115− (InstanceN i ss) == (InstanceN i' ss') = i == i' && ss == ss'

116− (ParentN n s) == (ParentN n' s') = n == n' && s == s'

117− (MethodN n) == (MethodN n') = n == n'

118− (CaseN fc n) == (CaseN fc' n') = fc == fc' && n == n'

119− (ElimN n) == (ElimN n') = n == n'

120− (InstanceCtorN n) == (InstanceCtorN n') = n == n'

121− (MetaN parent meta) == (MetaN parent' meta') = parent == parent' && meta == meta'

122− _ == _ = False

113+ (WhereN i n1 n2) == (WhereN i' n1' n2') = i == i' && n1 == n1' && n2 == n2'

114+ (WithN i n) == (WithN i' n') = i == i' && n == n'

115+ (ImplementationN i ss) == (ImplementationN i' ss') = i == i' && ss == ss'

116+ (ParentN n s) == (ParentN n' s') = n == n' && s == s'

117+ (MethodN n) == (MethodN n') = n == n'

118+ (CaseN fc n) == (CaseN fc' n') = fc == fc' && n == n'

119+ (ElimN n) == (ElimN n') = n == n'

120+ (ImplementationCtorN n) == (ImplementationCtorN n') = n == n'

121+ (MetaN parent meta) == (MetaN parent' meta') = parent == parent' && meta == meta'

122+ _ == _ = False

123123

124124implementation Show TTUExp where

125125 showPrec d (UVar ns i) = showCon d "UVar" $ showArg ns ++ showArg i

@@ -347,7 +347,7 @@ pure : Raw -> Raw

347347pure = id

348348

349349--------------------------------------

350−-- Instances for definition reflection

350+-- Implementations for definition reflection

351351--------------------------------------

352352implementation Show Erasure where

353353 show Erased = "Erased"

libs/contrib/Control/Algebra/NumericInstances.idr → libs/contrib/Control/Algebra/NumericImplementations.idrrenamed+2−2

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

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

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

22||| and Complex number types.

3−module Control.Algebra.NumericInstances

3+module Control.Algebra.NumericImplementations

44

55import Control.Algebra

66import Control.Algebra.VectorSpace

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

@@ -5,7 +5,7 @@ module Data.Matrix.Algebraic

55

66import public Control.Algebra

77import public Control.Algebra.VectorSpace

8−import public Control.Algebra.NumericInstances

8+import public Control.Algebra.NumericImplementations

99

1010import public Data.Matrix

1111

libs/contrib/Decidable/Decidable.idr+1−1

@@ -9,7 +9,7 @@ import Data.Fun

99-- Interface for decidable n-ary Relations

1010--------------------------------------------------------------------------------

1111

12−-- Note: Instance resolution for Decidable is likely to not work in the REPL

12+-- Note: Implementation resolution for Decidable is likely to not work in the REPL

1313-- at the moment.

1414interface Decidable (ts : Vect k Type) (p : Rel ts) where

1515 total decide : liftRel ts p Dec

libs/contrib/contrib.ipkg+1−1

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

55

66 Control.Algebra,

77 Control.Algebra.Lattice, Control.Algebra.VectorSpace,

8− Control.Algebra.NumericInstances,

8+ Control.Algebra.NumericImplementations,

99 Control.Isomorphism.Primitives,

1010 Control.Partial,

1111

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

@@ -3,40 +3,40 @@ module Default

33interface Default a where

44 default : a

55

6−instance Default Int where

6+implementation Default Int where

77 default = 0

88

9−instance Default Integer where

9+implementation Default Integer where

1010 default = 0

1111

12−instance Default Double where

12+implementation Default Double where

1313 default = 0

1414

15−instance Default Nat where

15+implementation Default Nat where

1616 default = 0

1717

18−instance Default Char where

18+implementation Default Char where

1919 default = '\0'

2020

21−instance Default String where

21+implementation Default String where

2222 default = ""

2323

24−instance Default Bool where

24+implementation Default Bool where

2525 default = False

2626

27−instance Default () where

27+implementation Default () where

2828 default = ()

2929

30−instance (Default a, Default b) => Default (a, b) where

30+implementation (Default a, Default b) => Default (a, b) where

3131 default = (default, default)

3232

33−instance Default (Maybe a) where

33+implementation Default (Maybe a) where

3434 default = Nothing

3535

36−instance Default (List a) where

36+implementation Default (List a) where

3737 default = []

3838

39−instance Default a => Default (Vect n a) where

39+implementation Default a => Default (Vect n a) where

4040 default = mkDef _ where

4141 mkDef : (n : Nat) -> Vect n a

4242 mkDef Z = []

libs/oldeffects/Effect/Exception.idr+5−5

@@ -7,20 +7,20 @@ import Control.IOExcept

77data Exception : Type -> Effect where

88 Raise : a -> { () } Exception a b

99

10−instance Handler (Exception a) Maybe where

10+implementation Handler (Exception a) Maybe where

1111 handle _ (Raise e) k = Nothing

1212

13−instance Handler (Exception a) List where

13+implementation Handler (Exception a) List where

1414 handle _ (Raise e) k = []

1515

16−instance Show a => Handler (Exception a) IO where

16+implementation Show a => Handler (Exception a) IO where

1717 handle _ (Raise e) k = do printLn e

1818 believe_me (exit 1)

1919

20−instance Handler (Exception a) (IOExcept a) where

20+implementation Handler (Exception a) (IOExcept a) where

2121 handle _ (Raise e) k = ioM (pure (Left e))

2222

23−instance Handler (Exception a) (Either a) where

23+implementation Handler (Exception a) (Either a) where

2424 handle _ (Raise e) k = Left e

2525

2626EXCEPTION : Type -> EFFECT

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

@@ -73,7 +73,7 @@ data FileIO : Effect where

7373-- ------------------------------------------------------------ [ The Handlers ]

7474

7575--- An implementation of the resource access protocol for the IO Context.

76−instance Handler FileIO IO where

76+implementation Handler FileIO IO where

7777 handle () (Open fname m) k = do h <- openFile fname m

7878 valid <- validFile h

7979 if valid then k True (FH h)

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

@@ -77,7 +77,7 @@ do_poke ptr offset (b::bs)

7777 = do mkForeign (FFun "idris_poke" [FPtr, FInt, FByte] FUnit) ptr (fromInteger $ cast offset) b

7878 do_poke ptr (S offset) bs

7979

80−instance Handler RawMemory (IOExcept String) where

80+implementation Handler RawMemory (IOExcept String) where

8181 handle () (Allocate n) k

8282 = do ptr <- do_malloc n

8383 k () (CH ptr)

libs/oldeffects/Effect/Monad.idr+3−3

@@ -5,17 +5,17 @@ import Effects

55-- Eff is a monad too, so we can happily use it in a monad transformer.

66

77using (xs : List EFFECT, m : Type -> Type)

8− instance Functor (\a => EffM m a xs (\v => xs)) where

8+ implementation Functor (\a => EffM m a xs (\v => xs)) where

99 map f prog = do t <- prog

1010 value (f t)

1111

12− instance Applicative (\a => EffM m a xs (\v => xs)) where

12+ implementation Applicative (\a => EffM m a xs (\v => xs)) where

1313 pure = value

1414 (<*>) f a = do f' <- f

1515 a' <- a

1616 value (f' a')

1717

18− instance Monad (\a => Eff m a xs (\v => xs)) where

18+ implementation Monad (\a => Eff m a xs (\v => xs)) where

1919 (>>=) = Effects.(>>=)

2020

2121

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

@@ -7,7 +7,7 @@ data Random : Effect where

77 setSeed : Integer -> { Integer } Random ()

88

99using (m : Type -> Type)

10− instance Handler Random m where

10+ implementation Handler Random m where

1111 handle seed getRandom k

1212 = let seed' = assert_total ((1664525 * seed + 1013904223) `prim__sremBigInt` (pow 2 32)) in

1313 k seed' seed'

libs/oldeffects/Effect/Select.idr+2−2

@@ -5,14 +5,14 @@ import Effects

55data Selection : Effect where

66 Select : List a -> { () } Selection a

77

8−instance Handler Selection Maybe where

8+implementation Handler Selection Maybe where

99 handle _ (Select xs) k = tryAll xs where

1010 tryAll [] = Nothing

1111 tryAll (x :: xs) = case k x () of

1212 Nothing => tryAll xs

1313 Just v => Just v

1414

15−instance Handler Selection List where

15+implementation Handler Selection List where

1616 handle r (Select xs) k = concatMap (\x => k x r) xs

1717

1818SELECT : EFFECT

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

@@ -9,7 +9,7 @@ data State : Effect where

99 Put : b -> { a ==> b } State ()

1010

1111using (m : Type -> Type)

12− instance Handler State m where

12+ implementation Handler State m where

1313 handle st Get k = k st st

1414 handle st (Put n) k = k () n

1515

libs/oldeffects/Effect/StdIO.idr+2−2

@@ -19,13 +19,13 @@ data StdIO : Effect where

1919-- IO effects handlers

2020-------------------------------------------------------------

2121

22−instance Handler StdIO IO where

22+implementation Handler StdIO IO where

2323 handle () (PutStr s) k = do putStr s; k () ()

2424 handle () GetStr k = do x <- getLine; k x ()

2525 handle () (PutCh c) k = do putChar c; k () ()

2626 handle () GetCh k = do x <- getChar; k x ()

2727

28−instance Handler StdIO (IOExcept a) where

28+implementation Handler StdIO (IOExcept a) where

2929 handle () (PutStr s) k = do ioe_lift $ putStr s; k () ()

3030 handle () GetStr k = do x <- ioe_lift $ getLine; k x ()

3131 handle () (PutCh c) k = do ioe_lift $ putChar c; k () ()

libs/oldeffects/Effect/System.idr+2−2

@@ -13,13 +13,13 @@ data System : Effect where

1313 GetEnv : String -> { () } System (Maybe String)

1414 CSystem : String -> { () } System Int

1515

16−instance Handler System IO where

16+implementation Handler System IO where

1717 handle () Args k = do x <- getArgs; k x ()

1818 handle () Time k = do x <- time; k x ()

1919 handle () (GetEnv s) k = do x <- getEnv s; k x ()

2020 handle () (CSystem s) k = do x <- system s; k x ()

2121

22−instance Handler System (IOExcept a) where

22+implementation Handler System (IOExcept a) where

2323 handle () Args k = do x <- ioe_lift getArgs; k x ()

2424 handle () Time k = do x <- ioe_lift time; k x ()

2525 handle () (GetEnv s) k = do x <- ioe_lift $ getEnv s; k x ()

libs/oldeffects/Effects.idr+1−1

@@ -116,7 +116,7 @@ data LRes : lbl -> Type -> Type where

116116(:::) {lbl} x (MkEff r e) = MkEff (LRes x r) e

117117

118118using (lbl : Type)

119− instance Default a => Default (LRes lbl a) where

119+ implementation Default a => Default (LRes lbl a) where

120120 default = lbl := default

121121

122122private

libs/prelude/Language/Reflection.idr+95−82

@@ -65,15 +65,23 @@ mutual

6565

6666 data SpecialName = WhereN Int TTName TTName

6767 | WithN Int TTName

68− | InstanceN TTName (List String)

68+ | ImplementationN TTName (List String)

6969 | ParentN TTName String

7070 | MethodN TTName

7171 | CaseN SourceLocation TTName

7272 | ElimN TTName

73− | InstanceCtorN TTName

73+ | ImplementationCtorN TTName

7474 | MetaN TTName TTName

7575 %name SpecialName sn, sn'

7676

77+InstanceN : TTName -> (List String) -> SpecialName

78+InstanceN = ImplementationN

79+%deprecate InstanceN "`InstanceN` is deprecated, Please use `ImplementationN` instead."

80+

81+InstanceCtorN : TTName -> SpecialName

82+InstanceCtorN = ImplementationCtorN

83+%deprecate InstanceCtorN "`InstanceCtorN` is deprecated, Please use `ImplementationCtorN` instead."

84+

7785-- Rather than implement one-off private functions, we make the

7886-- disjointness of the constructors available to all Idris programs,

7987-- at the cost of a bit of scrolling here.

@@ -117,7 +125,7 @@ implementation Uninhabited (SN _ = NS _ _) where

117125implementation Uninhabited ((WhereN x n n') = (WithN y z)) where

118126 uninhabited Refl impossible

119127

120−implementation Uninhabited ((WhereN x n n') = (InstanceN y xs)) where

128+implementation Uninhabited ((WhereN x n n') = (ImplementationN y xs)) where

121129 uninhabited Refl impossible

122130

123131implementation Uninhabited ((WhereN x n n') = (ParentN y z)) where

@@ -132,7 +140,7 @@ implementation Uninhabited ((WhereN x n n') = (CaseN loc y)) where

132140implementation Uninhabited ((WhereN x n n') = (ElimN y)) where

133141 uninhabited Refl impossible

134142

135−implementation Uninhabited ((WhereN x n n') = (InstanceCtorN y)) where

143+implementation Uninhabited ((WhereN x n n') = (ImplementationCtorN y)) where

136144 uninhabited Refl impossible

137145

138146implementation Uninhabited ((WhereN x n n') = (MetaN y z)) where

@@ -141,7 +149,7 @@ implementation Uninhabited ((WhereN x n n') = (MetaN y z)) where

141149implementation Uninhabited ((WithN x n) = (WhereN y n' z)) where

142150 uninhabited Refl impossible

143151

144−implementation Uninhabited ((WithN x n) = (InstanceN n' xs)) where

152+implementation Uninhabited ((WithN x n) = (ImplementationN n' xs)) where

145153 uninhabited Refl impossible

146154

147155implementation Uninhabited ((WithN x n) = (ParentN n' y)) where

@@ -156,34 +164,34 @@ implementation Uninhabited ((WithN x n) = (CaseN loc n')) where

156164implementation Uninhabited ((WithN x n) = (ElimN n')) where

157165 uninhabited Refl impossible

158166

159−implementation Uninhabited ((WithN x n) = (InstanceCtorN n')) where

167+implementation Uninhabited ((WithN x n) = (ImplementationCtorN n')) where

160168 uninhabited Refl impossible

161169

162170implementation Uninhabited ((WithN x n) = (MetaN n' y)) where

163171 uninhabited Refl impossible

164172

165−implementation Uninhabited ((InstanceN n xs) = (WhereN x n' y)) where

173+implementation Uninhabited ((ImplementationN n xs) = (WhereN x n' y)) where

166174 uninhabited Refl impossible

167175

168−implementation Uninhabited ((InstanceN n xs) = (WithN x n')) where

176+implementation Uninhabited ((ImplementationN n xs) = (WithN x n')) where

169177 uninhabited Refl impossible

170178

171−implementation Uninhabited ((InstanceN n xs) = (ParentN n' x)) where

179+implementation Uninhabited ((ImplementationN n xs) = (ParentN n' x)) where

172180 uninhabited Refl impossible

173181

174−implementation Uninhabited ((InstanceN n xs) = (MethodN n')) where

182+implementation Uninhabited ((ImplementationN n xs) = (MethodN n')) where

175183 uninhabited Refl impossible

176184

177−implementation Uninhabited ((InstanceN n xs) = (CaseN loc n')) where

185+implementation Uninhabited ((ImplementationN n xs) = (CaseN loc n')) where

178186 uninhabited Refl impossible

179187

180−implementation Uninhabited ((InstanceN n xs) = (ElimN n')) where

188+implementation Uninhabited ((ImplementationN n xs) = (ElimN n')) where

181189 uninhabited Refl impossible

182190

183−implementation Uninhabited ((InstanceN n xs) = (InstanceCtorN n')) where

191+implementation Uninhabited ((ImplementationN n xs) = (ImplementationCtorN n')) where

184192 uninhabited Refl impossible

185193

186−implementation Uninhabited ((InstanceN n xs) = (MetaN n' x)) where

194+implementation Uninhabited ((ImplementationN n xs) = (MetaN n' x)) where

187195 uninhabited Refl impossible

188196

189197implementation Uninhabited ((ParentN n x) = (WhereN y n' z)) where

@@ -192,7 +200,7 @@ implementation Uninhabited ((ParentN n x) = (WhereN y n' z)) where

192200implementation Uninhabited ((ParentN n x) = (WithN y n')) where

193201 uninhabited Refl impossible

194202

195−implementation Uninhabited ((ParentN n x) = (InstanceN n' xs)) where

203+implementation Uninhabited ((ParentN n x) = (ImplementationN n' xs)) where

196204 uninhabited Refl impossible

197205

198206implementation Uninhabited ((ParentN n x) = (MethodN n')) where

@@ -204,7 +212,7 @@ implementation Uninhabited ((ParentN n x) = (CaseN loc n')) where

204212implementation Uninhabited ((ParentN n x) = (ElimN n')) where

205213 uninhabited Refl impossible

206214

207−implementation Uninhabited ((ParentN n x) = (InstanceCtorN n')) where

215+implementation Uninhabited ((ParentN n x) = (ImplementationCtorN n')) where

208216 uninhabited Refl impossible

209217

210218implementation Uninhabited ((ParentN n x) = (MetaN n' y)) where

@@ -216,7 +224,7 @@ implementation Uninhabited ((MethodN n) = (WhereN x n' y)) where

216224implementation Uninhabited ((MethodN n) = (WithN x n')) where

217225 uninhabited Refl impossible

218226

219−implementation Uninhabited ((MethodN n) = (InstanceN n' xs)) where

227+implementation Uninhabited ((MethodN n) = (ImplementationN n' xs)) where

220228 uninhabited Refl impossible

221229

222230implementation Uninhabited ((MethodN n) = (ParentN n' x)) where

@@ -228,7 +236,7 @@ implementation Uninhabited ((MethodN n) = (CaseN loc n')) where

228236implementation Uninhabited ((MethodN n) = (ElimN n')) where

229237 uninhabited Refl impossible

230238

231−implementation Uninhabited ((MethodN n) = (InstanceCtorN n')) where

239+implementation Uninhabited ((MethodN n) = (ImplementationCtorN n')) where

232240 uninhabited Refl impossible

233241

234242implementation Uninhabited ((MethodN n) = (MetaN n' x)) where

@@ -240,7 +248,7 @@ implementation Uninhabited ((CaseN loc n) = (WhereN x n' y)) where

240248implementation Uninhabited ((CaseN loc n) = (WithN x n')) where

241249 uninhabited Refl impossible

242250

243−implementation Uninhabited ((CaseN loc n) = (InstanceN n' xs)) where

251+implementation Uninhabited ((CaseN loc n) = (ImplementationN n' xs)) where

244252 uninhabited Refl impossible

245253

246254implementation Uninhabited ((CaseN loc n) = (ParentN n' x)) where

@@ -252,7 +260,7 @@ implementation Uninhabited ((CaseN loc n) = (MethodN n')) where

252260implementation Uninhabited ((CaseN loc n) = (ElimN n')) where

253261 uninhabited Refl impossible

254262

255−implementation Uninhabited ((CaseN loc n) = (InstanceCtorN n')) where

263+implementation Uninhabited ((CaseN loc n) = (ImplementationCtorN n')) where

256264 uninhabited Refl impossible

257265

258266implementation Uninhabited ((CaseN loc n) = (MetaN n' x)) where

@@ -264,7 +272,7 @@ implementation Uninhabited ((ElimN n) = (WhereN x n' y)) where

264272implementation Uninhabited ((ElimN n) = (WithN x n')) where

265273 uninhabited Refl impossible

266274

267−implementation Uninhabited ((ElimN n) = (InstanceN n' xs)) where

275+implementation Uninhabited ((ElimN n) = (ImplementationN n' xs)) where

268276 uninhabited Refl impossible

269277

270278implementation Uninhabited ((ElimN n) = (ParentN n' x)) where

@@ -276,34 +284,34 @@ implementation Uninhabited ((ElimN n) = (MethodN n')) where

276284implementation Uninhabited ((ElimN n) = (CaseN loc n')) where

277285 uninhabited Refl impossible

278286

279−implementation Uninhabited ((ElimN n) = (InstanceCtorN n')) where

287+implementation Uninhabited ((ElimN n) = (ImplementationCtorN n')) where

280288 uninhabited Refl impossible

281289

282290implementation Uninhabited ((ElimN n) = (MetaN n' x)) where

283291 uninhabited Refl impossible

284292

285−implementation Uninhabited ((InstanceCtorN n) = (WhereN x n' y)) where

293+implementation Uninhabited ((ImplementationCtorN n) = (WhereN x n' y)) where

286294 uninhabited Refl impossible

287295

288−implementation Uninhabited ((InstanceCtorN n) = (WithN x n')) where

296+implementation Uninhabited ((ImplementationCtorN n) = (WithN x n')) where

289297 uninhabited Refl impossible

290298

291−implementation Uninhabited ((InstanceCtorN n) = (InstanceN n' xs)) where

299+implementation Uninhabited ((ImplementationCtorN n) = (ImplementationN n' xs)) where

292300 uninhabited Refl impossible

293301

294−implementation Uninhabited ((InstanceCtorN n) = (ParentN n' x)) where

302+implementation Uninhabited ((ImplementationCtorN n) = (ParentN n' x)) where

295303 uninhabited Refl impossible

296304

297−implementation Uninhabited ((InstanceCtorN n) = (MethodN n')) where

305+implementation Uninhabited ((ImplementationCtorN n) = (MethodN n')) where

298306 uninhabited Refl impossible

299307

300−implementation Uninhabited ((InstanceCtorN n) = (CaseN loc n')) where

308+implementation Uninhabited ((ImplementationCtorN n) = (CaseN loc n')) where

301309 uninhabited Refl impossible

302310

303−implementation Uninhabited ((InstanceCtorN n) = (ElimN n')) where

311+implementation Uninhabited ((ImplementationCtorN n) = (ElimN n')) where

304312 uninhabited Refl impossible

305313

306−implementation Uninhabited ((InstanceCtorN n) = (MetaN n' x)) where

314+implementation Uninhabited ((ImplementationCtorN n) = (MetaN n' x)) where

307315 uninhabited Refl impossible

308316

309317implementation Uninhabited ((MetaN n n') = (WhereN x y z)) where

@@ -312,7 +320,7 @@ implementation Uninhabited ((MetaN n n') = (WhereN x y z)) where

312320implementation Uninhabited ((MetaN n n') = (WithN x y)) where

313321 uninhabited Refl impossible

314322

315−implementation Uninhabited ((MetaN n n') = (InstanceN x xs)) where

323+implementation Uninhabited ((MetaN n n') = (ImplementationN x xs)) where

316324 uninhabited Refl impossible

317325

318326implementation Uninhabited ((MetaN n n') = (ParentN x y)) where

@@ -327,7 +335,7 @@ implementation Uninhabited ((MetaN n n') = (CaseN loc x)) where

327335implementation Uninhabited ((MetaN n n') = (ElimN x)) where

328336 uninhabited Refl impossible

329337

330−implementation Uninhabited ((MetaN n n') = (InstanceCtorN x)) where

338+implementation Uninhabited ((MetaN n n') = (ImplementationCtorN x)) where

331339 uninhabited Refl impossible

332340

333341mutual

@@ -398,7 +406,12 @@ mutual

398406 private

399407 instanceNInj : (InstanceN n xs = InstanceN n' ys) -> (n = n', xs = ys)

400408 instanceNInj Refl = (Refl, Refl)

409+ %deprecate instanceNInj "`instanceNInj` is deprecated, Please use `implementationNInj` instead."

401410

411+ private

412+ implementationNInj : (ImplementationN n xs = ImplementationN n' ys) -> (n = n', xs = ys)

413+ implementationNInj Refl = (Refl, Refl)

414+

402415 private

403416 parentNInj : (ParentN n x = ParentN n' y) -> (n = n', x = y)

404417 parentNInj Refl = (Refl, Refl)

@@ -416,8 +429,8 @@ mutual

416429 elimNInj Refl = Refl

417430

418431 private

419− instanceCtorNInj : (InstanceCtorN n = InstanceCtorN n') -> n = n'

420− instanceCtorNInj Refl = Refl

432+ implementationCtorNInj : (ImplementationCtorN n = ImplementationCtorN n') -> n = n'

433+ implementationCtorNInj Refl = Refl

421434

422435 private

423436 metaNInj : (MetaN n m = MetaN n' m') -> (n = n', m = m')

@@ -437,12 +450,12 @@ mutual

437450 decSNEq (WhereN x n n') (WhereN y z w) | No contra =

438451 No $ contra . fst . whereNInj

439452 decSNEq (WhereN x n n') (WithN y z) = No absurd

440− decSNEq (WhereN x n n') (InstanceN y xs) = No absurd

453+ decSNEq (WhereN x n n') (ImplementationN y xs) = No absurd

441454 decSNEq (WhereN x n n') (ParentN y z) = No absurd

442455 decSNEq (WhereN x n n') (MethodN y) = No absurd

443456 decSNEq (WhereN x n n') (CaseN loc y) = No absurd

444457 decSNEq (WhereN x n n') (ElimN y) = No absurd

445− decSNEq (WhereN x n n') (InstanceCtorN y) = No absurd

458+ decSNEq (WhereN x n n') (ImplementationCtorN y) = No absurd

446459 decSNEq (WhereN x n n') (MetaN y z) = No absurd

447460 decSNEq (WithN x n) (WhereN y n' z) = No absurd

448461 decSNEq (WithN x n) (WithN y n') with (decEq x y)

@@ -453,32 +466,32 @@ mutual

453466 No $ contra . snd . withNInj

454467 decSNEq (WithN x n) (WithN y n') | No contra =

455468 No $ contra . fst . withNInj

456− decSNEq (WithN x n) (InstanceN n' xs) = No absurd

469+ decSNEq (WithN x n) (ImplementationN n' xs) = No absurd

457470 decSNEq (WithN x n) (ParentN n' y) = No absurd

458471 decSNEq (WithN x n) (MethodN n') = No absurd

459472 decSNEq (WithN x n) (CaseN loc n') = No absurd

460473 decSNEq (WithN x n) (ElimN n') = No absurd

461− decSNEq (WithN x n) (InstanceCtorN n') = No absurd

474+ decSNEq (WithN x n) (ImplementationCtorN n') = No absurd

462475 decSNEq (WithN x n) (MetaN n' y) = No absurd

463− decSNEq (InstanceN n xs) (WhereN x n' y) = No absurd

464− decSNEq (InstanceN n xs) (WithN x n') = No absurd

465− decSNEq (InstanceN n xs) (InstanceN n' ys) with (assert_total $ decTTNameEq n n')

466− decSNEq (InstanceN n xs) (InstanceN n ys) | Yes Refl with (decEq xs ys)

467− decSNEq (InstanceN n xs) (InstanceN n xs) | Yes Refl | Yes Refl =

476+ decSNEq (ImplementationN n xs) (WhereN x n' y) = No absurd

477+ decSNEq (ImplementationN n xs) (WithN x n') = No absurd

478+ decSNEq (ImplementationN n xs) (ImplementationN n' ys) with (assert_total $ decTTNameEq n n')

479+ decSNEq (ImplementationN n xs) (ImplementationN n ys) | Yes Refl with (decEq xs ys)

480+ decSNEq (ImplementationN n xs) (ImplementationN n xs) | Yes Refl | Yes Refl =

468481 Yes Refl

469− decSNEq (InstanceN n xs) (InstanceN n ys) | Yes Refl | No contra =

470− No $ contra . snd . instanceNInj

471− decSNEq (InstanceN n xs) (InstanceN n' ys) | No contra =

472− No $ contra . fst . instanceNInj

473− decSNEq (InstanceN n xs) (ParentN n' x) = No absurd

474− decSNEq (InstanceN n xs) (MethodN n') = No absurd

475− decSNEq (InstanceN n xs) (CaseN loc n') = No absurd

476− decSNEq (InstanceN n xs) (ElimN n') = No absurd

477− decSNEq (InstanceN n xs) (InstanceCtorN n') = No absurd

478− decSNEq (InstanceN n xs) (MetaN n' x) = No absurd

482+ decSNEq (ImplementationN n xs) (ImplementationN n ys) | Yes Refl | No contra =

483+ No $ contra . snd . implementationNInj

484+ decSNEq (ImplementationN n xs) (ImplementationN n' ys) | No contra =

485+ No $ contra . fst . implementationNInj

486+ decSNEq (ImplementationN n xs) (ParentN n' x) = No absurd

487+ decSNEq (ImplementationN n xs) (MethodN n') = No absurd

488+ decSNEq (ImplementationN n xs) (CaseN loc n') = No absurd

489+ decSNEq (ImplementationN n xs) (ElimN n') = No absurd

490+ decSNEq (ImplementationN n xs) (ImplementationCtorN n') = No absurd

491+ decSNEq (ImplementationN n xs) (MetaN n' x) = No absurd

479492 decSNEq (ParentN n x) (WhereN y n' z) = No absurd

480493 decSNEq (ParentN n x) (WithN y n') = No absurd

481− decSNEq (ParentN n x) (InstanceN n' xs) = No absurd

494+ decSNEq (ParentN n x) (ImplementationN n' xs) = No absurd

482495 decSNEq (ParentN n x) (ParentN n' y) with (assert_total $ decTTNameEq n n')

483496 decSNEq (ParentN n x) (ParentN n y) | Yes Refl with (decEq x y)

484497 decSNEq (ParentN n x) (ParentN n x) | Yes Refl | Yes Refl =

@@ -490,11 +503,11 @@ mutual

490503 decSNEq (ParentN n x) (MethodN n') = No absurd

491504 decSNEq (ParentN n x) (CaseN loc n') = No absurd

492505 decSNEq (ParentN n x) (ElimN n') = No absurd

493− decSNEq (ParentN n x) (InstanceCtorN n') = No absurd

506+ decSNEq (ParentN n x) (ImplementationCtorN n') = No absurd

494507 decSNEq (ParentN n x) (MetaN n' y) = No absurd

495508 decSNEq (MethodN n) (WhereN x n' y) = No absurd

496509 decSNEq (MethodN n) (WithN x n') = No absurd

497− decSNEq (MethodN n) (InstanceN n' xs) = No absurd

510+ decSNEq (MethodN n) (ImplementationN n' xs) = No absurd

498511 decSNEq (MethodN n) (ParentN n' x) = No absurd

499512 decSNEq (MethodN n) (MethodN n') with (assert_total $ decTTNameEq n n')

500513 decSNEq (MethodN n) (MethodN n) | Yes Refl =

@@ -503,11 +516,11 @@ mutual

503516 No $ contra . methodNInj

504517 decSNEq (MethodN n) (CaseN loc n') = No absurd

505518 decSNEq (MethodN n) (ElimN n') = No absurd

506− decSNEq (MethodN n) (InstanceCtorN n') = No absurd

519+ decSNEq (MethodN n) (ImplementationCtorN n') = No absurd

507520 decSNEq (MethodN n) (MetaN n' x) = No absurd

508521 decSNEq (CaseN loc n) (WhereN x n' y) = No absurd

509522 decSNEq (CaseN loc n) (WithN x n') = No absurd

510− decSNEq (CaseN loc n) (InstanceN n' xs) = No absurd

523+ decSNEq (CaseN loc n) (ImplementationN n' xs) = No absurd

511524 decSNEq (CaseN loc n) (ParentN n' x) = No absurd

512525 decSNEq (CaseN loc n) (MethodN n') = No absurd

513526 decSNEq (CaseN loc n) (CaseN loc' n') with (decEq loc loc')

@@ -519,11 +532,11 @@ mutual

519532 decSNEq (CaseN loc n) (CaseN loc' n') | No contra =

520533 No $ contra . fst . caseNInj

521534 decSNEq (CaseN loc n) (ElimN n') = No absurd

522− decSNEq (CaseN loc n) (InstanceCtorN n') = No absurd

535+ decSNEq (CaseN loc n) (ImplementationCtorN n') = No absurd

523536 decSNEq (CaseN loc n) (MetaN n' x) = No absurd

524537 decSNEq (ElimN n) (WhereN x n' y) = No absurd

525538 decSNEq (ElimN n) (WithN x n') = No absurd

526− decSNEq (ElimN n) (InstanceN n' xs) = No absurd

539+ decSNEq (ElimN n) (ImplementationN n' xs) = No absurd

527540 decSNEq (ElimN n) (ParentN n' x) = No absurd

528541 decSNEq (ElimN n) (MethodN n') = No absurd

529542 decSNEq (ElimN n) (CaseN loc n') = No absurd

@@ -532,29 +545,29 @@ mutual

532545 Yes Refl

533546 decSNEq (ElimN n) (ElimN n') | No contra =

534547 No $ contra . elimNInj

535− decSNEq (ElimN n) (InstanceCtorN n') = No absurd

548+ decSNEq (ElimN n) (ImplementationCtorN n') = No absurd

536549 decSNEq (ElimN n) (MetaN n' x) = No absurd

537− decSNEq (InstanceCtorN n) (WhereN x n' y) = No absurd

538− decSNEq (InstanceCtorN n) (WithN x n') = No absurd

539− decSNEq (InstanceCtorN n) (InstanceN n' xs) = No absurd

540− decSNEq (InstanceCtorN n) (ParentN n' x) = No absurd

541− decSNEq (InstanceCtorN n) (MethodN n') = No absurd

542− decSNEq (InstanceCtorN n) (CaseN loc n') = No absurd

543− decSNEq (InstanceCtorN n) (ElimN n') = No absurd

544− decSNEq (InstanceCtorN n) (InstanceCtorN n') with (assert_total $ decTTNameEq n n')

545− decSNEq (InstanceCtorN n) (InstanceCtorN n) | Yes Refl =

550+ decSNEq (ImplementationCtorN n) (WhereN x n' y) = No absurd

551+ decSNEq (ImplementationCtorN n) (WithN x n') = No absurd

552+ decSNEq (ImplementationCtorN n) (ImplementationN n' xs) = No absurd

553+ decSNEq (ImplementationCtorN n) (ParentN n' x) = No absurd

554+ decSNEq (ImplementationCtorN n) (MethodN n') = No absurd

555+ decSNEq (ImplementationCtorN n) (CaseN loc n') = No absurd

556+ decSNEq (ImplementationCtorN n) (ElimN n') = No absurd

557+ decSNEq (ImplementationCtorN n) (ImplementationCtorN n') with (assert_total $ decTTNameEq n n')

558+ decSNEq (ImplementationCtorN n) (ImplementationCtorN n) | Yes Refl =

546559 Yes Refl

547− decSNEq (InstanceCtorN n) (InstanceCtorN n') | No contra =

548− No $ contra . instanceCtorNInj

549− decSNEq (InstanceCtorN n) (MetaN n' x) = No absurd

560+ decSNEq (ImplementationCtorN n) (ImplementationCtorN n') | No contra =

561+ No $ contra . implementationCtorNInj

562+ decSNEq (ImplementationCtorN n) (MetaN n' x) = No absurd

550563 decSNEq (MetaN n n') (WhereN x y z) = No absurd

551564 decSNEq (MetaN n n') (WithN x y) = No absurd

552− decSNEq (MetaN n n') (InstanceN x xs) = No absurd

565+ decSNEq (MetaN n n') (ImplementationN x xs) = No absurd

553566 decSNEq (MetaN n n') (ParentN x y) = No absurd

554567 decSNEq (MetaN n n') (MethodN x) = No absurd

555568 decSNEq (MetaN n n') (CaseN loc x) = No absurd

556569 decSNEq (MetaN n n') (ElimN x) = No absurd

557− decSNEq (MetaN n n') (InstanceCtorN x) = No absurd

570+ decSNEq (MetaN n n') (ImplementationCtorN x) = No absurd

558571 decSNEq (MetaN n n') (MetaN x y) with (assert_total $ decTTNameEq n x)

559572 decSNEq (MetaN n n') (MetaN n y) | Yes Refl with (assert_total $ decTTNameEq n' y)

560573 decSNEq (MetaN n n') (MetaN n n') | Yes Refl | Yes Refl =

@@ -798,7 +811,7 @@ data Tactic =

798811 ||| Build a proof by applying contructors up to a maximum depth

799812 Search Int |

800813 ||| Resolve an interface

801− Instance |

814+ Implementation |

802815 ||| Infer the proof target from the context

803816 Solve |

804817 ||| introduce all variables into the context

@@ -995,12 +1008,12 @@ mutual

9951008 quotedTy = `(SpecialName)

9961009 quote (WhereN i n1 n2) = `(WhereN ~(quote i) ~(quote n1) ~(quote n2))

9971010 quote (WithN i n) = `(WithN ~(quote i) ~(quote n))

998− quote (InstanceN i ss) = `(InstanceN ~(quote i) ~(quote ss))

1011+ quote (ImplementationN i ss) = `(ImplementationN ~(quote i) ~(quote ss))

9991012 quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))

10001013 quote (MethodN n) = `(MethodN ~(quote n))

10011014 quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n))

10021015 quote (ElimN n) = `(ElimN ~(quote n))

1003− quote (InstanceCtorN n) = `(InstanceCtorN ~(quote n))

1016+ quote (ImplementationCtorN n) = `(ImplementationCtorN ~(quote n))

10041017 quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))

10051018

10061019mutual

@@ -1015,12 +1028,12 @@ mutual

10151028 quotedTy = `(SpecialName)

10161029 quote (WhereN i n1 n2) = `(WhereN ~(quote i) ~(quote n1) ~(quote n2))

10171030 quote (WithN i n) = `(WithN ~(quote i) ~(quote n))

1018− quote (InstanceN i ss) = `(InstanceN ~(quote i) ~(quote ss))

1031+ quote (ImplementationN i ss) = `(ImplementationN ~(quote i) ~(quote ss))

10191032 quote (ParentN n s) = `(ParentN ~(quote n) ~(quote s))

10201033 quote (MethodN n) = `(MethodN ~(quote n))

10211034 quote (CaseN fc n) = `(CaseN ~(quote fc) ~(quote n))

10221035 quote (ElimN n) = `(ElimN ~(quote n))

1023− quote (InstanceCtorN n) = `(InstanceCtorN ~(quote n))

1036+ quote (ImplementationCtorN n) = `(ImplementationCtorN ~(quote n))

10241037 quote (MetaN parent meta) = `(MetaN ~(quote parent) ~(quote meta))

10251038

10261039

@@ -1272,7 +1285,7 @@ implementation Quotable Tactic TT where

12721285 quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))

12731286 quote Trivial = `(Trivial)

12741287 quote (Search x) = `(Search ~(quote x))

1275− quote Instance = `(Instance)

1288+ quote Implementation = `(Implementation)

12761289 quote Solve = `(Solve)

12771290 quote Intros = `(Intros)

12781291 quote (Intro n) = `(Intro ~(quote n))

@@ -1302,7 +1315,7 @@ implementation Quotable Tactic Raw where

13021315 quote (Seq tac tac') = `(Seq ~(quote tac) ~(quote tac'))

13031316 quote Trivial = `(Trivial)

13041317 quote (Search x) = `(Search ~(quote x))

1305− quote Instance = `(Instance)

1318+ quote Implementation = `(Implementation)

13061319 quote Solve = `(Solve)

13071320 quote Intros = `(Intros)

13081321 quote (Intro n) = `(Intro ~(quote n))

libs/prelude/Language/Reflection/Elab.idr+9−4

@@ -182,7 +182,7 @@ data Elab : Type -> Type where

182182 Prim__DefineFunction : FunDefn Raw -> Elab ()

183183 Prim__DeclareDatatype : TyDecl -> Elab ()

184184 Prim__DefineDatatype : DataDefn -> Elab ()

185− Prim__AddInstance : TTName -> TTName -> Elab ()

185+ Prim__AddImplementation : TTName -> TTName -> Elab ()

186186 Prim__IsTCName : TTName -> Elab Bool

187187

188188 Prim__ResolveTC : TTName -> Elab ()

@@ -555,10 +555,15 @@ namespace Tactics

555555 ||| Register a new implementation for interface resolution.

556556 |||

557557 ||| @ ifaceName the name of the interface for which an implementation is being registered

558− ||| @ instName the name of the definition to use in implementation search

558+ ||| @ implName the name of the definition to use in implementation search

559559 export

560− addInstance : (ifaceName, instName : TTName) -> Elab ()

561− addInstance ifaceName instName = Prim__AddInstance ifaceName instName

560+ addImplementation : (ifaceName, implName : TTName) -> Elab ()

561+ addImplementation ifaceName implName = Prim__AddImplementation ifaceName implName

562+

563+ export

564+ addInstance : (ifaceName, implName : TTName) -> Elab ()

565+ addInstance = addImplementation

566+ %deprecate addInstance "`addInstance` is deprecated, Please use `addImplementation` instead."

562567

563568 ||| Determine whether a name denotes an interface.

564569 |||

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

@@ -89,7 +89,7 @@ maybeToEither def Nothing = Left def

8989

9090

9191--------------------------------------------------------------------------------

92−-- Instances

92+-- Implementations

9393--------------------------------------------------------------------------------

9494

9595(Eq a, Eq b) => Eq (Either a b) where

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

@@ -249,7 +249,7 @@ replicate Z x = []

249249replicate (S n) x = x :: replicate n x

250250

251251--------------------------------------------------------------------------------

252−-- Instances

252+-- Implementations

253253--------------------------------------------------------------------------------

254254

255255(Eq a) => Eq (List a) where

libs/pruviloj/Pruviloj/Derive/DecEq.idr+1−1

@@ -127,7 +127,7 @@ mkRhs fn fam k =

127127||| deriving to occur. It must consist of zero or more non-constraint

128128||| arguments followed by zero or more constraint arguments, followed

129129||| by the two values to compare. The constraint arguments must

130−||| provide sufficient instances of `DecEq` to decide the equality of

130+||| provide sufficient implementations of `DecEq` to decide the equality of

131131||| each constructor field. The final two arguments to the function

132132||| declaration must be the two values that will be compared for

133133||| equality.

samples/effects/Exception.idr+1−1

@@ -7,7 +7,7 @@ import Control.IOExcept

77

88data MyErr = NotANumber | OutOfRange

99

10−instance Show MyErr where

10+implementation Show MyErr where

1111 show NotANumber = "Not a number"

1212 show OutOfRange = "Out of range"

1313

samples/effects/TreeTag.idr+1−1

@@ -6,7 +6,7 @@ import Effect.State

66data BTree a = Leaf

77 | Node (BTree a) a (BTree a)

88

9−instance Show a => Show (BTree a) where

9+implementation Show a => Show (BTree a) where

1010 show Leaf = "[]"

1111 show (Node l x r) = "[" ++ show l ++ " "

1212 ++ show x ++ " "

samples/misc/binary.idr+2−2

@@ -4,7 +4,7 @@ data Bit : Nat -> Type where

44 b0 : Bit 0

55 b1 : Bit 1

66

7−instance Show (Bit n) where

7+implementation Show (Bit n) where

88 show b0 = "0"

99 show b1 = "1"

1010

@@ -14,7 +14,7 @@ data Binary : (width : Nat) -> (value : Nat) -> Type where

1414 zero : Binary Z Z

1515 (#) : Binary w v -> Bit bit -> Binary (S w) (bit + 2 * v)

1616

17−instance Show (Binary w k) where

17+implementation Show (Binary w k) where

1818 show zero = ""

1919 show (bin # bit) = show bin ++ show bit

2020

samples/misc/interp.idr+1−1

@@ -51,7 +51,7 @@ using (G : Vect n Ty)

5151 (<) : Expr G TyInt -> Expr G TyInt -> Expr G TyBool

5252 (<) = Op (<)

5353

54− instance Num (Expr G TyInt) where

54+ implementation Num (Expr G TyInt) where

5555 (+) x y = Op (+) x y

5656 (-) x y = Op (-) x y

5757 (*) x y = Op (*) x y

samples/misc/named_instance.lidr → samples/misc/named_implementation.lidrrenamed+5−5

@@ -1,17 +1,17 @@

11> module MyOrd

22

3−An alternative Ord instance for Nats, with an explicit name "myord"

3+An alternative Ord implementation for Nats, with an explicit name "myord"

44for the dictionary:

55

6−> instance [myord] Ord Nat where

6+> implementation [myord] Ord Nat where

77> compare O (S n) = GT

88> compare (S n) O = LT

99> compare O O = EQ

1010

1111The @{name} syntax below gives an explicit dictionary for the compare function.

1212Here, we're telling it to use the "myord" dictionary. Otherwise, it'd just

13−use the default (unnamed) instance. Note that there can only be one unnamed

14−instance --- they must not overlap.

13+use the default (unnamed) implementation. Note that there can only be one unnamed

14+implementation --- they must not overlap.

1515

1616> compare (S x) (S y) = compare @{myord} x y

1717

@@ -25,7 +25,7 @@ Sort foo using the default comparison operator:

2525

2626-- which gives [1,2,3,4,5,6,7,8]

2727

28−Sort foo using the alternative instance. No need for 'sortBy' and other

28+Sort foo using the alternative implementation. No need for 'sortBy' and other

2929such functions. Hoorah!

3030

3131> test2 : List Nat

samples/tutorial/binary.idr+1−1

@@ -5,7 +5,7 @@ data Binary : Nat -> Type where

55 bO : Binary n -> Binary (n + n)

66 bI : Binary n -> Binary (S (n + n))

77

8−instance Show (Binary n) where

8+implementation Show (Binary n) where

99 show (bO x) = show x ++ "0"

1010 show (bI x) = show x ++ "1"

1111 show bEnd = ""

samples/tutorial/idiom.idr+2−2

@@ -13,10 +13,10 @@ fetch x = MkEval fetchVal where

1313 fetchVal [] = Nothing

1414 fetchVal ((v, val) :: xs) = if (x == v) then (Just val) else (fetchVal xs)

1515

16−instance Functor Eval where

16+implementation Functor Eval where

1717 map f (MkEval g) = MkEval (\e => map f (g e))

1818

19−instance Applicative Eval where

19+implementation Applicative Eval where

2020 pure x = MkEval (\e => Just x)

2121

2222 (<*>) (MkEval f) (MkEval g) = MkEval (\x => app (f x) (g x)) where

src/IRTS/Compiler.hs+4−4

@@ -185,12 +185,12 @@ showCaseTrees = showSep "\n\n" . map showCT . sortBy (comparing defnRank)

185185

186186 snRank :: SpecialName -> String

187187 snRank (WhereN i n n') = "1" ++ nameRank n' ++ nameRank n ++ show i

188− snRank (InstanceN n args) = "2" ++ nameRank n ++ concatMap show args

188+ snRank (ImplementationN n args) = "2" ++ nameRank n ++ concatMap show args

189189 snRank (ParentN n s) = "3" ++ nameRank n ++ show s

190190 snRank (MethodN n) = "4" ++ nameRank n

191191 snRank (CaseN _ n) = "5" ++ nameRank n

192192 snRank (ElimN n) = "6" ++ nameRank n

193− snRank (InstanceCtorN n) = "7" ++ nameRank n

193+ snRank (ImplementationCtorN n) = "7" ++ nameRank n

194194 snRank (WithN i n) = "8" ++ nameRank n ++ show i

195195

196196isCon (TyDecl _ _) = True

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

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

629629 where

630630 methodVars = case n of

631− SN (InstanceCtorN interfaceName)

631+ SN (ImplementationCtorN interfaceName)

632632 -> M.fromList [(v, VI

633633 { viMethod = Just $ mkFieldName n i

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

635635 _

636− -> M.empty -- not an instance constructor

636+ -> M.empty -- not an implementation constructor

637637

638638irAlt top vs _ (ConstCase x rhs)

639639 | matchable x = LConstCase x <$> irSC top vs rhs

src/Idris/AbsSyntax.hs+25−25

@@ -424,9 +424,9 @@ getFragile n = do

424424 return $ lookupCtxtExact n (idris_fragile i)

425425

426426push_estack :: Name -> Bool -> Idris ()

427−push_estack n inst

427+push_estack n impl

428428 = do i <- getIState

429− putIState (i { elab_stack = (n, inst) : elab_stack i })

429+ putIState (i { elab_stack = (n, impl) : elab_stack i })

430430

431431pop_estack :: Idris ()

432432pop_estack = do i <- getIState

@@ -438,16 +438,16 @@ pop_estack = do i <- getIState

438438--

439439-- Precondition: the implementation should have the correct type.

440440--

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

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

442442-- resolved by default.

443443--

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

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

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

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

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

449− -> Idris ()

450−addInstance int res n i

445+addImplementation :: Bool -- ^ whether the name is an Integer implementation

446+ -> Bool -- ^ whether to include the implementation in implementation search

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

448+ -> Name -- ^ the name of the implementation

449+ -> Idris ()

450+addImplementation int res n i

451451 = do ist <- getIState

452452 case lookupCtxt n (idris_interfaces ist) of

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

@@ -467,7 +467,7 @@ addInstance int res n i

467467 chaser (NS n _) = chaser n

468468 chaser _ = False

469469

470−-- | Add a privileged implementation - one which instance search will

470+-- | Add a privileged implementation - one which implementation search will

471471-- happily resolve immediately if it is type correct This is used for

472472-- naming parent implementations when defining an implementation with

473473-- constraints. Returns the old list, so we can revert easily at the

@@ -497,7 +497,7 @@ addInterface :: Name -> InterfaceInfo -> Idris ()

497497addInterface n i

498498 = do ist <- getIState

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

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

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

501501 _ -> i

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

503503

@@ -1363,27 +1363,27 @@ expandParamsD rhs ist dec ps ns (PInterface doc info f cs n nfc params pDocs fds

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

13641364 cn

13651365 cd

1366−expandParamsD rhs ist dec ps ns (PInstance doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)

1366+expandParamsD rhs ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)

13671367 = let cn' = case cn of

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

13691369 Nothing -> Nothing in

1370− PInstance doc argDocs info f

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

1372− pnames acc opts n

1373− nfc

1374− (map (expandParams dec ps ns []) params)

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

1376− (expandParams dec ps ns [] ty)

1377− cn'

1378− (map (expandParamsD True ist dec ps ns) decls)

1370+ PImplementation doc argDocs info f

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

1372+ pnames acc opts n

1373+ nfc

1374+ (map (expandParams dec ps ns []) params)

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

1376+ (expandParams dec ps ns [] ty)

1377+ cn'

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

13791379expandParamsD rhs ist dec ps ns d = d

13801380

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

13821382

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

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

1385− ty cn decls

1386−expandInstanceScope ist dec ps ns d = d

1383+expandImplementationScope ist dec ps ns (PImplementation doc argDocs info f cs pnames acc opts n nfc params pextra ty cn decls)

1384+ = PImplementation doc argDocs info f cs pnames acc opts n nfc params (ps ++ pextra)

1385+ ty cn decls

1386+expandImplementationScope ist dec ps ns d = d

13871387

13881388-- | Calculate a priority for a type, for deciding elaboration order

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

src/Idris/AbsSyntaxTree.hs+41−41

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

298298 , idris_repl_defs :: [Name]

299299

300300 -- | Stack of names currently being elaborated, Bool set if it's an

301− -- instance (instances appear twice; also as a funtion name)

301+ -- implementation (implementations appear twice; also as a funtion name)

302302 , elab_stack :: [(Name, Bool)]

303303

304304

@@ -348,7 +348,7 @@ data IBCWrite = IBCFix FixDecl

348348 | IBCStatic Name

349349 | IBCInterface Name

350350 | IBCRecord Name

351− | IBCInstance Bool Bool Name Name

351+ | IBCImplementation Bool Bool Name Name

352352 | IBCDSL Name

353353 | IBCData Name

354354 | IBCOpt Name

@@ -722,26 +722,26 @@ data PDecl' t

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

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

724724 [PDecl' t] -- declarations

725− (Maybe (Name, FC)) -- instance constructor name and location

726− (Docstring (Either Err t)) -- instance constructor docs

725+ (Maybe (Name, FC)) -- implementation constructor name and location

726+ (Docstring (Either Err t)) -- implementation constructor docs

727727

728− -- | Instance declaration: arguments are documentation, syntax

728+ -- | Implementation declaration: arguments are documentation, syntax

729729 -- info, source location, constraints, interface name, parameters, full

730− -- instance type, optional explicit name, and definitions

731− | PInstance (Docstring (Either Err t)) -- Instance docs

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

733− SyntaxInfo

734− FC [(Name, t)] -- constraints

735− [Name] -- parent dictionaries to search for constraints

736− Accessibility

737− FnOpts

738− Name -- interface

739− FC -- precise location of interface

740− [t] -- parameters

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

742− t -- full instance type

743− (Maybe Name) -- explicit name

744− [PDecl' t]

730+ -- Implementation type, optional explicit name, and definitions

731+ | PImplementation (Docstring (Either Err t)) -- Implementation docs

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

733+ SyntaxInfo

734+ FC [(Name, t)] -- constraints

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

736+ Accessibility

737+ FnOpts

738+ Name -- interface

739+ FC -- precise location of interface

740+ [t] -- parameters

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

742+ t -- full Implementation type

743+ (Maybe Name) -- explicit name

744+ [PDecl' t]

745745 | PDSL Name (DSL' t) -- ^ DSL declaration

746746 | PSyntax FC Syntax -- ^ Syntax definition

747747 | PMutual FC [PDecl' t] -- ^ Mutual block

@@ -790,7 +790,7 @@ data Directive = DLib Codegen String

790790-- after a term elaboration when there's been reflected elaboration.

791791data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

792792 | RClausesInstrs Name [([(Name, Term)], Term, Term)]

793− | RAddInstance Name Name

793+ | RAddImplementation Name Name

794794 | RDatatypeDeclInstrs Name [PArg]

795795 -- | Datatype, constructors

796796 | RDatatypeDefnInstrs Name Type [(Name, [PArg], Type)]

@@ -912,14 +912,14 @@ mapPDeclFC f g (PInterface doc syn fc constrs n nfc params paramDocs det body ct

912912 (map (mapPDeclFC f g) body)

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

914914 ctorDoc

915−mapPDeclFC f g (PInstance doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra instTy instN body) =

916− PInstance doc paramDocs syn (f fc)

917− (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)

918− pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)

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

920− (mapPTermFC f g instTy)

921− instN

922− (map (mapPDeclFC f g) body)

915+mapPDeclFC f g (PImplementation doc paramDocs syn fc constrs pnames cn acc opts cnfc params pextra implTy implN body) =

916+ PImplementation doc paramDocs syn (f fc)

917+ (map (\(constrN, constrT) -> (constrN, mapPTermFC f g constrT)) constrs)

918+ pnames cn acc opts (g cnfc) (map (mapPTermFC f g) params)

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

920+ (mapPTermFC f g implTy)

921+ implN

922+ (map (mapPDeclFC f g) body)

923923mapPDeclFC f g (PDSL n dsl) = PDSL n (fmap (mapPTermFC f g) dsl)

924924mapPDeclFC f g (PSyntax fc syn) = PSyntax (f fc) $

925925 case syn of

@@ -957,7 +957,7 @@ declared (POpenInterfaces _ _ ds) = concatMap declared ds

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

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

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

960−declared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

960+declared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

961961 = case mn of

962962 Nothing -> []

963963 Just n -> [n]

@@ -981,7 +981,7 @@ tldeclared (POpenInterfaces _ _ ds) = concatMap tldeclared ds

981981tldeclared (PMutual _ ds) = concatMap tldeclared ds

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

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

984−tldeclared (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

984+tldeclared (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

985985 = case mn of

986986 Nothing -> []

987987 Just n -> [n]

@@ -1001,7 +1001,7 @@ defined (POpenInterfaces _ _ ds) = concatMap defined ds

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

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

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

1004−defined (PInstance _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

1004+defined (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ _ mn _)

10051005 = case mn of

10061006 Nothing -> []

10071007 Just n -> [n]

@@ -1202,7 +1202,7 @@ data PTactic' t = Intro [Name] | Intros | Focus Name

12021202 | Unfocus

12031203 | MatchRefine Name

12041204 | LetTac Name t | LetTacTy Name t t

1205− | Exact t | Compute | Trivial | TCInstance

1205+ | Exact t | Compute | Trivial | TCImplementation

12061206 | ProofSearch Bool Bool Int (Maybe Name)

12071207 [Name] -- allowed local names

12081208 [Name] -- hints

@@ -1262,7 +1262,7 @@ instance Sized a => Sized (PTactic' a) where

12621262 size Unfocus = 1

12631263 size (MatchRefine x) = 1 + size x

12641264 size (LetTacTy x y z) = 1 + size x + size y + size z

1265− size TCInstance = 1

1265+ size TCImplementation = 1

12661266

12671267type PTactic = PTactic' PTerm

12681268

@@ -1398,12 +1398,12 @@ highestFC (PAppImpl t _) = highestFC t

13981398-- Interface data

13991399

14001400data InterfaceInfo = CI {

1401− instanceCtorName :: Name

1401+ implementationCtorName :: Name

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

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

14041404 , interface_default_super_interfaces :: [PDecl]

14051405 , interface_params :: [Name]

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

1406+ , interface_implementations :: [(Name, Bool)] -- ^ the Bool is whether to include in implementation search, so named implementations are excluded

14071407 , interface_determiners :: [Int]

14081408 } deriving (Show, Generic)

14091409{-!

@@ -1514,7 +1514,7 @@ updateSyntaxRules rules (SyntaxRules sr) = SyntaxRules newRules

15141514 EQ -> ruleSort ss1 ss2

15151515 r -> r

15161516

1517− -- Better than creating Ord instance for SSymbol since

1517+ -- Better than creating Ord implementation for SSymbol since

15181518 -- in general this ordering does not really make sense.

15191519 symCompare (Keyword n1) (Keyword n2) = compare n1 n2

15201520 symCompare (Keyword _) _ = LT

@@ -1694,7 +1694,7 @@ piBindp p ((n, ty):ns) t = PPi p n NoFC ty (piBindp p ns t)

16941694

16951695-- Pretty-printing declarations and terms

16961696

1697−-- These "show" instances render to an absurdly wide screen because inserted line breaks

1697+-- These "show" implementations render to an absurdly wide screen because inserted line breaks

16981698-- could interfere with interactive editing, which calls "show".

16991699

17001700instance Show PTerm where

@@ -1761,7 +1761,7 @@ prettyImp :: PPOption -- ^ pretty printing options

17611761 -> Doc OutputAnnotation

17621762prettyImp impl = pprintPTerm impl [] [] []

17631763

1764−-- | Serialise something to base64 using its Binary instance.

1764+-- | Serialise something to base64 using its Binary implementation.

17651765

17661766-- | Do the right thing for rendering a term in an IState

17671767prettyIst :: IState -> PTerm -> Doc OutputAnnotation

@@ -1932,7 +1932,7 @@ pprintPTerm ppo bnd docArgs infixes = prettySe (ppopt_depth ppo) startPrec bnd

19321932 , kwd "else" <+> prettySe (decD d) startPrec bnd f

19331933 ]

19341934 prettySe d p bnd (PHidden tm) = text "." <> prettySe (decD d) funcAppPrec bnd tm

1935− prettySe d p bnd (PResolveTC _) = kwd "%instance"

1935+ prettySe d p bnd (PResolveTC _) = kwd "%implementation"

19361936 prettySe d p bnd (PTrue _ IsType) = annName unitTy $ text "()"

19371937 prettySe d p bnd (PTrue _ IsTerm) = annName unitCon $ text "()"

19381938 prettySe d p bnd (PTrue _ TypeOrTerm) = text "()"

@@ -2216,7 +2216,7 @@ showDeclImp o (PNamespace n fc ps) = text "namespace" <+> text n <> braces (lin

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

22172217showDeclImp o (PInterface _ _ _ cs n _ ps _ _ ds _ _)

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

2219−showDeclImp o (PInstance _ _ _ _ cs _ acc _ n _ _ _ t _ ds)

2219+showDeclImp o (PImplementation _ _ _ _ cs _ acc _ n _ _ _ t _ ds)

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

22212221showDeclImp _ _ = text "..."

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

src/Idris/Core/Binary.hs+6−6

@@ -342,9 +342,9 @@ instance Binary SpecialName where

342342 put x1

343343 put x2

344344 put x3

345− InstanceN x1 x2 -> do putWord8 1

346− put x1

347− put x2

345+ ImplementationN x1 x2 -> do putWord8 1

346+ put x1

347+ put x2

348348 ParentN x1 x2 -> do putWord8 2

349349 put x1

350350 put x2

@@ -352,7 +352,7 @@ instance Binary SpecialName where

352352 put x1

353353 CaseN x1 x2 -> do putWord8 4; put x1; put x2

354354 ElimN x1 -> do putWord8 5; put x1

355− InstanceCtorN x1 -> do putWord8 6; put x1

355+ ImplementationCtorN x1 -> do putWord8 6; put x1

356356 WithN x1 x2 -> do putWord8 7

357357 put x1

358358 put x2

@@ -368,7 +368,7 @@ instance Binary SpecialName where

368368 return (WhereN x1 x2 x3)

369369 1 -> do x1 <- get

370370 x2 <- get

371− return (InstanceN x1 x2)

371+ return (ImplementationN x1 x2)

372372 2 -> do x1 <- get

373373 x2 <- get

374374 return (ParentN x1 x2)

@@ -380,7 +380,7 @@ instance Binary SpecialName where

380380 5 -> do x1 <- get

381381 return (ElimN x1)

382382 6 -> do x1 <- get

383− return (InstanceCtorN x1)

383+ return (ImplementationCtorN x1)

384384 7 -> do x1 <- get

385385 x2 <- get

386386 return (WithN x1 x2)

src/Idris/Core/Elaborate.hs+11−11

@@ -329,10 +329,10 @@ checkInjective (tm, l, r) = do ctxt <- get_context

329329 isInj ctxt (Bind _ (Pi _ _ _) sc) = True

330330 isInj ctxt _ = False

331331

332−-- | get instance argument names

333−get_instances :: Elab' aux [Name]

334−get_instances = do ES p _ _ <- get

335− return $! (instances (fst p))

332+-- | get implementation argument names

333+get_implementations :: Elab' aux [Name]

334+get_implementations = do ES p _ _ <- get

335+ return $! (implementations (fst p))

336336

337337-- | get auto argument names

338338get_autos :: Elab' aux [(Name, ([FailContext], [Name]))]

@@ -539,8 +539,8 @@ defer ds n = do n' <- unique_hole n

539539deferType :: Name -> Raw -> [Name] -> Elab' aux ()

540540deferType n ty ns = processTactic' (DeferType n ty ns)

541541

542−instanceArg :: Name -> Elab' aux ()

543−instanceArg n = processTactic' (Instance n)

542+implementationArg :: Name -> Elab' aux ()

543+implementationArg n = processTactic' (Implementation n)

544544

545545autoArg :: Name -> Elab' aux ()

546546autoArg n = processTactic' (AutoArg n)

@@ -895,7 +895,7 @@ try' t1 t2 proofSearch

895895 = do s <- get

896896 ps <- get_probs

897897 ulog <- getUnifyLog

898− ivs <- get_instances

898+ ivs <- get_implementations

899899 case prunStateT 999999 False ps Nothing t1 s of

900900 OK ((v, _, _), s') -> do put s'

901901 return $! v

@@ -961,7 +961,7 @@ tryAll' constrok xs = doAll [] 999999 xs

961961 doAll cs pmax ((x, msg):xs)

962962 = do s <- get

963963 ps <- get_probs

964− ivs <- get_instances

964+ ivs <- get_implementations

965965 case prunStateT pmax True ps (if constrok then Nothing

966966 else Just ivs) x s of

967967 OK ((v, newps, probs), s') ->

@@ -986,7 +986,7 @@ prunStateT pmax zok ps ivs x s

986986 = case runStateT x s of

987987 OK (v, s'@(ES (p, _) _ _)) ->

988988 let newps = length (problems p) - length ps

989− ibad = badInstances (instances p) ivs

989+ ibad = badImplementations (implementations p) ivs

990990 newpmax = if newps < 0 then 0 else newps in

991991 if (newpmax > pmax || (not zok && newps > 0)) -- length ps == 0 && newpmax > 0))

992992 then case reverse (problems p) of

@@ -996,8 +996,8 @@ prunStateT pmax zok ps ivs x s

996996 else OK ((v, newpmax, problems p), s')

997997 Error e -> Error e

998998 where

999− badInstances _ Nothing = False

1000− badInstances inow (Just ithen) = length inow > length ithen

999+ badImplementations _ Nothing = False

1000+ badImplementations inow (Just ithen) = length inow > length ithen

10011001

10021002debugElaborator :: [ErrorReportPart] -> Elab' aux a

10031003debugElaborator msg = do ps <- fmap proof get

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

@@ -32,36 +32,36 @@ import Debug.Trace

3232

3333import Util.Pretty hiding (fill)

3434

35−data ProofState = PS { thname :: Name,

36− holes :: [Name], -- ^ holes still to be solved

37− usedns :: [Name], -- ^ used names, don't use again

38− nextname :: Int, -- ^ name supply, for locally unique names

39− global_nextname :: Int, -- ^ a mirror of the global name supply,

40− -- for generating things like type tags

41− -- in reflection

42− pterm :: ProofTerm, -- ^ current proof term

43− ptype :: Type, -- ^ original goal

44− dontunify :: [Name], -- ^ explicitly given by programmer, leave it

45− unified :: (Name, [(Name, Term)]),

46− notunified :: [(Name, Term)],

47− dotted :: [(Name, [Name])], -- ^ dot pattern holes + environment

48− -- either hole or something in env must turn up in the 'notunified' list during elaboration

49− solved :: Maybe (Name, Term),

50− problems :: Fails,

51− injective :: [Name],

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

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

57− context :: Context,

58− datatypes :: Ctxt TypeInfo,

59− plog :: String,

60− unifylog :: Bool,

61− done :: Bool,

62− recents :: [Name],

35+data ProofState = PS { thname :: Name,

36+ holes :: [Name], -- ^ holes still to be solved

37+ usedns :: [Name], -- ^ used names, don't use again

38+ nextname :: Int, -- ^ name supply, for locally unique names

39+ global_nextname :: Int, -- ^ a mirror of the global name supply,

40+ -- for generating things like type tags

41+ -- in reflection

42+ pterm :: ProofTerm, -- ^ current proof term

43+ ptype :: Type, -- ^ original goal

44+ dontunify :: [Name], -- ^ explicitly given by programmer, leave it

45+ unified :: (Name, [(Name, Term)]),

46+ notunified :: [(Name, Term)],

47+ dotted :: [(Name, [Name])], -- ^ dot pattern holes + environment

48+ -- either hole or something in env must turn up in the 'notunified' list during elaboration

49+ solved :: Maybe (Name, Term),

50+ problems :: Fails,

51+ injective :: [Name],

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

53+ implementations :: [Name], -- ^ implementation 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

57+ context :: Context,

58+ datatypes :: Ctxt TypeInfo,

59+ plog :: String,

60+ unifylog :: Bool,

61+ done :: Bool,

62+ recents :: [Name],

6363 while_elaborating :: [FailContext],

64− constraint_ns :: String

64+ constraint_ns :: String

6565 }

6666

6767data Tactic = Attack

@@ -98,7 +98,7 @@ data Tactic = Attack

9898 | Focus Name

9999 | Defer [Name] Name

100100 | DeferType Name Raw [Name]

101− | Instance Name

101+ | Implementation Name

102102 | AutoArg Name

103103 | SetInjective Name

104104 | MoveLast Name

@@ -431,14 +431,14 @@ movelast n ctxt env t = do action (\ps -> let hs = holes ps in

431431 else ps)

432432 return t

433433

434−instanceArg :: Name -> RunTactic

435−instanceArg n ctxt env (Bind x (Hole t) sc)

434+implementationArg :: Name -> RunTactic

435+implementationArg n ctxt env (Bind x (Hole t) sc)

436436 = do action (\ps -> let hs = holes ps

437− is = instances ps in

437+ is = implementations ps in

438438 ps { holes = (hs \\ [x]) ++ [x],

439− instances = x:is })

439+ implementations = x:is })

440440 return (Bind x (Hole t) sc)

441−instanceArg n ctxt env _

441+implementationArg n ctxt env _

442442 = fail "The current focus is not a hole."

443443

444444autoArg :: Name -> RunTactic

@@ -600,7 +600,7 @@ solve ctxt env (Bind x (Guess ty val) sc)

600600 notunified = updateNotunified [(x,val)]

601601 (notunified ps),

602602 recents = x : recents ps,

603− instances = instances ps \\ [x],

603+ implementations = implementations ps \\ [x],

604604 dotted = dropUnified dropdots (dotted ps) })

605605 let (locked, did) = tryLock (holes ps \\ [x]) (updsubst x val sc) in

606606 return locked

@@ -1148,7 +1148,7 @@ process t h = tactic (Just h) (mktac t)

11481148 mktac (Focus n) = focus n

11491149 mktac (Defer ns n) = defer ns n

11501150 mktac (DeferType n t a) = deferType n t a

1151− mktac (Instance n) = instanceArg n

1151+ mktac (Implementation n)= implementationArg n

11521152 mktac (AutoArg n) = autoArg n

11531153 mktac (SetInjective n) = setinj n

11541154 mktac (MoveLast n) = movelast n

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

@@ -45,7 +45,7 @@ module Idris.Core.TT(

4545 , pEraseType, pmap, pprintRaw, pprintTT, pprintTTClause, prettyEnv, psubst

4646 , pToV, pToVs, pureTerm, raw_apply, raw_unapply, refsIn, safeForget

4747 , safeForgetEnv, showCG, showEnv, showEnvDbg, showSep

48− , sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm

48+ , sImplementationN, sMN, sNS, spanFC, str, subst, substNames, substTerm

4949 , substV, sUN, tcname, termSmallerThan, tfail, thead, tnull

5050 , toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName

5151 , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm

@@ -497,20 +497,20 @@ deriving instance Binary Name

497497

498498data SpecialName = WhereN !Int !Name !Name

499499 | WithN !Int !Name

500− | InstanceN !Name [T.Text]

500+ | ImplementationN !Name [T.Text]

501501 | ParentN !Name !T.Text

502502 | MethodN !Name

503503 | CaseN !FC' !Name

504504 | ElimN !Name

505− | InstanceCtorN !Name

505+ | ImplementationCtorN !Name

506506 | MetaN !Name !Name

507507 deriving (Eq, Ord, Data, Generic, Typeable)

508508{-!

509509deriving instance Binary SpecialName

510510!-}

511511

512−sInstanceN :: Name -> [String] -> SpecialName

513−sInstanceN n ss = InstanceN n (map T.pack ss)

512+sImplementationN :: Name -> [String] -> SpecialName

513+sImplementationN n ss = ImplementationN n (map T.pack ss)

514514

515515sParentN :: Name -> String -> SpecialName

516516sParentN n s = ParentN n (T.pack s)

@@ -544,13 +544,13 @@ instance Show Name where

544544instance Show SpecialName where

545545 show (WhereN i p c) = show p ++ ", " ++ show c

546546 show (WithN i n) = "with block in " ++ show n

547− show (InstanceN cl inst) = showSep ", " (map T.unpack inst) ++ " implementation of " ++ show cl

547+ show (ImplementationN cl impl) = showSep ", " (map T.unpack impl) ++ " implementation of " ++ show cl

548548 show (MethodN m) = "method " ++ show m

549549 show (ParentN p c) = show p ++ "#" ++ T.unpack c

550550 show (CaseN fc n) = "case block in " ++ show n ++

551551 if fc == FC' emptyFC then "" else " at " ++ show fc

552552 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"

553− show (InstanceCtorN n) = "constructor of " ++ show n

553+ show (ImplementationCtorN n) = "constructor of " ++ show n

554554 show (MetaN parent meta) = "<<" ++ show parent ++ " " ++ show meta ++ ">>"

555555

556556-- Show a name in a way decorated for code generation, not human reading

@@ -562,12 +562,12 @@ showCG (MN i s) = "{" ++ T.unpack s ++ show i ++ "}"

562562showCG (SN s) = showCG' s

563563 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i

564564 showCG' (WithN i n) = "_" ++ showCG n ++ "_with_" ++ show i

565− showCG' (InstanceN cl inst) = '@':showCG cl ++ '$':showSep ":" (map T.unpack inst)

565+ showCG' (ImplementationN cl impl) = '@':showCG cl ++ '$':showSep ":" (map T.unpack impl)

566566 showCG' (MethodN m) = '!':showCG m

567567 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

568568 showCG' (CaseN fc c) = showCG c ++ showFC' fc ++ "_case"

569569 showCG' (ElimN sn) = showCG sn ++ "_elim"

570− showCG' (InstanceCtorN n) = showCG n ++ "_ictor"

570+ showCG' (ImplementationCtorN n) = showCG n ++ "_ictor"

571571 showCG' (MetaN parent meta) = showCG parent ++ "_meta_" ++ showCG meta

572572 showFC' (FC' NoFC) = ""

573573 showFC' (FC' (FileFC f)) = "_" ++ cgFN f

@@ -593,7 +593,7 @@ mapCtxt = fmap . fmap

593593-- interface.

594594tcname (UN xs) = False

595595tcname (NS n _) = tcname n

596−tcname (SN (InstanceN _ _)) = True

596+tcname (SN (ImplementationN _ _)) = True

597597tcname (SN (MethodN _)) = True

598598tcname (SN (ParentN _ _)) = True

599599tcname _ = False

@@ -838,7 +838,7 @@ instance Pretty Raw OutputAnnotation where

838838deriving instance Binary Raw

839839!-}

840840

841−data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool,

841+data ImplicitInfo = Impl { tcimplementation :: Bool, toplevel_imp :: Bool,

842842 machine_gen :: Bool }

843843 deriving (Show, Eq, Ord, Data, Generic, Typeable)

844844

@@ -1488,12 +1488,12 @@ nextName (SN x) = SN (nextName' x)

14881488 where

14891489 nextName' (WhereN i f x) = WhereN i f (nextName x)

14901490 nextName' (WithN i n) = WithN i (nextName n)

1491− nextName' (InstanceN n ns) = InstanceN (nextName n) ns

1491+ nextName' (ImplementationN n ns) = ImplementationN (nextName n) ns

14921492 nextName' (ParentN n ns) = ParentN (nextName n) ns

14931493 nextName' (CaseN fc n) = CaseN fc (nextName n)

14941494 nextName' (ElimN n) = ElimN (nextName n)

14951495 nextName' (MethodN n) = MethodN (nextName n)

1496− nextName' (InstanceCtorN n) = InstanceCtorN (nextName n)

1496+ nextName' (ImplementationCtorN n) = ImplementationCtorN (nextName n)

14971497 nextName' (MetaN parent meta) = MetaN parent (nextName meta)

14981498nextName (SymRef i) = error "Can't generate a name from a symbol reference"

14991499

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

@@ -193,13 +193,13 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

193193-- case boundVs (envPos x 0 env) tm of

194194-- [] -> return [(x, tm)]

195195-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))

196−-- (inst ns tm) (errEnv env))

196+-- (impl ns tm) (errEnv env))

197197 let v = highV (-1) tm in

198198 if v >= length ns

199199 then lift $ tfail (Msg "SCOPE ERROR")

200200 else return [(x, bind v ns tm)]

201− where inst [] tm = tm

202− inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

201+ where impl [] tm = tm

202+ impl ((n, _) : ns) tm = impl ns (substV (P Bound n Erased) tm)

203203

204204 bind i ns tm

205205 | i < 0 = tm

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

667667-- case boundVs (envPos x 0 env) tm of

668668-- [] -> return [(x, tm)]

669669-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))

670−-- (inst ns tm) (errEnv env))

670+-- (impl ns tm) (errEnv env))

671671 let v = highV (-1) tm in

672672 if v >= length ns

673673 then lift $ tfail (Msg "SCOPE ERROR")

674674 else return [(x, bind v ns tm)]

675− where inst [] tm = tm

676− inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

675+ where impl [] tm = tm

676+ impl (((n, _), _) : ns) tm = impl ns (substV (P Bound n Erased) tm)

677677 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

678678

679679 bind i ns tm

src/Idris/Delaborate.hs+1−1

@@ -142,7 +142,7 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

142142 | toplevel_imp impl -- information in 'imps' repeated

143143 = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)

144144 de env is (Bind n (Pi (Just impl) ty _) sc)

145− | tcinstance impl

145+ | tcimplementation impl

146146 = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

147147 | otherwise

148148 = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)

src/Idris/Docs.hs+39−39

@@ -48,7 +48,7 @@ data Docs' d = FunDoc (FunDoc' d)

4848 | InterfaceDoc Name d -- interface docs

4949 [FunDoc' d] -- method docs

5050 [(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)]))] -- implementations: name for named implementations, the constraint term, the docs

5252 [PTerm] -- sub interfaces

5353 [PTerm] -- super interfaces

5454 (Maybe (FunDoc' d)) -- explicit constructor

@@ -56,7 +56,7 @@ data Docs' d = FunDoc (FunDoc' d)

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 interface

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

6060 | ModDoc [String] -- Module name

6161 d

6262 deriving Functor

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

139139 if null args then text "No constructors."

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

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

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

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

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

144144 if nullDocstring doc

145145 then empty

@@ -157,33 +157,33 @@ pprintDocs ist (InterfaceDoc n doc meths params instances sub_interfaces super_i

157157 ctor

158158 <>

159159 nest 4 (text "Implementations:" <$>

160− vsep (if null instances then [text "<no implementations>"]

161− else map pprintInstance normalInstances))

160+ vsep (if null implementations then [text "<no implementations>"]

161+ else map pprintImplementation normalImplementations))

162162 <>

163− (if null namedInstances then empty

163+ (if null namedImplementations then empty

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

165− vsep (map pprintInstance namedInstances)))

165+ vsep (map pprintImplementation namedImplementations)))

166166 <>

167167 (if null sub_interfaces then empty

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

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

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

170170 <>

171171 (if null super_interfaces then empty

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

173− vsep (map dumpInstance super_interfaces)))

173+ vsep (map dumpImplementation super_interfaces)))

174174 where

175175 params' = zip pNames (repeat False)

176176

177− (normalInstances, namedInstances) = partition (\(n, _, _) -> not $ isJust n)

178− instances

177+ (normalImplementations, namedImplementations) = partition (\(n, _, _) -> not $ isJust n)

178+ implementations

179179

180180 pNames = map fst params

181181

182182 ppo = ppOptionIst ist

183183 infixes = idris_infixes ist

184184

185− pprintInstance (mname, term, (doc, argDocs)) =

186− nest 4 (iname mname <> dumpInstance term <>

185+ pprintImplementation (mname, term, (doc, argDocs)) =

186+ nest 4 (iname mname <> dumpImplementation term <>

187187 (if nullDocstring doc

188188 then empty

189189 else line <>

@@ -194,13 +194,13 @@ pprintDocs ist (InterfaceDoc n doc meths params instances sub_interfaces super_i

194194 doc) <>

195195 if null argDocs

196196 then empty

197− else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))

197+ else line <> vsep (map (prettyImplementationParam (map fst argDocs)) argDocs))

198198

199199

200200 iname Nothing = empty

201201 iname (Just n) = annName n <+> colon <> space

202202

203− prettyInstanceParam params (name, doc) =

203+ prettyImplementationParam params (name, doc) =

204204 if nullDocstring doc

205205 then empty

206206 else prettyName True False (zip params (repeat False)) name <+>

@@ -210,8 +210,8 @@ pprintDocs ist (InterfaceDoc n doc meths params instances sub_interfaces super_i

210210-- then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

211211-- else hsep (punctuate comma (map (prettyName True False params' . fst) params))

212212

213− dumpInstance :: PTerm -> Doc OutputAnnotation

214− dumpInstance = pprintPTerm ppo params' [] infixes

213+ dumpImplementation :: PTerm -> Doc OutputAnnotation

214+ dumpImplementation = pprintPTerm ppo params' [] infixes

215215

216216 prettifySubInterfaces (PPi (Constraint _ _) _ _ tm _) = prettifySubInterfaces tm

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

@@ -264,8 +264,8 @@ pprintDocs ist (RecordDoc n doc ctor projs params)

264264 else hsep (punctuate comma (map prettyParam [(n,pt) | (n,pt,_) <- params]))

265265 prettyParam (n,pt) = prettyName True False params' n <+> text ":" <+> pprintPTerm ppo params' [] infixes pt

266266

267−pprintDocs ist (NamedInstanceDoc _cls doc)

268− = nest 4 (text "Named instance:" <$> pprintFDWithoutTotality ist True doc)

267+pprintDocs ist (NamedImplementationDoc _cls doc)

268+ = nest 4 (text "Named implementation:" <$> pprintFDWithoutTotality ist True doc)

269269

270270pprintDocs ist (ModDoc mod docs)

271271 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

@@ -293,18 +293,18 @@ getDocs n w

293293 -> docRecord n ri

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

295295 -> docData n ti

296− | Just interface_ <- interfaceNameForInst i n

296+ | Just interface_ <- interfaceNameForImpl i n

297297 -> do fd <- docFun n

298− return $ NamedInstanceDoc interface_ fd

298+ return $ NamedImplementationDoc interface_ fd

299299 | otherwise

300300 -> do fd <- docFun n

301301 return (FunDoc fd)

302302 return $ fmap (howMuch w) docs

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

304− interfaceNameForInst ist n =

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

304+ interfaceNameForImpl ist n =

305305 listToMaybe [ cn

306306 | (cn, ci) <- toAlist (idris_interfaces ist)

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

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

308308 ]

309309

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

@@ -320,31 +320,31 @@ docInterface n ci

320320 docstr = maybe emptyDocstring fst docStrings

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

322322 (interface_params ci)

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

323+ docsForImplementation impl = fromMaybe (emptyDocstring, []) .

324324 flip lookupCtxtExact (idris_docstrings i) $

325− inst

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

327− delabTy i inst,

328− docsForInstance inst))

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

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

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

325+ impl

326+ implementations = map (\impl -> (namedImpl impl,

327+ delabTy i impl,

328+ docsForImplementation impl))

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

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

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

332332 mdocs <- mapM (docFun . fst) (interface_methods ci)

333− let ctorN = instanceCtorName ci

333+ let ctorN = implementationCtorName ci

334334 ctorDocs <- case basename ctorN of

335335 SN _ -> return Nothing

336336 _ -> fmap Just $ docFun ctorN

337337 return $ InterfaceDoc

338338 n docstr mdocs params

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

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

340340 ctorDocs

341341 where

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

343− namedInst n@(UN _) = Just n

344− namedInst _ = Nothing

342+ namedImpl (NS n ns) = fmap (flip NS ns) (namedImpl n)

343+ namedImpl n@(UN _) = Just n

344+ namedImpl _ = Nothing

345345

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

347− getDInst _ = Nothing

346+ getDImpl (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t

347+ getDImpl _ = Nothing

348348

349349 isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))

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

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

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

666666

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

668668 let wb = map (mkStatic static_names) $

669− map (expandInstanceScope ist decorate newargs defs) $

669+ map (expandImplementationScope ist decorate newargs defs) $

670670 map (expandParamsD False ist decorate newargs defs) whereblock

671671

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

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

11101110 addResolves ty tm = tm

11111111

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

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

1113+ -- be inferred, then resolve it with implementation search

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

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

11161116 addResolvesArgs :: FC -> Term -> [PArg] -> [PArg]

src/Idris/Elab/Instance.hs → src/Idris/Elab/Implementation.hsrenamed+44−46

@@ -1,12 +1,12 @@

11{-|

2−Module : Idris.Elab.Instance

2+Module : Idris.Elab.Implementation

33Description : Code to elaborate instances.

44Copyright :

55License : BSD3

66Maintainer : The Idris Community.

77-}

88{-# LANGUAGE PatternGuards #-}

9−module Idris.Elab.Instance(elabInstance) where

9+module Idris.Elab.Implementation(elabImplementation) where

1010

1111import Idris.AbsSyntax

1212import Idris.ASTUtils

@@ -57,25 +57,25 @@ import Data.List.Split (splitOn)

5757

5858import Util.Pretty(pretty, text)

5959

60−elabInstance :: ElabInfo

61− -> SyntaxInfo

62− -> Docstring (Either Err PTerm)

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

64− -> ElabWhat -- ^ phase

65− -> FC

66− -> [(Name, PTerm)] -- ^ constraints

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

68− -> Accessibility

69− -> FnOpts

70− -> Name -- ^ the interface

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

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

76− -> [PDecl]

77− -> Idris ()

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

60+elabImplementation :: ElabInfo

61+ -> SyntaxInfo

62+ -> Docstring (Either Err PTerm)

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

64+ -> ElabWhat -- ^ phase

65+ -> FC

66+ -> [(Name, PTerm)] -- ^ constraints

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

68+ -> Accessibility

69+ -> FnOpts

70+ -> Name -- ^ the interface

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

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

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

74+ -> PTerm -- ^ full implementation type

75+ -> Maybe Name -- ^ explicit name

76+ -> [PDecl]

77+ -> Idris ()

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

7979 ist <- getIState

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

8181 [c] -> return c

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

9393 when (what /= EDefns) $ do

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

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

96+ -- if the implementation type matches any of the implementations we have already,

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

9898 case expn of

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

100− (map fst $ interface_instances ci)

101− addInstance intInst True n iname

102− Just _ -> addInstance intInst False n iname

100+ (map fst $ interface_implementations ci)

101+ addImplementation intImpl True n iname

102+ Just _ -> addImplementation intImpl False n iname

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

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

105105 oldOpen <- addOpenImpl parents

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

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

119119 concatMap (namesIn [] ist) ps

120120

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

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

123− mapM_ (rec_elabDecl info EAll info) undefinedSuperInterfaceInstances

121+ let superInterfaceImplementations = map (substImplementation ips pnames) (interface_default_super_interfaces ci)

122+ undefinedSuperInterfaceImplementations <- filterM (fmap not . isOverlapping ist) superInterfaceImplementations

123+ mapM_ (rec_elabDecl info EAll info) undefinedSuperInterfaceImplementations

124124

125125 ist <- getIState

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

126+ -- Bring variables in implementation head into scope when building the

127127 -- dictionary

128128 let headVars = nub $ concatMap getHeadVars ps

129129 let (headVarTypes, ty)

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

159159 let wb = wbTys ++ wbVals

160160

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

162− logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++

163− show (concat (nub wparams))

164−

162+ logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))

165163

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

167165

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

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

167+ let rhs = PApp fc (PRef fc [] (implementationCtorName ci))

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

171169

172− logElab 5 $ "Instance LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars

173− logElab 5 $ "Instance RHS " ++ show rhs

170+ logElab 5 $ "Implementation LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars

171+ logElab 5 $ "Implementation RHS " ++ show rhs

174172

175173 push_estack iname True

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

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

207205-- totalityCheckBlock

208206

209207 checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))

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

208+ addIBC (IBCImplementation intImpl (isNothing expn) n iname)

211209

212210 where

213− intInst = case ps of

211+ intImpl = case ps of

214212 [PConstant NoFC (AType (ATInt ITNative))] -> True

215213 _ -> False

216214

217215 mkiname n' ns ps' expn' =

218216 case expn' of

219217 Nothing -> case ns of

220− [] -> SN (sInstanceN n' (map show ps'))

221− m -> sNS (SN (sInstanceN n' (map show ps'))) m

218+ [] -> SN (sImplementationN n' (map show ps'))

219+ m -> sNS (SN (sImplementationN n' (map show ps'))) m

222220 Just nm -> nm

223221

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

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

222+ substImplementation ips pnames (PImplementation doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)

223+ = PImplementation doc argDocs syn fc cs parents acc opts n nfc

226224 (map (substMatchesShadow ips pnames) ps)

227225 pextra

228226 (substMatchesShadow ips pnames t) expn ds

229227

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

228+ isOverlapping i (PImplementation doc argDocs syn _ _ _ _ _ n nfc ps pextra t expn _)

231229 = case lookupCtxtName n (idris_interfaces i) of

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

233231 case lookupTy iname (tt_ctxt i) of

234232 [] -> elabFindOverlapping i ci iname syn t

235233 (_:_) -> return True

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

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

237235

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

239237 -- Issue #1614 in the issue tracker:

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

255253 ctxt <- getContext

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

257255 let nty = normalise ctxt [] cty

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

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

259257

260258 findOverlapping i dets t n

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

@@ -393,7 +391,7 @@ getHeadVars (PPair _ _ _ l r) = getHeadVars l ++ getHeadVars r

393391getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t

394392getHeadVars _ = []

395393

396−-- | Implicitly bind variables from the instance head in method types

394+-- | Implicitly bind variables from the implementation head in method types

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

398396impBind vs (PTy d ds syn fc opts n fc' t)

399397 = PTy d ds syn fc opts n fc'

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

@@ -62,21 +62,21 @@ import Util.Pretty(pretty, text)

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

6363

6464elabInterface :: ElabInfo

65− -> SyntaxInfo

66− -> Docstring (Either Err PTerm)

67− -> FC

68− -> [(Name, PTerm)]

69− -> Name

70− -> FC

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

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

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

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

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

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

77− -> Idris ()

65+ -> SyntaxInfo

66+ -> Docstring (Either Err PTerm)

67+ -> FC

68+ -> [(Name, PTerm)]

69+ -> Name

70+ -> FC

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

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

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

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

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

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

77+ -> Idris ()

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

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

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

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

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

8282 (map (pexp . PRef fc []) (map (\(n, _, _) -> n) ps))

@@ -88,8 +88,8 @@ 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 super interface implementation declarations

92− mapM_ checkDefaultSuperInterfaceInstance idecls

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

92+ mapM_ checkDefaultSuperInterfaceImplementation idecls

9393 let mnames = map getMName mdecls

9494 ist <- getIState

9595 let constraintNames = nub $

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

105105 = unzip (map (\ (x, y, z) -> (x, y)) ims)

106106 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

107107

108− -- build instance constructor type

108+ -- build implementation constructor type

109109 let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints

110110 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

111111 constraint

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

161161 chkUniq _ t = t

162162

163163 -- TODO: probably should normalise

164− checkDefaultSuperInterfaceInstance :: PDecl -> Idris ()

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

164+ checkDefaultSuperInterfaceImplementation :: PDecl -> Idris ()

165+ checkDefaultSuperInterfaceImplementation (PImplementation _ _ _ fc cs _ _ _ n _ ps _ _ _ _)

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

167167 $ tfail (At fc (Msg "Default super interface implementations can't have constraints."))

168168 i <- getIState

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

229229 tydecl (PTy{}) = True

230230 tydecl (PData _ _ _ _ _ _) = True

231231 tydecl _ = False

232− instdecl (PInstance{}) = True

233− instdecl _ = False

232+ impldecl (PImplementation{}) = True

233+ impldecl _ = False

234234 clause (PClauses{}) = True

235235 clause _ = False

236236

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

252252 let conn' = case lookupCtxtName conn (idris_interfaces i) of

253253 [(n, _)] -> n

254254 _ -> conn

255− addInstance False True conn' cfn

256− addIBC (IBCInstance False True conn' cfn)

255+ addImplementation False True conn' cfn

256+ addIBC (IBCImplementation False True conn' cfn)

257257-- iputStrLn ("Added " ++ show (conn, cfn, ty))

258258 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,

259259 PClauses fc [Inlinable, Dictionary] cfn [PClause fc cfn lhs [] rhs []]]

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

@@ -90,17 +90,17 @@ build ist info emode opts fn tm

9090 _ -> False

9191

9292 hs <- get_holes

93− ivs <- get_instances

93+ ivs <- get_implementations

9494 ptm <- get_term

9595 -- Resolve remaining interfaces. Two passes - first to get the

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

96+ -- default Num implementations, second to clean up the rest

9797 when (not pattern) $

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

9999 do focus n

100100 g <- goal

101101 try (resolveTC' True True 10 g fn ist)

102102 (movelast n)) ivs

103− ivs <- get_instances

103+ ivs <- get_implementations

104104 hs <- get_holes

105105 when (not pattern) $

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

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

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

398398 elab' ina fc (PResolveTC fc')

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

400− instanceArg c

400+ implementationArg c

401401 -- Elaborate the equality type first homogeneously, then

402402 -- heterogeneously as a fallback

403403 elab' ina _ (PApp fc (PRef _ _ n) args)

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

721721 highlightSource nfc (AnnBoundName n False)

722722 elab' ina _ tm@(PLet fc n nfc ty val sc)

723723 = do attack

724− ivs <- get_instances

724+ ivs <- get_implementations

725725 tyn <- getNameFrom (sMN 0 "letty")

726726 claim tyn RType

727727 valn <- getNameFrom (sMN 0 "letval")

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

738738 focus valn

739739 elabE (ina { e_inarg = True, e_intype = True })

740740 (Just fc) val

741− ivs' <- get_instances

741+ ivs' <- get_implementations

742742 env <- get_env

743743 elabE (ina { e_inarg = True }) (Just fc) sc

744744 when (not (pattern || intransform)) $

@@ -861,9 +861,9 @@ elab ist info emode opts fn tm

861861 (ffc, annot) : map (\f -> (f, annot)) hls

862862 return []

863863 else

864− do ivs <- get_instances

864+ do ivs <- get_implementations

865865 ps <- get_probs

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

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

867867 -- function or default definition.

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

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

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

913913 rs@(_:_) | not pattern -> return rs -- quit, try again

914914 _ -> do solve

915915 hs <- get_holes

916− ivs' <- get_instances

916+ ivs' <- get_implementations

917917 -- 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)) $

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

14731473 fullApp x = x

14741474

14751475 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1476− | tcinstance i && not (toplevel_imp i)

1476+ | tcimplementation i && not (toplevel_imp i)

14771477 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

14781478 | not (toplevel_imp i)

14791479 = pimp n Placeholder True : insertScopedImps fc sc xs

@@ -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 an interface constraint on the return type, and no instance

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

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

@@ -1756,7 +1756,7 @@ isPlausible ist var env n ty

17561756 = let tcs' = case unApply ty of

17571757 (P _ c _, _) ->

17581758 case lookupCtxtExact c (idris_interfaces ist) of

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

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

17601760 : tcs)

17611761 Nothing -> tcs

17621762 _ -> tcs

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

23192319 -- the rest happens in a bit

23202320 updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }

23212321 returnUnit

2322− | n == tacN "Prim__AddInstance"

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

2322+ | n == tacN "Prim__AddImplementation"

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

23242324 interfaceName <- reifyTTName cls

2325− instName <- reifyTTName inst

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

2325+ implName <- reifyTTName impl

2326+ updateAux $ \e -> e { new_tyDecls = RAddImplementation interfaceName implName :

23272327 new_tyDecls e }

23282328 returnUnit

23292329 | n == tacN "Prim__IsTCName"

@@ -2549,7 +2549,7 @@ runTac autoSolve ist perhapsFC fn tac

25492549 when autoSolve solveAll

25502550 runT Compute = compute

25512551 runT Trivial = do trivial' ist; when autoSolve solveAll

2552− runT TCInstance = runT (Exact (PResolveTC emptyFC))

2552+ runT TCImplementation = runT (Exact (PResolveTC emptyFC))

25532553 runT (ProofSearch rec prover depth top psns hints)

25542554 = do proofSearch' ist rec False depth prover top fn psns hints

25552555 when autoSolve solveAll

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

28192819 _ -> return ()

28202820 -- TODO: inaccessible

28212821

2822− RAddInstance interfaceName instName ->

2822+ RAddImplementation interfaceName implName ->

28232823 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

2827− addIBC (IBCInstance False True interfaceName instName)

2824+ logElab 2 $ "Adding elab script implementation " ++ show implName ++

2825+ " for " ++ show interfaceName

2826+ addImplementation False True interfaceName implName

2827+ addIBC (IBCImplementation False True interfaceName implName)

28282828 RClausesInstrs n cs ->

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

28302830 solveDeferred emptyFC n

src/Idris/ElabDecls.hs+3−3

@@ -35,7 +35,7 @@ import Idris.Elab.Clause

3535import Idris.Elab.Data

3636import Idris.Elab.Record

3737import Idris.Elab.Interface

38−import Idris.Elab.Instance

38+import Idris.Elab.Implementation

3939import Idris.Elab.Provider

4040import Idris.Elab.RunElab

4141import Idris.Elab.Transform

@@ -275,9 +275,9 @@ elabDecl' what info (PInterface doc s f cs n nfc ps pdocs fds ds cn cd)

275275 | what /= EDefns

276276 = do logElab 1 $ "Elaborating interface " ++ show n

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

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

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

279279 = do logElab 1 $ "Elaborating implementation " ++ show n

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

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

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

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

283283 elabRecord info what doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn

src/Idris/Erasure.hs+7−7

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

252252

253253 -- get Deps for a Name

254254 getDeps :: Name -> Deps

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

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

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

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

257257 getDeps n = case lookupDefExact n ctx of

258258 Just def -> getDepsDef n def

259259 Nothing -> error $ "erasure checker: unknown reference: " ++ show n

@@ -336,9 +336,9 @@ buildDepMap ci used externs ctx startNames

336336 -- this is safe because it's certainly a patvar

337337 varIdx = fromJust (viFunArg var)

338338

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

339+ -- generate metamethod names, "n" is the implementation ctor

340340 meth :: Int -> Maybe Name

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

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

342342 | otherwise = \j -> Nothing

343343

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

@@ -380,8 +380,8 @@ buildDepMap ci used externs ctx startNames

380380 -- applications may add items to Cond

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

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

383− -- instance constructors -> create metamethod deps

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

383+ -- implementation constructors -> create metamethod deps

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

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

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

387387

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

486486 then length $ getArgTys (argTys !! i)

487487 else error $ "invalid field number " ++ show i ++ " for " ++ show ctorName

488488

489− | otherwise = error $ "unknown instance constructor: " ++ show ctorName

489+ | otherwise = error $ "unknown implementation constructor: " ++ show ctorName

490490

491491 getArity n = case lookupDefExact n ctx of

492492 Just (CaseOp ci ty tys def tot cdefs) -> length tys

src/Idris/IBC.hs+11−11

@@ -276,7 +276,7 @@ ibc i (IBCRecord n) f

276276 = case lookupCtxtExact n (idris_records i) of

277277 Just v -> return f { ibc_records = (n,v): ibc_records f }

278278 _ -> ifail "IBC write failed"

279−ibc i (IBCInstance int res n ins) f

279+ibc i (IBCImplementation int res n ins) f

280280 = return f { ibc_implementations = (int, res, n, ins) : ibc_implementations f }

281281ibc i (IBCDSL n) f

282282 = case lookupCtxtExact n (idris_dsls i) of

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

392392 processStatics archive

393393 processInterfaces archive

394394 processRecords archive

395− processInstances archive

395+ processImplementations archive

396396 processDSLs archive

397397 processDatatypes archive

398398 processOptimise archive

@@ -550,12 +550,12 @@ processInterfaces ar = do

550550 cs <- getEntry [] "ibc_interfaces" ar

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

552552 i <- getIState

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

553+ -- Don't lose implementations from previous IBCs, which

554554 -- could have loaded in any order

555555 let is = case lookupCtxtExact n (idris_interfaces i) of

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

557557 _ -> []

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

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

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

560560

561561processRecords :: Archive -> Idris ()

@@ -564,10 +564,10 @@ processRecords ar = do

564564 mapM_ (\ (n, r) ->

565565 updateIState (\i -> i { idris_records = addDef n r (idris_records i) })) rs

566566

567−processInstances :: Archive -> Idris ()

568−processInstances ar = do

567+processImplementations :: Archive -> Idris ()

568+processImplementations ar = do

569569 cs <- getEntry [] "ibc_implementations" ar

570− mapM_ (\ (i, res, n, ins) -> addInstance i res n ins) cs

570+ mapM_ (\ (i, res, n, ins) -> addImplementation i res n ins) cs

571571

572572processDSLs :: Archive -> Idris ()

573573processDSLs ar = do

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

14241424 put x10

14251425 put x11

14261426 put x12

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

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

14281428 do putWord8 8

14291429 put x1

14301430 put x2

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

15631563 x13 <- get

15641564 x14 <- get

15651565 x15 <- get

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

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

15671567 9 -> do x1 <- get

15681568 x2 <- get

15691569 return (PDSL x1 x2)

@@ -2141,7 +2141,7 @@ instance (Binary t) => Binary (PTactic' t) where

21412141 put x1

21422142 put x2

21432143 put x3

2144− TCInstance -> putWord8 31

2144+ TCImplementation -> putWord8 31

21452145 GoalType x1 x2 -> do putWord8 32

21462146 put x1

21472147 put x2

@@ -2222,7 +2222,7 @@ instance (Binary t) => Binary (PTactic' t) where

22222222 x2 <- get

22232223 x3 <- get

22242224 return (LetTacTy x1 x2 x3)

2225− 31 -> return TCInstance

2225+ 31 -> return TCImplementation

22262226 32 -> do x1 <- get

22272227 x2 <- get

22282228 return (GoalType x1 x2)

src/Idris/IdrisDoc.hs+2−2

@@ -226,7 +226,7 @@ referredNss (n, Just d, _) =

226226 getFunDocs (DataDoc f fs) = f:fs

227227 getFunDocs (InterfaceDoc _ _ fs _ _ _ _ _) = fs

228228 getFunDocs (RecordDoc _ _ f fs _) = f:fs

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

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

230230 getFunDocs (ModDoc _ _) = []

231231 types (FD _ _ args t _) = t:(map second args)

232232 second (_, x, _, _) = x

@@ -643,7 +643,7 @@ createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do

643643 H.dt $ toHtml $ show name

644644 H.dd $ Docstrings.renderHtml docstring

645645

646−createOtherDoc ist (NamedInstanceDoc _ fd) = createFunDoc ist fd

646+createOtherDoc ist (NamedImplementationDoc _ fd) = createFunDoc ist fd

647647

648648createOtherDoc ist (ModDoc _ docstring) = do

649649 Docstrings.renderHtml docstring

src/Idris/Interactive.hs+1−1

@@ -81,7 +81,7 @@ addClauseFrom fn updatefile l n = do

8181 else iPrintResult cl

8282 where

8383 getIndent i n [] = 0

84− getIndent i n xs | take 9 xs == "instance " = i

84+ getIndent i n xs | take 9 xs == "implementation " = i

8585 getIndent i n xs | take (length n) xs == n = i

8686 getIndent i n (x : xs) = getIndent (i + 1) n xs

8787

src/Idris/Package.hs+2−2

@@ -216,9 +216,9 @@ documentPkg copts fp = do

216216 idrisMain opts

217217 addImportDir (sourcedir pkgdesc)

218218 load fs

219− idrisInstance <- run loader idrisInit

219+ idrisImplementation <- run loader idrisInit

220220 setCurrentDirectory cd

221− case idrisInstance of

221+ case idrisImplementation of

222222 Left err -> do

223223 putStrLn $ pshow idrisInit err

224224 exitWith (ExitFailure 1)

src/Idris/Parser.hs+63−63

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

180180 | Mutual

181181 | Namespace

182182 | Interface

183− | Instance

183+ | Implementation

184184 | DSL

185185 | Directive

186186 | Provider

@@ -219,7 +219,7 @@ internalDecl syn

219219 <|> fail "End of readable input"

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

221221 declBody b =

222− try (instance_ True syn)

222+ try (implementation True syn)

223223 <|> try (openInterface syn)

224224 <|> declBody' b

225225 <|> using_ syn

@@ -342,13 +342,13 @@ declExtension syn ns rules =

342342 s

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

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

345− (map (updateNs ns) ds)

346− (updateRecCon ns cname)

347− cdocs

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

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

350− ps pextra ity (fmap (updateB ns) ni)

351− (map (updateNs ns) ds)

345+ (map (updateNs ns) ds)

346+ (updateRecCon ns cname)

347+ cdocs

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

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

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

351+ (map (updateNs ns) ds)

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

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

354354 = PProvider docs s fc fc' pw (updateB ns n)

@@ -832,32 +832,32 @@ namespace syn =

832832 return [PNamespace n nfc (concat ds)]

833833 <?> "namespace declaration"

834834

835−{-| Parses a methods block (for instances)

835+{-| Parses a methods block (for implementations)

836836

837837@

838− InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock

838+ ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock

839839@

840840-}

841−instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

842−instanceBlock syn = do reservedHL "where"

843− openBlock

844− ds <- many (fnDecl syn)

845− closeBlock

846− return (concat ds)

847− <?> "implementation block"

841+implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]

842+implementationBlock syn = do reservedHL "where"

843+ openBlock

844+ ds <- many (fnDecl syn)

845+ closeBlock

846+ return (concat ds)

847+ <?> "implementation block"

848848

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

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

850850

851851@

852−MethodOrInstance ::=

852+MethodOrImplementation ::=

853853 FnDecl

854− | Instance

854+ | Implementation

855855 ;

856856@

857857

858858@

859859InterfaceBlock ::=

860− 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock

860+ 'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock

861861 ;

862862@

863863-}

@@ -871,7 +871,7 @@ interfaceBlock syn = do reservedHL "where"

871871 ist <- get

872872 let cd' = annotate syn ist cd

873873

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

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

875875 <|> do x <- data_ syn

876876 return [x]

877877 <|> fnDecl syn)

@@ -937,52 +937,52 @@ interface_ syn = do (doc, argDocs, acc)

937937{-| Parses an interface implementation declaration

938938

939939@

940− Instance ::=

941− DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

940+ Implementation ::=

941+ DocComment_t? 'implementation' ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?

942942 ;

943943@

944944

945945@

946−InstanceName ::= '[' Name ']';

946+ImplementationName ::= '[' Name ']';

947947@

948948-}

949−instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

950−instance_ kwopt syn

951− = do ist <- get

952− (doc, argDocs) <- docstring syn

953− (opts, acc) <- fnOpts

954− if kwopt then optional instanceKeyword

955− else do instanceKeyword

956− return (Just ())

949+implementation :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

950+implementation kwopt syn

951+ = do ist <- get

952+ (doc, argDocs) <- docstring syn

953+ (opts, acc) <- fnOpts

954+ if kwopt then optional implementationKeyword

955+ else do implementationKeyword

956+ return (Just ())

957957

958− fc <- getFC

959− en <- optional instanceName

960− cs <- constraintList syn

961− let cs' = [(c, ty) | (c, _, ty) <- cs]

962− (cn, cnfc) <- fnName

963− args <- many (simpleExpr syn)

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

965− let t = bindList (PPi constraint) cs sc

966− pnames <- instanceUsing

967− ds <- instanceBlock syn

968− return [PInstance doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]

969− <?> "implementation declaration"

970− where instanceName :: IdrisParser Name

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

972− let n = expandNS syn n_in

973− return n

974− <?> "implementation name"

975− instanceKeyword :: IdrisParser ()

976− instanceKeyword = reservedHL "implementation"

977− <|> do reservedHL "instance"

978− fc <- getFC

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

980−

981− instanceUsing :: IdrisParser [Name]

982− instanceUsing = do reservedHL "using"

983− ns <- sepBy1 fnName (lchar ',')

984− return (map fst ns)

985− <|> return []

958+ fc <- getFC

959+ en <- optional implementationName

960+ cs <- constraintList syn

961+ let cs' = [(c, ty) | (c, _, ty) <- cs]

962+ (cn, cnfc) <- fnName

963+ args <- many (simpleExpr syn)

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

965+ let t = bindList (PPi constraint) cs sc

966+ pnames <- implementationUsing

967+ ds <- implementationBlock syn

968+ return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]

969+ <?> "implementation declaration"

970+ where implementationName :: IdrisParser Name

971+ implementationName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

972+ let n = expandNS syn n_in

973+ return n

974+ <?> "implementation name"

975+ implementationKeyword :: IdrisParser ()

976+ implementationKeyword = reservedHL "implementation"

977+ <|> do reservedHL "instance"

978+ fc <- getFC

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

980+

981+ implementationUsing :: IdrisParser [Name]

982+ implementationUsing = do reservedHL "using"

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

984+ return (map fst ns)

985+ <|> return []

986986

987987-- | Parse a docstring

988988docstring :: SyntaxInfo

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

18671867 PClauses{} -> r

18681868 PInterface{} -> r

18691869 PData{} -> r

1870− PInstance{} -> r

1870+ PImplementation{} -> r

18711871 _ -> x

18721872

18731873 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

src/Idris/Parser/Expr.hs+7−4

@@ -385,7 +385,7 @@ tacticsExpr syn = do kw <- reservedFC "tactics"

385385SimpleExpr ::=

386386 {- External (User-defined) Simple Expression -}

387387 | '?' Name

388− | % 'instance'

388+ | % 'implementation'

389389 | 'Refl' ('{' Expr '}')?

390390 | ProofExpr

391391 | TacticsExpr

@@ -409,7 +409,10 @@ simpleExpr syn =

409409 try (simpleExternalExpr syn)

410410 <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)

411411 return (PMetavar (FC f (l, c-1) end) x)

412− <|> do lchar '%'; fc <- getFC; reserved "instance"; return (PResolveTC fc)

412+ <|> do lchar '%'; fc <- getFC; reserved "implementation"; return (PResolveTC fc)

413+ <|> do lchar '%'; fc <- getFC; reserved "instance"

414+ parserWarning fc Nothing $ Msg "The use of %instance is deprecated, use %implementation instead."

415+ return (PResolveTC fc)

413416 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

414417 <|> proofExpr syn

415418 <|> tacticsExpr syn

@@ -1467,7 +1470,7 @@ verbatimStringLiteral = token $ do (FC f start _) <- getFC

14671470

14681471@

14691472Static ::=

1470− '[' static ']'

1473+ '%static'

14711474;

14721475@

14731476-}

@@ -1582,7 +1585,7 @@ tactics =

15821585 , (["search"], Nothing, const $

15831586 do depth <- option 10 $ fst <$> natural

15841587 return (ProofSearch True True (fromInteger depth) Nothing [] []))

1585− , noArgs ["instance"] TCInstance

1588+ , noArgs ["implementation"] TCImplementation

15861589 , noArgs ["solve"] Solve

15871590 , noArgs ["attack"] Attack

15881591 , noArgs ["state", ":state"] ProofState

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

@@ -715,7 +715,7 @@ collect (PMutual f ms : ds) = PMutual f (collect ms) : collect ds

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

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

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

718−collect (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'

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

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

720720collect (d : ds) = d : collect ds

721721collect [] = []

src/Idris/ProofSearch.hs+6−6

@@ -352,7 +352,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

352352

353353-- | Resolve interfaces. This will only pick up 'normal'

354354-- implementations, never named implementations (which is enforced by

355−-- 'findInstances').

355+-- 'findImplementations').

356356resolveTC :: Bool -- ^ using default Int

357357 -> Bool -- ^ allow open implementations

358358 -> Int -- ^ depth

@@ -407,8 +407,8 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

407407 try' (trivialTCs okholes elab ist)

408408 (do addDefault t tc ttypes

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

410− let insts = idris_openimpls ist ++ findInstances ist t

411− blunderbuss t depth stk (stk ++ insts)) True

410+ let impls = idris_openimpls ist ++ findImplementations ist t

411+ blunderbuss t depth stk (stk ++ impls)) True

412412

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

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

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

489489 = do lams <- introImps

490490 t <- goal

491491 let (tc, ttypes) = trace (show t) $ unApply (getRetTy t)

492−-- if (all boundVar ttypes) then resolveTC (depth - 1) fn insts ist

492+-- if (all boundVar ttypes) then resolveTC (depth - 1) fn impls ist

493493-- else do

494494 -- if there's a hole in the goal, don't even try

495495 let imps = case lookupCtxtName n (idris_implicits ist) of

@@ -522,8 +522,8 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

522522

523523-- | Find the names of implementations that have been designeated for

524524-- searching (i.e. non-named implementations or implementations from Elab scripts)

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

526−findInstances ist t

525+findImplementations :: IState -> Term -> [Name]

526+findImplementations ist t

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

528528 = case lookupCtxt n (idris_interfaces ist) of

529529 [CI _ _ _ _ _ ins _] ->

src/Idris/REPL.hs+2−2

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

904904 fixClauses :: PDecl' t -> PDecl' t

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

906906 PClauses fc opts (getClauseName clause) css

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

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

907+ fixClauses (PImplementation doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty implName decls) =

908+ PImplementation doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty implName (map fixClauses decls)

909909 fixClauses decl = decl

910910

911911 info = recinfo (fileFC "toplevel")

src/Idris/Reflection.hs+13−13

@@ -84,7 +84,7 @@ tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]

8484reify :: IState -> Term -> ElabD PTactic

8585reify _ (P _ n _) | n == reflm "Intros" = return Intros

8686reify _ (P _ n _) | n == reflm "Trivial" = return Trivial

87−reify _ (P _ n _) | n == reflm "Instance" = return TCInstance

87+reify _ (P _ n _) | n == reflm "Implementation" = return TCImplementation

8888reify _ (P _ n _) | n == reflm "Solve" = return Solve

8989reify _ (P _ n _) | n == reflm "Compute" = return Compute

9090reify _ (P _ n _) | n == reflm "Skip" = return Skip

@@ -257,10 +257,10 @@ reifyTTNameApp t [sn]

257257 reifySN t [Constant (I i), n]

258258 | t == reflm "WithN" = WithN i <$> reifyTTName n

259259 reifySN t [n, ss]

260− | t == reflm "InstanceN" =

260+ | t == reflm "ImplementationN" =

261261 case unList ss of

262− Nothing -> fail "Can't reify InstanceN strings"

263− Just ss' -> InstanceN <$> reifyTTName n <*>

262+ Nothing -> fail "Can't reify ImplementationN strings"

263+ Just ss' -> ImplementationN <$> reifyTTName n <*>

264264 pure [T.pack s | Constant (Str s) <- ss']

265265 reifySN t [n, Constant (Str s)]

266266 | t == reflm "ParentN" =

@@ -275,8 +275,8 @@ reifyTTNameApp t [sn]

275275 | t == reflm "ElimN" =

276276 ElimN <$> reifyTTName n

277277 reifySN t [n]

278− | t == reflm "InstanceCtorN" =

279− InstanceCtorN <$> reifyTTName n

278+ | t == reflm "ImplementationCtorN" =

279+ ImplementationCtorN <$> reifyTTName n

280280 reifySN t [n1, n2]

281281 | t == reflm "MetaN" =

282282 MetaN <$> reifyTTName n1 <*> reifyTTName n2

@@ -699,11 +699,11 @@ reflectSpecialName (WhereN i n1 n2) =

699699reflectSpecialName (WithN i n) = reflCall "WithN" [ RConstant (I i)

700700 , reflectName n

701701 ]

702−reflectSpecialName (InstanceN inst ss) =

703− reflCall "InstanceN" [ reflectName inst

704− , mkList (RConstant StrType) $

705− map (RConstant . Str . T.unpack) ss

706− ]

702+reflectSpecialName (ImplementationN impl ss) =

703+ reflCall "ImplementationN" [ reflectName impl

704+ , mkList (RConstant StrType) $

705+ map (RConstant . Str . T.unpack) ss

706+ ]

707707reflectSpecialName (ParentN n s) =

708708 reflCall "ParentN" [reflectName n, RConstant (Str (T.unpack s))]

709709reflectSpecialName (MethodN n) =

@@ -712,8 +712,8 @@ reflectSpecialName (CaseN fc n) =

712712 reflCall "CaseN" [reflectFC (unwrapFC fc), reflectName n]

713713reflectSpecialName (ElimN n) =

714714 reflCall "ElimN" [reflectName n]

715−reflectSpecialName (InstanceCtorN n) =

716− reflCall "InstanceCtorN" [reflectName n]

715+reflectSpecialName (ImplementationCtorN n) =

716+ reflCall "ImplementationCtorN" [reflectName n]

717717reflectSpecialName (MetaN parent meta) =

718718 reflCall "MetaN" [reflectName parent, reflectName meta]

719719

src/Idris/TypeSearch.hs+12−12

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

3030import Data.Traversable (traverse)

3131

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

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

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

3434 , IState (idris_interfaces, idris_docstrings, tt_ctxt, idris_outputmode),

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

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

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

443443 guard $ scoreCriterion (score state')

444444 unifyQueue state' (queue ++ queueAdditions)

445445

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

447− possInterfaceInstances usedns ty = do

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

447+ possInterfaceImplementations usedns ty = do

448448 interfaceName <- getInterfaceName clss

449449 interfaceDef <- lookupCtxt interfaceName interfaceInfo

450− n <- interface_instances interfaceDef

450+ n <- interface_implementations interfaceDef

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

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

453453 let ty' = vToP (uniqueBinders usedns nty)

@@ -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 an interface constraint by replacing it with an instance

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

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

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

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

@@ -497,17 +497,17 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

497497 where

498498 allMods = parallel defMod mods

499499 mods :: Sided [( Interfaces, AsymMods, [Name] )]

500− mods = both (instanceMods . snd) unresolved

500+ mods = both (implementationMods . snd) unresolved

501501 defMod :: Sided (Interfaces, AsymMods, [Name])

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

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

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

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

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

507− | (_, ty) <- interfaces

508− , inst <- possInterfaceInstances usedns ty

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

510− , let newHoles = map fst newInterfaceArgs ]

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

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

507+ | (_, ty) <- interfaces

508+ , impl <- possInterfaceImplementations usedns ty

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

510+ , let newHoles = map fst newInterfaceArgs ]

511511

512512

513513 -- Stage 1 - match arguments

test/docs003/expected+2−2

@@ -28,11 +28,11 @@ Named implementations:

2828Child interfaces:

2929 Traversable f

3030 Applicative f

31−Named instance:

31+Named implementation:

3232 docs003.mine : Functor List

3333

3434

35−Named instance:

35+Named implementation:

3636 docs003.another : Functor List

3737 More functors!

3838

test/proof010/proof010.idr+6−6

@@ -1,24 +1,24 @@

11data MyShow : Type -> Type where

2− ShowInstance : (show : a -> String) -> MyShow a

2+ ShowImplementation : (show : a -> String) -> MyShow a

33

44myshow : {auto inst : MyShow a} -> a -> String

5−myshow {inst = ShowInstance show} x1 = show x1

5+myshow {inst = ShowImplementation show} x1 = show x1

66

77%hint

88showNat : MyShow Nat

9−showNat = ShowInstance show

9+showNat = ShowImplementation show

1010

1111%hint

1212showFn : MyShow (a -> b)

13−showFn = ShowInstance (\x => "<< function >>")

13+showFn = ShowImplementation (\x => "<< function >>")

1414

1515%hint

1616showBools : MyShow (Bool, Bool)

17−showBools = ShowInstance (\x => "some bools")

17+showBools = ShowImplementation (\x => "some bools")

1818

1919%hint

2020showStuff : MyShow a -> MyShow b -> MyShow (a, b)

21−showStuff sa sb = ShowInstance showPair

21+showStuff sa sb = ShowImplementation showPair

2222 where

2323 showPair : (a, b) -> String

2424 showPair (x, y) = myshow x ++ ", " ++ myshow y