free-foil 0.0.2 → 0.0.3

raw patch · 12 files changed

+868/−2 lines, 12 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• ChangeLog.md +31/−0
• free-foil.cabal +7/−1
• src/Control/Monad/Foil.hs +8/−1
• src/Control/Monad/Foil/Internal.hs +61/−0
• src/Control/Monad/Foil/Relative.hs +4/−0
• src/Control/Monad/Foil/TH/Util.hs +3/−0
• src/Control/Monad/Free/Foil.hs +231/−0
• src/Control/Monad/Free/Foil/TH.hs +11/−0
• src/Control/Monad/Free/Foil/TH/Convert.hs +272/−0
• src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs +86/−0
• src/Control/Monad/Free/Foil/TH/Signature.hs +97/−0
• src/Control/Monad/Free/Foil/TH/ZipMatch.hs +57/−0

@@ -0,0 +1,31 @@+# CHANGELOG for `free-foil`++# 0.0.3 — 2024-06-20++- Add α-equivalence checks and α-normalization (see [#12](https://github.com/fizruk/free-foil/pull/12)):++  - `Control.Monad.Foil` now offers more helpers to work with binder renaming and binder unification.+    These helpers can be used to implement (efficient) α-equivalence.+  - In `Control.Monad.Free.Foil` general implementation of α-equivalence and α-normalization is provided.++- Add general conversion functions for free foil (see [#14](https://github.com/fizruk/free-foil/pull/14)):++  - `Control.Monad.Free.Foil` now offers `convertToAST` and `convertFromAST` functions+    enabling easier implementation of conversions raw and scope-safe representations.++- Add Template Haskell functions for free foil (see [#14](https://github.com/fizruk/free-foil/pull/14)):++  - `Control.Monad.Free.Foil.TH` contains many useful functions to generate free foil from+    a raw representation (e.g. generated via BNFC), including generation of the signature,+    convenient pattern synonyms, `ZipMatch` instance, and conversion helpers.++# 0.0.2 — 2024-06-18++- Improve TH to support parametrized data types (see [#11](https://github.com/fizruk/free-foil/pull/11))+- Split `lambda-pi` into its own package (see [#10](https://github.com/fizruk/free-foil/pull/10))+- Switch to `template-haskell >= 2.21.0.0` (to support latest Stackage Nightly)+- Fix doctests (see [#9](https://github.com/fizruk/free-foil/pull/9))++# 0.0.1 — 2024-06-08++First release, corresponding to the ICCQ 2024 paper.

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           free-foil-version:        0.0.2+version:        0.0.3 synopsis:       Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads) description:    Please see the README on GitHub at <https://github.com/fizruk/free-foil#readme> category:       Parsing@@ -19,6 +19,7 @@ build-type:     Simple extra-source-files:     README.md+    ChangeLog.md     LICENSE  source-repository head@@ -39,6 +40,11 @@       Control.Monad.Foil.TH.Util       Control.Monad.Free.Foil       Control.Monad.Free.Foil.Example+      Control.Monad.Free.Foil.TH+      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:

@@ -28,11 +28,14 @@   withFresh,   withRefreshed,   unsinkName,-  -- * Safe (co)sinking+  -- * Safe (co)sinking and renaming   Sinkable(..),   CoSinkable(..),   sink,   extendRenaming,+  extendNameBinderRenaming,+  composeNameBinderRenamings,+  fromNameBinderRenaming,   extendRenamingNameBinder,   -- * Safe substitutions   Substitution,@@ -40,6 +43,9 @@   identitySubst,   addSubst,   addRename,+  -- * Unification of binders+  UnifyNameBinders(..),+  unifyNameBinders,   -- * Name maps   NameMap,   emptyNameMap,@@ -51,6 +57,7 @@   Distinct,   DistinctEvidence(..),   assertDistinct,+  assertExt,   DExt,   InjectName(..), ) where

@@ -40,6 +40,7 @@ import qualified Data.IntSet     as IntSet import           Data.Kind       (Type) import           Unsafe.Coerce+import Data.Coerce (coerce)  -- * Safe types and operations @@ -134,6 +135,10 @@ assertDistinct :: Distinct n => NameBinder n l -> DistinctEvidence l assertDistinct _ = unsafeDistinct +-- | A distinct scope extended with a 'NameBinder' is also distinct.+assertExt :: NameBinder n l -> ExtEvidence n l+assertExt _ = unsafeExt+ -- | Safely rename (if necessary) a given name to extend a given scope. -- This is similar to 'withFresh', except if the name does not clash with -- the scope, it can be used immediately, without renaming.@@ -155,6 +160,37 @@   | nameOf binder == name = Nothing   | otherwise = Just (UnsafeName raw) +-- * Unification of binders++-- | Unification result for two binders,+-- extending some common scope to scopes @l@ and @r@ respectively.+--+-- Due to the implementation of the foil,+data UnifyNameBinders n l r where+  -- | Binders are the same, proving that type parameters @l@ and @r@+  -- are in fact equivalent.+  SameNameBinders :: UnifyNameBinders n l l+  -- | It is possible to safely rename the left binder+  -- to match the right one.+  RenameLeftNameBinder :: (NameBinder n l -> NameBinder n r) -> UnifyNameBinders n l r+  -- | It is possible to safely rename the right binder+  -- to match the left one.+  RenameRightNameBinder :: (NameBinder n r -> NameBinder n l) -> UnifyNameBinders n l r++-- | Unify binders either by asserting that they are the same,+-- or by providing a /safe/ renaming function to convert one binder to another.+unifyNameBinders+  :: forall i l r.+     NameBinder i l+  -> NameBinder i r+  -> UnifyNameBinders i l r+unifyNameBinders (UnsafeNameBinder (UnsafeName i1)) (UnsafeNameBinder (UnsafeName i2))+  | i1 == i2  = unsafeCoerce (SameNameBinders @l)  -- equal names extend scopes equally+  | i1 < i2   = RenameRightNameBinder $ \(UnsafeNameBinder (UnsafeName i'')) ->+      if i'' == i2 then UnsafeNameBinder (UnsafeName i1) else UnsafeNameBinder (UnsafeName i'')+  | otherwise = RenameLeftNameBinder $ \(UnsafeNameBinder (UnsafeName i')) ->+      if i'  == i1 then UnsafeNameBinder (UnsafeName i2) else UnsafeNameBinder (UnsafeName i')+ -- * Safe sinking  -- | Sinking an expression from scope @n@ into a (usualy extended) scope @l@,@@ -195,6 +231,31 @@   -> r extendRenaming _ pattern cont =   cont unsafeCoerce (unsafeCoerce pattern)++-- | Extend renaming of binders when going under a 'CoSinkable' pattern (generalized binder).+-- Note that the scope under pattern is independent of the codomain of the renaming.+extendNameBinderRenaming+  :: CoSinkable pattern+  => (NameBinder i n -> NameBinder i n')  -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@.+  -> pattern n l          -- ^ A pattern that extends scope @n@ to another scope @l@.+  -> (forall l'. (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r )+  -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)+  -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.+  -> r+extendNameBinderRenaming _ pattern cont =+  cont unsafeCoerce (unsafeCoerce pattern)++-- | Safely compose renamings of name binders.+-- The underlying implementation is+composeNameBinderRenamings+  :: (NameBinder n i -> NameBinder n i')    -- ^ Rename binders extending scope @n@ from @i@ to @i'@.+  -> (NameBinder i' l -> NameBinder i' l')  -- ^ Rename binders extending scope @i'@ from @l@ to @l'@.+  -> (NameBinder n l -> NameBinder n l')+composeNameBinderRenamings = unsafeCoerce (flip (.))++-- | Convert renaming of name binders into renaming of names in the inner scopes.+fromNameBinderRenaming :: (NameBinder n l -> NameBinder n l') -> Name l -> Name l'+fromNameBinderRenaming = coerce  -- | Extend renaming when going under a 'NameBinder'. -- Note that the scope under binder is independent of the codomain of the renaming.

@@ -21,3 +21,7 @@   -- Also, we could probably treat types in 'S' as singletons and extract distinct scopes that way,   -- preserving the more general type signature for 'rbind'.   rbind :: Distinct b => Scope b -> m a -> (f a -> m b) -> m b++-- | Relative version of 'liftM' (an 'fmap' restricted to 'Monad').+liftRM :: (RelMonad f m, Distinct b) => Scope b -> (f a -> f b) -> m a -> m b+liftRM scope f m = rbind scope m (rreturn . f)

@@ -24,3 +24,6 @@ tvarName = \case   PlainTV name _ -> name   KindedTV name _ _ -> name++removeName :: VarBangType -> BangType+removeName (_name, bang_, type_) = (bang_, type_)

@@ -8,6 +8,7 @@ {-# LANGUAGE MultiParamTypeClasses #-} {-# LANGUAGE PolyKinds             #-} {-# LANGUAGE QuantifiedConstraints #-}+{-# LANGUAGE ScopedTypeVariables   #-} {-# LANGUAGE StandaloneDeriving    #-} {-# LANGUAGE UndecidableInstances  #-} -- | This module defines a variation of@@ -20,7 +21,13 @@ import           Control.DeepSeq import qualified Control.Monad.Foil.Internal as Foil import qualified Control.Monad.Foil.Relative as Foil+import           Data.Bifoldable import           Data.Bifunctor+import           Data.Bifunctor.Sum+import           Data.Coerce                 (coerce)+import           Data.Map                    (Map)+import qualified Data.Map                    as Map+import           Data.Monoid                 (All (..)) import           GHC.Generics                (Generic)  -- | Scoped term under a (single) name binder.@@ -53,6 +60,8 @@ instance Foil.InjectName (AST sig) where   injectName = Var +-- * Substitution+ -- | Substitution for free (scoped monads). substitute   :: (Bifunctor sig, Foil.Distinct o)@@ -71,6 +80,31 @@             body' = substitute scope' subst' body         in ScopedAST binder' body' +-- | Substitution for free (scoped monads).+--+-- This is a version of 'substitute' that forces refreshing of all name binders,+-- resulting in a term with normalized binders:+--+-- > substituteRefreshed scope subst = refreshAST scope . subtitute scope subst+--+-- In general, 'substitute' is more efficient since it does not always refresh binders.+substituteRefreshed+  :: (Bifunctor sig, Foil.Distinct o)+  => Foil.Scope o+  -> Foil.Substitution (AST sig) i o+  -> AST sig i+  -> AST sig o+substituteRefreshed scope subst = \case+  Var name -> Foil.lookupSubst subst name+  Node node -> Node (bimap f (substituteRefreshed scope subst) node)+  where+    f (ScopedAST binder body) =+      Foil.withFresh scope $ \binder' ->+        let subst' = Foil.addRename (Foil.sink subst) binder (Foil.nameOf binder')+            scope' = Foil.extendScope binder' scope+            body' = substituteRefreshed scope' subst' body+        in ScopedAST binder' body'+ -- | @'AST' sig@ is a monad relative to 'Foil.Name'. instance Bifunctor sig => Foil.RelMonad Foil.Name (AST sig) where   rreturn = Var@@ -87,3 +121,200 @@                           Nothing -> Foil.rreturn (Foil.nameOf binder')                           Just n  -> Foil.sink (subst n)            in ScopedAST binder' (Foil.rbind scope' body subst')++-- * \(\alpha\)-equivalence++-- | Refresh (force) all binders in a term, minimizing the used indices.+refreshAST+  :: (Bifunctor sig, Foil.Distinct n)+  => Foil.Scope n+  -> AST sig n+  -> AST sig n+refreshAST scope = \case+  t@Var{} -> t+  Node t -> Node (bimap (refreshScopedAST scope) (refreshAST scope) t)++-- | Similar to `refreshAST`, but for scoped terms.+refreshScopedAST :: (Bifunctor sig, Foil.Distinct n)+  => Foil.Scope n+  -> ScopedAST sig n+  -> ScopedAST sig n+refreshScopedAST scope (ScopedAST binder body) =+  Foil.withFresh scope $ \binder' ->+    let scope' = Foil.extendScope binder' scope+        subst = Foil.addRename (Foil.sink Foil.identitySubst) binder (Foil.nameOf binder')+    in ScopedAST binder' (substituteRefreshed scope' subst body)++-- | \(\alpha\)-equivalence check for two terms in one scope+-- via normalization of bound identifiers (via 'refreshAST').+--+-- Compared to 'alphaEquiv', this function may perform some unnecessary+-- changes of bound variables when the binders are the same on both sides.+alphaEquivRefreshed+  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n)+  => Foil.Scope n+  -> AST sig n+  -> AST sig n+  -> Bool+alphaEquivRefreshed scope t1 t2 = refreshAST scope t1 `unsafeEqAST` refreshAST scope t2++-- | \(\alpha\)-equivalence check for two terms in one scope+-- via unification of bound variables (via 'unifyNameBinders').+--+-- Compared to 'alphaEquivRefreshed', this function might skip unnecessary+-- changes of bound variables when both binders in two matching scoped terms coincide.+alphaEquiv+  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n)+  => Foil.Scope n+  -> AST sig n+  -> AST sig n+  -> Bool+alphaEquiv _scope (Var x) (Var y) = x == coerce y+alphaEquiv scope (Node l) (Node r) =+  case zipMatch l r of+    Nothing -> False+    Just tt -> getAll (bifoldMap (All . uncurry (alphaEquivScoped scope)) (All . uncurry (alphaEquiv scope)) tt)+alphaEquiv _ _ _ = False++-- | Same as 'alphaEquiv' but for scoped terms.+alphaEquivScoped+  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n)+  => Foil.Scope n+  -> ScopedAST sig n+  -> ScopedAST sig n+  -> Bool+alphaEquivScoped scope+  (ScopedAST binder1 body1)+  (ScopedAST binder2 body2) =+    case Foil.unifyNameBinders binder1 binder2 of+      -- if binders are the same, then we can safely compare bodies+      Foil.SameNameBinders ->  -- after seeing this we know that body scopes are the same+        case Foil.assertDistinct binder1 of+          Foil.Distinct ->+            let scope1 = Foil.extendScope binder1 scope+            in alphaEquiv scope1 body1 body2+      -- if we can safely rename first binder into second+      Foil.RenameLeftNameBinder rename1to2 ->+        case Foil.assertDistinct binder2 of+          Foil.Distinct ->+            let scope2 = Foil.extendScope binder2 scope+            in alphaEquiv scope2 (Foil.liftRM scope2 (Foil.fromNameBinderRenaming rename1to2) body1) body2+      -- if we can safely rename second binder into first+      Foil.RenameRightNameBinder rename2to1 ->+        case Foil.assertDistinct binder1 of+          Foil.Distinct ->+            let scope1 = Foil.extendScope binder1 scope+            in alphaEquiv scope1 body1 (Foil.liftRM scope1 (Foil.fromNameBinderRenaming rename2to1) body2)++-- ** Unsafe equality checks++-- | /Unsafe/ equality check for two terms.+-- This check ignores the possibility that two terms might have different+-- scope extensions under binders (which might happen due to substitution+-- under a binder in absence of name conflicts).+unsafeEqAST+  :: (Bifoldable sig, ZipMatch sig)+  => AST sig n+  -> AST sig l+  -> Bool+unsafeEqAST (Var x) (Var y) = x == coerce y+unsafeEqAST (Node t1) (Node t2) =+  case zipMatch t1 t2 of+    Nothing -> False+    Just tt -> getAll (bifoldMap (All . uncurry unsafeEqScopedAST) (All . uncurry unsafeEqAST) tt)+unsafeEqAST _ _ = False++-- | A version of 'unsafeEqAST' for scoped terms.+unsafeEqScopedAST+  :: (Bifoldable sig, ZipMatch sig)+  => ScopedAST sig n+  -> ScopedAST sig l+  -> Bool+unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and+  [ binder1 == coerce binder2+  , body1 `unsafeEqAST` body2+  ]++-- ** Syntactic matching (unification)++-- | Perform one-level matching for the two (non-variable) terms.+class ZipMatch sig where+  zipMatch+    :: sig scope term     -- ^ Left non-variable term.+    -> sig scope' term'   -- ^ Right non-variable term.+    -> Maybe (sig (scope, scope') (term, term'))++instance (ZipMatch f, ZipMatch g) => ZipMatch (Sum f g) where+  zipMatch (L2 f) (L2 f') = L2 <$> zipMatch f f'+  zipMatch (R2 g) (R2 g') = R2 <$> zipMatch g g'+  zipMatch _ _            = Nothing++-- * Converting to and from free foil++-- ** Convert to free foil++convertToAST+  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent)+  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))+  -> (rawPattern -> Maybe rawIdent)+  -> (rawScopedTerm -> rawTerm)+  -> Foil.Scope n+  -> Map rawIdent (Foil.Name n) -> rawTerm -> AST sig n+convertToAST toSig getPatternBinder getScopedTerm scope names t =+  case toSig t of+    Left x ->+      case Map.lookup x names of+        Nothing   -> error "undefined variable"+        Just name -> Var name+    Right node -> Node $+      bimap+        (convertToScopedAST toSig getPatternBinder getScopedTerm scope names)+        (convertToAST toSig getPatternBinder getScopedTerm scope names)+        node++convertToScopedAST+  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent)+  => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))+  -> (rawPattern -> Maybe rawIdent)+  -> (rawScopedTerm -> rawTerm)+  -> Foil.Scope n+  -> Map rawIdent (Foil.Name n)+  -> (rawPattern, rawScopedTerm)+  -> ScopedAST sig n+convertToScopedAST toSig getPatternBinder getScopedTerm scope names (pat, scopedTerm) =+  Foil.withFresh scope $ \binder ->+    let scope' = Foil.extendScope binder scope+        names' =+          case getPatternBinder pat of+            Nothing -> Foil.sink <$> names+            Just x  -> Map.insert x (Foil.nameOf binder) (Foil.sink <$> names)+     in ScopedAST binder (convertToAST toSig getPatternBinder getScopedTerm scope' names' (getScopedTerm scopedTerm))++-- ** Convert from free foil++convertFromAST+  :: Bifunctor sig+  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)+  -> (rawIdent -> rawTerm)+  -> (rawIdent -> rawPattern)+  -> (rawTerm -> rawScopedTerm)+  -> (Int -> rawIdent) -> AST sig n -> rawTerm+convertFromAST fromSig fromVar makePattern makeScoped f = \case+  Var x -> fromVar (f (Foil.nameId x))+  Node node -> fromSig $+    bimap+      (convertFromScopedAST fromSig fromVar makePattern makeScoped f)+      (convertFromAST fromSig fromVar makePattern makeScoped f)+      node++convertFromScopedAST+  :: Bifunctor sig+  => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)+  -> (rawIdent -> rawTerm)+  -> (rawIdent -> rawPattern)+  -> (rawTerm -> rawScopedTerm)+  -> (Int -> rawIdent) -> ScopedAST sig n -> (rawPattern, rawScopedTerm)+convertFromScopedAST fromSig fromVar makePattern makeScoped f = \case+  ScopedAST binder body ->+    ( makePattern (f (Foil.nameId (Foil.nameOf binder)))+    , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body))

@@ -0,0 +1,11 @@+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

@@ -0,0 +1,272 @@+{-# LANGUAGE LambdaCase      #-}+{-# OPTIONS_GHC -fno-warn-type-defaults      #-}+{-# LANGUAGE TemplateHaskell #-}+module Control.Monad.Free.Foil.TH.Convert where++import           Language.Haskell.TH+import           Language.Haskell.TH.Syntax++import           Control.Monad.Foil.TH.Util++-- * Bulk generators++-- | Generate helpers for conversion to scope-safe representation.+-- Includes 'mkConvertToSig', 'mkGetPatternBinder', and 'mkGetScopedTerm'.+mkConvertToFreeFoil+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw scoped terms.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkConvertToFreeFoil termT nameT scopeT patternT = concat <$> sequence+  [ mkConvertToSig termT nameT scopeT patternT+  , mkGetPatternBinder nameT patternT+  , mkGetScopedTerm termT scopeT+  ]++-- | Generate helpers for conversion from scope-safe representation.+-- Includes 'mkConvertFromSig'.+mkConvertFromFreeFoil+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw scoped terms.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkConvertFromFreeFoil termT nameT scopeT patternT = concat <$> sequence+  [ mkConvertFromSig termT nameT scopeT patternT+  ]++-- * Individual generators++-- | Generate conversion helper that goes unpeels one node from a raw term.+mkConvertToSig+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw scoped terms.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkConvertToSig termT nameT scopeT patternT = do+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT+  TyConI (NewtypeD _ctx _name nameTVars _kind _nameCons _deriv) <- reify nameT++  convertTermToSigClauses <- concat <$> mapM toClause termCons++  let params = map (VarT . tvarName) termTVars+      termType = return $ PeelConT termT params+      nameType = return $ PeelConT nameT (map (VarT . tvarName) nameTVars)+      scopeType = return $ PeelConT scopeT params+      patternType = return $ PeelConT patternT params+      signatureType = return $ PeelConT signatureT params+  convertTermToSigClausesType <-+    [t| $termType -> Either $nameType ($signatureType ($patternType, $scopeType) $termType) |]++  addModFinalizer $ putDoc (DeclDoc convertTermToSigT)+    ("/Generated/ with '" ++ show 'mkConvertToFreeFoil ++ "'. Perform one step of converting '" ++ show termT ++ "', peeling off one node of type '" ++ show signatureT ++ "'.")+  return+    [ SigD convertTermToSigT convertTermToSigClausesType+    , FunD convertTermToSigT convertTermToSigClauses+    ]+  where+    signatureT = mkName (nameBase termT ++ "Sig")+    convertTermToSigT = mkName ("convertTo" ++ nameBase signatureT)++    toClause :: Con -> Q [Clause]+    toClause = \case+      NormalC conName types | any isVarP pats+        -> return [Clause [ConP conName [] pats] (NormalB (AppE (ConE 'Left) (VarE x))) []]+        where+          x = mkName "x"+          isVarP VarP{} = True+          isVarP _ = False+          pats =+            [ case type_ of+                PeelConT typeName _ | typeName == nameT -> VarP x+                _ -> WildP+            | (_bang, type_) <- types ]+      NormalC conName types -> mkClause conName conName' types+        where+          conName' = mkName (nameBase conName ++ "Sig")+      RecC conName types -> toClause (NormalC conName (map removeName types))+      InfixC l conName r -> mkClause conName conName' [l, r]+        where+          conName' = mkName (nameBase conName ++ "---")+      ForallC _ _ con -> toClause con+      GadtC conNames types _retType -> concat <$> mapM (\conName -> toClause (NormalC conName types)) conNames+      RecGadtC conNames types retType -> toClause (GadtC conNames (map removeName types) retType)++    mkClause conName conName' types = return+      [ Clause [ConP conName [] pats] (NormalB (AppE (ConE 'Right) (foldl AppE (ConE conName') (concat args)))) [] ]+      where+        p = mkName "p"+        (pats, args) = unzip+          [ case type_ of+              PeelConT typeName _+                | typeName == patternT -> (VarP p, [])+                | typeName == scopeT -> (VarP x, [TupE [Just (VarE p), Just (VarE x)]])+              _ -> (VarP x, [VarE x])+          | (i, (_bang, type_)) <- zip [0..] types+          , let x = mkName ("x" ++ show i)+          ]++-- | Generate conversion helper that peels back one node to a raw term.+mkConvertFromSig+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw scoped terms.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkConvertFromSig termT nameT scopeT patternT = do+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT+  TyConI (NewtypeD _ctx _name _nameTVars _kind _nameCons _deriv) <- reify nameT++  convertTermFromSigClauses <- concat <$> mapM toClause termCons++  let params = map (VarT . tvarName) termTVars+      termType = return $ PeelConT termT params+      scopeType = return $ PeelConT scopeT params+      patternType = return $ PeelConT patternT params+      signatureType = return $ PeelConT signatureT params+  convertTermFromSigClausesType <-+    [t| $signatureType ($patternType, $scopeType) $termType -> $termType |]++  addModFinalizer $ putDoc (DeclDoc convertTermFromSigT)+    ("/Generated/ with '" ++ show 'mkConvertToFreeFoil ++ "'. Perform one step of converting '" ++ show termT ++ "', peeling off one node of type '" ++ show signatureT ++ "'.")+  return+    [ SigD convertTermFromSigT convertTermFromSigClausesType+    , FunD convertTermFromSigT convertTermFromSigClauses+    ]+  where+    signatureT = mkName (nameBase termT ++ "Sig")+    convertTermFromSigT = mkName ("convertFrom" ++ nameBase signatureT)++    toClause :: Con -> Q [Clause]+    toClause = \case+      NormalC _conName types | or [ typeName == nameT | (_bang, PeelConT typeName _typeParams) <- types ]+        -> pure []+      NormalC conName types -> mkClause conName conName' types+        where+          conName' = mkName (nameBase conName ++ "Sig")+      RecC conName types -> toClause (NormalC conName (map removeName types))+      InfixC l conName r -> mkClause conName conName' [l, r]+        where+          conName' = mkName (nameBase conName ++ "---")+      ForallC _ _ con -> toClause con+      GadtC conNames types _retType -> concat <$> mapM (\conName -> toClause (NormalC conName types)) conNames+      RecGadtC conNames types retType -> toClause (GadtC conNames (map removeName types) retType)++    mkClause conName conName' types = return+      [ Clause [ConP conName' [] (concat pats)] (NormalB (foldl AppE (ConE conName) args)) [] ]+      where+        p = mkName "p"+        (args, pats) = unzip+          [ case type_ of+              PeelConT typeName _+                | typeName == patternT -> (VarE p, [])+                | typeName == scopeT -> (VarE x, [TupP [VarP p, VarP x]])+              _ -> (VarE x, [VarP x])+          | (i, (_bang, type_)) <- zip [0..] types+          , let x = mkName ("x" ++ show i)+          ]++-- | Generate a helper that extracts at most one binder from a pattern.+mkGetPatternBinder+  :: Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkGetPatternBinder nameT patternT = do+  TyConI (NewtypeD _ctx _name nameTVars _kind _nameCons _deriv) <- reify nameT+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT++  getPatternBinderClauses <- concat <$> mapM toClause patternCons++  let nameType = return $ PeelConT nameT (map (VarT . tvarName) nameTVars)+      patternType = return $ PeelConT patternT (map (VarT . tvarName) patternTVars)+  getPatternBinderClausesType <-+    [t| $patternType -> Maybe $nameType |]++  addModFinalizer $ putDoc (DeclDoc getPatternBinderT)+    ("/Generated/ with '" ++ show 'mkGetPatternBinder ++ "'. Extract at most one binder from a pattern or __crash__.")+  return+    [ SigD getPatternBinderT getPatternBinderClausesType+    , FunD getPatternBinderT getPatternBinderClauses+    ]+  where+    getPatternBinderT = mkName ("get" ++ nameBase patternT ++ "Binder")++    toClause :: Con -> Q [Clause]+    toClause = \case+      NormalC conName types -> mkClause conName types+      RecC conName types -> toClause (NormalC conName (map removeName types))+      InfixC l conName r -> toClause (NormalC conName [l, r])+      ForallC _ _ con -> toClause con+      GadtC conNames types _retType -> concat <$> mapM (\conName -> mkClause conName types) conNames+      RecGadtC conNames types retType -> toClause (GadtC conNames (map removeName types) retType)++    mkClause :: Name -> [BangType] -> Q [Clause]+    mkClause conName types = do+      body <- case concat vars of+        [] -> [e| Nothing |]+        [Just y] -> [e| Just $y |]+        _ -> [e| error "complex patterns are not supported" |]+      return [ Clause [ConP conName [] pats] (NormalB body) [] ]+      where+        x = mkName "x"+        (pats, vars) = unzip+          [ case type_ of+              PeelConT typeName _+                | typeName == nameT -> (VarP x, [Just (return (VarE x))])+                | typeName == patternT -> (WildP, [Nothing])+              _ -> (WildP, [])+          | (_bang, type_) <- types+          ]++-- | Generate a helper that extracts a term from a scoped term.+mkGetScopedTerm+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw scoped terms.+  -> Q [Dec]+mkGetScopedTerm termT scopeT = do+  TyConI (DataD _ctx _name termTVars _kind _termCons _deriv) <- reify termT+  TyConI (DataD _ctx _name _scopeTVars _kind scopeCons _deriv) <- reify scopeT++  getScopedTermClauses <- concat <$> mapM toClause scopeCons++  let params = map (VarT . tvarName) termTVars+      termType = return $ PeelConT termT params+      scopeType = return $ PeelConT scopeT params+  getScopedTermClausesType <-+    [t| $scopeType -> $termType |]++  addModFinalizer $ putDoc (DeclDoc getScopedTermT)+    ("/Generated/ with '" ++ show 'mkGetScopedTerm ++ "'. Extract scoped term or __crash__.")+  return+    [ SigD getScopedTermT getScopedTermClausesType+    , FunD getScopedTermT getScopedTermClauses+    ]+  where+    getScopedTermT = mkName ("get" ++ nameBase termT ++ "From" ++ nameBase scopeT)++    toClause :: Con -> Q [Clause]+    toClause = \case+      NormalC conName types -> mkClause conName types+      RecC conName types -> toClause (NormalC conName (map removeName types))+      InfixC l conName r -> toClause (NormalC conName [l, r])+      ForallC _ _ con -> toClause con+      GadtC conNames types _retType -> concat <$> mapM (\conName -> mkClause conName types) conNames+      RecGadtC conNames types retType -> toClause (GadtC conNames (map removeName types) retType)++    mkClause :: Name -> [BangType] -> Q [Clause]+    mkClause conName types = do+      body <- case concat vars of+        [y] -> [e| $y |]+        _ -> [e| error "complex patterns are not supported" |]+      return [ Clause [ConP conName [] pats] (NormalB body) [] ]+      where+        x = mkName "x"+        (pats, vars) = unzip+          [ case type_ of+              PeelConT typeName _+                | typeName == termT -> (VarP x, [return (VarE x)])+              _ -> (WildP, [])+          | (_bang, type_) <- types+          ]

@@ -0,0 +1,86 @@+{-# LANGUAGE LambdaCase      #-}+{-# OPTIONS_GHC -fno-warn-type-defaults      #-}+{-# LANGUAGE PatternSynonyms #-}+{-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE ViewPatterns    #-}+module Control.Monad.Free.Foil.TH.PatternSynonyms where++import Control.Monad (forM_)+import qualified Control.Monad.Foil         as Foil+import           Control.Monad.Foil.TH.Util+import           Control.Monad.Free.Foil+import           Language.Haskell.TH+import           Language.Haskell.TH.Syntax++-- | Generate helpful pattern synonyms given a signature bifunctor.+mkPatternSynonyms+  :: Name -- ^ Type name for the signature bifunctor.+  -> Q [Dec]+mkPatternSynonyms signatureT = do+  TyConI (DataD _ctx _name signatureTVars _kind signatureCons _deriv) <- reify signatureT++  case reverse signatureTVars of+    (tvarName -> term) : (tvarName -> scope) : (reverse -> params) -> do+      concat <$> mapM (mkPatternSynonym (PeelConT signatureT (map (VarT . tvarName) params)) scope term) signatureCons+    _ -> fail "cannot generate pattern synonyms"++mkPatternSynonym :: Type -> Name -> Name -> Con -> Q [Dec]+mkPatternSynonym signatureType scope term = \case+  NormalC conName types -> mkPatternSynonym signatureType scope term+    (GadtC [conName] types (AppT (AppT signatureType (VarT scope)) (VarT term)))++  RecC conName types -> mkPatternSynonym signatureType scope term (NormalC conName (map removeName types))++  InfixC l conName r -> mkPatternSynonym signatureType scope term (NormalC conName [l, r])++  ForallC params ctx con -> do+    [ PatSynSigD patName patType, patD ] <- mkPatternSynonym signatureType scope term con+    return+      [ PatSynSigD patName (ForallT params ctx patType)+      , patD+      ]++  GadtC conNames types _retType -> do+    let argsWithTypes = zipWith toPatternArgType [0..] types+        argsWithTypes' = foldMap collapse argsWithTypes+        pats   = map toArg argsWithTypes+        args  = map fst argsWithTypes'+        types' = map snd argsWithTypes'+    forM_ conNames $ \conName ->+      addModFinalizer $ putDoc (DeclDoc (mkPatternName conName))+        ("/Generated/ with '" ++ show 'mkPatternSynonyms ++ "'. Pattern synonym for an '" ++ show ''AST ++ "' node of type '" ++ show conName ++ "'.")+    return $ concat+      [ [ PatSynSigD patternName (foldr (AppT . AppT ArrowT) termType types')+        , PatSynD  patternName (PrefixPatSyn args) ImplBidir (ConP 'Node [] [ConP conName [] pats])+        ]+      | conName <- conNames+      , let patternName = mkPatternName conName+      ]++  RecGadtC conNames types retType -> mkPatternSynonym signatureType scope term (GadtC conNames (map removeName types) retType)++  where+    n = mkName "n"+    termType = PeelConT ''AST [signatureType, VarT n]+    toArg = \case+      Left ((b, _), (x, _)) -> ConP 'ScopedAST [] [VarP b, VarP x]+      Right (x, _) -> VarP x++    toPatternArgType i (_bang, VarT typeName)+      | typeName == scope =+          Left+            ( (mkName ("b" ++ show i), PeelConT ''Foil.NameBinder [VarT n, VarT l])+            , (mkName ("x" ++ show i), PeelConT ''AST [signatureType, VarT l]))+      | typeName == term =+          Right (mkName ("x" ++ show i), PeelConT ''AST [signatureType, VarT n])+      where+        l = mkName ("l" ++ show i)+    toPatternArgType i (_bang, type_)+      = Right (mkName ("z" ++ show i), type_)++    mkPatternName conName = mkName (dropEnd (length "Sig") (nameBase conName))+    dropEnd k = reverse . drop k . reverse++    collapse = \case+      Left (x, y) -> [x, y]+      Right x -> [x]

@@ -0,0 +1,97 @@+{-# LANGUAGE LambdaCase      #-}+{-# LANGUAGE TemplateHaskell #-}+module Control.Monad.Free.Foil.TH.Signature where++import           Language.Haskell.TH+import           Language.Haskell.TH.Syntax++import           Control.Monad              (forM_)+import           Control.Monad.Foil.TH.Util+import           Data.Maybe                 (catMaybes)++-- | Generate a signature for the free foil (or free scoped monads)+-- based on a naïve recursive abstract syntax representation,+-- with clearly separated types for terms, variable identifiers, scoped terms,+-- and patterns (binders).+mkSignature+  :: Name -- ^ Type name for raw terms.+  -> Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw scoped terms.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkSignature termT nameT scopeT patternT = do+  scope <- newName "scope"+  term <- newName "term"+  TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT++  signatureCons <- catMaybes <$> mapM (toSignatureCons scope term) termCons++  addModFinalizer $ putDoc (DeclDoc signatureT)+    ("/Generated/ with '" ++ show 'mkSignature ++ "'. A signature bifunctor, specifying the nodes of a syntax tree corresponding to '" ++ show termT ++ "'.")+  return+    [ DataD [] signatureT (termTVars ++ [PlainTV scope BndrReq, PlainTV term BndrReq]) Nothing signatureCons+      [DerivClause Nothing [ConT ''Functor, ConT ''Foldable, ConT ''Traversable]]+    ]+  where+    signatureT = mkName (nameBase termT ++ "Sig")++    toSignatureCons :: Name -> Name -> Con -> Q (Maybe Con)+    toSignatureCons scope term con' = case con' of+      -- treat constructors with a single variable field as variable constructor and ignore+      NormalC _conName types | or [ typeName == nameT | (_bang, PeelConT typeName _typeParams) <- types ]+        -> pure Nothing+      RecC _conName types | or [ typeName == nameT | (_name, _bang, PeelConT typeName _typeParams) <- types ]+        -> pure Nothing++      NormalC conName params -> do+        addModFinalizer $ putDoc (DeclDoc conName') ("Corresponds to '" ++ show conName ++ "'.")+        Just . NormalC conName' . catMaybes <$> mapM toSignatureParam params+        where+          conName' = mkName (nameBase conName ++ "Sig")+      RecC conName params -> do+        addModFinalizer $ putDoc (DeclDoc conName') ("Corresponds to '" ++ show conName ++ "'.")+        Just . RecC conName' . catMaybes <$> mapM toSignatureParam' params+        where+          conName' = mkName (nameBase conName ++ "Sig")+      InfixC l conName r -> do+        addModFinalizer $ putDoc (DeclDoc conName') ("Corresponds to '" ++ show conName ++ "'.")+        Just <$> (flip InfixC conName' <$> toInfixParam l <*> toInfixParam r)+        where+          conName' = mkName (nameBase conName ++ "---")+      ForallC params ctx con -> fmap (ForallC params ctx) <$> toSignatureCons scope term con+      GadtC conNames argTypes retType -> do+        let conNames' = map (\conName -> mkName (nameBase conName ++ "---")) conNames+        forM_ (zip conNames conNames') $ \(conName, conName') ->+          addModFinalizer $ putDoc (DeclDoc conName') ("Corresponds to '" ++ show conName ++ "'.")+        Just <$> (GadtC conNames' <$> (catMaybes <$> mapM toSignatureParam argTypes) <*> retType')+        where+          retType' = case retType of+            PeelConT typeName typeParams+              | typeName == termT -> return (PeelConT signatureT (typeParams ++ [VarT scope, VarT term]))+            _ -> fail "unexpected return type in a GADT constructor"+      RecGadtC conNames argTypes retType -> do+        let conNames' = map (\conName -> mkName (nameBase conName ++ "---")) conNames+        forM_ (zip conNames conNames') $ \(conName, conName') ->+          addModFinalizer $ putDoc (DeclDoc conName') ("Corresponds to '" ++ show conName ++ "'.")+        Just <$> (RecGadtC conNames' <$> (catMaybes <$> mapM toSignatureParam' argTypes) <*> retType')+        where+          retType' = case retType of+            PeelConT typeName typeParams+              | typeName == termT -> return (PeelConT signatureT (typeParams ++ [VarT scope, VarT term]))+            _ -> fail "unexpected return type in a GADT constructor"++      where+        toInfixParam (bang_, type_) = toSignatureParam (bang_, type_) >>= \case+          Nothing -> pure (bang_, VarT ''())+          Just bt -> pure bt++        toSignatureParam' (name, bang_, type_) = fmap k <$> toSignatureParam (bang_, type_)+          where+            k (x, y) = (name, x, y)++        toSignatureParam (bang_, PeelConT typeName _typeParams)+          | typeName == nameT = fail ("variable with other stuff in constructor: " ++ show con')+          | typeName == patternT = pure Nothing -- skip binders, they will be inserted automatically with each scoped term+          | typeName == scopeT = pure (Just (bang_, VarT scope))+          | typeName == termT = pure (Just (bang_, VarT term))+        toSignatureParam bt = pure (Just bt)  -- everything else remains as is

@@ -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 'ZipMatch' instance for a given 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)+              ]