time for sirdi

tests/src/Options.idr

@@ -0,0 +1,40 @@
+module Options
+
+import Data.String
+import System
+import System.Console.GetOpt
+
+
+public export
+record Options where
+  constructor Opts
+  tapVersion : String
+
+defaultOpts = Opts {tapVersion = "13"}
+
+OptMod = Options -> Options
+
+opts : List (OptDescr OptMod)
+opts = [
+  MkOpt ['V'] ["version"]
+    (ReqArg (\v => the OptMod {tapVersion := v}) "VERSION")
+    "TAP version to output (13 or 14, default 13)"
+]
+-- [todo] get rid of "the OptMod" when type inference is better, maybe
+
+makeOpts : List OptMod -> Options
+makeOpts = foldl (flip ($)) defaultOpts
+
+
+getArgs1 : IO (List String)
+getArgs1 =
+  case !getArgs of
+       _ :: args => pure args
+       []        => die "expecting getArgs to start with exe name"
+
+export
+getTestOpts : IO Options
+getTestOpts =
+  case getOpt Permute opts !getArgs1 of
+       MkResult opts [] [] [] => pure $ makeOpts opts
+       res => die $ unlines $ res.errors ++ [usageInfo "quox test suite" opts]

tests/src/TAP.idr

@@ -0,0 +1,220 @@
+module TAP
+
+import public Quox.Error
+
+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)
+
+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
+All ToInfo es => ToInfo (OneOf es) where
+  toInfo (One Here      value) = toInfo value
+  toInfo (One (There x) value) = toInfo (One x value)
+
+export %inline ToInfo () where toInfo () = []
+
+export Show a => ToInfo (List (String, a)) where toInfo = map (map show)
+
+
+export
+data Test = One TestBase | Group String (List Test)
+
+
+private %inline
+success : ToInfo a => a -> IO Result
+success = pure . Tried True . toInfo
+
+private %inline
+failure : ToInfo e => e -> IO Result
+failure = pure . Tried False . toInfo
+
+private %inline
+lazyToIO : Lazy a -> IO a
+lazyToIO val = primIO $ \w => MkIORes (force val) w
+
+export
+testIO : (All ToInfo es, ToInfo a) => String -> ErrorT es IO a -> Test
+testIO label act = One $ MakeTest label $ do
+  case !(runErrorT act) of
+       Right val => success val
+       Left  err => failure err
+
+export %inline
+test : (All ToInfo es, ToInfo a) => String -> Lazy (Error es a) -> Test
+test label val =
+  testIO label $ MkErrorT $ lazyToIO $ runError val
+
+export %inline
+todoWith : String -> String -> Test
+todoWith label reason = One $ MakeTest label $ pure $ Todo reason
+
+export %inline
+todo : String -> Test
+todo label = todoWith label ""
+
+private %inline
+makeSkip : String -> String -> Test
+makeSkip label reason = One $ MakeTest label $ pure $ Skip reason
+
+export %inline
+skipWith : Test -> String -> Test
+skipWith (One   t)   reason = makeSkip t.label reason
+skipWith (Group l _) reason = makeSkip l       reason
+
+export %inline
+skip : Test -> Test
+skip test = skipWith test ""
+
+export
+testThrows : Show a => String -> Lazy (Error es a) -> Test
+testThrows label act = One $ MakeTest label $ do
+  case runError !(lazyToIO act) of
+       Left  err => success ()
+       Right val => failure [("success", val)]
+
+infix 0 :-
+export %inline
+(:-) : String -> List Test -> Test
+(:-) = Group
+
+export %inline
+bailOut : Test
+bailOut = One $ MakeTest "bail out" $ do
+  putStrLn "Bail out!"
+  exitFailure
+
+
+
+export %inline
+header : List a -> String
+header tests = "1..\{show $ length tests}"
+
+makePrefix : SnocList String -> String
+makePrefix [<]       = ""
+makePrefix (xs :< x) = foldr (\a, b => "\{a}/\{b}") x xs
+
+withPrefix : SnocList String -> TestBase -> Test
+withPrefix pfx b = One $ {label := "[\{makePrefix pfx}] \{b.label}"} b
+
+mutual
+  export
+  flattenWith : SnocList String -> List Test -> List Test
+  flattenWith pfx = concatMap (flatten1With pfx)
+
+  export
+  flatten1With : SnocList String -> Test -> List Test
+  flatten1With pfx (One   t)    = [withPrefix pfx t]
+  flatten1With pfx (Group x ts) = flattenWith (pfx :< x) ts
+
+export
+flatten : List Test -> List Test
+flatten = flattenWith [<]
+
+export
+flatten1 : Test -> List Test
+flatten1 = flatten1With [<]
+
+
+private
+Runner : Type -> Type
+Runner = ReaderT Nat IO
+
+private %inline
+putIndentLines : List String -> Runner ()
+putIndentLines xs = traverse_ (putStrLn . indent !ask) xs
+
+private %inline
+isOk : Bool -> String
+isOk b = if b then "ok" else "not ok"
+
+private %inline
+toBool : Result -> Bool
+toBool (Tried ok _) = ok
+toBool _ = True
+
+
+private
+numbered : List a -> List (Nat, a)
+numbered = go 1 where
+  go : Nat -> List a -> List (Nat, a)
+  go _ []        = []
+  go i (x :: xs) = (i, x) :: go (S i) xs
+
+private
+run1' : (Nat, TestBase) -> Runner Bool
+run1' (index, test) = do
+  res <- liftIO test.run
+  case res of
+       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
+         ["ok \{show 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 ["# Subtest: \{label}"]
+    res <- local (plus 4) $ runList tests
+    putIndentLines ["\{isOk res} \{show index} - \{label}"]
+    pure res
+
+  private
+  runList : List Test -> Runner Bool
+  runList tests = do
+    putIndentLines [header tests]
+    all id <$> traverse run' (numbered tests)
+
+
+export
+run : (ver : Nat) -> List Test -> IO ExitCode
+run ver tests = do
+  putStrLn "TAP version \{show ver}"
+  pure $ if !(runReaderT 0 $ runList tests)
+            then ExitSuccess
+            else ExitFailure 70
+
+export
+main : List Test -> IO ()
+main tests = exitWith !(run 14 tests)
+
+export
+mainFlat : List Test -> IO ()
+mainFlat tests = exitWith !(run 13 $ flatten tests)

tests/src/Tests.idr

@@ -0,0 +1,21 @@
+module Tests
+
+import Options
+import TAP
+import Tests.Lexer
+import Tests.Equal
+import System
+
+
+allTests = [
+  Lexer.tests,
+  skip Equal.tests
+]
+
+main = do
+  opts <- getTestOpts
+  go <- case opts.tapVersion of
+    "13" => pure TAP.mainFlat
+    "14" => pure TAP.main
+    _    => die "unrecognised TAP version; use 13 or 14"
+  go allTests

tests/src/Tests/Equal.idr

@@ -0,0 +1,101 @@
+module Tests.Equal
+
+import Quox.Equal
+import Quox.Pretty
+import TAP
+
+export
+ToInfo Equal.Error where
+  toInfo (ClashT mode s t) =
+    [("clash",  "term"),
+     ("mode",   show mode),
+     ("left",  prettyStr True s),
+     ("right", prettyStr True t)]
+  toInfo (ClashU mode k l) =
+    [("clash",  "universe"),
+     ("mode",   show mode),
+     ("left",  prettyStr True k),
+     ("right", prettyStr True l)]
+  toInfo (ClashQ pi rh) =
+    [("clash",  "quantity"),
+     ("left",  prettyStr True pi),
+     ("right", prettyStr True rh)]
+
+
+M = Error [Equal.Error]
+
+testEq : String -> Lazy (M ()) -> Test
+testEq = test
+
+testNeq : String -> Lazy (M ()) -> Test
+testNeq = testThrows
+
+
+subT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
+subT = Quox.Equal.subT
+%hide Quox.Equal.subT
+
+equalT : {default 0 d, n : Nat} -> Term d n -> Term d n -> M ()
+equalT = Quox.Equal.equalT
+%hide Quox.Equal.equalT
+
+subE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
+subE = Quox.Equal.subE
+%hide Quox.Equal.subE
+
+equalE : {default 0 d, n : Nat} -> Elim d n -> Elim d n -> M ()
+equalE = Quox.Equal.equalE
+%hide Quox.Equal.equalE
+
+
+export
+tests : Test
+tests = "equality & subtyping" :- [
+    "universes" :- [
+        testEq "Type 0 == Type 0" $
+          equalT (TYPE (U 0)) (TYPE (U 0)),
+        testNeq "Type 0 =/= Type 1" $
+          equalT (TYPE (U 0)) (TYPE (U 1)),
+        testNeq "Type 1 =/= Type 0" $
+          equalT (TYPE (U 1)) (TYPE (U 0)),
+        testEq "Type 0 <: Type 0" $
+          subT (TYPE (U 0)) (TYPE (U 0)),
+        testEq "Type 0 <: Type 1" $
+          subT (TYPE (U 0)) (TYPE (U 1)),
+        testNeq "Type 1 </: Type 0" $
+          subT (TYPE (U 1)) (TYPE (U 0))
+      ],
+    todo "pi",
+    todo "lambda",
+    todo "term closure",
+    todo "term d-closure",
+
+    "free var" :- [
+        testEq "A == A" $
+          equalE (F "A") (F "A"),
+        testNeq "A =/= B" $
+          equalE (F "A") (F "B"),
+        testEq "A <: A" $
+          subE (F "A") (F "A"),
+        testNeq "A </: B" $
+          subE (F "A") (F "B")
+      ],
+    todo "bound var",
+    "application" :-
+      let a    = F "a"; a' = E a
+          A    = FT "A"
+          λxx  = Lam "x" (TUsed (BVT 0))
+          A_A  = Arr one A A
+          λxx' = λxx :# A_A
+      in [
+        testEq "(λx. x : A -> A) a == ((a : A) : A)  (β)" $
+          equalE (λxx' :@ a') (E (a' :# A) :# A),
+        testEq "(λx. x : _) a == a  (βυ)" $
+          equalE (λxx' :@ a') a
+      ],
+    todo "annotation",
+    todo "elim closure",
+    todo "elim d-closure",
+
+    todo "clashes"
+  ]

tests/src/Tests/Lexer.idr

@@ -0,0 +1,105 @@
+module Tests.Lexer
+
+import Quox.Lexer
+import TAP
+
+
+export
+ToInfo Error where
+  toInfo (Err line col char) =
+    [("line", show line), ("col", show col), ("char", show char)]
+
+data ExtraError
+= WrongAnswer (List Kind) (List Kind)
+| TestFailed  (List Kind)
+
+ToInfo ExtraError where
+  toInfo (WrongAnswer exp got) =
+    [("expected", show exp), ("received", show got)]
+  toInfo (TestFailed got) = [("failed", show got)]
+
+
+parameters (label : String) (input : String)
+  acceptsSuchThat' : (List Kind -> Maybe ExtraError) -> Test
+  acceptsSuchThat' p = test {es = [Lexer.Error, ExtraError]} label $ do
+    res <- map (kind . val) <$> lex input
+    case p res of
+         Just err => throw err
+         Nothing  => pure ()
+
+  acceptsSuchThat : (List Kind -> Bool) -> Test
+  acceptsSuchThat p = acceptsSuchThat' $ \res =>
+    if p res then Nothing else Just $ TestFailed res
+
+  acceptsWith : List Kind -> Test
+  acceptsWith expect = acceptsSuchThat' $ \res =>
+    if res == expect then Nothing else Just $ WrongAnswer expect res
+
+  accepts : Test
+  accepts = acceptsSuchThat $ const True
+
+  rejects : Test
+  rejects = testThrows {es = [Lexer.Error]} label $ delay $
+    map (kind . val) <$> lex input
+
+parameters (input : String) {default False esc : Bool}
+  show' : String -> String
+  show' s = if esc then show s else "\"\{s}\""
+
+  acceptsWith' : List Kind -> Test
+  acceptsWith' = acceptsWith (show' input) input
+
+  accepts' : Test
+  accepts' = accepts (show' input) input
+
+  rejects' : Test
+  rejects' = rejects "\{show' input}  (reject)" input
+
+
+tests = "lexer" :- [
+  "comments" :- [
+    acceptsWith' ""            [],
+    acceptsWith' "  \n \t\t "  [] {esc = True},
+    acceptsWith' "-- a"        [],
+    acceptsWith' "{- -}"       [],
+    acceptsWith' "{--}"        [],
+    acceptsWith' "{------}"    [],
+    acceptsWith' "{- {- -} -}" [],
+    acceptsWith' "{- } -}"     [],
+    rejects' "{-}",
+    rejects' "{- {- -}",
+    acceptsWith' "( -- comment \n )" [P LParen, P RParen] {esc = True}
+  ],
+
+  "punctuation" :- [
+    acceptsWith' "({[:,::]})"
+      [P LParen, P LBrace, P LSquare,
+       P Colon, P Comma, P DblColon,
+       P RSquare, P RBrace, P RParen],
+    acceptsWith' " ( { [ : , :: ] } ) "
+      [P LParen, P LBrace, P LSquare,
+       P Colon, P Comma, P DblColon,
+       P RSquare, P RBrace, P RParen],
+    acceptsWith' "-> → => ⇒ ** × << ⊲ ∷"
+      [P Arrow, P Arrow, P DblArrow, P DblArrow,
+       P Times, P Times, P Triangle, P Triangle, P DblColon],
+    acceptsWith' "_" [P Wild]
+  ],
+
+  "names & symbols" :- [
+    acceptsWith' "a"        [Name],
+    acceptsWith' "abc"      [Name],
+    acceptsWith' "_a"       [Name],
+    acceptsWith' "a_"       [Name],
+    acceptsWith' "a_b"      [Name],
+    acceptsWith' "abc'"     [Name],
+    acceptsWith' "a'b'c''"  [Name],
+    acceptsWith' "abc123"   [Name],
+    acceptsWith' "ab cd"    [Name, Name],
+    acceptsWith' "ab{--}cd" [Name, Name],
+    acceptsWith' "'a"       [Symbol],
+    acceptsWith' "'ab"      [Symbol],
+    acceptsWith' "'_b"      [Symbol],
+    rejects'     "'"
+  ]
+]