Closed stefan-hoeck closed 1 year ago
This is now ready. @buzden feel free to tell me what parts of your own elab utilities you'd like to include here. I'll leave this open but plan to merge it tomorrow morning (Europe time), because I plan to add more (but hopefully not breaking) stuff in additional pull requests.
With this breaking change, functionality for deriving
Eq
,Ord
, andShow
(at the least) is added, and some pain points are being fixed. This will potentially break a lot of code, so I plan to do this slowly.Some of the breaking changes include:
Language.Reflection.Syntax.Arg
no longer takes a boolean index: AnArg
can be named or unnamed, but if we require names for binding arguments, we should generate a fresh set of names for all of them.Con
is now indexed over the type constructor's arguments, and a corresponding sequence of applied arguments is extracted from the constructor's return type. A major improvement is, that we thus can also support constructors, whose return types contain named arguments and applied auto-implicits, something that was not possible before.Language.Reflection.Types.Tpe
is a view onTTImp
corresponding in spirit to Haskell 98's kind system. We use this as the basis for reflecting on parameterized data types.Language.Reflection.Type.PArg
, which is indexed over the number of parameters. This enables some special treatment for parameters (constructorPPar
) and allows us to conveniently convert them back toTTImp
in the presence of a vector of parameter names.The following bullet points will need to be addressed before this is being merged:
idris2-sop
to these changes and deprecate deriving ofEq
,Show
, andOrd
therepretty-show
json