From 06557200bc538304c83f7538f2cf1f8ddbdb2278 Mon Sep 17 00:00:00 2001
From: rhiannon morris <rhi@rhiannon.website>
Date: Thu, 26 May 2022 14:23:50 +0200
Subject: [PATCH] first

---
 .gitignore      |   1 +
 TAP.idr         | 292 ++++++++++++++++++++++++
 TAP/Options.idr | 113 ++++++++++
 acsl.txt        |  34 +++
 default.nix     |   3 +
 flake.lock      | 575 ++++++++++++++++++++++++++++++++++++++++++++++++
 flake.nix       |  26 +++
 tap.ipkg        |  11 +
 8 files changed, 1055 insertions(+)
 create mode 100644 .gitignore
 create mode 100644 TAP.idr
 create mode 100644 TAP/Options.idr
 create mode 100644 acsl.txt
 create mode 100644 default.nix
 create mode 100644 flake.lock
 create mode 100644 flake.nix
 create mode 100644 tap.ipkg

diff --git a/.gitignore b/.gitignore
new file mode 100644
index 0000000..378eac2
--- /dev/null
+++ b/.gitignore
@@ -0,0 +1 @@
+build
diff --git a/TAP.idr b/TAP.idr
new file mode 100644
index 0000000..8e61271
--- /dev/null
+++ b/TAP.idr
@@ -0,0 +1,292 @@
+module TAP
+
+import public TAP.Options
+import public Control.Monad.Either
+import Data.String
+import Data.List
+import Data.List.Elem
+import Data.SnocList
+import Control.Monad.Reader
+import Control.Monad.State
+import Control.ANSI
+import System
+
+%default total
+
+
+public export
+Info : Type
+Info = List (String, String)
+
+private
+data Result = Tried Bool Info | Skip String | Todo String
+
+private
+record TestBase where
+  constructor MakeTest
+  label : String
+  run   : IO Result
+
+
+private
+toLines1 : (String, String) -> List String
+toLines1 (k, v) =
+  let vs = lines v in
+  if length vs == 1
+     then ["\{k}: \{v}"]
+     else "\{k}: |" :: map (indent 2) vs
+
+private
+toLines : Info -> List String
+toLines [] = []
+toLines xs = "---" :: concatMap toLines1 xs <+> ["..."]
+
+
+public export interface ToInfo e where toInfo : e -> Info
+
+export ToInfo () where toInfo () = []
+
+export Show a => ToInfo (List (String, a)) where toInfo = map (map show)
+
+
+export
+data Test
+= One TestBase
+| Group String (List Test)
+| Note String
+
+
+export
+isRealTest : Test -> Bool
+isRealTest (One   _)   = True
+isRealTest (Group _ _) = True
+isRealTest (Note  _)   = False
+
+
+private
+result : ToInfo a => Bool -> a -> IO Result
+result ok = pure . Tried ok . toInfo
+
+private
+lazyToIO : Lazy a -> IO a
+lazyToIO val = primIO $ \w => MkIORes (force val) w
+
+export
+testIO : (ToInfo e, ToInfo a) => String -> EitherT e IO a -> Test
+testIO label act = One $ MakeTest label $ do
+  case !(runEitherT act) of
+       Right val => result True  val
+       Left  err => result False err
+
+export
+test : (ToInfo e, ToInfo a) => String -> Lazy (Either e a) -> Test
+test label val = testIO label $ MkEitherT $ lazyToIO val
+
+export
+todoWith : String -> String -> Test
+todoWith label reason = One $ MakeTest label $ pure $ Todo reason
+
+export
+todo : String -> Test
+todo label = todoWith label ""
+
+private
+makeSkip : String -> String -> Test
+makeSkip label reason = One $ MakeTest label $ pure $ Skip reason
+
+export
+skipWith : Test -> String -> Test
+skipWith (One   t)   reason = makeSkip t.label reason
+skipWith (Group l _) reason = makeSkip l       reason
+skipWith (Note  n)   _      = Note n
+
+export
+skip : Test -> Test
+skip test = skipWith test ""
+
+export
+testThrows : (ToInfo e, Show a) =>
+             String -> (e -> Bool) -> Lazy (Either e a) -> Test
+testThrows label p act = One $ MakeTest label $ do
+  case !(lazyToIO act) of
+       Left  err => if p err then result True () else result False err
+       Right val => result False [("success", val)]
+
+infix 1 :-
+export
+(:-) : String -> List Test -> Test
+(:-) = Group
+
+export
+bailOut : Test
+bailOut = One $ MakeTest "bail out" $ do
+  putStrLn "Bail out!"
+  exitFailure
+
+export
+note : String -> Test
+note = Note
+
+
+
+export
+header : List Test -> String
+header tests =
+  let count = length $ filter isRealTest tests in
+  "1..\{show count}"
+
+
+private
+withPrefix : SnocList String -> TestBase -> Test
+withPrefix pfx = One . {label $= (makePrefix pfx ++)}
+  where makePrefix = concatMap $ \s => "\{s} ⟫ "
+
+mutual
+  export
+  flattenWith : SnocList String -> List Test -> List Test
+  flattenWith pfx tests =
+    concatMap (\t => flatten1With pfx (assert_smaller tests t)) tests
+
+  export
+  flatten1With : SnocList String -> Test -> List Test
+  flatten1With pfx (One   t)    = [withPrefix pfx t]
+  flatten1With pfx (Group x ts) = flattenWith (pfx :< x) ts
+  flatten1With pfx (Note  n)    = [Note n]
+
+export
+flatten : List Test -> List Test
+flatten = flattenWith [<]
+
+export
+flatten1 : Test -> List Test
+flatten1 = flatten1With [<]
+
+
+private
+record RunnerEnv where
+  constructor RE
+  indent : Nat
+  color  : Bool
+
+
+private
+Runner : Type -> Type
+Runner = ReaderT RunnerEnv IO
+
+private
+putIndentLines : List String -> Runner ()
+putIndentLines xs = traverse_ (putStrLn . indent (!ask).indent) xs
+
+private
+isOk : Bool -> String
+isOk b = if b then "ok" else "not ok"
+
+private
+toBool : Result -> Bool
+toBool (Tried ok _) = ok
+toBool _            = True
+
+
+private
+numbered : (a -> Bool) -> List a -> List (Nat, a)
+numbered p = go 1 where
+  go : Nat -> List a -> List (Nat, a)
+  go _ []        = []
+  go i (x :: xs) =
+    if p x then (i, x) :: go (S i) xs
+           else (0, x) :: go i     xs
+
+
+private
+col : Color -> String -> Runner String
+col c str = pure $ if (!ask).color then show $ colored c str else str
+
+private
+putColor : Color -> String -> Runner ()
+putColor c str = putIndentLines [!(col c str)]
+
+private
+okCol : Bool -> Color
+okCol True  = Green
+okCol False = Red
+
+private
+putOk' : Color -> Bool -> Nat -> String -> Runner ()
+putOk' c ok index label =
+  putIndentLines [!(col c "\{isOk ok} \{show index}") ++ " - \{label}"]
+
+private
+putOk : Bool -> Nat -> String -> Runner ()
+putOk ok = putOk' (okCol ok) ok
+
+private
+putVersion : TAPVersion -> Runner ()
+putVersion ver = putColor Cyan "TAP version \{show ver}"
+
+private
+run1' : (Nat, TestBase) -> Runner Bool
+run1' (index, test) = do
+  res <- liftIO test.run
+  case res of
+       Tried ok info => do
+         putOk ok index test.label
+         local {indent $= plus 2} $ putIndentLines $ toLines info
+       Skip reason =>
+         putOk' Yellow True index "\{test.label}  # skip \{reason}"
+       Todo reason =>
+         putOk' Yellow True index "\{test.label}  # todo \{reason}"
+  pure $ toBool res
+
+mutual
+  private
+  run' : (Nat, Test) -> Runner Bool
+  run' (index, One test) = run1' (index, test)
+  run' (index, Group label tests) = do
+    putIndentLines [!(col Magenta "# Subtest: ") ++ label]
+    res <- local {indent $= plus 4} $ runList tests
+    putOk res index label
+    pure res
+  run' (_, Note note) = do
+    putIndentLines [!(col Magenta "# ") ++ note]
+    pure True
+
+  private
+  runList : List Test -> Runner Bool
+  runList tests = do
+    putColor Cyan $ header tests
+    let tests' = numbered isRealTest tests
+    all id <$> traverse (\t => run' (assert_smaller tests t)) tests'
+
+
+mutual
+  export
+  filterMatch : Maybe String -> List Test -> List Test
+  filterMatch Nothing    tests = tests
+  filterMatch (Just pat) tests =
+    mapMaybe (\t => filterMatch1 pat (assert_smaller tests t)) tests
+
+  export
+  filterMatch1 : String -> Test -> Maybe Test
+  filterMatch1 pat test@(One base) =
+    guard (pat `isInfixOf` base.label) $> test
+  filterMatch1 pat all@(Group label tests) =
+    if pat `isInfixOf` label then Just all else
+    case filterMatch (Just pat) tests of
+         []  => Nothing
+         res => Just $ Group label res
+  filterMatch1 pat note@(Note _) = Just note
+
+
+export
+main' : Options -> List Test -> IO ExitCode
+main' opts tests = do
+  let tests = filterMatch opts.pattern $
+              case opts.version of V13 => flatten tests; V14 => tests
+  let act = do putVersion opts.version; runList tests
+  pure $ if !(runReaderT (RE 0 opts.color) act)
+            then ExitSuccess
+            else ExitFailure 70
+
+export
+main : Options -> List Test -> IO ()
+main opts tests = exitWith !(main' opts tests)
diff --git a/TAP/Options.idr b/TAP/Options.idr
new file mode 100644
index 0000000..8212970
--- /dev/null
+++ b/TAP/Options.idr
@@ -0,0 +1,113 @@
+module TAP.Options
+
+import Data.String
+import System
+import System.Console.GetOpt
+
+%default total
+
+
+public export
+data TAPVersion = V13 | V14
+
+export
+readVersion : String -> Maybe TAPVersion
+readVersion "13" = Just V13
+readVersion "14" = Just V14
+readVersion _    = Nothing
+
+export Show TAPVersion where show V13 = "13"; show V14 = "14"
+
+
+public export
+record Options where
+  constructor Opts
+  version : TAPVersion
+  pattern : Maybe String
+  color   : Bool
+
+export
+defaultOpts : Options
+defaultOpts = Opts {
+  version = V13,
+  pattern = Nothing,
+  color   = False
+}
+
+public export
+Mod : Type
+Mod = Options -> IO Options
+
+
+export
+failureWith : List String -> IO a
+failureWith msgs = do
+  traverse_ (\s => putStrLn "# \{s}") msgs
+  putStrLn "\nBail out!"
+  exitFailure
+
+private
+setTapVer : String -> Mod
+setTapVer ver opts =
+  case readVersion ver of
+       Just v  => pure $ {version := v} opts
+       Nothing => failureWith ["unrecognised TAP version '\{ver}'"]
+
+private
+setPat : String -> Mod
+setPat str opts = pure $ {pattern := Just str} opts
+
+mutual
+  export
+  opts : List (OptDescr Mod)
+  opts =
+    [ MkOpt {
+        description = "show this help",
+        shortNames  = ['h', '?'], longNames = ["help"],
+        argDescr    = NoArg $ const $ failureWith usage
+      },
+      MkOpt {
+        description = "TAP version to output (13 or 14, default 13)",
+        shortNames  = ['V'], longNames = ["version"],
+        argDescr    = ReqArg setTapVer "VERSION"
+      },
+      MkOpt {
+        description = "only run tests containing STR in their group or label",
+        shortNames  = ['F'], longNames = ["filter"],
+        argDescr    = ReqArg setPat "STR"
+      },
+      MkOpt {
+        description = "don't colour-code results (default)",
+        shortNames  = ['C'], longNames = ["no-color", "no-colour"],
+        argDescr    = NoArg $ pure . {color := False}
+      },
+      MkOpt {
+        description = "colour-code results (not TAP compliant)",
+        shortNames  = ['c'], longNames = ["color", "colour"],
+        argDescr    = NoArg $ pure . {color := True}
+      }
+    ]
+
+  export
+  usage : List String
+  usage = assert_total $ "quox test suite" :: lines (usageInfo "" opts)
+
+
+export
+makeOpts : List Mod -> IO Options
+makeOpts = foldlM (\x, f => f x) defaultOpts
+
+
+export
+getArgs1 : IO (List String)
+getArgs1 =
+  case !getArgs of
+       _ :: args => pure args
+       []        => failureWith ["expected getArgs to start with exe name"]
+
+export
+getTestOpts : IO Options
+getTestOpts =
+  case getOpt Permute opts !getArgs1 of
+       MkResult opts [] [] [] => makeOpts opts
+       res                    => failureWith $ res.errors ++ usage
diff --git a/acsl.txt b/acsl.txt
new file mode 100644
index 0000000..d82e332
--- /dev/null
+++ b/acsl.txt
@@ -0,0 +1,34 @@
+ANTI-CAPITALIST SOFTWARE LICENSE (v 1.4)
+
+Copyright © 2021 rhiannon morris
+
+This is anti-capitalist software, released for free use by individuals and
+organizations that do not operate by capitalist principles.
+
+Permission is hereby granted, free of charge, to any person or organization
+(the “User”) obtaining a copy of this software and associated documentation
+files (the “Software”), to use, copy, modify, merge, distribute, and/or sell
+copies of the Software, subject to the following conditions:
+
+1. The above copyright notice and this permission notice shall be included in
+   all copies or modified versions of the Software.
+
+2. The User is one of the following:
+   a. An individual person, laboring for themselves
+   b. A non-profit organization
+   c. An educational institution
+   d. An organization that seeks shared profit for all of its members, and
+      allows non-members to set the cost of their labor
+
+3. If the User is an organization with owners, then all owners are workers and
+   all workers are owners with equal equity and/or equal vote.
+
+4. If the User is an organization, then the User is not law enforcement or
+   military, or working for or under either.
+
+THE SOFTWARE IS PROVIDED “AS IS”, WITHOUT EXPRESS OR IMPLIED WARRANTY OF ANY
+KIND, INCLUDING BUT NOT LIMITED TO THE WARRANTIES OF MERCHANTABILITY, FITNESS
+FOR A PARTICULAR PURPOSE AND NONINFRINGEMENT. IN NO EVENT SHALL THE AUTHORS BE
+LIABLE FOR ANY CLAIM, DAMAGES OR OTHER LIABILITY, WHETHER IN AN ACTION OF
+CONTRACT, TORT OR OTHERWISE, ARISING FROM, OUT OF OR IN CONNECTION WITH THE
+SOFTWARE OR THE USE OR OTHER DEALINGS IN THE SOFTWARE.
diff --git a/default.nix b/default.nix
new file mode 100644
index 0000000..00ec5b6
--- /dev/null
+++ b/default.nix
@@ -0,0 +1,3 @@
+(import (fetchTarball "https://github.com/edolstra/flake-compat/archive/master.tar.gz") {
+  src = ./.;
+}).defaultNix
diff --git a/flake.lock b/flake.lock
new file mode 100644
index 0000000..faf8c1b
--- /dev/null
+++ b/flake.lock
@@ -0,0 +1,575 @@
+{
+  "nodes": {
+    "Prettier": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639310097,
+        "narHash": "sha256-+eSLEJDuy2ZRkh1h0Y5IF6RUeHEcWhAHpWhwdwW65f0=",
+        "owner": "Z-snails",
+        "repo": "prettier",
+        "rev": "4a90663b1d586f6d6fce25873aa0f0d7bc633b89",
+        "type": "github"
+      },
+      "original": {
+        "owner": "Z-snails",
+        "repo": "prettier",
+        "type": "github"
+      }
+    },
+    "collie": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1631011321,
+        "narHash": "sha256-goYctB+WBoLgsbjA0DlqGjD8i9wr1K0lv0agqpuwflU=",
+        "owner": "ohad",
+        "repo": "collie",
+        "rev": "ed2eda5e04fbd02a7728e915d396e14cc7ec298e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "ohad",
+        "repo": "collie",
+        "type": "github"
+      }
+    },
+    "comonad": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1638093386,
+        "narHash": "sha256-kxmN6XuszFLK2i76C6LSGHe5XxAURFu9NpzJbi3nodk=",
+        "owner": "stefan-hoeck",
+        "repo": "idris2-comonad",
+        "rev": "06d6b551db20f1f940eb24c1dae051c957de97ad",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stefan-hoeck",
+        "repo": "idris2-comonad",
+        "type": "github"
+      }
+    },
+    "dom": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639041519,
+        "narHash": "sha256-4ZYc0qaUEVARxhWuH3JgejIeT+GEDNxdS6zIGhBCk34=",
+        "owner": "stefan-hoeck",
+        "repo": "idris2-dom",
+        "rev": "01ab52d0ffdb3b47481413a949b8f0c0688c97e4",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stefan-hoeck",
+        "repo": "idris2-dom",
+        "type": "github"
+      }
+    },
+    "dot-parse": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1638264571,
+        "narHash": "sha256-VJQITz+vuQgl5HwR5QdUGwN8SRtGcb2/lJaAVfFbiSk=",
+        "owner": "CodingCellist",
+        "repo": "idris2-dot-parse",
+        "rev": "48fbda8bf8adbaf9e8ebd6ea740228e4394154d9",
+        "type": "github"
+      },
+      "original": {
+        "owner": "CodingCellist",
+        "repo": "idris2-dot-parse",
+        "type": "github"
+      }
+    },
+    "effect": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1637477153,
+        "narHash": "sha256-Ta2Vogg/IiSBkfhhD57jjPTEf3S4DOiVRmof38hmwlM=",
+        "owner": "russoul",
+        "repo": "idris2-effect",
+        "rev": "ea1daf53b2d7e52f9917409f5653adc557f0ee1a",
+        "type": "github"
+      },
+      "original": {
+        "owner": "russoul",
+        "repo": "idris2-effect",
+        "type": "github"
+      }
+    },
+    "elab-util": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639041013,
+        "narHash": "sha256-K61s/xifFiTDXJTak5NZmZL6757CTYCY+TGywRZMD7M=",
+        "owner": "stefan-hoeck",
+        "repo": "idris2-elab-util",
+        "rev": "7a381c7c5dc3adb7b97c8b8be17e4fb4cc63027d",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stefan-hoeck",
+        "repo": "idris2-elab-util",
+        "type": "github"
+      }
+    },
+    "flake-utils": {
+      "locked": {
+        "lastModified": 1652776076,
+        "narHash": "sha256-gzTw/v1vj4dOVbpBSJX4J0DwUR6LIyXo7/SuuTJp1kM=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "04c1b180862888302ddfb2e3ad9eaa63afc60cf8",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "flake-utils_2": {
+      "locked": {
+        "lastModified": 1638122382,
+        "narHash": "sha256-sQzZzAbvKEqN9s0bzWuYmRaA03v40gaJ4+iL1LXjaeI=",
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "rev": "74f7e4319258e287b0f9cb95426c9853b282730b",
+        "type": "github"
+      },
+      "original": {
+        "owner": "numtide",
+        "repo": "flake-utils",
+        "type": "github"
+      }
+    },
+    "frex": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1637410704,
+        "narHash": "sha256-BthU1t++n0ZvS76p0fCHsE33QSoXYxf0hMUSKajDY8w=",
+        "owner": "frex-project",
+        "repo": "idris-frex",
+        "rev": "22c480e879c757a5cebca7bb555ec3d21ae3ac28",
+        "type": "github"
+      },
+      "original": {
+        "owner": "frex-project",
+        "repo": "idris-frex",
+        "type": "github"
+      }
+    },
+    "fvect": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1633247988,
+        "narHash": "sha256-zElIze03XpcrYL4H5Aj0ZGNplJGbtOx+iWnivJMzHm0=",
+        "owner": "mattpolzin",
+        "repo": "idris-fvect",
+        "rev": "1c5e3761e0cd83e711a3535ef9051bea45e6db3f",
+        "type": "github"
+      },
+      "original": {
+        "owner": "mattpolzin",
+        "repo": "idris-fvect",
+        "type": "github"
+      }
+    },
+    "hashable": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1633965157,
+        "narHash": "sha256-Dggf5K//RCZ7uvtCyeiLNJS6mm+8/n0RFW3zAc7XqPg=",
+        "owner": "z-snails",
+        "repo": "idris2-hashable",
+        "rev": "d6fec8c878057909b67f3d4da334155de4f37907",
+        "type": "github"
+      },
+      "original": {
+        "owner": "z-snails",
+        "repo": "idris2-hashable",
+        "type": "github"
+      }
+    },
+    "hedgehog": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639041435,
+        "narHash": "sha256-893cPy7gGSQpVmm9co3QCpWsgjukafZHy8YFk9xts30=",
+        "owner": "stefan-hoeck",
+        "repo": "idris2-hedgehog",
+        "rev": "a66b1eb0bf84c4a7b743cfb217be69866bc49ad8",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stefan-hoeck",
+        "repo": "idris2-hedgehog",
+        "type": "github"
+      }
+    },
+    "idrall": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1636495701,
+        "narHash": "sha256-aOdCRd4XsSxwqVGta1adlZBy8TVTxTwFDnJ1dyMZK8M=",
+        "owner": "alexhumphreys",
+        "repo": "idrall",
+        "rev": "13ef174290169d05c9e9abcd77c53412e3e0c944",
+        "type": "github"
+      },
+      "original": {
+        "owner": "alexhumphreys",
+        "ref": "13ef174",
+        "repo": "idrall",
+        "type": "github"
+      }
+    },
+    "idris-server": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1634507315,
+        "narHash": "sha256-ulo23yLJXsvImoMB/1C6yRRTqmn/Odo+aUaVi+tUhJo=",
+        "owner": "avidela",
+        "repo": "idris-server",
+        "rev": "661a4ecf0fadaa2bd79c8e922c2d4f79b0b7a445",
+        "type": "gitlab"
+      },
+      "original": {
+        "owner": "avidela",
+        "repo": "idris-server",
+        "type": "gitlab"
+      }
+    },
+    "idris2": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639427352,
+        "narHash": "sha256-C1K2FM1Kio8vi9FTrivdacYCX4cywIsLBeNCsZ6ft4g=",
+        "owner": "idris-lang",
+        "repo": "idris2",
+        "rev": "36918e618646177b1e0c2fd01f21cc8d04d9da30",
+        "type": "github"
+      },
+      "original": {
+        "owner": "idris-lang",
+        "repo": "idris2",
+        "type": "github"
+      }
+    },
+    "idris2-pkgs": {
+      "inputs": {
+        "Prettier": "Prettier",
+        "collie": "collie",
+        "comonad": "comonad",
+        "dom": "dom",
+        "dot-parse": "dot-parse",
+        "effect": "effect",
+        "elab-util": "elab-util",
+        "flake-utils": "flake-utils_2",
+        "frex": "frex",
+        "fvect": "fvect",
+        "hashable": "hashable",
+        "hedgehog": "hedgehog",
+        "idrall": "idrall",
+        "idris-server": "idris-server",
+        "idris2": "idris2",
+        "indexed": "indexed",
+        "inigo": "inigo",
+        "ipkg-to-json": "ipkg-to-json",
+        "json": "json",
+        "katla": "katla",
+        "lsp": "lsp",
+        "nixpkgs": "nixpkgs",
+        "odf": "odf",
+        "pretty-show": "pretty-show",
+        "python": "python",
+        "rhone": "rhone",
+        "rhone-js": "rhone-js",
+        "snocvect": "snocvect",
+        "sop": "sop",
+        "tailrec": "tailrec",
+        "xml": "xml"
+      },
+      "locked": {
+        "lastModified": 1642030375,
+        "narHash": "sha256-J1uXnpPR72mjFjLBuYcvDHStBxVya6/MjBNNwqxGeD0=",
+        "owner": "claymager",
+        "repo": "idris2-pkgs",
+        "rev": "ac33a49d4d4bd2b50fddb040cd889733a02c8f09",
+        "type": "github"
+      },
+      "original": {
+        "owner": "claymager",
+        "repo": "idris2-pkgs",
+        "type": "github"
+      }
+    },
+    "indexed": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1638685238,
+        "narHash": "sha256-FceB7o88yKYzjTfRC6yfhOL6oDPMmCQAsJZu/pjE2uA=",
+        "owner": "mattpolzin",
+        "repo": "idris-indexed",
+        "rev": "ff3ba99b0063da6a74c96178e7f3c58a4ac1693e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "mattpolzin",
+        "repo": "idris-indexed",
+        "type": "github"
+      }
+    },
+    "inigo": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1637596767,
+        "narHash": "sha256-LNx30LO0YWDVSPTxRLWGTFL4f3d5ANG6c60WPdmiYdY=",
+        "owner": "idris-community",
+        "repo": "Inigo",
+        "rev": "57f5b5c051222d8c630010a0a3cf7d7138910127",
+        "type": "github"
+      },
+      "original": {
+        "owner": "idris-community",
+        "repo": "Inigo",
+        "type": "github"
+      }
+    },
+    "ipkg-to-json": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1634937414,
+        "narHash": "sha256-LhSmWRpI7vyIQE7QTo38ZTjlqYPVSvV/DIpIxzPmqS0=",
+        "owner": "claymager",
+        "repo": "ipkg-to-json",
+        "rev": "2969b6b83714eeddc31e41577a565778ee5922e6",
+        "type": "github"
+      },
+      "original": {
+        "owner": "claymager",
+        "repo": "ipkg-to-json",
+        "type": "github"
+      }
+    },
+    "json": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639041459,
+        "narHash": "sha256-TP/V1jBBP1hFPm/cJ5O2EJiaNoZ19KvBOAI0S9lvAR4=",
+        "owner": "stefan-hoeck",
+        "repo": "idris2-json",
+        "rev": "7c0c028acad0ba0b63b37b92199f37e6ec73864a",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stefan-hoeck",
+        "repo": "idris2-json",
+        "type": "github"
+      }
+    },
+    "katla": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1636542431,
+        "narHash": "sha256-X83NA/P3k1iPcBa8g5z8JldEmFEz/jxVeViJX0/FikY=",
+        "owner": "idris-community",
+        "repo": "katla",
+        "rev": "d841ec243f96b4762074211ee81033e28884c858",
+        "type": "github"
+      },
+      "original": {
+        "owner": "idris-community",
+        "repo": "katla",
+        "type": "github"
+      }
+    },
+    "lsp": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639486283,
+        "narHash": "sha256-po396FnUu8iqiipwPxqpFZEU4rtpX3jnt3cySwjLsH8=",
+        "owner": "idris-community",
+        "repo": "idris2-lsp",
+        "rev": "7ebb6caf6bb4b57c5107579aba2b871408e6f183",
+        "type": "github"
+      },
+      "original": {
+        "owner": "idris-community",
+        "repo": "idris2-lsp",
+        "type": "github"
+      }
+    },
+    "nixpkgs": {
+      "locked": {
+        "lastModified": 1639213685,
+        "narHash": "sha256-Evuobw7o9uVjAZuwz06Al0fOWZ5JMKOktgXR0XgWBtg=",
+        "owner": "nixos",
+        "repo": "nixpkgs",
+        "rev": "453bcb8380fd1777348245b3c44ce2a2b93b2e2d",
+        "type": "github"
+      },
+      "original": {
+        "owner": "nixos",
+        "ref": "nixpkgs-21.11-darwin",
+        "repo": "nixpkgs",
+        "type": "github"
+      }
+    },
+    "odf": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1638184051,
+        "narHash": "sha256-usSdPx+UqOGImHHdHcrytdzi2LXtIRZuUW0fkD/Wwnk=",
+        "owner": "madman-bob",
+        "repo": "idris2-odf",
+        "rev": "d2f532437321c8336f1ca786b44b6ebef4117126",
+        "type": "github"
+      },
+      "original": {
+        "owner": "madman-bob",
+        "repo": "idris2-odf",
+        "type": "github"
+      }
+    },
+    "pretty-show": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639041411,
+        "narHash": "sha256-BzEe1fpX+lqGEk8b1JZoQT1db5I7s7SZnLCttRVGXdY=",
+        "owner": "stefan-hoeck",
+        "repo": "idris2-pretty-show",
+        "rev": "a4bc6156b9dac43699f87504cbdb8dada5627863",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stefan-hoeck",
+        "repo": "idris2-pretty-show",
+        "type": "github"
+      }
+    },
+    "python": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1635936936,
+        "narHash": "sha256-c9mcMApN0qgu0AXQVu0V+NXt2poP258wCPkyvtQvv4I=",
+        "owner": "madman-bob",
+        "repo": "idris2-python",
+        "rev": "0eab028933c65bebe744e879881416f5136d6943",
+        "type": "github"
+      },
+      "original": {
+        "owner": "madman-bob",
+        "repo": "idris2-python",
+        "type": "github"
+      }
+    },
+    "rhone": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639041532,
+        "narHash": "sha256-2g43shlWQIT/1ogesUBUBV9N8YiD3RwaCbbhdKLVp1s=",
+        "owner": "stefan-hoeck",
+        "repo": "idris2-rhone",
+        "rev": "c4d828b0b8efea495d9a5f1e842a9c67cad57724",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stefan-hoeck",
+        "repo": "idris2-rhone",
+        "type": "github"
+      }
+    },
+    "rhone-js": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639041546,
+        "narHash": "sha256-ddWVsSRbfA6ghmwiRMzDpHBPM+esGdutuqm1qQZgs88=",
+        "owner": "stefan-hoeck",
+        "repo": "idris2-rhone-js",
+        "rev": "520dd59549f5b14075045314b6805c7492ed636e",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stefan-hoeck",
+        "repo": "idris2-rhone-js",
+        "type": "github"
+      }
+    },
+    "root": {
+      "inputs": {
+        "flake-utils": "flake-utils",
+        "idris2-pkgs": "idris2-pkgs",
+        "nixpkgs": [
+          "idris2-pkgs",
+          "nixpkgs"
+        ]
+      }
+    },
+    "snocvect": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1641633224,
+        "narHash": "sha256-6zTU4sDzd/R/dFCTNZaX41H4L3/USGLFghMS0Oc9liY=",
+        "owner": "mattpolzin",
+        "repo": "idris-snocvect",
+        "rev": "ff1e7afba360a62f7e522e9bbb856096a79702c4",
+        "type": "github"
+      },
+      "original": {
+        "owner": "mattpolzin",
+        "repo": "idris-snocvect",
+        "type": "github"
+      }
+    },
+    "sop": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1639041379,
+        "narHash": "sha256-PDTf1Wx6EygiWszguvoVPiqIISYFLabI4e0lXHlrjcA=",
+        "owner": "stefan-hoeck",
+        "repo": "idris2-sop",
+        "rev": "e4354d1883cd73616019457cb9ebf864d99df6a0",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stefan-hoeck",
+        "repo": "idris2-sop",
+        "type": "github"
+      }
+    },
+    "tailrec": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1637146655,
+        "narHash": "sha256-0yi7MQIrISPvAwkgDC1M5PHDEeVyIaISF0HjKDaT0Rw=",
+        "owner": "stefan-hoeck",
+        "repo": "idris2-tailrec",
+        "rev": "dd0bc6381b3a2e69aa37f9a8c1b165d4b1516ad7",
+        "type": "github"
+      },
+      "original": {
+        "owner": "stefan-hoeck",
+        "repo": "idris2-tailrec",
+        "type": "github"
+      }
+    },
+    "xml": {
+      "flake": false,
+      "locked": {
+        "lastModified": 1637939752,
+        "narHash": "sha256-yYJBhPfwYoi7amlHmeNGrVCOAc3BjZpKTCd9wDs3XEM=",
+        "owner": "madman-bob",
+        "repo": "idris2-xml",
+        "rev": "1292ccfcd58c551089ef699e4560343d5c473d64",
+        "type": "github"
+      },
+      "original": {
+        "owner": "madman-bob",
+        "repo": "idris2-xml",
+        "type": "github"
+      }
+    }
+  },
+  "root": "root",
+  "version": 7
+}
diff --git a/flake.nix b/flake.nix
new file mode 100644
index 0000000..a71fcba
--- /dev/null
+++ b/flake.nix
@@ -0,0 +1,26 @@
+{ description = "basic test framework for idris 2";
+
+  inputs = {
+    flake-utils.url = "github:numtide/flake-utils";
+    idris2-pkgs.url = "github:claymager/idris2-pkgs";
+    nixpkgs.follows = "idris2-pkgs/nixpkgs";
+  };
+
+  outputs = { self, nixpkgs, idris2-pkgs, flake-utils }:
+    flake-utils.lib.eachSystem [ "x86_64-darwin" "x86_64-linux" "i686-linux" ]
+      (system:
+        let
+          pkgs = import nixpkgs {
+            inherit system;
+            overlays = [ idris2-pkgs.overlay ];
+          };
+          inherit (pkgs.idris2-pkgs._builders) idrisPackage devEnv;
+
+          tap = idrisPackage ./. { };
+        in {
+          defaultPackage = tap;
+          packages = { inherit tap; };
+          devShell = pkgs.mkShell { buildInputs = [ (devEnv tap) ]; };
+        }
+      );
+}
diff --git a/tap.ipkg b/tap.ipkg
new file mode 100644
index 0000000..2d1347b
--- /dev/null
+++ b/tap.ipkg
@@ -0,0 +1,11 @@
+package tap
+version = 0.1
+
+authors   = "rhiannon morris"
+-- sourceloc = "https://git.rhiannon.website/rhi/idris2-tap"
+license   = "acsl"
+
+depends = base, contrib
+
+sourcedir = "."
+modules = TAP.Options, TAP