Error reflection for Fin

Add reflection-based error message improvements for Fin literals. Now,
instead of a collection of internal implementation details, a friendly
and descriptive message is returned.

See test/error005 for a demo.

libs/base/Decidable/Decidable.idr

@@ -18,6 +18,6 @@ class Decidable (ts : Vect k Type) (p : Rel ts) where
 --decision : Decidable ts p => (ts : Vect k Type) -> (p : Rel ts) -> liftRel ts p Dec
 --decision ts p = decide {ts} {p}
 
-using (P : Type, p : P)
-  data Given : Dec P -> Type where
-    always : Given (Yes p)
+using (a : Type, x : a)
+  data Given : Dec a -> Type where
+    Always : Given (Yes x)

libs/base/Language/Reflection/Utils.idr

@@ -3,17 +3,17 @@ module Language.Reflection.Utils
 import Language.Reflection
 import Language.Reflection.Errors
 
-%default total
-
 --------------------------------------------------------
 -- Tactic construction conveniences
 --------------------------------------------------------
 
+total
 seq : List Tactic -> Tactic
 seq []      = GoalType "This is an impossible case" Trivial
 seq [t]     = t
 seq (t::ts) = t `Seq` seq ts
 
+total
 try : List Tactic -> Tactic
 try []      = GoalType "This is an impossible case" Trivial
 try [t]     = t
@@ -23,6 +23,7 @@ try (t::ts) = t `Try` seq ts
 --------------------------------------------------------
 -- For use in tactic scripts
 --------------------------------------------------------
+total
 mkPair : a -> b -> (a, b)
 mkPair a b = (a, b)
 
@@ -30,22 +31,25 @@ mkPair a b = (a, b)
 --------------------------------------------------------
 -- Tools for constructing proof terms directly
 --------------------------------------------------------
-
+total
 getUName : TTName -> Maybe String
 getUName (UN n)    = Just n
 getUName (NS n ns) = getUName n
 getUName _         = Nothing
 
+total
 unApply : TT -> (TT, List TT)
 unApply t = unA t []
   where unA : TT -> List TT -> (TT, List TT)
         unA (App fn arg) args = unA fn (arg::args)
         unA tm           args = (tm, args)
 
+total
 mkApp : TT -> List TT -> TT
 mkApp tm []      = tm
 mkApp tm (a::as) = mkApp (App tm a) as
 
+total
 binderTy : (Eq t) => Binder t -> t
 binderTy (Lam t)       = t
 binderTy (Pi t _)      = t

libs/base/Network/Socket.idr

@@ -56,13 +56,13 @@ instance Show SocketType where
   show NotASocket = "Not a socket"
   show Stream     = "Stream"
   show Datagram   = "Datagram"
-  show Raw        = "Raw"
+  show RawSocket  = "Raw"
 
 instance ToCode SocketType where
   toCode NotASocket = 0
   toCode Stream     = 1
   toCode Datagram   = 2
-  toCode Raw        = 3
+  toCode RawSocket  = 3
 
 
 data RecvStructPtr = RSPtr Ptr

libs/base/base.ipkg

@@ -13,7 +13,7 @@ modules = System,
 
           Providers,
 
-          Language.Reflection, Language.Reflection.Utils, Language.Reflection.Errors,
+          Language.Reflection.Utils,
 
           Syntax.PreorderReasoning,
 

libs/prelude/Language/Reflection.idr

@@ -1,5 +1,14 @@
 module Language.Reflection
 
+import Builtins
+import Prelude.Applicative
+import Prelude.Basics
+import Prelude.Foldable
+import Prelude.Functor
+import Prelude.List
+import Prelude.Nat
+import Prelude.Traversable
+
 %access public
 
 data TTName =

libs/prelude/Language/Reflection/Errors.idr

@@ -1,7 +1,12 @@
 module Language.Reflection.Errors
 
+import Builtins
+
 import Language.Reflection
 
+import Prelude.Bool
+import Prelude.List
+import Prelude.Maybe
 
 data Err = Msg String
          | InternalMsg String

libs/prelude/Prelude.idr

@@ -27,6 +27,8 @@ import public Prelude.Uninhabited
 import public Prelude.Pairs
 
 import public Decidable.Equality
+import public Language.Reflection
+import public Language.Reflection.Errors
 
 %access public
 %default total

libs/prelude/Prelude/Fin.idr

@@ -6,11 +6,15 @@ import Prelude.Basics
 import Prelude.Bool
 import Prelude.Cast
 import Prelude.Classes
+import Prelude.List
 import Prelude.Maybe
 import Prelude.Nat
 import Prelude.Either
 import Prelude.Uninhabited
 
+import Language.Reflection
+import Language.Reflection.Errors
+
 %default total
 
 ||| Numbers strictly less than some bound.  The name comes from "finite sets".
@@ -157,3 +161,20 @@ fromInteger : (x : Integer) ->
 fromInteger {n} x {prf} with (integerToFin x n)
   fromInteger {n} x {prf = ItIsJust} | Just y = y
 
+%language ErrorReflection
+
+total
+finFromIntegerErrors : Err -> Maybe (List ErrorReportPart)
+finFromIntegerErrors (CantUnify x tm `(IsJust (integerToFin ~n ~m)) err xs y)
+  = Just [ TextPart "When using", TermPart n
+         , TextPart "as a literal for a"
+         , TermPart `(Fin ~m)
+         , SubReport [ TextPart "Could not show that"
+                     , TermPart n
+                     , TextPart "is less than"
+                     , TermPart m
+                     ]
+         ]
+finFromIntegerErrors _ = Nothing
+
+%error_handlers Prelude.Fin.fromInteger prf finFromIntegerErrors

libs/prelude/prelude.ipkg

@@ -3,6 +3,8 @@ package prelude
 opts = "--nobuiltins --total"
 modules = Builtins, Prelude, IO,
 
+          Language.Reflection, Language.Reflection.Errors,
+
           Prelude.Algebra, Prelude.Basics, Prelude.Bool, Prelude.Cast,
           Prelude.Classes, Prelude.Nat, Prelude.Fin, Prelude.List,
           Prelude.Maybe, Prelude.Monad, Prelude.Applicative, Prelude.Either,

test/error005/error005.idr

@@ -0,0 +1,18 @@
+module error005
+
+-- Test the Prelude's error rewrites for Fin
+
+one : Fin 2
+one = 1
+
+two : Fin 2
+two = 2
+
+hahaha : (n : Nat) -> Fin n
+hahaha n = 0
+
+ok : (n : Nat) -> Fin (plus 2 n)
+ok n = 1
+
+notOk : (n : Nat) -> Fin (plus 2 n)
+notOk n = 2

test/error005/expected

@@ -0,0 +1,12 @@
+error005.idr:11:1:When elaborating right hand side of two:
+When elaborating argument prf to function Prelude.Fin.fromInteger:
+        When using 2 as a literal for a Fin 2 
+                Could not show that 2 is less than 2
+error005.idr:14:1:When elaborating right hand side of hahaha:
+When elaborating argument prf to function Prelude.Fin.fromInteger:
+        When using 0 as a literal for a Fin n 
+                Could not show that 0 is less than n
+error005.idr:19:1:When elaborating right hand side of notOk:
+When elaborating argument prf to function Prelude.Fin.fromInteger:
+        When using 2 as a literal for a Fin (S (S n)) 
+                Could not show that 2 is less than S (S n)

test/error005/run

@@ -0,0 +1,3 @@
+#!/usr/bin/env bash
+idris $@ --check --nocolour error005.idr
+rm -f *.ibc

test/reg025/reg025.idr

@@ -24,13 +24,13 @@ FullBoard (MkBoard b) = All (All Filled) b
 indexStep : {i : Fin n} -> {xs : Vect n a} -> {x : a} -> index i xs = index (FS i) (x::xs)
 indexStep = Refl
 
-find : {P : a -> Type} -> ((x : a) -> Dec (P x)) -> (xs : Vect n a)
-       -> Either (All (\x => Not (P x)) xs) (y : a ** (P y, (i : Fin n ** y = index i xs)))
+find : {p : a -> Type} -> ((x : a) -> Dec (p x)) -> (xs : Vect n a)
+       -> Either (All (\x => Not (p x)) xs) (y : a ** (p y, (i : Fin n ** y = index i xs)))
 find _ Nil = Left Nil
-find {P} d (x::xs) with (d x)
+find {p} d (x::xs) with (d x)
   | Yes prf = Right (x ** (prf, (FZ ** Refl)))
   | No prf =
-    case find {P} d xs of
+    case find {p} d xs of
       Right (y ** (prf', (i ** prf''))) =>
         Right (y ** (prf', (FS i ** replace {P=(\x => y = x)} (indexStep {x=x}) prf'')))
       Left prf' => Left (prf::prf')
@@ -41,7 +41,7 @@ empty (Just _) = No nothingNotJust
 
 findEmptyInRow : (xs : Vect n (Cell n)) -> Either (All Filled xs) (i : Fin n ** Empty (index i xs))
 findEmptyInRow xs =
-  case find {P=Empty} empty xs of
+  case find {p=Empty} empty xs of
     Right (_ ** (pempty, (i ** pidx))) => Right (i ** trans pempty pidx)
     Left p => Left p