From 74e945c01bea3871213e63fd025043a0241facac Mon Sep 17 00:00:00 2001 From: Denis Buzdalov Date: Wed, 18 Oct 2023 00:12:39 +0300 Subject: [PATCH] [ derive ] Refine a constructor view to support implicit args --- CHANGELOG.md | 2 ++ libs/base/Deriving/Common.idr | 10 ++++++---- libs/base/Deriving/Foldable.idr | 8 ++++---- libs/base/Deriving/Functor.idr | 8 ++++---- libs/base/Deriving/Show.idr | 4 ++-- libs/base/Deriving/Traversable.idr | 8 ++++---- libs/base/Language/Reflection/TTImp.idr | 12 ++++++++++++ tests/base/deriving_traversable/expected | 2 +- 8 files changed, 35 insertions(+), 19 deletions(-) diff --git a/CHANGELOG.md b/CHANGELOG.md index 4cefe942d74..8b1dd64d161 100644 --- a/CHANGELOG.md +++ b/CHANGELOG.md @@ -224,6 +224,8 @@ * Adds a `Compose` and `FromApplicative` named implementations for `Zippable`. +* Constructor view in `Deriving.Common` supports implicit and auto arguments. + #### System * Changes `getNProcessors` to return the number of online processors rather than diff --git a/libs/base/Deriving/Common.idr b/libs/base/Deriving/Common.idr index c18834b85b5..3872c4b88ea 100644 --- a/libs/base/Deriving/Common.idr +++ b/libs/base/Deriving/Common.idr @@ -87,9 +87,13 @@ isType = go Z [] where public export record ConstructorView where constructor MkConstructorView - params : SnocList (Name, Nat) + params : SnocList (Argument Name, Nat) conArgTypes : List (Count, Argument TTImp) +getIVar : TTImp -> Maybe Name +getIVar (IVar _ nm) = Just nm +getIVar _ = Nothing + export constructorView : TTImp -> Maybe ConstructorView constructorView (IPi fc rig pinfo x a b) = do @@ -101,9 +105,7 @@ constructorView (IPi fc rig pinfo x a b) = do constructorView f = do MkAppView _ ts _ <- appView f 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 + let ps = flip mapMaybe (zip ts range) $ flip bitraverse pure $ traverse getIVar pure (MkConstructorView ps []) ------------------------------------------------------------------------------ diff --git a/libs/base/Deriving/Foldable.idr b/libs/base/Deriving/Foldable.idr index 7b200e06f32..00a910c587f 100644 --- a/libs/base/Deriving/Foldable.idr +++ b/libs/base/Deriving/Foldable.idr @@ -143,7 +143,7 @@ parameters {auto error : MonadError Error m} {auto cs : MonadState Parameters m} (t : Name) - (ps : List (Name, Nat)) + (ps : List (Argument Name, Nat)) (x : Name) ||| When analysing the type of a constructor for the type family t, @@ -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 lookup hd ps of + Nothing => case lookupBy (flip $ (==) . unArg) 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 lookup hd ps of + case lookupBy (flip $ (==) . unArg) hd ps of Just n => do -- record that the nth parameter should be bifoldable ns <- gets asBifoldables @@ -344,7 +344,7 @@ namespace Foldable $ 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) + res <- typeView f paras (unArg para) (unArg arg) case res of Left _ => case rig of MW => pure () diff --git a/libs/base/Deriving/Functor.idr b/libs/base/Deriving/Functor.idr index 30cddf02a51..ed4f561d9af 100644 --- a/libs/base/Deriving/Functor.idr +++ b/libs/base/Deriving/Functor.idr @@ -132,7 +132,7 @@ parameters {auto error : MonadError Error m} {auto cs : MonadState Parameters m} (t : Name) - (ps : List (Name, Nat)) + (ps : List (Argument 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 lookup hd ps of + Nothing => case lookupBy (flip $ (==) . unArg) 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 lookup hd ps of + case lookupBy (flip $ (==) . unArg) hd ps of Just n => do -- record that the nth parameter should be bifunctorial ns <- gets asBifunctors @@ -358,7 +358,7 @@ namespace Functor -- 2. explicit recs <- for (zip vars args) $ \ (v, (rig, arg)) => do res <- withError (WhenCheckingArg (mapTTImp cleanup $ unArg arg)) $ - typeView {pol = Positive} f paras para (unArg arg) + typeView {pol = Positive} f paras (unArg para) (unArg arg) pure $ case res of Left sp => -- do not bother with assert_total if you're generating -- a covering/partial definition diff --git a/libs/base/Deriving/Show.idr b/libs/base/Deriving/Show.idr index 84716584322..853b87a6cf7 100644 --- a/libs/base/Deriving/Show.idr +++ b/libs/base/Deriving/Show.idr @@ -150,7 +150,7 @@ parameters {auto error : MonadError Error m} {auto cs : MonadState Parameters m} (t : Name) - (ps : List (Name, Nat)) + (ps : List (Argument Name, Nat)) ||| Hoping to observe that ty can be shown export @@ -168,7 +168,7 @@ parameters let No _ = decEq hd t | Yes Refl => pure (ISRec prf) Just (hdty ** hT) <- hasType hd - | _ => case lookup hd ps <* guard (null ts) of + | _ => case lookupBy (flip $ (==) . unArg) hd ps <* guard (null ts) of Just n => do -- record that the nth parameter should be showable ns <- gets asShowables diff --git a/libs/base/Deriving/Traversable.idr b/libs/base/Deriving/Traversable.idr index a849f0a845c..b17f70479c6 100644 --- a/libs/base/Deriving/Traversable.idr +++ b/libs/base/Deriving/Traversable.idr @@ -122,7 +122,7 @@ parameters {auto error : MonadError Error m} {auto cs : MonadState Parameters m} (t : Name) - (ps : List (Name, Nat)) + (ps : List (Argument Name, Nat)) (x : Name) ||| When analysing the type of a constructor for the type family t, @@ -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 lookup hd ps of + Nothing => case lookupBy (flip $ (==) . unArg) 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 lookup hd ps of + case lookupBy (flip $ (==) . unArg) hd ps of Just n => do -- record that the nth parameter should be bitraversable ns <- gets asBitraversables @@ -368,7 +368,7 @@ namespace Traversable $ 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) + res <- typeView f paras (unArg para) (unArg arg) case res of Left _ => case rig of MW => pure () diff --git a/libs/base/Language/Reflection/TTImp.idr b/libs/base/Language/Reflection/TTImp.idr index 34c6ac3ad43..d81366a4c90 100644 --- a/libs/base/Language/Reflection/TTImp.idr +++ b/libs/base/Language/Reflection/TTImp.idr @@ -652,6 +652,18 @@ Functor Argument where map f (NamedArg fc nm a) = NamedArg fc nm (f a) map f (AutoArg fc a) = AutoArg fc (f a) +public export +Foldable Argument where + foldr f i (Arg _ x) = f x i + foldr f i (NamedArg _ _ x) = f x i + foldr f i (AutoArg _ x) = f x i + +public export +Traversable Argument where + traverse f (Arg fc x) = Arg fc <$> f x + traverse f (NamedArg fc nm x) = NamedArg fc nm <$> f x + traverse f (AutoArg fc x) = AutoArg fc <$> f x + public export iApp : TTImp -> Argument TTImp -> TTImp iApp f (Arg fc t) = IApp fc f t diff --git a/tests/base/deriving_traversable/expected b/tests/base/deriving_traversable/expected index 647d830cf9e..a5c3194e615 100644 --- a/tests/base/deriving_traversable/expected +++ b/tests/base/deriving_traversable/expected @@ -65,7 +65,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:13933} = eq} a -> f (EqMap key {{conArg:13933} = eq} b) + traverseEqMap : {0 key, eq : _} -> {0 a, b : Type} -> {0 f : Type -> Type} -> Applicative f => (a -> f b) -> EqMap key {{conArg:13937} = eq} a -> f (EqMap key {{conArg:13937} = 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)