[ deriving ] Try to reduce a type before searching it's showable

This commit is contained in:
Denis Buzdalov 2023-10-28 15:37:13 +03:00 committed by G. Allais
parent bee59d5fde
commit 64ad807f83
3 changed files with 21 additions and 0 deletions

View File

@ -245,6 +245,8 @@ namespace Show
let MW = rig let MW = rig
| _ => throwError (NotAnUnconstrainedValue rig) | _ => throwError (NotAnUnconstrainedValue rig)
-- try to reduce the type before analysis
ty <- try (check {expected=Type} ty >>= \x => quote x) (pure ty)
res <- withError (WhenCheckingArg (mapTTImp cleanup ty)) $ do res <- withError (WhenCheckingArg (mapTTImp cleanup ty)) $ do
typeView f (paraz <>> []) ty typeView f (paraz <>> []) ty
pure $ Just (showPrecFun fc mutualWith res v) pure $ Just (showPrecFun fc mutualWith res v)

View File

@ -192,3 +192,17 @@ namespace EqMap
eqMap : (eq : Eq key) => Show key => Show val => Show (EqMap key @{eq} val) eqMap : (eq : Eq key) => Show key => Show val => Show (EqMap key @{eq} val)
eqMap = %runElab derive eqMap = %runElab derive
namespace Reducible
Y : Bool -> Type
Y True = Bool
Y False = Nat
data X : Type where
X0 : X
X1 : Bool -> X
X2 : Y True -> Y False -> X
x : Show X
x = %runElab derive

View File

@ -83,6 +83,11 @@ LOG derive.show.assumption:10: I am assuming that the parameter val can be shown
LOG derive.show.clauses:1: LOG derive.show.clauses:1:
showPrecEqMap : {0 key : _} -> Show key => {0 eq, val : _} -> Show val => Prec -> EqMap key {{conArg:5125} = eq} val -> String showPrecEqMap : {0 key : _} -> Show key => {0 eq, val : _} -> Show val => Prec -> EqMap key {{conArg:5125} = eq} val -> String
showPrecEqMap d (MkEqMap x0) = showCon d "MkEqMap" (showArg x0) showPrecEqMap d (MkEqMap x0) = showCon d "MkEqMap" (showArg x0)
LOG derive.show.clauses:1:
showPrecX : Prec -> X -> String
showPrecX d X0 = "X0"
showPrecX d (X1 x0) = showCon d "X1" (showArg x0)
showPrecX d (X2 x0 x1) = showCon d "X2" (concat ((showArg x0) :: ((showArg x1) :: Nil)))
DeriveShow> "Lam (Call Add ((::) (Var Nothing) ((::) (Var (Just ())) Nil)))" DeriveShow> "Lam (Call Add ((::) (Var Nothing) ((::) (Var (Just ())) Nil)))"
DeriveShow> DeriveShow>
Bye for now! Bye for now!