ebe30dd · Idris-dev · git.iko.soy

git.iko.soy/Idris-dev

Merge pull request #1803 from david-christiansen/fin-error-reflection

Error reflection for Fin

commitebe30dd4116d7c202f1fd987834f1408adc7217b authorDavid Christiansen <david@davidchristiansen.dk> dateMon 22 Dec 2014, 14:11 (12 years ago) parent91cd4d5 d78e3c1

14 files changed+95−15

compare with master

unifiedsplit

idris.cabal+5−1 libs/base/Decidable/Decidable.idr+3−3 libs/base/Language/Reflection/Utils.idr+7−3 libs/base/Network/Socket.idr+2−2 libs/base/base.ipkg+1−1 libs/base/Language/Reflection.idr → libs/prelude/Language/Reflection.idr+9 libs/base/Language/Reflection/Errors.idr → libs/prelude/Language/Reflection/Errors.idr+5 libs/prelude/Prelude.idr+2 libs/prelude/Prelude/Fin.idr+21 libs/prelude/prelude.ipkg+2 test/error005/error005.idr+18 test/error005/expected+12 test/error005/run+3 test/reg025/reg025.idr+5−5

idris.cabal+5−1

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

9191 libs/prelude/prelude.ipkg

9292 libs/prelude/Prelude/*.idr

9393 libs/prelude/Decidable/*.idr

94+ libs/prelude/Language/*.idr

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

9496 libs/prelude/Makefile

9597 libs/prelude/*.idr

9698

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

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

104106 libs/base/Debug/*.idr

105107 libs/base/Decidable/*.idr

106− libs/base/Language/*.idr

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

108109 libs/base/Makefile

109110 libs/base/Network/*.idr

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

358359 test/error004/run

359360 test/error004/*.idr

360361 test/error004/expected

362+ test/error005/run

363+ test/error005/*.idr

364+ test/error005/expected

361365

362366 test/ffi001/run

363367 test/ffi001/*.idr

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

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

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

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

2020

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

22− data Given : Dec P -> Type where

23− always : Given (Yes p)

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

22+ data Given : Dec a -> Type where

23+ Always : Given (Yes x)

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

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

33import Language.Reflection

44import Language.Reflection.Errors

6−%default total

7−

86--------------------------------------------------------

97-- Tactic construction conveniences

108--------------------------------------------------------

119

10+total

1211seq : List Tactic -> Tactic

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

1413seq [t] = t

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

1615

16+total

1717try : List Tactic -> Tactic

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

1919try [t] = t

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

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

2424-- For use in tactic scripts

2525--------------------------------------------------------

26+total

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

2728mkPair a b = (a, b)

2829

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

3031--------------------------------------------------------

3132-- Tools for constructing proof terms directly

3233--------------------------------------------------------

33−

34+total

3435getUName : TTName -> Maybe String

3536getUName (UN n) = Just n

3637getUName (NS n ns) = getUName n

3738getUName _ = Nothing

3839

40+total

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

4042unApply t = unA t []

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

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

4345 unA tm args = (tm, args)

4446

47+total

4548mkApp : TT -> List TT -> TT

4649mkApp tm [] = tm

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

4851

52+total

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

5054binderTy (Lam t) = t

5155binderTy (Pi t _) = t

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

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

5656 show NotASocket = "Not a socket"

5757 show Stream = "Stream"

5858 show Datagram = "Datagram"

59− show Raw = "Raw"

59+ show RawSocket = "Raw"

6060

6161instance ToCode SocketType where

6262 toCode NotASocket = 0

6363 toCode Stream = 1

6464 toCode Datagram = 2

65− toCode Raw = 3

65+ toCode RawSocket = 3

6666

6767

6868data RecvStructPtr = RSPtr Ptr

libs/base/base.ipkg+1−1

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

1313

1414 Providers,

1515

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

16+ Language.Reflection.Utils,

1717

1818 Syntax.PreorderReasoning,

1919

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

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

11module Language.Reflection

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+

312%access public

413

514data TTName =

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

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

11module Language.Reflection.Errors

3+import Builtins

35import Language.Reflection

7+import Prelude.Bool

8+import Prelude.List

9+import Prelude.Maybe

510

611data Err = Msg String

712 | InternalMsg String

libs/prelude/Prelude.idr+2

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

2727import public Prelude.Pairs

2828

2929import public Decidable.Equality

30+import public Language.Reflection

31+import public Language.Reflection.Errors

3032

3133%access public

3234%default total

libs/prelude/Prelude/Fin.idr+21

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

66import Prelude.Bool

77import Prelude.Cast

88import Prelude.Classes

9+import Prelude.List

910import Prelude.Maybe

1011import Prelude.Nat

1112import Prelude.Either

1213import Prelude.Uninhabited

1314

15+import Language.Reflection

16+import Language.Reflection.Errors

17+

1418%default total

1519

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

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

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

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

159163

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

33opts = "--nobuiltins --total"

44modules = Builtins, Prelude, IO,

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

68 Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,

79 Prelude.Classes, Prelude.Nat, Prelude.Fin, Prelude.List,

810 Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

test/error005/error005.idrnew file+18

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

1+module error005

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

5+one : Fin 2

6+one = 1

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

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

2525indexStep = Refl

2626

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

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

2929find _ Nil = Left Nil

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

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

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

3232 | No prf =

33− case find {P} d xs of

33+ case find {p} d xs of

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

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

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

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

4141

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

4343findEmptyInRow xs =

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

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

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

4646 Left p => Left p

4747