ebe30dd · Idris-dev · git.iko.soy

idris.cabal+5−1

compare with master

unifiedsplit

@@ -91,6 +91,8 @@ Extra-source-files:

91 libs/prelude/prelude.ipkg

92 libs/prelude/Prelude/*.idr

93 libs/prelude/Decidable/*.idr

94+ libs/prelude/Language/*.idr

95+ libs/prelude/Language/Reflection/*.idr

94 libs/prelude/Makefile

96 libs/prelude/Makefile

95 libs/prelude/*.idr

97 libs/prelude/*.idr

96

98

@@ -103,7 +105,6 @@ Extra-source-files:

103 libs/base/Data/Vect/*.idr

105 libs/base/Data/Vect/*.idr

104 libs/base/Debug/*.idr

106 libs/base/Debug/*.idr

105 libs/base/Decidable/*.idr

107 libs/base/Decidable/*.idr

106− libs/base/Language/*.idr

107 libs/base/Language/Reflection/*.idr

108 libs/base/Language/Reflection/*.idr

108 libs/base/Makefile

109 libs/base/Makefile

109 libs/base/Network/*.idr

110 libs/base/Network/*.idr

@@ -358,6 +359,9 @@ Extra-source-files:

358 test/error004/run

359 test/error004/run

359 test/error004/*.idr

360 test/error004/*.idr

360 test/error004/expected

361 test/error004/expected

362+ test/error005/run

363+ test/error005/*.idr

364+ test/error005/expected

361

365

362 test/ffi001/run

366 test/ffi001/run

363 test/ffi001/*.idr

367 test/ffi001/*.idr

libs/base/Decidable/Decidable.idr+3−3

@@ -18,6 +18,6 @@ class Decidable (ts : Vect k Type) (p : Rel ts) where

18--decision : Decidable ts p => (ts : Vect k Type) -> (p : Rel ts) -> liftRel ts p Dec

19--decision ts p = decide {ts} {p}

20

21−using (P : Type, p : P)

21+using (a : Type, x : a)

22− data Given : Dec P -> Type where

22+ data Given : Dec a -> Type where

23− always : Given (Yes p)

23+ Always : Given (Yes x)

libs/base/Language/Reflection/Utils.idr+7−3

@@ -3,17 +3,17 @@ module Language.Reflection.Utils

3import Language.Reflection

4import Language.Reflection.Errors

5

6−%default total

7−

8--------------------------------------------------------

6--------------------------------------------------------

9-- Tactic construction conveniences

7-- Tactic construction conveniences

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

8--------------------------------------------------------

11

9

10+total

12seq : List Tactic -> Tactic

11seq : List Tactic -> Tactic

13seq [] = GoalType "This is an impossible case" Trivial

12seq [] = GoalType "This is an impossible case" Trivial

14seq [t] = t

13seq [t] = t

15seq (t::ts) = t `Seq` seq ts

14seq (t::ts) = t `Seq` seq ts

16

15

16+total

17try : List Tactic -> Tactic

18try [] = GoalType "This is an impossible case" Trivial

19try [t] = t

@@ -23,6 +23,7 @@ try (t::ts) = t `Try` seq ts

23--------------------------------------------------------

24-- For use in tactic scripts

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

26+total

26mkPair : a -> b -> (a, b)

27mkPair : a -> b -> (a, b)

27mkPair a b = (a, b)

28mkPair a b = (a, b)

28

29

@@ -30,22 +31,25 @@ mkPair a b = (a, b)

30--------------------------------------------------------

31--------------------------------------------------------

31-- Tools for constructing proof terms directly

32-- Tools for constructing proof terms directly

32--------------------------------------------------------

33--------------------------------------------------------

33−

34+total

34getUName : TTName -> Maybe String

35getUName : TTName -> Maybe String

35getUName (UN n) = Just n

36getUName (UN n) = Just n

36getUName (NS n ns) = getUName n

37getUName (NS n ns) = getUName n

37getUName _ = Nothing

38getUName _ = Nothing

38

39

40+total

39unApply : TT -> (TT, List TT)

41unApply : TT -> (TT, List TT)

40unApply t = unA t []

42unApply t = unA t []

41 where unA : TT -> List TT -> (TT, List TT)

43 where unA : TT -> List TT -> (TT, List TT)

42 unA (App fn arg) args = unA fn (arg::args)

44 unA (App fn arg) args = unA fn (arg::args)

43 unA tm args = (tm, args)

45 unA tm args = (tm, args)

44

46

47+total

45mkApp : TT -> List TT -> TT

48mkApp : TT -> List TT -> TT

46mkApp tm [] = tm

49mkApp tm [] = tm

47mkApp tm (a::as) = mkApp (App tm a) as

50mkApp tm (a::as) = mkApp (App tm a) as

48

51

52+total

49binderTy : (Eq t) => Binder t -> t

53binderTy : (Eq t) => Binder t -> t

50binderTy (Lam t) = t

54binderTy (Lam t) = t

51binderTy (Pi t _) = t

55binderTy (Pi t _) = t

libs/base/Network/Socket.idr+2−2

@@ -56,13 +56,13 @@ instance Show SocketType where

56 show NotASocket = "Not a socket"

57 show Stream = "Stream"

58 show Datagram = "Datagram"

59− show Raw = "Raw"

59+ show RawSocket = "Raw"

60

61instance ToCode SocketType where

62 toCode NotASocket = 0

63 toCode Stream = 1

64 toCode Datagram = 2

65− toCode Raw = 3

65+ toCode RawSocket = 3

66

67

68data RecvStructPtr = RSPtr Ptr

libs/base/base.ipkg+1−1

@@ -13,7 +13,7 @@ modules = System,

13

14 Providers,

15

16− Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,

16+ Language.Reflection.Utils,

17

18 Syntax.PreorderReasoning,

19

libs/base/Language/Reflection.idr → libs/prelude/Language/Reflection.idrrenamed+9

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

1module Language.Reflection

2

3+import Builtins

4+import Prelude.Applicative

5+import Prelude.Basics

6+import Prelude.Foldable

7+import Prelude.Functor

8+import Prelude.List

9+import Prelude.Nat

10+import Prelude.Traversable

11+

3%access public

12%access public

4

13

5data TTName =

14data TTName =

libs/base/Language/Reflection/Errors.idr → libs/prelude/Language/Reflection/Errors.idrrenamed+5

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

1module Language.Reflection.Errors

2

3+import Builtins

4+

3import Language.Reflection

5import Language.Reflection

4

6

7+import Prelude.Bool

8+import Prelude.List

9+import Prelude.Maybe

5

10

6data Err = Msg String

11data Err = Msg String

7 | InternalMsg String

12 | InternalMsg String

libs/prelude/Prelude.idr+2

@@ -27,6 +27,8 @@ import public Prelude.Uninhabited

27import public Prelude.Pairs

28

29import public Decidable.Equality

30+import public Language.Reflection

31+import public Language.Reflection.Errors

30

32

31%access public

33%access public

32%default total

34%default total

libs/prelude/Prelude/Fin.idr+21

@@ -6,11 +6,15 @@ import Prelude.Basics

6import Prelude.Bool

7import Prelude.Cast

8import Prelude.Classes

9+import Prelude.List

9import Prelude.Maybe

10import Prelude.Maybe

10import Prelude.Nat

11import Prelude.Nat

11import Prelude.Either

12import Prelude.Either

12import Prelude.Uninhabited

13import Prelude.Uninhabited

13

14

15+import Language.Reflection

16+import Language.Reflection.Errors

17+

14%default total

18%default total

15

19

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

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

@@ -157,3 +161,20 @@ fromInteger : (x : Integer) ->

157fromInteger {n} x {prf} with (integerToFin x n)

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

158 fromInteger {n} x {prf = ItIsJust} | Just y = y

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

159

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.ipkg+2

@@ -3,6 +3,8 @@ package prelude

3opts = "--nobuiltins --total"

4modules = Builtins, Prelude, IO,

5

6+ Language.Reflection, Language.Reflection.Errors,

7+

6 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

8 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

7 Prelude.Classes, Prelude.Nat, Prelude.Fin, Prelude.List,

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

8 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

10 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

test/error005/error005.idrnew file+18

@@ -0,0 +1,18 @@

1+module error005

2+

3+-- Test the Prelude's error rewrites for Fin

4+

5+one : Fin 2

6+one = 1

7+

8+two : Fin 2

9+two = 2

10+

11+hahaha : (n : Nat) -> Fin n

12+hahaha n = 0

13+

14+ok : (n : Nat) -> Fin (plus 2 n)

15+ok n = 1

16+

17+notOk : (n : Nat) -> Fin (plus 2 n)

18+notOk n = 2

test/error005/expectednew file+12

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

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

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

3+ When using 2 as a literal for a Fin 2

4+ 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:

7+ When using 0 as a literal for a Fin n

8+ 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:

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

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

test/error005/runnew file+3

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

1+#!/usr/bin/env bash

2+idris $@ --check --nocolour error005.idr

3+rm -f *.ibc

test/reg025/reg025.idr+5−5

@@ -24,13 +24,13 @@ FullBoard (MkBoard b) = All (All Filled) b

24indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (FS i) (x::xs)

25indexStep = Refl

26

27−find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)

27+find : {p : a -> Type} -> ((x : a) -> Dec (p x)) -> (xs : Vect n a)

28− -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))

28+ -> Either (All (\x => Not (p x)) xs) (y : a ** (p y, (i : Fin n ** y = index i xs)))

29find _ Nil = Left Nil

30−find {P} d (x::xs) with (d x)

30+find {p} d (x::xs) with (d x)

31 | Yes prf = Right (x ** (prf, (FZ ** Refl)))

32 | No prf =

33− case find {P} d xs of

33+ case find {p} d xs of

34 Right (y ** (prf', (i ** prf''))) =>

35 Right (y ** (prf', (FS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))

36 Left prf' => Left (prf::prf')

@@ -41,7 +41,7 @@ empty (Just _) = No nothingNotJust

41

42findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))

43findEmptyInRow xs =

44− case find {P=Empty} empty xs of

44+ case find {p=Empty} empty xs of

45 Right (_ ** (pempty, (i ** pidx))) => Right (i ** trans pempty pidx)

46 Left p => Left p

47