diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -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)): diff --git a/free-foil.cabal b/free-foil.cabal --- a/free-foil.cabal +++ b/free-foil.cabal @@ -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 category: Parsing diff --git a/src/Control/Monad/Foil.hs b/src/Control/Monad/Foil.hs --- a/src/Control/Monad/Foil.hs +++ b/src/Control/Monad/Foil.hs @@ -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, diff --git a/src/Control/Monad/Foil/Internal.hs b/src/Control/Monad/Foil/Internal.hs --- a/src/Control/Monad/Foil/Internal.hs +++ b/src/Control/Monad/Foil/Internal.hs @@ -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 diff --git a/src/Control/Monad/Foil/TH/MkFoilData.hs b/src/Control/Monad/Foil/TH/MkFoilData.hs --- a/src/Control/Monad/Foil/TH/MkFoilData.hs +++ b/src/Control/Monad/Foil/TH/MkFoilData.hs @@ -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 diff --git a/src/Control/Monad/Foil/TH/MkFromFoil.hs b/src/Control/Monad/Foil/TH/MkFromFoil.hs --- a/src/Control/Monad/Foil/TH/MkFromFoil.hs +++ b/src/Control/Monad/Foil/TH/MkFromFoil.hs @@ -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!" diff --git a/src/Control/Monad/Foil/TH/MkInstancesFoil.hs b/src/Control/Monad/Foil/TH/MkInstancesFoil.hs --- a/src/Control/Monad/Foil/TH/MkInstancesFoil.hs +++ b/src/Control/Monad/Foil/TH/MkInstancesFoil.hs @@ -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)) diff --git a/src/Control/Monad/Foil/TH/MkToFoil.hs b/src/Control/Monad/Foil/TH/MkToFoil.hs --- a/src/Control/Monad/Foil/TH/MkToFoil.hs +++ b/src/Control/Monad/Foil/TH/MkToFoil.hs @@ -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!" diff --git a/src/Control/Monad/Free/Foil.hs b/src/Control/Monad/Free/Foil.hs --- a/src/Control/Monad/Free/Foil.hs +++ b/src/Control/Monad/Free/Foil.hs @@ -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)) diff --git a/src/Control/Monad/Free/Foil/Example.hs b/src/Control/Monad/Free/Foil/Example.hs --- a/src/Control/Monad/Free/Foil/Example.hs +++ b/src/Control/Monad/Free/Foil/Example.hs @@ -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 diff --git a/src/Control/Monad/Free/Foil/TH/Convert.hs b/src/Control/Monad/Free/Foil/TH/Convert.hs --- a/src/Control/Monad/Free/Foil/TH/Convert.hs +++ b/src/Control/Monad/Free/Foil/TH/Convert.hs @@ -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" diff --git a/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs b/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs --- a/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs +++ b/src/Control/Monad/Free/Foil/TH/PatternSynonyms.hs @@ -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_) diff --git a/src/Control/Monad/Free/Foil/TH/ZipMatch.hs b/src/Control/Monad/Free/Foil/TH/ZipMatch.hs --- a/src/Control/Monad/Free/Foil/TH/ZipMatch.hs +++ b/src/Control/Monad/Free/Foil/TH/ZipMatch.hs @@ -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