[ derive ] Refine a constructor view to support implicit args

idris-lang · Oct 17, 2023 · 74e945c · 74e945c
1 parent 6c35157
commit 74e945c
Show file tree

Hide file tree

Showing 8 changed files with 35 additions and 19 deletions.
diff --git 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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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
@@ -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)