Skip to content

Commit

Permalink
Merge pull request #1 from Z-snails/error-location
Browse files Browse the repository at this point in the history
Error location
  • Loading branch information
hydrolarus authored Mar 17, 2022
2 parents 64eafbf + 7f1e5a0 commit 3dcdb54
Show file tree
Hide file tree
Showing 2 changed files with 67 additions and 9 deletions.
12 changes: 12 additions & 0 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -48,6 +48,18 @@ main = do
else putStrLn "Not all tests passed"
```

Source location can be added to assertions to improve error messages.

```idris
import Language.Reflection
%language ElabReflection
withSource = test "location" $ do
assert
{loc = here `(())}
False
```

## License

All code is licensed under the [MPL-2.0](LICENSES/MPL-2.0.txt).
Expand Down
64 changes: 55 additions & 9 deletions src/Tester.idr
Original file line number Diff line number Diff line change
Expand Up @@ -7,6 +7,10 @@ module Tester
import public Control.Monad.Either
import Data.String
import Control.ANSI
import Language.Reflection
import Language.Reflection.TTImp

%language ElabReflection

||| A function which can report test failures.
public export
Expand Down Expand Up @@ -37,31 +41,70 @@ public export
test : (description : String) -> (run : TestFunc ()) -> Test
test = MkTest

public export
record Location where
constructor Loc
inner : FC

export
emptyLoc : Location
emptyLoc = Loc EmptyFC

||| Get a `Location` token
||| This can be passed to assertion to attach source location
|||
||| ```idris example
||| let loc = here `(())
||| in assertEq {loc}
export %macro
here : TTImp -> Elab Location
here ttimp = pure $ Loc $ getFC ttimp

getFile : OriginDesc -> String
getFile (PhysicalIdrSrc (MkMI path)) = showSep "/" (reverse path) ++ ".idr"
getFile (PhysicalPkgSrc fname) = fname
getFile (Virtual _) = "virtual"

formatFC : FC -> String
formatFC (MkFC origin (startLn, startCol) (endLn, endCol)) = " at \{getFile origin}:\{show startLn}:\{show startCol}--\{show endLn}:\{show endCol}"
formatFC (MkVirtualFC origin (startLn, startCol) (endLn, endCol)) = " at \{getFile origin}:\{show startLn}:\{show startCol}--\{show endLn}:\{show endCol}"
formatFC EmptyFC = ""

export
formatLoc : Location -> String
formatLoc loc = formatFC loc.inner

||| Assert that two values are equal.
|||
||| Stops the test and reports a test failure if the values are not equal.
public export
assertEq : (Eq a, Show a) => (left, right : a) -> TestFunc ()
assertEq :
(Eq a, Show a) =>
{default emptyLoc loc : Location} ->
(left, right : a) ->
TestFunc ()
assertEq left right =
if left /= right then
unless (left == right) $
let msg = unlines [
red "assertEq" ++ " failed:",
red "assertEq" ++ " failed\{formatLoc loc}",
" left `" ++ red (show left) ++ "`",
" right `" ++ red (show right) ++ "`"
]
in throwE msg
else
pure ()

||| Assert that two values are not equal.
|||
||| Stops the test and reports a test failure if the values are equal.
public export
assertNotEq : (Eq a, Show a) => (left, right : a) -> TestFunc ()
assertNotEq :
(Eq a, Show a) =>
{default emptyLoc loc : Location} ->
(left, right : a) ->
TestFunc ()
assertNotEq left right =
if left == right then
let msg = unlines [
red "assertNotEq" ++ " failed:",
red "assertNotEq" ++ " failed\{formatLoc loc}:",
" left `" ++ red (show left) ++ "`",
" right `" ++ red (show right) ++ "`"
]
Expand All @@ -73,10 +116,13 @@ assertNotEq left right =
|||
||| Stops the test and reports a test failure if the condition does not hold.
public export
assert : (cond : Bool) -> TestFunc ()
assert :
{default emptyLoc loc : Location} ->
(cond : Bool) ->
TestFunc ()
assert cond =
if not cond then
let msg = red "assert" ++ "failed"
let msg = red "assert" ++ "failed\{formatLoc loc}"
in throwE msg
else
pure ()
Expand Down

0 comments on commit 3dcdb54

Please sign in to comment.