From 64fe3a5a0fbb6b0183c745746acaf43eba539af0 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 27 Apr 2022 14:54:22 +0200 Subject: [PATCH 1/7] list all modules in quox.ipkg since building succeeded i thought unlisted ones would just be private. but no they don't get installed --- quox.ipkg | 14 ++++++++++++++ 1 file changed, 14 insertions(+) diff --git a/quox.ipkg b/quox.ipkg index 6e0dc60..f3ca34e 100644 --- a/quox.ipkg +++ b/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, From 7629404097b9753043325affecb8b084611b5b73 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 27 Apr 2022 14:55:19 +0200 Subject: [PATCH 2/7] reexport Data.List.Elem from Quox.Error the constructors need to be in scope for auto to use them --- src/Quox/Error.idr | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/src/Quox/Error.idr b/src/Quox/Error.idr index 8c02208..cee1f3b 100644 --- a/src/Quox/Error.idr +++ b/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 From bcd454469207e02a836a8c5aab49c199ef11cfde Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 27 Apr 2022 14:56:39 +0200 Subject: [PATCH 3/7] Show Quox.Equal.Mode --- src/Quox/Equal.idr | 2 ++ 1 file changed, 2 insertions(+) diff --git a/src/Quox/Equal.idr b/src/Quox/Equal.idr index 943993a..c96d872 100644 --- a/src/Quox/Equal.idr +++ b/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) From d74b056e11df5d55abf2d2153da5cefb6efc20d7 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 27 Apr 2022 14:57:41 +0200 Subject: [PATCH 4/7] put single line yaml info on one line --- tests/TAP.idr | 14 ++++++++++---- 1 file changed, 10 insertions(+), 4 deletions(-) diff --git a/tests/TAP.idr b/tests/TAP.idr index 95346f9..7a86ed2 100644 --- a/tests/TAP.idr +++ b/tests/TAP.idr @@ -20,13 +20,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 From d062f7917659b96267402f8fbe94ec06b5ac25e7 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 27 Apr 2022 15:03:29 +0200 Subject: [PATCH 5/7] fix yaml doc indent --- tests/TAP.idr | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/tests/TAP.idr b/tests/TAP.idr index 7a86ed2..4be6880 100644 --- a/tests/TAP.idr +++ b/tests/TAP.idr @@ -117,12 +117,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 From a690ca12775e126c2cc3d79efb3fec05f07bdb79 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 27 Apr 2022 15:04:10 +0200 Subject: [PATCH 6/7] return an exit code from TAP.run 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 --- tests/TAP.idr | 7 +++++-- 1 file changed, 5 insertions(+), 2 deletions(-) diff --git a/tests/TAP.idr b/tests/TAP.idr index 4be6880..96dfcec 100644 --- a/tests/TAP.idr +++ b/tests/TAP.idr @@ -6,6 +6,7 @@ import Data.String import Data.List.Elem import Control.Monad.Reader import Control.Monad.State +import System public export Info : Type Info = List (String, String) @@ -144,7 +145,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 From 66c96cb3c4b913770eec4f88cd98409c691c1581 Mon Sep 17 00:00:00 2001 From: rhiannon morris Date: Wed, 27 Apr 2022 15:07:32 +0200 Subject: [PATCH 7/7] %inline, etc --- tests/TAP.idr | 13 +++++++------ 1 file changed, 7 insertions(+), 6 deletions(-) diff --git a/tests/TAP.idr b/tests/TAP.idr index 96dfcec..0367875 100644 --- a/tests/TAP.idr +++ b/tests/TAP.idr @@ -8,7 +8,8 @@ import Control.Monad.Reader import Control.Monad.State import System -public export Info : Type +public export +Info : Type Info = List (String, String) private @@ -42,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) @@ -83,7 +84,7 @@ export %inline -export +export %inline header : List a -> String header tests = "1..\{show $ length tests}" @@ -92,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