diff --git a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr index 58b43e0b6..acd204c18 100644 --- a/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr +++ b/src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr @@ -238,7 +238,7 @@ namespace NonObligatoryExts let theOrder = searchOrder $ removeDeeply givs determ - logPoint {level=10} "least-effort.order" [sig, con] "- used final order: \{show theOrder}" + logPoint {level=10} "least-effort.order" [sig, con] "- used final order: \{interpolate @{WithNames} theOrder}" labelGen "\{show con.name} (orders)".label <$> genForOrder theOrder diff --git a/src/Deriving/DepTyCheck/Util/Reflection.idr b/src/Deriving/DepTyCheck/Util/Reflection.idr index f2329f4a1..c6f1bec05 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 + Nothing => "#\{show i}" + Just n => "\{show n} (#\{show i})" + +export +[WithNames] {con : Con} -> Foldable f => Interpolation (f $ Fin con.args.length) where + interpolate xs = joinBy ", " $ toList xs <&> interpolate @{WithName} + ---------------------------------------------- --- Compiler-based `TTImp` transformations --- ----------------------------------------------