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

CHANGELOG.md+5−1

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

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

28* `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.

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

30−

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

30* `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.

32

36

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

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

34

38

CONTRIBUTORS+1

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

53Eric Weinstein

54Jonas Westerlund

55Bjö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:

209 -- stat types.

210 data BitWidth = B8 | B16 | B32 | B64

211

212− instance Show BitWidth where

212+ implementation Show BitWidth where

213 show B8 = "8 bits"

214 show B16 = "16 bits"

215 show B32 = "32 bits"

docs/proofs/pluscomm.rst+1−1

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

53.. code-block:: idris

54

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

56− Refl : x = x

56+ Refl : x = x

57

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

59because ``=`` 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

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

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

71+ Level 2: Provides details of the coverage checking, and further details the elaboration process specifically: 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.

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

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

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

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

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

130For 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.

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

132

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

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

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

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

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

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

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

173Just 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.

174Furthermore, 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.

176

177Using Idris's Features

178======================

docs/reference/ffi.rst+1−1

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

47 JS_IO a = IO' FFI_JS a

48

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

51following are both valid:

52

53.. code-block:: idris

docs/reference/misc.rst+4−4

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

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

273

274

275−Existence of an instance

275+Existence of an implementation

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

277

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

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

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

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

280

281.. code:: idris

282

283 foo : Num Nat

284− foo = %instance

284+ foo = %implementation

285

286'match' application

287===================

idris.cabal+1−1

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

152 , Idris.Elab.Data

153 , Idris.Elab.Record

154 , Idris.Elab.Interface

155− , Idris.Elab.Instance

155+ , Idris.Elab.Implementation

156 , Idris.Elab.Provider

157 , Idris.Elab.RunElab

158 , Idris.Elab.Transform

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

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

24toList : SortedSet k -> List k

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

26

27−instance Foldable SortedSet where

27+implementation Foldable SortedSet where

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

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

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

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

88 showArg n1 ++ showArg n2

89 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

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

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

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

94 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

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

97

98 implementation Show TTName where

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

110 x == y = False

111

112 implementation Eq SpecialName where

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

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'

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

122− _ == _ = False

122+ _ == _ = False

123

124implementation Show TTUExp where

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

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

347pure = id

348

349--------------------------------------

350−-- Instances for definition reflection

350+-- Implementations for definition reflection

351--------------------------------------

352implementation Show Erasure where

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

2||| and Complex number types.

3−module Control.Algebra.NumericInstances

3+module Control.Algebra.NumericImplementations

4

5import Control.Algebra

6import Control.Algebra.VectorSpace

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

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

5

6import public Control.Algebra

7import public Control.Algebra.VectorSpace

8−import public Control.Algebra.NumericInstances

8+import public Control.Algebra.NumericImplementations

9

10import public Data.Matrix

11

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

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

9-- Interface for decidable n-ary Relations

10--------------------------------------------------------------------------------

11

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

13-- at the moment.

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

15 total decide : liftRel ts p Dec

libs/contrib/contrib.ipkg+1−1

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

5

6 Control.Algebra,

7 Control.Algebra.Lattice, Control.Algebra.VectorSpace,

8− Control.Algebra.NumericInstances,

8+ Control.Algebra.NumericImplementations,

9 Control.Isomorphism.Primitives,

10 Control.Partial,

11

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

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

3interface Default a where

4 default : a

5

6−instance Default Int where

6+implementation Default Int where

7 default = 0

8

9−instance Default Integer where

9+implementation Default Integer where

10 default = 0

11

12−instance Default Double where

12+implementation Default Double where

13 default = 0

14

15−instance Default Nat where

15+implementation Default Nat where

16 default = 0

17

18−instance Default Char where

18+implementation Default Char where

19 default = '\0'

20

21−instance Default String where

21+implementation Default String where

22 default = ""

23

24−instance Default Bool where

24+implementation Default Bool where

25 default = False

26

27−instance Default () where

27+implementation Default () where

28 default = ()

29

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

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

31 default = (default, default)

32

33−instance Default (Maybe a) where

33+implementation Default (Maybe a) where

34 default = Nothing

35

36−instance Default (List a) where

36+implementation Default (List a) where

37 default = []

38

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

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

40 default = mkDef _ where

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

42 mkDef Z = []

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

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

7data Exception : Type -> Effect where

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

9

10−instance Handler (Exception a) Maybe where

10+implementation Handler (Exception a) Maybe where

11 handle _ (Raise e) k = Nothing

12

13−instance Handler (Exception a) List where

13+implementation Handler (Exception a) List where

14 handle _ (Raise e) k = []

15

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

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

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

18 believe_me (exit 1)

19

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

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

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

22

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

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

24 handle _ (Raise e) k = Left e

25

26EXCEPTION : Type -> EFFECT

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

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

73-- ------------------------------------------------------------ [ The Handlers ]

74

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

76−instance Handler FileIO IO where

76+implementation Handler FileIO IO where

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

78 valid <- validFile h

79 if valid then k True (FH h)

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

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

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

78 do_poke ptr (S offset) bs

79

80−instance Handler RawMemory (IOExcept String) where

80+implementation Handler RawMemory (IOExcept String) where

81 handle () (Allocate n) k

82 = do ptr <- do_malloc n

83 k () (CH ptr)

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

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

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

6

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

9 map f prog = do t <- prog

10 value (f t)

11

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

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

13 pure = value

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

15 a' <- a

16 value (f' a')

17

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

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

19 (>>=) = Effects.(>>=)

20

21

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

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

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

8

9using (m : Type -> Type)

10− instance Handler Random m where

10+ implementation Handler Random m where

11 handle seed getRandom k

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

13 k seed' seed'

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

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

5data Selection : Effect where

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

7

8−instance Handler Selection Maybe where

8+implementation Handler Selection Maybe where

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

10 tryAll [] = Nothing

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

12 Nothing => tryAll xs

13 Just v => Just v

14

15−instance Handler Selection List where

15+implementation Handler Selection List where

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

17

18SELECT : EFFECT

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

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

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

10

11using (m : Type -> Type)

12− instance Handler State m where

12+ implementation Handler State m where

13 handle st Get k = k st st

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

15

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

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

19-- IO effects handlers

20-------------------------------------------------------------

21

22−instance Handler StdIO IO where

22+implementation Handler StdIO IO where

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

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

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

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

27

28−instance Handler StdIO (IOExcept a) where

28+implementation Handler StdIO (IOExcept a) where

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

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

31 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

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

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

15

16−instance Handler System IO where

16+implementation Handler System IO where

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

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

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

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

21

22−instance Handler System (IOExcept a) where

22+implementation Handler System (IOExcept a) where

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

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

25 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

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

117

118using (lbl : Type)

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

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

120 default = lbl := default

121

122private

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

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

65

66 data SpecialName = WhereN Int TTName TTName

67 | WithN Int TTName

68− | InstanceN TTName (List String)

68+ | ImplementationN TTName (List String)

69 | ParentN TTName String

70 | MethodN TTName

71 | CaseN SourceLocation TTName

72 | ElimN TTName

73− | InstanceCtorN TTName

73+ | ImplementationCtorN TTName

74 | MetaN TTName TTName

75 %name SpecialName sn, sn'

76

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+

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

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

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

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

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

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

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

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

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

118 uninhabited Refl impossible

126 uninhabited Refl impossible

119

127

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

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

121 uninhabited Refl impossible

129 uninhabited Refl impossible

122

130

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

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

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

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

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

133 uninhabited Refl impossible

141 uninhabited Refl impossible

134

142

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

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

136 uninhabited Refl impossible

144 uninhabited Refl impossible

137

145

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

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

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

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

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

142 uninhabited Refl impossible

150 uninhabited Refl impossible

143

151

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

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

145 uninhabited Refl impossible

153 uninhabited Refl impossible

146

154

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

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

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

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

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

157 uninhabited Refl impossible

165 uninhabited Refl impossible

158

166

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

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

160 uninhabited Refl impossible

168 uninhabited Refl impossible

161

169

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

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

163 uninhabited Refl impossible

171 uninhabited Refl impossible

164

172

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

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

166 uninhabited Refl impossible

174 uninhabited Refl impossible

167

175

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

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

169 uninhabited Refl impossible

177 uninhabited Refl impossible

170

178

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

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

172 uninhabited Refl impossible

180 uninhabited Refl impossible

173

181

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

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

175 uninhabited Refl impossible

183 uninhabited Refl impossible

176

184

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

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

178 uninhabited Refl impossible

186 uninhabited Refl impossible

179

187

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

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

181 uninhabited Refl impossible

189 uninhabited Refl impossible

182

190

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

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

184 uninhabited Refl impossible

192 uninhabited Refl impossible

185

193

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

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

187 uninhabited Refl impossible

195 uninhabited Refl impossible

188

196

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

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

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

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

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

193 uninhabited Refl impossible

201 uninhabited Refl impossible

194

202

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

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

196 uninhabited Refl impossible

204 uninhabited Refl impossible

197

205

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

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

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

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

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

205 uninhabited Refl impossible

213 uninhabited Refl impossible

206

214

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

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

208 uninhabited Refl impossible

216 uninhabited Refl impossible

209

217

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

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

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

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

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

217 uninhabited Refl impossible

225 uninhabited Refl impossible

218

226

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

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

220 uninhabited Refl impossible

228 uninhabited Refl impossible

221

229

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

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

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

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

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

229 uninhabited Refl impossible

237 uninhabited Refl impossible

230

238

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

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

232 uninhabited Refl impossible

240 uninhabited Refl impossible

233

241

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

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

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

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

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

241 uninhabited Refl impossible

249 uninhabited Refl impossible

242

250

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

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

244 uninhabited Refl impossible

252 uninhabited Refl impossible

245

253

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

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

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

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

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

253 uninhabited Refl impossible

261 uninhabited Refl impossible

254

262

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

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

256 uninhabited Refl impossible

264 uninhabited Refl impossible

257

265

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

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

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

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

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

265 uninhabited Refl impossible

273 uninhabited Refl impossible

266

274

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

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

268 uninhabited Refl impossible

276 uninhabited Refl impossible

269

277

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

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

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

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

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

277 uninhabited Refl impossible

285 uninhabited Refl impossible

278

286

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

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

280 uninhabited Refl impossible

288 uninhabited Refl impossible

281

289

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

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

283 uninhabited Refl impossible

291 uninhabited Refl impossible

284

292

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

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

286 uninhabited Refl impossible

294 uninhabited Refl impossible

287

295

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

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

289 uninhabited Refl impossible

297 uninhabited Refl impossible

290

298

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

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

292 uninhabited Refl impossible

300 uninhabited Refl impossible

293

301

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

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

295 uninhabited Refl impossible

303 uninhabited Refl impossible

296

304

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

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

298 uninhabited Refl impossible

306 uninhabited Refl impossible

299

307

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

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

301 uninhabited Refl impossible

309 uninhabited Refl impossible

302

310

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

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

304 uninhabited Refl impossible

312 uninhabited Refl impossible

305

313

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

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

307 uninhabited Refl impossible

315 uninhabited Refl impossible

308

316

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

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

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

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

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

313 uninhabited Refl impossible

321 uninhabited Refl impossible

314

322

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

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

316 uninhabited Refl impossible

324 uninhabited Refl impossible

317

325

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

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

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

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

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

328 uninhabited Refl impossible

336 uninhabited Refl impossible

329

337

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

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

331 uninhabited Refl impossible

339 uninhabited Refl impossible

332

340

333mutual

341mutual

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

398 private

406 private

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

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

400 instanceNInj Refl = (Refl, Refl)

408 instanceNInj Refl = (Refl, Refl)

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

401

410

411+ private

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

413+ implementationNInj Refl = (Refl, Refl)

414+

402 private

415 private

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

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

404 parentNInj Refl = (Refl, Refl)

417 parentNInj Refl = (Refl, Refl)

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

416 elimNInj Refl = Refl

429 elimNInj Refl = Refl

417

430

418 private

431 private

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

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

420− instanceCtorNInj Refl = Refl

433+ implementationCtorNInj Refl = Refl

421

434

422 private

435 private

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

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

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

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

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

438 No $ contra . fst . whereNInj

451 No $ contra . fst . whereNInj

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

452 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

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

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

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

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

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

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

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

457 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

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

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

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

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

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

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

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

453 No $ contra . snd . withNInj

466 No $ contra . snd . withNInj

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

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

455 No $ contra . fst . withNInj

468 No $ contra . fst . withNInj

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

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

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

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

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

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

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

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

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

473 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

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

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

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

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

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

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

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

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

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

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

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

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

468 Yes Refl

481 Yes Refl

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

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

470− No $ contra . snd . instanceNInj

483+ No $ contra . snd . implementationNInj

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

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

472− No $ contra . fst . instanceNInj

485+ No $ contra . fst . implementationNInj

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

493 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

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

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

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

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

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

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

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

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

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

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

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

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

505 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

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

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

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

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

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

509 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

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

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

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

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

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

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

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

503 No $ contra . methodNInj

516 No $ contra . methodNInj

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

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

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

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

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

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

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

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

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

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

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

522 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

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

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

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

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

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

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

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

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

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

520 No $ contra . fst . caseNInj

533 No $ contra . fst . caseNInj

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

534 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

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

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

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

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

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

538 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

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

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

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

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

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

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

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

532 Yes Refl

545 Yes Refl

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

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

534 No $ contra . elimNInj

547 No $ contra . elimNInj

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

546 Yes Refl

559 Yes Refl

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

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

548− No $ contra . instanceCtorNInj

561+ No $ contra . implementationCtorNInj

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

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

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

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

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

564 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

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

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

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

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

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

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

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

569 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

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

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

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

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

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

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

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

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

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

799 Search Int |

812 Search Int |

800 ||| Resolve an interface

813 ||| Resolve an interface

801− Instance |

814+ Implementation |

802 ||| Infer the proof target from the context

815 ||| Infer the proof target from the context

803 Solve |

816 Solve |

804 ||| introduce all variables into the context

817 ||| introduce all variables into the context

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

995 quotedTy = `(SpecialName)

1008 quotedTy = `(SpecialName)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1005

1018

1006mutual

1019mutual

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

1015 quotedTy = `(SpecialName)

1028 quotedTy = `(SpecialName)

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

1025

1038

1026

1039

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

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

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

1273 quote Trivial = `(Trivial)

1286 quote Trivial = `(Trivial)

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

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

1275− quote Instance = `(Instance)

1288+ quote Implementation = `(Implementation)

1276 quote Solve = `(Solve)

1289 quote Solve = `(Solve)

1277 quote Intros = `(Intros)

1290 quote Intros = `(Intros)

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

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

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

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

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

1303 quote Trivial = `(Trivial)

1316 quote Trivial = `(Trivial)

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

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

1305− quote Instance = `(Instance)

1318+ quote Implementation = `(Implementation)

1306 quote Solve = `(Solve)

1319 quote Solve = `(Solve)

1307 quote Intros = `(Intros)

1320 quote Intros = `(Intros)

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

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

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

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

182 Prim__DefineFunction : FunDefn Raw -> Elab ()

183 Prim__DeclareDatatype : TyDecl -> Elab ()

184 Prim__DefineDatatype : DataDefn -> Elab ()

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

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

186 Prim__IsTCName : TTName -> Elab Bool

187

188 Prim__ResolveTC : TTName -> Elab ()

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

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

556 |||

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

559 export

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

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

561+ addImplementation ifaceName implName = Prim__AddImplementation ifaceName implName

562+

563+ export

561− addInstance ifaceName instName = Prim__AddInstance ifaceName instName

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

565+ addInstance = addImplementation

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

562

567

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

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

564 |||

569 |||

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

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

89

90

91--------------------------------------------------------------------------------

92−-- Instances

92+-- Implementations

93--------------------------------------------------------------------------------

94

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

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

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

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

250

251--------------------------------------------------------------------------------

252−-- Instances

252+-- Implementations

253--------------------------------------------------------------------------------

254

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

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

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

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

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

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

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

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

133||| equality.

samples/effects/Exception.idr+1−1

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

7

8data MyErr = NotANumber | OutOfRange

9

10−instance Show MyErr where

10+implementation Show MyErr where

11 show NotANumber = "Not a number"

12 show OutOfRange = "Out of range"

13

samples/effects/TreeTag.idr+1−1

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

6data BTree a = Leaf

7 | Node (BTree a) a (BTree a)

8

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

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

10 show Leaf = "[]"

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

12 ++ show x ++ " "

samples/misc/binary.idr+2−2

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

4 b0 : Bit 0

5 b1 : Bit 1

6

7−instance Show (Bit n) where

7+implementation Show (Bit n) where

8 show b0 = "0"

9 show b1 = "1"

10

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

14 zero : Binary Z Z

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

16

17−instance Show (Binary w k) where

17+implementation Show (Binary w k) where

18 show zero = ""

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

20

samples/misc/interp.idr+1−1

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

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

52 (<) = Op (<)

53

54− instance Num (Expr G TyInt) where

54+ implementation Num (Expr G TyInt) where

55 (+) x y = Op (+) x y

56 (-) x y = Op (-) x y

57 (*) x y = Op (*) x y

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

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

1> module MyOrd

2

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

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

4for the dictionary:

5

6−> instance [myord] Ord Nat where

6+> implementation [myord] Ord Nat where

7> compare O (S n) = GT

8> compare (S n) O = LT

9> compare O O = EQ

10

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

12Here, 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

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

14−instance --- they must not overlap.

14+implementation --- they must not overlap.

15

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

17

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

25

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

27

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

29such functions. Hoorah!

30

31> test2 : List Nat

samples/tutorial/binary.idr+1−1

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

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

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

7

8−instance Show (Binary n) where

8+implementation Show (Binary n) where

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

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

11 show bEnd = ""

samples/tutorial/idiom.idr+2−2

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

13 fetchVal [] = Nothing

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

15

16−instance Functor Eval where

16+implementation Functor Eval where

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

18

19−instance Applicative Eval where

19+implementation Applicative Eval where

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

21

22 (<*>) (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)

185

186 snRank :: SpecialName -> String

187 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

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

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

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

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

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

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

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

195

196isCon (TyDecl _ _) = True

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

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

629 where

630 methodVars = case n of

631− SN (InstanceCtorN interfaceName)

631+ SN (ImplementationCtorN interfaceName)

632 -> M.fromList [(v, VI

633 { viMethod = Just $ mkFieldName n i

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

635 _

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

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

637

638irAlt top vs _ (ConstCase x rhs)

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

src/Idris/AbsSyntax.hs+25−25

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

424 return $ lookupCtxtExact n (idris_fragile i)

425

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

427−push_estack n inst

427+push_estack n impl

428 = do i <- getIState

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

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

430

431pop_estack :: Idris ()

432pop_estack = do i <- getIState

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

438--

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

440--

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

442-- resolved by default.

443--

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

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

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

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

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

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

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

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

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

449− -> Idris ()

449+ -> Idris ()

450−addInstance int res n i

450+addImplementation int res n i

451 = do ist <- getIState

452 case lookupCtxt n (idris_interfaces ist) of

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

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

467 chaser (NS n _) = chaser n

468 chaser _ = False

469

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

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

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

472-- naming parent implementations when defining an implementation with

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

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

497addInterface n i

498 = do ist <- getIState

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

501 _ -> i

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

503

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

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

1364 cn

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

1367 = let cn' = case cn of

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

1369 Nothing -> Nothing in

1370− PInstance doc argDocs info f

1370+ PImplementation doc argDocs info f

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

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

1372− pnames acc opts n

1372+ pnames acc opts n

1373− nfc

1373+ nfc

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

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

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

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

1376− (expandParams dec ps ns [] ty)

1376+ (expandParams dec ps ns [] ty)

1377− cn'

1377+ cn'

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

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

1379expandParamsD rhs ist dec ps ns d = d

1380

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

1382

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

1383+expandImplementationScope ist dec ps ns (PImplementation 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)

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

1385− ty cn decls

1385+ ty cn decls

1386−expandInstanceScope ist dec ps ns d = d

1386+expandImplementationScope ist dec ps ns d = d

1387

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

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

298 , idris_repl_defs :: [Name]

299

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

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

303

304

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

348 | IBCStatic Name

349 | IBCInterface Name

350 | IBCRecord Name

351− | IBCInstance Bool Bool Name Name

351+ | IBCImplementation Bool Bool Name Name

352 | IBCDSL Name

353 | IBCData Name

354 | IBCOpt Name

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

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

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

724 [PDecl' t] -- declarations

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

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

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

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

727

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

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

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

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

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

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

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

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

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

733− SyntaxInfo

733+ SyntaxInfo

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

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

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

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

736− Accessibility

736+ Accessibility

737− FnOpts

737+ FnOpts

738− Name -- interface

738+ Name -- interface

739− FC -- precise location of interface

739+ FC -- precise location of interface

740− [t] -- parameters

740+ [t] -- parameters

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

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

742− t -- full instance type

742+ t -- full Implementation type

743− (Maybe Name) -- explicit name

743+ (Maybe Name) -- explicit name

744− [PDecl' t]

744+ [PDecl' t]

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

746 | PSyntax FC Syntax -- ^ Syntax definition

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

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

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

791data RDeclInstructions = RTyDeclInstrs Name FC [PArg] Type

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

793− | RAddInstance Name Name

793+ | RAddImplementation Name Name

794 | RDatatypeDeclInstrs Name [PArg]

795 -- | Datatype, constructors

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

912 (map (mapPDeclFC f g) body)

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

914 ctorDoc

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

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

916− PInstance doc paramDocs syn (f fc)

916+ PImplementation doc paramDocs syn (f fc)

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

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

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

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

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

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

920− (mapPTermFC f g instTy)

920+ (mapPTermFC f g implTy)

921− instN

921+ implN

922− (map (mapPDeclFC f g) body)

922+ (map (mapPDeclFC f g) body)

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

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

925 case syn of

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

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

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

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

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

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

961 = case mn of

962 Nothing -> []

963 Just n -> [n]

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

981tldeclared (PMutual _ ds) = concatMap tldeclared ds

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

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

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

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

985 = case mn of

986 Nothing -> []

987 Just n -> [n]

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

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

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

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

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

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

1005 = case mn of

1006 Nothing -> []

1007 Just n -> [n]

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

1202 | Unfocus

1203 | MatchRefine Name

1204 | LetTac Name t | LetTacTy Name t t

1205− | Exact t | Compute | Trivial | TCInstance

1205+ | Exact t | Compute | Trivial | TCImplementation

1206 | ProofSearch Bool Bool Int (Maybe Name)

1207 [Name] -- allowed local names

1208 [Name] -- hints

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

1262 size Unfocus = 1

1263 size (MatchRefine x) = 1 + size x

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

1265− size TCInstance = 1

1265+ size TCImplementation = 1

1266

1267type PTactic = PTactic' PTerm

1268

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

1398-- Interface data

1399

1400data InterfaceInfo = CI {

1401− instanceCtorName :: Name

1401+ implementationCtorName :: Name

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

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

1404 , interface_default_super_interfaces :: [PDecl]

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

1407 , interface_determiners :: [Int]

1408 } deriving (Show, Generic)

1409{-!

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

1514 EQ -> ruleSort ss1 ss2

1515 r -> r

1516

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

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

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

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

1520 symCompare (Keyword _) _ = LT

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

1694

1695-- Pretty-printing declarations and terms

1696

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

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

1699

1700instance Show PTerm where

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

1761 -> Doc OutputAnnotation

1762prettyImp impl = pprintPTerm impl [] [] []

1763

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

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

1765

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

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

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

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

1933 ]

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

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

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

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

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

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

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

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

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

2221showDeclImp _ _ = text "..."

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

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

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

342 put x1

343 put x2

344 put x3

345− InstanceN x1 x2 -> do putWord8 1

345+ ImplementationN x1 x2 -> do putWord8 1

346− put x1

346+ put x1

347− put x2

347+ put x2

348 ParentN x1 x2 -> do putWord8 2

349 put x1

350 put x2

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

352 put x1

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

354 ElimN x1 -> do putWord8 5; put x1

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

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

356 WithN x1 x2 -> do putWord8 7

357 put x1

358 put x2

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

368 return (WhereN x1 x2 x3)

369 1 -> do x1 <- get

370 x2 <- get

371− return (InstanceN x1 x2)

371+ return (ImplementationN x1 x2)

372 2 -> do x1 <- get

373 x2 <- get

374 return (ParentN x1 x2)

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

380 5 -> do x1 <- get

381 return (ElimN x1)

382 6 -> do x1 <- get

383− return (InstanceCtorN x1)

383+ return (ImplementationCtorN x1)

384 7 -> do x1 <- get

385 x2 <- get

386 return (WithN x1 x2)

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

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

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

330 isInj ctxt _ = False

331

332−-- | get instance argument names

332+-- | get implementation argument names

333−get_instances :: Elab' aux [Name]

333+get_implementations :: Elab' aux [Name]

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

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

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

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

336

337-- | get auto argument names

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

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

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

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

541

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

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

543−instanceArg n = processTactic' (Instance n)

543+implementationArg n = processTactic' (Implementation n)

544

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

546autoArg n = processTactic' (AutoArg n)

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

895 = do s <- get

896 ps <- get_probs

897 ulog <- getUnifyLog

898− ivs <- get_instances

898+ ivs <- get_implementations

899 case prunStateT 999999 False ps Nothing t1 s of

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

901 return $! v

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

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

962 = do s <- get

963 ps <- get_probs

964− ivs <- get_instances

964+ ivs <- get_implementations

965 case prunStateT pmax True ps (if constrok then Nothing

966 else Just ivs) x s of

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

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

986 = case runStateT x s of

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

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

989− ibad = badInstances (instances p) ivs

989+ ibad = badImplementations (implementations p) ivs

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

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

992 then case reverse (problems p) of

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

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

997 Error e -> Error e

998 where

999− badInstances _ Nothing = False

999+ badImplementations _ Nothing = False

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

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

1001

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

1003debugElaborator msg = do ps <- fmap proof get

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

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

32

33import Util.Pretty hiding (fill)

34

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

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

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

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

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

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

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

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

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

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

40− -- for generating things like type tags

40+ -- for generating things like type tags

41− -- in reflection

41+ -- in reflection

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

50− problems :: Fails,

50+ problems :: Fails,

51− injective :: [Name],

51+ injective :: [Name],

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

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

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

53+ implementations :: [Name], -- ^ implementation arguments (for interfaces)

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

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

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

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

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

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

57− context :: Context,

57+ context :: Context,

58− datatypes :: Ctxt TypeInfo,

58+ datatypes :: Ctxt TypeInfo,

59− plog :: String,

59+ plog :: String,

60− unifylog :: Bool,

60+ unifylog :: Bool,

61− done :: Bool,

61+ done :: Bool,

62− recents :: [Name],

62+ recents :: [Name],

63 while_elaborating :: [FailContext],

64− constraint_ns :: String

64+ constraint_ns :: String

65 }

66

67data Tactic = Attack

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

98 | Focus Name

99 | Defer [Name] Name

100 | DeferType Name Raw [Name]

101− | Instance Name

101+ | Implementation Name

102 | AutoArg Name

103 | SetInjective Name

104 | MoveLast Name

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

431 else ps)

432 return t

433

434−instanceArg :: Name -> RunTactic

434+implementationArg :: Name -> RunTactic

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

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

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

437− is = instances ps in

437+ is = implementations ps in

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

439− instances = x:is })

439+ implementations = x:is })

440 return (Bind x (Hole t) sc)

441−instanceArg n ctxt env _

441+implementationArg n ctxt env _

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

443

444autoArg :: Name -> RunTactic

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

600 notunified = updateNotunified [(x,val)]

601 (notunified ps),

602 recents = x : recents ps,

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

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

604 dotted = dropUnified dropdots (dotted ps) })

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

606 return locked

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

1148 mktac (Focus n) = focus n

1149 mktac (Defer ns n) = defer ns n

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

1151− mktac (Instance n) = instanceArg n

1151+ mktac (Implementation n)= implementationArg n

1152 mktac (AutoArg n) = autoArg n

1153 mktac (SetInjective n) = setinj n

1154 mktac (MoveLast n) = movelast n

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

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

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

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

47 , safeForgetEnv, showCG, showEnv, showEnvDbg, showSep

48− , sInstanceN, sMN, sNS, spanFC, str, subst, substNames, substTerm

48+ , sImplementationN, sMN, sNS, spanFC, str, subst, substNames, substTerm

49 , substV, sUN, tcname, termSmallerThan, tfail, thead, tnull

50 , toAlist, traceWhen, txt, unApply, uniqueBinders, uniqueName

51 , uniqueNameFrom, uniqueNameSet, unList, updateDef, vToP, weakenTm

@@ -497,20 +497,20 @@ deriving instance Binary Name

497

498data SpecialName = WhereN !Int !Name !Name

499 | WithN !Int !Name

500− | InstanceN !Name [T.Text]

500+ | ImplementationN !Name [T.Text]

501 | ParentN !Name !T.Text

502 | MethodN !Name

503 | CaseN !FC' !Name

504 | ElimN !Name

505− | InstanceCtorN !Name

505+ | ImplementationCtorN !Name

506 | MetaN !Name !Name

507 deriving (Eq, Ord, Data, Generic, Typeable)

508{-!

509deriving instance Binary SpecialName

510!-}

511

512−sInstanceN :: Name -> [String] -> SpecialName

512+sImplementationN :: Name -> [String] -> SpecialName

513−sInstanceN n ss = InstanceN n (map T.pack ss)

513+sImplementationN n ss = ImplementationN n (map T.pack ss)

514

515sParentN :: Name -> String -> SpecialName

516sParentN n s = ParentN n (T.pack s)

@@ -544,13 +544,13 @@ instance Show Name where

544instance Show SpecialName where

545 show (WhereN i p c) = show p ++ ", " ++ show c

546 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

548 show (MethodN m) = "method " ++ show m

549 show (ParentN p c) = show p ++ "#" ++ T.unpack c

550 show (CaseN fc n) = "case block in " ++ show n ++

551 if fc == FC' emptyFC then "" else " at " ++ show fc

552 show (ElimN n) = "<<" ++ show n ++ " eliminator>>"

553− show (InstanceCtorN n) = "constructor of " ++ show n

553+ show (ImplementationCtorN n) = "constructor of " ++ show n

554 show (MetaN parent meta) = "<<" ++ show parent ++ " " ++ show meta ++ ">>"

555

556-- 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 ++ "}"

562showCG (SN s) = showCG' s

563 where showCG' (WhereN i p c) = showCG p ++ ":" ++ showCG c ++ ":" ++ show i

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

566 showCG' (MethodN m) = '!':showCG m

567 showCG' (ParentN p c) = showCG p ++ "#" ++ show c

568 showCG' (CaseN fc c) = showCG c ++ showFC' fc ++ "_case"

569 showCG' (ElimN sn) = showCG sn ++ "_elim"

570− showCG' (InstanceCtorN n) = showCG n ++ "_ictor"

570+ showCG' (ImplementationCtorN n) = showCG n ++ "_ictor"

571 showCG' (MetaN parent meta) = showCG parent ++ "_meta_" ++ showCG meta

572 showFC' (FC' NoFC) = ""

573 showFC' (FC' (FileFC f)) = "_" ++ cgFN f

@@ -593,7 +593,7 @@ mapCtxt = fmap . fmap

593-- interface.

594tcname (UN xs) = False

595tcname (NS n _) = tcname n

596−tcname (SN (InstanceN _ _)) = True

596+tcname (SN (ImplementationN _ _)) = True

597tcname (SN (MethodN _)) = True

598tcname (SN (ParentN _ _)) = True

599tcname _ = False

@@ -838,7 +838,7 @@ instance Pretty Raw OutputAnnotation where

838deriving instance Binary Raw

839!-}

840

841−data ImplicitInfo = Impl { tcinstance :: Bool, toplevel_imp :: Bool,

841+data ImplicitInfo = Impl { tcimplementation :: Bool, toplevel_imp :: Bool,

842 machine_gen :: Bool }

843 deriving (Show, Eq, Ord, Data, Generic, Typeable)

844

@@ -1488,12 +1488,12 @@ nextName (SN x) = SN (nextName' x)

1488 where

1489 nextName' (WhereN i f x) = WhereN i f (nextName x)

1490 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

1492 nextName' (ParentN n ns) = ParentN (nextName n) ns

1493 nextName' (CaseN fc n) = CaseN fc (nextName n)

1494 nextName' (ElimN n) = ElimN (nextName n)

1495 nextName' (MethodN n) = MethodN (nextName n)

1496− nextName' (InstanceCtorN n) = InstanceCtorN (nextName n)

1496+ nextName' (ImplementationCtorN n) = ImplementationCtorN (nextName n)

1497 nextName' (MetaN parent meta) = MetaN parent (nextName meta)

1498nextName (SymRef i) = error "Can't generate a name from a symbol reference"

1499

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

@@ -193,13 +193,13 @@ match_unify ctxt env (topx, xfrom) (topy, yfrom) inj holes from =

193-- case boundVs (envPos x 0 env) tm of

194-- [] -> return [(x, tm)]

195-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))

196−-- (inst ns tm) (errEnv env))

196+-- (impl ns tm) (errEnv env))

197 let v = highV (-1) tm in

198 if v >= length ns

199 then lift $ tfail (Msg "SCOPE ERROR")

200 else return [(x, bind v ns tm)]

201− where inst [] tm = tm

201+ where impl [] tm = tm

202− inst ((n, _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

202+ impl ((n, _) : ns) tm = impl ns (substV (P Bound n Erased) tm)

203

204 bind i ns tm

205 | i < 0 = tm

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

667-- case boundVs (envPos x 0 env) tm of

668-- [] -> return [(x, tm)]

669-- (i:_) -> lift $ tfail (UnifyScope x (fst (fst (ns!!i)))

670−-- (inst ns tm) (errEnv env))

670+-- (impl ns tm) (errEnv env))

671 let v = highV (-1) tm in

672 if v >= length ns

673 then lift $ tfail (Msg "SCOPE ERROR")

674 else return [(x, bind v ns tm)]

675− where inst [] tm = tm

675+ where impl [] tm = tm

676− inst (((n, _), _) : ns) tm = inst ns (substV (P Bound n Erased) tm)

676+ impl (((n, _), _) : ns) tm = impl ns (substV (P Bound n Erased) tm)

677 checkScope ns (x, tm) = lift $ tfail (Msg "HOLE ERROR")

678

679 bind i ns tm

src/Idris/Delaborate.hs+1−1

@@ -142,7 +142,7 @@ delabTy' ist imps tm fullname mvs docases = de [] imps tm

142 | toplevel_imp impl -- information in 'imps' repeated

143 = PPi (Imp [] Dynamic False (Just impl) False) n NoFC (de env [] ty) (de ((n,n):env) is sc)

144 de env is (Bind n (Pi (Just impl) ty _) sc)

145− | tcinstance impl

145+ | tcimplementation impl

146 = PPi constraint n NoFC (de env [] ty) (de ((n,n):env) is sc)

147 | otherwise

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

48 | InterfaceDoc Name d -- interface docs

49 [FunDoc' d] -- method docs

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

51− [(Maybe Name, PTerm, (d, [(Name, d)]))] -- instances: name for named instances, the constraint term, the docs

51+ [(Maybe Name, PTerm, (d, [(Name, d)]))] -- implementations: name for named implementations, the constraint term, the docs

52 [PTerm] -- sub interfaces

53 [PTerm] -- super interfaces

54 (Maybe (FunDoc' d)) -- explicit constructor

@@ -56,7 +56,7 @@ data Docs' d = FunDoc (FunDoc' d)

56 (FunDoc' d) -- data constructor docs

57 [FunDoc' d] -- projection docs

58 [(Name, PTerm, Maybe d)] -- parameters with type and doc

59− | NamedInstanceDoc Name (FunDoc' d) -- name is interface

59+ | NamedImplementationDoc Name (FunDoc' d) -- name is interface

60 | ModDoc [String] -- Module name

61 d

62 deriving Functor

@@ -139,7 +139,7 @@ pprintDocs ist (DataDoc t args)

139 if null args then text "No constructors."

140 else nest 4 (text "Constructors:" <> line <>

141 vsep (map (pprintFDWithoutTotality ist False) args))

142−pprintDocs ist (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)

143 = nest 4 (text "Interface" <+> prettyName True (ppopt_impl ppo) [] n <>

144 if nullDocstring doc

145 then empty

@@ -157,33 +157,33 @@ pprintDocs ist (InterfaceDoc n doc meths params instances sub_interfaces super_i

157 ctor

158 <>

159 nest 4 (text "Implementations:" <$>

160− vsep (if null instances then [text "<no implementations>"]

160+ vsep (if null implementations then [text "<no implementations>"]

161− else map pprintInstance normalInstances))

161+ else map pprintImplementation normalImplementations))

162 <>

163− (if null namedInstances then empty

163+ (if null namedImplementations then empty

164 else line <$> nest 4 (text "Named implementations:" <$>

165− vsep (map pprintInstance namedInstances)))

165+ vsep (map pprintImplementation namedImplementations)))

166 <>

167 (if null sub_interfaces then empty

168 else line <$> nest 4 (text "Child interfaces:" <$>

169− vsep (map (dumpInstance . prettifySubInterfaces) sub_interfaces)))

169+ vsep (map (dumpImplementation . prettifySubInterfaces) sub_interfaces)))

170 <>

171 (if null super_interfaces then empty

172 else line <$> nest 4 (text "Default parent implementations:" <$>

173− vsep (map dumpInstance super_interfaces)))

173+ vsep (map dumpImplementation super_interfaces)))

174 where

175 params' = zip pNames (repeat False)

176

177− (normalInstances, namedInstances) = partition (\(n, _, _) -> not $ isJust n)

177+ (normalImplementations, namedImplementations) = partition (\(n, _, _) -> not $ isJust n)

178− instances

178+ implementations

179

180 pNames = map fst params

181

182 ppo = ppOptionIst ist

183 infixes = idris_infixes ist

184

185− pprintInstance (mname, term, (doc, argDocs)) =

185+ pprintImplementation (mname, term, (doc, argDocs)) =

186− nest 4 (iname mname <> dumpInstance term <>

186+ nest 4 (iname mname <> dumpImplementation term <>

187 (if nullDocstring doc

188 then empty

189 else line <>

@@ -194,13 +194,13 @@ pprintDocs ist (InterfaceDoc n doc meths params instances sub_interfaces super_i

194 doc) <>

195 if null argDocs

196 then empty

197− else line <> vsep (map (prettyInstanceParam (map fst argDocs)) argDocs))

197+ else line <> vsep (map (prettyImplementationParam (map fst argDocs)) argDocs))

198

199

200 iname Nothing = empty

201 iname (Just n) = annName n <+> colon <> space

202

203− prettyInstanceParam params (name, doc) =

203+ prettyImplementationParam params (name, doc) =

204 if nullDocstring doc

205 then empty

206 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

210-- then vsep (map (\(nm,md) -> prettyName True False params' nm <+> maybe empty (showDoc ist) md) params)

211-- else hsep (punctuate comma (map (prettyName True False params' . fst) params))

212

213− dumpInstance :: PTerm -> Doc OutputAnnotation

213+ dumpImplementation :: PTerm -> Doc OutputAnnotation

214− dumpInstance = pprintPTerm ppo params' [] infixes

214+ dumpImplementation = pprintPTerm ppo params' [] infixes

215

216 prettifySubInterfaces (PPi (Constraint _ _) _ _ tm _) = prettifySubInterfaces tm

217 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)

264 else hsep (punctuate comma (map prettyParam [(n,pt) | (n,pt,_) <- params]))

265 prettyParam (n,pt) = prettyName True False params' n <+> text ":" <+> pprintPTerm ppo params' [] infixes pt

266

267−pprintDocs ist (NamedInstanceDoc _cls doc)

267+pprintDocs ist (NamedImplementationDoc _cls doc)

268− = nest 4 (text "Named instance:" <$> pprintFDWithoutTotality ist True doc)

268+ = nest 4 (text "Named implementation:" <$> pprintFDWithoutTotality ist True doc)

269

270pprintDocs ist (ModDoc mod docs)

271 = nest 4 $ text "Module" <+> text (concat (intersperse "." mod)) <> colon <$>

@@ -293,18 +293,18 @@ getDocs n w

293 -> docRecord n ri

294 | Just ti <- lookupCtxtExact n (idris_datatypes i)

295 -> docData n ti

296− | Just interface_ <- interfaceNameForInst i n

296+ | Just interface_ <- interfaceNameForImpl i n

297 -> do fd <- docFun n

298− return $ NamedInstanceDoc interface_ fd

298+ return $ NamedImplementationDoc interface_ fd

299 | otherwise

300 -> do fd <- docFun n

301 return (FunDoc fd)

302 return $ fmap (howMuch w) docs

303− where interfaceNameForInst :: IState -> Name -> Maybe Name

303+ where interfaceNameForImpl :: IState -> Name -> Maybe Name

304− interfaceNameForInst ist n =

304+ interfaceNameForImpl ist n =

305 listToMaybe [ cn

306 | (cn, ci) <- toAlist (idris_interfaces ist)

307− , n `elem` map fst (interface_instances ci)

307+ , n `elem` map fst (interface_implementations ci)

308 ]

309

310docData :: Name -> TypeInfo -> Idris Docs

@@ -320,31 +320,31 @@ docInterface n ci

320 docstr = maybe emptyDocstring fst docStrings

321 params = map (\pn -> (pn, docStrings >>= (lookup pn . snd)))

322 (interface_params ci)

323− docsForInstance inst = fromMaybe (emptyDocstring, []) .

323+ docsForImplementation impl = fromMaybe (emptyDocstring, []) .

324 flip lookupCtxtExact (idris_docstrings i) $

325− inst

325+ impl

326− instances = map (\inst -> (namedInst inst,

326+ implementations = map (\impl -> (namedImpl impl,

327− delabTy i inst,

327+ delabTy i impl,

328− docsForInstance inst))

328+ docsForImplementation impl))

329− (nub (map fst (interface_instances ci)))

329+ (nub (map fst (interface_implementations ci)))

330− (sub_interfaces, instances') = partition (isSubInterface . (\(_,tm,_) -> tm)) instances

330+ (sub_interfaces, implementations') = partition (isSubInterface . (\(_,tm,_) -> tm)) implementations

331− super_interfaces = catMaybes $ map getDInst (interface_default_super_interfaces ci)

331+ super_interfaces = catMaybes $ map getDImpl (interface_default_super_interfaces ci)

332 mdocs <- mapM (docFun . fst) (interface_methods ci)

333− let ctorN = instanceCtorName ci

333+ let ctorN = implementationCtorName ci

334 ctorDocs <- case basename ctorN of

335 SN _ -> return Nothing

336 _ -> fmap Just $ docFun ctorN

337 return $ InterfaceDoc

338 n docstr mdocs params

339− instances' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces

339+ implementations' (map (\(_,tm,_) -> tm) sub_interfaces) super_interfaces

340 ctorDocs

341 where

342− namedInst (NS n ns) = fmap (flip NS ns) (namedInst n)

342+ namedImpl (NS n ns) = fmap (flip NS ns) (namedImpl n)

343− namedInst n@(UN _) = Just n

343+ namedImpl n@(UN _) = Just n

344− namedInst _ = Nothing

344+ namedImpl _ = Nothing

345

346− getDInst (PInstance _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t

346+ getDImpl (PImplementation _ _ _ _ _ _ _ _ _ _ _ _ t _ _) = Just t

347− getDInst _ = Nothing

347+ getDImpl _ = Nothing

348

349 isSubInterface (PPi (Constraint _ _) _ _ (PApp _ _ args) (PApp _ (PRef _ _ nm) args'))

350 = 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

666

667 let winfo = (pinfo info newargs defs windex) { elabFC = Just fc }

668 let wb = map (mkStatic static_names) $

669− map (expandInstanceScope ist decorate newargs defs) $

669+ map (expandImplementationScope ist decorate newargs defs) $

670 map (expandParamsD False ist decorate newargs defs) whereblock

671

672 -- 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)

1110 addResolves ty tm = tm

1111

1112 -- 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

1114 -- This is something of a hack, because matching on the top level

1115 -- application won't find this information for us

1116 addResolvesArgs :: FC -> Term -> [PArg] -> [PArg]

src/Idris/Elab/Instance.hs → src/Idris/Elab/Implementation.hsrenamed+44−46

@@ -1,12 +1,12 @@

1{-|

2−Module : Idris.Elab.Instance

2+Module : Idris.Elab.Implementation

3Description : Code to elaborate instances.

4Copyright :

5License : BSD3

6Maintainer : The Idris Community.

7-}

8{-# LANGUAGE PatternGuards #-}

9−module Idris.Elab.Instance(elabInstance) where

9+module Idris.Elab.Implementation(elabImplementation) where

10

11import Idris.AbsSyntax

12import Idris.ASTUtils

@@ -57,25 +57,25 @@ import Data.List.Split (splitOn)

57

58import Util.Pretty(pretty, text)

59

60−elabInstance :: ElabInfo

60+elabImplementation :: ElabInfo

61− -> SyntaxInfo

61+ -> SyntaxInfo

62− -> Docstring (Either Err PTerm)

62+ -> Docstring (Either Err PTerm)

63− -> [(Name, Docstring (Either Err PTerm))]

63+ -> [(Name, Docstring (Either Err PTerm))]

64− -> ElabWhat -- ^ phase

64+ -> ElabWhat -- ^ phase

65− -> FC

65+ -> FC

66− -> [(Name, PTerm)] -- ^ constraints

66+ -> [(Name, PTerm)] -- ^ constraints

67− -> [Name] -- ^ parent dictionary names (optionally)

67+ -> [Name] -- ^ parent dictionary names (optionally)

68− -> Accessibility

68+ -> Accessibility

69− -> FnOpts

69+ -> FnOpts

70− -> Name -- ^ the interface

70+ -> Name -- ^ the interface

71− -> FC -- ^ precise location of interface name

71+ -> FC -- ^ precise location of interface name

72− -> [PTerm] -- ^ interface parameters (i.e. instance)

72+ -> [PTerm] -- ^ interface parameters (i.e. implementation)

73− -> [(Name, PTerm)] -- ^ Extra arguments in scope (e.g. instance in where block)

73+ -> [(Name, PTerm)] -- ^ Extra arguments in scope (e.g. implementation in where block)

74− -> PTerm -- ^ full instance type

74+ -> PTerm -- ^ full implementation type

75− -> Maybe Name -- ^ explicit name

75+ -> Maybe Name -- ^ explicit name

76− -> [PDecl]

76+ -> [PDecl]

77− -> Idris ()

77+ -> Idris ()

78−elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t expn ds = do

78+elabImplementation info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t expn ds = do

79 ist <- getIState

80 (n, ci) <- case lookupCtxtName n (idris_interfaces ist) of

81 [c] -> return c

@@ -93,13 +93,13 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

93 when (what /= EDefns) $ do

94 nty <- elabType' True info syn doc argDocs fc totopts iname NoFC

95 (piBindp expl_param pextra t)

96− -- if the instance type matches any of the instances we have already,

96+ -- if the implementation type matches any of the implementations we have already,

97− -- and it's not a named instance, then it's overlapping, so report an error

97+ -- and it's not a named implementation, then it's overlapping, so report an error

98 case expn of

99 Nothing -> do mapM_ (maybe (return ()) overlapping . findOverlapping ist (interface_determiners ci) (delab ist nty))

100− (map fst $ interface_instances ci)

100+ (map fst $ interface_implementations ci)

101− addInstance intInst True n iname

101+ addImplementation intImpl True n iname

102− Just _ -> addInstance intInst False n iname

102+ Just _ -> addImplementation intImpl False n iname

103 when (what /= ETypes && (not (null ds && not emptyinterface))) $ do

104 -- Add the parent implementation names to the privileged set

105 oldOpen <- addOpenImpl parents

@@ -118,12 +118,12 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

118 let pnames = nub $ map pname (concat (nub wparams)) ++

119 concatMap (namesIn [] ist) ps

120

121− let superInterfaceInstances = map (substInstance ips pnames) (interface_default_super_interfaces ci)

121+ let superInterfaceImplementations = map (substImplementation ips pnames) (interface_default_super_interfaces ci)

122− undefinedSuperInterfaceInstances <- filterM (fmap not . isOverlapping ist) superInterfaceInstances

122+ undefinedSuperInterfaceImplementations <- filterM (fmap not . isOverlapping ist) superInterfaceImplementations

123− mapM_ (rec_elabDecl info EAll info) undefinedSuperInterfaceInstances

123+ mapM_ (rec_elabDecl info EAll info) undefinedSuperInterfaceImplementations

124

125 ist <- getIState

126− -- Bring variables in instance head into scope when building the

126+ -- Bring variables in implementation head into scope when building the

127 -- dictionary

128 let headVars = nub $ concatMap getHeadVars ps

129 let (headVarTypes, ty)

@@ -159,18 +159,16 @@ elabInstance info syn doc argDocs what fc cs parents acc opts n nfc ps pextra t

159 let wb = wbTys ++ wbVals

160

161 logElab 3 $ "Method types " ++ showSep "\n" (map (show . showDeclImp verbosePPOption . mkTyDecl) mtys)

162− logElab 3 $ "Instance is " ++ show ps ++ " implicits " ++

162+ logElab 3 $ "Implementation is " ++ show ps ++ " implicits " ++ show (concat (nub wparams))

163− show (concat (nub wparams))

164−

165

163

166 let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars

164 let lhsImps = map (\n -> pimp n (PRef fc [] n) True) headVars

167

165

168 let lhs = PApp fc (PRef fc [] iname) (lhsImps ++ map (toExp .fst) pextra)

166 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))

170 (map (pexp . (mkMethApp lhsImps)) mtys)

168 (map (pexp . (mkMethApp lhsImps)) mtys)

171

169

172− logElab 5 $ "Instance LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars

170+ logElab 5 $ "Implementation LHS " ++ show totopts ++ "\n" ++ showTmImpls lhs ++ " " ++ show headVars

173− logElab 5 $ "Instance RHS " ++ show rhs

171+ logElab 5 $ "Implementation RHS " ++ show rhs

174

172

175 push_estack iname True

173 push_estack iname True

176 logElab 3 ("Method types: " ++ show wbTys)

174 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

207-- totalityCheckBlock

205-- totalityCheckBlock

208

206

209 checkInjectiveArgs fc n (interface_determiners ci) (lookupTyExact iname (tt_ctxt ist))

207 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)

211

209

212 where

210 where

213− intInst = case ps of

211+ intImpl = case ps of

214 [PConstant NoFC (AType (ATInt ITNative))] -> True

212 [PConstant NoFC (AType (ATInt ITNative))] -> True

215 _ -> False

213 _ -> False

216

214

217 mkiname n' ns ps' expn' =

215 mkiname n' ns ps' expn' =

218 case expn' of

216 case expn' of

219 Nothing -> case ns of

217 Nothing -> case ns of

220− [] -> SN (sInstanceN n' (map show ps'))

218+ [] -> SN (sImplementationN n' (map show ps'))

221− m -> sNS (SN (sInstanceN n' (map show ps'))) m

219+ m -> sNS (SN (sImplementationN n' (map show ps'))) m

222 Just nm -> nm

220 Just nm -> nm

223

221

224− substInstance ips pnames (PInstance doc argDocs syn _ cs parents acc opts n nfc ps pextra t expn ds)

222+ substImplementation ips pnames (PImplementation 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

223+ = PImplementation doc argDocs syn fc cs parents acc opts n nfc

226 (map (substMatchesShadow ips pnames) ps)

224 (map (substMatchesShadow ips pnames) ps)

227 pextra

225 pextra

228 (substMatchesShadow ips pnames t) expn ds

226 (substMatchesShadow ips pnames t) expn ds

229

227

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 _)

231 = case lookupCtxtName n (idris_interfaces i) of

229 = case lookupCtxtName n (idris_interfaces i) of

232 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

230 [(n, ci)] -> let iname = (mkiname n (namespace info) ps expn) in

233 case lookupTy iname (tt_ctxt i) of

231 case lookupTy iname (tt_ctxt i) of

234 [] -> elabFindOverlapping i ci iname syn t

232 [] -> elabFindOverlapping i ci iname syn t

235 (_:_) -> return True

233 (_:_) -> 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

237

235

238 -- TODO: largely based upon elabType' - should try to abstract

236 -- TODO: largely based upon elabType' - should try to abstract

239 -- Issue #1614 in the issue tracker:

237 -- 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

255 ctxt <- getContext

253 ctxt <- getContext

256 (cty, _) <- recheckC (constraintNS info) fc id [] tyT

254 (cty, _) <- recheckC (constraintNS info) fc id [] tyT

257 let nty = normalise ctxt [] cty

255 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)

259

257

260 findOverlapping i dets t n

258 findOverlapping i dets t n

261 | SN (ParentN _ _) <- n = Nothing

259 | SN (ParentN _ _) <- n = Nothing

@@ -393,7 +391,7 @@ getHeadVars (PPair _ _ _ l r) = getHeadVars l ++ getHeadVars r

393getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t

391getHeadVars (PDPair _ _ _ l t r) = getHeadVars l ++ getHeadVars t ++ getHeadVars t

394getHeadVars _ = []

392getHeadVars _ = []

395

393

396−-- | Implicitly bind variables from the instance head in method types

394+-- | Implicitly bind variables from the implementation head in method types

397impBind :: [(Name, PTerm)] -> PDecl -> PDecl

395impBind :: [(Name, PTerm)] -> PDecl -> PDecl

398impBind vs (PTy d ds syn fc opts n fc' t)

396impBind vs (PTy d ds syn fc opts n fc' t)

399 = PTy d ds syn fc opts n fc'

397 = PTy d ds syn fc opts n fc'

src/Idris/Elab/Interface.hs+23−23

@@ -62,21 +62,21 @@ import Util.Pretty(pretty, text)

62data MArgTy = IA Name | EA Name | CA deriving Show

63

64elabInterface :: ElabInfo

65− -> SyntaxInfo

65+ -> SyntaxInfo

66− -> Docstring (Either Err PTerm)

66+ -> Docstring (Either Err PTerm)

67− -> FC

67+ -> FC

68− -> [(Name, PTerm)]

68+ -> [(Name, PTerm)]

69− -> Name

69+ -> Name

70− -> FC

70+ -> FC

71− -> [(Name, FC, PTerm)]

71+ -> [(Name, FC, PTerm)]

72− -> [(Name, Docstring (Either Err PTerm))]

72+ -> [(Name, Docstring (Either Err PTerm))]

73− -> [(Name, FC)] -- ^ determining params

73+ -> [(Name, FC)] -- ^ determining params

74− -> [PDecl] -- ^ interface body

74+ -> [PDecl] -- ^ interface body

75− -> Maybe (Name, FC) -- ^ instance ctor name and location

75+ -> Maybe (Name, FC) -- ^ implementation ctor name and location

76− -> Docstring (Either Err PTerm) -- ^ instance ctor docs

76+ -> Docstring (Either Err PTerm) -- ^ implementation ctor docs

77− -> Idris ()

77+ -> Idris ()

78elabInterface 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)

80 let tty = pibind (map (\(n, _, ty) -> (n, ty)) ps) (PType fc)

81 let constraint = PApp fc (PRef fc [] tn)

82 (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

88

89 -- build data declaration

90 let mdecls = filter tydecl ds -- method declarations

91− let idecls = filter instdecl ds -- default super interface implementation declarations

91+ let idecls = filter impldecl ds -- default super interface implementation declarations

92− mapM_ checkDefaultSuperInterfaceInstance idecls

92+ mapM_ checkDefaultSuperInterfaceImplementation idecls

93 let mnames = map getMName mdecls

94 ist <- getIState

95 let constraintNames = nub $

@@ -105,7 +105,7 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

105 = unzip (map (\ (x, y, z) -> (x, y)) ims)

106 let defaults = map (\ (x, (y, z)) -> (x,y)) defs

107

108− -- build instance constructor type

108+ -- build implementation constructor type

109 let cty = impbind [(pn, pt) | (pn, _, pt) <- ps] $ conbind constraints

110 $ pibind (map (\ (n, ty) -> (nsroot n, ty)) methods)

111 constraint

@@ -161,8 +161,8 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

161 chkUniq _ t = t

162

163 -- TODO: probably should normalise

164− checkDefaultSuperInterfaceInstance :: PDecl -> Idris ()

164+ checkDefaultSuperInterfaceImplementation :: PDecl -> Idris ()

165− checkDefaultSuperInterfaceInstance (PInstance _ _ _ fc cs _ _ _ n _ ps _ _ _ _)

165+ checkDefaultSuperInterfaceImplementation (PImplementation _ _ _ fc cs _ _ _ n _ ps _ _ _ _)

166 = do when (not $ null cs) . tclift

167 $ tfail (At fc (Msg "Default super interface implementations can't have constraints."))

168 i <- getIState

@@ -229,8 +229,8 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

229 tydecl (PTy{}) = True

230 tydecl (PData _ _ _ _ _ _) = True

231 tydecl _ = False

232− instdecl (PInstance{}) = True

232+ impldecl (PImplementation{}) = True

233− instdecl _ = False

233+ impldecl _ = False

234 clause (PClauses{}) = True

235 clause _ = False

236

@@ -252,8 +252,8 @@ elabInterface info syn_in doc fc constraints tn tnfc ps pDocs fds ds mcn cd

252 let conn' = case lookupCtxtName conn (idris_interfaces i) of

253 [(n, _)] -> n

254 _ -> conn

255− addInstance False True conn' cfn

255+ addImplementation False True conn' cfn

256− addIBC (IBCInstance False True conn' cfn)

256+ addIBC (IBCImplementation False True conn' cfn)

257-- iputStrLn ("Added " ++ show (conn, cfn, ty))

258 return [PTy emptyDocstring [] syn fc [] cfn NoFC ty,

259 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

90 _ -> False

91

92 hs <- get_holes

93− ivs <- get_instances

93+ ivs <- get_implementations

94 ptm <- get_term

95 -- 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

97 when (not pattern) $

98 mapM_ (\n -> when (n `elem` hs) $

99 do focus n

100 g <- goal

101 try (resolveTC' True True 10 g fn ist)

102 (movelast n)) ivs

103− ivs <- get_instances

103+ ivs <- get_implementations

104 hs <- get_holes

105 when (not pattern) $

106 mapM_ (\n -> when (n `elem` hs) $

@@ -397,7 +397,7 @@ elab ist info emode opts fn tm

397 = do g <- goal; resolveTC False False 5 g fn elabRec ist

398 elab' ina fc (PResolveTC fc')

399 = do c <- getNameFrom (sMN 0 "__interface")

400− instanceArg c

400+ implementationArg c

401 -- Elaborate the equality type first homogeneously, then

402 -- heterogeneously as a fallback

403 elab' ina _ (PApp fc (PRef _ _ n) args)

@@ -721,7 +721,7 @@ elab ist info emode opts fn tm

721 highlightSource nfc (AnnBoundName n False)

722 elab' ina _ tm@(PLet fc n nfc ty val sc)

723 = do attack

724− ivs <- get_instances

724+ ivs <- get_implementations

725 tyn <- getNameFrom (sMN 0 "letty")

726 claim tyn RType

727 valn <- getNameFrom (sMN 0 "letval")

@@ -738,7 +738,7 @@ elab ist info emode opts fn tm

738 focus valn

739 elabE (ina { e_inarg = True, e_intype = True })

740 (Just fc) val

741− ivs' <- get_instances

741+ ivs' <- get_implementations

742 env <- get_env

743 elabE (ina { e_inarg = True }) (Just fc) sc

744 when (not (pattern || intransform)) $

@@ -861,9 +861,9 @@ elab ist info emode opts fn tm

861 (ffc, annot) : map (\f -> (f, annot)) hls

862 return []

863 else

864− do ivs <- get_instances

864+ do ivs <- get_implementations

865 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

867 -- function or default definition.

868 let isinf = f == inferCon || tcname f

869 -- if f is an interface, we need to know its arguments so that

@@ -913,7 +913,7 @@ elab ist info emode opts fn tm

913 rs@(_:_) | not pattern -> return rs -- quit, try again

914 _ -> do solve

915 hs <- get_holes

916− ivs' <- get_instances

916+ ivs' <- get_implementations

917 -- Attempt to resolve any interfaces which have 'complete' types,

918 -- i.e. no holes in them

919 when (not pattern || (e_inarg ina && not tcgen)) $

@@ -1473,7 +1473,7 @@ elab ist info emode opts fn tm

1473 fullApp x = x

1474

1475 insertScopedImps fc (Bind n (Pi im@(Just i) _ _) sc) xs

1476− | tcinstance i && not (toplevel_imp i)

1476+ | tcimplementation i && not (toplevel_imp i)

1477 = pimp n (PResolveTC fc) True : insertScopedImps fc sc xs

1478 | not (toplevel_imp i)

1479 = pimp n Placeholder True : insertScopedImps fc sc xs

@@ -1738,7 +1738,7 @@ pruneByType env (P _ n _) goalty ist as

1738pruneByType _ t _ _ as = as

1739

1740-- Could the name feasibly be the return type?

1741−-- If there is an interface constraint on the return type, and no instance

1741+-- If there is an interface constraint on the return type, and no implementation

1742-- in the environment or globally for that name, then no

1743-- Otherwise, yes

1744-- (FIXME: This isn't complete, but I'm leaving it here and coming back

@@ -1756,7 +1756,7 @@ isPlausible ist var env n ty

1756 = let tcs' = case unApply ty of

1757 (P _ c _, _) ->

1758 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))

1760 : tcs)

1761 Nothing -> tcs

1762 _ -> tcs

@@ -2319,11 +2319,11 @@ runElabAction info ist fc env tm ns = do tm' <- eval tm

2319 -- the rest happens in a bit

2320 updateAux $ \e -> e { new_tyDecls = RDatatypeDefnInstrs n tyconTy ctors' : new_tyDecls e }

2321 returnUnit

2322− | n == tacN "Prim__AddInstance"

2322+ | n == tacN "Prim__AddImplementation"

2323− = do ~[cls, inst] <- tacTmArgs 2 tac args

2323+ = do ~[cls, impl] <- tacTmArgs 2 tac args

2324 interfaceName <- reifyTTName cls

2325− instName <- reifyTTName inst

2325+ implName <- reifyTTName impl

2326− updateAux $ \e -> e { new_tyDecls = RAddInstance interfaceName instName :

2326+ updateAux $ \e -> e { new_tyDecls = RAddImplementation interfaceName implName :

2327 new_tyDecls e }

2328 returnUnit

2329 | n == tacN "Prim__IsTCName"

@@ -2549,7 +2549,7 @@ runTac autoSolve ist perhapsFC fn tac

2549 when autoSolve solveAll

2550 runT Compute = compute

2551 runT Trivial = do trivial' ist; when autoSolve solveAll

2552− runT TCInstance = runT (Exact (PResolveTC emptyFC))

2552+ runT TCImplementation = runT (Exact (PResolveTC emptyFC))

2553 runT (ProofSearch rec prover depth top psns hints)

2554 = do proofSearch' ist rec False depth prover top fn psns hints

2555 when autoSolve solveAll

@@ -2819,12 +2819,12 @@ processTacticDecls info steps =

2819 _ -> return ()

2820 -- TODO: inaccessible

2821

2822− RAddInstance interfaceName instName ->

2822+ RAddImplementation interfaceName implName ->

2823 do -- The interface resolution machinery relies on a special

2824− logElab 2 $ "Adding elab script instance " ++ show instName ++

2824+ logElab 2 $ "Adding elab script implementation " ++ show implName ++

2825− " for " ++ show interfaceName

2825+ " for " ++ show interfaceName

2826− addInstance False True interfaceName instName

2826+ addImplementation False True interfaceName implName

2827− addIBC (IBCInstance False True interfaceName instName)

2827+ addIBC (IBCImplementation False True interfaceName implName)

2828 RClausesInstrs n cs ->

2829 do logElab 3 $ "Pattern-matching definition from tactics: " ++ show n

2830 solveDeferred emptyFC n

src/Idris/ElabDecls.hs+3−3

@@ -35,7 +35,7 @@ import Idris.Elab.Clause

35import Idris.Elab.Data

36import Idris.Elab.Record

37import Idris.Elab.Interface

38−import Idris.Elab.Instance

38+import Idris.Elab.Implementation

39import Idris.Elab.Provider

40import Idris.Elab.RunElab

41import Idris.Elab.Transform

@@ -275,9 +275,9 @@ elabDecl' what info (PInterface doc s f cs n nfc ps pdocs fds ds cn cd)

275 | what /= EDefns

276 = do logElab 1 $ "Elaborating interface " ++ show n

277 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)

279 = 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

281elabDecl' what info (PRecord doc rsyn fc opts name nfc ps pdocs fs cname cdoc csyn)

282 = do logElab 1 $ "Elaborating record " ++ show name

283 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

252

253 -- get Deps for a Name

254 getDeps :: Name -> Deps

255− getDeps (SN (WhereN i (SN (InstanceCtorN interfaceN)) (MN i' field)))

255+ getDeps (SN (WhereN i (SN (ImplementationCtorN interfaceN)) (MN i' field)))

256− = M.empty -- these deps are created when applying instance ctors

256+ = M.empty -- these deps are created when applying implementation ctors

257 getDeps n = case lookupDefExact n ctx of

258 Just def -> getDepsDef n def

259 Nothing -> error $ "erasure checker: unknown reference: " ++ show n

@@ -336,9 +336,9 @@ buildDepMap ci used externs ctx startNames

336 -- this is safe because it's certainly a patvar

337 varIdx = fromJust (viFunArg var)

338

339− -- generate metamethod names, "n" is the instance ctor

339+ -- generate metamethod names, "n" is the implementation ctor

340 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)

342 | otherwise = \j -> Nothing

343

344 -- Named variables -> DeBruijn variables -> Conds/guards -> Term -> Deps

@@ -380,8 +380,8 @@ buildDepMap ci used externs ctx startNames

380 -- applications may add items to Cond

381 getDepsTerm vs bs cd app@(App _ _ _)

382 | (fun, args) <- unApply app = case fun of

383− -- instance constructors -> create metamethod deps

383+ -- implementation constructors -> create metamethod deps

384− P (DCon _ _ _) ctorName@(SN (InstanceCtorN interfaceName)) _

384+ P (DCon _ _ _) ctorName@(SN (ImplementationCtorN interfaceName)) _

385 -> conditionalDeps ctorName args -- regular data ctor stuff

386 `union` unionMap (methodDeps ctorName) (zip [0..] args) -- method-specific stuff

387

@@ -486,7 +486,7 @@ buildDepMap ci used externs ctx startNames

486 then length $ getArgTys (argTys !! i)

487 else error $ "invalid field number " ++ show i ++ " for " ++ show ctorName

488

489− | otherwise = error $ "unknown instance constructor: " ++ show ctorName

489+ | otherwise = error $ "unknown implementation constructor: " ++ show ctorName

490

491 getArity n = case lookupDefExact n ctx of

492 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

276 = case lookupCtxtExact n (idris_records i) of

277 Just v -> return f { ibc_records = (n,v): ibc_records f }

278 _ -> ifail "IBC write failed"

279−ibc i (IBCInstance int res n ins) f

279+ibc i (IBCImplementation int res n ins) f

280 = return f { ibc_implementations = (int, res, n, ins) : ibc_implementations f }

281ibc i (IBCDSL n) f

282 = case lookupCtxtExact n (idris_dsls i) of

@@ -392,7 +392,7 @@ process reexp phase archive fn = do

392 processStatics archive

393 processInterfaces archive

394 processRecords archive

395− processInstances archive

395+ processImplementations archive

396 processDSLs archive

397 processDatatypes archive

398 processOptimise archive

@@ -550,12 +550,12 @@ processInterfaces ar = do

550 cs <- getEntry [] "ibc_interfaces" ar

551 mapM_ (\ (n, c) -> do

552 i <- getIState

553− -- Don't lose instances from previous IBCs, which

553+ -- Don't lose implementations from previous IBCs, which

554 -- could have loaded in any order

555 let is = case lookupCtxtExact n (idris_interfaces i) of

556 Just (CI _ _ _ _ _ ins _) -> ins

557 _ -> []

558− let c' = c { interface_instances = interface_instances c ++ is }

558+ let c' = c { interface_implementations = interface_implementations c ++ is }

559 putIState (i { idris_interfaces = addDef n c' (idris_interfaces i) })) cs

560

561processRecords :: Archive -> Idris ()

@@ -564,10 +564,10 @@ processRecords ar = do

564 mapM_ (\ (n, r) ->

565 updateIState (\i -> i { idris_records = addDef n r (idris_records i) })) rs

566

567−processInstances :: Archive -> Idris ()

567+processImplementations :: Archive -> Idris ()

568−processInstances ar = do

568+processImplementations ar = do

569 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

571

572processDSLs :: Archive -> Idris ()

573processDSLs ar = do

@@ -1424,7 +1424,7 @@ instance (Binary t) => Binary (PDecl' t) where

1424 put x10

1425 put x11

1426 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 ->

1428 do putWord8 8

1429 put x1

1430 put x2

@@ -1563,7 +1563,7 @@ instance (Binary t) => Binary (PDecl' t) where

1563 x13 <- get

1564 x14 <- get

1565 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)

1567 9 -> do x1 <- get

1568 x2 <- get

1569 return (PDSL x1 x2)

@@ -2141,7 +2141,7 @@ instance (Binary t) => Binary (PTactic' t) where

2141 put x1

2142 put x2

2143 put x3

2144− TCInstance -> putWord8 31

2144+ TCImplementation -> putWord8 31

2145 GoalType x1 x2 -> do putWord8 32

2146 put x1

2147 put x2

@@ -2222,7 +2222,7 @@ instance (Binary t) => Binary (PTactic' t) where

2222 x2 <- get

2223 x3 <- get

2224 return (LetTacTy x1 x2 x3)

2225− 31 -> return TCInstance

2225+ 31 -> return TCImplementation

2226 32 -> do x1 <- get

2227 x2 <- get

2228 return (GoalType x1 x2)

src/Idris/IdrisDoc.hs+2−2

@@ -226,7 +226,7 @@ referredNss (n, Just d, _) =

226 getFunDocs (DataDoc f fs) = f:fs

227 getFunDocs (InterfaceDoc _ _ fs _ _ _ _ _) = fs

228 getFunDocs (RecordDoc _ _ f fs _) = f:fs

229− getFunDocs (NamedInstanceDoc _ fd) = [fd]

229+ getFunDocs (NamedImplementationDoc _ fd) = [fd]

230 getFunDocs (ModDoc _ _) = []

231 types (FD _ _ args t _) = t:(map second args)

232 second (_, x, _, _) = x

@@ -643,7 +643,7 @@ createOtherDoc ist (DataDoc fd@(FD n docstring args _ _) fds) = do

643 H.dt $ toHtml $ show name

644 H.dd $ Docstrings.renderHtml docstring

645

646−createOtherDoc ist (NamedInstanceDoc _ fd) = createFunDoc ist fd

646+createOtherDoc ist (NamedImplementationDoc _ fd) = createFunDoc ist fd

647

648createOtherDoc ist (ModDoc _ docstring) = do

649 Docstrings.renderHtml docstring

src/Idris/Interactive.hs+1−1

@@ -81,7 +81,7 @@ addClauseFrom fn updatefile l n = do

81 else iPrintResult cl

82 where

83 getIndent i n [] = 0

84− getIndent i n xs | take 9 xs == "instance " = i

84+ getIndent i n xs | take 9 xs == "implementation " = i

85 getIndent i n xs | take (length n) xs == n = i

86 getIndent i n (x : xs) = getIndent (i + 1) n xs

87

src/Idris/Package.hs+2−2

@@ -216,9 +216,9 @@ documentPkg copts fp = do

216 idrisMain opts

217 addImportDir (sourcedir pkgdesc)

218 load fs

219− idrisInstance <- run loader idrisInit

219+ idrisImplementation <- run loader idrisInit

220 setCurrentDirectory cd

221− case idrisInstance of

221+ case idrisImplementation of

222 Left err -> do

223 putStrLn $ pshow idrisInit err

224 exitWith (ExitFailure 1)

src/Idris/Parser.hs+63−63

@@ -180,7 +180,7 @@ Decl ::=

180 | Mutual

181 | Namespace

182 | Interface

183− | Instance

183+ | Implementation

184 | DSL

185 | Directive

186 | Provider

@@ -219,7 +219,7 @@ internalDecl syn

219 <|> fail "End of readable input"

220 where declBody :: Bool -> IdrisParser [PDecl]

221 declBody b =

222− try (instance_ True syn)

222+ try (implementation True syn)

223 <|> try (openInterface syn)

224 <|> declBody' b

225 <|> using_ syn

@@ -342,13 +342,13 @@ declExtension syn ns rules =

342 s

343 updateNs ns (PInterface docs s fc cs cn fc' ps pdocs pdets ds cname cdocs)

344 = PInterface docs s fc cs (updateB ns cn) fc' ps pdocs pdets

345− (map (updateNs ns) ds)

345+ (map (updateNs ns) ds)

346− (updateRecCon ns cname)

346+ (updateRecCon ns cname)

347− cdocs

347+ cdocs

348− updateNs ns (PInstance docs pdocs s fc cs pnames acc opts cn fc' ps pextra ity ni ds)

348+ updateNs ns (PImplementation 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'

349+ = PImplementation docs pdocs s fc cs pnames acc opts (updateB ns cn) fc'

350− ps pextra ity (fmap (updateB ns) ni)

350+ ps pextra ity (fmap (updateB ns) ni)

351− (map (updateNs ns) ds)

351+ (map (updateNs ns) ds)

352 updateNs ns (PMutual fc ds) = PMutual fc (map (updateNs ns) ds)

353 updateNs ns (PProvider docs s fc fc' pw n)

354 = PProvider docs s fc fc' pw (updateB ns n)

@@ -832,32 +832,32 @@ namespace syn =

832 return [PNamespace n nfc (concat ds)]

833 <?> "namespace declaration"

834

835−{-| Parses a methods block (for instances)

835+{-| Parses a methods block (for implementations)

836

837@

838− InstanceBlock ::= 'where' OpenBlock FnDecl* CloseBlock

838+ ImplementationBlock ::= 'where' OpenBlock FnDecl* CloseBlock

839@

840-}

841−instanceBlock :: SyntaxInfo -> IdrisParser [PDecl]

841+implementationBlock :: SyntaxInfo -> IdrisParser [PDecl]

842−instanceBlock syn = do reservedHL "where"

842+implementationBlock syn = do reservedHL "where"

843− openBlock

843+ openBlock

844− ds <- many (fnDecl syn)

844+ ds <- many (fnDecl syn)

845− closeBlock

845+ closeBlock

846− return (concat ds)

846+ return (concat ds)

847− <?> "implementation block"

847+ <?> "implementation block"

848

849−{-| Parses a methods and instances block (for interfaces)

849+{-| Parses a methods and implementations block (for interfaces)

850

851@

852−MethodOrInstance ::=

852+MethodOrImplementation ::=

853 FnDecl

854− | Instance

854+ | Implementation

855 ;

856@

857

858@

859InterfaceBlock ::=

860− 'where' OpenBlock Constructor? MethodOrInstance* CloseBlock

860+ 'where' OpenBlock Constructor? MethodOrImplementation* CloseBlock

861 ;

862@

863-}

@@ -871,7 +871,7 @@ interfaceBlock syn = do reservedHL "where"

871 ist <- get

872 let cd' = annotate syn ist cd

873

874− ds <- many (notEndBlock >> try (instance_ True syn)

874+ ds <- many (notEndBlock >> try (implementation True syn)

875 <|> do x <- data_ syn

876 return [x]

877 <|> fnDecl syn)

@@ -937,52 +937,52 @@ interface_ syn = do (doc, argDocs, acc)

937{-| Parses an interface implementation declaration

938

939@

940− Instance ::=

940+ Implementation ::=

941− DocComment_t? 'instance' InstanceName? ConstraintList? Name SimpleExpr* InstanceBlock?

941+ DocComment_t? 'implementation' ImplementationName? ConstraintList? Name SimpleExpr* ImplementationBlock?

942 ;

943@

944

945@

946−InstanceName ::= '[' Name ']';

946+ImplementationName ::= '[' Name ']';

947@

948-}

949−instance_ :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

949+implementation :: Bool -> SyntaxInfo -> IdrisParser [PDecl]

950−instance_ kwopt syn

950+implementation kwopt syn

951− = do ist <- get

951+ = do ist <- get

952− (doc, argDocs) <- docstring syn

952+ (doc, argDocs) <- docstring syn

953− (opts, acc) <- fnOpts

953+ (opts, acc) <- fnOpts

954− if kwopt then optional instanceKeyword

954+ if kwopt then optional implementationKeyword

955− else do instanceKeyword

955+ else do implementationKeyword

956− return (Just ())

956+ return (Just ())

957

958− fc <- getFC

958+ fc <- getFC

959− en <- optional instanceName

959+ en <- optional implementationName

960− cs <- constraintList syn

960+ cs <- constraintList syn

961− let cs' = [(c, ty) | (c, _, ty) <- cs]

961+ let cs' = [(c, ty) | (c, _, ty) <- cs]

962− (cn, cnfc) <- fnName

962+ (cn, cnfc) <- fnName

963− args <- many (simpleExpr syn)

963+ args <- many (simpleExpr syn)

964− let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

964+ let sc = PApp fc (PRef cnfc [cnfc] cn) (map pexp args)

965− let t = bindList (PPi constraint) cs sc

965+ let t = bindList (PPi constraint) cs sc

966− pnames <- instanceUsing

966+ pnames <- implementationUsing

967− ds <- instanceBlock syn

967+ ds <- implementationBlock syn

968− return [PInstance doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]

968+ return [PImplementation doc argDocs syn fc cs' pnames acc opts cn cnfc args [] t en ds]

969− <?> "implementation declaration"

969+ <?> "implementation declaration"

970− where instanceName :: IdrisParser Name

970+ where implementationName :: IdrisParser Name

971− instanceName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

971+ implementationName = do lchar '['; n_in <- fst <$> fnName; lchar ']'

972− let n = expandNS syn n_in

972+ let n = expandNS syn n_in

973− return n

973+ return n

974− <?> "implementation name"

974+ <?> "implementation name"

975− instanceKeyword :: IdrisParser ()

975+ implementationKeyword :: IdrisParser ()

976− instanceKeyword = reservedHL "implementation"

976+ implementationKeyword = reservedHL "implementation"

977− <|> do reservedHL "instance"

977+ <|> do reservedHL "instance"

978− fc <- getFC

978+ fc <- getFC

979− parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")

979+ parserWarning fc Nothing (Msg "The 'instance' keyword is deprecated. Use 'implementation' (or omit it) instead.")

980−

980+

981− instanceUsing :: IdrisParser [Name]

981+ implementationUsing :: IdrisParser [Name]

982− instanceUsing = do reservedHL "using"

982+ implementationUsing = do reservedHL "using"

983− ns <- sepBy1 fnName (lchar ',')

983+ ns <- sepBy1 fnName (lchar ',')

984− return (map fst ns)

984+ return (map fst ns)

985− <|> return []

985+ <|> return []

986

987-- | Parse a docstring

988docstring :: SyntaxInfo

@@ -1867,7 +1867,7 @@ loadSource lidr f toline

1867 PClauses{} -> r

1868 PInterface{} -> r

1869 PData{} -> r

1870− PInstance{} -> r

1870+ PImplementation{} -> r

1871 _ -> x

1872

1873 addModDoc :: SyntaxInfo -> [String] -> Docstring () -> Idris ()

src/Idris/Parser/Expr.hs+7−4

@@ -385,7 +385,7 @@ tacticsExpr syn = do kw <- reservedFC "tactics"

385SimpleExpr ::=

386 {- External (User-defined) Simple Expression -}

387 | '?' Name

388− | % 'instance'

388+ | % 'implementation'

389 | 'Refl' ('{' Expr '}')?

390 | ProofExpr

391 | TacticsExpr

@@ -409,7 +409,10 @@ simpleExpr syn =

409 try (simpleExternalExpr syn)

410 <|> do (x, FC f (l, c) end) <- try (lchar '?' *> name)

411 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)

413 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

416 <|> do reserved "elim_for"; fc <- getFC; t <- fst <$> fnName; return (PRef fc [] (SN $ ElimN t))

414 <|> proofExpr syn

417 <|> proofExpr syn

415 <|> tacticsExpr syn

418 <|> tacticsExpr syn

@@ -1467,7 +1470,7 @@ verbatimStringLiteral = token $ do (FC f start _) <- getFC

1467

1470

1468@

1471@

1469Static ::=

1472Static ::=

1470− '[' static ']'

1473+ '%static'

1471;

1474;

1472@

1475@

1473-}

1476-}

@@ -1582,7 +1585,7 @@ tactics =

1582 , (["search"], Nothing, const $

1585 , (["search"], Nothing, const $

1583 do depth <- option 10 $ fst <$> natural

1586 do depth <- option 10 $ fst <$> natural

1584 return (ProofSearch True True (fromInteger depth) Nothing [] []))

1587 return (ProofSearch True True (fromInteger depth) Nothing [] []))

1585− , noArgs ["instance"] TCInstance

1588+ , noArgs ["implementation"] TCImplementation

1586 , noArgs ["solve"] Solve

1589 , noArgs ["solve"] Solve

1587 , noArgs ["attack"] Attack

1590 , noArgs ["attack"] Attack

1588 , noArgs ["state", ":state"] ProofState

1591 , 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

715collect (PNamespace ns fc ps : ds) = PNamespace ns fc (collect ps) : collect ds

716collect (PInterface doc f s cs n nfc ps pdocs fds ds cn cd : ds')

717 = 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')

718+collect (PImplementation 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'

719+ = PImplementation doc argDocs f s cs pnames acc opts n nfc ps pextra t en (collect ds) : collect ds'

720collect (d : ds) = d : collect ds

721collect [] = []

src/Idris/ProofSearch.hs+6−6

@@ -352,7 +352,7 @@ proofSearch rec fromProver ambigok deferonfail maxDepth elab fn nroot psnames hi

352

353-- | Resolve interfaces. This will only pick up 'normal'

354-- implementations, never named implementations (which is enforced by

355−-- 'findInstances').

355+-- 'findImplementations').

356resolveTC :: Bool -- ^ using default Int

357 -> Bool -- ^ allow open implementations

358 -> Int -- ^ depth

@@ -407,8 +407,8 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

407 try' (trivialTCs okholes elab ist)

408 (do addDefault t tc ttypes

409 let stk = map fst (filter snd $ elab_stack ist)

410− let insts = idris_openimpls ist ++ findInstances ist t

410+ let impls = idris_openimpls ist ++ findImplementations ist t

411− blunderbuss t depth stk (stk ++ insts)) True

411+ blunderbuss t depth stk (stk ++ impls)) True

412

413 -- returns Just hs if okay, where hs are holes which are okay in the

414 -- goal, or Nothing if not okay to proceed

@@ -489,7 +489,7 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

489 = do lams <- introImps

490 t <- goal

491 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

493-- else do

494 -- if there's a hole in the goal, don't even try

495 let imps = case lookupCtxtName n (idris_implicits ist) of

@@ -522,8 +522,8 @@ resTC' tcs defaultOn openOK topholes depth topg fn elab ist

522

523-- | Find the names of implementations that have been designeated for

524-- searching (i.e. non-named implementations or implementations from Elab scripts)

525−findInstances :: IState -> Term -> [Name]

525+findImplementations :: IState -> Term -> [Name]

526−findInstances ist t

526+findImplementations ist t

527 | (P _ n _, _) <- unApply (getRetTy t)

528 = case lookupCtxt n (idris_interfaces ist) of

529 [CI _ _ _ _ _ ins _] ->

src/Idris/REPL.hs+2−2

@@ -904,8 +904,8 @@ process fn (NewDefn decls) = do

904 fixClauses :: PDecl' t -> PDecl' t

905 fixClauses (PClauses fc opts _ css@(clause:cs)) =

906 PClauses fc opts (getClauseName clause) css

907− fixClauses (PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName decls) =

907+ fixClauses (PImplementation doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty implName decls) =

908− PInstance doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty instName (map fixClauses decls)

908+ PImplementation doc argDocs syn fc constraints pnames acc opts cls nfc parms pextra ty implName (map fixClauses decls)

909 fixClauses decl = decl

910

911 info = recinfo (fileFC "toplevel")

src/Idris/Reflection.hs+13−13

@@ -84,7 +84,7 @@ tacN str = sNS (sUN str) ["Elab", "Reflection", "Language"]

84reify :: IState -> Term -> ElabD PTactic

85reify _ (P _ n _) | n == reflm "Intros" = return Intros

86reify _ (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

88reify _ (P _ n _) | n == reflm "Solve" = return Solve

89reify _ (P _ n _) | n == reflm "Compute" = return Compute

90reify _ (P _ n _) | n == reflm "Skip" = return Skip

@@ -257,10 +257,10 @@ reifyTTNameApp t [sn]

257 reifySN t [Constant (I i), n]

258 | t == reflm "WithN" = WithN i <$> reifyTTName n

259 reifySN t [n, ss]

260− | t == reflm "InstanceN" =

260+ | t == reflm "ImplementationN" =

261 case unList ss of

262− Nothing -> fail "Can't reify InstanceN strings"

262+ Nothing -> fail "Can't reify ImplementationN strings"

263− Just ss' -> InstanceN <$> reifyTTName n <*>

263+ Just ss' -> ImplementationN <$> reifyTTName n <*>

264 pure [T.pack s | Constant (Str s) <- ss']

265 reifySN t [n, Constant (Str s)]

266 | t == reflm "ParentN" =

@@ -275,8 +275,8 @@ reifyTTNameApp t [sn]

275 | t == reflm "ElimN" =

276 ElimN <$> reifyTTName n

277 reifySN t [n]

278− | t == reflm "InstanceCtorN" =

278+ | t == reflm "ImplementationCtorN" =

279− InstanceCtorN <$> reifyTTName n

279+ ImplementationCtorN <$> reifyTTName n

280 reifySN t [n1, n2]

281 | t == reflm "MetaN" =

282 MetaN <$> reifyTTName n1 <*> reifyTTName n2

@@ -699,11 +699,11 @@ reflectSpecialName (WhereN i n1 n2) =

699reflectSpecialName (WithN i n) = reflCall "WithN" [ RConstant (I i)

700 , reflectName n

701 ]

702−reflectSpecialName (InstanceN inst ss) =

702+reflectSpecialName (ImplementationN impl ss) =

703− reflCall "InstanceN" [ reflectName inst

703+ reflCall "ImplementationN" [ reflectName impl

704− , mkList (RConstant StrType) $

704+ , mkList (RConstant StrType) $

705− map (RConstant . Str . T.unpack) ss

705+ map (RConstant . Str . T.unpack) ss

706− ]

706+ ]

707reflectSpecialName (ParentN n s) =

708 reflCall "ParentN" [reflectName n, RConstant (Str (T.unpack s))]

709reflectSpecialName (MethodN n) =

@@ -712,8 +712,8 @@ reflectSpecialName (CaseN fc n) =

712 reflCall "CaseN" [reflectFC (unwrapFC fc), reflectName n]

713reflectSpecialName (ElimN n) =

714 reflCall "ElimN" [reflectName n]

715−reflectSpecialName (InstanceCtorN n) =

715+reflectSpecialName (ImplementationCtorN n) =

716− reflCall "InstanceCtorN" [reflectName n]

716+ reflCall "ImplementationCtorN" [reflectName n]

717reflectSpecialName (MetaN parent meta) =

718 reflCall "MetaN" [reflectName parent, reflectName meta]

719

src/Idris/TypeSearch.hs+12−12

@@ -30,7 +30,7 @@ import qualified Data.Text as T (pack, isPrefixOf)

30import Data.Traversable (traverse)

31

32import Idris.AbsSyntax (addUsingConstraints, addImpl, getIState, putIState, implicit, logLvl)

33−import Idris.AbsSyntaxTree (interface_instances, InterfaceInfo, defaultSyntax, eqTy, Idris

33+import Idris.AbsSyntaxTree (interface_implementations, InterfaceInfo, defaultSyntax, eqTy, Idris

34 , IState (idris_interfaces, idris_docstrings, tt_ctxt, idris_outputmode),

35 implicitAllowed, OutputMode(..), PTerm, toplevel)

36import Idris.Core.Evaluate (Context (definitions), Def (Function, TyDecl, CaseOp), normaliseC)

@@ -443,11 +443,11 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

443 guard $ scoreCriterion (score state')

444 unifyQueue state' (queue ++ queueAdditions)

445

446− possInterfaceInstances :: [Name] -> Type -> [Type]

446+ possInterfaceImplementations :: [Name] -> Type -> [Type]

447− possInterfaceInstances usedns ty = do

447+ possInterfaceImplementations usedns ty = do

448 interfaceName <- getInterfaceName clss

449 interfaceDef <- lookupCtxt interfaceName interfaceInfo

450− n <- interface_instances interfaceDef

450+ n <- interface_implementations interfaceDef

451 def <- lookupCtxt (fst n) (definitions ctxt)

452 nty <- normaliseC ctxt [] <$> (case typeFromDef def of Just x -> [x]; Nothing -> [])

453 let ty' = vToP (uniqueBinders usedns nty)

@@ -489,7 +489,7 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

489 scoreAcc usedns) [(ty1, ty2)]

490 | (n1, ty1) <- c1, (n2, ty2) <- c2, let subst2for1 = psubst n2 (P Bound n1 ty1)]

491

492− -- try to hunt match an interface constraint by replacing it with an instance

492+ -- try to hunt match an interface constraint by replacing it with an implementation

493 results4 = [ State [] (both (\(cs, _, _) -> ([], cs)) sds)

494 (scoreAcc `mappend` Score 0 0 (both (\(_, amods, _) -> amods) sds))

495 (usedns ++ sided (++) (both (\(_, _, hs) -> hs) sds))

@@ -497,17 +497,17 @@ matchTypesBulk istate maxScore type1 types = getAllResults startQueueOfQueues wh

497 where

498 allMods = parallel defMod mods

499 mods :: Sided [( Interfaces, AsymMods, [Name] )]

500− mods = both (instanceMods . snd) unresolved

500+ mods = both (implementationMods . snd) unresolved

501 defMod :: Sided (Interfaces, AsymMods, [Name])

502 defMod = both (\(_, cs) -> (cs, mempty , [])) unresolved

503 parallel :: Sided a -> Sided [a] -> [Sided a]

504 parallel (Sided l r) (Sided ls rs) = map (flip Sided r) ls ++ map (Sided l) rs

505− instanceMods :: Interfaces -> [( Interfaces , AsymMods, [Name] )]

505+ implementationMods :: Interfaces -> [( Interfaces , AsymMods, [Name] )]

506− instanceMods interfaces = [ ( newInterfaceArgs, mempty { interfaceApp = 1 }, newHoles )

506+ implementationMods interfaces = [ ( newInterfaceArgs, mempty { interfaceApp = 1 }, newHoles )

507− | (_, ty) <- interfaces

507+ | (_, ty) <- interfaces

508− , inst <- possInterfaceInstances usedns ty

508+ , impl <- possInterfaceImplementations usedns ty

509− , newInterfaceArgs <- maybeToList $ interfaceUnify interfaceInfo ctxt ty inst

509+ , newInterfaceArgs <- maybeToList $ interfaceUnify interfaceInfo ctxt ty impl

510− , let newHoles = map fst newInterfaceArgs ]

510+ , let newHoles = map fst newInterfaceArgs ]

511

512

513 -- Stage 1 - match arguments

test/docs003/expected+2−2

@@ -28,11 +28,11 @@ Named implementations:

28Child interfaces:

29 Traversable f

30 Applicative f

31−Named instance:

31+Named implementation:

32 docs003.mine : Functor List

33

34

35−Named instance:

35+Named implementation:

36 docs003.another : Functor List

37 More functors!

38

test/proof010/proof010.idr+6−6

@@ -1,24 +1,24 @@

1data MyShow : Type -> Type where

2− ShowInstance : (show : a -> String) -> MyShow a

2+ ShowImplementation : (show : a -> String) -> MyShow a

3

4myshow : {auto inst : MyShow a} -> a -> String

5−myshow {inst = ShowInstance show} x1 = show x1

5+myshow {inst = ShowImplementation show} x1 = show x1

6

7%hint

8showNat : MyShow Nat

9−showNat = ShowInstance show

9+showNat = ShowImplementation show

10

11%hint

12showFn : MyShow (a -> b)

13−showFn = ShowInstance (\x => "<< function >>")

13+showFn = ShowImplementation (\x => "<< function >>")

14

15%hint

16showBools : MyShow (Bool, Bool)

17−showBools = ShowInstance (\x => "some bools")

17+showBools = ShowImplementation (\x => "some bools")

18

19%hint

20showStuff : MyShow a -> MyShow b -> MyShow (a, b)

21−showStuff sa sb = ShowInstance showPair

21+showStuff sa sb = ShowImplementation showPair

22 where

23 showPair : (a, b) -> String

24 showPair (x, y) = myshow x ++ ", " ++ myshow y