From d0501572ba84b226acfbb19a4b27a7c1bffdaad6 Mon Sep 17 00:00:00 2001
From: Denis Buzdalov <public@buzden.ru>
Date: Fri, 16 Aug 2024 23:34:11 +0300
Subject: [PATCH] [ derive ] Log used order using argument names too

---
 src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr |  9 +++++++--
 src/Deriving/DepTyCheck/Util/Reflection.idr     | 10 ++++++++++
 2 files changed, 17 insertions(+), 2 deletions(-)

diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
index 2dbe763da..8e134f159 100644
--- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
+++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
@@ -42,7 +42,12 @@ namespace NonObligatoryExts
   [LeastEffort] {default False simplificationHack : Bool} -> ConstructorDerivator where
     consGenExpr sig con givs fuel = do
 
-      let niit : NamesInfoInTypes = %search    -- I don't why it won't be found without this
+      -- Prepare local search context
+      let _ : NamesInfoInTypes = %search    -- I don't why it won't be found without this
+      let _ : ({0 f : _} -> Foldable f => Interpolation $ f _) = WithNames {con}
+
+      -- Log all arguments' position and their names (if they have some)
+      logPoint {level=15} "least-effort" [sig, con] "- con args: \{List.allFins con.args.length}"
 
       -------------------------------------------------------------
       -- Prepare intermediate data and functions using this data --
@@ -199,7 +204,7 @@ namespace NonObligatoryExts
       let allOrders = List.nub $ nub <$> allOrders
 
       for_ allOrders $ \order =>
-        logPoint {level=10} "least-effort.order" [sig, con] "- one of used final orders: \{show order}"
+        logPoint {level=10} "least-effort" [sig, con] "- used final order: \{order}"
 
       --------------------------
       -- Producing the result --
diff --git a/src/Deriving/DepTyCheck/Util/Reflection.idr b/src/Deriving/DepTyCheck/Util/Reflection.idr
index f2329f4a1..374fb89bf 100644
--- a/src/Deriving/DepTyCheck/Util/Reflection.idr
+++ b/src/Deriving/DepTyCheck/Util/Reflection.idr
@@ -56,6 +56,16 @@ SingleLogPosition Con where
     let fullName' = unpack fullName
     maybe fullName (pack . flip drop fullName' . S . finToNat) $ findLastIndex (== '.') fullName'
 
+export
+[WithName] {con : Con} -> Interpolation (Fin con.args.length) where
+  interpolate i = case name $ index' con.args i of
+    Just (UN n) => "#\{show i} (\{show n})"
+    _           => "#\{show i}"
+
+export
+[WithNames] {con : Con} -> Foldable f => Interpolation (f $ Fin con.args.length) where
+  interpolate = ("[" ++) . (++ "]") . joinBy ", " . map (interpolate @{WithName}) . toList
+
 ----------------------------------------------
 --- Compiler-based `TTImp` transformations ---
 ----------------------------------------------