43127b1 · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Move Fin, Vect and So from prelude to base

They can be imported from the modules Data.Fin, Data.Vect, and Data.So respectively. The general thinking here is that not every program is going to need these, and they are often used especially by newcomers in place of something more appropriate. Also, all of them are useful for teaching, which means it is instructive for tutorials to introduce them and have people implement them themselves.

commit43127b17a765dbab2e7bcb6be2f6f2efc7a42386 authorEdwin Brady <ecb10@st-andrews.ac.uk> dateWed 31 Dec 2014, 20:18 (12 years ago) parent40ee5f3

91 files changed+291−379

compare with master

unifiedsplit

libs/base/Control/Isomorphism.idr+1 libs/base/Data/Bits.idr+2 libs/base/Data/BoundedList.idr+2 libs/base/Data/Buffer.idr+2 libs/base/Data/Fun.idr+2 libs/base/Data/HVect.idr+1 libs/base/Data/Hash.idr+2 libs/base/Data/Matrix.idr+2 libs/base/Data/So.idr+25 libs/base/Data/Vect.idr+1 libs/base/Data/Vect/Quantifiers.idr+2 libs/prelude/Prelude/Vect.idr → libs/base/Data/VectType.idr+60−13 libs/base/Decidable/Order.idr+1 libs/base/base.ipkg+3−2 libs/effects/Effect/Default.idr+2 libs/effects/Effect/Memory.idr+4−2 libs/effects/Effect/Random.idr+2 libs/effects/Effects.idr+1 libs/prelude/Decidable/Equality.idr−47 libs/prelude/Prelude.idr+13−43 libs/prelude/Prelude/Bits.idr+1−2 libs/prelude/Prelude/Bool.idr−15 libs/prelude/Prelude/Either.idr−5 libs/prelude/Prelude/Fin.idr−180 libs/prelude/Prelude/Maybe.idr+4 libs/prelude/Prelude/Stream.idr+10−9 libs/prelude/Prelude/Strings.idr+6−5 libs/prelude/prelude.ipkg+4−4 test/basic001/basic001a.idr+2 test/basic001/reg005.idr+2 test/basic005/test019.lidr+2 test/basic006/expected+1−1 test/basic006/test020.idr+2 test/basic006/test020a.idr+2 test/basic009/Multiple.idr+2−2 test/dsl001/test001.idr+3 test/dsl002/Resimp.idr+3 test/dsl003/DSLPi.idr+3 test/effects002/test025.idr+1 test/error003/ErrorReflection.idr+1 test/error003/expected+1−1 test/error005/error005.idr+2 test/error005/expected+6−6 test/folding001/folding001.idr+2 test/folding002/folding002.idr+2 test/interactive001/input+6−6 test/interactive001/test032.idr+1 test/interactive002/input+10−10 test/interactive002/interactive002.idr+1 test/interactive003/input+4−4 test/interactive003/interactive003.idr+2 test/interactive004/input+2−2 test/interactive004/interactive004.idr+2 test/primitives003/test038.idr+3 test/proof001/test029.idr+2 test/proof002/Reflect.idr+1 test/proof002/expected+1−1 test/quasiquote002/GoalQQuote.idr+1 test/quasiquote003/NoInfer.idr+1 test/quasiquote003/expected+1−1 test/records001/test011.idr+2 test/reg002/reg002.idr → test/reg002/reg012.idr+2 test/reg002/run+3−3 test/reg005/reg032.idr → test/reg005/reg005.idr+2 test/reg005/run+1−1 test/reg009/reg009.lidr+3 test/reg011/reg011.idr+2 test/reg012/reg012.lidr+2 test/reg014/reg014.idr+2 test/reg018/expected+2−2 test/reg018/reg018c.idr+2 test/reg018/reg018d.idr+3 test/reg020/reg020.idr+2 test/reg025/reg025.idr+2 test/reg026/reg026.idr+2 test/reg033/reg033.idr+2 test/reg035/expected+1−1 test/reg035/reg035a.lidr+2 test/reg035/reg035b.idr+1 test/sourceLocation001/SourceLoc.idr+2 test/sourceLocation001/expected+4−4 test/totality001/expected+1−1 test/totality001/test010.idr+2 test/totality002/expected+1−1 test/totality002/test017.idr+2 test/totality002/test017a.idr+2 test/totality006/expected+2−2 test/totality006/totality006.idr+3−1 test/totality006/totality006a.idr+2 test/tutorial006/expected+2−2 test/tutorial006/tutorial006a.idr+2

libs/base/Control/Isomorphism.idr+1

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

11module Control.Isomorphism

33import Syntax.PreorderReasoning

4+import Data.Fin

56%default total

libs/base/Data/Bits.idr+2

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

11module Data.Bits

3+import Data.Fin

35%default total

57divCeil : Nat -> Nat -> Nat

libs/base/Data/BoundedList.idr+2

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

11module Data.BoundedList

3+import Data.Fin

35%access public

46%default total

libs/base/Data/Buffer.idr+2

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

11module Data.Buffer

3+import Data.Fin

35%default total

57-- !!! TODO: Open issues:

libs/base/Data/Fun.idr+2

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

11module Data.Fun

3+import Data.Vect

35%default total

57||| Build an n-ary function type from a Vect of Types and a result type

libs/base/Data/HVect.idr+1

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

11module Data.HVect

3+import Data.Fin

34import Data.Vect

56%access public

libs/base/Data/Hash.idr+2

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

11module Data.Hash

3+import Data.Vect

35%access public

46%default total

libs/base/Data/Matrix.idr+2

@@ -2,6 +2,8 @@ module Data.Matrix

33import Data.Complex

44import Data.ZZ

5+import Data.Fin

6+import Data.Vect

68%default total

libs/base/Data/So.idrnew file+25

@@ -0,0 +1,25 @@

1+module Data.So

3+%default total

5+||| Ensure that some run-time Boolean test has been performed.

6+|||

7+||| This lifts a Boolean predicate to the type level. See the function `choose`

8+||| if you need to perform a Boolean test and convince the type checker of this

9+||| fact.

10+|||

11+||| If you find yourself using `So` for something other than primitive types,

12+||| it may be appropriate to define a type of evidence for the property that you

13+||| care about instead.

14+data So : Bool -> Type where

15+ Oh : So True

16+

17+instance Uninhabited (So False) where

18+ uninhabited Oh impossible

19+

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

21+choose : (b : Bool) -> Either (So b) (So (not b))

22+choose True = Left Oh

23+choose False = Right Oh

24+

25+

libs/base/Data/Vect.idr+1

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

11module Data.Vect

33import Language.Reflection

4+import public Data.VectType

56%access public

67%default total

libs/base/Data/Vect/Quantifiers.idr+2

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

11module Data.Vect.Quantifiers

3+import Data.Vect

35||| A proof that some element of a vector satisfies some property

46|||

57||| @ P the property to be satsified

libs/prelude/Prelude/Vect.idr → libs/base/Data/VectType.idrrenamed+60−13

@@ -1,21 +1,12 @@

1−module Prelude.Vect

1+module Data.VectType

3−import Builtins

4−

5−import Prelude.Basics

6−import Prelude.Bool

7−import Prelude.Fin

8−import Prelude.Foldable

9−import Prelude.Functor

10−import Prelude.Maybe

11−import Prelude.List

12−import Prelude.Classes

13−import Prelude.Nat

14−import Prelude.Uninhabited

3+import Data.Fin

154

165%access public

176%default total

187

8+namespace Vect {

1910infixr 7 ::

2011

2112%elim data Vect : Nat -> Type -> Type where

@@ -531,6 +522,29 @@ transpose : Vect m (Vect n a) -> Vect n (Vect m a)

531522transpose [] = replicate _ []

532523transpose (x :: xs) = zipWith (::) x (transpose xs)

533524

525+--------------------------------------------------------------------------------

526+-- Applicative/Monad/Traversable

527+--------------------------------------------------------------------------------

528+

529+instance Applicative (Vect k) where

530+ pure = replicate _

531+

532+ fs <$> vs = zipWith apply fs vs

533+

534+instance Monad (Vect n) where

535+ m >>= f = diag (map f m)

536+

537+instance Traversable (Vect n) where

538+ traverse f [] = pure Vect.Nil

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

540+

541+--------------------------------------------------------------------------------

542+-- Show

543+--------------------------------------------------------------------------------

544+

545+instance Show a => Show (Vect n a) where

546+ show = show . toList

547+

534548--------------------------------------------------------------------------------

535549-- Properties

536550--------------------------------------------------------------------------------

@@ -548,4 +562,37 @@ vectAppendAssociative [] y z = Refl

548562vectAppendAssociative (x :: xs) ys zs =

549563 vectConsCong _ _ _ (vectAppendAssociative xs ys zs)

550564

565+}

566+

567+--------------------------------------------------------------------------------

568+-- DecEq

569+--------------------------------------------------------------------------------

570+

571+total

572+vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y

573+vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

574+

575+total

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

577+vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

578+

579+instance DecEq a => DecEq (Vect n a) where

580+ decEq [] [] = Yes Refl

581+ decEq (x :: xs) (y :: ys) with (decEq x y)

582+ decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)

583+ decEq (x :: xs) (x :: xs) | Yes Refl | Yes Refl = Yes Refl

584+ decEq (x :: xs) (x :: ys) | Yes Refl | No neq = No (neq . vectInjective2)

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

586+

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

588+instance DecEq a => DecEq (Vect n a) where

589+ decEq [] [] = Yes Refl

590+ decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)

591+ decEq (x :: xs) (x :: xs) | (Yes Refl, Yes Refl) = Yes Refl

592+ decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))

593+ decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))

594+-}

595+

596+-- For the primitives, we have to cheat because we don't have access to their

597+-- internal implementations.

551598

libs/base/Decidable/Order.idr+1

@@ -2,6 +2,7 @@ module Decidable.Order

33import Decidable.Decidable

44import Decidable.Equality

5+import Data.Fin

56import Data.Fun

67import Data.Rel

libs/base/base.ipkg+3−2

@@ -21,10 +21,12 @@ modules = System,

2121 Data.Bits, Data.Mod2,

2222 Data.ZZ, Data.Sign,

2323 Data.SortedMap, Data.SortedSet, Data.BoundedList,

24− Data.Vect, Data.HVect, Data.Vect.Quantifiers,

24+ Data.Fin, Data.Vect, Data.VectType,

25+ Data.HVect, Data.Vect.Quantifiers,

2526 Data.Floats, Data.Complex, Data.Heap, Data.Fun,

2627 Data.Rel, Data.Buffer, Data.Erased,

2728 Data.List, Data.Hash, Data.Matrix,

29+ Data.So,

2830

2931 Control.Isomorphism, Control.Isomorphism.Primitives,

3032 Control.Monad.Identity,

@@ -33,4 +35,3 @@ modules = System,

3335 Control.Category, Control.Arrow,

3436 Control.Catchable, Control.IOExcept

3537

36−

libs/effects/Effect/Default.idr+2

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

11module Default

3+import Data.Vect

35class Default a where

46 default : a

libs/effects/Effect/Memory.idr+4−2

@@ -2,6 +2,8 @@ module Effect.Memory

33import Effects

44import Control.IOExcept

5+import Data.Vect

6+import public Data.So

68%access public

@@ -64,11 +66,11 @@ do_memmove dest src dest_offset src_offset size

6466

6567private

6668do_peek : Ptr -> Nat -> (size : Nat) -> IO (Vect size Bits8)

67−do_peek _ _ Z = return (Prelude.Vect.Nil)

69+do_peek _ _ Z = return (Vect.Nil)

6870do_peek ptr offset (S n)

6971 = do b <- mkForeign (FFun "idris_peek" [FPtr, FInt] FByte) ptr (fromInteger $ cast offset)

7072 bs <- do_peek ptr (S offset) n

71− Prelude.Monad.return (Prelude.Vect.(::) b bs)

73+ Monad.return (Vect.(::) b bs)

7274

7375private

7476do_poke : Ptr -> Nat -> Vect size Bits8 -> IO ()

libs/effects/Effect/Random.idr+2

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

11module Effect.Random

33import Effects

4+import Data.Vect

5+import Data.Fin

57data Random : Effect where

68 getRandom : { Integer } Random Integer

libs/effects/Effects.idr+1

@@ -2,6 +2,7 @@ module Effects

33import Language.Reflection

44import public Effect.Default

5+import Data.Vect

67--- Effectful computations are described as algebraic data types that

78--- explain how an effect is interpreted in some underlying context.

libs/prelude/Decidable/Equality.idr−47

@@ -6,9 +6,7 @@ import Prelude.Bool

66import Prelude.Classes

77import Prelude.Either

88import Prelude.List

9−import Prelude.Vect

109import Prelude.Nat

11−import Prelude.Fin

1210import Prelude.Maybe

1311

1412--------------------------------------------------------------------------------

@@ -95,21 +93,6 @@ instance (DecEq a, DecEq b) => DecEq (Either a b) where

9593 decEq (Left x') (Right y') = No leftNotRight

9694 decEq (Right x') (Left y') = No $ negEqSym leftNotRight

9795

98−--------------------------------------------------------------------------------

99−-- Fin

100−--------------------------------------------------------------------------------

101−

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

103−FZNotFS Refl impossible

104−

105−instance DecEq (Fin n) where

106− decEq FZ FZ = Yes Refl

107− decEq FZ (FS f) = No FZNotFS

108− decEq (FS f) FZ = No $ negEqSym FZNotFS

109− decEq (FS f) (FS f') with (decEq f f')

110− | Yes p = Yes $ cong p

111− | No p = No $ \h => p $ FSinjective {f = f} {f' = f'} h

112−

11396--------------------------------------------------------------------------------

11497-- Tuple

11598--------------------------------------------------------------------------------

@@ -165,36 +148,6 @@ instance DecEq a => DecEq (List a) where

165148 decEq (x :: xs) (y :: ys) | (No p) | (No p') = No (\eq => lemma_x_neq_xs_neq p p' eq)

166149

167150

168−--------------------------------------------------------------------------------

169−-- Vect

170−--------------------------------------------------------------------------------

171−

172−total

173−vectInjective1 : {xs, ys : Vect n a} -> {x, y : a} -> x :: xs = y :: ys -> x = y

174−vectInjective1 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

175−

176−total

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

178−vectInjective2 {x=x} {y=x} {xs=xs} {ys=xs} Refl = Refl

179−

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

181− decEq [] [] = Yes Refl

182− decEq (x :: xs) (y :: ys) with (decEq x y)

183− decEq (x :: xs) (x :: ys) | Yes Refl with (decEq xs ys)

184− decEq (x :: xs) (x :: xs) | Yes Refl | Yes Refl = Yes Refl

185− decEq (x :: xs) (x :: ys) | Yes Refl | No neq = No (neq . vectInjective2)

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

187−

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

189−

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

191− decEq [] [] = Yes Refl

192− decEq (x :: xs) (y :: ys) with (decEq x y, decEq xs ys)

193− decEq (x :: xs) (x :: xs) | (Yes Refl, Yes Refl) = Yes Refl

194− decEq (x :: xs) (y :: ys) | (_, No nEqTl) = No (\p => nEqTl (vectInjective2 p))

195− decEq (x :: xs) (y :: ys) | (No nEqHd, _) = No (\p => nEqHd (vectInjective1 p))

196−-}

197−

198151-- For the primitives, we have to cheat because we don't have access to their

199152-- internal implementations.

200153

libs/prelude/Prelude.idr+13−43

@@ -9,7 +9,6 @@ import public Prelude.Bool

99import public Prelude.Classes

1010import public Prelude.Cast

1111import public Prelude.Nat

12−import public Prelude.Fin

1312import public Prelude.List

1413import public Prelude.Maybe

1514import public Prelude.Monad

@@ -17,14 +16,13 @@ import public Prelude.Applicative

1716import public Prelude.Foldable

1817import public Prelude.Functor

1918import public Prelude.Either

20−import public Prelude.Vect

2119import public Prelude.Strings

2220import public Prelude.Chars

2321import public Prelude.Traversable

2422import public Prelude.Bits

25−import public Prelude.Stream

2623import public Prelude.Uninhabited

2724import public Prelude.Pairs

25+import public Prelude.Stream

2826

2927import public Decidable.Equality

3028import public Language.Reflection

@@ -47,11 +45,6 @@ instance Show Integer where

4745instance Show Float where

4846 show = prim__floatToStr

4947

50−asciiTab : Vect 32 String

51−asciiTab = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",

52− "BS", "HT", "LF", "VT", "FF", "CR", "SO", "SI",

53− "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",

54− "CAN", "EM", "SUB", "ESC", "FS", "GS", "RS", "US"]

5548

5649firstCharIs : (Char -> Bool) -> String -> Bool

5750firstCharIs p s with (strM s)

@@ -72,11 +65,21 @@ showLitChar '\v' = ("\\v" ++)

7265showLitChar '\SO' = protectEsc (== 'H') "\\SO"

7366showLitChar '\DEL' = ("\\DEL" ++)

7467showLitChar '\\' = ("\\\\" ++)

75−showLitChar c = case (integerToFin (cast (cast {to=Int} c)) 32) of

76− Just k => strCons '\\' . ((index k asciiTab) ++)

68+showLitChar c = case getAt (cast (cast {to=Int} c)) asciiTab of

69+ Just k => strCons '\\' . (k ++)

7770 Nothing => if (c > '\DEL')

7871 then strCons '\\' . protectEsc isDigit (show (cast {to=Int} c))

7972 else strCons c

73+ where asciiTab : List String

74+ asciiTab = ["NUL", "SOH", "STX", "ETX", "EOT", "ENQ", "ACK", "BEL",

75+ "BS", "HT", "LF", "VT", "FF", "CR", "SO", "SI",

76+ "DLE", "DC1", "DC2", "DC3", "DC4", "NAK", "SYN", "ETB",

77+ "CAN", "EM", "SUB", "ESC", "FS", "GS", "RS", "US"]

78+

79+ getAt : Nat -> List String -> Maybe String

80+ getAt Z (x :: xs) = Just x

81+ getAt (S k) (x :: xs) = getAt k xs

82+ getAt _ [] = Nothing

8083

8184showLitString : List Char -> String -> String

8285showLitString [] = id

@@ -221,9 +224,6 @@ instance Show a => Show (List a) where

221224 show' acc [x] = acc ++ show x

222225 show' acc (x :: xs) = show' (acc ++ show x ++ ", ") xs

223226

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

225− show = show . toList

226−

227227instance Show a => Show (Maybe a) where

228228 show Nothing = "Nothing"

229229 show (Just x) = "Just " ++ show x

@@ -275,15 +275,6 @@ instance Applicative List where

275275

276276 fs <$> vs = concatMap (\f => map f vs) fs

277277

278−instance Applicative (Vect k) where

279− pure = replicate _

280−

281− fs <$> vs = zipWith apply fs vs

282−

283−instance Applicative Stream where

284− pure = repeat

285− (<$>) = zipWith apply

286−

287278---- Alternative instances

288279

289280instance Alternative Maybe where

@@ -316,12 +307,6 @@ instance Monad (Either e) where

316307instance Monad List where

317308 m >>= f = concatMap f m

318309

319−instance Monad (Vect n) where

320− m >>= f = diag (map f m)

321−

322−instance Monad Stream where

323− s >>= f = diag (map f s)

324−

325310---- Traversable instances

326311

327312instance Traversable Maybe where

@@ -332,10 +317,6 @@ instance Traversable List where

332317 traverse f [] = pure List.Nil

333318 traverse f (x::xs) = [| List.(::) (f x) (traverse f xs) |]

334319

335−instance Traversable (Vect n) where

336− traverse f [] = pure Vect.Nil

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

338−

339320---- some mathematical operations

340321---- XXX this should probably go some place else,

341322pow : (Num a) => a -> Nat -> a

@@ -420,17 +401,6 @@ instance Enum Int where

420401 go [] = []

421402 go (x :: xs) = n + (cast x * inc) :: go xs

422403

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

424− pred FZ = FZ

425− pred (FS n) = weaken n

426− succ n = case strengthen (FS n) of

427− Left _ => last

428− Right k => k

429− toNat n = cast n

430− fromNat {n=n} m = case natToFin m (S n) of

431− Just k => k

432− Nothing => last

433−

434404syntax "[" [start] ".." [end] "]"

435405 = enumFromTo start end

436406syntax "[" [start] "," [next] ".." [end] "]"

libs/prelude/Prelude/Bits.idr+1−2

@@ -8,13 +8,12 @@ import Prelude.Cast

88import Prelude.Classes

99import Prelude.Foldable

1010import Prelude.Nat

11+import Prelude.List

1112import Prelude.Strings

12−import Prelude.Vect

1313

1414%access public

1515%default total

1616

17−

1817b8ToString : Bits8 -> String

1918b8ToString c = pack (with List [c1, c2])

2019 where getDigit : Bits8 -> Char

libs/prelude/Prelude/Bool.idr−15

@@ -15,21 +15,6 @@ boolElim : (b : Bool) -> (t : Lazy a) -> (e : Lazy a) -> a

1515boolElim True t e = t

1616boolElim False t e = e

1717

18−||| Ensure that some run-time Boolean test has been performed.

19−|||

20−||| This lifts a Boolean predicate to the type level. See the function `choose`

21−||| if you need to perform a Boolean test and convince the type checker of this

22−||| fact.

23−|||

24−||| If you find yourself using `So` for something other than primitive types,

25−||| it may be appropriate to define a type of evidence for the property that you

26−||| care about instead.

27−data So : Bool -> Type where

28− Oh : So True

29−

30−instance Uninhabited (So False) where

31− uninhabited Oh impossible

32−

3318-- Syntactic sugar for boolean elimination.

3419syntax if [test] then [t] else [e] = boolElim test (Delay t) (Delay e)

3520

libs/prelude/Prelude/Either.idr−5

@@ -33,11 +33,6 @@ isRight (Right r) = True

3333-- Misc.

3434--------------------------------------------------------------------------------

3535

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

37−choose : (b : Bool) -> Either (So b) (So (not b))

38−choose True = Left Oh

39−choose False = Right Oh

40−

4136||| Simply-typed eliminator for Either

4237||| @ f the action to take on Left

4338||| @ g the action to take on Right

libs/prelude/Prelude/Fin.idrdeleted−180

@@ -1,180 +0,0 @@

1−module Prelude.Fin

2−

3−import Builtins

4−

5−import Prelude.Basics

6−import Prelude.Bool

7−import Prelude.Cast

8−import Prelude.Classes

9−import Prelude.List

10−import Prelude.Maybe

11−import Prelude.Nat

12−import Prelude.Either

13−import Prelude.Uninhabited

14−

15−import Language.Reflection

16−import Language.Reflection.Errors

17−

18−%default total

19−

20−||| Numbers strictly less than some bound. The name comes from "finite sets".

21−|||

22−||| It's probably not a good idea to use `Fin` for arithmetic, and they will be

23−||| exceedingly inefficient at run time.

24−||| @ n the upper bound

25−data Fin : (n : Nat) -> Type where

26− FZ : Fin (S k)

27− FS : Fin k -> Fin (S k)

28−

29−instance Uninhabited (Fin Z) where

30− uninhabited FZ impossible

31− uninhabited (FS f) impossible

32−

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

34−FSInjective left _ Refl = Refl

35−

36−instance Eq (Fin n) where

37− (==) FZ FZ = True

38− (==) (FS k) (FS k') = k == k'

39− (==) _ _ = False

40−

41−||| There are no elements of `Fin Z`

42−FinZAbsurd : Fin Z -> Void

43−FinZAbsurd FZ impossible

44−

45−FinZElim : Fin Z -> a

46−FinZElim x = void (FinZAbsurd x)

47−

48−||| Convert a Fin to a Nat

49−finToNat : Fin n -> Nat

50−finToNat FZ = Z

51−finToNat (FS k) = S (finToNat k)

52−

53−||| `finToNat` is injective

54−finToNatInjective : (fm : Fin k) -> (fn : Fin k) -> (finToNat fm) = (finToNat fn) -> fm = fn

55−finToNatInjective FZ FZ Refl = Refl

56−finToNatInjective (FS m) FZ Refl impossible

57−finToNatInjective FZ (FS n) Refl impossible

58−finToNatInjective (FS m) (FS n) prf =

59− cong (finToNatInjective m n (succInjective (finToNat m) (finToNat n) prf))

60−

61−instance Cast (Fin n) Nat where

62− cast x = finToNat x

63−

64−||| Convert a Fin to an Integer

65−finToInteger : Fin n -> Integer

66−finToInteger FZ = 0

67−finToInteger (FS k) = 1 + finToInteger k

68−

69−instance Cast (Fin n) Integer where

70− cast x = finToInteger x

71−

72−||| Weaken the bound on a Fin by 1

73−weaken : Fin n -> Fin (S n)

74−weaken FZ = FZ

75−weaken (FS k) = FS (weaken k)

76−

77−||| Weaken the bound on a Fin by some amount

78−weakenN : (n : Nat) -> Fin m -> Fin (m + n)

79−weakenN n FZ = FZ

80−weakenN n (FS f) = FS (weakenN n f)

81−

82−||| Attempt to tighten the bound on a Fin.

83−||| Return `Left` if the bound could not be tightened, or `Right` if it could.

84−strengthen : Fin (S n) -> Either (Fin (S n)) (Fin n)

85−strengthen {n = S k} FZ = Right FZ

86−strengthen {n = S k} (FS i) with (strengthen i)

87− strengthen (FS k) | Left x = Left (FS x)

88− strengthen (FS k) | Right x = Right (FS x)

89−strengthen f = Left f

90−

91−||| Add some natural number to a Fin, extending the bound accordingly

92−||| @ n the previous bound

93−||| @ m the number to increase the Fin by

94−shift : (m : Nat) -> Fin n -> Fin (m + n)

95−shift Z f = f

96−shift {n=n} (S m) f = FS {k = (m + n)} (shift m f)

97−

98−||| The largest element of some Fin type

99−last : Fin (S n)

100−last {n=Z} = FZ

101−last {n=S _} = FS last

102−

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

104−FSinjective Refl = Refl

105−

106−instance Ord (Fin n) where

107− compare FZ FZ = EQ

108− compare FZ (FS _) = LT

109− compare (FS _) FZ = GT

110− compare (FS x) (FS y) = compare x y

111−

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

113− minBound = FZ

114−

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

116− maxBound = last

117−

118−

119−||| Add two Fins, extending the bound

120−(+) : Fin n -> Fin m -> Fin (n + m)

121−(+) {n=S n} {m=m} FZ f' = rewrite plusCommutative n m in weaken (weakenN n f')

122−(+) (FS f) f' = FS (f + f')

123−

124−||| Substract two Fins, keeping the bound of the minuend

125−(-) : Fin n -> Fin m -> Fin n

126−FZ - _ = FZ

127−f - FZ = f

128−(FS f) - (FS f') = weaken $ f - f'

129−

130−||| Multiply two Fins, extending the bound

131−(*) : Fin n -> Fin m -> Fin (n * m)

132−(*) {n=Z} f f' = FinZElim f

133−(*) {m=Z} f f' = FinZElim f'

134−(*) {n=S n} {m=S m} FZ f' = FZ

135−(*) {n=S n} {m=S m} (FS f) f' = f' + (f * f')

136−

137−-- Construct a Fin from an integer literal which must fit in the given Fin

138−

139−natToFin : Nat -> (n : Nat) -> Maybe (Fin n)

140−natToFin Z (S j) = Just FZ

141−natToFin (S k) (S j) with (natToFin k j)

142− | Just k' = Just (FS k')

143− | Nothing = Nothing

144−natToFin _ _ = Nothing

145−

146−integerToFin : Integer -> (n : Nat) -> Maybe (Fin n)

147−integerToFin x Z = Nothing -- make sure 'n' is concrete, to save reduction!

148−integerToFin x n = if x >= 0 then natToFin (cast x) n else Nothing

149−

150−||| Proof that some `Maybe` is actually `Just`

151−data IsJust : Maybe a -> Type where

152− ItIsJust : IsJust (Just x)

153−

154−||| Allow overloading of Integer literals for Fin.

155−||| @ x the Integer that the user typed

156−||| @ prf an automatically-constructed proof that `x` is in bounds

157−fromInteger : (x : Integer) ->

158− {default ItIsJust

159− prf : (IsJust (integerToFin x n))} ->

160− Fin n

161−fromInteger {n} x {prf} with (integerToFin x n)

162− fromInteger {n} x {prf = ItIsJust} | Just y = y

163−

164−%language ErrorReflection

165−

166−total

167−finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)

168−finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)

169− = Just [ TextPart "When using", TermPart n

170− , TextPart "as a literal for a"

171− , TermPart `(Fin ~m)

172− , SubReport [ TextPart "Could not show that"

173− , TermPart n

174− , TextPart "is less than"

175− , TermPart m

176− ]

177− ]

178−finFromIntegerErrors _ = Nothing

179−

180−%error_handlers Prelude.Fin.fromInteger prf finFromIntegerErrors

libs/prelude/Prelude/Maybe.idr+4

@@ -27,6 +27,10 @@ isJust : Maybe a -> Bool

2727isJust Nothing = False

2828isJust (Just j) = True

2929

30+||| Proof that some `Maybe` is actually `Just`

31+data IsJust : Maybe a -> Type where

32+ ItIsJust : IsJust (Just x)

33+

3034--------------------------------------------------------------------------------

3135-- Misc

3236--------------------------------------------------------------------------------

libs/prelude/Prelude/Stream.idr+10−9

@@ -4,8 +4,10 @@ import Builtins

55import Prelude.Basics

66import Prelude.Functor

7+import Prelude.Applicative

8+import Prelude.Monad

79import Prelude.Nat

8−import Prelude.Vect

10+import Prelude.List

911

1012%access public

1113%default total

@@ -31,7 +33,7 @@ tail (x::xs) = xs

3133||| Take precisely n elements from the stream

3234||| @ n how many elements to take

3335||| @ xs the stream

34−take : (n : Nat) -> (xs : Stream a) -> Vect n a

36+take : (n : Nat) -> (xs : Stream a) -> List a

3537take Z _ = []

3638take (S n) (x :: xs) = x :: (take n xs)

3739

@@ -107,11 +109,10 @@ partial -- and the call to foldr isn't guarded anyway!

107109scanr : (f : a -> Inf b -> b) -> (xs : Stream a) -> Stream b

108110scanr f (x :: xs) = f x (foldr f xs) :: scanr f xs

109111

110−||| Produce a Stream repeating a sequence

111−||| @ xs the sequence to repeat

112−cycle : (xs : Vect (S n) a) -> Stream a

113−cycle xs = cycle_ xs xs

114− where cycle_ : Vect (S n) a -> Vect m a -> Stream a

115− cycle_ (x :: xs) [] = x :: cycle_ (x :: xs) xs

116− cycle_ xs (x :: ys) = x :: cycle_ xs ys

112+instance Applicative Stream where

113+ pure = repeat

114+ (<$>) = zipWith apply

115+

116+instance Monad Stream where

117+ s >>= f = diag (map f s)

117118

libs/prelude/Prelude/Strings.idr+6−5

@@ -13,6 +13,7 @@ import Prelude.Foldable

1313import Prelude.Functor

1414import Prelude.List

1515import Prelude.Nat

16+import Decidable.Equality

1617

1718||| Appends two strings together.

1819|||

@@ -81,20 +82,20 @@ data StrM : String -> Type where

8182 StrCons : (x : Char) -> (xs : String) -> StrM (strCons x xs)

8283

8384||| Version of 'strHead' that statically verifies that the string is not empty.

84−strHead' : (x : String) -> So (not (x == "")) -> Char

85+strHead' : (x : String) -> (not (x == "") = True) -> Char

8586strHead' x p = assert_total $ prim__strHead x

8687

8788||| Version of 'strTail' that statically verifies that the string is not empty.

88−strTail' : (x : String) -> So (not (x == "")) -> String

89+strTail' : (x : String) -> (not (x == "") = True) -> String

8990strTail' x p = assert_total $ prim__strTail x

9091

9192-- we need the 'believe_me' because the operations are primitives

9293strM : (x : String) -> StrM x

93−strM x with (choose (not (x == "")))

94− strM x | (Left p) = really_believe_me $

94+strM x with (decEq (not (x == "")) True)

95+ strM x | (Yes p) = really_believe_me $

9596 StrCons (assert_total (strHead' x p))

9697 (assert_total (strTail' x p))

97− strM x | (Right p) = really_believe_me StrNil

98+ strM x | (No p) = really_believe_me StrNil

9899

99100-- annoyingly, we need these assert_totals because StrCons doesn't have

100101-- a recursive argument, therefore the termination checker doesn't believe

libs/prelude/prelude.ipkg+4−4

@@ -3,14 +3,14 @@ package prelude

33opts = "--nobuiltins --total"

44modules = Builtins, Prelude, IO,

6− Language.Reflection, Language.Reflection.Errors,

7−

86 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

9− Prelude.Classes, Prelude.Nat, Prelude.Fin, Prelude.List,

7+ Prelude.Classes, Prelude.Nat, Prelude.List,

108 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

11− Prelude.Vect, Prelude.Strings, Prelude.Chars, Prelude.Functor,

9+ Prelude.Strings, Prelude.Chars, Prelude.Functor,

1210 Prelude.Foldable, Prelude.Traversable, Prelude.Bits, Prelude.Stream,

1311 Prelude.Uninhabited, Prelude.Pairs,

1412

13+ Language.Reflection, Language.Reflection.Errors,

14+

1515 Decidable.Equality

1616

test/basic001/basic001a.idr+2

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

11module Main

3+import Data.Vect

35data RLE : Vect n Char -> Type where

46 REnd : RLE []

57 RChar : {xs : Vect k Char} ->

test/basic001/reg005.idr+2

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

11module Main

3+import Data.Vect

35%flag C "-g3"

46%flag C "-ggdb"

57%flag C "-O0"

test/basic005/test019.lidr+2

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

11> module Main

3+> import Data.So

35> ifTrue : So True -> Nat

46> ifTrue Oh = S Z

test/basic006/expected+1−1

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

1−test020a.idr:14:18:When elaborating right hand side of foo:

1+test020a.idr:16:18:When elaborating right hand side of foo:

22When elaborating an application of function Prelude.List.reverse:

33 Can't unify

44 Vect n a

test/basic006/test020.idr+2

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

11module Main

3+import Data.Vect

35implicit

46natInt : Nat -> Integer

57natInt x = cast x

test/basic006/test020a.idr+2

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

11module Main

3+import Data.Vect

35implicit

46forget : Vect n a -> List a

57forget [] = []

test/basic009/Multiple.idr+2−2

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

11module Multiple

3−import Prelude.Vect as X

4−import Prelude.List as X

3+import Data.Vect as X

4+import Data.List as X

test/dsl001/test001.idr+3

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

11module Main

3+import Data.Vect

4+import Data.Fin

36data Ty = TyInt | TyBool| TyFun Ty Ty

58interpTy : Ty -> Type

test/dsl002/Resimp.idr+3

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

11module Resimp

3+import Data.Vect

4+import public Data.Fin

36-- IO operations which read a resource

47data Reader : Type -> Type where

58 MkReader : IO a -> Reader a

test/dsl003/DSLPi.idr+3

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

11module DSLPi

3+import Data.Fin

4+import Data.Vect

36data Ty = BOOL | INT | UNIT | ARR Ty Ty

58dsl simple_type

test/effects002/test025.idr+1

@@ -3,6 +3,7 @@ module Main

33import Effects

44import Effect.Memory

55import Control.IOExcept

6+import Data.Vect

78MemoryIO : Type -> Type -> Type -> Type

89MemoryIO td ts r = { [ Dst ::: RAW_MEMORY td

test/error003/ErrorReflection.idr+1

@@ -3,6 +3,7 @@ module Main

33import Language.Reflection

44import Language.Reflection.Errors

55import Language.Reflection.Utils

6+import Data.Vect

78%language ErrorReflection

test/error003/expected+1−1

@@ -1,2 +1,2 @@

1−ErrorReflection.idr:67:5:When elaborating right hand side of bad:

1+ErrorReflection.idr:68:5:When elaborating right hand side of bad:

22DSL type error: (t(503) => t'(504)) doesn't match ()

test/error005/error005.idr+2

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

11module error005

3+import Data.Fin

35-- Test the Prelude's error rewrites for Fin

57one : Fin 2

test/error005/expected+6−6

@@ -1,12 +1,12 @@

1−error005.idr:11:1:When elaborating right hand side of two:

2−When elaborating argument prf to function Prelude.Fin.fromInteger:

1+error005.idr:13:1:When elaborating right hand side of two:

2+When elaborating argument prf to function Data.Fin.fromInteger:

33 When using 2 as a literal for a Fin 2

44 Could not show that 2 is less than 2

5−error005.idr:14:1:When elaborating right hand side of hahaha:

6−When elaborating argument prf to function Prelude.Fin.fromInteger:

5+error005.idr:16:1:When elaborating right hand side of hahaha:

6+When elaborating argument prf to function Data.Fin.fromInteger:

77 When using 0 as a literal for a Fin n

88 Could not show that 0 is less than n

9−error005.idr:19:1:When elaborating right hand side of notOk:

10−When elaborating argument prf to function Prelude.Fin.fromInteger:

9+error005.idr:21:1:When elaborating right hand side of notOk:

10+When elaborating argument prf to function Data.Fin.fromInteger:

1111 When using 2 as a literal for a Fin (S (S n))

1212 Could not show that 2 is less than S (S n)

test/folding001/folding001.idr+2

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

11module Main

3+import Data.Vect

35-- foldr (::) [] converts to lists

46foldToList : (Foldable t) => t a -> List a

57foldToList = foldr (::) []

test/folding002/folding002.idr+2

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

1+import Data.Vect

13-- perform a very large foldr to test tail recursion

24addAll : (Foldable t, Num a) => t a -> a

35addAll = foldr (+) 0

test/interactive001/input+6−6

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

1−:cs 11 xs

2−:cs 17 ys

3−:ps 21 maprhs

4−:mw 25 isElem2

5−:cs 30 p

6−:cs 35 xs'

1+:cs 12 xs

2+:cs 18 ys

3+:ps 22 maprhs

4+:mw 26 isElem2

5+:cs 31 p

6+:cs 36 xs'

test/interactive001/test032.idr+1

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

11module elem

33import Decidable.Equality

4+import Data.Vect

56using (xs : List a)

67 data Elem : a -> List a -> Type where

test/interactive002/input+10−10

@@ -1,11 +1,11 @@

1−:ps 2 foo_arg1

2−:ps 2 foo_arg2

3−:ps 2 foo_arg3

4−:ps 2 foo_ret

5−:ps 6 bar_out

6−:ps 9 plus_in1

7−:ps 9 plus_out

8−:ps 13 what

9−:ps 16 ifoo_arg1

10−:ps 16 ifoo_out

1+:ps 3 foo_arg1

2+:ps 3 foo_arg2

3+:ps 3 foo_arg3

4+:ps 3 foo_ret

5+:ps 7 bar_out

6+:ps 10 plus_in1

7+:ps 10 plus_out

8+:ps 14 what

9+:ps 17 ifoo_arg1

10+:ps 17 ifoo_out

1111

test/interactive002/interactive002.idr+1

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

1+import Data.Vect

23foo : ?foo_arg1 -> ?foo_arg2 -> ?foo_arg3 -> ?foo_ret

34foo (S a) b c = plus (a + b + c) 42

test/interactive003/input+4−4

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

1−:ps 2 app_rhs_1

2−:ps 3 app_rhs_2

3−:ps 6 vzipWith_rhs_3

4−:ps 7 vzipWith_rhs_1

1+:ps 4 app_rhs_1

2+:ps 5 app_rhs_2

3+:ps 8 vzipWith_rhs_3

4+:ps 9 vzipWith_rhs_1

test/interactive003/interactive003.idr+2

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

1+import Data.Vect

13app : Vect n a -> Vect m a -> Vect (n + m) a

24app [] ys = ?app_rhs_1

35app (x :: xs) ys = ?app_rhs_2

test/interactive004/input+2−2

@@ -1,2 +1,2 @@

1−:ref 2 foo_rhs1 plus

2−:ref 6 append_rhs1 append

1+:ref 4 foo_rhs1 plus

2+:ref 8 append_rhs1 append

test/interactive004/interactive004.idr+2

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

1+import Data.Vect

13foo : Nat -> Nat -> Nat

24foo k j = ?foo_rhs1

test/primitives003/test038.idr+3

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

11module Main

3+import Data.Vect

4+import Data.Fin

36test : DecEq a => a -> a -> Bool

47test i1 i2 with (decEq i1 i2)

58 test i1 i1 | Yes Refl = True

test/proof001/test029.idr+2

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

11module simple

3+import Data.Vect

35plus_comm : (n : Nat) -> (m : Nat) -> (n + m = m + n)

57-- Base case

test/proof002/Reflect.idr+1

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

11module Reflect

33import Decidable.Equality

45%default total

67using (xs : List a, ys : List a, G : List (List a))

test/proof002/expected+1−1

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

1−Reflect.idr:207:38:When elaborating right hand side of testReflect1:

1+Reflect.idr:208:38:When elaborating right hand side of testReflect1:

22When elaborating an application of function Reflect.getJust:

33 Can't unify

44 IsJust (Just x1)

test/quasiquote002/GoalQQuote.idr+1

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

11module GoalQQuote

3+import Data.Vect

34import Language.Reflection

45import Language.Reflection.Utils

test/quasiquote003/NoInfer.idr+1

@@ -2,6 +2,7 @@ module NoInfer

33import Language.Reflection

44import Language.Reflection.Utils

5+import Data.Fin

67zzz2 : TT

78zzz2 = `(FZ : Fin 3)

test/quasiquote003/expected+1−1

@@ -1,2 +1,2 @@

1−NoInfer.idr:10:5:When elaborating right hand side of zzz:

1+NoInfer.idr:11:5:When elaborating right hand side of zzz:

22No such variable k

test/records001/test011.idr+2

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

11module Main

3+import Data.Vect

35record Foo : Nat -> Type where

46 MkFoo : (name : String) ->

57 (things : Vect n a) ->

test/reg002/reg002.idr → test/reg002/reg012.idrrenamed+2

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

11module Main

3+import Data.Vect

35%default total

57data CoNat

test/reg002/run+3−3

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

11#!/usr/bin/env bash

2−idris reg002.idr -o reg002

3−./reg002

4−rm -f reg002 *.ibc

2+idris reg012.idr -o reg012

3+./reg012

4+rm -f reg012 *.ibc

test/reg005/reg032.idr → test/reg005/reg005.idrrenamed+2

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

11module reg032

3+import Data.Fin

35zfin : Fin 1

46zfin = 0

test/reg005/run+1−1

@@ -1,3 +1,3 @@

11#!/usr/bin/env bash

2−idris $@ reg032.idr --check

2+idris $@ reg005.idr --check

33rm -f *.ibc

test/reg009/reg009.lidr+3

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

1+> import Data.So

2+> import Data.Vect

14> isAnyBy : (alpha -> Bool) -> (n : Nat ** Vect n alpha) -> Bool

25> isAnyBy _ (_ ** Nil) = False

36> isAnyBy p (_ ** (a :: as)) = p a || isAnyBy p (_ ** as)

test/reg011/reg011.idr+2

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

1+import Data.Vect

13vfoldl : (P : Nat -> Type) ->

24 ((x : Nat) -> P x -> a -> P (S x)) -> P Z

35 -> Vect m a -> P m

test/reg012/reg012.lidr+2

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

1+> import Data.So

13> total soElim : (C : (b : Bool) -> So b -> Type) ->

24> C True Oh ->

35> (b : Bool) -> (s : So b) -> (C b s)

test/reg014/reg014.idr+2

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

11module reg014

3+import Data.Vect

35Matrix : Type -> Nat -> Nat -> Type

46Matrix a n m = Vect n (Vect m a)

test/reg018/expected+2−2

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

11reg018a.idr:16:1:conat.minusCoNat is possibly not total due to recursive path conat.minusCoNat

22reg018a.idr:21:1:conat.loopForever is possibly not total due to: conat.minusCoNat

33reg018b.idr:8:1:A.showB is possibly not total due to recursive path A.showB

4−reg018c.idr:19:1:CodataTest.inf is possibly not total due to: with block in CodataTest.inf

5−reg018d.idr:5:1:Main.pull is not total as there are missing cases

4+reg018c.idr:21:1:CodataTest.inf is possibly not total due to: with block in CodataTest.inf

5+reg018d.idr:8:1:Main.pull is not total as there are missing cases

test/reg018/reg018c.idr+2

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

11module CodataTest

2+import Data.Vect

24%default total

46codata InfStream a = (::) a (InfStream a)

test/reg018/reg018d.idr+3

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

11module Main

3+import Data.Vect

4+import Data.Fin

36total

47pull : Fin (S n) -> Vect (S n) a -> (a, Vect n a)

58pull {n=Z} _ (x :: xs) = (x, xs)

test/reg020/reg020.idr+2

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

11module Main

3+import Data.Vect

35emptyString : String

46emptyString = ""

test/reg025/reg025.idr+2

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

11module Main

3+import Data.Fin

4+import Data.Vect

35import Data.Vect.Quantifiers

46import Decidable.Equality

test/reg026/reg026.idr+2

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

11module Test

3+import Data.So

35X : Nat -> Type

46X t = (c : Nat ** So (c < 5))

test/reg033/reg033.idr+2

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

1+import Data.Vect

13mapFilter : (alpha -> beta) ->

24 (alpha -> Bool) ->

35 Vect n alpha ->

test/reg035/expected+1−1

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

1−reg035b.idr:7:6:Can't convert

1+reg035b.idr:8:6:Can't convert

22 [94mAdditive[0m -> [94mNat[0m

33with

44 [94mFin[0m [91m0[0m

test/reg035/reg035a.lidr+2

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

11> module Set

3+> import Data.So

35> %default total

57> postulate soAndIntro : (p : alpha -> Bool) ->

test/reg035/reg035b.idr+1

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

11import Data.Vect

2+import Data.Fin

34total

45finZEmpty : Fin Z -> a

test/sourceLocation001/SourceLoc.idr+2

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

11module SourceLoc

3+import Data.Vect

4+import Data.Fin

35import Language.Reflection

46import Language.Reflection.Utils

test/sourceLocation001/expected+4−4

@@ -1,11 +1,11 @@

11Testing using definition

2−FileLoc "SourceLoc.idr" (14, 11) (14, 11)

2+FileLoc "SourceLoc.idr" (16, 11) (16, 11)

33Testing using inline tactics

4−FileLoc "SourceLoc.idr" (18, 17) (18, 17)

4+FileLoc "SourceLoc.idr" (20, 17) (20, 17)

55Testing using metavariable with later definition

6−FileLoc "SourceLoc.idr" (94, 16) (94, 16)

6+FileLoc "SourceLoc.idr" (96, 16) (96, 16)

77-----------------------

88Success!

9−Error at FileLoc "SourceLoc.idr" (68, 23) (68, 23)

9+Error at FileLoc "SourceLoc.idr" (70, 23) (70, 23)

1010Success!

1111Success!

test/totality001/expected+1−1

@@ -1,3 +1,3 @@

1−test010.idr:13:1:Main.foo is possibly not total due to: Main.MkBad

1+test010.idr:15:1:Main.foo is possibly not total due to: Main.MkBad

22test010a.idr:9:1:main.bar is possibly not total due to: main.MkBad

33test010b.idr:9:1:main.bar is possibly not total due to: main.MkBad

test/totality001/test010.idr+2

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

1+import Data.Vect

13data MyNat = MyO | MyS MyNat

35%default total

test/totality002/expected+1−1

@@ -1,2 +1,2 @@

1−test017a.idr:5:1:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

1+test017a.idr:7:1:scg.vtrans is possibly not total due to recursive path scg.vtrans --> scg.vtrans

22test017b.idr:4:1:foo.foo is possibly not total due to recursive path foo.foo

test/totality002/test017.idr+2

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

11module scg

3+import Data.Vect

35%default total

57data Ord = Zero | Suc Ord | Sup (Nat -> Ord)

test/totality002/test017a.idr+2

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

11module scg

3+import Data.Vect

35total

46vtrans : Vect n a -> Vect n a -> List a

57vtrans [] _ = []

test/totality006/expected+2−2

@@ -1,2 +1,2 @@

1−totality006.idr:6:1:Main.prf is not total as there are missing cases

2−totality006a.idr:9:6:prf' (S _) (S _) Oh is a valid case

1+totality006.idr:8:1:Main.prf is not total as there are missing cases

2+totality006a.idr:11:6:prf' (S _) (S _) Oh is a valid case

test/totality006/totality006.idr+3−1

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

1+import Data.So

13antitrue : So False -> a

24antitrue Oh impossible

@@ -6,6 +8,6 @@ prf : (a:Nat) -> (b:Nat) -> So (a > b) -> GT a b

68prf Z Z Oh impossible

79prf Z (S k) um = antitrue um

810prf (S k) Z um = LTESucc LTEZero

9−-- prf (S _) (S _) Oh impossible

11+-- prf (S x) (S y) Oh impossible

1012

1113

test/totality006/totality006a.idr+2

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

1+import Data.So

13antitrue : So False -> a

24antitrue Oh impossible

test/tutorial006/expected+2−2

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

1−tutorial006a.idr:3:23:When elaborating right hand side of vapp:

2−When elaborating argument [95mxs[0m to constructor [91mPrelude.Vect.::[0m:

1+tutorial006a.idr:5:23:When elaborating right hand side of vapp:

2+When elaborating argument [95mxs[0m to constructor [91mData.VectType.Vect.::[0m:

33 Can't unify

44 [94mVect[0m ([95mn[0m [92m+[0m [95mn[0m) [95ma[0m

55 with

test/tutorial006/tutorial006a.idr+2

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

1+import Data.Vect

13vapp : Vect n a -> Vect m a -> Vect (n + m) a

24vapp Nil ys = ys

35vapp (x :: xs) ys = x :: vapp xs xs -- BROKEN