Skip to content

Commit

Permalink
[ derive ] Log used order using argument names too
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Aug 20, 2024
1 parent f5c0758 commit d050157
Show file tree
Hide file tree
Showing 2 changed files with 17 additions and 2 deletions.
9 changes: 7 additions & 2 deletions src/Deriving/DepTyCheck/Gen/Core/ConsDerive.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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 --
Expand Down Expand Up @@ -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 --
Expand Down
10 changes: 10 additions & 0 deletions src/Deriving/DepTyCheck/Util/Reflection.idr
Original file line number Diff line number Diff line change
Expand Up @@ -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 ---
----------------------------------------------
Expand Down

0 comments on commit d050157

Please sign in to comment.