Derive ZipMatch with TemplateHaskell

haskell/free-foil/free-foil.cabal

@@ -44,6 +44,7 @@ library
       Control.Monad.Free.Foil.TH.Convert
       Control.Monad.Free.Foil.TH.PatternSynonyms
       Control.Monad.Free.Foil.TH.Signature
+      Control.Monad.Free.Foil.TH.ZipMatch
   other-modules:
       Paths_free_foil
   hs-source-dirs:

haskell/free-foil/src/Control/Monad/Free/Foil/TH.hs

@@ -2,8 +2,10 @@ module Control.Monad.Free.Foil.TH (
   module Control.Monad.Free.Foil.TH.Signature,
   module Control.Monad.Free.Foil.TH.PatternSynonyms,
   module Control.Monad.Free.Foil.TH.Convert,
+  module Control.Monad.Free.Foil.TH.ZipMatch,
 ) where
 
 import Control.Monad.Free.Foil.TH.Signature
 import Control.Monad.Free.Foil.TH.PatternSynonyms
 import Control.Monad.Free.Foil.TH.Convert
+import Control.Monad.Free.Foil.TH.ZipMatch

haskell/free-foil/src/Control/Monad/Free/Foil/TH/ZipMatch.hs

@@ -0,0 +1,57 @@
+{-# LANGUAGE LambdaCase      #-}
+{-# OPTIONS_GHC -fno-warn-type-defaults      #-}
+{-# LANGUAGE ViewPatterns      #-}
+{-# LANGUAGE TemplateHaskell #-}
+module Control.Monad.Free.Foil.TH.ZipMatch where
+
+import           Language.Haskell.TH
+
+import           Control.Monad.Foil.TH.Util
+import           Control.Monad.Free.Foil
+
+-- | Generate helpful pattern synonyms given a signature bifunctor.
+deriveZipMatch
+  :: Name -- ^ Type name for the signature bifunctor.
+  -> Q [Dec]
+deriveZipMatch signatureT = do
+  TyConI (DataD _ctx _name signatureTVars _kind signatureCons _deriv) <- reify signatureT
+
+  case reverse signatureTVars of
+    (tvarName -> term) : (tvarName -> scope) : (reverse -> params) -> do
+      let signatureType = PeelConT signatureT (map (VarT . tvarName) params)
+      clauses <- concat <$> mapM (toClause scope term) signatureCons
+      let defaultClause = Clause [WildP, WildP] (NormalB (ConE 'Nothing)) []
+      let instType = AppT (ConT ''ZipMatch) signatureType
+
+      return
+        [ InstanceD Nothing [] instType
+          [ FunD 'zipMatch (clauses ++ [defaultClause]) ]
+        ]
+    _ -> fail "cannot generate pattern synonyms"
+
+  where
+    toClause :: Name -> Name -> Con -> Q [Clause]
+    toClause scope term = go
+      where
+        go = \case
+          NormalC conName types -> mkClause conName types
+          RecC conName types -> go (NormalC conName (map removeName types))
+          InfixC l conName r -> go (NormalC conName [l, r])
+          ForallC _ _ con -> go con
+          GadtC conNames types _retType -> concat <$> mapM (\conName -> mkClause conName types) conNames
+          RecGadtC conNames types retType -> go (GadtC conNames (map removeName types) retType)
+
+        mkClause :: Name -> [BangType] -> Q [Clause]
+        mkClause conName types = return
+          [Clause [ConP conName [] lpats, ConP conName [] rpats]
+            (NormalB (AppE (ConE 'Just) (foldl AppE (ConE conName) args))) []]
+          where
+            (lpats, rpats, args) = unzip3
+              [ case type_ of
+                  VarT typeName
+                    | typeName `elem` [scope, term] -> (VarP l, VarP r, TupE [Just (VarE l), Just (VarE r)])
+                  _ -> (VarP l, WildP, VarE l)
+              | (i, (_bang, type_)) <- zip [0..] types
+              , let l = mkName ("l" ++ show i)
+              , let r = mkName ("r" ++ show i)
+              ]

haskell/lambda-pi/src/Language/LambdaPi/Impl/FreeFoilTH.hs

@@ -30,6 +30,7 @@ import qualified Language.LambdaPi.Syntax.Print as Raw
 
 -- ** Signature
 mkSignature ''Raw.Term' ''Raw.VarIdent ''Raw.ScopedTerm' ''Raw.Pattern'
+deriveZipMatch ''Term'Sig
 deriveBifunctor ''Term'Sig
 deriveBifoldable ''Term'Sig
 deriveBitraversable ''Term'Sig
@@ -86,17 +87,6 @@ instance IsString (AST (Term'Sig Raw.BNFC'Position) Foil.VoidS) where
 instance Show (AST (Term'Sig a) Foil.VoidS) where
   show = Raw.printTree . fromTerm'
 
-instance ZipMatch (Term'Sig a) where
-  zipMatch (AppSig loc l r) (AppSig _loc l' r') = Just (AppSig loc (l, l') (r, r'))
-  zipMatch (PairSig loc l r) (PairSig _loc l' r') = Just (PairSig loc (l, l') (r, r'))
-  zipMatch (ProductSig loc l r) (ProductSig _loc l' r') = Just (ProductSig loc (l, l') (r, r'))
-  zipMatch (LamSig loc s) (LamSig _loc s') = Just (LamSig loc (s, s'))
-  zipMatch (FirstSig loc t) (FirstSig _loc t') = Just (FirstSig loc (t, t'))
-  zipMatch (SecondSig loc t) (SecondSig _loc t') = Just (SecondSig loc (t, t'))
-  zipMatch (UniverseSig loc) (UniverseSig _loc) = Just (UniverseSig loc)
-  zipMatch (PiSig loc l r) (PiSig _loc l' r') = Just (PiSig loc (l, l') (r, r'))
-  zipMatch _ _ = Nothing
-
 -- ** Evaluation
 
 -- | Compute weak head normal form (WHNF) of a \(\lambda\Pi\)-term.