%inline, etc

the value 70 is EX_SOFTWARE from bsd's sysexits.h. i was looking for an
excuse to use 69 but alas it was not to be

quox.ipkg

@@ -15,6 +15,20 @@ modules =
   Quox.Pretty,
 
   Quox.Syntax,
+  Quox.Syntax.Dim,
+  Quox.Syntax.DimEq,
+  Quox.Syntax.Qty,
+  Quox.Syntax.Shift,
+  Quox.Syntax.Subst,
+  Quox.Syntax.Term,
+  Quox.Syntax.Term.Base,
+  Quox.Syntax.Term.Pretty,
+  Quox.Syntax.Term.Reduce,
+  Quox.Syntax.Term.Split,
+  Quox.Syntax.Term.Subst,
+  Quox.Syntax.Universe,
+  Quox.Syntax.Var,
+
   Quox.Context,
   Quox.Equal,
   Quox.Name,

src/Quox/Equal.idr

@@ -10,6 +10,8 @@ import Quox.Error
 public export
 data Mode = Equal | Sub
 
+export %inline Show Mode where show Equal = "Equal"; show Sub = "Sub"
+
 public export
 data Error
 = ClashT Mode (Term d n) (Term d n)

src/Quox/Error.idr

@@ -1,6 +1,6 @@
 module Quox.Error
 
-import Data.List.Elem
+import public Data.List.Elem
 
 import public Control.Monad.Identity
 import Control.Monad.Trans

tests/TAP.idr

@@ -6,8 +6,10 @@ import Data.String
 import Data.List.Elem
 import Control.Monad.Reader
 import Control.Monad.State
+import System
 
-public export Info : Type
+public export
+Info : Type
 Info = List (String, String)
 
 private
@@ -20,13 +22,19 @@ record TestBase where
   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 (\(k, v) => "\{k}: |" :: map (indent 2) (lines v)) xs
-  <+> ["..."]
+toLines xs = "---" :: concatMap toLines1 xs <+> ["..."]
+
 
 public export interface ToInfo e where toInfo : e -> Info
 
@@ -35,7 +43,7 @@ All ToInfo es => ToInfo (OneOf es) where
   toInfo (One Here      value) = toInfo value
   toInfo (One (There x) value) = toInfo (One x value)
 
-export ToInfo () where toInfo () = []
+export %inline ToInfo () where toInfo () = []
 
 export
 data Test = One TestBase | Group String (List Test)
@@ -76,7 +84,7 @@ export %inline
 
 
 
-export
+export %inline
 header : List a -> String
 header tests = "1..\{show $ length tests}"
 
@@ -85,15 +93,15 @@ private
 Runner : Type -> Type
 Runner = ReaderT Nat IO
 
-private
+private %inline
 putIndentLines : List String -> Runner ()
 putIndentLines xs = traverse_ (putStrLn . indent !ask) xs
 
-private
+private %inline
 isOk : Bool -> String
 isOk b = if b then "ok" else "not ok"
 
-private
+private %inline
 toBool : Result -> Bool
 toBool (Tried ok _) = ok
 toBool _ = True
@@ -111,12 +119,12 @@ run1' : (Nat, TestBase) -> Runner Bool
 run1' (index, test) = do
   res <- liftIO test.run
   case res of
-       Tried ok info => putIndentLines $
-         "\{isOk ok} \{show index} - \{test.label}" ::
-         toLines info
-       Skip reason => putIndentLines $
+       Tried ok info => do
+         putIndentLines ["\{isOk ok} \{show index} - \{test.label}"]
+         local (plus 2) $ putIndentLines $ toLines info
+       Skip reason => putIndentLines
          ["ok \{show index} - \{test.label}  # skip \{reason}"]
-       Todo reason => putIndentLines $
+       Todo reason => putIndentLines
          ["ok \{show index} - \{test.label}  # todo \{reason}"]
   pure $ toBool res
 
@@ -138,7 +146,9 @@ mutual
 
 
 export
-run : List Test -> IO ()
+run : List Test -> IO ExitCode
 run tests = do
   putStrLn "TAP version 14"
-  ignore $ runReaderT 0 $ runList tests
+  pure $ if !(runReaderT 0 $ runList tests)
+            then ExitSuccess
+            else ExitFailure 70