explore alternative implementation

idris-lang · Jul 16, 2024 · 3e20c4f · 3e20c4f
1 parent bb6c5af
commit 3e20c4f
Show file tree

Hide file tree

Showing 2 changed files with 62 additions and 83 deletions.
diff --git a/libs/test/Test/Golden.idr b/libs/test/Test/Golden.idr
@@ -332,40 +332,19 @@ pathLookup names = do
 ||| Return Nothing to indicate the requirement is not met and tests relying on it
 ||| should be skipped.
 public export
-interface Requirement r where
+record Requirement where
   constructor MkReq
-  name : r -> String
-  satisfy : r -> IO (Maybe String)
+  name : String
+  satisfy : IO (Maybe String)
+
+export
+Show Requirement where
+  show = name
 
 ||| Some test may involve Idris' backends and have requirements.
 ||| We define here the ones supported by Idris
 public export
-data BackendRequirement = C | Chez | Node | Racket | Gambit
-
-export
-Eq BackendRequirement where
-  C == C = True
-  Chez == Chez = True
-  Node == Node = True
-  Racket == Racket = True
-  Gambit == Gambit = True
-  _ == _ = False
-
-export
-Show BackendRequirement where
-  show C = "C"
-  show Chez = "Chez"
-  show Node = "node"
-  show Racket = "racket"
-  show Gambit = "gambit"
-
-export
-[CG] Show BackendRequirement where
-  show C = "refc"
-  show Chez = "chez"
-  show Node = "node"
-  show Racket = "racket"
-  show Gambit = "gambit"
+data BackendRequirement = ReqC | ReqChez | ReqNodeJS | ReqRacket | ReqGambit
 
 export
 checkRequirement : BackendRequirement -> IO (Maybe String)
@@ -377,32 +356,46 @@ checkRequirement req
       else pure Nothing
   where
     requirement : BackendRequirement -> (String, List String)
-    requirement C = ("CC", ["cc"])
-    requirement Chez = ("CHEZ", ["chez", "chezscheme9.5", "chezscheme", "chez-scheme", "scheme"])
-    requirement Node = ("NODE", ["node"])
-    requirement Racket = ("RACKET", ["racket"])
-    requirement Gambit = ("GAMBIT", ["gsc"])
+    requirement ReqC = ("CC", ["cc"])
+    requirement ReqChez = ("CHEZ", ["chez", "chezscheme9.5", "chezscheme", "chez-scheme", "scheme"])
+    requirement ReqNodeJS = ("NODE", ["node"])
+    requirement ReqRacket = ("RACKET", ["racket"])
+    requirement ReqGambit = ("GAMBIT", ["gsc"])
 
     platformSupport : BackendRequirement -> Bool
-    platformSupport C = not isWindows
-    platformSupport Racket = not isWindows
+    platformSupport ReqC = not isWindows
+    platformSupport ReqRacket = not isWindows
     platformSupport _ = True
 
-||| Create a Requirement from a BackendRequirement
 export
-Requirement BackendRequirement where
-  name = show
-  satisfy = checkRequirement
+C : Requirement
+C = MkReq "refc" (checkRequirement ReqC)
+
+export
+Chez : Requirement
+Chez = MkReq "chez" (checkRequirement ReqChez)
+
+export
+Node : Requirement
+Node = MkReq "node" (checkRequirement ReqNodeJS)
+
+export
+Racket : Requirement
+Racket = MkReq "racket" (checkRequirement ReqRacket)
+
+export
+Gambit : Requirement
+Gambit = MkReq "gambit" (checkRequirement ReqGambit)
 
 export
 findCG : IO (Maybe String)
 findCG
   = do Nothing <- getEnv "IDRIS2_TESTS_CG" | p => pure p
-       Nothing <- checkRequirement Chez    | p => pure (Just "chez")
-       Nothing <- checkRequirement Node    | p => pure (Just "node")
-       Nothing <- checkRequirement Racket  | p => pure (Just "racket")
-       Nothing <- checkRequirement Gambit  | p => pure (Just "gsc")
-       Nothing <- checkRequirement C       | p => pure (Just "refc")
+       Nothing <- checkRequirement ReqChez    | p => pure (Just "chez")
+       Nothing <- checkRequirement ReqNodeJS  | p => pure (Just "node")
+       Nothing <- checkRequirement ReqRacket  | p => pure (Just "racket")
+       Nothing <- checkRequirement ReqGambit  | p => pure (Just "gsc")
+       Nothing <- checkRequirement ReqC       | p => pure (Just "refc")
        pure Nothing
 
 ||| A choice of a codegen
@@ -414,10 +407,10 @@ data Codegen
     ||| and if nothing was passed guess a sensible default using findCG
     Default
   | ||| Use exactly the given requirement
-    Just BackendRequirement
+    Just Requirement
 
 export
-codegenRequirement : Codegen -> List BackendRequirement
+codegenRequirement : Codegen -> List Requirement
 codegenRequirement (Just r) = [r]
 codegenRequirement _ = []
 
@@ -430,9 +423,7 @@ public export
 record TestPool where
   constructor MkTestPool
   poolName : String
-  {default BackendRequirement 0 req : Type}
-  {auto reqPrf : Requirement req}
-  constraints : List req
+  constraints : List Requirement
   codegen : Codegen
   testCases : List String
 
@@ -456,35 +447,20 @@ findTests pred codegen poolName dirName = do
                True  => pure $ p :: rem
                False => pure rem
 
-||| Find all the test in the given directory.
+||| Find all the test in the given directory but only run them given any
+||| requirements specified are met.
 export
 testsInDir :
   (dirName : String) ->
   {default (const True) pred : String -> Bool} ->
   (poolName : String) ->
+  {default [] requirements : List Requirement} ->
   {default Nothing codegen : Codegen} ->
   Lazy (IO TestPool)
 testsInDir dirName poolName = do
   testNames <- findTests pred codegen poolName dirName
   when (length testNames == 0) $ die $ "no tests found in " ++ dirName
-  pure $ MkTestPool poolName [] codegen testNames
-
-||| Find all the test in the given directory but only run them given the
-||| requirements specified are met.
-export
-testsInDir' :
-  {0 req : Type} ->
-  Requirement req =>
-  (dirName : String) ->
-  {default (const True) pred : String -> Bool} ->
-  (poolName : String) ->
-  (requirements : List req) ->
-  {default Nothing codegen : Codegen} ->
-  Lazy (IO TestPool)
-testsInDir' dirName poolName requirements = do
-  testNames <- findTests pred codegen poolName dirName
-  when (length testNames == 0) $ die $ "no tests found in " ++ dirName
-  pure $ MkTestPool {req} poolName requirements codegen testNames
+  pure $ MkTestPool poolName requirements codegen testNames
 
 ||| Only keep the tests that have been asked for
 export
@@ -612,20 +588,23 @@ poolRunner opts pool
        let (_ :: _) = tests
              | [] => pure initSummary
        -- if so make sure the constraints are satisfied
-       let cgReq = codegenRequirement pool.codegen
-       cs1 <- traverse checkReq cgReq
-       cs2 <- traverse (checkReq @{pool.reqPrf}) pool.constraints
-       let (cs, msgs) = unzip (cs1 ++ cs2)
+       cs <- for (codegenRequirement pool.codegen ++ pool.constraints) $ \ req => do
+          mfp <- satisfy req
+          let msg = case mfp of
+                      Nothing => "✗ " ++ req.name ++ " not found"
+                      Just fp => "✓ Found " ++ req.name ++ " at " ++ fp
+          pure (mfp, msg)
+       let (cs, msgs) = unzip cs
 
        putStrLn (banner msgs)
 
        let Just _ = the (Maybe (List String)) (sequence cs)
              | Nothing => pure initSummary
 
        -- if the test pool requires a specific codegen then use that
-       let opts = case codegen pool of
+       let opts = case pool.codegen of
                     Nothing => { codegen := Nothing } opts
-                    Just cg => { codegen := Just (show @{CG} cg) } opts
+                    Just cg => { codegen := Just cg.name } opts
                     Default => opts
 
        -- set up the channels
@@ -647,7 +626,7 @@ poolRunner opts pool
 
   where
 
-    checkReq : {0 req : Type} -> Requirement req => req -> IO (Maybe String, String)
+    checkReq : {0 req : Type} -> Requirement -> IO (Maybe String, String)
     checkReq req = do
       mfp <- satisfy req
       let msg = case mfp of

diff --git a/tests/Main.idr b/tests/Main.idr
@@ -75,19 +75,19 @@ idrisTestsEvaluator = testsInDir "idris2/evaluator" "Evaluation"
 idrisTestsREPL : IO TestPool
 idrisTestsREPL = testsInDir "idris2/repl" "REPL commands and help"
 
-idrisTestsAllSchemes : BackendRequirement -> IO TestPool
+idrisTestsAllSchemes : Requirement -> IO TestPool
 idrisTestsAllSchemes cg = testsInDir "allschemes"
       ("Test across all scheme backends: " ++ show cg ++ " instance")
       {codegen = Just cg}
 
-idrisTestsAllBackends : BackendRequirement -> TestPool
+idrisTestsAllBackends : Requirement -> TestPool
 idrisTestsAllBackends cg = MkTestPool
       ("Test across all backends: " ++ show cg ++ " instance")
       [] (Just cg)
        -- RefC implements IEEE standard and distinguishes between 0.0 and -0.0
        -- unlike other backends. So turn this test for now.
-      $ ([ "issue2362" ] <* guard (cg /= C))
-      ++ ([ "popen2" ] <* guard (cg /= Node))
+      $ ([ "issue2362" ] <* guard (cg.name /= "refc"))
+      ++ ([ "popen2" ] <* guard (cg.name /= "node"))
       ++ [ -- Evaluator
        "evaluator004",
        -- Unfortunately the behaviour of Double is platform dependent so the
@@ -186,15 +186,15 @@ templateTests = testsInDir "templates" "Test templates"
 -- that only runs if all backends are
 -- available.
 baseLibraryTests : IO TestPool
-baseLibraryTests = testsInDir' "base" "Base library" [Chez, Node]
+baseLibraryTests = testsInDir "base" "Base library" {requirements = [Chez, Node]}
 
 -- same behavior as `baseLibraryTests`
 contribLibraryTests : IO TestPool
-contribLibraryTests = testsInDir' "contrib" "Contrib library" [Chez, Node]
+contribLibraryTests = testsInDir "contrib" "Contrib library" {requirements = [Chez, Node]}
 
 -- same behavior as `baseLibraryTests`
 linearLibraryTests : IO TestPool
-linearLibraryTests = testsInDir' "linear" "Linear library" [Chez, Node]
+linearLibraryTests = testsInDir "linear" "Linear library" {requirements = [Chez, Node]}
 
 codegenTests : IO TestPool
 codegenTests = testsInDir "codegen" "Code generation"