From ab6c26234d95df2e3d71530cc21f7f39c326b391 Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Sat, 31 Aug 2024 13:42:21 +0300 Subject: [PATCH] [ derive ] Support printing derived gens with Idris representation --- src/Deriving/DepTyCheck/Gen/Entry.idr | 5 +++-- 1 file changed, 3 insertions(+), 2 deletions(-) diff --git a/src/Deriving/DepTyCheck/Gen/Entry.idr b/src/Deriving/DepTyCheck/Gen/Entry.idr index 299598bc7..7ff973b99 100644 --- a/src/Deriving/DepTyCheck/Gen/Entry.idr +++ b/src/Deriving/DepTyCheck/Gen/Entry.idr @@ -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 "" ]