[ refactor ] Make argDeps function to be pure, not monadic

buzden · Sep 16, 2024 · 13cbeff · 13cbeff
1 parent 5111134
commit 13cbeff
Show file tree

Hide file tree

Showing 3 changed files with 4 additions and 4 deletions.
diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
@@ -159,7 +159,7 @@ namespace NonObligatoryExts
               `(Prelude.pure {f=Test.DepTyCheck.Gen.Gen _} ~consExpr)
 
       -- Get dependencies of constructor's arguments
-      rawDeps <- argDeps con.args
+      let rawDeps = argDeps con.args
       let deps = downmap ((`difference` givs) . mapIn weakenToSuper) rawDeps
 
       -------------------------------------------------

diff --git a/src/Deriving/DepTyCheck/Util/Reflection.idr b/src/Deriving/DepTyCheck/Util/Reflection.idr
@@ -618,9 +618,9 @@ genTypeName g = do
 ----------------------------------------------
 
 export
-argDeps : Elaboration m => (args : List Arg) -> m $ DVect args.length $ SortedSet . Fin . Fin.finToNat
+argDeps : (args : List Arg) -> DVect args.length $ SortedSet . Fin . Fin.finToNat
 argDeps args = do
   let nameToIndices = SortedMap.fromList $ mapI args $ \i, arg => (argName arg, SortedSet.singleton i)
   let args = Vect.fromList args <&> \arg => allVarNames arg.type |> map (fromMaybe empty . lookup' nameToIndices)
-  pure $ flip upmapI args $ \i, argDeps => flip concatMap argDeps $ \candidates =>
+  flip upmapI args $ \i, argDeps => flip concatMap argDeps $ \candidates =>
     maybe empty singleton $ last' $ mapMaybe tryToFit $ SortedSet.toList candidates
diff --git a/tests/derivation/utils/arg-deps/_common/Infra.idr b/tests/derivation/utils/arg-deps/_common/Infra.idr
@@ -21,7 +21,7 @@ ppTys tys = do
   let tys = unlist tys
   for_ tys $ \expr => do
     let (args, ret) = unPi expr
-    deps <- map SortedSet.toList <$> argDeps args
+    let deps = map SortedSet.toList $ argDeps args
     let expr' = piAll ret $ {piInfo := ExplicitArg} <$> args -- as if all arguments were explicit
     logSugaredTerm "deptycheck.arg-deps" 0 "type        " expr'
     logMsg         "deptycheck.arg-deps" 0 "dependencies: \{show deps}\n"