4d0a065 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Change "class/instance" keywords

To "interface/implementation". Old syntax is still valid but gives a deprecation warning.

commit4d0a065f86c06a3215caf1f1b6969ea7b193d849 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 13 Jan 2016, 11:18 (11 years ago) parent79ff02f

130 files changed+772−753

compare with master

unifiedsplit

CHANGELOG+3

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

11New in 0.9.21:

22==============

4+* 'class' and 'instance' are now deprecated keywords. They have been

5+ replaced by 'interface' and 'implementation' respectively. This is to

6+ properly reflect their purpose.

47* Idris' logging infrastructure has been categorised. Command line and repl

58 are available. For command line the option `--logging-categories CATS`

69 is used to pass in the categories. Here `CATS` is a colon separated quoted

libs/base/Control/Arrow.idr+13−13

@@ -11,7 +11,7 @@ infixr 3 &&&

1111infixr 2 +++

1212infixr 2 \|/

1313

14−class Category arr => Arrow (arr : Type -> Type -> Type) where

14+interface Category arr => Arrow (arr : Type -> Type -> Type) where

1515 arrow : (a -> b) -> arr a b

1616 first : arr a b -> arr (a, c) (b, c)

1717

@@ -26,14 +26,14 @@ class Category arr => Arrow (arr : Type -> Type -> Type) where

2626 dup : x -> (x,x)

2727 dup x = (x,x)

2828

29−instance Arrow Morphism where

29+implementation Arrow Morphism where

3030 arrow f = Mor f

3131 first (Mor f) = Mor $ \(a, b) => (f a, b)

3232 second (Mor f) = Mor $ \(a, b) => (a, f b)

3333 (Mor f) *** (Mor g) = Mor $ \(a, b) => (f a, g b)

3434 (Mor f) &&& (Mor g) = Mor $ \a => (f a, g a)

3535

36−instance Monad m => Arrow (Kleislimorphism m) where

36+implementation Monad m => Arrow (Kleislimorphism m) where

3737 arrow f = Kleisli (return . f)

3838 first (Kleisli f) = Kleisli $ \(a, b) => do x <- f a

3939 return (x, b)

@@ -49,13 +49,13 @@ instance Monad m => Arrow (Kleislimorphism m) where

4949 y <- g a

5050 return (x, y)

5151

52−class Arrow arr => ArrowZero (arr : Type -> Type -> Type) where

52+interface Arrow arr => ArrowZero (arr : Type -> Type -> Type) where

5353 zeroArrow : arr a b

5454

55−class ArrowZero arr => ArrowPlus (arr : Type -> Type -> Type) where

55+interface ArrowZero arr => ArrowPlus (arr : Type -> Type -> Type) where

5656 (<++>) : arr a b -> arr a b -> arr a b

5757

58−class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where

58+interface Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where

5959 left : arr a b -> arr (Either a c) (Either b c)

6060

6161 right : arr a b -> arr (Either c a) (Either c b)

@@ -67,16 +67,16 @@ class Arrow arr => ArrowChoice (arr : Type -> Type -> Type) where

6767 (\|/) : arr a b -> arr c b -> arr (Either a c) b

6868 f \|/ g = f +++ g >>> arrow fromEither

6969

70−instance Monad m => ArrowChoice (Kleislimorphism m) where

70+implementation Monad m => ArrowChoice (Kleislimorphism m) where

7171 left f = f +++ (arrow id)

7272 right f = (arrow id) +++ f

7373 f +++ g = (f >>> (arrow Left)) \|/ (g >>> (arrow Right))

7474 (Kleisli f) \|/ (Kleisli g) = Kleisli (either f g)

7575

76−class Arrow arr => ArrowApply (arr : Type -> Type -> Type) where

76+interface Arrow arr => ArrowApply (arr : Type -> Type -> Type) where

7777 app : arr (arr a b, a) b

7878

79−instance Monad m => ArrowApply (Kleislimorphism m) where

79+implementation Monad m => ArrowApply (Kleislimorphism m) where

8080 app = Kleisli $ \(Kleisli f, x) => f x

8181

8282data ArrowMonad : (Type -> Type -> Type) -> Type -> Type where

@@ -85,16 +85,16 @@ data ArrowMonad : (Type -> Type -> Type) -> Type -> Type where

8585runArrowMonad : ArrowMonad arr a -> arr (the Type ()) a

8686runArrowMonad (MkArrowMonad a) = a

8787

88−instance Arrow a => Functor (ArrowMonad a) where

88+implementation Arrow a => Functor (ArrowMonad a) where

8989 map f (MkArrowMonad m) = MkArrowMonad $ m >>> arrow f

9090

91−instance Arrow a => Applicative (ArrowMonad a) where

91+implementation Arrow a => Applicative (ArrowMonad a) where

9292 pure x = MkArrowMonad $ arrow $ \_ => x

9393 (MkArrowMonad f) <*> (MkArrowMonad x) = MkArrowMonad $ f &&& x >>> arrow (uncurry id)

9494

95−instance ArrowApply a => Monad (ArrowMonad a) where

95+implementation ArrowApply a => Monad (ArrowMonad a) where

9696 (MkArrowMonad m) >>= f =

9797 MkArrowMonad $ m >>> (arrow $ \x => (runArrowMonad (f x), ())) >>> app

9898

99−class Arrow arr => ArrowLoop (arr : Type -> Type -> Type) where

99+interface Arrow arr => ArrowLoop (arr : Type -> Type -> Type) where

100100 loop : arr (Pair a c) (Pair b c) -> arr a b

libs/base/Control/Catchable.idr+5−5

@@ -2,30 +2,30 @@ module Control.Catchable

33import Control.IOExcept

5−class Catchable (m : Type -> Type) t where

5+interface Catchable (m : Type -> Type) t where

66 throw : t -> m a

77 catch : m a -> (t -> m a) -> m a

9−instance Catchable Maybe () where

9+implementation Catchable Maybe () where

1010 catch Nothing h = h ()

1111 catch (Just x) h = Just x

1212

1313 throw () = Nothing

1414

15−instance Catchable (Either a) a where

15+implementation Catchable (Either a) a where

1616 catch (Left err) h = h err

1717 catch (Right x) h = (Right x)

1818

1919 throw = Left

2020

21−instance Catchable (IOExcept err) err where

21+implementation Catchable (IOExcept err) err where

2222 catch (IOM prog) h = IOM (do p' <- prog

2323 case p' of

2424 Left e => let IOM he = h e in he

2525 Right val => return (Right val))

2626 throw = ioe_fail

2727

28−instance Catchable List () where

28+implementation Catchable List () where

2929 catch [] h = h ()

3030 catch xs h = xs

3131

libs/base/Control/Category.idr+4−4

@@ -4,17 +4,17 @@ import Data.Morphisms

55%access public

7−class Category (cat : Type -> Type -> Type) where

7+interface Category (cat : Type -> Type -> Type) where

88 id : cat a a

99 (.) : cat b c -> cat a b -> cat a c

1010

11−instance Category Morphism where

11+implementation Category Morphism where

1212 id = Mor id

1313 -- disambiguation needed below, because unification can now get further

14− -- here with Category.(.) and it's only type class resolution that fails!

14+ -- here with Category.(.) and it's only interface resolution that fails!

1515 (Mor f) . (Mor g) = with Basics (Mor (f . g))

1616

17−instance Monad m => Category (Kleislimorphism m) where

17+implementation Monad m => Category (Kleislimorphism m) where

1818 id = Kleisli (return . id)

1919 (Kleisli f) . (Kleisli g) = Kleisli $ \a => g a >>= f

2020

libs/base/Control/IOExcept.idr+3−3

@@ -6,14 +6,14 @@ record IOExcept err a where

66 constructor IOM

77 runIOExcept : IO (Either err a)

9−instance Functor (IOExcept e) where

9+implementation Functor (IOExcept e) where

1010 map f (IOM fn) = IOM (map (map f) fn)

1111

12−instance Applicative (IOExcept e) where

12+implementation Applicative (IOExcept e) where

1313 pure x = IOM (pure (pure x))

1414 (IOM f) <*> (IOM a) = IOM [| f <*> a |]

1515

16−instance Monad (IOExcept e) where

16+implementation Monad (IOExcept e) where

1717 (IOM x) >>= f = IOM $ x >>= either (pure . Left) (runIOExcept . f)

1818

1919ioe_lift : IO a -> IOExcept err a

libs/base/Control/Monad/Identity.idr+3−3

@@ -4,13 +4,13 @@ public record Identity (a : Type) where

44 constructor Id

55 runIdentity : a

7−instance Functor Identity where

7+implementation Functor Identity where

88 map fn (Id a) = Id (fn a)

10−instance Applicative Identity where

10+implementation Applicative Identity where

1111 pure x = Id x

1212

1313 (Id f) <*> (Id g) = Id (f g)

1414

15−instance Monad Identity where

15+implementation Monad Identity where

1616 (Id x) >>= k = k x

libs/base/Control/Monad/RWS.idr+9−9

@@ -8,46 +8,46 @@ import Control.Monad.Reader

88%access public

1010||| A combination of the Reader, Writer, and State monads

11−class (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}

11+interface (Monoid w, MonadReader r m, MonadWriter w m, MonadState s m) => MonadRWS r w s (m : Type -> Type) where {}

1212

1313||| The transformer on which the RWS monad is based

1414record RWST (r : Type) (w : Type) (s : Type) (m : Type -> Type) (a : Type) where

1515 constructor MkRWST

1616 runRWST : r -> s -> m (a, s, w)

1717

18−instance Monad m => Functor (RWST r w s m) where

18+implementation Monad m => Functor (RWST r w s m) where

1919 map f (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s

2020 return (f a, s', w)

2121

22−instance (Monoid w, Monad m) => Applicative (RWST r w s m) where

22+implementation (Monoid w, Monad m) => Applicative (RWST r w s m) where

2323 pure a = MkRWST $ \_,s => return (a, s, neutral)

2424 (MkRWST f) <*> (MkRWST v) = MkRWST $ \r,s => do (a, s', w) <- v r s

2525 (fn, ss, w') <- f r s

2626 return (fn a, ss, w <+> w')

2727

28−instance (Monoid w, Monad m) => Monad (RWST r w s m) where

28+implementation (Monoid w, Monad m) => Monad (RWST r w s m) where

2929 (MkRWST m) >>= k = MkRWST $ \r,s => do (a, s', w) <- m r s

3030 let MkRWST ka = k a

3131 (b, ss, w') <- ka r s'

3232 return (b, ss, w <+> w')

3333

34−instance (Monoid w, Monad m) => MonadReader r (RWST r w s m) where

34+implementation (Monoid w, Monad m) => MonadReader r (RWST r w s m) where

3535 ask = MkRWST $ \r,s => return (r, s, neutral)

3636 local f (MkRWST m) = MkRWST $ \r,s => m (f r) s

3737

38−instance (Monoid w, Monad m) => MonadWriter w (RWST r w s m) where

38+implementation (Monoid w, Monad m) => MonadWriter w (RWST r w s m) where

3939 tell w = MkRWST $ \_,s => return ((), s, w)

4040 listen (MkRWST m) = MkRWST $ \r,s => do (a, s', w) <- m r s

4141 return ((a, w), s', w)

4242 pass (MkRWST m) = MkRWST $ \r,s => do ((a, f), s', w) <- m r s

4343 return (a, s', f w)

4444

45−instance (Monoid w, Monad m) => MonadState s (RWST r w s m) where

45+implementation (Monoid w, Monad m) => MonadState s (RWST r w s m) where

4646 get = MkRWST $ \_,s => return (s, s, neutral)

4747 put s = MkRWST $ \_,_ => return ((), s, neutral)

4848

49−instance (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}

49+implementation (Monoid w, Monad m) => MonadRWS r w s (RWST r w s m) where {}

5050

51−||| The RWS monad. See the MonadRWS class

51+||| The RWS monad. See the MonadRWS interface

5252RWS : Type -> Type -> Type -> Type -> Type

5353RWS r w s a = RWST r w s Identity a

libs/base/Control/Monad/Reader.idr+7−7

@@ -7,7 +7,7 @@ import Control.Monad.Trans

77%access public

99||| A monad representing a computation that runs in an immutable context

10−class Monad m => MonadReader r (m : Type -> Type) where

10+interface Monad m => MonadReader r (m : Type -> Type) where

1111 ||| Return the context

1212 ask : m r

1313 ||| Temprorarily modify the input and run an action in the new context

@@ -22,27 +22,27 @@ record ReaderT (r : Type) (m : Type -> Type) (a : Type) where

2222liftReaderT : {m : Type -> Type} -> m a -> ReaderT r m a

2323liftReaderT m = RD $ const m

2424

25−instance Functor f => Functor (ReaderT r f) where

25+implementation Functor f => Functor (ReaderT r f) where

2626 map f (RD g) = RD $ (map f) . g

2727

28−instance Applicative m => Applicative (ReaderT r m) where

28+implementation Applicative m => Applicative (ReaderT r m) where

2929 pure = liftReaderT . pure

3030 (RD f) <*> (RD v) = RD $ \r => f r <*> v r

3131

32−instance Alternative m => Alternative (ReaderT r m) where

32+implementation Alternative m => Alternative (ReaderT r m) where

3333 empty = liftReaderT empty

3434 (RD m) <|> (RD n) = RD $ \r => m r <|> n r

3535

36−instance Monad m => Monad (ReaderT r m) where

36+implementation Monad m => Monad (ReaderT r m) where

3737 (RD f) >>= k = RD $ \r => do a <- f r

3838 let RD ka = k a

3939 ka r

4040

41−instance Monad m => MonadReader r (ReaderT r m) where

41+implementation Monad m => MonadReader r (ReaderT r m) where

4242 ask = RD return

4343 local f (RD m) = RD $ m . f

4444

45−instance MonadTrans (ReaderT r) where

45+implementation MonadTrans (ReaderT r) where

4646 lift x = RD (const x)

4747

4848||| Evaluate a function in the context of a Reader monad

libs/base/Control/Monad/State.idr+7−7

@@ -6,7 +6,7 @@ import public Control.Monad.Trans

66%access public

88||| A computation which runs in a context and produces an output

9−class Monad m => MonadState s (m : Type -> Type) | m where

9+interface Monad m => MonadState s (m : Type -> Type) | m where

1010 ||| Get the context

1111 get : m s

1212 ||| Write a new context/output

@@ -17,28 +17,28 @@ record StateT (s : Type) (m : Type -> Type) (a : Type) where

1717 constructor ST

1818 runStateT : s -> m (a, s)

1919

20−instance Functor f => Functor (StateT s f) where

20+implementation Functor f => Functor (StateT s f) where

2121 map f (ST g) = ST (\st => map (mapFst f) (g st)) where

2222 mapFst : (a -> x) -> (a, s) -> (x, s)

2323 mapFst fn (a, b) = (fn a, b)

2424

25−instance Monad f => Applicative (StateT s f) where

25+implementation Monad f => Applicative (StateT s f) where

2626 pure x = ST (\st => pure (x, st))

2727

2828 (ST f) <*> (ST a) = ST (\st => do (g, r) <- f st

2929 (b, t) <- a r

3030 return (g b, t))

3131

32−instance Monad m => Monad (StateT s m) where

32+implementation Monad m => Monad (StateT s m) where

3333 (ST f) >>= k = ST (\st => do (v, st') <- f st

3434 let ST kv = k v

3535 kv st')

3636

37−instance Monad m => MonadState s (StateT s m) where

37+implementation Monad m => MonadState s (StateT s m) where

3838 get = ST (\x => return (x, x))

3939 put x = ST (\y => return ((), x))

4040

41−instance MonadTrans (StateT s) where

41+implementation MonadTrans (StateT s) where

4242 lift x = ST (\st => do r <- x

4343 return (r, st))

4444

@@ -52,7 +52,7 @@ gets : MonadState s m => (s -> a) -> m a

5252gets f = do s <- get

5353 return (f s)

5454

55−||| The State monad. See the MonadState class

55+||| The State monad. See the MonadState interface

5656State : Type -> Type -> Type

5757State s a = StateT s Identity a

5858

libs/base/Control/Monad/Trans.idr+1−1

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

11module Control.Monad.Trans

3−class MonadTrans (t : (Type -> Type) -> Type -> Type) where

3+interface MonadTrans (t : (Type -> Type) -> Type -> Type) where

44 lift : Monad m => m a -> t m a

libs/base/Control/Monad/Writer.idr+8−8

@@ -7,7 +7,7 @@ import Control.Monad.Trans

77%access public

99||| A monad representing a computation that produces a stream of output

10−class (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where

10+interface (Monoid w, Monad m) => MonadWriter w (m : Type -> Type) where

1111 ||| tell w produces the output w

1212 tell : w -> m ()

1313 ||| Execute an action and add it's output to the value of the computation

@@ -20,32 +20,32 @@ record WriterT (w : Type) (m : Type -> Type) (a : Type) where

2020 constructor WR

2121 runWriterT : m (a, w)

2222

23−instance Functor f => Functor (WriterT w f) where

23+implementation Functor f => Functor (WriterT w f) where

2424 map f (WR g) = WR $ map (\w => (f . fst $ w, snd w)) g

2525

26−instance (Monoid w, Applicative m) => Applicative (WriterT w m) where

26+implementation (Monoid w, Applicative m) => Applicative (WriterT w m) where

2727 pure a = WR $ pure (a, neutral)

2828 (WR f) <*> (WR v) = WR $ liftA2 merge f v where

2929 merge (fn, w) (a, w') = (fn a, w <+> w')

3030

31−instance (Monoid w, Alternative m) => Alternative (WriterT w m) where

31+implementation (Monoid w, Alternative m) => Alternative (WriterT w m) where

3232 empty = WR empty

3333 (WR m) <|> (WR n) = WR $ m <|> n

3434

35−instance (Monoid w, Monad m) => Monad (WriterT w m) where

35+implementation (Monoid w, Monad m) => Monad (WriterT w m) where

3636 (WR m) >>= k = WR $ do (a, w) <- m

3737 let WR ka = k a

3838 (b, w') <- ka

3939 return (b, w <+> w')

4040

41−instance (Monoid w, Monad m) => MonadWriter w (WriterT w m) where

41+implementation (Monoid w, Monad m) => MonadWriter w (WriterT w m) where

4242 tell w = WR $ return ((), w)

4343 listen (WR m) = WR $ do (a, w) <- m

4444 return ((a, w), w)

4545 pass (WR m) = WR $ do ((a, f), w) <- m

4646 return (a, f w)

4747

48−instance Monoid w => MonadTrans (WriterT w) where

48+implementation Monoid w => MonadTrans (WriterT w) where

4949 lift x = WR $ do r <- x

5050 return (r, neutral)

5151

@@ -61,6 +61,6 @@ censor : MonadWriter w m => (w -> w) -> m a -> m a

6161censor f m = pass $ do a <- m

6262 return (a, f)

6363

64−||| The Writer monad itself. See the MonadWriter class

64+||| The Writer monad itself. See the MonadWriter interface

6565Writer : Type -> Type -> Type

6666Writer w a = WriterT w Identity a

libs/base/Data/Bits.idr+5−5

@@ -273,10 +273,10 @@ gt {n=n} x y with (nextBytes n)

273273 | S (S Z) = prim__gtB32 x y

274274 | S (S (S _)) = prim__gtB64 x y

275275

276−instance Eq (Bits n) where

276+implementation Eq (Bits n) where

277277 (MkBits x) == (MkBits y) = boolOp eq x y

278278

279−instance Ord (Bits n) where

279+implementation Ord (Bits n) where

280280 (MkBits x) < (MkBits y) = boolOp lt x y

281281 (MkBits x) <= (MkBits y) = boolOp lte x y

282282 (MkBits x) >= (MkBits y) = boolOp gte x y

@@ -338,7 +338,7 @@ public

338338intToBits : Integer -> Bits n

339339intToBits n = MkBits (intToBits' n)

340340

341−instance Cast Integer (Bits n) where

341+implementation Cast Integer (Bits n) where

342342 cast = intToBits

343343

344344bitsToInt' : machineTy (nextBytes n) -> Integer

@@ -356,7 +356,7 @@ bitsToInt (MkBits x) = bitsToInt' x

356356zeroUnused : machineTy (nextBytes n) -> machineTy (nextBytes n)

357357zeroUnused {n} x = x `and'` complement' (intToBits' {n=n} 0)

358358

359−--instance Cast Nat (Bits n) where

359+--implementation Cast Nat (Bits n) where

360360-- cast x = MkBits (zeroUnused (natToBits n))

361361

362362-- TODO: Prove

@@ -437,6 +437,6 @@ bitsToStr x = pack (helper last x)

437437 helper FZ _ = []

438438 helper (FS x) b = (if getBit x b then '1' else '0') :: helper (weaken x) b

439439

440−instance Show (Bits n) where

440+implementation Show (Bits n) where

441441 show = bitsToStr

442442

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

@@ -16,10 +16,10 @@ realPart (r:+i) = r

1616imagPart : Complex a -> a

1717imagPart (r:+i) = i

1818

19−instance Eq a => Eq (Complex a) where

19+implementation Eq a => Eq (Complex a) where

2020 (==) a b = realPart a == realPart b && imagPart a == imagPart b

2121

22−instance Show a => Show (Complex a) where

22+implementation Show a => Show (Complex a) where

2323 showPrec d (r :+ i) = showParens (d >= plus_i) $ showPrec plus_i r ++ " :+ " ++ showPrec plus_i i

2424 where plus_i : Prec

2525 plus_i = User 6

@@ -28,7 +28,7 @@ instance Show a => Show (Complex a) where

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

2929-- we can do:

3030{-

31−instance Fractional a => Fractional (Complex a) where

31+implementation Fractional a => Fractional (Complex a) where

3232 (/) (a:+b) (c:+d) = let

3333 real = (a*c+b*d)/(c*c+d*d)

3434 imag = (b*c-a*d)/(c*c+d*d)

@@ -58,17 +58,17 @@ phase (x:+y) = atan2 y x

5858conjugate : Neg a => Complex a -> Complex a

5959conjugate (r:+i) = (r :+ (0-i))

6060

61−instance Functor Complex where

61+implementation Functor Complex where

6262 map f (r :+ i) = f r :+ f i

6363

64−-- We can't do "instance Num a => Num (Complex a)" because

64+-- We can't do "implementation Num a => Num (Complex a)" because

6565-- we need "abs" which needs "magnitude" which needs "sqrt" which needs Double

66−instance Num (Complex Double) where

66+implementation Num (Complex Double) where

6767 (+) (a:+b) (c:+d) = ((a+c):+(b+d))

6868 (*) (a:+b) (c:+d) = ((a*c-b*d):+(b*c+a*d))

6969 fromInteger x = (fromInteger x:+0)

7070

71−instance Neg (Complex Double) where

71+implementation Neg (Complex Double) where

7272 negate = map negate

7373 (-) (a:+b) (c:+d) = ((a-c):+(b-d))

7474 abs (a:+b) = (magnitude (a:+b):+0)

libs/base/Data/Erased.idr+3−3

@@ -11,14 +11,14 @@ data Erased : Type -> Type where

1111 ||| Construct an erased value from any value.

1212 Erase : .(x : a) -> Erased a

1313

14−instance Functor Erased where

14+implementation Functor Erased where

1515 map f (Erase x) = Erase (f x)

1616

17−instance Applicative Erased where

17+implementation Applicative Erased where

1818 pure = Erase

1919 (<*>) (Erase f) (Erase x) = Erase (f x)

2020

21−instance Monad Erased where

21+implementation Monad Erased where

2222 (>>=) (Erase x) f = f x

2323

2424||| Project the erased value out of the monad.

libs/base/Data/Fin.idr+9−9

@@ -12,14 +12,14 @@ data Fin : (n : Nat) -> Type where

1212 FZ : Fin (S k)

1313 FS : Fin k -> Fin (S k)

1414

15−instance Uninhabited (Fin Z) where

15+implementation Uninhabited (Fin Z) where

1616 uninhabited FZ impossible

1717 uninhabited (FS f) impossible

1818

1919FSInjective : (m : Fin k) -> (n : Fin k) -> FS m = FS n -> m = n

2020FSInjective left _ Refl = Refl

2121

22−instance Eq (Fin n) where

22+implementation Eq (Fin n) where

2323 (==) FZ FZ = True

2424 (==) (FS k) (FS k') = k == k'

2525 (==) _ _ = False

@@ -44,7 +44,7 @@ finToNatInjective FZ (FS n) Refl impossible

4444finToNatInjective (FS m) (FS n) prf =

4545 cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))

4646

47−instance Cast (Fin n) Nat where

47+implementation Cast (Fin n) Nat where

4848 cast x = finToNat x

4949

5050||| Convert a Fin to an Integer

@@ -52,7 +52,7 @@ finToInteger : Fin n -> Integer

5252finToInteger FZ = 0

5353finToInteger (FS k) = 1 + finToInteger k

5454

55−instance Cast (Fin n) Integer where

55+implementation Cast (Fin n) Integer where

5656 cast x = finToInteger x

5757

5858||| Weaken the bound on a Fin by 1

@@ -89,16 +89,16 @@ last {n=S _} = FS last

8989total FSinjective : {f : Fin n} -> {f' : Fin n} -> (FS f = FS f') -> f = f'

9090FSinjective Refl = Refl

9191

92−instance Ord (Fin n) where

92+implementation Ord (Fin n) where

9393 compare FZ FZ = EQ

9494 compare FZ (FS _) = LT

9595 compare (FS _) FZ = GT

9696 compare (FS x) (FS y) = compare x y

9797

98−instance MinBound (Fin (S n)) where

98+implementation MinBound (Fin (S n)) where

9999 minBound = FZ

100100

101−instance MaxBound (Fin (S n)) where

101+implementation MaxBound (Fin (S n)) where

102102 maxBound = last

103103

104104

@@ -174,7 +174,7 @@ finFromIntegerErrors _ = Nothing

174174

175175%error_handlers Data.Fin.fromInteger prf finFromIntegerErrors

176176

177−instance Enum (Fin (S n)) where

177+implementation Enum (Fin (S n)) where

178178 pred FZ = FZ

179179 pred (FS n) = weaken n

180180 succ n = case strengthen (FS n) of

@@ -192,7 +192,7 @@ instance Enum (Fin (S n)) where

192192total FZNotFS : {f : Fin n} -> FZ {k = n} = FS f -> Void

193193FZNotFS Refl impossible

194194

195−instance DecEq (Fin n) where

195+implementation DecEq (Fin n) where

196196 decEq FZ FZ = Yes Refl

197197 decEq FZ (FS f) = No FZNotFS

198198 decEq (FS f) FZ = No $ negEqSym FZNotFS

libs/base/Data/HVect.idr+8−8

@@ -35,10 +35,10 @@ updateAt (FS j) f (x::xs) = x :: updateAt j f xs

3535(++) [] ys = ys

3636(++) (x::xs) ys = x :: (xs ++ ys)

3737

38−instance Eq (HVect []) where

38+implementation Eq (HVect []) where

3939 [] == [] = True

4040

41−instance (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where

41+implementation (Eq t, Eq (HVect ts)) => Eq (HVect (t::ts)) where

4242 (x::xs) == (y::ys) = x == y && xs == ys

4343

4444total

@@ -49,26 +49,26 @@ total

4949hvectInjective2 : {xs, ys: HVect ts} -> {x, y:a} -> x :: xs = y :: ys -> xs = ys

5050hvectInjective2 Refl = Refl

5151

52−instance DecEq (HVect []) where

52+implementation DecEq (HVect []) where

5353 decEq [] [] = Yes Refl

5454

55−instance (DecEq t, DecEq (HVect ts)) => DecEq (HVect (t::ts)) where

55+implementation (DecEq t, DecEq (HVect ts)) => DecEq (HVect (t::ts)) where

5656 decEq (x::xs) (y::ys) with (decEq x y)

5757 decEq (z::xs) (z::ys) | Yes Refl with (decEq xs ys)

5858 decEq (z::zs) (z::zs) | Yes Refl | Yes Refl = Yes Refl

5959 decEq (z::xs) (z::ys) | Yes Refl | No ctr = No (ctr . hvectInjective2)

6060 decEq (x::xs) (y::ys) | No ctr = No (ctr . hvectInjective1)

6161

62−class Shows (k : Nat) (ts : Vect k Type) where

62+interface Shows (k : Nat) (ts : Vect k Type) where

6363 shows : HVect ts -> Vect k String

6464

65−instance Shows Z [] where

65+implementation Shows Z [] where

6666 shows [] = []

6767

68−instance (Show t, Shows k ts) => Shows (S k) (t::ts) where

68+implementation (Show t, Shows k ts) => Shows (S k) (t::ts) where

6969 shows (x::xs) = show x :: shows xs

7070

71−instance (Shows k ts) => Show (HVect ts) where

71+implementation (Shows k ts) => Show (HVect ts) where

7272 show xs = "[" ++ (pack . intercalate [','] . map unpack . toList $ shows xs) ++ "]"

7373

7474||| Extract an arbitrary element of the correct type.

libs/base/Data/List.idr+2−2

@@ -15,7 +15,7 @@ data Elem : a -> List a -> Type where

1515 ||| Example: `the (Elem "b" ["a", "b"]) (There Here)`

1616 There : Elem x xs -> Elem x (y :: xs)

1717

18−instance Uninhabited (Elem {a} x []) where

18+implementation Uninhabited (Elem {a} x []) where

1919 uninhabited Here impossible

2020 uninhabited (There p) impossible

2121

@@ -49,7 +49,7 @@ dropElem (x :: ys) (There p) = x :: dropElem ys p

4949intersectBy : (a -> a -> Bool) -> List a -> List a -> List a

5050intersectBy eq xs ys = [x | x <- xs, any (eq x) ys]

5151

52−||| Compute the intersection of two lists according to their `Eq` instance.

52+||| Compute the intersection of two lists according to their `Eq` implementation.

5353|||

5454||| ```idris example

5555||| intersect [1, 2, 3, 4] [2, 4, 6, 8]

libs/base/Data/List/Quantifiers.idr+1−1

@@ -16,7 +16,7 @@ anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void

1616anyNilAbsurd (Here _) impossible

1717anyNilAbsurd (There _) impossible

1818

19−instance Uninhabited (Any p Nil) where

19+implementation Uninhabited (Any p Nil) where

2020 uninhabited = anyNilAbsurd

2121

2222||| Eliminator for `Any`

libs/base/Data/Mod2.idr+6−6

@@ -28,25 +28,25 @@ public

2828intToMod : {n : Nat} -> Integer -> Mod2 n

2929intToMod {n=n} x = MkMod2 (intToBits x)

3030

31−instance Eq (Mod2 n) where

31+implementation Eq (Mod2 n) where

3232 (==) = modComp (==)

3333

34−instance Ord (Mod2 n) where

34+implementation Ord (Mod2 n) where

3535 (<) = modComp (<)

3636 (<=) = modComp (<=)

3737 (>=) = modComp (>=)

3838 (>) = modComp (>)

3939 compare = modComp compare

4040

41−instance Num (Mod2 n) where

41+implementation Num (Mod2 n) where

4242 (+) = modBin plus

4343 (*) = modBin times

4444 fromInteger = intToMod

4545

46−instance Cast (Mod2 n) (Bits n) where

46+implementation Cast (Mod2 n) (Bits n) where

4747 cast (MkMod2 x) = x

4848

49−instance Cast (Bits n) (Mod2 n) where

49+implementation Cast (Bits n) (Mod2 n) where

5050 cast x = MkMod2 x

5151

5252modToStr : Mod2 n -> String

@@ -58,5 +58,5 @@ modToStr x = pack (reverse (helper x))

5858 :: (if x < 10 then [] else helper (x `div` 10))

5959

6060

61−instance Show (Mod2 n) where

61+implementation Show (Mod2 n) where

6262 show = modToStr

libs/base/Data/Morphisms.idr+5−5

@@ -20,20 +20,20 @@ applyMor (Mor f) a = f a

2020applyEndo : Endomorphism a -> a -> a

2121applyEndo (Endo f) a = f a

2222

23−instance Functor (Morphism r) where

23+implementation Functor (Morphism r) where

2424 map f (Mor a) = Mor (f . a)

2525

26−instance Applicative (Morphism r) where

26+implementation Applicative (Morphism r) where

2727 pure a = Mor $ const a

2828 (Mor f) <*> (Mor a) = Mor $ \r => f r $ a r

2929

30−instance Monad (Morphism r) where

30+implementation Monad (Morphism r) where

3131 (Mor h) >>= f = Mor $ \r => applyMor (f $ h r) r

3232

33−instance Semigroup (Endomorphism a) where

33+implementation Semigroup (Endomorphism a) where

3434 (Endo f) <+> (Endo g) = Endo $ g . f

3535

36−instance Monoid (Endomorphism a) where

36+implementation Monoid (Endomorphism a) where

3737 neutral = Endo id

3838

3939infixr 1 ~>

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

@@ -14,7 +14,7 @@ module Data.So

1414data So : Bool -> Type where

1515 Oh : So True

1616

17−instance Uninhabited (So False) where

17+implementation Uninhabited (So False) where

1818 uninhabited Oh impossible

1919

2020||| Perform a case analysis on a Boolean, providing clients with a `So` proof

libs/base/Data/Vect.idr+10−10

@@ -232,7 +232,7 @@ unzip3 ((l,c,r)::xs) with (unzip3 xs)

232232-- Equality

233233--------------------------------------------------------------------------------

234234

235−instance (Eq a) => Eq (Vect n a) where

235+implementation (Eq a) => Eq (Vect n a) where

236236 (==) [] [] = True

237237 (==) (x::xs) (y::ys) = x == y && xs == ys

238238

@@ -241,7 +241,7 @@ instance (Eq a) => Eq (Vect n a) where

241241-- Order

242242--------------------------------------------------------------------------------

243243

244−instance Ord a => Ord (Vect n a) where

244+implementation Ord a => Ord (Vect n a) where

245245 compare [] [] = EQ

246246 compare (x::xs) (y::ys) = compare x y `thenCompare` compare xs ys

247247

@@ -250,7 +250,7 @@ instance Ord a => Ord (Vect n a) where

250250-- Maps

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

252252

253−instance Functor (Vect n) where

253+implementation Functor (Vect n) where

254254 map f [] = []

255255 map f (x::xs) = f x :: map f xs

256256

@@ -281,7 +281,7 @@ foldrImpl : (t -> acc -> acc) -> acc -> (acc -> acc) -> Vect n t -> acc

281281foldrImpl f e go [] = go e

282282foldrImpl f e go (x::xs) = foldrImpl f e (go . (f x)) xs

283283

284−instance Foldable (Vect n) where

284+implementation Foldable (Vect n) where

285285 foldr f e xs = foldrImpl f e id xs

286286

287287--------------------------------------------------------------------------------

@@ -501,17 +501,17 @@ transpose (x :: xs) = zipWith (::) x (transpose xs)

501501-- Applicative/Monad/Traversable

502502--------------------------------------------------------------------------------

503503

504−instance Applicative (Vect k) where

504+implementation Applicative (Vect k) where

505505 pure = replicate _

506506

507507 fs <*> vs = zipWith apply fs vs

508508

509509||| This monad is different from the List monad, (>>=)

510510||| uses the diagonal.

511−instance Monad (Vect n) where

511+implementation Monad (Vect n) where

512512 m >>= f = diag (map f m)

513513

514−instance Traversable (Vect n) where

514+implementation Traversable (Vect n) where

515515 traverse f [] = pure Vect.Nil

516516 traverse f (x::xs) = [| Vect.(::) (f x) (traverse f xs) |]

517517

@@ -519,7 +519,7 @@ instance Traversable (Vect n) where

519519-- Show

520520--------------------------------------------------------------------------------

521521

522−instance Show a => Show (Vect n a) where

522+implementation Show a => Show (Vect n a) where

523523 show = show . toList

524524

525525--------------------------------------------------------------------------------

@@ -549,7 +549,7 @@ vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

549549vectInjective2 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> xs = ys

550550vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

551551

552−instance DecEq a => DecEq (Vect n a) where

552+implementation DecEq a => DecEq (Vect n a) where

553553 decEq [] [] = Yes Refl

554554 decEq (x :: xs) (y :: ys) with (decEq x y)

555555 decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)

@@ -558,7 +558,7 @@ instance DecEq a => DecEq (Vect n a) where

558558 decEq (x :: xs) (y :: ys) | No neq = No (neq . vectInjective1)

559559

560560{- The following definition is elaborated in a wrong case-tree. Examination pending.

561−instance DecEq a => DecEq (Vect n a) where

561+implementation DecEq a => DecEq (Vect n a) where

562562 decEq [] [] = Yes Refl

563563 decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)

564564 decEq (x :: xs) (x :: xs) | (Yes Refl, Yes Refl) = Yes Refl

libs/base/Data/Vect/Quantifiers.idr+1−1

@@ -16,7 +16,7 @@ anyNilAbsurd : {P : a -> Type} -> Any P Nil -> Void

1616anyNilAbsurd (Here _) impossible

1717anyNilAbsurd (There _) impossible

1818

19−instance Uninhabited (Any p Nil) where

19+implementation Uninhabited (Any p Nil) where

2020 uninhabited = anyNilAbsurd

2121

2222||| Eliminator for `Any`

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

@@ -61,14 +61,14 @@ binderTy (Guess t1 t2) = t1

6161binderTy (PVar t) = t

6262binderTy (PVTy t) = t

6363

64−instance Show SourceLocation where

64+implementation Show SourceLocation where

6565 showPrec d (FileLoc filename line col) = showCon d "FileLoc" $ showArg filename ++ showArg line ++ showArg col

6666

67−instance Eq SourceLocation where

67+implementation Eq SourceLocation where

6868 (FileLoc fn s e) == (FileLoc fn' s' e') = fn == fn' && s == s' && e == e'

6969

7070mutual

71− instance Show SpecialName where

71+ implementation Show SpecialName where

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

7373 showArg n1 ++ showArg n2

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

@@ -80,21 +80,21 @@ mutual

8080 showPrec d (InstanceCtorN n) = showCon d "InstanceCtorN" $ showArg n

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

8282

83− instance Show TTName where

83+ implementation Show TTName where

8484 showPrec d (UN str) = showCon d "UN" $ showArg str

8585 showPrec d (NS n ns) = showCon d "NS" $ showArg n ++ showArg ns

8686 showPrec d (MN i str) = showCon d "MN" $ showArg i ++ showArg str

8787 showPrec d (SN sn) = showCon d "SN" $ assert_total (showArg sn)

8888

8989mutual

90− instance Eq TTName where

90+ implementation Eq TTName where

9191 (UN str1) == (UN str2) = str1 == str2

9292 (NS n ns) == (NS n' ns') = n == n' && ns == ns'

9393 (MN i str) == (MN i' str') = i == i' && str == str'

9494 (SN sn) == (SN sn') = assert_total $ sn == sn'

9595 x == y = False

9696

97− instance Eq SpecialName where

97+ implementation Eq SpecialName where

9898 (WhereN i n1 n2) == (WhereN i' n1' n2') = i == i' && n1 == n1' && n2 == n2'

9999 (WithN i n) == (WithN i' n') = i == i' && n == n'

100100 (InstanceN i ss) == (InstanceN i' ss') = i == i' && ss == ss'

@@ -106,32 +106,32 @@ mutual

106106 (MetaN parent meta) == (MetaN parent' meta') = parent == parent' && meta == meta'

107107 _ == _ = False

108108

109−instance Show TTUExp where

109+implementation Show TTUExp where

110110 showPrec d (UVar i) = showCon d "UVar" $ showArg i

111111 showPrec d (UVal i) = showCon d "UVal" $ showArg i

112112

113−instance Eq TTUExp where

113+implementation Eq TTUExp where

114114 (UVar i) == (UVar j) = i == j

115115 (UVal i) == (UVal j) = i == j

116116 x == y = False

117117

118−instance Show NativeTy where

118+implementation Show NativeTy where

119119 show IT8 = "IT8"

120120 show IT16 = "IT16"

121121 show IT32 = "IT32"

122122 show IT64 = "IT64"

123123

124−instance Show IntTy where

124+implementation Show IntTy where

125125 showPrec d (ITFixed t) = showCon d "ITFixed" $ showArg t

126126 showPrec d ITNative = "ITNative"

127127 showPrec d ITBig = "ITBig"

128128 showPrec d ITChar = "ITChar"

129129

130−instance Show ArithTy where

130+implementation Show ArithTy where

131131 showPrec d (ATInt t) = showCon d "ATInt" $ showArg t

132132 showPrec d ATDouble = "ATDouble"

133133

134−instance Show Const where

134+implementation Show Const where

135135 showPrec d (I i) = showCon d "I" $ showArg i

136136 showPrec d (BI n) = showCon d "BI" $ showArg n

137137 showPrec d (Fl f) = showCon d "Fl" $ showArg f

@@ -146,26 +146,26 @@ instance Show Const where

146146 showPrec d VoidType = "VoidType"

147147 showPrec d Forgot = "Forgot"

148148

149−instance Eq NativeTy where

149+implementation Eq NativeTy where

150150 IT8 == IT8 = True

151151 IT16 == IT16 = True

152152 IT32 == IT32 = True

153153 IT64 == IT64 = True

154154 _ == _ = False

155155

156−instance Eq Reflection.IntTy where

156+implementation Eq Reflection.IntTy where

157157 (ITFixed x) == (ITFixed y) = x == y

158158 ITNative == ITNative = True

159159 ITBig == ITBig = True

160160 ITChar == ITChar = True

161161 _ == _ = False

162162

163−instance Eq ArithTy where

163+implementation Eq ArithTy where

164164 (ATInt x) == (ATInt y) = x == y

165165 ATDouble == ATDouble = True

166166 _ == _ = False

167167

168−instance Eq Const where

168+implementation Eq Const where

169169 (I x) == (I y) = x == y

170170 (BI x) == (BI y) = x == y

171171 (Fl x) == (Fl y) = x == y

@@ -182,20 +182,20 @@ instance Eq Const where

182182 _ == _ = False

183183

184184

185−instance Show NameType where

185+implementation Show NameType where

186186 showPrec d Bound = "Bound"

187187 showPrec d Ref = "Ref"

188188 showPrec d (DCon t ar) = showCon d "DCon" $ showArg t ++ showArg ar

189189 showPrec d (TCon t ar) = showCon d "TCon" $ showArg t ++ showArg ar

190190

191−instance Eq NameType where

191+implementation Eq NameType where

192192 Bound == Bound = True

193193 Ref == Ref = True

194194 (DCon t ar) == (DCon t' ar') = t == t' && ar == ar'

195195 (TCon t ar) == (TCon t' ar') = t == t' && ar == ar'

196196 x == y = False

197197

198−instance (Show a) => Show (Binder a) where

198+implementation (Show a) => Show (Binder a) where

199199 showPrec d (Lam t) = showCon d "Lam" $ showArg t

200200 showPrec d (Pi t1 t2) = showCon d "Pi" $ showArg t1 ++ showArg t2

201201 showPrec d (Let t1 t2) = showCon d "Let" $ showArg t1 ++ showArg t2

@@ -205,7 +205,7 @@ instance (Show a) => Show (Binder a) where

205205 showPrec d (PVar t) = showCon d "PVar" $ showArg t

206206 showPrec d (PVTy t) = showCon d "PVTy" $ showArg t

207207

208−instance (Eq a) => Eq (Binder a) where

208+implementation (Eq a) => Eq (Binder a) where

209209 (Lam t) == (Lam t') = t == t'

210210 (Pi t k) == (Pi t' k') = t == t' && k == k'

211211 (Let t1 t2) == (Let t1' t2') = t1 == t1' && t2 == t2'

@@ -216,7 +216,7 @@ instance (Eq a) => Eq (Binder a) where

216216 (PVTy t) == (PVTy t') = t == t'

217217 x == y = False

218218

219−instance Show TT where

219+implementation Show TT where

220220 showPrec = my_show

221221 where %assert_total my_show : Prec -> TT -> String

222222 my_show d (P nt n t) = showCon d "P" $ showArg nt ++ showArg n ++ showArg t

@@ -227,7 +227,7 @@ instance Show TT where

227227 my_show d Erased = "Erased"

228228 my_show d (TType u) = showCon d "TType" $ showArg u

229229

230−instance Eq TT where

230+implementation Eq TT where

231231 a == b = equalp a b

232232 where %assert_total equalp : TT -> TT -> Bool

233233 equalp (P nt n t) (P nt' n' t') = nt == nt' && n == n' && t == t'

@@ -239,7 +239,7 @@ instance Eq TT where

239239 equalp (TType u) (TType u') = u == u'

240240 equalp x y = False

241241

242−instance Eq Universe where

242+implementation Eq Universe where

243243 Reflection.NullType == Reflection.NullType = True

244244 Reflection.UniqueType == Reflection.UniqueType = True

245245 Reflection.AllTypes == Reflection.AllTypes = True

@@ -269,7 +269,7 @@ forget tm = fe [] tm

269269 fe env (UType uni) = Just (RUType uni)

270270 fe env Erased = Just $ RConstant Forgot

271271

272−instance Show Raw where

272+implementation Show Raw where

273273 showPrec = my_show

274274 where %assert_total my_show : Prec -> Raw -> String

275275 my_show d (Var n) = showCon d "Var" $ showArg n

@@ -279,7 +279,7 @@ instance Show Raw where

279279 my_show d (RConstant c) = showCon d "RConstant" $ showArg c

280280

281281

282−instance Show Err where

282+implementation Show Err where

283283 showPrec d (Msg x) = showCon d "Msg" $ showArg x

284284 showPrec d (InternalMsg x) = showCon d "InternalMsg" $ showArg x

285285 showPrec d (CantUnify x tm tm' err xs y) = showCon d "CantUnify" $ showArg x ++

@@ -329,28 +329,28 @@ pure = id

329329--------------------------------------

330330-- Instances for definition reflection

331331--------------------------------------

332−instance Show Erasure where

332+implementation Show Erasure where

333333 show Erased = "Erased"

334334 show NotErased = "NotErased"

335335

336−instance Show Plicity where

336+implementation Show Plicity where

337337 show Explicit = "Explicit"

338338 show Implicit = "Implicit"

339339 show Constraint = "Constraint"

340340

341−instance Show FunArg where

341+implementation Show FunArg where

342342 showPrec d (MkFunArg n ty plic era) = showCon d "MkFunArg" $ showArg n ++

343343 showArg ty ++ showArg plic ++ showArg era

344344

345−instance Show CtorArg where

345+implementation Show CtorArg where

346346 showPrec d (CtorParameter fa) = showCon d "CtorParameter" $ showArg fa

347347 showPrec d (CtorField fa) = showCon d "CtorField" $ showArg fa

348348

349−instance Show TyDecl where

349+implementation Show TyDecl where

350350 showPrec d (Declare fn args ret) = showCon d "Declare" $ showArg fn ++

351351 showArg args ++ showArg ret

352352

353−instance Show tm => Show (FunClause tm) where

353+implementation Show tm => Show (FunClause tm) where

354354 showPrec d (MkFunClause lhs rhs) =

355355 showCon d "MkFunClause" $ showArg lhs ++ showArg rhs

356356 showPrec d (MkImpossibleClause lhs) =

libs/contrib/Classes/Verified.idr+23−23

@@ -6,18 +6,18 @@ import Control.Algebra.VectorSpace

77-- Due to these being basically unused and difficult to implement,

88-- they're in contrib for a bit. Once a design is found that lets them

9−-- be implemented for a number of instances, and we get those

9+-- be implemented for a number of implementations, and we get those

1010-- implementations, then some of them can move back to base (or even

1111-- prelude, in the cases of Functor, Applicative, Monad, Semigroup,

1212-- and Monoid).

1313

14−class Functor f => VerifiedFunctor (f : Type -> Type) where

14+interface Functor f => VerifiedFunctor (f : Type -> Type) where

1515 functorIdentity : {a : Type} -> (x : f a) -> map id x = id x

1616 functorComposition : {a : Type} -> {b : Type} -> (x : f a) ->

1717 (g1 : a -> b) -> (g2 : b -> c) ->

1818 map (g2 . g1) x = (map g2 . map g1) x

1919

20−class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

20+interface (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Type) where

2121 applicativeMap : (x : f a) -> (g : a -> b) ->

2222 map g x = pure g <*> x

2323 applicativeIdentity : (x : f a) -> pure Basics.id <*> x = x

@@ -28,7 +28,7 @@ class (Applicative f, VerifiedFunctor f) => VerifiedApplicative (f : Type -> Typ

2828 applicativeInterchange : (x : a) -> (g : f (a -> b)) ->

2929 g <*> pure x = pure (\g' : a -> b => g' x) <*> g

3030

31−class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

31+interface (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

3232 monadApplicative : (mf : m (a -> b)) -> (mx : m a) ->

3333 mf <*> mx = mf >>= \f =>

3434 mx >>= \x =>

@@ -39,76 +39,76 @@ class (Monad m, VerifiedApplicative m) => VerifiedMonad (m : Type -> Type) where

3939 (mx >>= f) >>= g = mx >>= (\x => f x >>= g)

4040

4141

42−class Semigroup a => VerifiedSemigroup a where

42+interface Semigroup a => VerifiedSemigroup a where

4343 total semigroupOpIsAssociative : (l, c, r : a) -> l <+> (c <+> r) = (l <+> c) <+> r

4444

45−instance VerifiedSemigroup (List a) where

45+implementation VerifiedSemigroup (List a) where

4646 semigroupOpIsAssociative = appendAssociative

4747

48−--instance VerifiedSemigroup Nat where

48+--implementation VerifiedSemigroup Nat where

4949-- semigroupOpIsAssociative = plusAssociative

5050

5151

52−class (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

52+interface (VerifiedSemigroup a, Monoid a) => VerifiedMonoid a where

5353 total monoidNeutralIsNeutralL : (l : a) -> l <+> Algebra.neutral = l

5454 total monoidNeutralIsNeutralR : (r : a) -> Algebra.neutral <+> r = r

5555

56−-- instance VerifiedMonoid Nat where

56+-- implementation VerifiedMonoid Nat where

5757-- monoidNeutralIsNeutralL = plusZeroRightNeutral

5858-- monoidNeutralIsNeutralR = plusZeroLeftNeutral

5959

60−instance VerifiedMonoid (List a) where

60+implementation VerifiedMonoid (List a) where

6161 monoidNeutralIsNeutralL = appendNilRightNeutral

6262 monoidNeutralIsNeutralR xs = Refl

6363

64−class (VerifiedMonoid a, Group a) => VerifiedGroup a where

64+interface (VerifiedMonoid a, Group a) => VerifiedGroup a where

6565 total groupInverseIsInverseL : (l : a) -> l <+> inverse l = Algebra.neutral

6666 total groupInverseIsInverseR : (r : a) -> inverse r <+> r = Algebra.neutral

6767

68−class (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

68+interface (VerifiedGroup a, AbelianGroup a) => VerifiedAbelianGroup a where

6969 total abelianGroupOpIsCommutative : (l, r : a) -> l <+> r = r <+> l

7070

71−class (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

71+interface (VerifiedAbelianGroup a, Ring a) => VerifiedRing a where

7272 total ringOpIsAssociative : (l, c, r : a) -> l <.> (c <.> r) = (l <.> c) <.> r

7373 total ringOpIsDistributiveL : (l, c, r : a) -> l <.> (c <+> r) = (l <.> c) <+> (l <.> r)

7474 total ringOpIsDistributiveR : (l, c, r : a) -> (l <+> c) <.> r = (l <.> r) <+> (c <.> r)

7575

76−class (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

76+interface (VerifiedRing a, RingWithUnity a) => VerifiedRingWithUnity a where

7777 total ringWithUnityIsUnityL : (l : a) -> l <.> Algebra.unity = l

7878 total ringWithUnityIsUnityR : (r : a) -> Algebra.unity <.> r = r

7979

80−--class (VerifiedRingWithUnity a, Field a) => VerifiedField a where

80+--interface (VerifiedRingWithUnity a, Field a) => VerifiedField a where

8181-- total fieldInverseIsInverseL : (l : a) -> (notId : Not (l = neutral)) -> l <.> (inverseM l notId) = Algebra.unity

8282-- total fieldInverseIsInverseR : (r : a) -> (notId : Not (r = neutral)) -> (inverseM r notId) <.> r = Algebra.unity

8383

8484

85−class JoinSemilattice a => VerifiedJoinSemilattice a where

85+interface JoinSemilattice a => VerifiedJoinSemilattice a where

8686 total joinSemilatticeJoinIsAssociative : (l, c, r : a) -> join l (join c r) = join (join l c) r

8787 total joinSemilatticeJoinIsCommutative : (l, r : a) -> join l r = join r l

8888 total joinSemilatticeJoinIsIdempotent : (e : a) -> join e e = e

8989

90−class MeetSemilattice a => VerifiedMeetSemilattice a where

90+interface MeetSemilattice a => VerifiedMeetSemilattice a where

9191 total meetSemilatticeMeetIsAssociative : (l, c, r : a) -> meet l (meet c r) = meet (meet l c) r

9292 total meetSemilatticeMeetIsCommutative : (l, r : a) -> meet l r = meet r l

9393 total meetSemilatticeMeetIsIdempotent : (e : a) -> meet e e = e

9494

95−class (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

95+interface (VerifiedJoinSemilattice a, BoundedJoinSemilattice a) => VerifiedBoundedJoinSemilattice a where

9696 total boundedJoinSemilatticeBottomIsBottom : (e : a) -> join e Algebra.bottom = e

9797

98−class (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

98+interface (VerifiedMeetSemilattice a, BoundedMeetSemilattice a) => VerifiedBoundedMeetSemilattice a where

9999 total boundedMeetSemilatticeTopIsTop : (e : a) -> meet e Algebra.top = e

100100

101−class (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

101+interface (VerifiedJoinSemilattice a, VerifiedMeetSemilattice a) => VerifiedLattice a where

102102 total latticeMeetAbsorbsJoin : (l, r : a) -> meet l (join l r) = l

103103 total latticeJoinAbsorbsMeet : (l, r : a) -> join l (meet l r) = l

104104

105−class (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }

105+interface (VerifiedBoundedJoinSemilattice a, VerifiedBoundedMeetSemilattice a, VerifiedLattice a) => VerifiedBoundedLattice a where { }

106106

107107

108−--class (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

108+--interface (VerifiedRingWithUnity a, VerifiedAbelianGroup b, Module a b) => VerifiedModule a b where

109109-- total moduleScalarMultiplyComposition : (x,y : a) -> (v : b) -> x <#> (y <#> v) = (x <.> y) <#> v

110110-- total moduleScalarUnityIsUnity : (v : b) -> Algebra.unity {a} <#> v = v

111111-- total moduleScalarMultDistributiveWRTVectorAddition : (s : a) -> (v, w : b) -> s <#> (v <+> w) = (s <#> v) <+> (s <#> w)

112112-- total moduleScalarMultDistributiveWRTModuleAddition : (s, t : a) -> (v : b) -> (s <+> t) <#> v = (s <#> v) <+> (t <#> v)

113113

114−--class (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}

114+--interface (VerifiedField a, VerifiedModule a b) => VerifiedVectorSpace a b where {}

libs/contrib/Control/Algebra.idr+5−5

@@ -15,7 +15,7 @@ infixl 7 <.>

1515||| + Inverse for `<+>`:

1616||| forall a, a <+> inverse a == neutral

1717||| forall a, inverse a <+> a == neutral

18−class Monoid a => Group a where

18+interface Monoid a => Group a where

1919 inverse : a -> a

2020

2121(<->) : Group a => a -> a -> a

@@ -35,7 +35,7 @@ class Monoid a => Group a where

3535||| + Inverse for `<+>`:

3636||| forall a, a <+> inverse a == neutral

3737||| forall a, inverse a <+> a == neutral

38−class Group a => AbelianGroup a where { }

38+interface Group a => AbelianGroup a where { }

3939

4040||| Sets equipped with two binary operations, one associative and commutative

4141||| supplied with a neutral element, and the other associative, with

@@ -57,7 +57,7 @@ class Group a => AbelianGroup a where { }

5757||| + Distributivity of `<.>` and `<+>`:

5858||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

5959||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

60−class AbelianGroup a => Ring a where

60+interface AbelianGroup a => Ring a where

6161 (<.>) : a -> a -> a

6262

6363||| Sets equipped with two binary operations, one associative and commutative

@@ -83,7 +83,7 @@ class AbelianGroup a => Ring a where

8383||| + Distributivity of `<.>` and `<+>`:

8484||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

8585||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

86−class Ring a => RingWithUnity a where

86+interface Ring a => RingWithUnity a where

8787 unity : a

8888

8989||| Sets equipped with two binary operations – both associative, commutative and

@@ -112,7 +112,7 @@ class Ring a => RingWithUnity a where

112112||| + Distributivity of `<.>` and `<+>`:

113113||| forall a b c, a <.> (b <+> c) == (a <.> b) <+> (a <.> c)

114114||| forall a b c, (a <+> b) <.> c == (a <.> c) <+> (b <.> c)

115−class RingWithUnity a => Field a where

115+interface RingWithUnity a => Field a where

116116 inverseM : (x : a) -> Not (x = Algebra.neutral) -> a

117117

118118sum' : (Foldable t, Monoid a) => t a -> a

libs/contrib/Control/Algebra/Lattice.idr+11−11

@@ -15,13 +15,13 @@ import Data.Heap

1515||| forall a, join a a == a

1616|||

1717||| Join semilattices capture the notion of sets with a "least upper bound".

18−class JoinSemilattice a where

18+interface JoinSemilattice a where

1919 join : a -> a -> a

2020

21−instance JoinSemilattice Nat where

21+implementation JoinSemilattice Nat where

2222 join = maximum

2323

24−instance Ord a => JoinSemilattice (MaxiphobicHeap a) where

24+implementation Ord a => JoinSemilattice (MaxiphobicHeap a) where

2525 join = merge

2626

2727||| Sets equipped with a binary operation that is commutative, associative and

@@ -35,10 +35,10 @@ instance Ord a => JoinSemilattice (MaxiphobicHeap a) where

3535||| forall a, meet a a == a

3636|||

3737||| Meet semilattices capture the notion of sets with a "greatest lower bound".

38−class MeetSemilattice a where

38+interface MeetSemilattice a where

3939 meet : a -> a -> a

4040

41−instance MeetSemilattice Nat where

41+implementation MeetSemilattice Nat where

4242 meet = minimum

4343

4444||| Sets equipped with a binary operation that is commutative, associative and

@@ -56,10 +56,10 @@ instance MeetSemilattice Nat where

5656|||

5757||| Join semilattices capture the notion of sets with a "least upper bound"

5858||| equipped with a "bottom" element.

59−class JoinSemilattice a => BoundedJoinSemilattice a where

59+interface JoinSemilattice a => BoundedJoinSemilattice a where

6060 bottom : a

6161

62−instance BoundedJoinSemilattice Nat where

62+implementation BoundedJoinSemilattice Nat where

6363 bottom = Z

6464

6565||| Sets equipped with a binary operation that is commutative, associative and

@@ -77,7 +77,7 @@ instance BoundedJoinSemilattice Nat where

7777|||

7878||| Meet semilattices capture the notion of sets with a "greatest lower bound"

7979||| equipped with a "top" element.

80−class MeetSemilattice a => BoundedMeetSemilattice a where

80+interface MeetSemilattice a => BoundedMeetSemilattice a where

8181 top : a

8282

8383||| Sets equipped with two binary operations that are both commutative,

@@ -96,9 +96,9 @@ class MeetSemilattice a => BoundedMeetSemilattice a where

9696||| + Absorbtion laws for meet and join:

9797||| forall a b, meet a (join a b) == a

9898||| forall a b, join a (meet a b) == a

99−class (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }

99+interface (JoinSemilattice a, MeetSemilattice a) => Lattice a where { }

100100

101−instance Lattice Nat where { }

101+implementation Lattice Nat where { }

102102

103103||| Sets equipped with two binary operations that are both commutative,

104104||| associative and idempotent and supplied with neutral elements, along with

@@ -120,4 +120,4 @@ instance Lattice Nat where { }

120120||| + Neutral for meet and join:

121121||| forall a, meet a top == top

122122||| forall a, join a bottom == bottom

123−class (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }

123+interface (BoundedJoinSemilattice a, BoundedMeetSemilattice a) => BoundedLattice a where { }

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

@@ -8,106 +8,106 @@ import Data.Complex

88import Data.ZZ

1010

11−instance Semigroup Integer where

11+implementation Semigroup Integer where

1212 (<+>) = (+)

1313

14−instance Monoid Integer where

14+implementation Monoid Integer where

1515 neutral = 0

1616

17−instance Group Integer where

17+implementation Group Integer where

1818 inverse = (* -1)

1919

20−instance AbelianGroup Integer

20+implementation AbelianGroup Integer

2121

22−instance Ring Integer where

22+implementation Ring Integer where

2323 (<.>) = (*)

2424

25−instance RingWithUnity Integer where

25+implementation RingWithUnity Integer where

2626 unity = 1

2727

2828

29−instance Semigroup Int where

29+implementation Semigroup Int where

3030 (<+>) = (+)

3131

32−instance Monoid Int where

32+implementation Monoid Int where

3333 neutral = 0

3434

35−instance Group Int where

35+implementation Group Int where

3636 inverse = (* -1)

3737

38−instance AbelianGroup Int

38+implementation AbelianGroup Int

3939

40−instance Ring Int where

40+implementation Ring Int where

4141 (<.>) = (*)

4242

43−instance RingWithUnity Int where

43+implementation RingWithUnity Int where

4444 unity = 1

4545

4646

47−instance Semigroup Double where

47+implementation Semigroup Double where

4848 (<+>) = (+)

4949

50−instance Monoid Double where

50+implementation Monoid Double where

5151 neutral = 0

5252

53−instance Group Double where

53+implementation Group Double where

5454 inverse = (* -1)

5555

56−instance AbelianGroup Double

56+implementation AbelianGroup Double

5757

58−instance Ring Double where

58+implementation Ring Double where

5959 (<.>) = (*)

6060

61−instance RingWithUnity Double where

61+implementation RingWithUnity Double where

6262 unity = 1

6363

64−instance Field Double where

64+implementation Field Double where

6565 inverseM f _ = 1 / f

6666

6767

68−instance Semigroup Nat where

68+implementation Semigroup Nat where

6969 (<+>) = (+)

7070

71−instance Monoid Nat where

71+implementation Monoid Nat where

7272 neutral = 0

7373

74−instance Semigroup ZZ where

74+implementation Semigroup ZZ where

7575 (<+>) = (+)

7676

77−instance Monoid ZZ where

77+implementation Monoid ZZ where

7878 neutral = 0

7979

80−instance Group ZZ where

80+implementation Group ZZ where

8181 inverse = (* -1)

8282

83−instance AbelianGroup ZZ

83+implementation AbelianGroup ZZ

8484

85−instance Ring ZZ where

85+implementation Ring ZZ where

8686 (<.>) = (*)

8787

88−instance RingWithUnity ZZ where

88+implementation RingWithUnity ZZ where

8989 unity = 1

9090

9191

92−instance Semigroup a => Semigroup (Complex a) where

92+implementation Semigroup a => Semigroup (Complex a) where

9393 (<+>) (a :+ b) (c :+ d) = (a <+> c) :+ (b <+> d)

9494

95−instance Monoid a => Monoid (Complex a) where

95+implementation Monoid a => Monoid (Complex a) where

9696 neutral = (neutral :+ neutral)

9797

98−instance Group a => Group (Complex a) where

98+implementation Group a => Group (Complex a) where

9999 inverse (r :+ i) = (inverse r :+ inverse i)

100100

101−instance Ring a => AbelianGroup (Complex a) where {}

101+implementation Ring a => AbelianGroup (Complex a) where {}

102102

103−instance Ring a => Ring (Complex a) where

103+implementation Ring a => Ring (Complex a) where

104104 (<.>) (a :+ b) (c :+ d) = (a <.> c <-> b <.> d) :+ (a <.> d <+> b <.> c)

105105

106−instance RingWithUnity a => RingWithUnity (Complex a) where

106+implementation RingWithUnity a => RingWithUnity (Complex a) where

107107 unity = (unity :+ neutral)

108108

109−instance RingWithUnity a => Module a (Complex a) where

109+implementation RingWithUnity a => Module a (Complex a) where

110110 (<#>) x = map (x <.>)

111111

112−instance RingWithUnity a => InnerProductSpace a (Complex a) where

112+implementation RingWithUnity a => InnerProductSpace a (Complex a) where

113113 (x :+ y) <||> z = realPart $ (x :+ inverse y) <.> z

libs/contrib/Control/Algebra/VectorSpace.idr+3−3

@@ -18,13 +18,13 @@ infixr 2 <||>

1818||| + Distributivity of `<#>` and `<+>`:

1919||| forall a v w, a <#> (v <+> w) == (a <#> v) <+> (a <#> w)

2020||| forall a b v, (a <+> b) <#> v == (a <#> v) <+> (b <#> v)

21−class (RingWithUnity a, AbelianGroup b) => Module a b where

21+interface (RingWithUnity a, AbelianGroup b) => Module a b where

2222 (<#>) : a -> b -> b

2323

2424||| A vector space is a module over a ring that is also a field

25−class (Field a, Module a b) => VectorSpace a b where {}

25+interface (Field a, Module a b) => VectorSpace a b where {}

2626

2727||| An inner product space is a module – or vector space – over a ring, with a binary function

2828||| associating a ring value to each pair of vectors.

29−class Module a b => InnerProductSpace a b where

29+interface Module a b => InnerProductSpace a b where

3030 (<||>) : b -> b -> a

libs/contrib/Control/WellFounded.idr+1−1

@@ -26,7 +26,7 @@ data Accessible : (rel : a -> a -> Type) -> (x : a) -> Type where

2626||| acessible.

2727|||

2828||| @ rel the well-founded relation

29−class WellFounded (rel : a -> a -> Type) where

29+interface WellFounded (rel : a -> a -> Type) where

3030 wellFounded : (x : _) -> Accessible rel x

3131

3232

libs/contrib/Data/BoundedList.idr+2−2

@@ -62,7 +62,7 @@ replicate (S n) x = x :: replicate n x

6262-- Folds

6363--------------------------------------------------------------------------------

6464

65−instance Foldable (BoundedList n) where

65+implementation Foldable (BoundedList n) where

6666 foldr f e [] = e

6767 foldr f e (x::xs) = f x (foldr f e xs)

6868 foldl f e [] = e

@@ -72,7 +72,7 @@ instance Foldable (BoundedList n) where

7272-- Maps

7373--------------------------------------------------------------------------------

7474

75−instance Functor (BoundedList n) where

75+implementation Functor (BoundedList n) where

7676 map f [] = []

7777 map f (x :: xs) = f x :: map f xs

7878

libs/contrib/Data/CoList.idr+4−4

@@ -13,17 +13,17 @@ codata CoList : Type -> Type where

1313(++) [] right = right

1414(++) (x::xs) right = x :: (xs ++ right)

1515

16−instance Semigroup (CoList a) where

16+implementation Semigroup (CoList a) where

1717 (<+>) = (++)

1818

19−instance Monoid (CoList a) where

19+implementation Monoid (CoList a) where

2020 neutral = []

2121

22−instance Functor CoList where

22+implementation Functor CoList where

2323 map f [] = []

2424 map f (x::xs) = f x :: map f xs

2525

26−instance Show a => Show (CoList a) where

26+implementation Show a => Show (CoList a) where

2727 show xs = "[" ++ show' "" 20 xs ++ "]" where

2828 show' : String -> (n : Nat) -> (xs : CoList a) -> String

2929 show' acc Z _ = acc ++ "..."

libs/contrib/Data/Hash.idr+15−15

@@ -15,7 +15,7 @@ import Data.Vect

1515-}

1616

1717||| A type that can be hashed

18−class Hashable a where

18+interface Hashable a where

1919 saltedHash64 : a -> Bits64 -> Bits64 -- value to hash, salt, hash

2020

2121||| Computes a non cryptographic hash

@@ -40,48 +40,48 @@ private

4040mod64 : Integer -> Bits64

4141mod64 i = assert_total $ prim__truncBigInt_B64 (abs i `mod` 0xffffffffffffffff)

4242

43−instance Hashable Bits64 where

43+implementation Hashable Bits64 where

4444 saltedHash64 w salt = foldr (\b,acc => (acc `prim__shlB64` 10) + acc + b)

4545 salt

4646 [byte (fromInteger n) w | n <- [7,6..0]] -- djb2 hash function. Not meant for crypto

4747

48−instance Hashable Integer where

48+implementation Hashable Integer where

4949 saltedHash64 i = saltedHash64 (mod64 i)

5050

51−instance Hashable () where

51+implementation Hashable () where

5252 saltedHash64 _ salt = salt

5353

54−instance Hashable Bool where

54+implementation Hashable Bool where

5555 saltedHash64 True = saltedHash64 (the Bits64 1)

5656 saltedHash64 False = saltedHash64 (the Bits64 0)

5757

58−instance Hashable Int where

58+implementation Hashable Int where

5959 saltedHash64 w = saltedHash64 (prim__zextInt_B64 w)

6060

61−instance Hashable Char where

61+implementation Hashable Char where

6262 saltedHash64 w = saltedHash64 (the Int (cast w))

6363

64−instance Hashable Bits8 where

64+implementation Hashable Bits8 where

6565 saltedHash64 w = saltedHash64 (prim__zextB8_B64 w)

6666

67−instance Hashable Bits16 where

67+implementation Hashable Bits16 where

6868 saltedHash64 w = saltedHash64 (prim__zextB16_B64 w)

6969

70−instance Hashable Bits32 where

70+implementation Hashable Bits32 where

7171 saltedHash64 w = saltedHash64 (prim__zextB32_B64 w)

7272

73−instance Hashable a => Hashable (Maybe a) where

73+implementation Hashable a => Hashable (Maybe a) where

7474 saltedHash64 Nothing salt = salt

7575 saltedHash64 (Just k) salt = saltedHash64 k salt

7676

77−instance (Hashable a, Hashable b) => Hashable (a, b) where

77+implementation (Hashable a, Hashable b) => Hashable (a, b) where

7878 saltedHash64 (a,b) salt = saltedHash64 b (saltedHash64 a salt)

7979

80−instance Hashable a => Hashable (List a) where

80+implementation Hashable a => Hashable (List a) where

8181 saltedHash64 l salt = foldr (\c,acc => saltedHash64 c acc) salt l

8282

83−instance Hashable a => Hashable (Vect n a) where

83+implementation Hashable a => Hashable (Vect n a) where

8484 saltedHash64 l salt = foldr (\c,acc => saltedHash64 c acc) salt l

8585

86−instance Hashable String where

86+implementation Hashable String where

8787 saltedHash64 s = saltedHash64 (unpack s)

libs/contrib/Data/Heap.idr+5−5

@@ -110,23 +110,23 @@ sort : Ord a => List a -> List a

110110sort = Heap.toList . Heap.fromList

111111

112112--------------------------------------------------------------------------------

113−-- Class instances

113+-- Interface implementations

114114--------------------------------------------------------------------------------

115115

116−instance Show a => Show (MaxiphobicHeap a) where

116+implementation Show a => Show (MaxiphobicHeap a) where

117117 showPrec d Empty = "Empty"

118118 showPrec d (Node s l e r) = showCon d "Node" $ " _" ++ showArg l ++ showArg e ++ showArg r

119119

120−instance Eq a => Eq (MaxiphobicHeap a) where

120+implementation Eq a => Eq (MaxiphobicHeap a) where

121121 Empty == Empty = True

122122 (Node ls ll le lr) == (Node rs rl re rr) =

123123 ls == rs && ll == rl && le == re && lr == rr

124124 _ == _ = False

125125

126−instance Ord a => Semigroup (MaxiphobicHeap a) where

126+implementation Ord a => Semigroup (MaxiphobicHeap a) where

127127 (<+>) = merge

128128

129−instance Ord a => Monoid (MaxiphobicHeap a) where

129+implementation Ord a => Monoid (MaxiphobicHeap a) where

130130 neutral = empty

131131

132132--------------------------------------------------------------------------------

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

@@ -26,29 +26,29 @@ infixr 7 <&> -- matrix tensor product

2626-- Vectors as members of algebraic classes

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

2828

29−instance Semigroup a => Semigroup (Vect n a) where

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

3030 (<+>)= zipWith (<+>)

3131

32−instance Monoid a => Monoid (Vect n a) where

32+implementation Monoid a => Monoid (Vect n a) where

3333 neutral {n} = replicate n neutral

3434

35−instance Group a => Group (Vect n a) where

35+implementation Group a => Group (Vect n a) where

3636 inverse = map inverse

3737

38−instance AbelianGroup a => AbelianGroup (Vect n a) where {}

38+implementation AbelianGroup a => AbelianGroup (Vect n a) where {}

3939

40−instance Ring a => Ring (Vect n a) where

40+implementation Ring a => Ring (Vect n a) where

4141 (<.>) = zipWith (<.>)

4242

43−instance RingWithUnity a => RingWithUnity (Vect n a) where

43+implementation RingWithUnity a => RingWithUnity (Vect n a) where

4444 unity {n} = replicate n unity

4545

46−instance RingWithUnity a => Module a (Vect n a) where

46+implementation RingWithUnity a => Module a (Vect n a) where

4747 (<#>) r = map (r <.>)

4848

49−instance RingWithUnity a => Module a (Vect n (Vect l a)) where

49+implementation RingWithUnity a => Module a (Vect n (Vect l a)) where

5050 (<#>) r = map (r <#>)

51−-- should be Module a b => Module a (Vect n b), but results in 'overlapping instance'

51+-- should be Module a b => Module a (Vect n b), but results in 'overlapping implementation'

5252

5353-----------------------------------------------------------------------

5454-- (Ring) Vector functions

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

@@ -22,12 +22,12 @@ infixr 7 <&> -- matrix tensor product

2222-- Vectors as members of Num

2323-----------------------------------------------------------------------

2424

25−instance Num a => Num (Vect n a) where

25+implementation Num a => Num (Vect n a) where

2626 (+) = zipWith (+)

2727 (*) = zipWith (*)

2828 fromInteger n = replicate _ (fromInteger n)

2929

30−instance Neg a => Neg (Vect n a) where

30+implementation Neg a => Neg (Vect n a) where

3131 (-) = zipWith (-)

3232 abs = map abs

3333 negate = map negate

libs/contrib/Data/Nat/DivMod/IteratedSubtraction.idr+2−2

@@ -23,7 +23,7 @@ data LT' : (n,m : Nat) -> Type where

2323%name LT' lt, lt'

2424

2525||| Nothing is strictly less than zero

26−instance Uninhabited (LT' n 0) where

26+implementation Uninhabited (LT' n 0) where

2727 uninhabited LTSucc impossible

2828

2929||| Zero is less than any non-zero number.

@@ -56,7 +56,7 @@ minusLT' (S k) (S j) = LTStep (minusLT' k j)

5656||| zero (because there's nothing less than zero). This can't be done

5757||| for LTE, because that one doesn't stop at zero (because `LTE 0 0`

5858||| is inhabited).

59−instance WellFounded LT' where

59+implementation WellFounded LT' where

6060 wellFounded x = Access (acc x)

6161 where

6262 ||| Show accessibility by induction on the structure of the LT' witness

libs/contrib/Data/Sign.idr+1−1

@@ -4,5 +4,5 @@ module Data.Sign

44data Sign = Plus | Zero | Minus

66||| Discover the sign of some type

7−class Signed t where

7+interface Signed t where

88 total sign : t -> Sign

libs/contrib/Data/SortedMap.idr+1−1

@@ -242,7 +242,7 @@ treeMap f (Branch2 t1 k t2) = Branch2 (treeMap f t1) k (treeMap f t2)

242242treeMap f (Branch3 t1 k1 t2 k2 t3)

243243 = Branch3 (treeMap f t1) k1 (treeMap f t2) k2 (treeMap f t3)

244244

245−instance Functor (SortedMap k) where

245+implementation Functor (SortedMap k) where

246246 map _ Empty = Empty

247247 map f (M n t) = M _ (treeMap f t)

248248

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

@@ -31,5 +31,5 @@ public

3131toList : SortedSet k -> List k

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

3333

34−instance Foldable SortedSet where

34+implementation Foldable SortedSet where

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

libs/contrib/Data/ZZ.idr+10−10

@@ -14,7 +14,7 @@ import Data.Sign

1414|||

1515data ZZ = Pos Nat | NegS Nat

1616

17−instance Signed ZZ where

17+implementation Signed ZZ where

1818 sign (Pos Z) = Zero

1919 sign (Pos _) = Plus

2020 sign (NegS _) = Minus

@@ -24,7 +24,7 @@ absZ : ZZ -> Nat

2424absZ (Pos n) = n

2525absZ (NegS n) = S n

2626

27−instance Show ZZ where

27+implementation Show ZZ where

2828 show (Pos n) = show n

2929 show (NegS n) = "-" ++ show (S n)

3030

@@ -46,13 +46,13 @@ plusZ (NegS n) (NegS m) = NegS (S (n + m))

4646plusZ (Pos n) (NegS m) = minusNatZ n (S m)

4747plusZ (NegS n) (Pos m) = minusNatZ m (S n)

4848

49−instance Eq ZZ where

49+implementation Eq ZZ where

5050 (Pos n) == (Pos m) = n == m

5151 (NegS n) == (NegS m) = n == m

5252 _ == _ = False

5353

5454

55−instance Ord ZZ where

55+implementation Ord ZZ where

5656 compare (Pos n) (Pos m) = compare n m

5757 compare (NegS n) (NegS m) = compare m n

5858 compare (Pos _) (NegS _) = GT

@@ -71,16 +71,16 @@ fromInt n = if n < 0

7171 then NegS $ fromInteger {a=Nat} ((-n) - 1)

7272 else Pos $ fromInteger {a=Nat} n

7373

74−instance Cast Nat ZZ where

74+implementation Cast Nat ZZ where

7575 cast n = Pos n

7676

77−instance Num ZZ where

77+implementation Num ZZ where

7878 (+) = plusZ

7979 (*) = multZ

8080 fromInteger = fromInt

8181

8282mutual

83− instance Neg ZZ where

83+ implementation Neg ZZ where

8484 negate (Pos Z) = Pos Z

8585 negate (Pos (S n)) = NegS n

8686 negate (NegS n) = Pos (S n)

@@ -93,11 +93,11 @@ mutual

9393 subZ n m = plusZ n (negate m)

9494

9595

96−instance Cast ZZ Integer where

96+implementation Cast ZZ Integer where

9797 cast (Pos n) = cast n

9898 cast (NegS n) = (-1) * (cast n + 1)

9999

100−instance Cast Integer ZZ where

100+implementation Cast Integer ZZ where

101101 cast = fromInteger

102102

103103

@@ -130,7 +130,7 @@ posNotNeg : Pos n = NegS m -> Void

130130posNotNeg Refl impossible

131131

132132-- Decidable equality

133−instance DecEq ZZ where

133+implementation DecEq ZZ where

134134 decEq (Pos n) (NegS m) = No posNotNeg

135135 decEq (NegS n) (Pos m) = No $ negEqSym posNotNeg

136136 decEq (Pos n) (Pos m) with (decEq n m)

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

@@ -6,12 +6,12 @@ import Data.Fun

66%access public

88--------------------------------------------------------------------------------

9−-- Typeclass for decidable n-ary Relations

9+-- Interface for decidable n-ary Relations

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

1111

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

1313-- at the moment.

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

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

1515 total decide : liftRel ts p Dec

1616

1717-- 'No such variable {k506}'

libs/contrib/Decidable/Order.idr+16−16

@@ -16,20 +16,20 @@ import Data.Rel

1616-- Preorders, Posets, total Orders, Equivalencies, Congruencies

1717--------------------------------------------------------------------------------

1818

19−class Preorder t (po : t -> t -> Type) where

19+interface Preorder t (po : t -> t -> Type) where

2020 total transitive : (a : t) -> (b : t) -> (c : t) -> po a b -> po b c -> po a c

2121 total reflexive : (a : t) -> po a a

2222

23−class (Preorder t po) => Poset t (po : t -> t -> Type) where

23+interface (Preorder t po) => Poset t (po : t -> t -> Type) where

2424 total antisymmetric : (a : t) -> (b : t) -> po a b -> po b a -> a = b

2525

26−class (Poset t to) => Ordered t (to : t -> t -> Type) where

26+interface (Poset t to) => Ordered t (to : t -> t -> Type) where

2727 total order : (a : t) -> (b : t) -> Either (to a b) (to b a)

2828

29−class (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where

29+interface (Preorder t eq) => Equivalence t (eq : t -> t -> Type) where

3030 total symmetric : (a : t) -> (b : t) -> eq a b -> eq b a

3131

32−class (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where

32+interface (Equivalence t eq) => Congruence t (f : t -> t) (eq : t -> t -> Type) where

3333 total congruent : (a : t) ->

3434 (b : t) ->

3535 eq a b ->

@@ -49,14 +49,14 @@ maximum {to} x y with (order {to} x y)

4949-- Syntactic equivalence (=)

5050--------------------------------------------------------------------------------

5151

52−instance Preorder t ((=) {A = t} {B = t}) where

52+implementation Preorder t ((=) {A = t} {B = t}) where

5353 transitive a b c = trans {a = a} {b = b} {c = c}

5454 reflexive a = Refl

5555

56−instance Equivalence t ((=) {A = t} {B = t}) where

56+implementation Equivalence t ((=) {A = t} {B = t}) where

5757 symmetric a b prf = sym prf

5858

59−instance Congruence t f ((=) {A = t} {B = t}) where

59+implementation Congruence t f ((=) {A = t} {B = t}) where

6060 congruent a b = cong {a = a} {b = b} {f = f}

6161

6262--------------------------------------------------------------------------------

@@ -73,7 +73,7 @@ total LTEIsReflexive : (n : Nat) -> LTE n n

7373LTEIsReflexive Z = LTEZero

7474LTEIsReflexive (S n) = LTESucc (LTEIsReflexive n)

7575

76−instance Preorder Nat LTE where

76+implementation Preorder Nat LTE where

7777 transitive = LTEIsTransitive

7878 reflexive = LTEIsReflexive

7979

@@ -84,7 +84,7 @@ LTEIsAntisymmetric (S n) (S m) (LTESucc mLTEn) (LTESucc nLTEm) with (LTEIsAntisy

8484 LTEIsAntisymmetric (S n) (S n) (LTESucc mLTEn) (LTESucc nLTEm) | Refl = Refl

8585

8686

87−instance Poset Nat LTE where

87+implementation Poset Nat LTE where

8888 antisymmetric = LTEIsAntisymmetric

8989

9090total zeroNeverGreater : {n : Nat} -> LTE (S n) Z -> Void

@@ -108,7 +108,7 @@ decideLTE (S x) (S y) with (decEq (S x) (S y))

108108 | Yes nLTEm = Yes (LTESucc nLTEm)

109109 | No nGTm = No (ltesuccinjective nGTm)

110110

111−instance Decidable [Nat,Nat] LTE where

111+implementation Decidable [Nat,Nat] LTE where

112112 decide = decideLTE

113113

114114total

@@ -119,7 +119,7 @@ total

119119shift : (m : Nat) -> (n : Nat) -> LTE m n -> LTE (S m) (S n)

120120shift m n mLTEn = LTESucc mLTEn

121121

122−instance Ordered Nat LTE where

122+implementation Ordered Nat LTE where

123123 order Z n = Left LTEZero

124124 order m Z = Right LTEZero

125125 order (S k) (S j) with (order {to=LTE} k j)

@@ -134,21 +134,21 @@ using (k : Nat)

134134 data FinLTE : Fin k -> Fin k -> Type where

135135 FromNatPrf : {m : Fin k} -> {n : Fin k} -> LTE (finToNat m) (finToNat n) -> FinLTE m n

136136

137− instance Preorder (Fin k) FinLTE where

137+ implementation Preorder (Fin k) FinLTE where

138138 transitive m n o (FromNatPrf p1) (FromNatPrf p2) =

139139 FromNatPrf (LTEIsTransitive (finToNat m) (finToNat n) (finToNat o) p1 p2)

140140 reflexive n = FromNatPrf (LTEIsReflexive (finToNat n))

141141

142− instance Poset (Fin k) FinLTE where

142+ implementation Poset (Fin k) FinLTE where

143143 antisymmetric m n (FromNatPrf p1) (FromNatPrf p2) =

144144 finToNatInjective m n (LTEIsAntisymmetric (finToNat m) (finToNat n) p1 p2)

145145

146− instance Decidable [Fin k, Fin k] FinLTE where

146+ implementation Decidable [Fin k, Fin k] FinLTE where

147147 decide m n with (decideLTE (finToNat m) (finToNat n))

148148 | Yes prf = Yes (FromNatPrf prf)

149149 | No disprf = No (\ (FromNatPrf prf) => disprf prf)

150150

151− instance Ordered (Fin k) FinLTE where

151+ implementation Ordered (Fin k) FinLTE where

152152 order m n =

153153 either (Left . FromNatPrf)

154154 (Right . FromNatPrf)

libs/contrib/Network/Cgi.idr+3−4

@@ -30,21 +30,20 @@ data CGI : Type -> Type where

3030getAction : CGI a -> CGIInfo -> IO (a, CGIInfo)

3131getAction (MkCGI act) = act

3232

33−instance Functor CGI where

33+implementation Functor CGI where

3434 map f (MkCGI c) = MkCGI (\s => do (a, i) <- c s

3535 return (f a, i))

3636

37−instance Applicative CGI where

37+implementation Applicative CGI where

3838 pure v = MkCGI (\s => return (v, s))

3939

4040 (MkCGI a) <*> (MkCGI b) = MkCGI (\s => do (f, i) <- a s

4141 (c, j) <- b i

4242 return (f c, j))

4343

44−instance Monad CGI where {

44+implementation Monad CGI where

4545 (>>=) (MkCGI f) k = MkCGI (\s => do v <- f s

4646 getAction (k (fst v)) (snd v))

47−}

4847

4948setInfo : CGIInfo -> CGI ()

5049setInfo i = MkCGI (\s => return ((), i))

libs/contrib/Network/Socket.idr+6−6

@@ -13,7 +13,7 @@ module IdrisNet.Socket

1313ByteLength : Type

1414ByteLength = Int

1515

16−class ToCode a where

16+interface ToCode a where

1717 toCode : a -> Int

1818

1919||| Socket Families

@@ -28,12 +28,12 @@ data SocketFamily =

2828 ||| IP / UDP etc. IPv6

2929 AF_INET6

3030

31−instance Show SocketFamily where

31+implementation Show SocketFamily where

3232 show AF_UNSPEC = "AF_UNSPEC"

3333 show AF_INET = "AF_INET"

3434 show AF_INET6 = "AF_INET6"

3535

36−instance ToCode SocketFamily where

36+implementation ToCode SocketFamily where

3737 toCode AF_UNSPEC = 0

3838 toCode AF_INET = 2

3939 toCode AF_INET6 = 10

@@ -52,13 +52,13 @@ data SocketType =

5252 ||| Raw sockets

5353 RawSocket

5454

55−instance Show SocketType where

55+implementation Show SocketType where

5656 show NotASocket = "Not a socket"

5757 show Stream = "Stream"

5858 show Datagram = "Datagram"

5959 show RawSocket = "Raw"

6060

61−instance ToCode SocketType where

61+implementation ToCode SocketType where

6262 toCode NotASocket = 0

6363 toCode Stream = 1

6464 toCode Datagram = 2

@@ -89,7 +89,7 @@ data SocketAddress = IPv4Addr Int Int Int Int

8989 | Hostname String

9090 | InvalidAddress -- Used when there's a parse error

9191

92−instance Show SocketAddress where

92+implementation Show SocketAddress where

9393 show (IPv4Addr i1 i2 i3 i4) = concat $ Prelude.List.intersperse "." (map show [i1, i2, i3, i4])

9494 show IPv6Addr = "NOT IMPLEMENTED YET"

9595 show (Hostname host) = host

libs/contrib/System/Concurrency/Process.idr+3−3

@@ -14,14 +14,14 @@ data ProcID msg = MkPID Ptr

1414data Process : (msgType : Type) -> Type -> Type where

1515 Lift : IO a -> Process msg a

1616

17−instance Functor (Process msg) where

17+implementation Functor (Process msg) where

1818 map f (Lift a) = Lift (map f a)

1919

20−instance Applicative (Process msg) where

20+implementation Applicative (Process msg) where

2121 pure = Lift . return

2222 (Lift f) <*> (Lift a) = Lift (f <*> a)

2323

24−instance Monad (Process msg) where

24+implementation Monad (Process msg) where

2525 (Lift io) >>= k = Lift (do x <- io

2626 case k x of

2727 Lift v => v)

libs/effects/Effect/Default.idr+13−13

@@ -2,43 +2,43 @@ module Default

33import Data.Vect

5−class Default a where

5+interface Default a where

66 default : a

8−instance Default Int where

8+implementation Default Int where

99 default = 0

1010

11−instance Default Integer where

11+implementation Default Integer where

1212 default = 0

1313

14−instance Default Double where

14+implementation Default Double where

1515 default = 0

1616

17−instance Default Nat where

17+implementation Default Nat where

1818 default = 0

1919

20−instance Default Char where

20+implementation Default Char where

2121 default = '\0'

2222

23−instance Default String where

23+implementation Default String where

2424 default = ""

2525

26−instance Default Bool where

26+implementation Default Bool where

2727 default = False

2828

29−instance Default () where

29+implementation Default () where

3030 default = ()

3131

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

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

3333 default = (default, default)

3434

35−instance Default (Maybe a) where

35+implementation Default (Maybe a) where

3636 default = Nothing

3737

38−instance Default (List a) where

38+implementation Default (List a) where

3939 default = []

4040

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

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

4242 default = mkDef _ where

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

4444 mkDef Z = []

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

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

77data Exception : Type -> Effect where

88 Raise : a -> sig (Exception a) b

10−instance Handler (Exception a) Maybe where

10+implementation Handler (Exception a) Maybe where

1111 handle _ (Raise e) k = Nothing

1212

13−instance Handler (Exception a) List where

13+implementation Handler (Exception a) List where

1414 handle _ (Raise e) k = []

1515

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

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

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

1818 believe_me (exit 1)

1919

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

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

2121 handle _ (Raise e) k = ioe_fail e

2222

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

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

2424 handle _ (Raise e) k = Left e

2525

2626EXCEPTION : Type -> EFFECT

libs/effects/Effect/File.idr+2−2

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

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

7474

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

76−instance Handler FileIO IO where

76+implementation Handler FileIO IO where

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

7878 | Left err => k False ()

7979 k True (FH h)

@@ -89,7 +89,7 @@ instance Handler FileIO IO where

8989 handle (FH h) EOF k = do e <- fEOF h

9090 k e (FH h)

9191

92−instance Handler FileIO (IOExcept a) where

92+implementation Handler FileIO (IOExcept a) where

9393 handle () (Open fname m) k = do Right h <- ioe_lift $ openFile fname m

9494 | Left err => k False ()

9595 k True (FH h)

libs/effects/Effect/Logging/Category.idr+2−2

@@ -25,7 +25,7 @@ record LogRes (a : Type) where

2525 getLevel : LogLevel n

2626 getCategories : List a

2727

28−instance Default (LogRes a) where

28+implementation Default (LogRes a) where

2929 default = MkLogRes OFF Nil

3030

3131-- ------------------------------------------------------- [ Effect Definition ]

@@ -68,7 +68,7 @@ data Logging : Effect where

6868

6969-- -------------------------------------------------------------- [ IO Handler ]

7070

71−instance Handler Logging IO where

71+implementation Handler Logging IO where

7272 handle st (SetLogLvl nlvl) k = do

7373 let newSt = record {getLevel = nlvl} st

7474 k () newSt

libs/effects/Effect/Logging/Default.idr+2−2

@@ -24,7 +24,7 @@ record LogRes where

2424 constructor MkLogRes

2525 getLevel : LogLevel n

2626

27−instance Default LogRes where

27+implementation Default LogRes where

2828 default = MkLogRes OFF

2929

3030-- ------------------------------------------------------ [ The Logging Effect ]

@@ -49,7 +49,7 @@ data Logging : Effect where

4949-- -------------------------------------------------------------- [ IO Handler ]

5050

5151-- For logging in the IO context

52−instance Handler Logging IO where

52+implementation Handler Logging IO where

5353 handle st (SetLvl newLvl) k = k () (MkLogRes newLvl)

5454 handle st (Log lvl msg) k = do

5555 case cmpLevel lvl (getLevel st) of

libs/effects/Effect/Logging/Level.idr+3−3

@@ -54,10 +54,10 @@ data LogLevel : Nat -> Type where

5454 ||| User defined logging level.

5555 CUSTOM : (n : Nat) -> {auto prf : LTE n 70} -> LogLevel n

5656

57−instance Cast (LogLevel n) Nat where

57+implementation Cast (LogLevel n) Nat where

5858 cast {n} _ = n

5959

60−instance Show (LogLevel n) where

60+implementation Show (LogLevel n) where

6161 show OFF = "OFF"

6262 show TRACE = "TRACE"

6363 show DEBUG = "DEBUG"

@@ -68,7 +68,7 @@ instance Show (LogLevel n) where

6868 show ALL = "ALL"

6969 show (CUSTOM n) = unwords ["CUSTOM", show n]

7070

71−instance Eq (LogLevel n) where

71+implementation Eq (LogLevel n) where

7272 (==) x y = lvlEq x y

7373 where

7474 lvlEq : LogLevel a -> LogLevel b -> Bool

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

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

7979 = do foreign FFI_C "idris_poke" (Ptr -> Int -> Bits8 -> IO ()) ptr (fromInteger $ cast offset) b

8080 do_poke ptr (S offset) bs

8181

82−instance Handler RawMemory (IOExcept String) where

82+implementation Handler RawMemory (IOExcept String) where

8383 handle () (Allocate n) k

8484 = do ptr <- do_malloc n

8585 k () (CH ptr)

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

@@ -5,18 +5,18 @@ import Effects

55data MonadEffT : List EFFECT -> (Type -> Type) -> Type -> Type where

66 MkMonadEffT : EffM m a xs (\v => xs) -> MonadEffT xs m a

8−instance Functor (MonadEffT xs f) where

8+implementation Functor (MonadEffT xs f) where

99 map f (MkMonadEffT x) = MkMonadEffT (do x' <- x

1010 pure (f x'))

1111

12−instance Applicative (MonadEffT xs f) where

12+implementation Applicative (MonadEffT xs f) where

1313 pure x = MkMonadEffT (pure x)

1414 (<*>) (MkMonadEffT f) (MkMonadEffT x)

1515 = MkMonadEffT (do f' <- f

1616 x' <- x

1717 pure (f' x'))

1818

19−instance Monad (MonadEffT xs f) where

19+implementation Monad (MonadEffT xs f) where

2020 (>>=) (MkMonadEffT x) f = MkMonadEffT (do x' <- x

2121 let MkMonadEffT fx = f x'

2222 fx)

libs/effects/Effect/Perf.idr+2−2

@@ -57,7 +57,7 @@ record PMetrics where

5757 stamps : List (String, Integer)

5858

5959

60−instance Default PMetrics where

60+implementation Default PMetrics where

6161 default = MkPMetrics False False Nil Nil 0 Nil

6262

6363displayPerfMetrics : PMetrics -> String

@@ -121,7 +121,7 @@ data Perf : Effect where

121121

122122-- ---------------------------------------------------------- [ Handler for IO ]

123123

124−instance Handler Perf IO where

124+implementation Handler Perf IO where

125125 handle res (TurnOn b) k = do

126126 v <- time

127127 let res' = record {canPerf = True, livePerf = b, stime = v} res

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

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

77 GetRandom : sig Random Integer Integer

88 SetSeed : Integer -> sig Random () Integer

10−instance Handler Random m where

10+implementation Handler Random m where

1111 handle seed GetRandom k

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

1313 k seed' seed'

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

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

55data Selection : Effect where

66 Select : List a -> sig Selection a ()

8−instance Handler Selection Maybe where

8+implementation Handler Selection Maybe where

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

1010 tryAll [] = Nothing

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

1212 Nothing => tryAll xs

1313 Just v => Just v

1414

15−instance Handler Selection List where

15+implementation Handler Selection List where

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

1717

1818SELECT : EFFECT

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

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

99 Put : b -> sig State () a b

1010

1111-- using (m : Type -> Type)

12−instance Handler State m where

12+implementation Handler State m where

1313 handle st Get k = k st st

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

1515

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

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

1919-- IO effects handlers

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

2121

22−instance Handler StdIO IO where

22+implementation Handler StdIO IO where

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

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

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

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

2727

28−instance Handler StdIO (IOExcept a) where

28+implementation Handler StdIO (IOExcept a) where

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

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

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

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

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

1313 GetEnv : String -> sig System (Maybe String)

1414 CSystem : String -> sig System Int

1515

16−instance Handler System IO where

16+implementation Handler System IO where

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

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

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

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

2121

22−instance Handler System (IOExcept a) where

22+implementation Handler System (IOExcept a) where

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

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

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

libs/effects/Effect/Trans.idr+1−1

@@ -8,7 +8,7 @@ data Trans : (Type -> Type) -> Effect where

88 Lift : m a -> sig (Trans m) a

1010-- using (m : Type -> Type)

11−instance Monad m => Handler (Trans m) m where

11+implementation Monad m => Handler (Trans m) m where

1212 handle st (Lift op) k = do x <- op

1313 k x ()

1414

libs/effects/Effects.idr+4−4

@@ -46,9 +46,9 @@ namespace DepUpdateEffect

4646 (ret : Type) -> (res_in : Type) -> (res_out : ret -> Type) -> Type

4747 sig e r e_in e_out = e r e_in e_out

4848

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

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

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

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

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

5252 ||| How to handle the effect.

5353 |||

5454 ||| @ r The resource being handled.

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

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

139139

140140using (lbl : Type)

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

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

142142 default = lbl := default

143143

144144private

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

285285 = let env' = unlabel env in

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

287287

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

288+-- yuck :) Haven't got interface instances working nicely in tactic

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

290290-- so just brute force it.

291291syntax MkDefaultEnv = with Env

libs/prelude/Decidable/Equality.idr+14−14

@@ -23,7 +23,7 @@ negEqSym p h = p (sym h)

2323--------------------------------------------------------------------------------

2424

2525||| Decision procedures for propositional equality

26−class DecEq t where

26+interface DecEq t where

2727 ||| Decide whether two elements of `t` are propositionally equal

2828 total decEq : (x1 : t) -> (x2 : t) -> Dec (x1 = x2)

2929

@@ -31,7 +31,7 @@ class DecEq t where

3131--- Unit

3232--------------------------------------------------------------------------------

3333

34−instance DecEq () where

34+implementation DecEq () where

3535 decEq () () = Yes Refl

3636

3737--------------------------------------------------------------------------------

@@ -40,7 +40,7 @@ instance DecEq () where

4040total trueNotFalse : True = False -> Void

4141trueNotFalse Refl impossible

4242

43−instance DecEq Bool where

43+implementation DecEq Bool where

4444 decEq True True = Yes Refl

4545 decEq False False = Yes Refl

4646 decEq True False = No trueNotFalse

@@ -53,7 +53,7 @@ instance DecEq Bool where

5353total ZnotS : Z = S n -> Void

5454ZnotS Refl impossible

5555

56−instance DecEq Nat where

56+implementation DecEq Nat where

5757 decEq Z Z = Yes Refl

5858 decEq Z (S _) = No ZnotS

5959 decEq (S _) Z = No (negEqSym ZnotS)

@@ -68,7 +68,7 @@ instance DecEq Nat where

6868total nothingNotJust : {x : t} -> (Nothing {a = t} = Just x) -> Void

6969nothingNotJust Refl impossible

7070

71−instance (DecEq t) => DecEq (Maybe t) where

71+implementation (DecEq t) => DecEq (Maybe t) where

7272 decEq Nothing Nothing = Yes Refl

7373 decEq (Just x') (Just y') with (decEq x' y')

7474 | Yes p = Yes $ cong p

@@ -83,7 +83,7 @@ instance (DecEq t) => DecEq (Maybe t) where

8383total leftNotRight : {x : a} -> {y : b} -> Left {b = b} x = Right {a = a} y -> Void

8484leftNotRight Refl impossible

8585

86−instance (DecEq a, DecEq b) => DecEq (Either a b) where

86+implementation (DecEq a, DecEq b) => DecEq (Either a b) where

8787 decEq (Left x') (Left y') with (decEq x' y')

8888 | Yes p = Yes $ cong p

8989 | No p = No $ \h : Left x' = Left y' => p $ leftInjective {b = b} h

@@ -109,7 +109,7 @@ lemma_fst_neq_snd_eq : {x : a, x' : b, y : c, y' : d} ->

109109 ((x, y) = (x', y) -> Void)

110110lemma_fst_neq_snd_eq p_x_not_x' Refl Refl = p_x_not_x' Refl

111111

112−instance (DecEq a, DecEq b) => DecEq (a, b) where

112+implementation (DecEq a, DecEq b) => DecEq (a, b) where

113113 decEq (a, b) (a', b') with (decEq a a')

114114 decEq (a, b) (a, b') | (Yes Refl) with (decEq b b')

115115 decEq (a, b) (a, b) | (Yes Refl) | (Yes Refl) = Yes Refl

@@ -135,7 +135,7 @@ lemma_x_neq_xs_eq p Refl Refl = p Refl

135135lemma_x_neq_xs_neq : {x : t, xs : List t, y : t, ys : List t} -> (x = y -> Void) -> (xs = ys -> Void) -> ((x :: xs) = (y :: ys) -> Void)

136136lemma_x_neq_xs_neq p p' Refl = p Refl

137137

138−instance DecEq a => DecEq (List a) where

138+implementation DecEq a => DecEq (List a) where

139139 decEq [] [] = Yes Refl

140140 decEq (x :: xs) [] = No lemma_val_not_nil

141141 decEq [] (x :: xs) = No (negEqSym lemma_val_not_nil)

@@ -155,7 +155,7 @@ instance DecEq a => DecEq (List a) where

155155-- Int

156156--------------------------------------------------------------------------------

157157

158−instance DecEq Int where

158+implementation DecEq Int where

159159 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

160160 where primitiveEq : x = y

161161 primitiveEq = believe_me (Refl {x})

@@ -165,7 +165,7 @@ instance DecEq Int where

165165-- Char

166166--------------------------------------------------------------------------------

167167

168−instance DecEq Char where

168+implementation DecEq Char where

169169 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

170170 where primitiveEq : x = y

171171 primitiveEq = believe_me (Refl {x})

@@ -175,7 +175,7 @@ instance DecEq Char where

175175-- Integer

176176--------------------------------------------------------------------------------

177177

178−instance DecEq Integer where

178+implementation DecEq Integer where

179179 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

180180 where primitiveEq : x = y

181181 primitiveEq = really_believe_me (Refl {x})

@@ -186,7 +186,7 @@ instance DecEq Integer where

186186-- String

187187--------------------------------------------------------------------------------

188188

189−instance DecEq String where

189+implementation DecEq String where

190190 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

191191 where primitiveEq : x = y

192192 primitiveEq = believe_me (Refl {x})

@@ -196,7 +196,7 @@ instance DecEq String where

196196-- Ptr

197197--------------------------------------------------------------------------------

198198

199−instance DecEq Ptr where

199+implementation DecEq Ptr where

200200 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

201201 where primitiveEq : x = y

202202 primitiveEq = believe_me (Refl {x})

@@ -206,7 +206,7 @@ instance DecEq Ptr where

206206-- ManagedPtr

207207--------------------------------------------------------------------------------

208208

209−instance DecEq ManagedPtr where

209+implementation DecEq ManagedPtr where

210210 decEq x y = if x == y then Yes primitiveEq else No primitiveNotEq

211211 where primitiveEq : x = y

212212 primitiveEq = believe_me (Refl {x})

libs/prelude/Language/Reflection.idr+66−66

@@ -80,34 +80,34 @@ data Const = I Int | BI Integer | Fl Double | Ch Char | Str String

8080 | WorldType | TheWorld

8181%name Const c, c'

8282

83−abstract class ReflConst (a : Type) where

83+abstract interface ReflConst (a : Type) where

8484 toConst : a -> Const

8585

86−instance ReflConst Int where

86+implementation ReflConst Int where

8787 toConst x = I x

8888

89−instance ReflConst Integer where

89+implementation ReflConst Integer where

9090 toConst = BI

9191

92−instance ReflConst Double where

92+implementation ReflConst Double where

9393 toConst = Fl

9494

95−instance ReflConst Char where

95+implementation ReflConst Char where

9696 toConst = Ch

9797

98−instance ReflConst String where

98+implementation ReflConst String where

9999 toConst = Str

100100

101−instance ReflConst Bits8 where

101+implementation ReflConst Bits8 where

102102 toConst = B8

103103

104−instance ReflConst Bits16 where

104+implementation ReflConst Bits16 where

105105 toConst = B16

106106

107−instance ReflConst Bits32 where

107+implementation ReflConst Bits32 where

108108 toConst = B32

109109

110−instance ReflConst Bits64 where

110+implementation ReflConst Bits64 where

111111 toConst = B64

112112

113113implicit

@@ -182,7 +182,7 @@ data Binder : (tmTy : Type) -> Type where

182182

183183%name Binder b, b'

184184

185−instance Functor Binder where

185+implementation Functor Binder where

186186 map f (Lam x) = Lam (f x)

187187 map f (Pi x k) = Pi (f x) (f k)

188188 map f (Let x y) = Let (f x) (f y)

@@ -192,7 +192,7 @@ instance Functor Binder where

192192 map f (PVar x) = PVar (f x)

193193 map f (PVTy x) = PVTy (f x)

194194

195−instance Foldable Binder where

195+implementation Foldable Binder where

196196 foldr f z (Lam x) = f x z

197197 foldr f z (Pi x k) = f x (f k z)

198198 foldr f z (Let x y) = f x (f y z)

@@ -202,7 +202,7 @@ instance Foldable Binder where

202202 foldr f z (PVar x) = f x z

203203 foldr f z (PVTy x) = f x z

204204

205−instance Traversable Binder where

205+implementation Traversable Binder where

206206 traverse f (Lam x) = [| Lam (f x) |]

207207 traverse f (Pi x k) = [| Pi (f x) (f k) |]

208208 traverse f (Let x y) = [| Let (f x) (f y) |]

@@ -285,7 +285,7 @@ data Tactic =

285285 Trivial |

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

287287 Search Int |

288− ||| Resolve a type class

288+ ||| Resolve an interface

289289 Instance |

290290 ||| Infer the proof target from the context

291291 Solve |

@@ -330,12 +330,12 @@ data Tactic =

330330

331331||| Things with a canonical representation as a reflected term.

332332|||

333−||| This type class is intended to be used during proof automation and the

333+||| This interface is intended to be used during proof automation and the

334334||| construction of custom tactics.

335335|||

336336||| @ a the type to be quoted

337337||| @ t the type to quote it to (typically `TT` or `Raw`)

338−class Quotable a t where

338+interface Quotable a t where

339339 ||| A representation of the type `a`.

340340 |||

341341 ||| This is to enable quoting polymorphic datatypes

@@ -346,122 +346,122 @@ class Quotable a t where

346346 ||| Each equation should look something like ```quote (Foo x y) = `(Foo ~(quote x) ~(quote y))```

347347 quote : a -> t

348348

349−instance Quotable Nat TT where

349+implementation Quotable Nat TT where

350350 quotedTy = `(Nat)

351351

352352 quote Z = `(Z)

353353 quote (S k) = `(S ~(quote k))

354354

355−instance Quotable Nat Raw where

355+implementation Quotable Nat Raw where

356356 quotedTy = `(Nat)

357357

358358 quote Z = `(Z)

359359 quote (S k) = `(S ~(quote k))

360360

361−instance Quotable Int TT where

361+implementation Quotable Int TT where

362362 quotedTy = `(Int)

363363 quote x = TConst (I x)

364364

365−instance Quotable Int Raw where

365+implementation Quotable Int Raw where

366366 quotedTy = `(Int)

367367 quote x = RConstant (I x)

368368

369−instance Quotable Double TT where

369+implementation Quotable Double TT where

370370 quotedTy = `(Double)

371371 quote x = TConst (Fl x)

372372

373−instance Quotable Double Raw where

373+implementation Quotable Double Raw where

374374 quotedTy = `(Double)

375375 quote x = RConstant (Fl x)

376376

377−instance Quotable Char TT where

377+implementation Quotable Char TT where

378378 quotedTy = `(Char)

379379 quote x = TConst (Ch x)

380380

381−instance Quotable Char Raw where

381+implementation Quotable Char Raw where

382382 quotedTy = `(Char)

383383 quote x = RConstant (Ch x)

384384

385−instance Quotable Bits8 TT where

385+implementation Quotable Bits8 TT where

386386 quotedTy = `(Bits8)

387387 quote x = TConst (B8 x)

388388

389−instance Quotable Bits8 Raw where

389+implementation Quotable Bits8 Raw where

390390 quotedTy = `(Bits8)

391391 quote x = RConstant (B8 x)

392392

393−instance Quotable Bits16 TT where

393+implementation Quotable Bits16 TT where

394394 quotedTy = `(Bits16)

395395 quote x = TConst (B16 x)

396396

397−instance Quotable Bits16 Raw where

397+implementation Quotable Bits16 Raw where

398398 quotedTy = `(Bits16)

399399 quote x = RConstant (B16 x)

400400

401−instance Quotable Bits32 TT where

401+implementation Quotable Bits32 TT where

402402 quotedTy = `(Bits32)

403403 quote x = TConst (B32 x)

404404

405−instance Quotable Bits32 Raw where

405+implementation Quotable Bits32 Raw where

406406 quotedTy = `(Bits32)

407407 quote x = RConstant (B32 x)

408408

409−instance Quotable Bits64 TT where

409+implementation Quotable Bits64 TT where

410410 quotedTy = `(Bits64)

411411 quote x = TConst (B64 x)

412412

413−instance Quotable Bits64 Raw where

413+implementation Quotable Bits64 Raw where

414414 quotedTy = `(Bits64)

415415 quote x = RConstant (B64 x)

416416

417−instance Quotable Integer TT where

417+implementation Quotable Integer TT where

418418 quotedTy = `(Integer)

419419 quote x = TConst (BI x)

420420

421−instance Quotable Integer Raw where

421+implementation Quotable Integer Raw where

422422 quotedTy = `(Integer)

423423 quote x = RConstant (BI x)

424424

425−instance Quotable String TT where

425+implementation Quotable String TT where

426426 quotedTy = `(String)

427427 quote x = TConst (Str x)

428428

429−instance Quotable String Raw where

429+implementation Quotable String Raw where

430430 quotedTy = `(String)

431431 quote x = RConstant (Str x)

432432

433−instance Quotable NameType TT where

433+implementation Quotable NameType TT where

434434 quotedTy = `(NameType)

435435 quote Bound = `(Bound)

436436 quote Ref = `(Ref)

437437 quote (DCon x y) = `(DCon ~(quote x) ~(quote y))

438438 quote (TCon x y) = `(TCon ~(quote x) ~(quote y))

439439

440−instance Quotable NameType Raw where

440+implementation Quotable NameType Raw where

441441 quotedTy = `(NameType)

442442 quote Bound = `(Bound)

443443 quote Ref = `(Ref)

444444 quote (DCon x y) = `(DCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))

445445 quote (TCon x y) = `(TCon ~(quote {t=Raw} x) ~(quote {t=Raw} y))

446446

447−instance Quotable a TT => Quotable (List a) TT where

447+implementation Quotable a TT => Quotable (List a) TT where

448448 quotedTy = `(List ~(quotedTy {a}))

449449 quote [] = `(List.Nil {elem=~(quotedTy {a})})

450450 quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))

451451

452−instance Quotable a Raw => Quotable (List a) Raw where

452+implementation Quotable a Raw => Quotable (List a) Raw where

453453 quotedTy = `(List ~(quotedTy {a}))

454454 quote [] = `(List.Nil {elem=~(quotedTy {a})})

455455 quote (x :: xs) = `(List.(::) {elem=~(quotedTy {a})} ~(quote x) ~(quote xs))

456456

457−instance Quotable SourceLocation TT where

457+implementation Quotable SourceLocation TT where

458458 quotedTy = `(SourceLocation)

459459 quote (FileLoc fn (sl, sc) (el, ec)) =

460460 `(FileLoc ~(quote fn)

461461 (~(quote sl), ~(quote sc))

462462 (~(quote el), ~(quote ec)))

463463

464−instance Quotable SourceLocation Raw where

464+implementation Quotable SourceLocation Raw where

465465 quotedTy = `(SourceLocation)

466466 quote (FileLoc fn (sl, sc) (el, ec)) =

467467 `(FileLoc ~(quote {t=Raw} fn)

@@ -470,14 +470,14 @@ instance Quotable SourceLocation Raw where

470470

471471

472472mutual

473− instance Quotable TTName TT where

473+ implementation Quotable TTName TT where

474474 quotedTy = `(TTName)

475475 quote (UN x) = `(UN ~(quote x))

476476 quote (NS n xs) = `(NS ~(quote n) ~(quote xs))

477477 quote (MN x y) = `(MN ~(quote x) ~(quote y))

478478 quote (SN sn) = `(SN ~(assert_total $ quote sn))

479479

480− instance Quotable SpecialName TT where

480+ implementation Quotable SpecialName TT where

481481 quotedTy = `(SpecialName)

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

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

@@ -490,14 +490,14 @@ mutual

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

491491

492492mutual

493− instance Quotable TTName Raw where

493+ implementation Quotable TTName Raw where

494494 quotedTy = `(TTName)

495495 quote (UN x) = `(UN ~(quote {t=Raw} x))

496496 quote (NS n xs) = `(NS ~(quote {t=Raw} n) ~(quote {t=Raw} xs))

497497 quote (MN x y) = `(MN ~(quote {t=Raw} x) ~(quote {t=Raw} y))

498498 quote (SN sn) = `(SN ~(assert_total $ quote sn))

499499

500− instance Quotable SpecialName Raw where

500+ implementation Quotable SpecialName Raw where

501501 quotedTy = `(SpecialName)

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

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

@@ -510,45 +510,45 @@ mutual

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

511511

512512

513−instance Quotable NativeTy TT where

513+implementation Quotable NativeTy TT where

514514 quotedTy = `(NativeTy)

515515 quote IT8 = `(Reflection.IT8)

516516 quote IT16 = `(Reflection.IT16)

517517 quote IT32 = `(Reflection.IT32)

518518 quote IT64 = `(Reflection.IT64)

519519

520−instance Quotable NativeTy Raw where

520+implementation Quotable NativeTy Raw where

521521 quotedTy = `(NativeTy)

522522 quote IT8 = `(Reflection.IT8)

523523 quote IT16 = `(Reflection.IT16)

524524 quote IT32 = `(Reflection.IT32)

525525 quote IT64 = `(Reflection.IT64)

526526

527−instance Quotable Reflection.IntTy TT where

527+implementation Quotable Reflection.IntTy TT where

528528 quotedTy = `(Reflection.IntTy)

529529 quote (ITFixed x) = `(ITFixed ~(quote x))

530530 quote ITNative = `(Reflection.ITNative)

531531 quote ITBig = `(ITBig)

532532 quote ITChar = `(Reflection.ITChar)

533533

534−instance Quotable Reflection.IntTy Raw where

534+implementation Quotable Reflection.IntTy Raw where

535535 quotedTy = `(Reflection.IntTy)

536536 quote (ITFixed x) = `(ITFixed ~(quote {t=Raw} x))

537537 quote ITNative = `(Reflection.ITNative)

538538 quote ITBig = `(ITBig)

539539 quote ITChar = `(Reflection.ITChar)

540540

541−instance Quotable ArithTy TT where

541+implementation Quotable ArithTy TT where

542542 quotedTy = `(ArithTy)

543543 quote (ATInt x) = `(ATInt ~(quote x))

544544 quote ATDouble = `(ATDouble)

545545

546−instance Quotable ArithTy Raw where

546+implementation Quotable ArithTy Raw where

547547 quotedTy = `(ArithTy)

548548 quote (ATInt x) = `(ATInt ~(quote {t=Raw} x))

549549 quote ATDouble = `(ATDouble)

550550

551−instance Quotable Const TT where

551+implementation Quotable Const TT where

552552 quotedTy = `(Const)

553553 quote (I x) = `(I ~(quote x))

554554 quote (BI x) = `(BI ~(quote x))

@@ -566,7 +566,7 @@ instance Quotable Const TT where

566566 quote WorldType = `(WorldType)

567567 quote TheWorld = `(TheWorld)

568568

569−instance Quotable Const Raw where

569+implementation Quotable Const Raw where

570570 quotedTy = `(Const)

571571 quote (I x) = `(I ~(quote {t=Raw} x))

572572 quote (BI x) = `(BI ~(quote {t=Raw} x))

@@ -584,30 +584,30 @@ instance Quotable Const Raw where

584584 quote WorldType = `(WorldType)

585585 quote TheWorld = `(TheWorld)

586586

587−instance Quotable TTUExp TT where

587+implementation Quotable TTUExp TT where

588588 quotedTy = `(TTUExp)

589589 quote (UVar x) = `(UVar ~(quote x))

590590 quote (UVal x) = `(UVal ~(quote x))

591591

592−instance Quotable TTUExp Raw where

592+implementation Quotable TTUExp Raw where

593593 quotedTy = `(TTUExp)

594594 quote (UVar x) = `(UVar ~(quote {t=Raw} x))

595595 quote (UVal x) = `(UVal ~(quote {t=Raw} x))

596596

597−instance Quotable Universe TT where

597+implementation Quotable Universe TT where

598598 quotedTy = `(Universe)

599599 quote Reflection.NullType = `(NullType)

600600 quote Reflection.UniqueType = `(UniqueType)

601601 quote Reflection.AllTypes = `(AllTypes)

602602

603−instance Quotable Universe Raw where

603+implementation Quotable Universe Raw where

604604 quotedTy = `(Universe)

605605 quote Reflection.NullType = `(NullType)

606606 quote Reflection.UniqueType = `(UniqueType)

607607 quote Reflection.AllTypes = `(AllTypes)

608608

609609mutual

610− instance Quotable TT TT where

610+ implementation Quotable TT TT where

611611 quotedTy = `(TT)

612612 quote (P nt n tm) = `(P ~(quote nt) ~(quote n) ~(quote tm))

613613 quote (V x) = `(V ~(quote x))

@@ -618,7 +618,7 @@ mutual

618618 quote (TType uexp) = `(TType ~(quote uexp))

619619 quote (UType u) = `(UType ~(quote u))

620620

621− instance Quotable (Binder TT) TT where

621+ implementation Quotable (Binder TT) TT where

622622 quotedTy = `(Binder TT)

623623 quote (Lam x) = `(Lam {a=TT} ~(assert_total (quote x)))

624624 quote (Pi x k) = `(Pi {a=TT} ~(assert_total (quote x))

@@ -651,11 +651,11 @@ mutual

651651 quoteRawBinderTT (PVar x) = `(PVar {a=Raw} ~(quoteRawTT x))

652652 quoteRawBinderTT (PVTy x) = `(PVTy {a=Raw} ~(quoteRawTT x))

653653

654−instance Quotable Raw TT where

654+implementation Quotable Raw TT where

655655 quotedTy = `(Raw)

656656 quote = quoteRawTT

657657

658−instance Quotable (Binder Raw) TT where

658+implementation Quotable (Binder Raw) TT where

659659 quotedTy = `(Binder Raw)

660660 quote = quoteRawBinderTT

661661

@@ -678,15 +678,15 @@ mutual

678678 quoteRawBinderRaw (PVar x) = `(PVar {a=Raw} ~(quoteRawRaw x))

679679 quoteRawBinderRaw (PVTy x) = `(PVTy {a=Raw} ~(quoteRawRaw x))

680680

681−instance Quotable Raw Raw where

681+implementation Quotable Raw Raw where

682682 quotedTy = `(Raw)

683683 quote = quoteRawRaw

684684

685−instance Quotable (Binder Raw) Raw where

685+implementation Quotable (Binder Raw) Raw where

686686 quotedTy = `(Binder Raw)

687687 quote = quoteRawBinderRaw

688688

689−instance Quotable ErrorReportPart TT where

689+implementation Quotable ErrorReportPart TT where

690690 quotedTy = `(ErrorReportPart)

691691 quote (TextPart x) = `(TextPart ~(quote x))

692692 quote (NamePart n) = `(NamePart ~(quote n))

@@ -694,7 +694,7 @@ instance Quotable ErrorReportPart TT where

694694 quote (RawPart tm) = `(RawPart ~(quote tm))

695695 quote (SubReport xs) = `(SubReport ~(assert_total $ quote xs))

696696

697−instance Quotable Tactic TT where

697+implementation Quotable Tactic TT where

698698 quotedTy = `(Tactic)

699699 quote (Try tac tac') = `(Try ~(quote tac) ~(quote tac'))

700700 quote (GoalType x tac) = `(GoalType ~(quote x) ~(quote tac))

libs/prelude/Language/Reflection/Elab.idr+14−14

@@ -28,7 +28,7 @@ data Plicity =

2828 Explicit |

2929 ||| The argument is found by Idris at the application site

3030 Implicit |

31− ||| The argument is solved using type class resolution

31+ ||| The argument is solved using interface resolution

3232 Constraint

3333

3434||| Function arguments

@@ -166,23 +166,23 @@ data Elab : Type -> Type where

166166-------------

167167%access public

168168namespace Tactics

169− instance Functor Elab where

169+ implementation Functor Elab where

170170 map f t = Prim__BindElab t (\x => Prim__PureElab (f x))

171171

172− instance Applicative Elab where

172+ implementation Applicative Elab where

173173 pure x = Prim__PureElab x

174174 f <*> x = Prim__BindElab f $ \g =>

175175 Prim__BindElab x $ \y =>

176176 Prim__PureElab $ g y

177177

178− ||| The Alternative instance on Elab represents left-biased error

178+ ||| The Alternative implementation on Elab represents left-biased error

179179 ||| handling. In other words, `t <|> t'` will run `t`, and if it

180180 ||| fails, roll back the elaboration state and run `t'`.

181− instance Alternative Elab where

181+ implementation Alternative Elab where

182182 empty = Prim__Fail [TextPart "empty"]

183183 x <|> y = Prim__Try x y

184184

185− instance Monad Elab where

185+ implementation Monad Elab where

186186 x >>= f = Prim__BindElab x f

187187

188188 ||| Halt elaboration with an error

@@ -468,20 +468,20 @@ namespace Tactics

468468 defineFunction : FunDefn Raw -> Elab ()

469469 defineFunction defun = Prim__DefineFunction defun

470470

471− ||| Register a new instance for type class resolution.

471+ ||| Register a new implementation for interface resolution.

472472 |||

473− ||| @ className the name of the class for which an instance is being registered

474− ||| @ instName the name of the definition to use in instance search

475− addInstance : (className, instName : TTName) -> Elab ()

476− addInstance className instName = Prim__AddInstance className instName

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

474+ ||| @ instName the name of the definition to use in implementation search

475+ addInstance : (ifaceName, instName : TTName) -> Elab ()

476+ addInstance ifaceName instName = Prim__AddInstance ifaceName instName

477477

478− ||| Determine whether a name denotes a class.

478+ ||| Determine whether a name denotes an interface.

479479 |||

480− ||| @ name a name that might denote a class.

480+ ||| @ name a name that might denote an interface.

481481 isTCName : (name : TTName) -> Elab Bool

482482 isTCName name = Prim__IsTCName name

483483

484− ||| Attempt to solve the current goal with a type class dictionary

484+ ||| Attempt to solve the current goal with an interface dictionary

485485 |||

486486 ||| @ fn the name of the definition being elaborated (to prevent Idris

487487 ||| from looping)

libs/prelude/Prelude.idr+25−25

@@ -46,80 +46,80 @@ decAsBool (Yes _) = True

4646decAsBool (No _) = False

4747

4848

49−---- Functor instances

49+---- Functor implementations

5050

51−instance Functor PrimIO where

51+implementation Functor PrimIO where

5252 map f io = prim_io_bind io (prim_io_return . f)

5353

54−instance Functor Maybe where

54+implementation Functor Maybe where

5555 map f (Just x) = Just (f x)

5656 map f Nothing = Nothing

5757

58−instance Functor (Either e) where

58+implementation Functor (Either e) where

5959 map f (Left l) = Left l

6060 map f (Right r) = Right (f r)

6161

62−---- Applicative instances

62+---- Applicative implementations

6363

64−instance Applicative PrimIO where

64+implementation Applicative PrimIO where

6565 pure = prim_io_return

6666

6767 am <*> bm = prim_io_bind am (\f => prim_io_bind bm (prim_io_return . f))

6868

69−instance Applicative Maybe where

69+implementation Applicative Maybe where

7070 pure = Just

7171

7272 (Just f) <*> (Just a) = Just (f a)

7373 _ <*> _ = Nothing

7474

75−instance Applicative (Either e) where

75+implementation Applicative (Either e) where

7676 pure = Right

7777

7878 (Left a) <*> _ = Left a

7979 (Right f) <*> (Right r) = Right (f r)

8080 (Right _) <*> (Left l) = Left l

8181

82−instance Applicative List where

82+implementation Applicative List where

8383 pure x = [x]

8484

8585 fs <*> vs = concatMap (\f => map f vs) fs

8686

87−---- Alternative instances

87+---- Alternative implementations

8888

89−instance Alternative Maybe where

89+implementation Alternative Maybe where

9090 empty = Nothing

9191

9292 (Just x) <|> _ = Just x

9393 Nothing <|> v = v

9494

95−instance Alternative List where

95+implementation Alternative List where

9696 empty = []

9797

9898 (<|>) = (++)

9999

100−---- Monad instances

100+---- Monad implementations

101101

102−instance Monad PrimIO where

102+implementation Monad PrimIO where

103103 b >>= k = prim_io_bind b k

104104

105−instance Monad Maybe where

105+implementation Monad Maybe where

106106 Nothing >>= k = Nothing

107107 (Just x) >>= k = k x

108108

109−instance Monad (Either e) where

109+implementation Monad (Either e) where

110110 (Left n) >>= _ = Left n

111111 (Right r) >>= f = f r

112112

113−instance Monad List where

113+implementation Monad List where

114114 m >>= f = concatMap f m

115115

116−---- Traversable instances

116+---- Traversable implementations

117117

118−instance Traversable Maybe where

118+implementation Traversable Maybe where

119119 traverse f Nothing = pure Nothing

120120 traverse f (Just x) = [| Just (f x) |]

121121

122−instance Traversable List where

122+implementation Traversable List where

123123 traverse f [] = pure List.Nil

124124 traverse f (x::xs) = [| List.(::) (f x) (traverse f xs) |]

125125

@@ -145,7 +145,7 @@ total natEnumFromThenTo : Nat -> Nat -> Nat -> List Nat

145145natEnumFromThenTo _ Z _ = []

146146natEnumFromThenTo n (S inc) m = map (plus n . (* (S inc))) (natRange (S (divNatNZ (minus m n) (S inc) SIsNotZ)))

147147

148−class Enum a where

148+interface Enum a where

149149 total pred : a -> a

150150 total succ : a -> a

151151 succ e = fromNat (S (toNat e))

@@ -160,7 +160,7 @@ class Enum a where

160160 total enumFromThenTo : a -> a -> a -> List a

161161 enumFromThenTo x1 x2 y = map fromNat (natEnumFromThenTo (toNat x1) (toNat x2) (toNat y))

162162

163−instance Enum Nat where

163+implementation Enum Nat where

164164 pred n = Nat.pred n

165165 succ n = S n

166166 toNat x = id x

@@ -169,7 +169,7 @@ instance Enum Nat where

169169 enumFromThenTo x y z = natEnumFromThenTo x y z

170170 enumFromTo x y = natEnumFromTo x y

171171

172−instance Enum Integer where

172+implementation Enum Integer where

173173 pred n = n - 1

174174 succ n = n + 1

175175 toNat n = cast n

@@ -187,7 +187,7 @@ instance Enum Integer where

187187 go [] = []

188188 go (x :: xs) = n + (cast x * inc) :: go xs

189189

190−instance Enum Int where

190+implementation Enum Int where

191191 pred n = n - 1

192192 succ n = n + 1

193193 toNat n = cast n

@@ -207,7 +207,7 @@ instance Enum Int where

207207 go [] = []

208208 go (x :: xs) = n + (cast x * inc) :: go xs

209209

210−instance Enum Char where

210+implementation Enum Char where

211211 toNat c = toNat (ord c)

212212 fromNat n = chr (fromNat n)

213213

libs/prelude/Prelude/Algebra.idr+3−3

@@ -7,7 +7,7 @@ infixl 6 <+>

77%access public

99--------------------------------------------------------------------------------

10−-- A modest class hierarchy

10+-- A modest interface hierarchy

1111--------------------------------------------------------------------------------

1212

1313||| Sets equipped with a single binary operation that is associative. Must

@@ -15,7 +15,7 @@ infixl 6 <+>

1515|||

1616||| + Associativity of `<+>`:

1717||| forall a b c, a <+> (b <+> c) == (a <+> b) <+> c

18−class Semigroup a where

18+interface Semigroup a where

1919 (<+>) : a -> a -> a

2020

2121

@@ -28,6 +28,6 @@ class Semigroup a where

2828||| + Neutral for `<+>`:

2929||| forall a, a <+> neutral == a

3030||| forall a, neutral <+> a == a

31−class Semigroup a => Monoid a where

31+interface Semigroup a => Monoid a where

3232 neutral : a

3333

libs/prelude/Prelude/Applicative.idr+2−2

@@ -12,7 +12,7 @@ import Prelude.Functor

1212

1313infixl 2 <*>

1414

15−class Functor f => Applicative (f : Type -> Type) where

15+interface Functor f => Applicative (f : Type -> Type) where

1616 pure : a -> f a

1717 (<*>) : f (a -> b) -> f a -> f b

1818

@@ -37,7 +37,7 @@ liftA3 : Applicative f => (a -> b -> c -> d) -> f a -> f b -> f c -> f d

3737liftA3 f a b c = (map f a) <*> b <*> c

3838

3939infixl 3 <|>

40−class Applicative f => Alternative (f : Type -> Type) where

40+interface Applicative f => Alternative (f : Type -> Type) where

4141 empty : f a

4242 (<|>) : f a -> f a -> f a

4343

libs/prelude/Prelude/Cast.idr+14−14

@@ -3,8 +3,8 @@ module Prelude.Cast

33import Prelude.Bool

44import public Builtins

6−||| Type class for transforming an instance of a data type to another type.

7−class Cast from to where

6+||| Interface for transforming an instance of a data type to another type.

7+interface Cast from to where

88 ||| Perform a cast operation.

99 |||

1010 ||| @orig The original type.

@@ -12,46 +12,46 @@ class Cast from to where

1212

1313-- String casts

1414

15−instance Cast String Int where

15+implementation Cast String Int where

1616 cast = prim__fromStrInt

1717

18−instance Cast String Double where

18+implementation Cast String Double where

1919 cast = prim__strToFloat

2020

21−instance Cast String Integer where

21+implementation Cast String Integer where

2222 cast = prim__fromStrBigInt

2323

2424-- Int casts

2525

26−instance Cast Int String where

26+implementation Cast Int String where

2727 cast = prim__toStrInt

2828

29−instance Cast Int Double where

29+implementation Cast Int Double where

3030 cast = prim__toFloatInt

3131

32−instance Cast Int Integer where

32+implementation Cast Int Integer where

3333 cast = prim__sextInt_BigInt

3434

3535-- Double casts

3636

37−instance Cast Double String where

37+implementation Cast Double String where

3838 cast = prim__floatToStr

3939

40−instance Cast Double Int where

40+implementation Cast Double Int where

4141 cast = prim__fromFloatInt

4242

43−instance Cast Double Integer where

43+implementation Cast Double Integer where

4444 cast = prim__fromFloatBigInt

4545

4646-- Integer casts

4747

48−instance Cast Integer String where

48+implementation Cast Integer String where

4949 cast = prim__toStrBigInt

5050

51−instance Cast Integer Double where

51+implementation Cast Integer Double where

5252 cast = prim__toFloatBigInt

5353

5454-- Char casts

5555

56−instance Cast Char Int where

56+implementation Cast Char Int where

5757 cast = prim__charToInt

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

@@ -13,7 +13,7 @@ chr x = if (x >= 0 && x < 0x110000)

1313 then assert_total (prim__intToChar x)

1414 else '\0'

1515

16−instance Cast Int Char where

16+implementation Cast Int Char where

1717 cast = chr

1818

1919||| Return the ASCII representation of the character.

libs/prelude/Prelude/Classes.idr+66−66

@@ -19,53 +19,53 @@ intToBool x = True

1919boolOp : (a -> a -> Int) -> a -> a -> Bool

2020boolOp op x y = intToBool (op x y)

2121

22−-- ---------------------------------------------------------- [ Equality Class ]

23−||| The Eq class defines inequality and equality.

24−class Eq a where

22+-- ---------------------------------------------------------- [ Equality Interface ]

23+||| The Eq interface defines inequality and equality.

24+interface Eq a where

2525 (==) : a -> a -> Bool

2626 (/=) : a -> a -> Bool

2727

2828 x /= y = not (x == y)

2929 x == y = not (x /= y)

3030

31−instance Eq () where

31+implementation Eq () where

3232 () == () = True

3333

34−instance Eq Int where

34+implementation Eq Int where

3535 (==) = boolOp prim__eqInt

3636

37−instance Eq Integer where

37+implementation Eq Integer where

3838 (==) = boolOp prim__eqBigInt

3939

40−instance Eq Double where

40+implementation Eq Double where

4141 (==) = boolOp prim__eqFloat

4242

43−instance Eq Char where

43+implementation Eq Char where

4444 (==) = boolOp prim__eqChar

4545

46−instance Eq String where

46+implementation Eq String where

4747 (==) = boolOp prim__eqString

4848

49−instance Eq Ptr where

49+implementation Eq Ptr where

5050 (==) = boolOp prim__eqPtr

5151

52−instance Eq ManagedPtr where

52+implementation Eq ManagedPtr where

5353 (==) = boolOp prim__eqManagedPtr

5454

55−instance Eq Bool where

55+implementation Eq Bool where

5656 True == True = True

5757 True == False = False

5858 False == True = False

5959 False == False = True

6060

61−instance (Eq a, Eq b) => Eq (a, b) where

61+implementation (Eq a, Eq b) => Eq (a, b) where

6262 (==) (a, c) (b, d) = (a == b) && (c == d)

6363

6464

65−-- ---------------------------------------------------------- [ Ordering Class ]

65+-- ---------------------------------------------------------- [ Ordering Interface ]

6666%elim data Ordering = LT | EQ | GT

6767

68−instance Eq Ordering where

68+implementation Eq Ordering where

6969 LT == LT = True

7070 EQ == EQ = True

7171 GT == GT = True

@@ -77,8 +77,8 @@ thenCompare LT y = LT

7777thenCompare EQ y = y

7878thenCompare GT y = GT

7979

80−||| The Ord class defines comparison operations on ordered data types.

81−class Eq a => Ord a where

80+||| The Ord interface defines comparison operations on ordered data types.

81+interface Eq a => Ord a where

8282 compare : a -> a -> Ordering

8383

8484 (<) : a -> a -> Bool

@@ -103,137 +103,137 @@ class Eq a => Ord a where

103103 min : a -> a -> a

104104 min x y = if (x < y) then x else y

105105

106−instance Ord () where

106+implementation Ord () where

107107 compare () () = EQ

108108

109−instance Ord Int where

109+implementation Ord Int where

110110 compare x y = if (x == y) then EQ else

111111 if (boolOp prim__sltInt x y) then LT else

112112 GT

113113

114114

115−instance Ord Integer where

115+implementation Ord Integer where

116116 compare x y = if (x == y) then EQ else

117117 if (boolOp prim__sltBigInt x y) then LT else

118118 GT

119119

120120

121−instance Ord Double where

121+implementation Ord Double where

122122 compare x y = if (x == y) then EQ else

123123 if (boolOp prim__sltFloat x y) then LT else

124124 GT

125125

126126

127−instance Ord Char where

127+implementation Ord Char where

128128 compare x y = if (x == y) then EQ else

129129 if (boolOp prim__sltChar x y) then LT else

130130 GT

131131

132132

133−instance Ord String where

133+implementation Ord String where

134134 compare x y = if (x == y) then EQ else

135135 if (boolOp prim__ltString x y) then LT else

136136 GT

137137

138138

139−instance Ord Bool where

139+implementation Ord Bool where

140140 compare True True = EQ

141141 compare False False = EQ

142142 compare False True = LT

143143 compare True False = GT

144144

145145

146−instance (Ord a, Ord b) => Ord (a, b) where

146+implementation (Ord a, Ord b) => Ord (a, b) where

147147 compare (xl, xr) (yl, yr) =

148148 if xl /= yl

149149 then compare xl yl

150150 else compare xr yr

151151

152−-- --------------------------------------------------------- [ Numerical Class ]

153−||| The Num class defines basic numerical arithmetic.

154−class Num a where

152+-- --------------------------------------------------------- [ Numerical Interface ]

153+||| The Num interface defines basic numerical arithmetic.

154+interface Num a where

155155 (+) : a -> a -> a

156156 (*) : a -> a -> a

157157 ||| Conversion from Integer.

158158 fromInteger : Integer -> a

159159

160−instance Num Integer where

160+implementation Num Integer where

161161 (+) = prim__addBigInt

162162 (*) = prim__mulBigInt

163163

164164 fromInteger = id

165165

166−instance Num Int where

166+implementation Num Int where

167167 (+) = prim__addInt

168168 (*) = prim__mulInt

169169

170170 fromInteger = prim__truncBigInt_Int

171171

172172

173−instance Num Double where

173+implementation Num Double where

174174 (+) = prim__addFloat

175175 (*) = prim__mulFloat

176176

177177 fromInteger = prim__toFloatBigInt

178178

179−instance Num Bits8 where

179+implementation Num Bits8 where

180180 (+) = prim__addB8

181181 (*) = prim__mulB8

182182 fromInteger = prim__truncBigInt_B8

183183

184−instance Num Bits16 where

184+implementation Num Bits16 where

185185 (+) = prim__addB16

186186 (*) = prim__mulB16

187187 fromInteger = prim__truncBigInt_B16

188188

189−instance Num Bits32 where

189+implementation Num Bits32 where

190190 (+) = prim__addB32

191191 (*) = prim__mulB32

192192 fromInteger = prim__truncBigInt_B32

193193

194−instance Num Bits64 where

194+implementation Num Bits64 where

195195 (+) = prim__addB64

196196 (*) = prim__mulB64

197197 fromInteger = prim__truncBigInt_B64

198198

199−-- --------------------------------------------------------- [ Negatable Class ]

200−||| The `Neg` class defines operations on numbers which can be negative.

201−class Num a => Neg a where

199+-- --------------------------------------------------------- [ Negatable Interface ]

200+||| The `Neg` interface defines operations on numbers which can be negative.

201+interface Num a => Neg a where

202202 ||| The underlying implementation of unary minus. `-5` desugars to `negate (fromInteger 5)`.

203203 negate : a -> a

204204 (-) : a -> a -> a

205205 ||| Absolute value

206206 abs : a -> a

207207

208−instance Neg Integer where

208+implementation Neg Integer where

209209 negate x = prim__subBigInt 0 x

210210 (-) = prim__subBigInt

211211 abs x = if x < 0 then -x else x

212212

213−instance Neg Int where

213+implementation Neg Int where

214214 negate x = prim__subInt 0 x

215215 (-) = prim__subInt

216216 abs x = if x < (prim__truncBigInt_Int 0) then -x else x

217217

218−instance Neg Double where

218+implementation Neg Double where

219219 negate x = prim__negFloat x

220220 (-) = prim__subFloat

221221 abs x = if x < (prim__toFloatBigInt 0) then -x else x

222222

223223-- ------------------------------------------------------------

224−instance Eq Bits8 where

224+implementation Eq Bits8 where

225225 x == y = intToBool (prim__eqB8 x y)

226226

227−instance Eq Bits16 where

227+implementation Eq Bits16 where

228228 x == y = intToBool (prim__eqB16 x y)

229229

230−instance Eq Bits32 where

230+implementation Eq Bits32 where

231231 x == y = intToBool (prim__eqB32 x y)

232232

233−instance Eq Bits64 where

233+implementation Eq Bits64 where

234234 x == y = intToBool (prim__eqB64 x y)

235235

236−instance Ord Bits8 where

236+implementation Ord Bits8 where

237237 (<) = boolOp prim__ltB8

238238 (>) = boolOp prim__gtB8

239239 (<=) = boolOp prim__lteB8

@@ -242,7 +242,7 @@ instance Ord Bits8 where

242242 else if l > r then GT

243243 else EQ

244244

245−instance Ord Bits16 where

245+implementation Ord Bits16 where

246246 (<) = boolOp prim__ltB16

247247 (>) = boolOp prim__gtB16

248248 (<=) = boolOp prim__lteB16

@@ -251,7 +251,7 @@ instance Ord Bits16 where

251251 else if l > r then GT

252252 else EQ

253253

254−instance Ord Bits32 where

254+implementation Ord Bits32 where

255255 (<) = boolOp prim__ltB32

256256 (>) = boolOp prim__gtB32

257257 (<=) = boolOp prim__lteB32

@@ -260,7 +260,7 @@ instance Ord Bits32 where

260260 else if l > r then GT

261261 else EQ

262262

263−instance Ord Bits64 where

263+implementation Ord Bits64 where

264264 (<) = boolOp prim__ltB64

265265 (>) = boolOp prim__gtB64

266266 (<=) = boolOp prim__lteB64

@@ -271,36 +271,36 @@ instance Ord Bits64 where

271271

272272-- ------------------------------------------------------------- [ Bounded ]

273273

274−class Ord b => MinBound b where

274+interface Ord b => MinBound b where

275275 ||| The lower bound for the type

276276 minBound : b

277277

278−class Ord b => MaxBound b where

278+interface Ord b => MaxBound b where

279279 ||| The upper bound for the type

280280 maxBound : b

281281

282−instance MinBound Bits8 where

282+implementation MinBound Bits8 where

283283 minBound = 0x0

284284

285−instance MaxBound Bits8 where

285+implementation MaxBound Bits8 where

286286 maxBound = 0xff

287287

288−instance MinBound Bits16 where

288+implementation MinBound Bits16 where

289289 minBound = 0x0

290290

291−instance MaxBound Bits16 where

291+implementation MaxBound Bits16 where

292292 maxBound = 0xffff

293293

294−instance MinBound Bits32 where

294+implementation MinBound Bits32 where

295295 minBound = 0x0

296296

297−instance MaxBound Bits32 where

297+implementation MaxBound Bits32 where

298298 maxBound = 0xffffffff

299299

300−instance MinBound Bits64 where

300+implementation MinBound Bits64 where

301301 minBound = 0x0

302302

303−instance MaxBound Bits64 where

303+implementation MaxBound Bits64 where

304304 maxBound = 0xffffffffffffffff

305305

306306

@@ -314,7 +314,7 @@ instance MaxBound Bits64 where

314314-- --------------------------------------------------------------- [ Integrals ]

315315%default partial

316316

317−class Integral a where

317+interface Integral a where

318318 div : a -> a -> a

319319 mod : a -> a -> a

320320

@@ -327,7 +327,7 @@ modBigInt : Integer -> Integer -> Integer

327327modBigInt x y = case y == 0 of

328328 False => prim__sremBigInt x y

329329

330−instance Integral Integer where

330+implementation Integral Integer where

331331 div = divBigInt

332332 mod = modBigInt

333333

@@ -341,7 +341,7 @@ modInt : Int -> Int -> Int

341341modInt x y = case y == 0 of

342342 False => prim__sremInt x y

343343

344−instance Integral Int where

344+implementation Integral Int where

345345 div = divInt

346346 mod = modInt

347347

@@ -354,7 +354,7 @@ modB8 : Bits8 -> Bits8 -> Bits8

354354modB8 x y = case y == 0 of

355355 False => prim__sremB8 x y

356356

357−instance Integral Bits8 where

357+implementation Integral Bits8 where

358358 div = divB8

359359 mod = modB8

360360

@@ -367,7 +367,7 @@ modB16 : Bits16 -> Bits16 -> Bits16

367367modB16 x y = case y == 0 of

368368 False => prim__sremB16 x y

369369

370−instance Integral Bits16 where

370+implementation Integral Bits16 where

371371 div = divB16

372372 mod = modB16

373373

@@ -380,7 +380,7 @@ modB32 : Bits32 -> Bits32 -> Bits32

380380modB32 x y = case y == 0 of

381381 False => prim__sremB32 x y

382382

383−instance Integral Bits32 where

383+implementation Integral Bits32 where

384384 div = divB32

385385 mod = modB32

386386

@@ -393,7 +393,7 @@ modB64 : Bits64 -> Bits64 -> Bits64

393393modB64 x y = case y == 0 of

394394 False => prim__sremB64 x y

395395

396−instance Integral Bits64 where

396+implementation Integral Bits64 where

397397 div = divB64

398398 mod = modB64

399399

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

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

9090-- Instances

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

9292

93−instance (Eq a, Eq b) => Eq (Either a b) where

93+implementation (Eq a, Eq b) => Eq (Either a b) where

9494 (==) (Left x) (Left y) = x == y

9595 (==) (Right x) (Right y) = x == y

9696 (==) _ _ = False

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

@@ -43,7 +43,7 @@ getFileError = do MkRaw err <- foreign FFI_C "idris_mkFileError"

4343 (Ptr -> IO (Raw FileError)) prim__vm

4444 return err

4545

46−instance Show FileError where

46+implementation Show FileError where

4747 show FileNotFound = "File Not Found"

4848 show PermissionDenied = "Permission Denied"

4949 show (GenericFileError errno) = strError errno

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

@@ -9,7 +9,7 @@ import Prelude.Algebra

99%access public

1010%default total

1111

12−class Foldable (t : Type -> Type) where

12+interface Foldable (t : Type -> Type) where

1313 foldr : (elt -> acc -> acc) -> acc -> t elt -> acc

1414 foldl : (acc -> elt -> acc) -> acc -> t elt -> acc

1515 foldl f z t = foldr (flip (.) . flip f) id t z

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

@@ -4,7 +4,7 @@ import Prelude.Basics

55||| Functors allow a uniform action over a parameterised type.

66||| @ f a parameterised type

7−class Functor (f : Type -> Type) where

7+interface Functor (f : Type -> Type) where

88 ||| Apply a function across everything of type 'a' in a

99 ||| parameterised type

1010 ||| @ f the parameterised type

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

@@ -56,7 +56,7 @@ data NonEmpty : (xs : List a) -> Type where

5656 ||| The proof that a cons cell is non-empty

5757 IsNonEmpty : NonEmpty (x :: xs)

5858

59−instance Uninhabited (NonEmpty []) where

59+implementation Uninhabited (NonEmpty []) where

6060 uninhabited IsNonEmpty impossible

6161

6262||| Decide whether a list is non-empty

@@ -74,7 +74,7 @@ data InBounds : (k : Nat) -> (xs : List a) -> Type where

7474 ||| Valid indices can be extended

7575 InLater : InBounds k xs -> InBounds (S k) (x :: xs)

7676

77−instance Uninhabited (InBounds k []) where

77+implementation Uninhabited (InBounds k []) where

7878 uninhabited InFirst impossible

7979

8080||| Decide whether `k` is a valid index into `xs`

@@ -252,7 +252,7 @@ replicate (S n) x = x :: replicate n x

252252-- Instances

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

254254

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

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

256256 (==) [] [] = True

257257 (==) (x::xs) (y::ys) =

258258 if x == y then

@@ -262,7 +262,7 @@ instance (Eq a) => Eq (List a) where

262262 (==) _ _ = False

263263

264264

265−instance Ord a => Ord (List a) where

265+implementation Ord a => Ord (List a) where

266266 compare [] [] = EQ

267267 compare [] _ = LT

268268 compare _ [] = GT

@@ -272,13 +272,13 @@ instance Ord a => Ord (List a) where

272272 else

273273 compare xs ys

274274

275−instance Semigroup (List a) where

275+implementation Semigroup (List a) where

276276 (<+>) = (++)

277277

278−instance Monoid (List a) where

278+implementation Monoid (List a) where

279279 neutral = []

280280

281−instance Functor List where

281+implementation Functor List where

282282 map f [] = []

283283 map f (x::xs) = f x :: map f xs

284284

@@ -349,7 +349,7 @@ mapMaybe f (x::xs) =

349349-- Folds

350350--------------------------------------------------------------------------------

351351

352−instance Foldable List where

352+implementation Foldable List where

353353 foldr c n [] = n

354354 foldr c n (x::xs) = c x (foldr c n xs)

355355

@@ -590,7 +590,7 @@ delete = deleteBy (==)

590590unionBy : (a -> a -> Bool) -> List a -> List a -> List a

591591unionBy eq xs ys = xs ++ foldl (flip (deleteBy eq)) (nubBy eq ys) xs

592592

593−||| Compute the union of two lists according to their `Eq` instance.

593+||| Compute the union of two lists according to their `Eq` implementation.

594594|||

595595||| ```idris example

596596||| union ['d', 'o', 'g'] ['c', 'o', 'w']

libs/prelude/Prelude/Maybe.idr+9−9

@@ -72,25 +72,25 @@ raiseToMaybe : (Monoid a, Eq a) => a -> Maybe a

7272raiseToMaybe x = if x == neutral then Nothing else Just x

7373

7474--------------------------------------------------------------------------------

75−-- Class instances

75+-- Interface implementations

7676--------------------------------------------------------------------------------

7777

7878maybe_bind : Maybe a -> (a -> Maybe b) -> Maybe b

7979maybe_bind Nothing k = Nothing

8080maybe_bind (Just x) k = k x

8181

82−instance (Eq a) => Eq (Maybe a) where

82+implementation (Eq a) => Eq (Maybe a) where

8383 Nothing == Nothing = True

8484 Nothing == (Just _) = False

8585 (Just _) == Nothing = False

8686 (Just a) == (Just b) = a == b

8787

88−||| Prioritised choice. Just like the `Alternative` instance, the

88+||| Prioritised choice. Just like the `Alternative` implementation, the

8989||| `Semigroup` for `Maybe a` keeps the first succeeding computation.

9090|||

9191||| **NB**: This is a different choice than in the Haskell libraries.

9292||| Use `collectJust` to get the Haskell behaviour.

93−instance Semigroup (Maybe a) where

93+implementation Semigroup (Maybe a) where

9494 Nothing <+> m = m

9595 (Just x) <+> _ = Just x

9696

@@ -98,20 +98,20 @@ instance Semigroup (Maybe a) where

9898||| designated neutral element and collecting the contents of the

9999||| `Just` constructors using a semigroup structure on `a`. This is

100100||| the behaviour in the Haskell libraries.

101−instance [collectJust] Semigroup a => Semigroup (Maybe a) where

101+implementation [collectJust] Semigroup a => Semigroup (Maybe a) where

102102 Nothing <+> m = m

103103 m <+> Nothing = m

104104 (Just m1) <+> (Just m2) = Just (m1 <+> m2)

105105

106−instance Monoid (Maybe a) where

106+implementation Monoid (Maybe a) where

107107 neutral = Nothing

108108

109−instance (Monoid a, Eq a) => Cast a (Maybe a) where

109+implementation (Monoid a, Eq a) => Cast a (Maybe a) where

110110 cast = raiseToMaybe

111111

112−instance (Monoid a) => Cast (Maybe a) a where

112+implementation (Monoid a) => Cast (Maybe a) a where

113113 cast = lowerMaybe

114114

115−instance Foldable Maybe where

115+implementation Foldable Maybe where

116116 foldr _ z Nothing = z

117117 foldr f z (Just x) = f x z

libs/prelude/Prelude/Monad.idr+4−4

@@ -12,7 +12,7 @@ import IO

1212

1313infixl 5 >>=

1414

15−class Applicative m => Monad (m : Type -> Type) where

15+interface Applicative m => Monad (m : Type -> Type) where

1616 (>>=) : m a -> ((result : a) -> m b) -> m b

1717

1818||| Also called `join` or mu

@@ -27,16 +27,16 @@ return = pure

2727-- Annoyingly, these need to be here, so that we can use them in other

2828-- Prelude modules other than the top level.

2929

30−instance Functor (IO' ffi) where

30+implementation Functor (IO' ffi) where

3131 map f io = io_bind io (\b => io_return (f b))

3232

33−instance Applicative (IO' ffi) where

33+implementation Applicative (IO' ffi) where

3434 pure x = io_return x

3535 f <*> a = io_bind f (\f' =>

3636 io_bind a (\a' =>

3737 io_return (f' a')))

3838

3939

40−instance Monad (IO' ffi) where

40+implementation Monad (IO' ffi) where

4141 b >>= k = io_bind b k

4242

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

@@ -23,7 +23,7 @@ import Prelude.Uninhabited

2323-- name hints for interactive editing

2424%name Nat k,j,i,n,m

2525

26−instance Uninhabited (Z = S n) where

26+implementation Uninhabited (Z = S n) where

2727 uninhabited Refl impossible

2828

2929--------------------------------------------------------------------------------

@@ -100,7 +100,7 @@ data LTE : (n, m : Nat) -> Type where

100100 ||| If n <= m, then n + 1 <= m + 1

101101 LTESucc : LTE left right -> LTE (S left) (S right)

102102

103−instance Uninhabited (LTE (S n) Z) where

103+implementation Uninhabited (LTE (S n) Z) where

104104 uninhabited LTEZero impossible

105105

106106||| Greater than or equal to

@@ -184,50 +184,50 @@ toIntNat n = toIntNat' n 0 where

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

185185

186186--------------------------------------------------------------------------------

187−-- Type class instances

187+-- Type class implementations

188188--------------------------------------------------------------------------------

189189

190−instance Eq Nat where

190+implementation Eq Nat where

191191 Z == Z = True

192192 (S l) == (S r) = l == r

193193 _ == _ = False

194194

195−instance Cast Nat Integer where

195+implementation Cast Nat Integer where

196196 cast = toIntegerNat

197197

198−instance Ord Nat where

198+implementation Ord Nat where

199199 compare Z Z = EQ

200200 compare Z (S k) = LT

201201 compare (S k) Z = GT

202202 compare (S x) (S y) = compare x y

203203

204−instance Num Nat where

204+implementation Num Nat where

205205 (+) = plus

206206 (*) = mult

207207

208208 fromInteger = fromIntegerNat

209209

210−instance MinBound Nat where

210+implementation MinBound Nat where

211211 minBound = Z

212212

213213||| Casts negative `Integers` to 0.

214−instance Cast Integer Nat where

214+implementation Cast Integer Nat where

215215 cast = fromInteger

216216

217−instance Cast String Nat where

217+implementation Cast String Nat where

218218 cast str = cast (the Integer (cast str))

219219

220−||| A wrapper for Nat that specifies the semigroup and monad instances that use (*)

220+||| A wrapper for Nat that specifies the semigroup and monad implementations that use (*)

221221record Multiplicative where

222222 constructor GetMultiplicative

223223 _ : Nat

224224

225−||| A wrapper for Nat that specifies the semigroup and monad instances that use (+)

225+||| A wrapper for Nat that specifies the semigroup and monad implementations that use (+)

226226record Additive where

227227 constructor GetAdditive

228228 _ : Nat

229229

230−instance Semigroup Multiplicative where

230+implementation Semigroup Multiplicative where

231231 (<+>) left right = GetMultiplicative $ left' * right'

232232 where

233233 left' : Nat

@@ -240,7 +240,7 @@ instance Semigroup Multiplicative where

240240 case right of

241241 GetMultiplicative m => m

242242

243−instance Semigroup Additive where

243+implementation Semigroup Additive where

244244 left <+> right = GetAdditive $ left' + right'

245245 where

246246 left' : Nat

@@ -253,20 +253,20 @@ instance Semigroup Additive where

253253 case right of

254254 GetAdditive m => m

255255

256−instance Monoid Multiplicative where

256+implementation Monoid Multiplicative where

257257 neutral = GetMultiplicative $ S Z

258258

259−instance Monoid Additive where

259+implementation Monoid Additive where

260260 neutral = GetAdditive Z

261261

262262||| Casts negative `Ints` to 0.

263−instance Cast Int Nat where

263+implementation Cast Int Nat where

264264 cast i = fromInteger (cast i)

265265

266−instance Cast Nat Int where

266+implementation Cast Nat Int where

267267 cast = toIntNat

268268

269−instance Cast Nat Double where

269+implementation Cast Nat Double where

270270 cast = cast . toIntegerNat

271271

272272--------------------------------------------------------------------------------

@@ -341,7 +341,7 @@ partial

341341divCeil : Nat -> Nat -> Nat

342342divCeil x (S y) = divCeilNZ x (S y) SIsNotZ

343343

344−instance Integral Nat where

344+implementation Integral Nat where

345345 div = divNat

346346 mod = modNat

347347

libs/prelude/Prelude/Providers.idr+3−4

@@ -15,17 +15,16 @@ data Provider : (a : Type) -> Type where

1515 ||| @ msg the error message

1616 Error : (msg : String) -> Provider a

1717

18−-- instances

19−instance Functor Provider where

18+implementation Functor Provider where

2019 map f (Provide a) = Provide (f a)

2120 map f (Error err) = Error err

2221

23−instance Applicative Provider where

22+implementation Applicative Provider where

2423 (Provide f) <*> (Provide x) = Provide (f x)

2524 (Provide f) <*> (Error err) = Error err

2625 (Error err) <*> _ = Error err

2726 pure = Provide

2827

29−instance Monad Provider where

28+implementation Monad Provider where

3029 (Provide x) >>= f = f x

3130 (Error err) >>= _ = Error err

libs/prelude/Prelude/Show.idr+22−22

@@ -19,7 +19,7 @@ import Prelude.Strings

1919||| The precedence of an Idris operator or syntactic context.

2121

22−||| Gives the constructor index of the Prec as a helper for writing instances.

22+||| Gives the constructor index of the Prec as a helper for writing implementations.

2323precCon : Prec -> Integer

2424precCon Open = 0

2525precCon Eq = 1

@@ -29,16 +29,16 @@ precCon (User n) = 4

2929precCon PrefixMinus = 5

3030precCon App = 6

3131

32−instance Eq Prec where

32+implementation Eq Prec where

3333 (==) (User m) (User n) = m == n

3434 (==) x y = precCon x == precCon y

3535

36−instance Ord Prec where

36+implementation Ord Prec where

3737 compare (User m) (User n) = compare m n

3838 compare x y = compare (precCon x) (precCon y)

3939

4040||| Things that have a canonical `String` representation.

41−class Show a where

41+interface Show a where

4242 ||| Convert a value to its `String` representation.

4343 |||

4444 ||| @ a the value to convert

@@ -78,7 +78,7 @@ showParens True s = "(" ++ s ++ ")"

7878||| ```

7979||| data Ann a = MkAnn String a

8080|||

81−||| instance Show a => Show (Ann a) where

81+||| implementation Show a => Show (Ann a) where

8282||| showPrec d (MkAnn s x) = showCon d "MkAnn" $ showArg s ++ showArg x

8383||| ```

8484showCon : (d : Prec) -> (conName : String) -> (shownArgs : String) -> String

@@ -100,13 +100,13 @@ firstCharIs p s with (strM s)

100100primNumShow : (a -> String) -> Prec -> a -> String

101101primNumShow f d x = let str = f x in showParens (d >= PrefixMinus && firstCharIs (== '-') str) str

102102

103−instance Show Int where

103+implementation Show Int where

104104 showPrec = primNumShow prim__toStrInt

105105

106−instance Show Integer where

106+implementation Show Integer where

107107 showPrec = primNumShow prim__toStrBigInt

108108

109−instance Show Double where

109+implementation Show Double where

110110 showPrec = primNumShow prim__floatToStr

111111

112112protectEsc : (Char -> Bool) -> String -> String -> String

@@ -144,52 +144,52 @@ showLitString [] = id

144144showLitString ('"'::cs) = ("\\\"" ++) . showLitString cs

145145showLitString (c ::cs) = showLitChar c . showLitString cs

146146

147−instance Show Char where

147+implementation Show Char where

148148 show '\'' = "'\\''"

149149 show c = strCons '\'' (showLitChar c "'")

150150

151−instance Show String where

151+implementation Show String where

152152 show cs = strCons '"' (showLitString (cast cs) "\"")

153153

154−instance Show Nat where

154+implementation Show Nat where

155155 show n = show (the Integer (cast n))

156156

157−instance Show Bool where

157+implementation Show Bool where

158158 show True = "True"

159159 show False = "False"

160160

161−instance Show () where

161+implementation Show () where

162162 show () = "()"

163163

164−instance Show Bits8 where

164+implementation Show Bits8 where

165165 show b = b8ToString b

166166

167−instance Show Bits16 where

167+implementation Show Bits16 where

168168 show b = b16ToString b

169169

170−instance Show Bits32 where

170+implementation Show Bits32 where

171171 show b = b32ToString b

172172

173−instance Show Bits64 where

173+implementation Show Bits64 where

174174 show b = b64ToString b

175175

176−instance (Show a, Show b) => Show (a, b) where

176+implementation (Show a, Show b) => Show (a, b) where

177177 show (x, y) = "(" ++ show x ++ ", " ++ show y ++ ")"

178178

179−instance Show a => Show (List a) where

179+implementation Show a => Show (List a) where

180180 show xs = "[" ++ show' "" xs ++ "]" where

181181 show' acc [] = acc

182182 show' acc [x] = acc ++ show x

183183 show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

184184

185−instance Show a => Show (Maybe a) where

185+implementation Show a => Show (Maybe a) where

186186 showPrec d Nothing = "Nothing"

187187 showPrec d (Just x) = showCon d "Just" $ showArg x

188188

189−instance (Show a, Show b) => Show (Either a b) where

189+implementation (Show a, Show b) => Show (Either a b) where

190190 showPrec d (Left x) = showCon d "Left" $ showArg x

191191 showPrec d (Right x) = showCon d "Right" $ showArg x

192192

193−instance (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

193+implementation (Show a, {y : a} -> Show (p y)) => Show (Sigma a p) where

194194 show (y ** prf) = "(" ++ show y ++ " ** " ++ show prf ++ ")"

195195

libs/prelude/Prelude/Stream.idr+3−3

@@ -22,7 +22,7 @@ codata Stream : Type -> Type where

2222-- Usage hints for erasure analysis

2323%used Stream.(::) e

2424

25−instance Functor Stream where

25+implementation Functor Stream where

2626 map f (x::xs) = f x :: map f xs

2727

2828||| The first element of an infinite stream

@@ -121,10 +121,10 @@ cycle {a} (x :: xs) {ok = IsNonEmpty} = x :: cycle' xs

121121 cycle' [] = x :: cycle' xs

122122 cycle' (y :: ys) = y :: cycle' ys

123123

124−instance Applicative Stream where

124+implementation Applicative Stream where

125125 pure = repeat

126126 (<*>) = zipWith apply

127127

128−instance Monad Stream where

128+implementation Monad Stream where

129129 s >>= f = diag (map f s)

130130

libs/prelude/Prelude/Strings.idr+5−5

@@ -143,19 +143,19 @@ pack = foldr strCons ""

143143singleton : Char -> String

144144singleton c = strCons c ""

145145

146−instance Cast String (List Char) where

146+implementation Cast String (List Char) where

147147 cast = unpack

148148

149−instance Cast (List Char) String where

149+implementation Cast (List Char) String where

150150 cast = pack

151151

152−instance Cast Char String where

152+implementation Cast Char String where

153153 cast = singleton

154154

155−instance Semigroup String where

155+implementation Semigroup String where

156156 (<+>) = (++)

157157

158−instance Monoid String where

158+implementation Monoid String where

159159 neutral = ""

160160

161161||| Splits the string into a part before the predicate

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

@@ -16,7 +16,7 @@ sequence_ = foldr (*>) (pure ())

1616for_ : (Foldable t, Applicative f) => t a -> (a -> f b) -> f ()

1717for_ = flip traverse_

1818

19−class (Functor t, Foldable t) => Traversable (t : Type -> Type) where

19+interface (Functor t, Foldable t) => Traversable (t : Type -> Type) where

2020 traverse : Applicative f => (a -> f b) -> t a -> f (t b)

2121

2222sequence : (Traversable t, Applicative f) => t (f a) -> f (t a)

libs/prelude/Prelude/Uninhabited.idr+2−2

@@ -6,12 +6,12 @@ module Prelude.Uninhabited

66import Builtins

88||| A canonical proof that some type is empty

9−class Uninhabited t where

9+interface Uninhabited t where

1010 ||| If I have a t, I've had a contradiction

1111 ||| @ t the uninhabited type

1212 total uninhabited : t -> Void

1313

14−instance Uninhabited Void where

14+implementation Uninhabited Void where

1515 uninhabited a = a

1616

1717||| Use an absurd assumption to discharge a proof obligation

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

@@ -129,7 +129,7 @@ getElimTy info ctors =

129129

130130data ElimArg = IHArgument TTName | NormalArgument TTName

131131

132−instance Show ElimArg where

132+implementation Show ElimArg where

133133 show (IHArgument x) = "IHArgument " ++ show x

134134 show (NormalArgument x) = "NormalArgument " ++ show x

135135

src/Idris/AbsSyntaxTree.hs+2−2

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

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

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

21092109showDeclImp o (PClass _ _ _ cs n _ ps _ _ ds _ _)

2110− = text "class" <+> text (show cs) <+> text (show n) <+> text (show ps) <> line <> showDecls o ds

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

21112111showDeclImp o (PInstance _ _ _ _ cs n _ _ t _ ds)

2112− = text "instance" <+> text (show cs) <+> text (show n) <+> prettyImp o t <> line <> showDecls o ds

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

21132113showDeclImp _ _ = text "..."

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

21152115

src/Idris/Docs.hs+7−7

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

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

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

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

119− = nest 4 (text "Type class" <+> prettyName True (ppopt_impl ppo) [] n <>

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

120120 if nullDocstring doc

121121 then empty

122122 else line <> renderDocstring (renderDocTerm (pprintDelab ist) (normaliseAll (tt_ctxt ist) [])) doc)

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

128128 <$>

129129 maybe empty

130130 ((<> line) . nest 4 .

131− (text "Instance constructor:" <$>) .

131+ (text "Implementation constructor:" <$>) .

132132 pprintFDWithoutTotality ist False)

133133 ctor

134134 <>

135− nest 4 (text "Instances:" <$>

136− vsep (if null instances then [text "<no instances>"]

135+ nest 4 (text "Implementations:" <$>

136+ vsep (if null instances then [text "<no implementations>"]

137137 else map pprintInstance normalInstances))

138138 <>

139139 (if null namedInstances then empty

140− else line <$> nest 4 (text "Named instances:" <$>

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

141141 vsep (map pprintInstance namedInstances)))

142142 <>

143143 (if null subclasses then empty

144− else line <$> nest 4 (text "Subclasses:" <$>

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

145145 vsep (map (dumpInstance . prettifySubclasses) subclasses)))

146146 <>

147147 (if null superclasses then empty

148− else line <$> nest 4 (text "Default superclass instances:" <$>

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

149149 vsep (map dumpInstance superclasses)))

150150 where

151151 params' = zip pNames (repeat False)

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

@@ -203,7 +203,7 @@ elabInstance info syn doc argDocs what fc cs n nfc ps t expn ds = do

203203 Left _ -> Nothing

204204 _ -> Nothing

205205 overlapping t' = tclift $ tfail (At fc (Msg $

206− "Overlapping instance: " ++ show t' ++ " already defined"))

206+ "Overlapping implementation: " ++ show t' ++ " already defined"))

207207 getRetType (PPi _ _ _ _ sc) = getRetType sc

208208 getRetType t = t

209209

src/Idris/ParseHelpers.hs+2−1

@@ -246,7 +246,8 @@ idrisStyle = IdentifierStyle _styleName _styleStart _styleLetter _styleReserved

246246 "case", "of", "total", "partial", "mutual",

247247 "infix", "infixl", "infixr", "rewrite",

248248 "where", "with", "syntax", "proof", "postulate",

249− "using", "namespace", "class", "instance", "parameters",

249+ "using", "namespace", "class", "instance",

250+ "interface", "implementation", "parameters",

250251 "public", "private", "abstract", "implicit",

251252 "quoteGoal", "constructor",

252253 "if", "then", "else"]

src/Idris/Parser.hs+19−2

@@ -856,7 +856,7 @@ class_ :: SyntaxInfo -> IdrisParser [PDecl]

856856class_ syn = do (doc, argDocs, acc)

857857 <- try (do (doc, argDocs) <- docstring syn

858858 acc <- optional accessibility

859− reservedHL "class"

859+ classKeyword

860860 return (doc, argDocs, acc))

861861 fc <- getFC

862862 cons <- constraintList syn

@@ -872,6 +872,15 @@ class_ syn = do (doc, argDocs, acc)

872872 where

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

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

875+

876+ classKeyword :: IdrisParser ()

877+ classKeyword = reservedHL "interface"

878+ <|> do reservedHL "class"

879+ fc <- getFC

880+ ist <- get

881+ put ist { parserWarnings =

882+ (fc, Msg "The 'class' keyword is deprecated. Use 'interface' instead.")

883+ : parserWarnings ist }

875884

876885 carg :: IdrisParser (Name, FC, PTerm)

877886 carg = do lchar '('; (i, ifc) <- name; lchar ':'; ty <- expr syn; lchar ')'

@@ -894,7 +903,7 @@ InstanceName ::= '[' Name ']';

894903-}

895904instance_ :: SyntaxInfo -> IdrisParser [PDecl]

896905instance_ syn = do (doc, argDocs)

897− <- try (docstring syn <* reservedHL "instance")

906+ <- try (docstring syn <* instanceKeyword)

898907 fc <- getFC

899908 en <- optional instanceName

900909 cs <- constraintList syn

@@ -911,6 +920,14 @@ instance_ syn = do (doc, argDocs)

911920 let n = expandNS syn n_in

912921 return n

913922 <?> "instance name"

923+ instanceKeyword :: IdrisParser ()

924+ instanceKeyword = reservedHL "implementation"

925+ <|> do reservedHL "instance"

926+ fc <- getFC

927+ ist <- get

928+ put ist { parserWarnings =

929+ (fc, Msg "The 'instance' keyword is deprecated. Use 'implementation' instead.")

930+ : parserWarnings ist }

914931

915932

916933-- | Parse a docstring

test/basic015/basic015.idr+2−2

@@ -44,11 +44,11 @@ transpose_vec (row :: rest) = let rest_trans = transpose_vec rest in

4444

4545------- A main program to read dimensions, generate and tranpose a vector

4646

47−instance Functor (Vect m) where

47+implementation Functor (Vect m) where

4848 map m [] = []

4949 map m (x :: xs) = m x :: map m xs

5050

51−instance Show a => Show (Vect m a) where

51+implementation Show a => Show (Vect m a) where

5252 show x = show (toList x)

5353 where

5454 toList : Vect m a -> List a

test/classes001/ClassName.idr+6−6

@@ -2,7 +2,7 @@ module ClassName

33||| A fancy shower with a constructor

44||| @ a the thing to be shown

5−class MyShow a where

5+interface MyShow a where

66 ||| Build a MyShow

77 constructor MkMyShow

88 ||| The shower

@@ -12,7 +12,7 @@ class MyShow a where

1212twiceAString : MyShow a => a -> String

1313twiceAString x = myShow x ++ myShow x

1414

15−instance MyShow Integer where

15+implementation MyShow Integer where

1616 myShow x = show x

1717

1818badShow : MyShow Integer

@@ -25,17 +25,17 @@ test2 : twiceAString @{ClassName.badShow} 2 = "hejhej"

2525test2 = Refl

2626

2727

28−||| Superclass fun

29−class MyMagma a where

28+||| Parent interface fun

29+interface MyMagma a where

3030 constructor MkMyMagma

3131 total op : a -> a -> a

3232

3333||| Semigroup

34−class MyMagma a => MySemigroup a where

34+interface MyMagma a => MySemigroup a where

3535 constructor MkMySemigroup

3636 total isAssoc : (x, y, z : a) -> op x $ op y z = op (op x y) z

3737

38−instance [addition] MyMagma Nat where

38+implementation [addition] MyMagma Nat where

3939 op = plus

4040

4141additionS : MySemigroup Nat

test/classes001/expected+3−3

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

1−Type class MyShow

1+Interface MyShow

22 A fancy shower with a constructor

44Parameters:

@@ -9,7 +9,7 @@ Methods:

99 The shower

1010

1111 The function is Total

12−Instance constructor:

12+Implementation constructor:

1313 MkMyShow : (myShow : a -> String) -> MyShow a

1414 Build a MyShow

1515 Arguments:

@@ -17,7 +17,7 @@ Instance constructor:

1717

1818 myShow : a -> String -- The shower

1919

20−Instances:

20+Implementations:

2121 MyShow Integer

2222MkMyShow : (myShow : a -> String) -> MyShow a

2323 Build a MyShow

test/corecords001/corecords001.idr+1−1

@@ -5,7 +5,7 @@ corecord Str a where -- Current stream is codata, not a corecord

55 head : a

66 tail : Str a

8−instance Functor Str where

8+implementation Functor Str where

99 map f (x :: xs) = (f x) :: (map f xs)

1010

1111total -- marked total to check that corecords are indeed treated as coinductive types

test/docs001/docs001.idr+7−7

@@ -1,7 +1,7 @@

1−||| class

1+||| interface

22||| @ t a type

3−class C (t : Type) where

4− ||| member of class

3+interface C (t : Type) where

4+ ||| member of interface

55 m : t

77||| type

@@ -10,11 +10,11 @@ data A = B

1010||| type 2

1111data D a b = E

1212

13−||| instance of class

14−instance C A where

13+||| implementation of interface

14+implementation C A where

1515 m = B

1616

17−||| another instance of class

17+||| another implementation of interface

1818||| @ a parameter type

19−instance C (D a b) where

19+implementation C (D a b) where

2020 m = E

test/docs001/expected+6−6

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

1−Type class C

2− class

1+Interface C

2+ interface

44Parameters:

55 t -- a type

77Methods:

88 m : C t => t

9− member of class

9+ member of interface

1010

1111 The function is Total

12−Instances:

12+Implementations:

1313 C A

14− instance of class

14+ implementation of interface

1515 C (D a b)

16− another instance of class

16+ another implementation of interface

1717 a -- parameter type

test/docs003/docs003.idr+2−2

@@ -1,9 +1,9 @@

11module docs003

3−instance [mine] Functor List where

3+implementation [mine] Functor List where

44 map m [] = []

55 map m (x :: xs) = m x :: map m xs

77||| More functors!

8−instance [another] Functor List where

8+implementation [another] Functor List where

99 map f xs = map @{mine} f xs

test/docs003/expected+4−4

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

1−Type class Functor

1+Interface Functor

22 Functors allow a uniform action over a parameterised type.

44Parameters:

@@ -10,7 +10,7 @@ Methods:

1010 parameterised type

1111

1212 The function is Total

13−Instances:

13+Implementations:

1414 Functor List

1515 Functor (IO' ffi)

1616 Functor Stream

@@ -21,12 +21,12 @@ Instances:

2121 Functor Maybe

2222 Functor (Either e)

2323

24−Named instances:

24+Named implementations:

2525 docs003.mine : Functor List

2626 docs003.another : Functor List

2727 More functors!

2828

29−Subclasses:

29+Child interfaces:

3030 Traversable f

3131 Applicative f

3232Named instance:

test/effects003/VectMissing.idr+1−1

@@ -3,7 +3,7 @@ module VectMissing

33import Data.Fin

44import Data.Vect

6−instance Uninhabited (Elem x []) where

6+implementation Uninhabited (Elem x []) where

77 uninhabited Here impossible

99shrink : (xs : Vect (S n) a) -> Elem x xs -> Vect n a

test/effects003/hangman.idr+3−3

@@ -27,10 +27,10 @@ data Hangman : HState -> Type where

2727 (missing : Vect m Char) ->

2828 Hangman (Running guesses m)

2929

30−instance Default (Hangman NotRunning) where

30+implementation Default (Hangman NotRunning) where

3131 default = Init

3232

33−instance Show (Hangman s) where

33+implementation Show (Hangman s) where

3434 show Init = "Not ready yet"

3535 show (GameWon w) = "You won! Successfully guessed " ++ w

3636 show (GameLost w) = "You lost! The word was " ++ w

@@ -139,7 +139,7 @@ whether the letter is in the word, and branch accordingly (and if it

139139is in the word, update the vector of missing letters to be the right

140140length). -}

141141

142−instance Handler HangmanRules m where

142+implementation Handler HangmanRules m where

143143 handle (MkH w g got []) Won k = k () (GameWon w)

144144 handle (MkH w Z got m) Lost k = k () (GameLost w)

145145

test/error003/ErrorReflection.idr+2−2

@@ -11,7 +11,7 @@ import Data.Vect

1111

1212data Ty = TUnit | TFun Ty Ty

1313

14−instance Show Ty where

14+implementation Show Ty where

1515 show TUnit = "()"

1616 show (TFun t1 t2) = "(" ++ show t1 ++ " => " ++ show t2 ++ ")"

1717

@@ -33,7 +33,7 @@ namespace ErrorReports

3333 | TFun Ty' Ty'

3434 | TVar Int String -- To show in unification failures

3535

36− instance Show Ty' where

36+ implementation Show Ty' where

3737 show TUnit = "()"

3838 show (TFun x y) = "(" ++ show x ++ " => " ++ show y ++ ")"

3939 show (TVar i n) = n ++ "(" ++ cast i ++ ")"

test/idrisdoc004/TestTypeclasses.idr+2−2

@@ -3,6 +3,6 @@ module TestTypeclasses

33||| This is a test

44|||

55||| @ a Test arg

6−class Test a where

6+interface Test a where

77 ||| Test function

8− test : a -> Int

8+ test : a -> Int

test/interactive011/interactive011.idr+1−1

@@ -2,7 +2,7 @@ import Data.Vect

33data Foo = Bar | Baz

5−instance Show Foo where

5+implementation Show Foo where

77append : Vect n a -> Vect m a -> Vect (n + m) a

88append (x :: xs) ys = ?append_rhs_2

test/meta002/AgdaStyleReflection.idr+1−1

@@ -17,7 +17,7 @@ record Arg a where

1717 plicity : Plicity

1818 argValue : a

1919

20−instance Functor Arg where

20+implementation Functor Arg where

2121 map f (MkArg plic x) = MkArg plic (f x)

2222

2323||| Reflected terms, in the tradition of Agda's reflection library

test/meta002/Deriving.idr+1−1

@@ -14,7 +14,7 @@ total

1414decVectEq : DecEq a => (xs, ys : Vect n a) -> Dec (xs = ys)

1515%runElab (deriveDecEq `{decVectEq})

1616

17−instance DecEq a => DecEq (Vect n a) where

17+implementation DecEq a => DecEq (Vect n a) where

1818 decEq xs ys = decVectEq xs ys

1919

2020forgetProof : Dec a -> Bool

test/meta002/Tacs.idr+1−1

@@ -102,7 +102,7 @@ namespace STLC

102102

103103 %name Ty t,t',t''

104104

105− instance Quotable Ty TT where

105+ implementation Quotable Ty TT where

106106 quotedTy = `(Ty : Type)

107107 quote UNIT = `(UNIT : Ty)

108108 quote (ARR t t') = `(ARR ~(quote t) ~(quote t'))

test/proof003/test015.idr+2−2

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

77 B0 : Bit Z

88 B1 : Bit (S Z)

10−instance Show (Bit n) where

10+implementation Show (Bit n) where

1111 show = show' where

1212 show' : Bit x -> String

1313 show' B0 = "0"

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

1919 Zero : Binary Z Z

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

2121

22−instance Show (Binary w k) where

22+implementation Show (Binary w k) where

2323 show Zero = ""

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

2525

test/proofsearch001/proofsearch001.idr+2−2

@@ -1,7 +1,7 @@

11%default total

3−class C a (f : Bool -> Bool) | a where {}

4−instance C Int Bool.not where {}

3+interface C a (f : Bool -> Bool) | a where {}

4+implementation C Int Bool.not where {}

66foo : C Int g => {auto pf : g True = False} -> Unit

77foo = ()

test/proofsearch003/proofsearch003.idr+2−2

@@ -6,10 +6,10 @@ data Seq : Fin 9 -> Fin 9 -> Type where

66 Seq12 : {n : Fin 8} -> Seq (weaken n) (FS n)

77 Seq21 : {n : Fin 8} -> Seq (FS n) (weaken n)

9−class Evil t where

9+interface Evil t where

1010 value : t -> Fin 9

1111

12−instance Evil Wrapper where

12+implementation Evil Wrapper where

1313 value (Wrap n) = n

1414

1515consTest : (Evil t) => (a : t) -> (b : t) ->

test/records002/record002.idr+1−1

@@ -2,7 +2,7 @@ record Foo (param : Nat) where

22 constructor MkFoo

33 num : Int

5−instance Show (Foo n) where

5+implementation Show (Foo n) where

66 show f = show (param_param f) ++ ", " ++ show (num f)

88main : IO ()

test/reg001/reg001.idr+5−5

@@ -7,7 +7,7 @@ import Data.HVect

77import Data.Fin

88import Control.Isomorphism

10−class Functor f => VerifiedFunctor (f : Type -> Type) where

10+interface Functor f => VerifiedFunctor (f : Type -> Type) where

1111 identity : (fa : f a) -> map Basics.id fa = fa

1212

1313data Imp : Type where

@@ -66,7 +66,7 @@ soTrue : So b -> b = True

6666soTrue {b = False} x = soFalseElim x

6767soTrue {b = True} x = Refl

6868

69−class Eq alpha => ReflEqEq alpha where

69+interface Eq alpha => ReflEqEq alpha where

7070 reflexive_eqeq : (a : alpha) -> So (a == a)

7171

7272modifyFun : (Eq alpha) =>

@@ -126,7 +126,7 @@ interp (TNot x) = map not (interp x)

126126

127127data Result str a = Success str a | Failure String

128128

129−instance Functor (Result str) where

129+implementation Functor (Result str) where

130130 map f (Success s x) = Success s (f x)

131131 map f (Failure e ) = Failure e

132132

@@ -154,13 +154,13 @@ admissible {t} x Left = column {t} x <= 2

154154admissible {t} x Right = column {t} x >= 2

155155

156156

157−class Set univ where

157+interface Set univ where

158158 member : univ -> univ -> Type

159159

160160isSubsetOf : Set univ => univ -> univ -> Type

161161isSubsetOf {univ} a b = (c : univ) -> (member c a) -> (member c b)

162162

163−class Set univ => HasPower univ where

163+interface Set univ => HasPower univ where

164164 Powerset : (a : univ) ->

165165 Sigma univ (\Pa => (c : univ) ->

166166 (isSubsetOf c a) -> member c Pa)

test/reg018/reg018b.idr+1−1

@@ -8,7 +8,7 @@ showB : B -> String

88showB (I x) = "I" ++ showB x

99showB (Z x) = "Z" ++ showB x

1010

11−instance Show B where show = showB

11+implementation Show B where show = showB

1212

1313os : B

1414os = Z os

test/reg027/expected+2−2

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

11<<int fn>>

226

3−reg027a.idr:9:10:

4−Overlapping instance: Show (Int -> a) already defined

3+reg027a.idr:9:16:

4+Overlapping implementation: Show (Int -> a) already defined

test/reg027/reg027.idr+5−5

@@ -1,22 +1,22 @@

11module Main

3−instance Show (Int -> b) where

3+implementation Show (Int -> b) where

44 show x = "<<int fn>>"

6−instance Show (Char -> b) where

6+implementation Show (Char -> b) where

77 show x = "<<char fn>>"

99IntFn : Type -> Type

1010IntFn = \x => Int -> x

1111

12−instance Functor IntFn where -- (\x => Int -> x) where

12+implementation Functor IntFn where -- (\x => Int -> x) where

1313 map f intf = \x => f (intf x)

1414

15−instance Applicative (\x => Int -> x) where

15+implementation Applicative (\x => Int -> x) where

1616 pure v = \x => v

1717 (<*>) f a = \x => f x (a x)

1818

19−instance Monad IntFn where

19+implementation Monad IntFn where

2020 f >>= k = \x => k (f x) x

2121

2222dbl : IntFn Int

test/reg027/reg027a.idr+2−2

@@ -3,8 +3,8 @@ module Main

33IntFn : Type -> Type

44IntFn = \x => Int -> x

6−instance Show (IntFn a) where

6+implementation Show (IntFn a) where

77 show x = "<<char fn>>"

9−instance Show (Int -> b) where

9+implementation Show (Int -> b) where

1010 show x = "<<int fn>>"

test/reg035/reg035a.lidr+1−1

@@ -30,7 +30,7 @@

3030> data Set : Type -> Type where

3131> Setify : (as : List a) -> Set a

3232

33−> instance (Eq a) => Eq (Set a) where

33+> implementation (Eq a) => Eq (Set a) where

3434> (==) (Setify as) (Setify bs) = setEq as bs

3535

3636> postulate reflexive_Set_eqeq : (Eq a) =>

test/reg036/reg036.idr+1−1

@@ -8,5 +8,5 @@ using (m : Nat, ts : Vect m Type)

88 showHV : Shows m ts => HV ts -> String

99 showHV (MkHV v) = show v

1010

11− instance Shows m ts => Show (HV ts) where

11+ implementation Shows m ts => Show (HV ts) where

1212 show = showHV

test/reg037/reg037.idr+2−2

@@ -1,9 +1,9 @@

22--- Parser regression for (=) as a function name (fnName)

4−class Foo (t : a -> b -> Type) where

4+interface Foo (t : a -> b -> Type) where

55 foo : (x : _) -> (y : _) -> t x y -> t x y

7−instance Foo ((=) {A=a} {B=b}) where

7+implementation Foo ((=) {A=a} {B=b}) where

88 foo x y prf = prf

test/reg038/reg038.idr+4−4

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

1−class C t (f : t -> t) (r : t -> t -> Type) where

1+interface C t (f : t -> t) (r : t -> t -> Type) where

22 g : (a : t) -> r (f a) (f a) -> r (f a) (f a)

44data Foo : {t : Type} -> t -> t -> Type where

55 MkFoo : {t : Type} -> {x : t} -> {y : t} -> Foo x y

7−instance C t f (Foo {t = t}) where

7+implementation C t f (Foo {t = t}) where

88 g x = id

1010data Bar : {t1 : Type} -> {t2 : Type} -> t1 -> t2 -> Type where

1111 MkBar : {x : t1} -> Bar x x

1212

13−instance C s f (Bar {t1 = s} {t2 = s}) where

13+implementation C s f (Bar {t1 = s} {t2 = s}) where

1414 g x = id

1515

16−instance C s f ((=) {A = s} {B = s}) where

16+implementation C s f ((=) {A = s} {B = s}) where

1717 g x = id

test/reg045/reg045.idr+1−1

@@ -4,7 +4,7 @@ data ListZ : Type -> Type where

44 (::) : a -> Lazy (ListZ a) -> ListZ a

55 Nil : ListZ a

7−instance Show a => Show (ListZ a) where

7+implementation Show a => Show (ListZ a) where

88 show xs = "[" ++ show' "" xs ++ "]"

99 where

1010 show' acc Nil = acc

test/reg058/implicits.idr+2−2

@@ -3,10 +3,10 @@

33InterpBool : () -> Type

44InterpBool () = {x : Type} -> x -> Nat

6−class IdrisBug (u : ()) where

6+interface IdrisBug (u : ()) where

77 idrisBug : InterpBool u

9−instance IdrisBug () where

9+implementation IdrisBug () where

1010 idrisBug _ = Z

1111

1212f : Nat

test/reg059/reg059.idr+2−2

@@ -1,8 +1,8 @@

1−class Monad m => ContainerMonad (m : Type -> Type) where

1+interface Monad m => ContainerMonad (m : Type -> Type) where

22 Elem : a -> m a -> Type

33 tagElem : (mx : m a) -> m (x : a ** Elem x mx)

5−class Monad m => ContainerMonad2 a (m : Type -> Type) where

5+interface Monad m => ContainerMonad2 a (m : Type -> Type) where

66 Elem2 : a -> m a -> Type

77 tagElem2 : (mx : m a) -> m (x : a ** Elem2 x mx)

test/reg060/reg060.idr+3−3

@@ -1,12 +1,12 @@

2−class MyFunctor (f : Type -> Type) where

2+interface MyFunctor (f : Type -> Type) where

33 mymap : (m : a -> b) -> f a -> f b

55data Foo x y = Bar y

7−instance MyFunctor (Foo m) where

7+implementation MyFunctor (Foo m) where

88 mymap m x = ?wibble

10−instance [foo] Functor m => MyFunctor m where

10+implementation [foo] Functor m => MyFunctor m where

1111 mymap m x = map m x

1212

test/reg065/reg065.idr+5−5

@@ -1,21 +1,21 @@

1−||| Test that dependent type class definitions work.

1+||| Test that dependent type interface definitions work.

22|||

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

4−||| type would lead to "can't resolve type class" errors

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

55module TypeClassDep

77import Data.Vect

10−class Foo a where

10+interface Foo a where

1111 getLen : Nat

1212 item : a -> Vect getLen a

1313

14−instance Foo () where

14+implementation Foo () where

1515 getLen = 3

1616 item () = [(), (), ()]

1717

18−instance Foo String where

18+implementation Foo String where

1919 getLen = 1

2020 item str = [str]

2121

test/sugar001/test007.idr+2−2

@@ -13,10 +13,10 @@ fetch x = MkEval (\e => fetchVal e) where

1313 fetchVal [] = Nothing

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

1515

16−instance Functor Eval where

16+implementation Functor Eval where

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

1818

19−instance Applicative Eval where

19+implementation Applicative Eval where

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

2121

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

test/syntax002/syntax002.idr+1−1

@@ -7,7 +7,7 @@ decl syntax newtype {tname} "=" {conname} [tysyn]

77 = data tname = conname tysyn

99decl syntax EmptyShow {n} =

10− instance Show n where

10+ implementation Show n where

1111 show x = "Nothing"

1212

1313fun add : (Int -> Int -> Int) = \x, y => x + y

test/tutorial002/tutorial002.idr+1−1

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

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

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

8−instance Show (Binary n) where

8+implementation Show (Binary n) where

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

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

1111 show BEnd = ""

test/tutorial003/tutorial003.idr+2−2

@@ -13,10 +13,10 @@ fetch x = MkEval (\e => fetchVal e) where

1313 fetchVal [] = Nothing

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

1515

16−instance Functor Eval where

16+implementation Functor Eval where

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

1818

19−instance Applicative Eval where

19+implementation Applicative Eval where

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

2121

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

test/unique001/unique001c.idr+3−3

@@ -25,14 +25,14 @@ share : UTree -> Tree

2525share ULeaf = Leaf

2626share (UNode x y z) = Node (share x) y (share z)

2727

28−class UFunctor (f : Type -> AnyType) where

28+interface UFunctor (f : Type -> AnyType) where

2929 fmap : (a -> b) -> f a -> f b

3030

31−instance UFunctor List where

31+implementation UFunctor List where

3232 fmap f [] = []

3333 fmap f (x :: xs) = f x :: fmap f xs

3434

35−instance UFunctor UList where

35+implementation UFunctor UList where

3636 fmap f UNil = UNil

3737 fmap f (UCons x xs) = UCons (f x) (fmap f xs)

3838