idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-09-20 01:37:35 +03:00
Code Issues Projects Releases Wiki Activity

[ new ] deriving Show (#2741)

Browse Source
This commit is contained in:
G. Allais 2022-11-02 11:57:07 +00:00 committed by GitHub
parent 078445b178
commit 4cd38a8c5d
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
17 changed files with 694 additions and 53 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

25
libs/base/Data/SnocList.idr
View File

@ -156,6 +156,31 @@ findIndex p (xs :< x) = if p x
then Just FZ
else FS <$> findIndex p xs
---------------------------
-- Zippable --
---------------------------
public export
Zippable SnocList where
zipWith _ [<] _ = [<]
zipWith _ _ [<] = [<]
zipWith f (xs :< x) (ys :< y) = zipWith f xs ys :< f x y
zipWith3 _ [<] _ _ = [<]
zipWith3 _ _ [<] _ = [<]
zipWith3 _ _ _ [<] = [<]
zipWith3 f (xs :< x) (ys :< y) (zs :< z) = zipWith3 f xs ys zs :< f x y z
unzipWith f [<] = ([<], [<])
unzipWith f (xs :< x) = let (bs, cs) = unzipWith f xs
(b, c) = f x
in (bs :< b, cs :< c)
unzipWith3 f [<] = ([<], [<], [<])
unzipWith3 f (xs :< x) = let (bs, cs, ds) = unzipWith3 f xs
(b, c, d) = f x
in (bs :< b, cs :< c, ds :< d)
------------------
--- Properties ---
------------------

53
libs/base/Deriving/Common.idr
View File

@ -1,5 +1,6 @@
module Deriving.Common
import Data.SnocList
import Language.Reflection
%default total
@ -64,7 +65,7 @@ isType : Elaboration m => TTImp -> m IsType
isType = go Z [] where
go : Nat -> List (Argument Name, Nat) -> TTImp -> m IsType
go idx acc (IVar _ n) = MkIsType n acc <$> isTypeCon n
go idx acc (IVar _ n) = MkIsType n (map (map (minus idx . S)) acc) <$> isTypeCon n
go idx acc (IApp _ t (IVar _ nm)) = case nm of
-- Unqualified: that's a local variable
UN (Basic _) => go (S idx) ((Arg emptyFC nm, idx) :: acc) t
@ -86,8 +87,7 @@ isType = go Z [] where
public export
record ConstructorView where
constructor MkConstructorView
params : List Name
functorPara : Name
params : SnocList (Name, Nat)
conArgTypes : List (Count, Argument TTImp)
export
@ -98,13 +98,13 @@ constructorView (IPi fc rig pinfo x a b) = do
let True = rig /= M1
| False => constructorView b -- this better be another boring argument...
{ conArgTypes $= ((rig, arg) ::) } <$> constructorView b
constructorView (IApp _ f (IVar _ a)) = do
constructorView f = do
MkAppView _ ts _ <- appView f
let ps = flip mapMaybe ts $ \ t => the (Maybe Name) $ case t of
Arg _ (IVar _ nm) => Just nm
let range = [<] <>< [0..minus (length ts) 1]
let ps = flip mapMaybe (zip ts range) $ \ t => the (Maybe (Name, Nat)) $ case t of
(Arg _ (IVar _ nm), n) => Just (nm, n)
_ => Nothing
pure (MkConstructorView (ps <>> []) a [])
constructorView _ = Nothing
pure (MkConstructorView ps [])
------------------------------------------------------------------------------
-- Satisfying an interface
@ -131,6 +131,32 @@ withParams fc params nms t = go nms where
$ addConstraint (params pos) nm
$ go nms
||| Type of proofs that something has a given type
export
data HasType : (nm : Name) -> (ty : TTImp) -> Type where
TrustMeHT : HasType nm ty
export
hasType : Elaboration m => (nm : Name) ->
m (Maybe (ty : TTImp ** HasType nm ty))
hasType nm = catch $ do
[(_, ty)] <- getType nm
| _ => fail "Ambiguous name"
pure (ty ** TrustMeHT)
||| Type of proofs that a type is inhabited
export
data IsProvable : (ty : TTImp) -> Type where
TrustMeIP : IsProvable ty
export
isProvable : Elaboration m => (ty : TTImp) ->
m (Maybe (IsProvable ty))
isProvable ty = catch $ do
ty <- check {expected = Type} ty
ignore $ check {expected = ty} `(%search)
pure TrustMeIP
||| Type of proofs that a type satisfies a constraint.
||| Internally it's vacuous. We don't export the constructor so
||| that users cannot manufacture buggy proofs.
@ -196,14 +222,3 @@ freshName ns a = assert_total $ go (basicNames ns) Nothing where
go ns mi =
let nm = a ++ maybe "" show mi in
ifThenElse (nm `elem` ns) (go ns (Just $ maybe 0 S mi)) nm
------------------------------------------------------------------------------
-- TODO: move to Data.List?
export
elemPos : Eq a => a -> List a -> Maybe Nat
elemPos x = go 0 where
go : Nat -> List a -> Maybe Nat
go idx [] = Nothing
go idx (y :: ys) = idx <$ guard (x == y) <|> go (S idx) ys

11
libs/base/Deriving/Foldable.idr
View File

@ -143,7 +143,7 @@ parameters
{auto error : MonadError Error m}
{auto cs : MonadState Parameters m}
(t : Name)
(ps : List Name)
(ps : List (Name, Nat))
(x : Name)
||| When analysing the type of a constructor for the type family t,
@ -161,7 +161,7 @@ parameters
fromTypeView (Left prf) = prf
fromTypeView (Right fo) = FIFree fo
||| Hoping to observe that ty is functorial
||| Hoping to observe that ty is foldable
export
typeView : (ty : TTImp) -> m (TypeView ty)
@ -187,7 +187,7 @@ parameters
Yes Refl => pure $ Left (FIRec prf sp)
No diff => case !(hasImplementation Foldable f) of
Just prf => pure (Left (FIFold isFO prf sp))
Nothing => case hd `elemPos` ps of
Nothing => case lookup hd ps of
Just n => do
-- record that the nth parameter should be functorial
ns <- gets asFoldables
@ -220,7 +220,7 @@ parameters
Nothing => do
let Just (MkAppView (_, hd) ts prf) = appView f
| _ => throwError (NotAnApplication f)
case hd `elemPos` ps of
case lookup hd ps of
Just n => do
-- record that the nth parameter should be bifoldable
ns <- gets asBifoldables
@ -335,8 +335,9 @@ namespace Foldable
(ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
withError (WhenCheckingConstructor cName) $ do
-- Grab the types of the constructor's explicit arguments
let Just (MkConstructorView paras para args) = constructorView ty
let Just (MkConstructorView (paraz :< (para, _)) args) = constructorView ty
| _ => throwError ConfusingReturnType
let paras = paraz <>> []
logMsg "derive.foldable.clauses" 10 $
"\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
let vars = map (map (IVar fc . un . ("x" ++) . show . (`minus` 1)))

14
libs/base/Deriving/Functor.idr
View File

@ -132,7 +132,7 @@ parameters
{auto error : MonadError Error m}
{auto cs : MonadState Parameters m}
(t : Name)
(ps : List Name)
(ps : List (Name, Nat))
(x : Name)
||| When analysing the type of a constructor for the type family t,
@ -178,7 +178,7 @@ parameters
Negative => throwError (NegativeOccurrence t (IApp fc f arg))
No diff => case !(hasImplementation Functor f) of
Just prf => pure (Left (FIFun isFO prf sp))
Nothing => case hd `elemPos` ps of
Nothing => case lookup hd ps of
Just n => do
-- record that the nth parameter should be functorial
ns <- gets asFunctors
@ -222,7 +222,7 @@ parameters
Nothing => do
let Just (MkAppView (_, hd) ts prf) = appView f
| _ => throwError (NotAnApplication f)
case hd `elemPos` ps of
case lookup hd ps of
Just n => do
-- record that the nth parameter should be bifunctorial
ns <- gets asBifunctors
@ -345,8 +345,9 @@ namespace Functor
(ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
withError (WhenCheckingConstructor cName) $ do
-- Grab the types of the constructor's explicit arguments
let Just (MkConstructorView paras para args) = constructorView ty
let Just (MkConstructorView (paraz :< (para, _)) args) = constructorView ty
| _ => throwError ConfusingReturnType
let paras = paraz <>> []
logMsg "derive.functor.clauses" 10 $
"\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
let vars = map (map (IVar fc . un . ("x" ++) . show . (`minus` 1)))
@ -376,6 +377,11 @@ namespace Functor
let b = un $ freshName paramNames "b"
let va = IVar fc a
let vb = IVar fc b
logMsg "derive.functor.parameters" 20 $ unlines
[ "Functors: \{show ns.asFunctors}"
, "Bifunctors: \{show ns.asBifunctors}"
, "Parameters: \{show (map (mapFst unArg) params)}"
]
let ty = MkTy fc fc mapName $ withParams fc (paramConstraints ns) params
$ IPi fc M0 ImplicitArg (Just a) (IType fc)
$ IPi fc M0 ImplicitArg (Just b) (IType fc)

293
libs/base/Deriving/Show.idr Normal file
View File

@ -0,0 +1,293 @@
||| Deriving show instances using reflection
||| You can for instance define:
||| ```
||| data Tree a = Leaf a | Node (Tree a) (Tree a)
||| treeShow : Show a => Show (Tree a)
||| treeShow = %runElab derive
||| ```
module Deriving.Show
import public Control.Monad.Either
import public Control.Monad.State
import public Data.Maybe
import public Decidable.Equality
import public Language.Reflection
import public Deriving.Common
%language ElabReflection
%default total
public export
fromShowPrec :
(Prec -> ty -> String) ->
Show ty
fromShowPrec sp = MkShow (sp Open) sp
------------------------------------------------------------------------------
-- Errors
||| Possible errors for the functor-deriving machinery.
public export
data Error : Type where
NotAShowable : Name -> Error
UnsupportedType : TTImp -> Error
NotAFiniteStructure : Error
NotAnUnconstrainedValue : Count -> Error
InvalidGoal : Error
ConfusingReturnType : Error
-- Contextual information
WhenCheckingConstructor : Name -> Error -> Error
WhenCheckingArg : TTImp -> Error -> Error
export
Show Error where
show = joinBy "\n" . go [<] where
go : SnocList String -> Error -> List String
go acc (NotAShowable nm) = acc <>> ["Couldn't find a `Show' instance for the type \{show nm}"]
go acc (UnsupportedType s) = acc <>> ["Unsupported type \{show s}"]
go acc NotAFiniteStructure = acc <>> ["Cannot show an infinite structure"]
go acc (NotAnUnconstrainedValue rig) = acc <>> ["Cannot show a \{enunciate rig} value"]
go acc InvalidGoal = acc <>> ["Expected a goal of the form `Show t`"]
go acc ConfusingReturnType = acc <>> ["Confusing telescope"]
go acc (WhenCheckingConstructor nm err) = go (acc :< "When checking constructor \{show nm}") err
go acc (WhenCheckingArg s err) = go (acc :< "When checking argument of type \{show s}") err
record Parameters where
constructor MkParameters
asShowables : List Nat
initParameters : Parameters
initParameters = MkParameters []
paramConstraints : Parameters -> Nat -> Maybe TTImp
paramConstraints params pos
= IVar emptyFC `{Prelude.Show.Show} <$ guard (pos `elem` params.asShowables)
------------------------------------------------------------------------------
-- Core machinery: being showable
ShowN : TTImp -> Name -> TTImp
ShowN ty nm = go (IVar emptyFC nm) ty Z where
go : TTImp -> TTImp -> Nat -> TTImp
go acc (IPi _ _ pinfo mn (IType _) ty) n
= let var = MN "__param" (cast n) in
IPi emptyFC M0 ImplicitArg (Just var) (Implicit emptyFC False)
$ IPi emptyFC MW AutoImplicit Nothing (IApp emptyFC `(Show) (IVar emptyFC var))
$ go (TTImp.apply acc (toList (fromPiInfo emptyFC pinfo mn (IVar emptyFC var)))) ty (S n)
go acc (IPi _ _ pinfo mn _ ty) n
= let var = MN "__param" (cast n) in
IPi emptyFC M0 ImplicitArg (Just var) (Implicit emptyFC False)
$ go (TTImp.apply acc (toList (fromPiInfo emptyFC pinfo mn (IVar emptyFC var)))) ty (S n)
go acc _ _ = IApp emptyFC `(Show) acc
||| IsShowable is parametrised by
||| @ t the name of the data type whose constructors are being analysed
||| @ ty the type being analysed
||| The inductive type delivers a proof that ty can be shown,
||| assuming that t also is showable.
public export
data IsShowable : (t : Name) -> (ty : TTImp) -> Type
data IsShowableArgs : (t : Name) -> (tconty : TTImp) -> (ty : List (Argument TTImp)) -> Type
data IsShowable : (t : Name) -> (ty : TTImp) -> Type where
||| The subterm is delayed (Lazy only, we can't traverse infinite structures)
ISDelayed : IsShowable t ty -> IsShowable t (IDelayed fc LLazy ty)
||| There is a recursive subtree of type (t a1 ... an)
ISRec : (0 _ : IsAppView (_, t) _ ty) -> IsShowable t ty
||| There are nested subtrees somewhere inside a 3rd party type constructor
||| which satisfies the Show interface
ISShowN : (0 _ : IsAppView (_, tcon) args ty) ->
HasType tcon tconty ->
IsProvable (ShowN tconty tcon) ->
IsShowableArgs t tconty (args <>> []) -> IsShowable t ty
||| Or we could be referring to one of the parameters
ISParam : IsShowable t ty
||| A primitive type is trivially Showable
ISPrim : (ty : PrimType) -> IsShowable t (IPrimVal fc (PrT ty))
data IsShowableArgs : (t : Name) -> (tconty : TTImp) -> (ty : List (Argument TTImp)) -> Type where
Done : IsShowableArgs t tconty []
Step : IsShowable t (unArg arg) -> IsShowableArgs t ty args ->
IsShowableArgs t (IPi fc1 r ExplicitArg mn (IType fc2) ty) (arg :: args)
Drop : (forall fc. Not (dom === IType fc)) -> IsShowableArgs t ty args ->
IsShowableArgs t (IPi fc1 r ExplicitArg mn dom ty) (arg :: args)
Skip : Not (pinfo === ExplicitArg) -> IsShowableArgs t ty args ->
IsShowableArgs t (IPi fc1 r pinfo mn dom ty) args -- TODO: constrain more?
parameters (fc : FC) (mutualWith : List Name)
isRecs : IsShowableArgs t ty ts -> Bool
isRec : IsShowable t ts -> Bool
isRecs Done = False
isRecs (Step x xs) = isRec x || isRecs xs
isRecs (Drop f xs) = isRecs xs
isRecs (Skip f xs) = isRecs xs
isRec (ISDelayed x) = isRec x
isRec (ISRec _) = True
isRec (ISShowN _ _ _ xs) = isRecs xs
isRec ISParam = False
isRec (ISPrim _) = False
showPrecFun : {ty : _} -> IsShowable t ty -> TTImp -> TTImp
showPrecFun (ISDelayed p) t = showPrecFun p (IForce (getFC t) t)
showPrecFun (ISRec _) t = IApp emptyFC `(assert_total) (IApp emptyFC `(showArg) t)
showPrecFun {ty} (ISShowN _ _ _ as) t
= let isMutual = fromMaybe False (appView ty >>= \ v => pure (snd v.head `elem` mutualWith)) in
ifThenElse (isMutual || isRecs as) (IApp emptyFC `(assert_total)) id
$ IApp emptyFC `(showArg) t
showPrecFun ISParam t = IApp emptyFC `(showArg) t
showPrecFun (ISPrim pty) t = IApp emptyFC `(showArg) t
parameters
{0 m : Type -> Type}
{auto elab : Elaboration m}
{auto error : MonadError Error m}
{auto cs : MonadState Parameters m}
(t : Name)
(ps : List (Name, Nat))
||| Hoping to observe that ty can be shown
export
typeView : (ty : TTImp) -> m (IsShowable t ty)
typeViews : (tconty : TTImp) -> (tys : List (Argument TTImp)) ->
m (IsShowableArgs t tconty tys)
typeView (IDelayed _ lz ty) = case lz of
LLazy => ISDelayed <$> typeView ty
_ => throwError NotAFiniteStructure
typeView (IPrimVal _ (PrT ty)) = pure (ISPrim ty)
typeView ty = do
let Just (MkAppView (_, hd) ts prf) = appView ty
| _ => throwError (UnsupportedType ty)
let No _ = decEq hd t
| Yes Refl => pure (ISRec prf)
Just (hdty ** hT) <- hasType hd
| _ => case lookup hd ps <* guard (null ts) of
Just n => do
-- record that the nth parameter should be showable
ns <- gets asShowables
let ns = ifThenElse (n `elem` ns) ns (n :: ns)
modify { asShowables := ns }
-- and happily succeed
logMsg "derive.show.assumption" 10 $
"I am assuming that the parameter \{show hd} can be shown"
pure ISParam
_ => throwError (UnsupportedType ty)
Just iP <- isProvable (ShowN hdty hd)
| _ => throwError (NotAShowable hd)
ISShowN prf hT iP <$> typeViews hdty (ts <>> [])
typeViews _ [] = pure Done
typeViews (IPi _ _ ExplicitArg _ (IType fc) ty) (t :: ts)
= Step <$> assert_total (typeView (unArg t)) <*> typeViews ty ts
typeViews (IPi _ _ ExplicitArg _ dom ty) (t :: ts)
= Drop (\ x => believe_me x) <$> typeViews ty ts
typeViews (IPi _ _ _ _ _ ty) ts
= Skip (\ x => believe_me x) <$> typeViews ty ts
typeViews ty ts = throwError (UnsupportedType ty)
namespace Show
derive' : (Elaboration m, MonadError Error m) =>
{default Private vis : Visibility} ->
{default Total treq : TotalReq} ->
{default [] mutualWith : List Name} ->
m (Show f)
derive' = do
-- expand the mutualwith names to have the internal, fully qualified, names
mutualWith <- map concat $ for mutualWith $ \ nm => do
ntys <- getType nm
pure (fst <$> ntys)
-- The goal should have the shape (Show t)
Just (IApp _ (IVar _ showable) t) <- goal
| _ => throwError InvalidGoal
when (`{Prelude.Show.Show} /= showable) $
logMsg "derive.show" 1 "Expected to derive Show but got \{show showable}"
-- t should be a type constructor
logMsg "derive.show" 1 "Deriving Show for \{showPrec App $ mapTTImp cleanup t}"
MkIsType f params cs <- isType t
logMsg "derive.show.constructors" 1 $
joinBy "\n" $ "" :: map (\ (n, ty) => " \{showPrefix True $ dropNS n} : \{show $ mapTTImp cleanup ty}") cs
-- Generate a clause for each data constructor
let fc = emptyFC
let un = UN . Basic
let showName = un ("showPrec" ++ show (dropNS f))
let precName = un "d"
let prec = IVar fc precName
(ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
withError (WhenCheckingConstructor cName) $ do
-- Grab the types of the constructor's explicit arguments
let Just (MkConstructorView paraz args) = constructorView ty
| _ => throwError ConfusingReturnType
logMsg "derive.show.clauses" 10 $
"\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
-- Only keep the visible arguments
let args = mapMaybe (bitraverse pure (map snd . isExplicit)) args
-- Special case for constructors with no argument
let (_ :: _) = args
| [] => pure $ PatClause fc
(apply fc (IVar fc showName) [ prec, IVar fc cName])
(IPrimVal fc (Str (showPrefix True (dropNS cName))))
let vars = zipWith (const . IVar fc . un . ("x" ++) . show . (`minus` 1)) [1..length args] args
recs <- for (zip vars args) $ \ (v, (rig, ty)) => do
let MW = rig
| _ => throwError (NotAnUnconstrainedValue rig)
res <- withError (WhenCheckingArg (mapTTImp cleanup ty)) $ do
typeView f (paraz <>> []) ty
pure $ Just (showPrecFun fc mutualWith res v)
let args = catMaybes recs
let asList = foldr (\ a, as => apply fc (IVar fc `{Prelude.(::)}) [a,as]) `(Prelude.Nil)
pure $ PatClause fc
(apply fc (IVar fc showName) [ prec, apply fc (IVar fc cName) vars])
(apply fc (IVar fc (un "showCon"))
[ prec
, IPrimVal fc (Str (showPrefix True (dropNS cName)))
, case args of
[a] => a
_ => IApp fc (IVar fc (un "concat")) (asList args)
])
-- Generate the type of the show function
let ty = MkTy fc fc showName $ withParams fc (paramConstraints ns) params
$ `(Prec -> ~(t) -> String)
logMsg "derive.show.clauses" 1 $
joinBy "\n" ("" :: (" " ++ show (mapITy cleanup ty))
:: map ((" " ++) . showClause InDecl . mapClause cleanup) cls)
-- Define the instance
check $ ILocal fc
[ IClaim fc MW vis [Totality treq] ty
, IDef fc showName cls
] `(fromShowPrec ~(IVar fc showName))
||| Derive an implementation of Show for a type constructor.
||| This can be used like so:
||| ```
||| data Tree a = Leaf a | Node (Tree a) (Tree a)
||| treeShow : Show a => Show (Tree a)
||| treeShow = %runElab derive
||| ```
export
derive : {default Private vis : Visibility} ->
{default Total treq : TotalReq} ->
{default [] mutualWith : List Name} ->
Elab (Show f)
derive = do
res <- runEitherT {e = Error, m = Elab} (derive' {vis, treq, mutualWith})
case res of
Left err => fail (show err)
Right prf => pure prf

13
libs/base/Deriving/Traversable.idr
View File

@ -89,7 +89,7 @@ isFreeOf' x ty = case isFreeOf x ty of
||| @ t the name of the data type whose constructors are being analysed
||| @ x the name of the type variable that the traversable action will act on
||| @ ty the type being analysed
||| The inductive type delivers a proof that x can be folded over in ty,
||| The inductive type delivers a proof that x can be traversed over in ty,
||| assuming that t also is traversable.
public export
data IsTraversableIn : (t, x : Name) -> (ty : TTImp) -> Type where
@ -122,7 +122,7 @@ parameters
{auto error : MonadError Error m}
{auto cs : MonadState Parameters m}
(t : Name)
(ps : List Name)
(ps : List (Name, Nat))
(x : Name)
||| When analysing the type of a constructor for the type family t,
@ -140,7 +140,7 @@ parameters
fromTypeView (Left prf) = prf
fromTypeView (Right fo) = TIFree fo
||| Hoping to observe that ty is functorial
||| Hoping to observe that ty is traversable
export
typeView : (ty : TTImp) -> m (TypeView ty)
@ -166,7 +166,7 @@ parameters
Yes Refl => pure $ Left (TIRec prf sp)
No diff => case !(hasImplementation Traversable f) of
Just prf => pure (Left (TIFold isFO prf sp))
Nothing => case hd `elemPos` ps of
Nothing => case lookup hd ps of
Just n => do
-- record that the nth parameter should be functorial
ns <- gets asTraversables
@ -199,7 +199,7 @@ parameters
Nothing => do
let Just (MkAppView (_, hd) ts prf) = appView f
| _ => throwError (NotAnApplication f)
case hd `elemPos` ps of
case lookup hd ps of
Just n => do
-- record that the nth parameter should be bitraversable
ns <- gets asBitraversables
@ -359,8 +359,9 @@ namespace Traversable
(ns, cls) <- runStateT {m = m} initParameters $ for cs $ \ (cName, ty) =>
withError (WhenCheckingConstructor cName) $ do
-- Grab the types of the constructor's explicit arguments
let Just (MkConstructorView paras para args) = constructorView ty
let Just (MkConstructorView (paraz :< (para, _)) args) = constructorView ty
| _ => throwError ConfusingReturnType
let paras = paraz <>> []
logMsg "derive.traversable.clauses" 10 $
"\{showPrefix True (dropNS cName)} (\{joinBy ", " (map (showPrec Dollar . mapTTImp cleanup . unArg . snd) args)})"
let vars = map (map (IVar fc . un . ("x" ++) . show . (`minus` 1)))

1
libs/base/base.ipkg
View File

@ -88,6 +88,7 @@ modules = Control.App,
Deriving.Common,
Deriving.Foldable,
Deriving.Functor,
Deriving.Show,
Deriving.Traversable,
Decidable.Decidable,

8
tests/base/deriving_foldable/DeriveFoldable.idr
View File

@ -171,16 +171,16 @@ namespace MaybeT
namespace TreeT
data TreeT : (Type -> Type -> Type) -> Type -> Type where
MkTreeT : layer a (TreeT layer a) -> TreeT layer a
data TreeT : (lbl : Type) -> (Type -> Type -> Type) -> Type -> Type where
MkTreeT : lbl -> layer a (TreeT lbl layer a) -> TreeT lbl layer a
%hint
treeT : Bifoldable layer => Foldable (TreeT layer)
treeT : Bifoldable layer => Foldable (TreeT lbl layer)
treeT = %runElab derive {treq = CoveringOnly}
record Tree (a : Type) where
constructor MkTree
runTree : TreeT Either a
runTree : TreeT () Either a
tree : Foldable Tree
tree = %runElab derive {treq = CoveringOnly}

6
tests/base/deriving_foldable/expected
View File

@ -56,8 +56,8 @@ LOG derive.foldable.clauses:1:
foldMapMaybeT f (MkMaybeT x2) = foldMap (foldMap f) x2
LOG derive.foldable.assumption:10: I am assuming that the parameter layer is a Bifoldable
LOG derive.foldable.clauses:1:
foldMapTreeT : {0 layer : _} -> Bifoldable layer => {0 a, b : Type} -> Monoid b => (a -> b) -> TreeT layer a -> b
foldMapTreeT f (MkTreeT x2) = bifoldMap f (foldMapTreeT f) x2
foldMapTreeT : {0 lbl, layer : _} -> Bifoldable layer => {0 a, b : Type} -> Monoid b => (a -> b) -> TreeT lbl layer a -> b
foldMapTreeT f (MkTreeT x3 x4) = bifoldMap f (foldMapTreeT f) x4
LOG derive.foldable.clauses:1:
foldMapTree : {0 a, b : Type} -> Monoid b => (a -> b) -> Tree a -> b
foldMapTree f (MkTree x1) = foldMap f x1
@ -65,7 +65,7 @@ LOG derive.foldable.clauses:1:
foldMapIVect : {0 m : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> IVect {n = m} a -> b
foldMapIVect f (MkIVect x2) = foldMap f x2
LOG derive.foldable.clauses:1:
foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5682} = eq} a -> b
foldMapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> EqMap key {{conArg:5707} = eq} a -> b
foldMapEqMap f (MkEqMap x3) = foldMap (foldMap f) x3
LOG derive.foldable.clauses:1:
foldMapTree : {0 l : _} -> {0 a, b : Type} -> Monoid b => (a -> b) -> Tree l a -> b

8
tests/base/deriving_functor/DeriveFunctor.idr
View File

@ -167,16 +167,16 @@ namespace MaybeT
namespace TreeT
data TreeT : (Type -> Type -> Type) -> Type -> Type where
MkTreeT : layer a (TreeT layer a) -> TreeT layer a
data TreeT : (lbl : Type) -> (Type -> Type -> Type) -> Type -> Type where
MkTreeT : lbl -> layer a (TreeT lbl layer a) -> TreeT lbl layer a
%hint
treeT : Bifunctor layer => Functor (TreeT layer)
treeT : Bifunctor layer => Functor (TreeT lbl layer)
treeT = %runElab derive {treq = CoveringOnly}
record Tree (a : Type) where
constructor MkTree
runTree : TreeT Either a
runTree : TreeT () Either a
tree : Functor Tree
tree = %runElab derive {treq = CoveringOnly}

14
tests/base/deriving_functor/expected
View File

@ -66,8 +66,8 @@ LOG derive.functor.clauses:1:
mapMaybeT f (MkMaybeT x2) = MkMaybeT (map (map f) x2)
LOG derive.functor.assumption:10: I am assuming that the parameter layer is a Bifunctor
LOG derive.functor.clauses:1:
mapTreeT : {0 layer : _} -> Bifunctor layer => {0 a, b : Type} -> (a -> b) -> TreeT layer a -> TreeT layer b
mapTreeT f (MkTreeT x2) = MkTreeT (bimap f (mapTreeT f) x2)
mapTreeT : {0 lbl, layer : _} -> Bifunctor layer => {0 a, b : Type} -> (a -> b) -> TreeT lbl layer a -> TreeT lbl layer b
mapTreeT f (MkTreeT x3 x4) = MkTreeT x3 (bimap f (mapTreeT f) x4)
LOG derive.functor.clauses:1:
mapTree : {0 a, b : Type} -> (a -> b) -> Tree a -> Tree b
mapTree f (MkTree x1) = MkTree (map f x1)
@ -75,20 +75,20 @@ LOG derive.functor.clauses:1:
mapIVect : {0 m : _} -> {0 a, b : Type} -> (a -> b) -> IVect {n = m} a -> IVect {n = m} b
mapIVect f (MkIVect x2) = MkIVect (map f x2)
LOG derive.functor.clauses:1:
mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5665} = eq} a -> EqMap key {{conArg:5665} = eq} b
mapEqMap : {0 key, eq : _} -> {0 a, b : Type} -> (a -> b) -> EqMap key {{conArg:5692} = eq} a -> EqMap key {{conArg:5692} = eq} b
mapEqMap f (MkEqMap x3) = MkEqMap (map (map f) x3)
LOG derive.functor.clauses:1:
mapCont : {0 r : _} -> {0 a, b : Type} -> (a -> b) -> Cont r a -> Cont r b
mapCont f (MkCont x2) = MkCont (\ {arg:6021} => x2 (\ {arg:6023} => {arg:6021} (f {arg:6023})))
mapCont f (MkCont x2) = MkCont (\ {arg:6048} => x2 (\ {arg:6050} => {arg:6048} (f {arg:6050})))
LOG derive.functor.clauses:1:
mapCont2 : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2 r e a -> Cont2 r e b
mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6113} => \ {arg:6120} => x3 {arg:6113} (\ {arg:6122} => {arg:6120} (f {arg:6122})))
mapCont2 f (MkCont2 x3) = MkCont2 (\ {arg:6140} => \ {arg:6147} => x3 {arg:6140} (\ {arg:6149} => {arg:6147} (f {arg:6149})))
LOG derive.functor.clauses:1:
mapCont2' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2' r e a -> Cont2' r e b
mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6227} => x3 (mapFst (\ t => \ {arg:6229} => t (f {arg:6229})) {arg:6227}))
mapCont2' f (MkCont2' x3) = MkCont2' (\ {arg:6254} => x3 (mapFst (\ t => \ {arg:6256} => t (f {arg:6256})) {arg:6254}))
LOG derive.functor.clauses:1:
mapCont2'' : {0 r, e : _} -> {0 a, b : Type} -> (a -> b) -> Cont2'' r e a -> Cont2'' r e b
mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6351} => x3 (Delay (mapFst (\ t => \ {arg:6354} => t (Delay (f {arg:6354}))) {arg:6351})))
mapCont2'' f (MkCont2'' x3) = MkCont2'' (\ {arg:6378} => x3 (Delay (mapFst (\ t => \ {arg:6381} => t (Delay (f {arg:6381}))) {arg:6378})))
LOG derive.functor.clauses:1:
mapWithImplicits : {0 a, b : Type} -> (a -> b) -> WithImplicits a -> WithImplicits b
mapWithImplicits f (MkImplicit {x = x1} x2) = MkImplicit {x = f x1} (f x2)

194
tests/base/deriving_show/DeriveShow.idr Normal file
View File

@ -0,0 +1,194 @@
module DeriveShow
import Deriving.Show
%language ElabReflection
%default covering
%logging "derive.show.clauses" 1
%logging "derive.show.assumption" 10
namespace Enum
data Enum = A | B | C
enumShow : Show Enum
enumShow = %runElab derive
namespace Sum
data Sum : Type where
AString : String -> Sum
ANat : Nat -> Sum
sumShow : Show Sum
sumShow = %runElab derive
list : Show a => Show (List a)
list = %runElab derive
maybe : Show a => Show (Maybe a)
maybe = %runElab derive
either : (Show err, Show a) => Show (Either err a)
either = %runElab derive
namespace Constant
record Constant (a, b : Type) where
constructor MkConstant
runConstant : a
constant : Show a => Show (Constant a b)
constant = %runElab derive
namespace Vect
public export
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect n a -> Vect (S n) a
export %hint
total
vect : Show a => Show (Vect n a)
vect = %runElab derive
namespace BigTree
data BigTree a
= End a
| Branch String (List a) (Bool -> BigTree a)
| Rose (List (BigTree a))
failing "Unsupported type"
bigTree : Show a => Show (BigTree a)
bigTree = %runElab derive
namespace Matrix
record Matrix m n a where
constructor MkMatrix
runMatrix : Vect m (Vect n a)
total
matrix : Show a => Show (Matrix m n a)
matrix = %runElab derive
namespace Tm
public export
data Op : Nat -> Type where
Neg : Op 1
Add : Op 2
%hint
op : Show (Op n)
op = %runElab derive
public export
data Tm : Type -> Type where
Var : a -> Tm a
Call : Op n -> Vect n (Tm a) -> Tm a
Lam : Tm (Maybe a) -> Tm a
public export total %hint
tm : Show a => Show (Tm a)
tm = %runElab derive
namespace Forest
data Tree : Type -> Type
data Forest : Type -> Type
data Tree : Type -> Type where
Leaf : a -> Tree a
Node : Forest a -> Tree a
data Forest : Type -> Type where
Empty : Forest a
Plant : Tree a -> Forest a -> Forest a
%hint total tree : Show a => Show (Tree a)
%hint total forest : Show a => Show (Forest a)
tree = %runElab derive {mutualWith = [`{Forest}]}
forest = %runElab derive {mutualWith = [`{Tree}]}
namespace List1
data List1 : Type -> Type where
MkList1 : (a, Maybe (List1 a)) -> List1 a
total %hint
list1 : Show a => Show (List1 a)
list1 = %runElab derive
namespace Full
data Full a = Leaf a | Node (Full (a, a))
total %hint
full : Show a => Show (Full a)
full = %runElab derive
failing "Unsupported type"
data NOT : Type -> Type where
MkNOT : (a -> Void) -> NOT a
total
negative : Show a => Show (NOT a)
negative = %runElab derive
namespace Colist
data Colist a = Nil | (::) a (Inf (Colist a))
failing "Cannot show an infinite structure"
total
colist : Show a => Show (Colist a)
colist = %runElab derive
namespace LAZY
record LAZY (a : Type) where
constructor MkLAZY
wrapped : Lazy a
total
lazy : Show a => Show (LAZY a)
lazy = %runElab derive
namespace Implicit
data IVect : {n : Nat} -> (a : Type) -> Type where
MkIVect : (v : Vect n a) -> IVect {n} a
ivect : {m : Nat} -> Show a => Show (IVect {n = m} a)
ivect = %runElab derive
namespace EqMap
data EqMap : (key : Type) -> Eq key => (val : Type) -> Type where
MkEqMap : (eq : Eq key) => List (key, val) -> EqMap key @{eq} val
empty : Eq key => EqMap key val
empty = MkEqMap []
insert : (eq : Eq key) => key -> val -> EqMap key @{eq} val -> EqMap key @{eq} val
insert k v (MkEqMap kvs) = MkEqMap ((k, v) :: filter ((k /=) . fst) kvs)
fromList : Eq key => List (key, val) -> EqMap key val
fromList = foldr (uncurry insert) empty
toList : EqMap key @{eq} val -> List (key, val)
toList (MkEqMap kvs) = kvs
test : EqMap.toList (fromList [(1,2), (1,3), (2, 4), (5, 3), (1, 0)])
=== [(1,2), (2, 4), (5, 3)]
test = Refl
eqMap : (eq : Eq key) => Show key => Show val => Show (EqMap key @{eq} val)
eqMap = %runElab derive

12
tests/base/deriving_show/Search.idr Normal file
View File

@ -0,0 +1,12 @@
module Search
import Language.Reflection
import Language.Reflection.TTImp
%language ElabReflection
nothing : Maybe (Not Nat)
nothing = %runElab (search ?)
test : Search.nothing === Nothing
test = Refl

88
tests/base/deriving_show/expected Normal file
View File

@ -0,0 +1,88 @@
1/1: Building DeriveShow (DeriveShow.idr)
LOG derive.show.clauses:1:
showPrecEnum : Prec -> Enum -> String
showPrecEnum d A = "A"
showPrecEnum d B = "B"
showPrecEnum d C = "C"
LOG derive.show.clauses:1:
showPrecSum : Prec -> Sum -> String
showPrecSum d (AString x0) = showCon d "AString" (showArg x0)
showPrecSum d (ANat x0) = showCon d "ANat" (showArg x0)
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecList : {0 a : _} -> Show a => Prec -> List a -> String
showPrecList d Nil = "Nil"
showPrecList d (x0 :: x1) = showCon d "(::)" (concat ((showArg x0) :: ((assert_total (showArg x1)) :: Nil)))
LOG derive.show.assumption:10: I am assuming that the parameter ty can be shown
LOG derive.show.clauses:1:
showPrecMaybe : {0 a : _} -> Show a => Prec -> Maybe a -> String
showPrecMaybe d Nothing = "Nothing"
showPrecMaybe d (Just x0) = showCon d "Just" (showArg x0)
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.assumption:10: I am assuming that the parameter b can be shown
LOG derive.show.clauses:1:
showPrecEither : {0 err : _} -> Show err => {0 a : _} -> Show a => Prec -> Either err a -> String
showPrecEither d (Left x0) = showCon d "Left" (showArg x0)
showPrecEither d (Right x0) = showCon d "Right" (showArg x0)
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecConstant : {0 a : _} -> Show a => {0 b : _} -> Prec -> Constant a b -> String
showPrecConstant d (MkConstant x0) = showCon d "MkConstant" (showArg x0)
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecVect : {0 n, a : _} -> Show a => Prec -> Vect n a -> String
showPrecVect d Nil = "Nil"
showPrecVect d (x0 :: x1) = showCon d "(::)" (concat ((showArg x0) :: ((assert_total (showArg x1)) :: Nil)))
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecMatrix : {0 m, n, a : _} -> Show a => Prec -> Matrix m n a -> String
showPrecMatrix d (MkMatrix x0) = showCon d "MkMatrix" (showArg x0)
LOG derive.show.clauses:1:
showPrecOp : {0 n : _} -> Prec -> Op n -> String
showPrecOp d Neg = "Neg"
showPrecOp d Add = "Add"
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecTm : {0 a : _} -> Show a => Prec -> Tm a -> String
showPrecTm d (Var x0) = showCon d "Var" (showArg x0)
showPrecTm d (Call x0 x1) = showCon d "Call" (concat ((showArg x0) :: ((assert_total (showArg x1)) :: Nil)))
showPrecTm d (Lam x0) = showCon d "Lam" (assert_total (showArg x0))
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecTree : {0 a : _} -> Show a => Prec -> Tree a -> String
showPrecTree d (Leaf x0) = showCon d "Leaf" (showArg x0)
showPrecTree d (Node x0) = showCon d "Node" (assert_total (showArg x0))
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecForest : {0 a : _} -> Show a => Prec -> Forest a -> String
showPrecForest d Empty = "Empty"
showPrecForest d (Plant x0 x1) = showCon d "Plant" (concat ((assert_total (showArg x0)) :: ((assert_total (showArg x1)) :: Nil)))
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecList1 : {0 a : _} -> Show a => Prec -> List1 a -> String
showPrecList1 d (MkList1 x0) = showCon d "MkList1" (assert_total (showArg x0))
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecFull : {0 a : _} -> Show a => Prec -> Full a -> String
showPrecFull d (Leaf x0) = showCon d "Leaf" (showArg x0)
showPrecFull d (Node x0) = showCon d "Node" (assert_total (showArg x0))
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecLAZY : {0 a : _} -> Show a => Prec -> LAZY a -> String
showPrecLAZY d (MkLAZY x0) = showCon d "MkLAZY" (showArg (Force x0))
LOG derive.show.assumption:10: I am assuming that the parameter a can be shown
LOG derive.show.clauses:1:
showPrecIVect : {0 m, a : _} -> Show a => Prec -> IVect {n = m} a -> String
showPrecIVect d (MkIVect x0) = showCon d "MkIVect" (showArg x0)
LOG derive.show.assumption:10: I am assuming that the parameter key can be shown
LOG derive.show.assumption:10: I am assuming that the parameter val can be shown
LOG derive.show.clauses:1:
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)
DeriveShow> "Lam (Call Add ((::) (Var Nothing) ((::) (Var (Just ())) Nil)))"
DeriveShow>
Bye for now!

2
tests/base/deriving_show/input Normal file
View File

@ -0,0 +1,2 @@
show (Lam (Call Add [Var Nothing, Var (Just ())]))
:q

3
tests/base/deriving_show/run Executable file
View File

@ -0,0 +1,3 @@
rm -rf build
$1 --no-color --console-width 0 --no-banner DeriveShow.idr < input

2
tests/base/deriving_traversable/expected
View File

@ -68,7 +68,7 @@ LOG derive.traversable.clauses:1:
traverseIVect : {0 m : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> IVect {n = m} a -> f (IVect {n = m} b)
traverseIVect f (MkIVect x2) = MkIVect <$> (traverse f x2)
LOG derive.traversable.clauses:1:
traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13793} = eq} a -> f (EqMap key {{conArg:13793} = eq} b)
traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13922} = eq} a -> f (EqMap key {{conArg:13922} = eq} b)
traverseEqMap f (MkEqMap x3) = MkEqMap <$> (traverse (traverse f) x3)
LOG derive.traversable.clauses:1:
traverseTree : {0 l : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree l a -> f (Tree l b)