idris-lang/Idris2
1
1
Fork 0
mirror of https://github.com/idris-lang/Idris2.git synced 2024-11-28 11:05:17 +03:00
Code Issues Projects Releases Wiki Activity

[ base ] deriving Traversable (#2678)

Browse Source
This commit is contained in:
G. Allais 2022-09-24 12:43:49 +01:00 committed by GitHub
parent 5631608782
commit 81ea363ae8
No known key found for this signature in database
GPG Key ID: 4AEE18F83AFDEB23
9 changed files with 981 additions and 28 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

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

@ -41,6 +41,18 @@ isSnoc : SnocList a -> Bool
isSnoc Lin = False
isSnoc (sx :< x) = True
||| Given a predicate and a snoclist, returns a tuple consisting of the longest
||| prefix of the snoclist whose elements satisfy the predicate, and the rest of the
||| snoclist.
public export
spanBy : (a -> Maybe b) -> SnocList a -> (SnocList a, SnocList b)
spanBy p [<] = ([<], [<])
spanBy p (xs :< x) = case p x of
Just b =>
let (as, bs) = spanBy p xs in
(as, bs :< b)
Nothing => (xs :< x, [<])
export
Show a => Show (SnocList a) where
show xs = concat ("[< " :: intersperse ", " (show' [] xs) ++ ["]"])

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

@ -181,6 +181,22 @@ cleanup = \case
IVar fc n => IVar fc (dropNS n)
t => t
||| Create fresh names
export
freshName : List Name -> String -> String
freshName ns a = assert_total $ go (basicNames ns) Nothing where
basicNames : List Name -> List String
basicNames = mapMaybe $ \ nm => case dropNS nm of
UN (Basic str) => Just str
_ => Nothing
covering
go : List String -> Maybe Nat -> String
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?

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

@ -42,20 +42,6 @@ fromFoldMap f fm = MkFoldable
foldl : forall a, b. (b -> a -> b) -> b -> f a -> b
foldl cons base t = foldr (flip (.) . flip cons) id t base
freshName : List Name -> String -> String
freshName ns a = assert_total $ go (basicNames ns) Nothing where
basicNames : List Name -> List String
basicNames = mapMaybe $ \ nm => case dropNS nm of
UN (Basic str) => Just str
_ => Nothing
covering
go : List String -> Maybe Nat -> String
go ns mi =
let nm = a ++ maybe "" show mi in
ifThenElse (nm `elem` ns) (go ns (Just $ maybe 0 S mi)) nm
------------------------------------------------------------------------------
-- Errors

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

@ -19,20 +19,6 @@ import public Deriving.Common
%language ElabReflection
%default total
freshName : List Name -> String -> String
freshName ns a = assert_total $ go (basicNames ns) Nothing where
basicNames : List Name -> List String
basicNames = mapMaybe $ \ nm => case dropNS nm of
UN (Basic str) => Just str
_ => Nothing
covering
go : List String -> Maybe Nat -> String
go ns mi =
let nm = a ++ maybe "" show mi in
ifThenElse (nm `elem` ns) (go ns (Just $ maybe 0 S mi)) nm
------------------------------------------------------------------------------
-- Errors

428
libs/base/Deriving/Traversable.idr Normal file
View File

@ -0,0 +1,428 @@
||| Deriving traversable instances using reflection
||| You can for instance define:
||| ```
||| data Tree a = Leaf a | Node (Tree a) (Tree a)
||| treeFoldable : Traversable Tree
||| treeFoldable = %runElab derive
||| ```
module Deriving.Traversable
import public Control.Monad.Either
import public Control.Monad.State
import public Data.List1
import public Data.Maybe
import public Data.Morphisms
import public Decidable.Equality
import public Language.Reflection
import public Deriving.Common
%language ElabReflection
%default total
------------------------------------------------------------------------------
-- Errors
||| Possible errors for the functor-deriving machinery.
public export
data Error : Type where
NotFreeOf : Name -> TTImp -> Error
NotAnApplication : TTImp -> Error
NotATraversable : TTImp -> Error
NotABitraversable : TTImp -> Error
NotTraversableInItsLastArg : TTImp -> 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 (NotFreeOf x ty) = acc <>> ["The term \{show ty} is not free of \{show x}"]
go acc (NotAnApplication s) = acc <>> ["The type \{show s} is not an application"]
go acc (NotATraversable s) = acc <>> ["Couldn't find a `Traversable' instance for the type constructor \{show s}"]
go acc (NotABitraversable s) = acc <>> ["Couldn't find a `Bitraversable' instance for the type constructor \{show s}"]
go acc (NotTraversableInItsLastArg s) = acc <>> ["Not traversable in its last argument \{show s}"]
go acc (UnsupportedType s) = acc <>> ["Unsupported type \{show s}"]
go acc NotAFiniteStructure = acc <>> ["Cannot traverse an infinite structure"]
go acc (NotAnUnconstrainedValue rig) = acc <>> ["Cannot traverse a \{enunciate rig} value"]
go acc InvalidGoal = acc <>> ["Expected a goal of the form `Traversable f`"]
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
asTraversables : List Nat
asBitraversables : List Nat
initParameters : Parameters
initParameters = MkParameters [] []
paramConstraints : Parameters -> Nat -> Maybe TTImp
paramConstraints params pos
= IVar emptyFC `{Prelude.Interfaces.Traversable} <$ guard (pos `elem` params.asTraversables)
<|> IVar emptyFC `{Prelude.Interfaces.Bitraversable} <$ guard (pos `elem` params.asBitraversables)
------------------------------------------------------------------------------
-- Core machinery: being traversable
-- Not meant to be re-exported as it's using the internal notion of error
isFreeOf' :
{0 m : Type -> Type} ->
{auto elab : Elaboration m} ->
{auto error : MonadError Error m} ->
(x : Name) -> (ty : TTImp) -> m (IsFreeOf x ty)
isFreeOf' x ty = case isFreeOf x ty of
Nothing => throwError (NotFreeOf x ty)
Just prf => pure prf
||| IsTraversableIn is parametrised by
||| @ 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,
||| assuming that t also is traversable.
public export
data IsTraversableIn : (t, x : Name) -> (ty : TTImp) -> Type where
||| The type variable x occurs alone
TIVar : IsTraversableIn t x (IVar fc x)
||| There is a recursive subtree of type (t a1 ... an u) and u is Traversable in x.
||| We do not insist that u is exactly x so that we can deal with nested types
||| like the following:
||| data Full a = Leaf a | Node (Full (a, a))
||| data Term a = Var a | App (Term a) (Term a) | Lam (Term (Maybe a))
TIRec : (0 _ : IsAppView (_, t) _ f) -> IsTraversableIn t x arg ->
IsTraversableIn t x (IApp fc f arg)
||| The subterm is delayed (Lazy only, we can't traverse infinite structures)
TIDelayed : IsTraversableIn t x ty -> IsTraversableIn t x (IDelayed fc LLazy ty)
||| There are nested subtrees somewhere inside a 3rd party type constructor
||| which satisfies the Bitraversable interface
TIBifold : IsFreeOf x sp -> HasImplementation Bitraversable sp ->
IsTraversableIn t x arg1 -> Either (IsTraversableIn t x arg2) (IsFreeOf x arg2) ->
IsTraversableIn t x (IApp fc1 (IApp fc2 sp arg1) arg2)
||| There are nested subtrees somewhere inside a 3rd party type constructor
||| which satisfies the Traversable interface
TIFold : IsFreeOf x sp -> HasImplementation Traversable sp ->
IsTraversableIn t x arg -> IsTraversableIn t x (IApp fc sp arg)
||| A type free of x is trivially Traversable in it
TIFree : IsFreeOf x a -> IsTraversableIn t x a
parameters
{0 m : Type -> Type}
{auto elab : Elaboration m}
{auto error : MonadError Error m}
{auto cs : MonadState Parameters m}
(t : Name)
(ps : List Name)
(x : Name)
||| When analysing the type of a constructor for the type family t,
||| we hope to observe
||| 1. either that it is traversable in x
||| 2. or that it is free of x
||| If it is not the case, we will use the `MonadError Error` constraint
||| to fail with an informative message.
public export
TypeView : TTImp -> Type
TypeView ty = Either (IsTraversableIn t x ty) (IsFreeOf x ty)
export
fromTypeView : TypeView ty -> IsTraversableIn t x ty
fromTypeView (Left prf) = prf
fromTypeView (Right fo) = TIFree fo
||| Hoping to observe that ty is functorial
export
typeView : (ty : TTImp) -> m (TypeView ty)
||| To avoid code duplication in typeView, we have an auxiliary function
||| specifically to handle the application case
typeAppView :
{fc : FC} ->
{f : TTImp} -> IsFreeOf x f ->
(arg : TTImp) ->
m (TypeView (IApp fc f arg))
typeAppView {fc, f} isFO arg = do
chka <- typeView arg
case chka of
-- if x is present in the argument then the function better be:
-- 1. free of x
-- 2. either an occurrence of t i.e. a subterm
-- or a type constructor already known to be functorial
Left sp => do
let Just (MkAppView (_, hd) ts prf) = appView f
| _ => throwError (NotAnApplication f)
case decEq t hd of
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
Just n => do
-- record that the nth parameter should be functorial
ns <- gets asTraversables
let ns = ifThenElse (n `elem` ns) ns (n :: ns)
modify { asTraversables := ns }
-- and happily succeed
logMsg "derive.traversable.assumption" 10 $
"I am assuming that the parameter \{show hd} is a Traversable"
pure (Left (TIFold isFO assert_hasImplementation sp))
Nothing => throwError (NotATraversable f)
-- Otherwise it better be the case that f is also free of x so that
-- we can mark the whole type as being x-free.
Right fo => do
Right _ <- typeView f
| _ => throwError $ NotTraversableInItsLastArg (IApp fc f arg)
pure (Right assert_IsFreeOf)
typeView tm@(IVar fc y) = case decEq x y of
Yes Refl => pure (Left TIVar)
No _ => pure (Right assert_IsFreeOf)
typeView fab@(IApp _ (IApp fc1 f arg1) arg2) = do
chka1 <- typeView arg1
case chka1 of
Right _ => do isFO <- isFreeOf' x (IApp _ f arg1)
typeAppView {f = assert_smaller fab (IApp _ f arg1)} isFO arg2
Left sp => do
isFO <- isFreeOf' x f
case !(hasImplementation Bitraversable f) of
Just prf => pure (Left (TIBifold isFO prf sp !(typeView arg2)))
Nothing => do
let Just (MkAppView (_, hd) ts prf) = appView f
| _ => throwError (NotAnApplication f)
case hd `elemPos` ps of
Just n => do
-- record that the nth parameter should be bitraversable
ns <- gets asBitraversables
let ns = ifThenElse (n `elem` ns) ns (n :: ns)
modify { asBitraversables := ns }
-- and happily succeed
logMsg "derive.traversable.assumption" 10 $
"I am assuming that the parameter \{show hd} is a Bitraversable"
pure (Left (TIBifold isFO assert_hasImplementation sp !(typeView arg2)))
Nothing => throwError (NotABitraversable f)
typeView (IApp _ f arg) = do
isFO <- isFreeOf' x f
typeAppView isFO arg
typeView (IDelayed _ lz f) = case !(typeView f) of
Left sp => case lz of
LLazy => pure (Left (TIDelayed sp))
_ => throwError NotAFiniteStructure
Right _ => pure (Right assert_IsFreeOf)
typeView (IPrimVal _ _) = pure (Right assert_IsFreeOf)
typeView (IType _) = pure (Right assert_IsFreeOf)
typeView ty = case isFreeOf x ty of
Nothing => throwError (UnsupportedType ty)
Just prf => pure (Right prf)
------------------------------------------------------------------------------
-- Core machinery: building the traverse function from an IsTraversableIn proof
parameters (fc : FC) (mutualWith : List Name)
||| traverseFun takes
||| @ mutualWith a list of mutually defined type constructors. Calls to their
||| respective mapping functions typically need an assert_total because the
||| termination checker is not doing enough inlining to see that things are
||| terminating
||| @ assert records whether we should mark recursive calls as total because
||| we are currently constructing the argument to a higher order function
||| which will obscure the termination argument. Starts as `Nothing`, becomes
||| `Just False` if an `assert_total` has already been inserted.
||| @ ty the type being transformed by the mapping function
||| @ rec the name of the mapping function being defined (used for recursive calls)
||| @ f the name of the function we're mapping
||| @ arg the (optional) name of the argument being mapped over. This lets us use
||| Nothing when generating arguments to higher order functions so that we generate
||| the eta contracted `map (mapTree f)` instead of `map (\ ts => mapTree f ts)`.
traverseFun : (assert : Maybe Bool) -> {ty : TTImp} -> IsTraversableIn t x ty ->
(rec, f : Name) -> (arg : Maybe TTImp) -> TTImp
traverseFun assert TIVar rec f t = apply fc (IVar fc f) (toList t)
traverseFun assert (TIRec y sp) rec f t
-- only add assert_total if it is declared to be needed
= ifThenElse (fromMaybe False assert) (IApp fc (IVar fc (UN $ Basic "assert_total"))) id
$ apply fc (IVar fc rec) (traverseFun (Just False) sp rec f Nothing :: toList t)
traverseFun assert (TIDelayed sp) rec f Nothing
-- here we need to eta-expand to avoid "Lazy t does not unify with t" errors
= let nm = UN $ Basic "eta" in
ILam fc MW ExplicitArg (Just nm) (IDelayed fc LLazy (Implicit fc False))
$ apply fc `((<$>))
[ `(delay)
, traverseFun assert sp rec f (Just (IVar fc nm))
]
traverseFun assert (TIDelayed sp) rec f (Just t)
= apply fc `((<$>))
[ `(delay)
, traverseFun assert sp rec f (Just t)
]
traverseFun assert {ty = IApp _ ty _} (TIFold _ _ sp) rec f t
-- only add assert_total if we are calling a mutually defined Traversable implementation.
= let isMutual = fromMaybe False (appView ty >>= \ v => pure (snd v.head `elem` mutualWith)) in
ifThenElse isMutual (IApp fc (IVar fc (UN $ Basic "assert_total"))) id
$ apply fc (IVar fc (UN $ Basic "traverse"))
(traverseFun ((False <$ guard isMutual) <|> assert <|> Just True) sp rec f Nothing
:: toList t)
traverseFun assert (TIBifold _ _ sp1 (Left sp2)) rec f t
= apply fc (IVar fc (UN $ Basic "bitraverse"))
(traverseFun (assert <|> Just True) sp1 rec f Nothing
:: traverseFun (assert <|> Just True) sp2 rec f Nothing
:: toList t)
traverseFun assert (TIBifold _ _ sp (Right _)) rec f t
= apply fc (IVar fc (UN $ Basic "bitraverseFst"))
(traverseFun (assert <|> Just True) sp rec f Nothing
:: toList t)
traverseFun assert (TIFree y) rec f t = `(mempty)
------------------------------------------------------------------------------
-- User-facing: Traversable deriving
applyA : FC -> TTImp -> List (Either (Argument TTImp) TTImp) -> TTImp
applyA fc c [] = `(pure ~(c))
applyA fc c (Right a :: as) = applyA fc (IApp fc c a) as
applyA fc c as =
let (pref, suff) = spanBy canBeApplied ([<] <>< as) in
let (lams, args, vals) = preEta 0 (pref <>> []) in
let eta = foldr (\ x => ILam fc MW ExplicitArg (Just x) (Implicit fc False)) (apply c args) lams in
fire eta (map Left vals ++ (suff <>> []))
where
canBeApplied : Either (Argument TTImp) TTImp -> Maybe (Either TTImp TTImp)
canBeApplied (Left (Arg _ t)) = pure (Left t)
canBeApplied (Right t) = pure (Right t)
canBeApplied _ = Nothing
preEta : Nat -> List (Either (Argument TTImp) TTImp) ->
(List Name, List (Argument TTImp), List TTImp)
preEta n [] = ([], [], [])
preEta n (a :: as) =
let (n, ns, args, vals) = the (Nat, List Name, List (Argument TTImp), List _) $
let x = UN (Basic ("y" ++ show n)); vx = IVar fc x in case a of
Left (Arg fc t) => (S n, [x], [Arg fc vx], [t])
Left (NamedArg fc nm t) => (S n, [x], [NamedArg fc nm vx], [t])
Left (AutoArg fc t) => (S n, [x], [AutoArg fc vx], [t])
Right t => (n, [], [Arg fc t], [])
in
let (nss, argss, valss) = preEta n as in
(ns ++ nss, args ++ argss, vals ++ valss)
go : TTImp -> List (Either TTImp TTImp) -> TTImp
go f [] = f
go f (Left a :: as) = go (apply fc `((<*>)) [f, a]) as
go f (Right a :: as) = go (apply fc `((<*>)) [f, IApp fc `(pure) a]) as
fire : TTImp -> List (Either TTImp TTImp) -> TTImp
fire f [] = f
fire f (a :: as) = go (apply fc `((<$>)) [f, either id id a]) as
namespace Traversable
derive' : (Elaboration m, MonadError Error m) =>
{default Private vis : Visibility} ->
{default Total treq : TotalReq} ->
{default [] mutualWith : List Name} ->
m (Traversable 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 (Traversable t)
Just (IApp _ (IVar _ traversable) t) <- goal
| _ => throwError InvalidGoal
when (`{Prelude.Interfaces.Traversable} /= traversable) $
logMsg "derive.traversable" 1 "Expected to derive Traversable but got \{show traversable}"
-- t should be a type constructor
logMsg "derive.traversable" 1 "Deriving Traversable for \{showPrec App $ mapTTImp cleanup t}"
MkIsType f params cs <- isType t
logMsg "derive.traversable.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 traverseName = un ("traverse" ++ show (dropNS f))
let funName = un "f"
let fun = IVar fc funName
(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
| _ => throwError ConfusingReturnType
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)))
$ zipWith (<$) [1..length args] (map snd args)
recs <- for (zip vars args) $ \ (v, (rig, arg)) => do
res <- withError (WhenCheckingArg (mapTTImp cleanup (unArg arg))) $ do
res <- typeView f paras para (unArg arg)
case res of
Left _ => case rig of
MW => pure ()
_ => throwError (NotAnUnconstrainedValue rig)
_ => pure ()
pure res
pure $ case res of
Left sp => -- do not bother with assert_total if you're generating
-- a covering/partial definition
let useTot = False <$ guard (treq /= Total) in
Just (v, Left (traverseFun fc mutualWith useTot sp traverseName funName . Just <$> v))
Right free => do ignore $ isExplicit v
Just (v, Right (unArg v))
let (vars, recs) = unzip (catMaybes recs)
pure $ PatClause fc
(apply fc (IVar fc traverseName) [ fun, apply (IVar fc cName) vars])
(applyA fc (IVar fc cName) recs)
-- Generate the type of the mapping function
let paramNames = unArg . fst <$> params
let a = un $ freshName paramNames "a"
let b = un $ freshName paramNames "b"
let f = un $ freshName paramNames "f"
let va = IVar fc a
let vb = IVar fc b
let vf = IVar fc f
let ty = MkTy fc fc traverseName $ withParams fc (paramConstraints ns) params
$ IPi fc M0 ImplicitArg (Just a) (IType fc)
$ IPi fc M0 ImplicitArg (Just b) (IType fc)
$ IPi fc M0 ImplicitArg (Just f) (IPi fc MW ExplicitArg Nothing (IType fc) (IType fc))
$ `(Applicative ~(vf) => (~(va) -> ~(vf) ~(vb)) -> ~(t) ~(va) -> ~(vf) (~(t) ~(vb)))
logMsg "derive.traversable.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 traverseName cls
] `(MkTraversable {t = ~(t)} ~(IVar fc traverseName))
||| Derive an implementation of Traversable for a type constructor.
||| This can be used like so:
||| ```
||| data Tree a = Leaf a | Node (Tree a) (Tree a)
||| treeTraversable : Traversable Tree
||| treeTraversable = %runElab derive
||| ```
export
derive : {default Private vis : Visibility} ->
{default Total treq : TotalReq} ->
{default [] mutualWith : List Name} ->
Elab (Traversable 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

1
libs/base/base.ipkg
View File

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

439
tests/base/deriving_traversable/DeriveTraversable.idr Normal file
View File

@ -0,0 +1,439 @@
module DeriveTraversable
import Deriving.Functor
import Deriving.Foldable
import Deriving.Traversable
%language ElabReflection
%default covering
%logging "derive.traversable.clauses" 1
%logging "derive.traversable.assumption" 10
listT : Traversable List
listT = %runElab derive
maybeT : Traversable Maybe
maybeT = %runElab derive
eitherT : Traversable (Either err)
eitherT = %runElab derive
-- Here we don't have a `Foldable (Pair a)` instance and the tactics
-- unfortunately builds
-- pairT = let traversePair = (...) in
-- MkTraversable @{pairT .foldable} traversePair
-- because the `pairT` name is a %hint.
--
-- TODO: find a way to program defensively against this!
failing "pairT is not total"
%hint total
pairT : Traversable (Pair a)
pairT = %runElab derive
%hint total
pairM : Foldable (Pair a)
pairM = %runElab derive
%hint total
pairT : Traversable (Pair a)
pairT = %runElab derive
namespace Constant
record Constant (a, b : Type) where
constructor MkConstant
runConstant : a
%hint
constantF : Functor (Constant a)
constantF = %runElab derive
%hint
constantM : Foldable (Constant a)
constantM = %runElab derive
constantT : Traversable (Constant a)
constantT = %runElab derive
namespace Vect
public export
data Vect : Nat -> Type -> Type where
Nil : Vect Z a
(::) : a -> Vect n a -> Vect (S n) a
%hint total
vectF : Functor (Vect n)
vectF = %runElab derive
%hint total
vectM : Foldable (Vect n)
vectM = %runElab derive
export %hint
total
vectT : Traversable (Vect n)
vectT = %runElab derive
namespace Matrix
record Matrix m n a where
constructor MkMatrix
runMatrix : Vect m (Vect n a)
%hint total
matrixF : Functor (Matrix m n)
matrixF = %runElab derive
%hint total
matrixM : Foldable (Matrix m n)
matrixM = %runElab derive
total
matrix : Traversable (Matrix m n)
matrix = %runElab derive
namespace Tm
data Op : Nat -> Type where
Neg : Op 1
Add : Op 2
data Tm : Type -> Type where
Var : a -> Tm a
Call : Op n -> Vect n (Tm a) -> Tm a
Lam : Tm (Maybe a) -> Tm a
%hint total
tmF : Functor Tm
tmF = %runElab derive
%hint total
tmM : Foldable Tm
tmM = %runElab derive
total
tm : Traversable Tm
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 treeF : Functor Tree
%hint total forestF : Functor Forest
treeF = %runElab derive {mutualWith = [`{Forest}]}
forestF = %runElab derive {mutualWith = [`{Tree}]}
%hint total treeM : Foldable Tree
%hint total forestM : Foldable Forest
treeM = %runElab derive {mutualWith = [`{Forest}]}
forestM = %runElab derive {mutualWith = [`{Tree}]}
%hint total treeT : Traversable Tree
%hint total forestT : Traversable Forest
treeT = %runElab derive {mutualWith = [`{Forest}]}
forestT = %runElab derive {mutualWith = [`{Tree}]}
namespace List1
%hide List1
data List1 : Type -> Type where
MkList1 : (a, Maybe (List1 a)) -> List1 a
%hint total
list1F : Functor List1
list1F = %runElab derive
%hint total
list1M : Foldable List1
list1M = %runElab derive
total
list1T : Traversable List1
list1T = %runElab derive
namespace Full
data Full a = Leaf a | Node (Full (a, a))
%hint total
fullF : Functor Full
fullF = %runElab derive
%hint total
fullM : Foldable Full
fullM = %runElab derive
total
fullT : Traversable Full
fullT = %runElab derive
namespace LAZY
record LAZY (a : Type) where
constructor MkLAZY
wrapped : Lazy a
%hint total
lazyF : Functor LAZY
lazyF = %runElab derive
%hint total
lazyM : Foldable LAZY
lazyM = %runElab derive
total
lazyT : Traversable LAZY
lazyT = %runElab derive
namespace Rose
data Rose a = Node (List (Lazy (Rose a)))
%hint total
roseF : Functor Rose
roseF = %runElab derive
%hint total
roseM : Foldable Rose
roseM = %runElab derive
total
roseT : Traversable Rose
roseT = %runElab derive
namespace MaybeT
record MaybeT (m : Type -> Type) (a : Type) where
constructor MkMaybeT
runMaybeT : m (Maybe a)
%hint total
maybeTF : Functor m => Functor (MaybeT m)
maybeTF = %runElab derive
%hint total
maybeTM : Foldable m => Foldable (MaybeT m)
maybeTM = %runElab derive
total
maybeTT : Traversable m => Traversable (MaybeT m)
maybeTT = %runElab derive
namespace TreeT
data TreeT : (Type -> Type -> Type) -> Type -> Type where
MkTreeT : layer a (TreeT layer a) -> TreeT layer a
%hint
treeTF : Bifunctor layer => Functor (TreeT layer)
treeTF = %runElab derive {treq = CoveringOnly}
%hint
treeTM : Bifoldable layer => Foldable (TreeT layer)
treeTM = %runElab derive {treq = CoveringOnly}
%hint
treeTT : Bitraversable layer => Traversable (TreeT layer)
treeTT = %runElab derive {treq = CoveringOnly}
record Tree (a : Type) where
constructor MkTree
runTree : TreeT Either a
%hint
treeF : Functor Tree
treeF = %runElab derive {treq = CoveringOnly}
%hint
treeM : Foldable Tree
treeM = %runElab derive {treq = CoveringOnly}
treeT : Traversable Tree
treeT = %runElab derive {treq = CoveringOnly}
namespace Implicit
data IVect : {n : Nat} -> (a : Type) -> Type where
MkIVect : (v : Vect n a) -> IVect {n} a
%hint total
ivectF : {m : Nat} -> Functor (IVect {n = m})
ivectF = %runElab derive
%hint total
ivectM : {m : Nat} -> Foldable (IVect {n = m})
ivectM = %runElab derive
total
ivectT : {m : Nat} -> Traversable (IVect {n = m})
ivectT = %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
%hint total
eqMapF : (eq : Eq key) => Functor (EqMap key @{eq})
eqMapF = %runElab derive
%hint total
eqMapM : (eq : Eq key) => Foldable (EqMap key @{eq})
eqMapM = %runElab derive
total
eqMapT : (eq : Eq key) => Traversable (EqMap key @{eq})
eqMapT = %runElab derive
namespace Implicit
data WithImplicits : Type -> Type where
MkImplicit : {x : a} -> (0 y : a) -> WithImplicits a
OtherImplicit : {0 x : a} -> a => WithImplicits a
LastOne : {auto 0 _ : a} -> a -> WithImplicits a
failing "Cannot traverse a runtime irrelevant value"
total
withImplicits : Traversable WithImplicits
withImplicits = %runElab derive
failing "Couldn't find a `Traversable' instance for the type constructor DeriveTraversable.Wrap"
record Wrap (a : Type) where
constructor MkWrap
unWrap : a
%hint total
wrapF : Functor Wrap
wrapF = %runElab derive
%hint total
wrapM : Foldable Wrap
wrapM = %runElab derive
data Indirect : Type -> Type where
MkIndirect : Wrap a -> Indirect a
%hint total
indirectF : Functor Indirect
indirectF = %runElab derive
%hint total
indirectM : Foldable Indirect
indirectM = %runElab derive
total
indirectT : Traversable Indirect
indirectT = %runElab derive
namespace BitraversableFail
data Tree : (l, n : Type) -> Type where
Leaf : l -> Tree l n
Node : Tree l n -> n -> Tree l n -> Tree l n
-- this one will succeed
%hint total
treeF : Functor (Tree l)
treeF = %runElab derive
%hint total
treeM : Foldable (Tree l)
treeM = %runElab derive
total
tree : Traversable (Tree l)
tree = %runElab derive
failing "Couldn't find a `Bitraversable' instance for the type constructor DeriveTraversable.BitraversableFail.Tree"
record Tree' (a : Type) where
constructor MkTree'
getTree : Tree a a
-- and this one will fail
tree' : Traversable Tree'
tree' = %runElab derive
failing "Expected a type constructor, got: Prelude.Basics.id {a = Type}"
total
traverable : Traversable Prelude.id
traverable = %runElab derive
namespace Triple
data Triple a b c = MkTriple a b c
%hint
triple : Traversable (Triple a b)
triple = %runElab derive
data Tree3 a = Node (Triple a () (Tree3 a))
failing "The term DeriveTraversable.Triple.Triple a Builtin.Unit is not free of a"
tree : Traversable Tree3
tree = %runElab derive
namespace WriterList
data WList : (w, u, a : Type) -> Type where
(::) : (w, a) -> WList {- oops -} a u a -> WList w u a
Nil : WList w u a
failing "The term DeriveTraversable.WriterList.WList a u is not free of a"
wlist : Traversable (WList w ())
wlist = %runElab derive
namespace WithImplicits
data F : Type -> Type where
MkF : {x : a} -> Nat -> a -> String -> {y : a} -> a -> List a -> F a
%hint
fF : Functor F
fF = %runElab derive
%hint
fM : Foldable F
fM = %runElab derive
fT : Traversable F
fT = %runElab derive

82
tests/base/deriving_traversable/expected Normal file
View File

@ -0,0 +1,82 @@
1/1: Building DeriveTraversable (DeriveTraversable.idr)
LOG derive.traversable.clauses:1:
traverseList : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> List a -> f (List b)
traverseList f Nil = pure Nil
traverseList f (x1 :: x2) = ((::) <$> (f x1)) <*> (traverseList f x2)
LOG derive.traversable.clauses:1:
traverseMaybe : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Maybe a -> f (Maybe b)
traverseMaybe f Nothing = pure Nothing
traverseMaybe f (Just x1) = Just <$> (f x1)
LOG derive.traversable.clauses:1:
traverseEither : {0 err : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Either err a -> f (Either err b)
traverseEither f (Left x2) = pure (Left x2)
traverseEither f (Right x2) = Right <$> (f x2)
LOG derive.traversable.clauses:1:
traversePair : {0 a : _} -> {0 a0, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a0 -> f b) -> Pair a a0 -> f (Pair a b)
traversePair f (MkPair x2 x3) = (MkPair x2) <$> (f x3)
LOG derive.traversable.clauses:1:
traversePair : {0 a : _} -> {0 a0, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a0 -> f b) -> Pair a a0 -> f (Pair a b)
traversePair f (MkPair x2 x3) = (MkPair x2) <$> (f x3)
LOG derive.traversable.clauses:1:
traverseConstant : {0 a : _} -> {0 a0, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a0 -> f b) -> Constant a a0 -> f (Constant a b)
traverseConstant f (MkConstant x2) = pure (MkConstant x2)
LOG derive.traversable.clauses:1:
traverseVect : {0 n : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Vect n a -> f (Vect n b)
traverseVect f Nil = pure Nil
traverseVect f (x2 :: x3) = ((::) <$> (f x2)) <*> (traverseVect f x3)
LOG derive.traversable.clauses:1:
traverseMatrix : {0 m, n : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Matrix m n a -> f (Matrix m n b)
traverseMatrix f (MkMatrix x3) = MkMatrix <$> (traverse (traverse f) x3)
LOG derive.traversable.clauses:1:
traverseTm : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tm a -> f (Tm b)
traverseTm f (Var x1) = Var <$> (f x1)
traverseTm f (Call x2 x3) = (Call x2) <$> (traverse (assert_total (traverseTm f)) x3)
traverseTm f (Lam x1) = Lam <$> (traverseTm (traverse f) x1)
LOG derive.traversable.clauses:1:
traverseTree : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree a -> f (Tree b)
traverseTree f (Leaf x1) = Leaf <$> (f x1)
traverseTree f (Node x1) = Node <$> (assert_total (traverse f x1))
LOG derive.traversable.clauses:1:
traverseForest : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Forest a -> f (Forest b)
traverseForest f Empty = pure Empty
traverseForest f (Plant x1 x2) = (Plant <$> (assert_total (traverse f x1))) <*> (traverseForest f x2)
LOG derive.traversable.clauses:1:
traverseList1 : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> List1 a -> f (List1 b)
traverseList1 f (MkList1 x1) = MkList1 <$> (bitraverse f (traverse (assert_total (traverseList1 f))) x1)
LOG derive.traversable.clauses:1:
traverseFull : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Full a -> f (Full b)
traverseFull f (Leaf x1) = Leaf <$> (f x1)
traverseFull f (Node x1) = Node <$> (traverseFull (bitraverse f f) x1)
LOG derive.traversable.clauses:1:
traverseLAZY : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> LAZY a -> f (LAZY b)
traverseLAZY f (MkLAZY x1) = MkLAZY <$> (delay <$> (f x1))
LOG derive.traversable.clauses:1:
traverseRose : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Rose a -> f (Rose b)
traverseRose f (Node x1) = Node <$> (traverse (\ eta => delay <$> (assert_total (traverseRose f eta))) x1)
LOG derive.traversable.assumption:10: I am assuming that the parameter m is a Traversable
LOG derive.traversable.clauses:1:
traverseMaybeT : {0 m : _} -> Traversable m => {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> MaybeT m a -> f (MaybeT m b)
traverseMaybeT f (MkMaybeT x2) = MkMaybeT <$> (traverse (traverse f) x2)
LOG derive.traversable.assumption:10: I am assuming that the parameter layer is a Bitraversable
LOG derive.traversable.clauses:1:
traverseTreeT : {0 layer : _} -> Bitraversable layer => {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> TreeT layer a -> f (TreeT layer b)
traverseTreeT f (MkTreeT x2) = MkTreeT <$> (bitraverse f (traverseTreeT f) x2)
LOG derive.traversable.clauses:1:
traverseTree : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> Tree a -> f (Tree b)
traverseTree f (MkTree x1) = MkTree <$> (traverse f x1)
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 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)
traverseTree f (Leaf x2) = pure (Leaf x2)
traverseTree f (Node x2 x3 x4) = ((Node <$> (traverseTree f x2)) <*> (f x3)) <*> (traverseTree f x4)
LOG derive.traversable.clauses:1:
traverseTriple : {0 a, b : _} -> {0 a0, b0 : Type} -> {0 f : Type -> Type} -> Applicative f => (a0 -> f b0) -> Triple a b a0 -> f (Triple a b b0)
traverseTriple f (MkTriple x3 x4 x5) = (MkTriple x3 x4) <$> (f x5)
LOG derive.traversable.clauses:1:
traverseF : {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> F a -> f (F b)
traverseF f (MkF {x = x1} x2 x3 x4 {y = x5} x6 x7) = (((((\ y0 => \ y1 => \ y2 => MkF {x = y0} x2 y1 x4 {y = y2}) <$> (f x1)) <*> (f x3)) <*> (f x5)) <*> (f x6)) <*> (traverse f x7)

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

@ -0,0 +1,3 @@
rm -rf build
$1 --no-color --console-width 0 --no-banner -c DeriveTraversable.idr