free-foil 0.0.3 → 0.1.0

raw patch · 13 files changed

+1058/−227 lines, 13 filesPVP ok

version bump matches the API change (PVP)

API changes (from Hackage documentation)

Files

• ChangeLog.md +28/−0
• free-foil.cabal +1/−1
• src/Control/Monad/Foil.hs +15/−0
• src/Control/Monad/Foil/Internal.hs +469/−54
• src/Control/Monad/Foil/TH/MkFoilData.hs +56/−32
• src/Control/Monad/Foil/TH/MkFromFoil.hs +79/−7
• src/Control/Monad/Foil/TH/MkInstancesFoil.hs +141/−11
• src/Control/Monad/Foil/TH/MkToFoil.hs +108/−18
• src/Control/Monad/Free/Foil.hs +142/−85
• src/Control/Monad/Free/Foil/Example.hs +3/−3
• src/Control/Monad/Free/Foil/TH/Convert.hs +8/−8
• src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs +6/−6
• src/Control/Monad/Free/Foil/TH/ZipMatch.hs +2/−2

@@ -1,5 +1,33 @@ # CHANGELOG for `free-foil` +# 0.1.0 — 2024-08-18++- Generalize functions for binders, support general patterns (see [#16](https://github.com/fizruk/free-foil/pull/16))++  - Add `withPattern` method to `CoSinkable`. It can be seen as a CPS-style traversal over binders in a pattern.+    Our Template Haskell support covers generation of `withPattern`,+    so normally the user does not have to think about it.++  - Generalize many functions to work with arbitrary patterns, not just `NameBinder`:++    - `withFreshPattern` — to+    - `withRefreshedPattern` and `withRefreshedPattern'`+    - `extendScopePattern` — extend a given scope with all binders in a given pattern+    - `namesOfPattern` — collect all names from a pattern+    - `unsinkNamePattern` — try to unsink names from a scope extended with binders from a given pattern+    - `assertDistinctPattern` — establish that extended scope is distinct (if outer scope is)+    - `assertDistinctExt` — establish that extended scope is distinct and indeed an extension++  - Implement unification for patterns in `unifyPatterns`.+    This turns out to be one of the most difficult places, especially for compound patterns.+    Implementing patterns properly on the user side not comfortable at all!+    Luckily, we provide useful helpers like `andThenUnifyPatterns` and `andThenUnifyNameBinders`,+    as well as Template Haskell support to derive `UnifiablePattern`.++  - Generalize Free Foil to support arbitrary patterns.++  - The `Foil` and `FreeFoilTH` implementations now make use of the generalized pattern support.+ # 0.0.3 — 2024-06-20  - Add α-equivalence checks and α-normalization (see [#12](https://github.com/fizruk/free-foil/pull/12)):

@@ -5,7 +5,7 @@ -- see: https://github.com/sol/hpack  name:           free-foil-version:        0.0.3+version:        0.1.0 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

@@ -21,13 +21,19 @@   NameBinder,   emptyScope,   extendScope,+  extendScopePattern,   member,   nameOf,+  namesOfPattern,   nameId,   withFreshBinder,   withFresh,+  withFreshPattern,   withRefreshed,+  withRefreshedPattern,+  withRefreshedPattern',   unsinkName,+  unsinkNamePattern,   -- * Safe (co)sinking and renaming   Sinkable(..),   CoSinkable(..),@@ -46,6 +52,15 @@   -- * Unification of binders   UnifyNameBinders(..),   unifyNameBinders,+  andThenUnifyPatterns,+  andThenUnifyNameBinders,+  UnifiablePattern(..),+  UnifiableInPattern(..),+  NameBinders,+  emptyNameBinders,+  mergeNameBinders,+  -- ** Eliminating impossible unification+  V2, absurd2,   -- * Name maps   NameMap,   emptyNameMap,

@@ -1,9 +1,11 @@ {-# LANGUAGE BlockArguments             #-} {-# LANGUAGE ConstraintKinds            #-} {-# LANGUAGE DataKinds                  #-}+{-# LANGUAGE EmptyCase                  #-} {-# LANGUAGE FlexibleInstances          #-} {-# LANGUAGE GADTs                      #-} {-# LANGUAGE KindSignatures             #-}+{-# LANGUAGE LambdaCase                 #-} {-# LANGUAGE MultiParamTypeClasses      #-} {-# LANGUAGE QuantifiedConstraints      #-} {-# LANGUAGE RankNTypes                 #-}@@ -15,6 +17,7 @@ {-# LANGUAGE DerivingStrategies         #-} {-# LANGUAGE GeneralizedNewtypeDeriving #-} {-# OPTIONS_GHC -Wno-redundant-constraints #-}+{-# LANGUAGE DefaultSignatures          #-} -- | Main definitions of the foil that can be -- reused for specific implementations. -- This is an internal module, so it also contains implementation details of the foil.@@ -34,13 +37,13 @@ module Control.Monad.Foil.Internal where  import           Control.DeepSeq (NFData (..))+import           Data.Coerce     (coerce) import           Data.IntMap import qualified Data.IntMap     as IntMap import           Data.IntSet import qualified Data.IntSet     as IntSet import           Data.Kind       (Type) import           Unsafe.Coerce-import Data.Coerce (coerce)  -- * Safe types and operations @@ -58,6 +61,11 @@ newtype Name (n :: S) = UnsafeName RawName   deriving newtype (NFData, Eq, Ord, Show) +-- | Convert 'Name' into an identifier.+-- This may be useful for printing and debugging.+nameId :: Name l -> Id+nameId (UnsafeName i) = i+ -- | A name binder is a name that extends scope @n@ to a (larger) scope @l@. newtype NameBinder (n :: S) (l :: S) =   UnsafeNameBinder (Name l)@@ -67,6 +75,12 @@ emptyScope :: Scope VoidS emptyScope = UnsafeScope IntSet.empty +-- | A runtime check for potential name capture.+member :: Name l -> Scope n -> Bool+member (UnsafeName name) (UnsafeScope s) = rawMember name s++-- ** Extending scopes+ -- | \(O(\min(n,W))\). -- Extend a scope with one name (safely). -- Note that as long as the foil is used as intended,@@ -76,19 +90,68 @@ extendScope (UnsafeNameBinder (UnsafeName name)) (UnsafeScope scope) =   UnsafeScope (IntSet.insert name scope) --- | A runtime check for potential name capture.-member :: Name l -> Scope n -> Bool-member (UnsafeName name) (UnsafeScope s) = rawMember name s+-- | Extend scope with variables inside a pattern.+-- This is a more flexible version of 'extendScope'.+extendScopePattern+  :: (Distinct n, CoSinkable pattern)+  => pattern n l -> Scope n -> Scope l+extendScopePattern pat scope = withPattern+  (\_scope' binder k ->+    unsafeAssertFresh binder $ \binder' ->+      k (ExtendScope (extendScope binder)) binder')+  idExtendScope+  compExtendScope+  scope+  pat+  (\(ExtendScope extend) _ -> extend scope) +-- | Auxiliary data structure for scope extension. Used in 'extendScopePattern'.+newtype ExtendScope n l (o :: S) (o' :: S) = ExtendScope (Scope n -> Scope l)++-- | Identity scope extension (no extension).+idExtendScope :: ExtendScope n n o o'+idExtendScope = ExtendScope id++-- | Compose scope extensions.+compExtendScope+  :: ExtendScope n i o o'+  -> ExtendScope i l o' o''+  -> ExtendScope n l o o''+compExtendScope (ExtendScope f) (ExtendScope g)+  = ExtendScope (g . f)++-- ** Collecting new names+ -- | Extract name from a name binder. nameOf :: NameBinder n l -> Name l nameOf (UnsafeNameBinder name) = name --- | Convert 'Name' into an identifier.--- This may be useful for printing and debugging.-nameId :: Name l -> Id-nameId (UnsafeName i) = i+-- | Extract names from a pattern.+-- This is a more flexible version of 'namesOf'.+namesOfPattern+  :: forall pattern n l. (Distinct n, CoSinkable pattern) => pattern n l -> [Name l]+namesOfPattern pat = withPattern @_ @n+  (\_scope' binder k ->+    unsafeAssertFresh binder $ \binder' ->+      k (NamesOf [nameOf binder]) binder')+  idNamesOf compNamesOf (error "impossible") pat+  (\(NamesOf names) _ -> names) +-- | Auxiliary structure collecting names in scope @l@ that extend scope @n@.+-- Used in 'namesOfPattern'.+newtype NamesOf (n :: S) l (o :: S) (o' :: S) = NamesOf [Name l]++-- | Empty list of names in scope @n@.+idNamesOf :: NamesOf n n o o'+idNamesOf = NamesOf []++-- | Concatenation of names, resulting in a list of names in @l@ that extend scope @n@.+compNamesOf :: NamesOf n i o o' -> NamesOf i l o' o'' -> NamesOf n l o o''+compNamesOf (NamesOf xs) (NamesOf ys) =+  NamesOf (coerce xs ++ ys)++-- ** Refreshing binders+ -- | Allocate a fresh binder for a given scope. withFreshBinder   :: Scope n@@ -98,30 +161,87 @@   where     binder = UnsafeNameBinder (UnsafeName (rawFreshName scope)) --- | Evidence that scope @n@ contains distinct names.-data DistinctEvidence (n :: S) where-  Distinct :: Distinct n => DistinctEvidence n---- | Unsafely declare that scope @n@ is distinct.--- Used in 'unsafeAssertFresh'.-unsafeDistinct :: DistinctEvidence n-unsafeDistinct = unsafeCoerce (Distinct :: DistinctEvidence VoidS)---- | Evidence that scope @l@ extends scope @n@.-data ExtEvidence (n :: S) (l :: S) where-  Ext :: Ext n l => ExtEvidence n l---- | Unsafely declare that scope @l@ extends scope @n@.--- Used in 'unsafeAssertFresh'.-unsafeExt :: ExtEvidence n l-unsafeExt = unsafeCoerce (Ext :: ExtEvidence VoidS VoidS)- -- | Safely produce a fresh name binder with respect to a given scope. withFresh   :: Distinct n => Scope n   -> (forall l. DExt n l => NameBinder n l -> r) -> r withFresh scope cont = withFreshBinder scope (`unsafeAssertFresh` cont) +-- | Rename a given pattern into a fresh version of it to extend a given scope.+--+-- This is similar to 'withRefreshPattern', except here renaming always takes place.+withFreshPattern+  :: (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)+  => Scope o      -- ^ Ambient scope.+  -> pattern n l  -- ^ Pattern to refresh (if it clashes with the ambient scope).+  -> (forall o'. DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)+  -- ^ Continuation, accepting the refreshed pattern.+  -> r+withFreshPattern scope pattern cont = withPattern+  (\scope' binder f -> withFresh scope'+    (\binder' -> f (WithRefreshedPattern (\subst -> addRename (sink subst) binder (nameOf binder'))) binder'))+  idWithRefreshedPattern+  compWithRefreshedPattern+  scope+  pattern+  (\(WithRefreshedPattern f) pattern' -> cont f pattern')++-- | 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.+withRefreshed+  :: Distinct o+  => Scope o    -- ^ Ambient scope.+  -> Name i     -- ^ Name to refresh (if it clashes with the ambient scope).+  -> (forall o'. DExt o o' => NameBinder o o' -> r)+  -- ^ Continuation, accepting the refreshed name.+  -> r+withRefreshed scope@(UnsafeScope rawScope) name@(UnsafeName rawName) cont+  | IntSet.member rawName rawScope = withFresh scope cont+  | otherwise = unsafeAssertFresh (UnsafeNameBinder name) cont++-- | Safely rename (if necessary) a given pattern to extend a given scope.+-- This is similar to 'withFreshPattern', except if a name in the pattern+-- does not clash with the scope, it can be used immediately, without renaming.+--+-- This is a more general version of 'withRefreshed'.+withRefreshedPattern+  :: (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)+  => Scope o      -- ^ Ambient scope.+  -> pattern n l  -- ^ Pattern to refresh (if it clashes with the ambient scope).+  -> (forall o'. DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)+  -- ^ Continuation, accepting the refreshed pattern.+  -> r+withRefreshedPattern scope pattern cont = withPattern+  (\scope' binder f -> withRefreshed scope' (nameOf binder)+    (\binder' -> f (WithRefreshedPattern (\subst -> addRename (sink subst) binder (nameOf binder'))) binder'))+  idWithRefreshedPattern+  compWithRefreshedPattern+  scope+  pattern+  (\(WithRefreshedPattern f) pattern' -> cont f pattern')++-- | Refresh (if needed) bound variables introduced in a pattern.+--+-- This is a version of 'withRefreshedPattern' that uses functional renamings instead of 'Substitution'.+withRefreshedPattern'+  :: (CoSinkable pattern, Distinct o, InjectName e, Sinkable e)+  => Scope o+  -> pattern n l+  -> (forall o'. DExt o o' => ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r) -> r+withRefreshedPattern' scope pattern cont = withPattern+  (\scope' binder f -> withRefreshed scope' (nameOf binder)+    (\binder' ->+      let k subst name = case unsinkName binder name of+              Nothing    -> injectName (nameOf binder')+              Just name' -> sink (subst name')+       in f (WithRefreshedPattern' k) binder'))+  idWithRefreshedPattern'+  compWithRefreshedPattern'+  scope+  pattern+  (\(WithRefreshedPattern' f) pattern' -> cont f pattern')+ -- | Unsafely declare that a given name (binder) -- is already fresh in any scope @n'@. unsafeAssertFresh :: forall n l n' l' r. NameBinder n l@@ -131,28 +251,73 @@     Distinct -> case unsafeExt @n' @l' of       Ext -> cont (unsafeCoerce binder) +-- | Auxiliary structure to accumulate substitution extensions+-- produced when refreshing a pattern.+-- Used in 'withRefreshedPattern' and 'withFreshPattern'.+newtype WithRefreshedPattern e n l o o' = WithRefreshedPattern (Substitution e n o -> Substitution e l o')++-- | Trivial substitution (coercion via 'sink').+idWithRefreshedPattern :: (Sinkable e, DExt o o') => WithRefreshedPattern e n n o o'+idWithRefreshedPattern = WithRefreshedPattern sink++-- | Composition of substitution extensions.+compWithRefreshedPattern+  :: (DExt o o', DExt o' o'')+  => WithRefreshedPattern e n i o o'+  -> WithRefreshedPattern e i l o' o''+  -> WithRefreshedPattern e n l o o''+compWithRefreshedPattern (WithRefreshedPattern f) (WithRefreshedPattern g) =+  WithRefreshedPattern (g . f)++-- | Auxiliary structure to accumulate substitution extensions+-- produced when refreshing a pattern.+-- Similar to 'WithRefreshedPattern', except here substitutions are represented as functions.+-- Used in 'withRefreshedPattern''.+newtype WithRefreshedPattern' e n l (o :: S) (o' :: S) = WithRefreshedPattern' ((Name n -> e o) -> Name l -> e o')++-- | Trivial substitution extension (coercion via 'sink').+idWithRefreshedPattern' :: (Sinkable e, DExt o o') => WithRefreshedPattern' e n n o o'+idWithRefreshedPattern' = WithRefreshedPattern' (\f n -> sink (f n))++-- | Composition of substitution extensions.+compWithRefreshedPattern'+  :: (DExt o o', DExt o' o'')+  => WithRefreshedPattern' e n i o o'+  -> WithRefreshedPattern' e i l o' o''+  -> WithRefreshedPattern' e n l o o''+compWithRefreshedPattern' (WithRefreshedPattern' f) (WithRefreshedPattern' g) =+  WithRefreshedPattern' (g . f)++-- ** Extracting proofs from binders and patterns++-- | Evidence that scope @n@ contains distinct names.+data DistinctEvidence (n :: S) where+  Distinct :: Distinct n => DistinctEvidence n++-- | Evidence that scope @l@ extends scope @n@.+data ExtEvidence (n :: S) (l :: S) where+  Ext :: Ext n l => ExtEvidence n l+ -- | A distinct scope extended with a 'NameBinder' is also distinct.-assertDistinct :: Distinct n => NameBinder n l -> DistinctEvidence l+assertDistinct :: (Distinct n, CoSinkable pattern) => pattern n l -> DistinctEvidence l assertDistinct _ = unsafeDistinct  -- | A distinct scope extended with a 'NameBinder' is also distinct.-assertExt :: NameBinder n l -> ExtEvidence n l+assertExt :: CoSinkable pattern => pattern 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.-withRefreshed-  :: Distinct o-  => Scope o    -- ^ Ambient scope.-  -> Name i     -- ^ Name to refresh (if it clashes with the ambient scope).-  -> (forall o'. DExt o o' => NameBinder o o' -> r)-  -- ^ Continuation, accepting the refreshed name.-  -> r-withRefreshed scope@(UnsafeScope rawScope) name@(UnsafeName rawName) cont-  | IntSet.member rawName rawScope = withFresh scope cont-  | otherwise = unsafeAssertFresh (UnsafeNameBinder name) cont+-- | Unsafely declare that scope @n@ is distinct.+-- Used in 'unsafeAssertFresh'.+unsafeDistinct :: DistinctEvidence n+unsafeDistinct = unsafeCoerce (Distinct :: DistinctEvidence VoidS) +-- | Unsafely declare that scope @l@ extends scope @n@.+-- Used in 'unsafeAssertFresh'.+unsafeExt :: ExtEvidence n l+unsafeExt = unsafeCoerce (Ext :: ExtEvidence VoidS VoidS)++-- ** Unsinking names+ -- | Try coercing the name back to the (smaller) scope, -- given a binder that extends that scope. unsinkName :: NameBinder n l -> Name l -> Maybe (Name n)@@ -160,37 +325,266 @@   | nameOf binder == name = Nothing   | otherwise = Just (UnsafeName raw) +-- | Check if a name in the extended context+-- is introduced in a pattern or comes from the outer scope @n@.+--+-- This is a generalization of 'unsinkName'.+unsinkNamePattern+  :: forall pattern n l. (Distinct n, CoSinkable pattern)+  => pattern n l -> Name l -> Maybe (Name n)+unsinkNamePattern pat = withPattern @_ @n+  (\_scope' binder k ->+      unsafeAssertFresh binder $ \binder' ->+        k (UnsinkName (unsinkName binder)) binder')+  idUnsinkName+  compUnsinkName+  (error "impossible")  -- scope is not used, but has to be provided in general+  pat+  (\(UnsinkName unsink) _ -> unsink)++-- | Auxiliary structure for unsinking names.+-- Used in 'unsinkNamePattern'.+newtype UnsinkName n l (o :: S) (o' :: S) = UnsinkName (Name l -> Maybe (Name n))++-- | Trivial unsinking. If no scope extension took place, any name is free (since it cannot be bound by anything).+idUnsinkName :: UnsinkName n n o o'+idUnsinkName = UnsinkName Just++-- | Composition of unsinking for nested binders/patterns.+compUnsinkName+  :: UnsinkName n i o o'+  -> UnsinkName i l o' o''+  -> UnsinkName n l o o''+compUnsinkName (UnsinkName f) (UnsinkName g)+  = UnsinkName (\name -> g name >>= f)+ -- * 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+-- Due to the implementation of the foil, we can often rename binders efficiently,+-- by renaming binders only in one of the two unified terms.+data UnifyNameBinders (pattern :: S -> S -> Type) n l r where   -- | Binders are the same, proving that type parameters @l@ and @r@   -- are in fact equivalent.-  SameNameBinders :: UnifyNameBinders n l l+  SameNameBinders+    :: NameBinders n l  -- ^ /Unordered/ set of binders in the unified pattern (from any of the original patterns).+    -> UnifyNameBinders pattern 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+  RenameLeftNameBinder+    :: NameBinders n r                    -- ^ /Unordered/ set of binders in the unified pattern (the binders from the right pattern).+    -> (NameBinder n l -> NameBinder n r) -- ^ Binder renaming for the left pattern.+    -> UnifyNameBinders pattern 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+  RenameRightNameBinder+    :: NameBinders n l                    -- ^ /Unordered/ set of binders in the unified pattern (the binders from the left pattern).+    -> (NameBinder n r -> NameBinder n l) -- ^ Binder renaming for the right pattern.+    -> UnifyNameBinders pattern n l r+  -- | It is necessary to rename both binders.+  RenameBothBinders+    :: NameBinders n lr                     -- ^ /Unordered/ set of binders in the unified pattern+    -> (NameBinder n l -> NameBinder n lr)  -- ^ Binder renaming for the left pattern.+    -> (NameBinder n r -> NameBinder n lr)  -- ^ Binder renaming for the right pattern.+    -> UnifyNameBinders pattern n l r+  -- | Cannot unify to (sub)patterns.+  NotUnifiable :: UnifyNameBinders pattern 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'')) ->+  :: forall i l r pattern. Distinct i+  => NameBinder i l -- ^ Left pattern.+  -> NameBinder i r -- ^ Right pattern.+  -> UnifyNameBinders pattern i l r+unifyNameBinders l@(UnsafeNameBinder (UnsafeName i1)) r@(UnsafeNameBinder (UnsafeName i2))+  | i1 == i2  = case assertDistinct l of+      Distinct -> unsafeCoerce (SameNameBinders (nameBindersSingleton l))  -- equal names extend scopes equally+  | i1 < i2   = RenameRightNameBinder (nameBindersSingleton l) $ \(UnsafeNameBinder (UnsafeName i'')) ->       if i'' == i2 then UnsafeNameBinder (UnsafeName i1) else UnsafeNameBinder (UnsafeName i'')-  | otherwise = RenameLeftNameBinder $ \(UnsafeNameBinder (UnsafeName i')) ->+  | otherwise = RenameLeftNameBinder (nameBindersSingleton r) $ \(UnsafeNameBinder (UnsafeName i')) ->       if i'  == i1 then UnsafeNameBinder (UnsafeName i2) else UnsafeNameBinder (UnsafeName i') +-- | Unsafely merge results of unification for nested binders/patterns.+-- Used in 'andThenUnifyPatterns'.+unsafeMergeUnifyBinders :: UnifyNameBinders pattern a a' a'' -> UnifyNameBinders pattern a''' b' b'' -> UnifyNameBinders pattern a b' b''+unsafeMergeUnifyBinders = \case++  SameNameBinders x -> \case+    SameNameBinders y -> SameNameBinders (x `unsafeMergeNameBinders` y)+    RenameLeftNameBinder y f -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f)+    RenameRightNameBinder y g -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g)+    RenameBothBinders y f g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)+    NotUnifiable -> NotUnifiable++  RenameLeftNameBinder x f -> \case+    SameNameBinders y -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f)+    RenameLeftNameBinder y g -> RenameLeftNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce g)+    RenameRightNameBinder y g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)+    RenameBothBinders y f' g -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g)+    NotUnifiable -> NotUnifiable++  RenameRightNameBinder x g -> \case+    SameNameBinders y -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g)+    RenameLeftNameBinder y f -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)+    RenameRightNameBinder y g' -> RenameRightNameBinder (x `unsafeMergeNameBinders` y) (unsafeCoerce g . unsafeCoerce g')+    RenameBothBinders y f g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g . unsafeCoerce g')+    NotUnifiable -> NotUnifiable++  RenameBothBinders x f g -> \case+    SameNameBinders y -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g)+    RenameLeftNameBinder y f' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g)+    RenameRightNameBinder y g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f) (unsafeCoerce g . unsafeCoerce g')+    RenameBothBinders y f' g' -> RenameBothBinders (x `unsafeMergeNameBinders` y) (unsafeCoerce f . unsafeCoerce f') (unsafeCoerce g . unsafeCoerce g')+    NotUnifiable -> NotUnifiable++  NotUnifiable -> const (NotUnifiable)++-- | Chain unification of nested patterns.+andThenUnifyPatterns+  :: (UnifiablePattern pattern, Distinct l, Distinct l')+  => UnifyNameBinders pattern n l l'    -- ^ Unifying action for some outer patterns.+  -> (pattern l r, pattern l' r')       -- ^ Two nested patterns (cannot be unified directly since they extend different scopes).+  -> UnifyNameBinders pattern n r r'+andThenUnifyPatterns u (l, r) = unsafeMergeUnifyBinders u (unifyPatterns (unsafeCoerce l) r)++-- | Chain unification of nested patterns with 'NameBinder's.+andThenUnifyNameBinders+  :: (UnifiablePattern pattern, Distinct l, Distinct l')+  => UnifyNameBinders pattern n l l'    -- ^ Unifying action for some outer patterns.+  -> (NameBinder l r, NameBinder l' r') -- ^ Two nested binders (cannot be unified directly since they extend different scopes).+  -> UnifyNameBinders pattern n r r'+andThenUnifyNameBinders u (l, r) = unsafeMergeUnifyBinders u (unifyNameBinders (unsafeCoerce l) r)++-- | An /unordered/ collection of 'NameBinder's, that together extend scope @n@ to scope @l@.+--+-- For an ordered version see 'NameBinderList'.+newtype NameBinders (n :: S) (l :: S) = UnsafeNameBinders IntSet++-- | /Unsafely/ merge sets of binders (via set union).+unsafeMergeNameBinders :: NameBinders a b -> NameBinders c d -> NameBinders n l+unsafeMergeNameBinders (UnsafeNameBinders x) (UnsafeNameBinders y) = UnsafeNameBinders (x <> y)++-- | An empty set of binders keeps the scope as is.+emptyNameBinders :: NameBinders n n+emptyNameBinders = UnsafeNameBinders IntSet.empty++-- | Composition of sets of binders.+mergeNameBinders :: NameBinders n i -> NameBinders i l -> NameBinders n l+mergeNameBinders = unsafeMergeNameBinders++-- | A singleton name binder set.+nameBindersSingleton :: NameBinder n l -> NameBinders n l+nameBindersSingleton binder = UnsafeNameBinders (IntSet.singleton (nameId (nameOf binder)))++-- | An /ordered/ collection (list) of 'NameBinder's, that together extend scope @n@ to scope @l@.+--+-- For an unordered version see 'NameBinders'.+data NameBinderList n l where+  -- | An empty list of binders keeps the scope as is.+  NameBinderListEmpty :: NameBinderList n n+  -- | A non-empty list of binders.+  NameBinderListCons+    :: NameBinder n i       -- ^ Outermost binder.+    -> NameBinderList i l   -- ^ Remaining list of binders.+    -> NameBinderList n l++-- | Convert an unordered set of name binders into an ordered list (with some order).+nameBindersList :: NameBinders n l -> NameBinderList n l+nameBindersList (UnsafeNameBinders names) = go (IntSet.toList names)+  where+    go []     = unsafeCoerce NameBinderListEmpty+    go (x:xs) = NameBinderListCons (UnsafeNameBinder (UnsafeName x)) (go xs)++-- | Convert an ordered list of name binders into an unordered set.+fromNameBindersList :: NameBinderList n l -> NameBinders n l+fromNameBindersList = UnsafeNameBinders . IntSet.fromList . go+  where+    go :: NameBinderList n l -> [RawName]+    go NameBinderListEmpty                 = []+    go (NameBinderListCons binder binders) = nameId (nameOf binder) : go binders++instance CoSinkable NameBinders where+  coSinkabilityProof _rename (UnsafeNameBinders names) cont =+    cont unsafeCoerce (UnsafeNameBinders names)++  withPattern withBinder unit comp scope binders cont =+    withPattern withBinder unit comp scope (nameBindersList binders) $ \f binders' ->+      cont f (fromNameBindersList binders')++instance CoSinkable NameBinderList where+  coSinkabilityProof rename NameBinderListEmpty cont = cont rename NameBinderListEmpty+  coSinkabilityProof rename (NameBinderListCons binder binders) cont =+    coSinkabilityProof rename binder $ \rename' binder' ->+      coSinkabilityProof rename' binders $ \rename'' binders' ->+        cont rename'' (NameBinderListCons binder' binders')++  withPattern withBinder unit comp scope binders cont = case binders of+    NameBinderListEmpty -> cont unit NameBinderListEmpty+    NameBinderListCons x xs ->+      withBinder scope x $ \f x' ->+        let scope' = extendScopePattern x' scope+        in withPattern withBinder unit comp scope' xs $ \f' xs' ->+            cont (comp f f') (NameBinderListCons x' xs')++-- ** Pattern combinators++-- | An empty pattern type specifies zero possibilities for patterns.+--+-- This type can be used to specify that patterns are not possible.+data V2 (n :: S) (l :: S)++-- | Since 'V2' values logically don't exist, this witnesses the logical reasoning tool of "ex falso quodlibet".+absurd2 :: V2 n l -> a+absurd2 v2 = case v2 of {}++instance CoSinkable V2 where+  coSinkabilityProof _ v2 _ = absurd2 v2+  withPattern _ _ _ _ v2 _ = absurd2 v2+instance UnifiablePattern V2 where+  unifyPatterns = absurd2++-- | A unit pattern type corresponds to a wildcard pattern.+data U2 (n :: S) (l :: S) where+  U2 :: U2 n n  -- ^ Wildcard patten does not modify the scope.++instance CoSinkable U2 where+  coSinkabilityProof rename U2 cont = cont rename U2+  withPattern _withBinder unit _combine _scope U2 cont = cont unit U2+instance UnifiablePattern U2 where+  unifyPatterns U2 U2 = SameNameBinders emptyNameBinders++-- ** Unifiable patterns++-- | A pattern type is unifiable if it is possible to match two+-- patterns and decide how to rename binders.+class CoSinkable pattern => UnifiablePattern pattern where+  -- | Unify two patterns and decide which binders need to be renamed.+  unifyPatterns :: Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r++-- | Unification of values in patterns.+-- By default, 'Eq' instance is used, but it may be useful to ignore+-- some data in pattens (such as location annotations).+class UnifiableInPattern a where+  -- | Unify non-binding components of a pattern.+  unifyInPattern :: a -> a -> Bool+  default unifyInPattern :: Eq a => a -> a -> Bool+  unifyInPattern = (==)++instance UnifiablePattern NameBinder where+  unifyPatterns = unifyNameBinders++-- | The easiest way to compare two patterns is to check if they are the same.+-- This function is labelled /unsafe/, since we generally are interested in proper α-equivalence+-- instead of direct equality.+unsafeEqPattern :: (UnifiablePattern pattern, Distinct n) => pattern n l -> pattern n' l' -> Bool+unsafeEqPattern l r =+  case unifyPatterns l (unsafeCoerce r) of+    SameNameBinders{} -> True+    _                 -> False+ -- * Safe sinking  -- | Sinking an expression from scope @n@ into a (usualy extended) scope @l@,@@ -295,9 +689,30 @@     -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.     -> r +  -- | Generalized processing of a pattern.+  --+  -- You can see 'withPattern' as a CPS-style traversal over the binders in a pattern.+  withPattern+    :: Distinct o+    => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')+    -- ^ Processing of a single 'NameBinder', this will be applied to each binder in a pattern.+    -> (forall x z z'. DExt z z' => f x x z z')+    -- ^ Result in case no binders are present. This can be seen as scope-indexed 'mempty'.+    -> (forall x y y' z z' z''. (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')+    -- ^ Composition of results for nested binders/patterns. This can be seen as scope-indexed 'mappend'.+    -> Scope o+    -- ^ Ambient scope.+    -> pattern n l+    -- ^ Pattern to process.+    -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)+    -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.+    -> r+ instance CoSinkable NameBinder where   coSinkabilityProof _rename (UnsafeNameBinder name) cont =     cont unsafeCoerce (UnsafeNameBinder name)++  withPattern f _ _ = f  -- * Safe substitions 

@@ -3,9 +3,10 @@ {-# LANGUAGE TemplateHaskellQuotes #-} {-# OPTIONS_GHC -Wno-incomplete-patterns #-} {-# OPTIONS_GHC -Wno-incomplete-uni-patterns #-}-module Control.Monad.Foil.TH.MkFoilData (mkFoilData) where+module Control.Monad.Foil.TH.MkFoilData where  import           Language.Haskell.TH+import Language.Haskell.TH.Syntax (addModFinalizer)  import qualified Control.Monad.Foil.Internal as Foil import Control.Monad.Foil.TH.Util@@ -20,24 +21,72 @@ mkFoilData termT nameT scopeT patternT = do   n <- newName "n"   l <- newName "l"-  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT   TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT   TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT -  foilPatternCons <- mapM (toPatternCon patternTVars n) patternCons   let foilScopeCons = map (toScopeCon scopeTVars n) scopeCons   let foilTermCons = map (toTermCon termTVars n l) termCons -  return+  patternD <- mkFoilPattern nameT patternT+  addModFinalizer $ putDoc (DeclDoc foilTermT)+    ("/Generated/ with '" ++ show 'mkFoilData ++ "'. A scope-safe version of '" ++ show termT ++ "'.")+  addModFinalizer $ putDoc (DeclDoc foilScopeT)+    ("/Generated/ with '" ++ show 'mkFoilData ++ "'. A scope-safe version of '" ++ show scopeT ++ "'.")+  return $     [ DataD [] foilTermT (termTVars ++ [KindedTV n BndrReq (PromotedT ''Foil.S)]) Nothing foilTermCons []     , DataD [] foilScopeT (scopeTVars ++ [KindedTV n BndrReq (PromotedT ''Foil.S)]) Nothing foilScopeCons []-    , DataD [] foilPatternT (patternTVars ++ [KindedTV n BndrReq (PromotedT ''Foil.S), KindedTV l BndrReq (PromotedT ''Foil.S)]) Nothing foilPatternCons []-    ]+    ] ++ patternD   where     foilTermT = mkName ("Foil" ++ nameBase termT)     foilScopeT = mkName ("Foil" ++ nameBase scopeT)     foilPatternT = mkName ("Foil" ++ nameBase patternT) +    -- | Convert a constructor declaration for a raw scoped term+    -- into a constructor for the scope-safe scoped term.+    toScopeCon :: [TyVarBndr BndrVis] -> Name -> Con -> Con+    toScopeCon _tvars n (NormalC conName params) =+      NormalC foilConName (map toScopeParam params)+      where+        foilConName = mkName ("Foil" ++ nameBase conName)+        toScopeParam (_bang, PeelConT tyName tyParams)+          | tyName == termT = (_bang, PeelConT foilTermT (tyParams ++ [VarT n]))+        toScopeParam _bangType = _bangType++    -- | Convert a constructor declaration for a raw term+    -- into a constructor for the scope-safe term.+    toTermCon :: [TyVarBndr BndrVis] -> Name -> Name -> Con -> Con+    toTermCon tvars n l (NormalC conName params) =+      GadtC [foilConName] (map toTermParam params) (PeelConT foilTermT (map (VarT . tvarName) tvars ++ [VarT n]))+      where+        foilNames = [n, l]+        foilConName = mkName ("Foil" ++ nameBase conName)+        toTermParam (_bang, PeelConT tyName tyParams)+          | tyName == patternT = (_bang, PeelConT foilPatternT (tyParams ++ map VarT foilNames))+          | tyName == nameT = (_bang, AppT (ConT ''Foil.Name) (VarT n))+          | tyName == scopeT = (_bang, PeelConT foilScopeT (tyParams ++ [VarT l]))+          | tyName == termT = (_bang, PeelConT foilTermT (tyParams ++ [VarT n]))+        toTermParam _bangType = _bangType++-- | Generate just the scope-safe patterns.+mkFoilPattern+  :: Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkFoilPattern nameT patternT = do+  n <- newName "n"+  l <- newName "l"+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT++  foilPatternCons <- mapM (toPatternCon patternTVars n) patternCons++  addModFinalizer $ putDoc (DeclDoc foilPatternT)+    ("/Generated/ with '" ++ show 'mkFoilPattern ++ "'. A scope-safe version of '" ++ show patternT ++ "'.")+  return+    [ DataD [] foilPatternT (patternTVars ++ [KindedTV n BndrReq (PromotedT ''Foil.S), KindedTV l BndrReq (PromotedT ''Foil.S)]) Nothing foilPatternCons []+    ]+  where+    foilPatternT = mkName ("Foil" ++ nameBase patternT)+     -- | Convert a constructor declaration for a raw pattern type     -- into a constructor for the scope-safe pattern type.     toPatternCon@@ -48,6 +97,7 @@     toPatternCon tvars n (NormalC conName params) = do       (lastScopeName, foilParams) <- toPatternConParams 1 n params       let foilConName = mkName ("Foil" ++ nameBase conName)+      addModFinalizer $ putDoc (DeclDoc foilConName) ("Corresponds to '" ++ show conName ++ "'.")       return (GadtC [foilConName] foilParams (PeelConT foilPatternT (map (VarT . tvarName) tvars ++ [VarT n, VarT lastScopeName])))       where         -- | Process type parameters of a pattern,@@ -79,29 +129,3 @@             _ -> do               (l, conParams') <- toPatternConParams (i+1) p conParams               return (l, param : conParams')--    -- | Convert a constructor declaration for a raw scoped term-    -- into a constructor for the scope-safe scoped term.-    toScopeCon :: [TyVarBndr BndrVis] -> Name -> Con -> Con-    toScopeCon _tvars n (NormalC conName params) =-      NormalC foilConName (map toScopeParam params)-      where-        foilConName = mkName ("Foil" ++ nameBase conName)-        toScopeParam (_bang, PeelConT tyName tyParams)-          | tyName == termT = (_bang, PeelConT foilTermT (tyParams ++ [VarT n]))-        toScopeParam _bangType = _bangType--    -- | Convert a constructor declaration for a raw term-    -- into a constructor for the scope-safe term.-    toTermCon :: [TyVarBndr BndrVis] -> Name -> Name -> Con -> Con-    toTermCon tvars n l (NormalC conName params) =-      GadtC [foilConName] (map toTermParam params) (PeelConT foilTermT (map (VarT . tvarName) tvars ++ [VarT n]))-      where-        foilNames = [n, l]-        foilConName = mkName ("Foil" ++ nameBase conName)-        toTermParam (_bang, PeelConT tyName tyParams)-          | tyName == patternT = (_bang, PeelConT foilPatternT (tyParams ++ map VarT foilNames))-          | tyName == nameT = (_bang, AppT (ConT ''Foil.Name) (VarT n))-          | tyName == scopeT = (_bang, PeelConT foilScopeT (tyParams ++ [VarT l]))-          | tyName == termT = (_bang, PeelConT foilTermT (tyParams ++ [VarT n]))-        toTermParam _bangType = _bangType

@@ -4,7 +4,7 @@ {-# LANGUAGE RankNTypes            #-} {-# LANGUAGE QuasiQuotes           #-} {-# LANGUAGE TemplateHaskellQuotes #-}-module Control.Monad.Foil.TH.MkFromFoil (mkFromFoil) where+module Control.Monad.Foil.TH.MkFromFoil where  import           Language.Haskell.TH import Language.Haskell.TH.Syntax (addModFinalizer)@@ -57,12 +57,12 @@           -> $rtype         |] -  addModFinalizer $ putDoc (DeclDoc fromFoilTermT)-    "Convert a scope-safe term into a raw term."-  addModFinalizer $ putDoc (DeclDoc fromFoilPatternT)-    "Convert a scope-safe pattern into a raw pattern."-  addModFinalizer $ putDoc (DeclDoc fromFoilScopedT)-    "Convert a scope-safe scoped term into a raw scoped term."+  addModFinalizer $ putDoc (DeclDoc fromFoilTermT) $+    "/Generated/ with '" ++ show 'mkFromFoil ++ "'. Convert a scope-safe term into a raw term."+  addModFinalizer $ putDoc (DeclDoc fromFoilPatternT) $+    "/Generated/ with '" ++ show 'mkFromFoil ++ "'. Convert a scope-safe pattern into a raw pattern."+  addModFinalizer $ putDoc (DeclDoc fromFoilScopedT) $+    "/Generated/ with '" ++ show 'mkFromFoil ++ "'. Convert a scope-safe scoped term into a raw scoped term."    return     [ fromFoilTermSignature@@ -225,6 +225,78 @@              mkConParamVar :: BangType -> Int -> Name             mkConParamVar _ty i = mkName ("x" <> show i)+        toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"+        toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+        toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+        toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+        toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"++-- | Generate conversion function from raw to scope-safe pattern.+mkFromFoilPattern+  :: Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkFromFoilPattern nameT patternT = do+  n <- newName "n"+  let ntype = return (VarT n)+  l <- newName "l"+  let ltype = return (VarT l)+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT++  let patternParams = map (VarT . tvarName) patternTVars++  fromFoilPatternSignature <-+    SigD fromFoilPatternT <$>+      [t| (Int -> $(return (ConT nameT)))+          -> $(return (PeelConT foilPatternT patternParams)) $ntype $ltype+          -> $(return (PeelConT patternT patternParams))+        |]++  addModFinalizer $ putDoc (DeclDoc fromFoilPatternT) $+    "/Generated/ with '" ++ show 'mkFromFoilPattern ++ "'. Convert a scope-safe pattern into a raw pattern."++  return+    [ fromFoilPatternSignature+    , fromFoilPatternBody patternCons+    ]+  where+    foilPatternT = mkName ("Foil" ++ nameBase patternT)++    fromFoilPatternT = mkName ("fromFoil" ++ nameBase patternT)++    fromFoilPatternBody patternCons = FunD fromFoilPatternT+      [Clause [VarP toRawIdent, VarP pattern] (NormalB (CaseE (VarE pattern) (map toMatch patternCons))) []]+      where+        toRawIdent = mkName "toRawIdent"+        pattern = mkName "pattern"++        toMatch (NormalC conName params) =+          Match (ConP foilConName [] conParamPatterns) (NormalB conMatchBody) []+          where+            conMatchBody = go 1 (ConE conName) params++            go _i p [] = p+            go i p ((_bang, PeelConT tyName _tyParams) : conParams)+              | tyName == nameT = go (i + 1)+                  (AppE p (AppE (VarE toRawIdent) (AppE (VarE 'Foil.nameId) (AppE (VarE 'Foil.nameOf) (VarE xi)))))+                  conParams+              | tyName == patternT = go (i+1)+                  (AppE p (foldl AppE (VarE fromFoilPatternT) [VarE toRawIdent, VarE xi]))+                  conParams+              where+                xi = mkName ("x" <> show i)+            go i p (_ : conParams) =+              go (i + 1) (AppE p (VarE xi)) conParams+              where+                xi = mkName ("x" <> show i)++            foilConName = mkName ("Foil" ++ nameBase conName)+            conParamPatterns = map VarP conParamVars++            conParamVars = zipWith mkConParamVar params [1..]++            mkConParamVar :: BangType -> Int -> Name+            mkConParamVar _ i = mkName ("x" <> show i)         toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"         toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"         toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"

@@ -3,12 +3,13 @@ {-# LANGUAGE QuasiQuotes           #-} {-# LANGUAGE TemplateHaskellQuotes #-} {-# OPTIONS_GHC -fno-warn-type-defaults #-}-module Control.Monad.Foil.TH.MkInstancesFoil (mkInstancesFoil) where+module Control.Monad.Foil.TH.MkInstancesFoil where  import           Language.Haskell.TH -import qualified Control.Monad.Foil  as Foil-import Control.Monad.Foil.TH.Util+import qualified Control.Monad.Foil         as Foil+import           Control.Monad.Foil.TH.Util+import           Data.List                  (nub)  -- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances. mkInstancesFoil@@ -18,25 +19,22 @@   -> Name -- ^ Type name for raw patterns.   -> Q [Dec] mkInstancesFoil termT nameT scopeT patternT = do-  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT   TyConI (DataD _ctx _name scopeTVars _kind scopeCons _deriv) <- reify scopeT   TyConI (DataD _ctx _name termTVars _kind termCons _deriv) <- reify termT -  return+  coSinkablePatternD <- deriveCoSinkable nameT patternT++  return $     [ InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilScopeT (map (VarT . tvarName) scopeTVars)))         [ FunD 'Foil.sinkabilityProof (map clauseScopedTerm scopeCons) ] -    , InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars)))-        [ FunD 'Foil.coSinkabilityProof (map clausePattern patternCons) ]-     , InstanceD Nothing [] (AppT (ConT ''Foil.Sinkable) (PeelConT foilTermT (map (VarT . tvarName) termTVars)))         [ FunD 'Foil.sinkabilityProof (map clauseTerm termCons)]-    ]+    ] ++ coSinkablePatternD    where     foilTermT = mkName ("Foil" ++ nameBase termT)     foilScopeT = mkName ("Foil" ++ nameBase scopeT)-    foilPatternT = mkName ("Foil" ++ nameBase patternT)      clauseScopedTerm :: Con -> Clause     clauseScopedTerm = clauseTerm@@ -54,7 +52,7 @@         []       where         foilConName = mkName ("Foil" ++ nameBase conName)-        rename = mkName "rename"+        rename = mkName "_rename"         conParamPatterns = zipWith mkConParamPattern params [1..]         mkConParamPattern _ i = VarP (mkName ("x" ++ show i)) @@ -80,6 +78,23 @@           where             xi = mkName ("x" ++ show i) +-- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances.+deriveCoSinkable+  :: Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+deriveCoSinkable nameT patternT = do+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT++  return+    [ InstanceD Nothing [] (AppT (ConT ''Foil.CoSinkable) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars)))+        [ FunD 'Foil.coSinkabilityProof (map clausePattern patternCons)+        , FunD 'Foil.withPattern (map clauseWithPattern patternCons) ]+    ]++  where+    foilPatternT = mkName ("Foil" ++ nameBase patternT)+     clausePattern :: Con -> Clause     clausePattern RecC{} = error "Record constructors (RecC) are not supported yet!"     clausePattern InfixC{} = error "Infix constructors (InfixC) are not supported yet!"@@ -113,3 +128,118 @@           go (i + 1) rename' (AppE p (VarE xi)) conPatterns           where             xi = mkName ("x" ++ show i)++    clauseWithPattern :: Con -> Clause+    clauseWithPattern RecC{} = error "Record constructors (RecC) are not supported yet!"+    clauseWithPattern InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+    clauseWithPattern ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+    clauseWithPattern GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+    clauseWithPattern RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"+    clauseWithPattern (NormalC conName params) =+      Clause+        [VarP withNameBinder, VarP id', VarP comp, VarP scope, ConP foilConName [] conParamPatterns, VarP cont]+        (NormalB (go 1 scope (VarE id') (ConE foilConName) params))+        []+      where+        foilConName = mkName ("Foil" ++ nameBase conName)+        withNameBinder = mkName "_withNameBinder"+        id' = mkName "id'"+        comp = mkName "_comp"+        scope = mkName "_scope"+        cont = mkName "cont"+        conParamPatterns = zipWith mkConParamPattern params [1..]+        mkConParamPattern _ i = VarP (mkName ("x" ++ show i))++        go _i _scope' rename' p [] = AppE (AppE (VarE cont) rename') p+        go i scope' rename' p ((_bang, PeelConT tyName _tyParams) : conParams)+          | tyName == nameT || tyName == patternT =+              AppE+                (foldl AppE (VarE 'Foil.withPattern) [VarE withNameBinder, VarE id', VarE comp, VarE scope', VarE xi])+                (LamE [VarP renamei, VarP xi']+                  (LetE [ValD (VarP scopei) (NormalB (AppE (AppE (VarE 'Foil.extendScopePattern) (VarE xi')) (VarE scope'))) []]+                    (go (i + 1) scopei (foldl AppE (VarE comp) [rename', VarE renamei]) (AppE p (VarE xi')) conParams)))+          where+            xi = mkName ("x" ++ show i)+            xi' = mkName ("x" ++ show i ++ "'")+            renamei = mkName ("f" ++ show i)+            scopei = mkName ("_scope" ++ show i)+        go i scope' rename' p (_ : conPatterns) =+          go (i + 1) scope' rename' (AppE p (VarE xi)) conPatterns+          where+            xi = mkName ("x" ++ show i)++-- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances.+deriveUnifiablePattern+  :: Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+deriveUnifiablePattern nameT patternT = do+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT++  let (eqTypes, clauses) = mapM clauseUnifyPatterns patternCons+      ctx = nub [ AppT (ConT ''Foil.UnifiableInPattern) type_ | type_ <- eqTypes, type_ `elem` map (VarT . tvarName) patternTVars ]+  return+    [ InstanceD Nothing ctx (AppT (ConT ''Foil.UnifiablePattern) (PeelConT foilPatternT (map (VarT . tvarName) patternTVars)))+        [ FunD 'Foil.unifyPatterns (clauses ++ [notUnifiableClause]) ]+    ]++  where+    foilPatternT = mkName ("Foil" ++ nameBase patternT)++    notUnifiableClause :: Clause+    notUnifiableClause = Clause [WildP, WildP] (NormalB (ConE 'Foil.NotUnifiable)) []++    clauseUnifyPatterns :: Con -> ([Type], Clause)+    clauseUnifyPatterns RecC{} = error "Record constructors (RecC) are not supported yet!"+    clauseUnifyPatterns InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+    clauseUnifyPatterns ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+    clauseUnifyPatterns GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+    clauseUnifyPatterns RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"+    clauseUnifyPatterns (NormalC conName params) =+      case go 1 [] [] params of+        (body, eqTypes) ->+          (eqTypes, Clause+            [ConP foilConName [] paramsL, ConP foilConName [] paramsR]+            (NormalB body)+            [])+      where+        foilConName = mkName ("Foil" ++ nameBase conName)+        paramsL = zipWith (mkConParamPattern "l") params [1..]+        paramsR = zipWith (mkConParamPattern "r") params [1..]+        mkConParamPattern s _ i = VarP (mkName (s ++ show i))++        mkUnifyAllPairsRev [] = AppE (ConE 'Foil.SameNameBinders) (VarE 'Foil.emptyNameBinders)+        mkUnifyAllPairsRev [(isNameBinder, l, r)]+          | isNameBinder = AppE (AppE (VarE 'Foil.unifyNameBinders) l) r+          | otherwise    = AppE (AppE (VarE 'Foil.unifyPatterns) l) r+        mkUnifyAllPairsRev ((isNameBinder, l, r) : pairs) =+          InfixE+            (Just (mkUnifyAllPairsRev pairs))+            (VarE (if isNameBinder then 'Foil.andThenUnifyNameBinders else 'Foil.andThenUnifyPatterns))+            (Just (TupE [Just l, Just r]))+++        go _i eqTypes pairsRev [] = (mkUnifyAllPairsRev pairsRev, eqTypes)+        go i eqTypes pairsRev ((_bang, PeelConT tyName _tyParams) : conParams)+          | tyName == nameT || tyName == patternT =+            case go (i + 1) eqTypes ((isNameBinder, l, r) : pairsRev) conParams of+              (next, eqTypes') ->+                (CaseE (TupE [Just (AppE (VarE 'Foil.assertDistinct) l), Just (AppE (VarE 'Foil.assertDistinct) r)])+                  [Match+                    (TupP [ConP 'Foil.Distinct [] [], ConP 'Foil.Distinct [] []])+                    (NormalB next)+                    []], eqTypes')+          where+            isNameBinder = tyName == nameT+            l = VarE (mkName ("l" ++ show i))+            r = VarE (mkName ("r" ++ show i))+        go i eqTypes pairsRev ((_bang, type_) : conPatterns) =+          case go (i + 1) eqTypes pairsRev conPatterns of+            (next, eqTypes') ->+              (CondE+                (InfixE (Just l) (VarE 'Foil.unifyInPattern) (Just r))+                next+                (ConE 'Foil.NotUnifiable), type_ : eqTypes')+          where+            l = VarE (mkName ("l" ++ show i))+            r = VarE (mkName ("r" ++ show i))

@@ -4,7 +4,7 @@ {-# LANGUAGE RankNTypes            #-} {-# LANGUAGE QuasiQuotes           #-} {-# LANGUAGE TemplateHaskellQuotes #-}-module Control.Monad.Foil.TH.MkToFoil (mkToFoil) where+module Control.Monad.Foil.TH.MkToFoil where  import           Language.Haskell.TH import Language.Haskell.TH.Syntax (addModFinalizer)@@ -55,8 +55,10 @@   idfun <- [e| id |]   extendScopeFun <- [e| Foil.extendScope |] -  addModFinalizer $ putDoc (DeclDoc extendScopePatternFunName)-    "Extend a scope with the names bound by the given pattern.\nThis is a more flexible version of 'Control.Monad.Foil.extendScope'."+  addModFinalizer $ putDoc (DeclDoc extendScopePatternFunName) $ unlines+    [ "/Generated/ with '" ++ show 'mkExtendScopeFoilPattern ++ "'."+    , "Extend a scope with the names bound by the given pattern."+    , "This is a more flexible version of '" ++ show 'Foil.extendScope ++ "'." ]    return     [ extendScopePatternSignature@@ -144,8 +146,10 @@   withRefreshedFun <- [e| Foil.withRefreshed |]   extendScopeFun <- [e| Foil.extendScope |] -  addModFinalizer $ putDoc (DeclDoc withRefreshedFoilPatternFunName)-    "Refresh (if needed) bound variables introduced in a pattern.\nThis is a more flexible version of 'Control.Monad.Foil.withRefreshed'."+  addModFinalizer $ putDoc (DeclDoc withRefreshedFoilPatternFunName) $ unlines+    [ "/Generated/ with '" ++ show 'mkWithRefreshedFoilPattern ++ "'."+    , "Refresh (if needed) bound variables introduced in a pattern."+    , "This is a more flexible version of '" ++ show 'Foil.withRefreshed ++ "'." ]    return     [ withRefreshedFoilPatternSignature@@ -189,7 +193,7 @@               where                 xi = mkName ("x" <> show i)                 xi' = mkName ("x" <> show i <> "'")-                scopei = mkName ("scope" <> show i)+                scopei = mkName ("_scope" <> show i)                 xsubst = mkName ("subst" <> show i)                 subst = mkName "subst"                 fi = LamE [VarP subst]@@ -258,12 +262,12 @@           -> $rtype         |] -  addModFinalizer $ putDoc (DeclDoc toFoilTermT)-    "Convert a raw term into a scope-safe term."-  addModFinalizer $ putDoc (DeclDoc toFoilPatternT)-    "Convert a raw pattern into a scope-safe pattern."-  addModFinalizer $ putDoc (DeclDoc toFoilScopedT)-    "Convert a raw scoped term into a scope-safe scoped term."+  addModFinalizer $ putDoc (DeclDoc toFoilTermT) $+    "/Generated/ with '" ++ show 'mkToFoilTerm ++ "'. Convert a raw term into a scope-safe term."+  addModFinalizer $ putDoc (DeclDoc toFoilPatternT) $+    "/Generated/ with '" ++ show 'mkToFoilTerm ++ "'. Convert a raw pattern into a scope-safe pattern."+  addModFinalizer $ putDoc (DeclDoc toFoilScopedT) $+    "/Generated/ with '" ++ show 'mkToFoilTerm ++ "'. Convert a raw scoped term into a scope-safe scoped term."    return     [ toFoilTermSignature@@ -295,7 +299,7 @@         toMatch (NormalC conName params) =           Match (ConP conName [] conParamPatterns) (NormalB conMatchBody) [toFoilVarD]           where-            toFoilVarFunName = mkName "lookupRawVar"+            toFoilVarFunName = mkName "_lookupRawVar"             toFoilVarFun = VarE toFoilVarFunName             x = mkName "x"             name = mkName "name"@@ -324,7 +328,7 @@               where                 xi = mkName ("x" <> show i)                 xi' = mkName ("x" <> show i <> "'")-                scopei = mkName ("scope" <> show i)+                scopei = mkName ("_scope" <> show i)                 envi = mkName ("env" <> show i)             go i scope' env' p (_ : conParams) =               go (i + 1) scope' env' (AppE p (VarE xi)) conParams@@ -366,7 +370,7 @@                             , ValD (VarP envi) (NormalB                                 (AppE (AppE (AppE (VarE 'Map.insert) (VarE xi))                                   (AppE (VarE 'Foil.nameOf) (VarE xi')))-                                  (InfixE (Just (VarE 'Foil.sink)) (VarE '(<$>)) (Just (VarE envi))))) []]+                                  (InfixE (Just (VarE 'Foil.sink)) (VarE '(<$>)) (Just env')))) []]                         (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams)))               | tyName == patternT =                   AppE@@ -377,7 +381,7 @@               where                 xi = mkName ("x" <> show i)                 xi' = mkName ("x" <> show i <> "'")-                scopei = mkName ("scope" <> show i)+                scopei = mkName ("_scope" <> show i)                 envi = mkName ("env" <> show i)             go i scope' env' p (_ : conParams) =               go (i + 1) scope' env' (AppE p (VarE xi)) conParams@@ -407,7 +411,7 @@         toMatch (NormalC conName params) =           Match (ConP conName [] conParamPatterns) (NormalB conMatchBody) [toFoilVarD]           where-            toFoilVarFunName = mkName "lookupRawVar"+            toFoilVarFunName = mkName "_lookupRawVar"             toFoilVarFun = VarE toFoilVarFunName             x = mkName "x"             name = mkName "name"@@ -436,7 +440,7 @@               where                 xi = mkName ("x" <> show i)                 xi' = mkName ("x" <> show i <> "'")-                scopei = mkName ("scope" <> show i)+                scopei = mkName ("_scope" <> show i)                 envi = mkName ("env" <> show i)             go i scope' env' p (_ : conParams) =               go (i + 1) scope' env' (AppE p (VarE xi)) conParams@@ -451,6 +455,92 @@             mkConParamVar :: BangType -> Int -> Name             mkConParamVar _ty i = mkName ("x" <> show i) +        toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"+        toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"+        toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"+        toMatch GadtC{} = error "GADT constructors (GadtC) are not supported yet!"+        toMatch RecGadtC{} = error "Record GADT constructors (RecGadtC) are not supported yet!"++-- | Generate a conversion function from raw terms to scope-safe terms.+mkToFoilPattern+  :: Name -- ^ Type name for raw variable identifiers.+  -> Name -- ^ Type name for raw patterns.+  -> Q [Dec]+mkToFoilPattern nameT patternT = do+  n <- newName "n"+  let ntype = return (VarT n)+  r <- newName "r"+  let rtype = return (VarT r)+  TyConI (DataD _ctx _name patternTVars _kind patternCons _deriv) <- reify patternT++  toFoilPatternSignature <-+    SigD toFoilPatternT <$>+      [t| Foil.Distinct $ntype+          => Foil.Scope $ntype+          -> Map $(return (ConT nameT)) (Foil.Name $ntype)+          -> $(return (PeelConT patternT (map (VarT . tvarName) patternTVars)))+          -> (forall l. Foil.DExt $ntype l => $(return (PeelConT foilPatternT (map (VarT . tvarName) patternTVars))) $ntype l -> Map $(return (ConT nameT)) (Foil.Name l) -> $rtype)+          -> $rtype+        |]++  addModFinalizer $ putDoc (DeclDoc toFoilPatternT) $+    "/Generated/ with '" ++ show 'mkToFoilPattern ++ "'. Convert a raw pattern into a scope-safe pattern."++  return+    [ toFoilPatternSignature+    , toFoilPatternBody patternCons+    ]+  where+    foilPatternT = mkName ("Foil" ++ nameBase patternT)+    toFoilPatternT = mkName ("toFoil" ++ nameBase patternT)++    toFoilPatternBody patternCons = FunD toFoilPatternT+      [Clause [VarP scope, VarP env, VarP pattern, VarP cont] (NormalB (CaseE (VarE pattern) (map toMatch patternCons))) []]+      where+        scope = mkName "scope"+        env = mkName "env"+        pattern = mkName "pattern"+        cont = mkName "cont"++        toMatch (NormalC conName params) =+          Match (ConP conName [] conParamPatterns) (NormalB conMatchBody) []+          where+            conMatchBody = go 1 (VarE scope) (VarE env) (ConE foilConName) params++            go _i _scope' env' p [] = AppE (AppE (VarE cont) p) env'+            go i scope' env' p ((_bang, PeelConT tyName _tyParams) : conParams)+              | tyName == nameT =+                  AppE (AppE (VarE 'Foil.withFresh) scope')+                    (LamE [VarP xi']+                      (LetE [ ValD (VarP scopei) (NormalB (AppE (AppE (VarE 'Foil.extendScope) (VarE xi')) scope')) []+                            , ValD (VarP envi) (NormalB+                                (AppE (AppE (AppE (VarE 'Map.insert) (VarE xi))+                                  (AppE (VarE 'Foil.nameOf) (VarE xi')))+                                  (InfixE (Just (VarE 'Foil.sink)) (VarE '(<$>)) (Just env')))) []]+                        (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams)))+              | tyName == patternT =+                  AppE+                    (AppE (AppE (AppE (VarE toFoilPatternT) scope') env') (VarE xi))+                    (LamE [VarP xi', VarP envi]+                      (LetE [ValD (VarP scopei) (NormalB (AppE (AppE (VarE 'Foil.extendScopePattern) (VarE xi')) scope')) []]+                        (go (i+1) (VarE scopei) (VarE envi) (AppE p (VarE xi')) conParams)))+              where+                xi = mkName ("x" <> show i)+                xi' = mkName ("x" <> show i <> "'")+                scopei = mkName ("_scope" <> show i)+                envi = mkName ("env" <> show i)+            go i scope' env' p (_ : conParams) =+              go (i + 1) scope' env' (AppE p (VarE xi)) conParams+              where+                xi = mkName ("x" <> show i)++            foilConName = mkName ("Foil" ++ nameBase conName)+            conParamPatterns = map VarP conParamVars++            conParamVars = zipWith mkConParamVar params [1..]++            mkConParamVar :: BangType -> Int -> Name+            mkConParamVar _ i = mkName ("x" <> show i)         toMatch RecC{} = error "Record constructors (RecC) are not supported yet!"         toMatch InfixC{} = error "Infix constructors (InfixC) are not supported yet!"         toMatch ForallC{} = error "Existential constructors (ForallC) are not supported yet!"

@@ -1,4 +1,5 @@ {-# LANGUAGE DataKinds             #-}+{-# LANGUAGE RankNTypes             #-} {-# LANGUAGE DeriveAnyClass        #-} {-# LANGUAGE DeriveGeneric         #-} {-# LANGUAGE FlexibleContexts      #-}@@ -31,24 +32,25 @@ import           GHC.Generics                (Generic)  -- | Scoped term under a (single) name binder.-data ScopedAST sig n where-  ScopedAST :: Foil.NameBinder n l -> AST sig l -> ScopedAST sig n+data ScopedAST binder sig n where+  ScopedAST :: binder n l -> AST binder sig l -> ScopedAST binder sig n -instance (forall l. NFData (AST sig l)) => NFData (ScopedAST sig n) where+instance (forall x y. NFData (binder x y), forall l. NFData (AST binder sig l)) => NFData (ScopedAST binder sig n) where   rnf (ScopedAST binder body) = rnf binder `seq` rnf body  -- | A term, generated by a signature 'Bifunctor' @sig@, -- with (free) variables in scope @n@.-data AST sig n where+data AST binder sig n where   -- | A (free) variable in scope @n@.-  Var :: Foil.Name n -> AST sig n+  Var :: Foil.Name n -> AST binder sig n   -- | A non-variable syntactic construction specified by the signature 'Bifunctor' @sig@.-  Node :: sig (ScopedAST sig n) (AST sig n) -> AST sig n+  Node :: sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n -deriving instance Generic (AST sig n)-deriving instance (forall scope term. (NFData scope, NFData term) => NFData (sig scope term)) => NFData (AST sig n)+deriving instance Generic (AST binder sig n)+deriving instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))+  => NFData (AST binder sig n) -instance Bifunctor sig => Foil.Sinkable (AST sig) where+instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.Sinkable (AST binder sig) where   sinkabilityProof rename = \case     Var name -> Var (rename name)     Node node -> Node (bimap f (Foil.sinkabilityProof rename) node)@@ -57,26 +59,26 @@         Foil.extendRenaming rename binder $ \rename' binder' ->           ScopedAST binder' (Foil.sinkabilityProof rename' body) -instance Foil.InjectName (AST sig) where+instance Foil.InjectName (AST binder sig) where   injectName = Var  -- * Substitution  -- | Substitution for free (scoped monads). substitute-  :: (Bifunctor sig, Foil.Distinct o)+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder)   => Foil.Scope o-  -> Foil.Substitution (AST sig) i o-  -> AST sig i-  -> AST sig o+  -> Foil.Substitution (AST binder sig) i o+  -> AST binder sig i+  -> AST binder sig o substitute scope subst = \case   Var name -> Foil.lookupSubst subst name   Node node -> Node (bimap f (substitute scope subst) node)   where     f (ScopedAST binder body) =-      Foil.withRefreshed scope (Foil.nameOf binder) $ \binder' ->-        let subst' = Foil.addRename (Foil.sink subst) binder (Foil.nameOf binder')-            scope' = Foil.extendScope binder' scope+      Foil.withRefreshedPattern scope binder $ \extendSubst binder' ->+        let subst' = extendSubst (Foil.sink subst)+            scope' = Foil.extendScopePattern binder' scope             body' = substitute scope' subst' body         in ScopedAST binder' body' @@ -89,24 +91,24 @@ -- -- In general, 'substitute' is more efficient since it does not always refresh binders. substituteRefreshed-  :: (Bifunctor sig, Foil.Distinct o)+  :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder)   => Foil.Scope o-  -> Foil.Substitution (AST sig) i o-  -> AST sig i-  -> AST sig o+  -> Foil.Substitution (AST binder sig) i o+  -> AST binder sig i+  -> AST binder 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+      Foil.withFreshPattern scope binder $ \extendSubst binder' ->+        let subst' = extendSubst (Foil.sink subst)+            scope' = Foil.extendScopePattern 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+instance (Bifunctor sig, Foil.CoSinkable binder) => Foil.RelMonad Foil.Name (AST binder sig) where   rreturn = Var   rbind scope term subst =     case term of@@ -115,34 +117,32 @@     where       g x = Foil.rbind scope x subst       g' (ScopedAST binder body) =-        Foil.withRefreshed scope (Foil.nameOf binder) $ \binder' ->-          let scope' = Foil.extendScope binder' scope-              subst' name = case Foil.unsinkName binder name of-                          Nothing -> Foil.rreturn (Foil.nameOf binder')-                          Just n  -> Foil.sink (subst n)+        Foil.withRefreshedPattern' scope binder $ \extendSubst binder' ->+          let scope' = Foil.extendScopePattern binder' scope+              subst' = extendSubst subst            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)+  :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)   => Foil.Scope n-  -> AST sig n-  -> AST sig n+  -> AST binder sig n+  -> AST binder 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)+refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder)   => Foil.Scope n-  -> ScopedAST sig n-  -> ScopedAST sig n+  -> ScopedAST binder sig n+  -> ScopedAST binder 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')+  Foil.withFreshPattern scope binder $ \extendSubst binder' ->+    let scope' = Foil.extendScopePattern binder' scope+        subst = extendSubst (Foil.sink Foil.identitySubst)     in ScopedAST binder' (substituteRefreshed scope' subst body)  -- | \(\alpha\)-equivalence check for two terms in one scope@@ -151,10 +151,10 @@ -- 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)+  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)   => Foil.Scope n-  -> AST sig n-  -> AST sig n+  -> AST binder sig n+  -> AST binder sig n   -> Bool alphaEquivRefreshed scope t1 t2 = refreshAST scope t1 `unsafeEqAST` refreshAST scope t2 @@ -164,10 +164,10 @@ -- 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)+  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)   => Foil.Scope n-  -> AST sig n-  -> AST sig n+  -> AST binder sig n+  -> AST binder sig n   -> Bool alphaEquiv _scope (Var x) (Var y) = x == coerce y alphaEquiv scope (Node l) (Node r) =@@ -178,33 +178,43 @@  -- | Same as 'alphaEquiv' but for scoped terms. alphaEquivScoped-  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n)+  :: (Bifunctor sig, Bifoldable sig, ZipMatch sig, Foil.Distinct n, Foil.UnifiablePattern binder)   => Foil.Scope n-  -> ScopedAST sig n-  -> ScopedAST sig n+  -> ScopedAST binder sig n+  -> ScopedAST binder sig n   -> Bool alphaEquivScoped scope   (ScopedAST binder1 body1)   (ScopedAST binder2 body2) =-    case Foil.unifyNameBinders binder1 binder2 of+    case Foil.unifyPatterns 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+      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+            let scope1 = Foil.extendScopePattern binder1 scope             in alphaEquiv scope1 body1 body2       -- if we can safely rename first binder into second-      Foil.RenameLeftNameBinder rename1to2 ->+      Foil.RenameLeftNameBinder _ rename1to2 ->         case Foil.assertDistinct binder2 of           Foil.Distinct ->-            let scope2 = Foil.extendScope binder2 scope+            let scope2 = Foil.extendScopePattern 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 ->+      Foil.RenameRightNameBinder _ rename2to1 ->         case Foil.assertDistinct binder1 of           Foil.Distinct ->-            let scope1 = Foil.extendScope binder1 scope+            let scope1 = Foil.extendScopePattern binder1 scope             in alphaEquiv scope1 body1 (Foil.liftRM scope1 (Foil.fromNameBinderRenaming rename2to1) body2)+      -- if we need to rename both patterns+      Foil.RenameBothBinders binder' rename1 rename2 ->+        case Foil.assertDistinct binder' of+          Foil.Distinct ->+            let scope' = Foil.extendScopePattern binder' scope+            in alphaEquiv scope'+                (Foil.liftRM scope' (Foil.fromNameBinderRenaming rename1) body1)+                (Foil.liftRM scope' (Foil.fromNameBinderRenaming rename2) body2)+      -- if we cannot unify patterns then scopes are not alpha-equivalent+      Foil.NotUnifiable -> False  -- ** Unsafe equality checks @@ -213,9 +223,9 @@ -- 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+  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)+  => AST binder sig n+  -> AST binder sig l   -> Bool unsafeEqAST (Var x) (Var y) = x == coerce y unsafeEqAST (Node t1) (Node t2) =@@ -226,13 +236,14 @@  -- | A version of 'unsafeEqAST' for scoped terms. unsafeEqScopedAST-  :: (Bifoldable sig, ZipMatch sig)-  => ScopedAST sig n-  -> ScopedAST sig l+  :: (Bifoldable sig, ZipMatch sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l)+  => ScopedAST binder sig n+  -> ScopedAST binder sig l   -> Bool unsafeEqScopedAST (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and-  [ binder1 == coerce binder2-  , body1 `unsafeEqAST` body2+  [ Foil.unsafeEqPattern binder1 binder2+  , case (Foil.assertDistinct binder1, Foil.assertDistinct binder2) of+      (Foil.Distinct, Foil.Distinct) -> body1 `unsafeEqAST` body2   ]  -- ** Syntactic matching (unification)@@ -253,14 +264,31 @@  -- ** Convert to free foil +-- | Convert a raw term into a scope-safe term. convertToAST-  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent)+  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)   => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))-  -> (rawPattern -> Maybe rawIdent)+  -- ^ Unpeel one syntax node (or a variable) from a raw term.+  -> (forall x z. Foil.Distinct x+      => Foil.Scope x+      -> Map rawIdent (Foil.Name x)+      -> rawPattern+      -> (forall y. Foil.DExt x y+          => binder x y+          -> Map rawIdent (Foil.Name y)+          -> z)+      -> z)+  -- ^ Convert raw pattern into a scope-safe pattern.   -> (rawScopedTerm -> rawTerm)+  -- ^ Extract a term from a scoped term (or crash).   -> Foil.Scope n-  -> Map rawIdent (Foil.Name n) -> rawTerm -> AST sig n-convertToAST toSig getPatternBinder getScopedTerm scope names t =+  -- ^ Resulting scope of the constructed term.+  -> Map rawIdent (Foil.Name n)+  -- ^ Known names of free variables in scope @n@.+  -> rawTerm+  -- ^ Raw term.+  -> AST binder sig n+convertToAST toSig fromRawPattern getScopedTerm scope names t =   case toSig t of     Left x ->       case Map.lookup x names of@@ -268,37 +296,57 @@         Just name -> Var name     Right node -> Node $       bimap-        (convertToScopedAST toSig getPatternBinder getScopedTerm scope names)-        (convertToAST toSig getPatternBinder getScopedTerm scope names)+        (convertToScopedAST toSig fromRawPattern getScopedTerm scope names)+        (convertToAST toSig fromRawPattern getScopedTerm scope names)         node +-- | Same as 'convertToAST' but for scoped terms. convertToScopedAST-  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent)+  :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)   => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))-  -> (rawPattern -> Maybe rawIdent)+  -- ^ Unpeel one syntax node (or a variable) from a raw term.+  -> (forall x z. Foil.Distinct x+      => Foil.Scope x+      -> Map rawIdent (Foil.Name x)+      -> rawPattern+      -> (forall y. Foil.DExt x y+          => binder x y+          -> Map rawIdent (Foil.Name y)+          -> z)+      -> z)+  -- ^ Convert raw pattern into a scope-safe pattern.   -> (rawScopedTerm -> rawTerm)+  -- ^ Extract a term from a scoped term (or crash).   -> Foil.Scope n+  -- ^ Resulting scope of the constructed term.   -> Map rawIdent (Foil.Name n)+  -- ^ Known names of free variables in scope @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))+  -- ^ A pair of a pattern and a corresponding scoped term.+  -> ScopedAST binder sig n+convertToScopedAST toSig fromRawPattern getScopedTerm scope names (pat, scopedTerm) =+  fromRawPattern scope names pat $ \binder' names' ->+    let scope' = Foil.extendScopePattern binder' scope+     in ScopedAST binder' (convertToAST toSig fromRawPattern getScopedTerm scope' names' (getScopedTerm scopedTerm))  -- ** Convert from free foil +-- | Convert a scope-safe term back into a raw term. convertFromAST   :: Bifunctor sig   => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)+  -- ^ Peel back one layer of syntax.   -> (rawIdent -> rawTerm)-  -> (rawIdent -> rawPattern)+  -- ^ Convert identifier into a raw variable term.+  -> (forall x y. (Int -> rawIdent) -> binder x y -> rawPattern)+  -- ^ Convert scope-safe pattern into a raw pattern.   -> (rawTerm -> rawScopedTerm)-  -> (Int -> rawIdent) -> AST sig n -> rawTerm+  -- ^ Wrap raw term into a scoped term.+  -> (Int -> rawIdent)+  -- ^ Convert underlying integer identifier of a bound variable into a raw identifier.+  -> AST binder sig n+  -- ^ Scope-safe term.+  -> rawTerm convertFromAST fromSig fromVar makePattern makeScoped f = \case   Var x -> fromVar (f (Foil.nameId x))   Node node -> fromSig $@@ -307,14 +355,23 @@       (convertFromAST fromSig fromVar makePattern makeScoped f)       node +-- | Same as 'convertFromAST' but for scoped terms. convertFromScopedAST   :: Bifunctor sig   => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm)+  -- ^ Peel back one layer of syntax.   -> (rawIdent -> rawTerm)-  -> (rawIdent -> rawPattern)+  -- ^ Convert identifier into a raw variable term.+  -> (forall x y. (Int -> rawIdent) -> binder x y -> rawPattern)+  -- ^ Convert scope-safe pattern into a raw pattern.   -> (rawTerm -> rawScopedTerm)-  -> (Int -> rawIdent) -> ScopedAST sig n -> (rawPattern, rawScopedTerm)+  -- ^ Wrap raw term into a scoped term.+  -> (Int -> rawIdent)+  -- ^ Convert underlying integer identifier of a bound variable into a raw identifier.+  -> ScopedAST binder sig n+  -- ^ Scope-safe scoped term.+  -> (rawPattern, rawScopedTerm) convertFromScopedAST fromSig fromVar makePattern makeScoped f = \case   ScopedAST binder body ->-    ( makePattern (f (Foil.nameId (Foil.nameOf binder)))+    ( makePattern f binder     , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body))

@@ -25,15 +25,15 @@   deriving (Functor) deriveBifunctor ''ExprF -pattern AppE :: AST ExprF n -> AST ExprF n -> AST ExprF n+pattern AppE :: AST binder ExprF n -> AST binder ExprF n -> AST binder ExprF n pattern AppE x y = Node (AppF x y) -pattern LamE :: NameBinder n l -> AST ExprF l -> AST ExprF n+pattern LamE :: binder n l -> AST binder ExprF l -> AST binder ExprF n pattern LamE binder body = Node (LamF (ScopedAST binder body))  {-# COMPLETE Var, AppE, LamE #-} -type Expr = AST ExprF+type Expr = AST NameBinder ExprF  -- | Use 'ppExpr' to show \(\lambda\)-terms. instance Show (Expr n) where

@@ -1,5 +1,5 @@-{-# LANGUAGE LambdaCase      #-} {-# OPTIONS_GHC -fno-warn-type-defaults      #-}+{-# LANGUAGE LambdaCase      #-} {-# LANGUAGE TemplateHaskell #-} module Control.Monad.Free.Foil.TH.Convert where @@ -61,7 +61,7 @@     [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 ++ "'.")+    ("/Generated/ with '" ++ show 'mkConvertToSig ++ "'. Perform one step of converting '" ++ show termT ++ "', peeling off one node of type '" ++ show signatureT ++ "'.")   return     [ SigD convertTermToSigT convertTermToSigClausesType     , FunD convertTermToSigT convertTermToSigClauses@@ -77,11 +77,11 @@         where           x = mkName "x"           isVarP VarP{} = True-          isVarP _ = False+          isVarP _      = False           pats =             [ case type_ of                 PeelConT typeName _ | typeName == nameT -> VarP x-                _ -> WildP+                _                                       -> WildP             | (_bang, type_) <- types ]       NormalC conName types -> mkClause conName conName' types         where@@ -130,7 +130,7 @@     [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 ++ "'.")+    ("/Generated/ with '" ++ show 'mkConvertFromSig ++ "'. Perform one step of converting '" ++ show termT ++ "', peeling off one node of type '" ++ show signatureT ++ "'.")   return     [ SigD convertTermFromSigT convertTermFromSigClausesType     , FunD convertTermFromSigT convertTermFromSigClauses@@ -205,9 +205,9 @@     mkClause :: Name -> [BangType] -> Q [Clause]     mkClause conName types = do       body <- case concat vars of-        [] -> [e| Nothing |]+        []       -> [e| Nothing |]         [Just y] -> [e| Just $y |]-        _ -> [e| error "complex patterns are not supported" |]+        _        -> [e| error "complex patterns are not supported" |]       return [ Clause [ConP conName [] pats] (NormalB body) [] ]       where         x = mkName "x"@@ -259,7 +259,7 @@     mkClause conName types = do       body <- case concat vars of         [y] -> [e| $y |]-        _ -> [e| error "complex patterns are not supported" |]+        _   -> [e| error "complex patterns are not supported" |]       return [ Clause [ConP conName [] pats] (NormalB body) [] ]       where         x = mkName "x"

@@ -5,8 +5,7 @@ {-# LANGUAGE ViewPatterns    #-} module Control.Monad.Free.Foil.TH.PatternSynonyms where -import Control.Monad (forM_)-import qualified Control.Monad.Foil         as Foil+import           Control.Monad              (forM_) import           Control.Monad.Foil.TH.Util import           Control.Monad.Free.Foil import           Language.Haskell.TH@@ -61,7 +60,8 @@    where     n = mkName "n"-    termType = PeelConT ''AST [signatureType, VarT n]+    binderT = VarT (mkName "binder")+    termType = PeelConT ''AST [binderT, signatureType, VarT n]     toArg = \case       Left ((b, _), (x, _)) -> ConP 'ScopedAST [] [VarP b, VarP x]       Right (x, _) -> VarP x@@ -69,10 +69,10 @@     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]))+            ( (mkName ("b" ++ show i), foldl AppT binderT [VarT n, VarT l])+            , (mkName ("x" ++ show i), PeelConT ''AST [binderT, signatureType, VarT l]))       | typeName == term =-          Right (mkName ("x" ++ show i), PeelConT ''AST [signatureType, VarT n])+          Right (mkName ("x" ++ show i), PeelConT ''AST [binderT, signatureType, VarT n])       where         l = mkName ("l" ++ show i)     toPatternArgType i (_bang, type_)

@@ -1,7 +1,7 @@-{-# LANGUAGE LambdaCase      #-} {-# OPTIONS_GHC -fno-warn-type-defaults      #-}-{-# LANGUAGE ViewPatterns      #-}+{-# LANGUAGE LambdaCase      #-} {-# LANGUAGE TemplateHaskell #-}+{-# LANGUAGE ViewPatterns    #-} module Control.Monad.Free.Foil.TH.ZipMatch where  import           Language.Haskell.TH