Skip to content

Commit

Permalink
[ derive ] Support printing derived gens with Idris representation
Browse files Browse the repository at this point in the history
  • Loading branch information
buzden committed Aug 31, 2024
1 parent 1e06f50 commit e60d370
Showing 1 changed file with 3 additions and 2 deletions.
5 changes: 3 additions & 2 deletions src/Deriving/DepTyCheck/Gen/Entry.idr
Original file line number Diff line number Diff line change
Expand Up @@ -374,15 +374,16 @@ deriveGenFor a = do

||| Declares `main : IO Unit` function that prints derived generator for the given generator's signature
export
deriveGenPrinter : DerivatorCore => Type -> Elab Unit
deriveGenPrinter : {default True printTTImp : Bool} -> DerivatorCore => Type -> Elab Unit
deriveGenPrinter ty = do
ty <- quote ty
logSugaredTerm "deptycheck.derive.print" DefaultLogLevel "type" ty
expr <- deriveGenExpr ty
expr <- quote expr
printTTImp <- quote printTTImp
declare `[
main : IO Unit
main = do
putStr $ interpolate ~(expr)
putStr $ if ~printTTImp then interpolate ~expr else show ~expr
putStrLn ""
]

0 comments on commit e60d370

Please sign in to comment.