diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,35 @@ # CHANGELOG for `free-foil` +# 0.3.1 — 2026-07-14 + +A bug fix and a set of additions, all of them prompted by the projects built on free-foil. Nothing is removed or changed, so upgrading from 0.3.0 needs no work. + +Fixes: + +- `mkFreeFoil` and `mkFreeFoilConversions` generated ill-typed code for a raw constructor whose shape does not line up with the free foil node it becomes (see [#38](https://github.com/fizruk/free-foil/pull/38)): + + ``` + Let ::= Pattern Term ScopedTerm -- a term between the pattern and its scope + LetRec ::= Pattern ScopedTerm ScopedTerm -- one pattern binding two scopes + ``` + + - The pattern synonym's arguments and its type signature were computed by two traversals that disagreed, and the conversions had the mirror problem. + - A constructor binding several scopes binds the same raw name in each of them, so raw-to-foil now sends that one binder into every scoped child, and foil-to-raw reads it back from the first. + - Constructors with at most one scoped child generate exactly what they did before. + - Reported and diagnosed by [@AbsoluteNikola](https://github.com/AbsoluteNikola), who had to vendor the generated code by hand in [free-foil-refinement-types](https://github.com/AbsoluteNikola/free-foil-refinement-types). + +New functions, absorbed from the projects built on free-foil, several of which were importing `Control.Monad.Foil.Internal` to get at them (see [#40](https://github.com/fizruk/free-foil/pull/40)): + +- `popNameBinder` — the inverse of `addNameBinder`, for leaving a binder. +- `withFreshNameBinderList` — a fresh binder for each element of a list, bound to it in a `NameMap`. +- `snocNameBinderList` and `concatNameBinderLists`. +- `nameBindersList`, `fromNameBindersList` and `nameMapToScope` are now exported (they existed, but were unreachable). +- With thanks to [@Probirochniy](https://github.com/Probirochniy), [@fedor-ivn](https://github.com/fedor-ivn) and [@snejugal](https://github.com/snejugal) ([free-foil-hou](https://github.com/fedor-ivn/free-foil-hou)), and to [@evermake](https://github.com/evermake), [@frog-da](https://github.com/frog-da) and [@Vikono](https://github.com/Vikono) ([free-foil-typecheck](https://github.com/evermake/free-foil-typecheck)), whose copies of these helpers carried the comment *"Should be in `Control.Monad.Foil`"*. + +Documentation: + +- `unifyNameBinders` renames the binder with the larger name towards the one with the smaller name. That is safe, since the renaming is pushed through a term with `liftRM`, which refreshes a binder whenever it would capture. The haddock now says so, with a test to match (see [#39](https://github.com/fizruk/free-foil/pull/39)). Raised by [@AbsoluteNikola](https://github.com/AbsoluteNikola). + # 0.3.0 — 2026-07-14 This release makes generic deriving the default way to instantiate the library: 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.3.0 +version: 0.3.1 synopsis: Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads) description: Please see the README on GitHub at category: Parsing @@ -91,6 +91,11 @@ type: exitcode-stdio-1.0 main-is: Spec.hs other-modules: + Control.Monad.Foil.NameMapSpec + Control.Monad.Foil.UnifyNameBindersSpec + Control.Monad.Free.Foil.TH.MkFreeFoilSpec + Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config + Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax Paths_free_foil hs-source-dirs: test @@ -102,7 +107,10 @@ , containers >=0.6 && <0.9 , deepseq >=1.4 && <1.6 , free-foil + , hspec + , hspec-discover , kind-generics >=0.5.0 && <0.6 + , kind-generics-th , template-haskell >=2.21.0.0 && <2.24 , text >=1.2.3.1 && <2.2 default-language: Haskell2010 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 @@ -71,10 +71,17 @@ emptyNameMap, lookupName, addNameBinder, + popNameBinder, nameMapToSubstitution, + nameMapToScope, addNameBinders, addNameBinderList, + withFreshNameBinderList, NameBinderList(..), + nameBindersList, + fromNameBindersList, + snocNameBinderList, + concatNameBinderLists, -- * Constraints Ext, ExtEvidence(..), 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 @@ -408,6 +408,20 @@ -- | Unify binders either by asserting that they are the same, -- or by providing a /safe/ renaming function to convert one binder to another. +-- +-- When the binders differ, the one with the /larger/ name is renamed towards the +-- one with the smaller name. The direction is deliberate, but it is not what makes +-- the renaming safe, and it is worth being explicit about that, since the choice +-- looks arbitrary and has been "fixed" downstream before. +-- +-- The renaming returned here is not applied by substituting names blindly: callers +-- push it through a term with 'Control.Monad.Foil.Relative.liftRM', which refreshes +-- a binder whenever it would capture. So the target name may perfectly well be used +-- by a binder /inside/ the term being renamed — a term built in a small scope keeps +-- its small binder names when 'sink' places it in a larger one, so binder names do +-- not always grow with depth — and the result is still correct. See +-- @Control.Monad.Foil.UnifyNameBindersSpec@ for the term that exercises exactly +-- this. unifyNameBinders :: forall i l r pattern. Distinct i => NameBinder i l -- ^ Left pattern. @@ -512,6 +526,23 @@ go [] = unsafeCoerce NameBinderListEmpty go (x:xs) = NameBinderListCons (UnsafeNameBinder (UnsafeName x)) (go xs) +-- | Add a binder to the end of an (ordered) list of binders. +-- +-- Note that 'NameBinderListCons' adds a binder to the /front/ of the list, which +-- is the outermost position. This adds one to the innermost position instead. +snocNameBinderList :: NameBinderList n i -> NameBinder i l -> NameBinderList n l +snocNameBinderList NameBinderListEmpty binder = + NameBinderListCons binder NameBinderListEmpty +snocNameBinderList (NameBinderListCons binder binders) binder' = + NameBinderListCons binder (snocNameBinderList binders binder') + +-- | Concatenate two (ordered) lists of binders, the second extending the scope +-- that the first extends to. +concatNameBinderLists :: NameBinderList n i -> NameBinderList i l -> NameBinderList n l +concatNameBinderLists NameBinderListEmpty binders = binders +concatNameBinderLists (NameBinderListCons binder binders) binders' = + NameBinderListCons binder (concatNameBinderLists binders binders') + -- | Convert an ordered list of name binders into an unordered set. fromNameBindersList :: NameBinderList n l -> NameBinders n l fromNameBindersList = UnsafeNameBinders . IntSet.fromList . go @@ -901,6 +932,45 @@ -- Note that the scope parameter of the result differs from the initial map. addNameBinder :: NameBinder n l -> a -> NameMap n a -> NameMap l a addNameBinder name x (NameMap m) = NameMap (IntMap.insert (nameId (nameOf name)) x m) + +-- | Remove the mapping for a binder, shrinking the map back to the outer scope. +-- +-- This is the inverse of 'addNameBinder', and is what a type checker wants when +-- it leaves a binder it has entered. +popNameBinder :: NameBinder n l -> NameMap l a -> NameMap n a +popNameBinder binder (NameMap m) = NameMap (IntMap.delete (nameId (nameOf binder)) m) + +-- | Allocate a fresh binder for each element of a list, binding each element to +-- its binder in the map. +-- +-- The continuation receives the extended scope, the binders in the order of the +-- input list, and the extended map. This is the list-shaped counterpart of +-- 'withFresh', and saves a caller from threading the scope, the binders, and the +-- map through a recursion by hand. +withFreshNameBinderList + :: forall n a r. Distinct n + => [a] -- ^ A value to bind to each fresh binder. + -> Scope n -- ^ The ambient scope. + -> NameMap n a -- ^ The map to extend. + -> (forall l. DExt n l => Scope l -> NameBinderList n l -> NameMap l a -> r) + -> r +withFreshNameBinderList xs0 scope0 nameMap0 cont = + go xs0 scope0 NameBinderListEmpty nameMap0 cont + where + go :: forall i r'. Distinct i + => [a] -> Scope i -> NameBinderList n i -> NameMap i a + -> (forall l. DExt n l => Scope l -> NameBinderList n l -> NameMap l a -> r') + -> r' + go [] scope binders nameMap cont' = + case (assertDistinct binders, assertExt binders) of + (Distinct, Ext) -> cont' scope binders nameMap + go (x:xs) scope binders nameMap cont' = + withFresh scope $ \binder -> + go xs + (extendScope binder scope) + (snocNameBinderList binders binder) + (addNameBinder binder x nameMap) + cont' -- * Raw types and operations diff --git a/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs b/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs --- a/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs +++ b/src/Control/Monad/Free/Foil/TH/MkFreeFoil.hs @@ -21,7 +21,8 @@ import qualified Control.Monad.Free.Foil as Foil import Data.Bifunctor import Data.List (find, unzip4, (\\), nub) -import Data.Maybe (catMaybes, mapMaybe) +import Data.Maybe (catMaybes, listToMaybe, mapMaybe, + maybeToList) import Data.Map (Map) import qualified Data.Map as Map import qualified GHC.Generics as GHC @@ -333,6 +334,23 @@ ForallC params ctx con -> ForallC params ctx <$> go con RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) +-- | Is this raw field a binding (pattern) field? +-- +-- Such a field has no counterpart in the free foil node: the binder it stands for +-- lives inside the 'Foil.ScopedAST' of each scoped child. +isBindingField :: FreeFoilConfig -> Type -> Bool +isBindingField FreeFoilConfig{..} = \case + PeelConT typeName _ | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> True + _ -> False + +-- | Is this raw field a scoped-term field? +-- +-- Such a field becomes a 'Foil.ScopedAST', which carries a binder of its own. +isScopeField :: FreeFoilConfig -> Type -> Bool +isScopeField FreeFoilConfig{..} = \case + PeelConT typeName _ | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> True + _ -> False + termConToPat :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [([Name], Pat, Pat, [Exp])] termConToPat rawTypeName config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go where @@ -384,8 +402,40 @@ GadtC conNames rawArgTypes _rawRetType -> concat <$> do forM conNames $ \conName -> do let newConName = toSignatureName config conName - (concat -> vars, concat -> pats, concat -> pats', concat -> exps) <- unzip4 <$> - mapM (fromArgType . snd) rawArgTypes + perField <- mapM (fromArgType . snd) rawArgTypes + let (concat -> vars, concat -> pats, _, _) = unzip4 perField + -- These expressions rebuild the /raw/ constructor, whose fields are + -- shaped differently from the free foil node's: the raw constructor + -- has a single binding (pattern) field and its scoped fields carry + -- no binder of their own, whereas in the free foil every scoped + -- child carries its own binder. So a scoped child contributes only + -- its body here, and the binding field is filled from the first + -- scoped child's binder -- the raw syntax can name only one binder, + -- and a constructor that binds several scopes binds the same name + -- in each of them. + firstScopeBinder = listToMaybe + [ binder + | (rawArgType, (binder : _, _, _, _)) <- zip (map snd rawArgTypes) perField + , isScopeField config rawArgType ] + rawFieldExp rawArgType (_, _, _, fieldExps) + | isBindingField config rawArgType = map VarE (maybeToList firstScopeBinder) + | isScopeField config rawArgType = drop 1 fieldExps -- the body; the binder is not a raw field + | otherwise = fieldExps + exps = concat (zipWith rawFieldExp (map snd rawArgTypes) perField) + -- Only the first scoped child's binder makes it back into the raw + -- syntax (see above), so matching the others' binders would bind a + -- variable we never use. + sigPats = goSigPats True (zip (map snd rawArgTypes) perField) + goSigPats _ [] = [] + goSigPats isFirstScope ((rawArgType, (_, _, fieldPats, _)) : rest) + | isScopeField config rawArgType = + (if isFirstScope then fieldPats else map ignoreBinder fieldPats) + ++ goSigPats False rest + | otherwise = fieldPats ++ goSigPats isFirstScope rest + ignoreBinder = \case + TupP [_binder, body] -> TupP [WildP, body] + p -> p + pats' = sigPats return $ if rawTypeName == rawTermName then [ (vars, ConP 'Foil.Node [] [ConP newConName [] pats], ConP newConName [] pats', exps) ] @@ -521,6 +571,52 @@ ForallC _params _ctx con -> go con RecGadtC conNames argTypes retType -> go (GadtC conNames (map removeName argTypes) retType) +-- | Argument types of a pattern synonym for a single raw constructor. +-- +-- This has to agree with 'termConToPat', which decides what the synonym's +-- /arguments/ are, and the two used to disagree: +-- +-- * a raw binding (pattern) field contributes __no__ argument, since a binder +-- in the free foil lives inside the 'Foil.ScopedAST' it binds, not beside it; +-- * a raw scoped-term field contributes __two__ arguments, a binder and a body; +-- * every other field contributes one argument, as before. +-- +-- Crucially, each scoped-term field gets a __fresh__ inner scope: a constructor +-- with several scoped children (a recursive @let@, say) binds a separate name in +-- each of them, so sharing one scope variable between them is wrong. A +-- constructor with at most one scoped child keeps the inner scope named @i@, +-- so the generated code for such constructors is unchanged. +patternSynonymArgTypes :: FreeFoilConfig -> Type -> Type -> [Type] -> [Type] +patternSynonymArgTypes config@FreeFoilConfig{..} outerScope innerScope rawArgTypes = + go (1 :: Int) rawArgTypes + where + -- Only when there are several scoped children do we need to number the + -- scopes; with one child, @i@ keeps the generated code as it was. + scopeCount = length (filter (isScopeField config) rawArgTypes) + innerScopeFor k + | scopeCount <= 1 = innerScope + | otherwise = VarT (mkName ("i" ++ show k)) + + go _ [] = [] + go k (rawArgType : rest) = case rawArgType of + PeelConT typeName _params + -- The binder is an argument of the ScopedAST, not of the node. + | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> go k rest + -- A scoped child: its own binder, then its body, in its own scope. + | Just FreeFoilTermConfig{..} <- lookupScopeName typeName freeFoilTermConfigs -> + let inner = innerScopeFor k + rawBindingType = PeelConT rawBindingName (typeParamsOf rawArgType) + in toFreeFoilType SortTerm config outerScope inner rawBindingType + : toFreeFoilType SortTerm config outerScope inner rawArgType + : go (k + 1) rest + _ -> toFreeFoilType SortTerm config outerScope innerScope rawArgType : go k rest + + -- A scoped type and its binding type are parametrised alike (both carry the + -- annotation type, if any), so the binder type reuses the scope's parameters. + typeParamsOf = \case + PeelConT _ params -> params + _ -> [] + mkPatternSynonym :: Name -> FreeFoilConfig -> FreeFoilTermConfig -> Type -> Con -> Q [(Name, [Dec])] mkPatternSynonym rawTypeName config termConfig@FreeFoilTermConfig{..} rawRetType = go where @@ -529,16 +625,18 @@ GadtC conNames rawArgTypes _rawRetType -> concat <$> do forM (conNames \\ [rawVarConName]) $ \conName -> do let patName = toConName config conName - rawConType = foldr (\x y -> AppT (AppT ArrowT x) y) rawRetType (map snd rawArgTypes) outerScope = VarT (mkName "o") innerScope | rawTypeName `elem` rawSubScopeNames = outerScope | otherwise = VarT (mkName "i") + synType = foldr (\x y -> AppT (AppT ArrowT x) y) + (toFreeFoilType SortTerm config outerScope innerScope rawRetType) + (patternSynonymArgTypes config outerScope innerScope (map snd rawArgTypes)) [(vars, pat, _, _)] <- termConToPat rawTypeName config termConfig (GadtC [conName] rawArgTypes rawRetType) -- FIXME: unsafe matching! addModFinalizer $ putDoc (DeclDoc patName) ("/Generated/ with '" ++ show 'mkFreeFoil ++ "'. Pattern synonym for an '" ++ show ''Foil.AST ++ "' node of type '" ++ show conName ++ "'.") return [(patName, - [ PatSynSigD patName (toFreeFoilType SortTerm config outerScope innerScope rawConType) + [ PatSynSigD patName synType , PatSynD patName (PrefixPatSyn vars) ImplBidir pat ])] @@ -1187,6 +1285,19 @@ sigConToClause :: Sort -> Type -> FreeFoilConfig -> FreeFoilTermConfig -> Con -> Q [Clause] sigConToClause sort rawRetType config@FreeFoilConfig{..} FreeFoilTermConfig{..} = go where + -- Matching a raw constructor, we must bind exactly one variable per raw + -- field. The binding (pattern) field binds @theBinder@, and each scoped + -- field binds only a body -- and then every scoped child of the free foil + -- node is given /the same/ @theBinder@, since the raw syntax names one + -- binder and a constructor binding several scopes binds it in each of them. + fromRawArgType :: Bool -> Name -> Name -> Type -> Q ([Pat], [Exp]) + fromRawArgType isVarCon theIdent theBinder rawArgType + | isBindingField config rawArgType = return ([VarP theBinder], []) + | isScopeField config rawArgType = do + body <- newName "body" + return ([VarP body], [TupE [Just (VarE theBinder), Just (VarE body)]]) + | otherwise = fromArgType isVarCon theIdent rawArgType + fromArgType :: Bool -> Name -> Type -> Q ([Pat], [Exp]) fromArgType isVarCon theIdent = \case PeelConT typeName _params @@ -1227,11 +1338,12 @@ go = \case GadtC conNames rawArgTypes _rawRetType -> concat <$> do theIdent <- newName "_theRawIdent" + theBinder <- newName "binder" forM conNames $ \conName -> do let newConName = toSignatureName config conName isVarCon = conName == rawVarConName (concat -> pats, concat -> exps) <- unzip <$> - mapM (fromArgType isVarCon theIdent . snd) rawArgTypes + mapM (fromRawArgType isVarCon theIdent theBinder . snd) rawArgTypes case sort of SortTerm | isVarCon -> return diff --git a/test/Control/Monad/Foil/NameMapSpec.hs b/test/Control/Monad/Foil/NameMapSpec.hs new file mode 100644 --- /dev/null +++ b/test/Control/Monad/Foil/NameMapSpec.hs @@ -0,0 +1,53 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE GADTs #-} + +-- | Helpers for 'Foil.NameMap' and 'Foil.NameBinderList'. +module Control.Monad.Foil.NameMapSpec (spec) where + +import Data.Foldable (toList) +import Test.Hspec + +import qualified Control.Monad.Foil as Foil + +-- | The raw names bound by a list of binders, outermost first. +binderIds :: Foil.NameBinderList n l -> [Int] +binderIds Foil.NameBinderListEmpty = [] +binderIds (Foil.NameBinderListCons binder binders) = + Foil.nameId (Foil.nameOf binder) : binderIds binders + +spec :: Spec +spec = do + describe "withFreshNameBinderList" $ do + it "binds each value to a fresh binder, in order" $ + Foil.withFreshNameBinderList "abc" Foil.emptyScope Foil.emptyNameMap $ + \_scope binders nameMap -> do + binderIds binders `shouldBe` [0, 1, 2] -- a fresh name is max scope + 1 + toList nameMap `shouldBe` "abc" + + it "binds nothing when there is nothing to bind" $ + Foil.withFreshNameBinderList ([] :: [Int]) Foil.emptyScope Foil.emptyNameMap $ + \_scope binders nameMap -> do + binderIds binders `shouldBe` [] + toList nameMap `shouldBe` [] + + describe "popNameBinder" $ + it "undoes addNameBinder" $ + Foil.withFresh Foil.emptyScope $ \binder -> + let nameMap = Foil.addNameBinder binder 'x' Foil.emptyNameMap + in toList (Foil.popNameBinder binder nameMap) `shouldBe` "" + + describe "snocNameBinderList" $ + it "adds a binder to the innermost position" $ + Foil.withFreshNameBinderList "ab" Foil.emptyScope Foil.emptyNameMap $ + \scope binders _nameMap -> + Foil.withFresh scope $ \binder -> + binderIds (Foil.snocNameBinderList binders binder) `shouldBe` [0, 1, 2] + + describe "concatNameBinderLists" $ + it "agrees with snocNameBinderList on a singleton" $ + Foil.withFreshNameBinderList "ab" Foil.emptyScope Foil.emptyNameMap $ + \scope binders _nameMap -> + Foil.withFresh scope $ \binder -> + let singleton = Foil.NameBinderListCons binder Foil.NameBinderListEmpty + in binderIds (Foil.concatNameBinderLists binders singleton) + `shouldBe` binderIds (Foil.snocNameBinderList binders binder) diff --git a/test/Control/Monad/Foil/UnifyNameBindersSpec.hs b/test/Control/Monad/Foil/UnifyNameBindersSpec.hs new file mode 100644 --- /dev/null +++ b/test/Control/Monad/Foil/UnifyNameBindersSpec.hs @@ -0,0 +1,68 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE ScopedTypeVariables #-} + +-- | 'Foil.unifyNameBinders' renames the binder with the /larger/ name towards the +-- one with the smaller name. This module pins that down, because the choice looks +-- arbitrary and is not: it is safe, but only because the renaming it asks for is +-- applied by a capture-avoiding substitution. +-- +-- A fresh name is @max scope + 1@, so binder names normally grow as one goes +-- deeper into a term. They do not have to: 'Foil.sink' is a coercion, so a term +-- built in a small scope keeps its (small) binder names when it is placed inside +-- a larger one. A term whose /outer/ binder is named after its /inner/ one is +-- therefore reachable, and it is the term that makes the direction of the +-- renaming observable. +module Control.Monad.Foil.UnifyNameBindersSpec (spec) where + +import Data.Maybe (fromJust) +import Test.Hspec + +import qualified Control.Monad.Foil as Foil +import Control.Monad.Free.Foil + +import Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax + +-- | @\\x. x@, with the binder named @max scope + 1@. +identityIn :: Foil.Distinct n => Foil.Scope n -> FFTerm n +identityIn scope = Foil.withFresh scope $ \binder -> + case Foil.assertDistinct binder of + Foil.Distinct -> FFFun (FFPatternVar binder) (Var (Foil.nameOf binder)) + +-- | @\\x. \\y. y@, built outside-in: the outer binder is named 0, the inner 1. +nestedNormal :: FFTerm Foil.VoidS +nestedNormal = Foil.withFresh Foil.emptyScope $ \outer -> + case Foil.assertDistinct outer of + Foil.Distinct -> + FFFun (FFPatternVar outer) (identityIn (Foil.extendScope outer Foil.emptyScope)) + +-- | The same term, @\\x. \\y. y@, built inside-out: the outer binder is named 1 +-- and the inner one 0, so the names run backwards. +nestedInverted :: FFTerm Foil.VoidS +nestedInverted = fromJust $ + Foil.withFresh Foil.emptyScope $ \(binder0 :: Foil.NameBinder Foil.VoidS n1) -> + case Foil.assertDistinct binder0 of + Foil.Distinct -> + let scope1 = Foil.extendScope binder0 Foil.emptyScope + inner = Foil.sink (identityIn Foil.emptyScope) :: FFTerm n1 -- binder named 0 + in Foil.withFresh scope1 $ \outer -> -- named 1 + case Foil.assertDistinct outer of + Foil.Distinct -> + unsinkAST Foil.emptyScope + (FFFun (FFPatternVar outer) (Foil.sink inner)) + +spec :: Spec +spec = describe "unifyNameBinders (via alphaEquiv)" $ do + it "identifies two spellings of the same term whose binder names run opposite ways" $ + -- Unifying the two outer binders renames the right one (1) down to the left + -- one (0) -- onto a name a binder /inside that very body/ already uses. The + -- renaming is applied with 'liftRM', which refreshes on a clash, so it does + -- not capture. Renaming towards the smaller name is therefore safe, and this + -- is the example that says so. + alphaEquiv Foil.emptyScope nestedNormal nestedInverted `shouldBe` True + + it "is symmetric on that pair" $ + alphaEquiv Foil.emptyScope nestedInverted nestedNormal `shouldBe` True + + it "still tells genuinely different terms apart" $ + alphaEquiv Foil.emptyScope nestedNormal (identityIn Foil.emptyScope) `shouldBe` False diff --git a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs new file mode 100644 --- /dev/null +++ b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE PatternSynonyms #-} + +-- | Regression tests for 'mkFreeFoil' and 'mkFreeFoilConversions' on raw +-- constructors whose shape does not line up with the free foil node they become. +-- +-- That "Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax" compiles at all is half +-- the test: the generated pattern synonyms and conversions used to be ill-typed +-- for @Let@ and @LetRec@. These examples are the other half — they check that a +-- raw binder still binds what it used to. +module Control.Monad.Free.Foil.TH.MkFreeFoilSpec (spec) where + +import qualified Control.Monad.Foil as Foil +import qualified Data.Map as Map +import Test.Hspec + +import Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config +import Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax + +-- | Convert a closed raw term into the scope-safe representation and back. +-- +-- Binders come back renamed (that is what 'intToVarIdent' is for), so the +-- examples below check how names /relate/, not what they are called. +roundtrip :: Term -> Term +roundtrip = fromTerm . toTerm Foil.emptyScope Map.empty + +x, y :: VarIdent +x = VarIdent "x" +y = VarIdent "y" + +-- | A closed term, to use where a term must not mention the surrounding binder. +identity :: Term +identity = Fun (PatternVar y) (ScopedTerm (Var y)) + +spec :: Spec +spec = do + describe "a pattern adjacent to its scope (Fun)" $ + it "round-trips, and the body still refers to the binder" $ + case roundtrip (Fun (PatternVar x) (ScopedTerm (Var x))) of + Fun (PatternVar binder) (ScopedTerm (Var v)) -> v `shouldBe` binder + other -> expectationFailure ("unexpected shape: " <> show other) + + describe "a pattern separated from its scope (Let)" $ do + it "puts the binder in the binding position, not the bound term's" $ + -- The generated conversions used to hand the raw constructor its arguments + -- in the free foil node's order rather than the raw one, which put the + -- bound term where the pattern belongs. + case roundtrip (Let (PatternVar x) identity (ScopedTerm (Var x))) of + Let (PatternVar binder) bound (ScopedTerm (Var v)) -> do + v `shouldBe` binder -- the body refers to the binder + bound `shouldSatisfy` isFun -- the bound term is still a term + other -> expectationFailure ("unexpected shape: " <> show other) + + describe "one pattern binding two scopes (LetRec)" $ do + it "binds the same name in both scopes" $ + -- Each scoped child of a free foil node carries its own binder, so the two + -- scopes get two distinct foil names. The raw syntax has only one pattern, + -- so converting back must give both scopes the same name again. + case roundtrip (LetRec (PatternVar x) (ScopedTerm (Var x)) (ScopedTerm (Var x))) of + LetRec (PatternVar binder) (ScopedTerm (Var v1)) (ScopedTerm (Var v2)) -> do + v1 `shouldBe` binder + v2 `shouldBe` binder + other -> expectationFailure ("unexpected shape: " <> show other) + + it "keeps the two scopes apart" $ + case roundtrip (LetRec (PatternVar x) (ScopedTerm identity) (ScopedTerm (Var x))) of + LetRec (PatternVar binder) (ScopedTerm first) (ScopedTerm (Var v)) -> do + first `shouldSatisfy` isFun -- the first scope does not mention the binder + v `shouldBe` binder -- the second one does + other -> expectationFailure ("unexpected shape: " <> show other) + where + isFun Fun{} = True + isFun _ = False diff --git a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Config.hs b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Config.hs new file mode 100644 --- /dev/null +++ b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Config.hs @@ -0,0 +1,73 @@ +{-# LANGUAGE TemplateHaskell #-} + +-- | A raw syntax in the shape BNFC produces, used to test 'mkFreeFoil'. +-- +-- The interesting constructors are the ones whose /raw/ shape does not line up +-- with the free foil node they become: +-- +-- * @Let@ has a pattern, a term, and one scoped term (so the pattern is not +-- adjacent to the scope it binds); +-- * @LetRec@ has a pattern and __two__ scoped terms (so one raw binder binds +-- two separate scopes). +-- +-- Both used to generate ill-typed code. See the spec. +-- +-- The config lives in its own module because Template Haskell may not splice a +-- value defined in the same module. +module Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config where + +import Control.Monad.Free.Foil.TH.MkFreeFoil + +newtype VarIdent = VarIdent String + deriving (Eq, Ord, Show) + +newtype Pattern = PatternVar VarIdent + deriving (Eq, Show) + +newtype ScopedTerm = ScopedTerm Term + deriving (Eq, Show) + +data Term + = Var VarIdent + | App Term Term + | Fun Pattern ScopedTerm -- ^ pattern, then its scope (this always worked) + | Let Pattern Term ScopedTerm -- ^ a term between the pattern and its scope + | LetRec Pattern ScopedTerm ScopedTerm -- ^ one pattern binding two scopes + deriving (Eq, Show) + +rawVar :: VarIdent -> Term +rawVar = Var + +intToVarIdent :: Int -> VarIdent +intToVarIdent i = VarIdent ("x" <> show i) + +rawScopedTerm :: Term -> ScopedTerm +rawScopedTerm = ScopedTerm + +rawScopeToTerm :: ScopedTerm -> Term +rawScopeToTerm (ScopedTerm t) = t + +config :: FreeFoilConfig +config = FreeFoilConfig + { rawQuantifiedNames = [] + , freeFoilTermConfigs = + [ FreeFoilTermConfig + { rawIdentName = ''VarIdent + , rawTermName = ''Term + , rawBindingName = ''Pattern + , rawScopeName = ''ScopedTerm + , rawVarConName = 'Var + , rawSubTermNames = [] + , rawSubScopeNames = [] + , intToRawIdentName = 'intToVarIdent + , rawVarIdentToTermName = 'rawVar + , rawTermToScopeName = 'rawScopedTerm + , rawScopeToTermName = 'rawScopeToTerm + } ] + , freeFoilNameModifier = ("FF" ++) + , freeFoilScopeNameModifier = ("FFScoped" ++) + , freeFoilConNameModifier = ("FF" ++) + , freeFoilConvertFromName = ("from" ++) + , freeFoilConvertToName = ("to" ++) + , signatureNameModifier = (++ "Sig") + } diff --git a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs new file mode 100644 --- /dev/null +++ b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec/Syntax.hs @@ -0,0 +1,52 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE PatternSynonyms #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} +-- Generated conversions carry a redundant @Ord@ constraint; 'soas' silences the +-- same warning in its generated module, as it does the orphan 'ZipMatchK' +-- instance for the raw identifier type. +{-# OPTIONS_GHC -Wno-missing-signatures -Wno-redundant-constraints -Wno-orphans #-} + +-- | The scope-safe syntax generated from +-- "Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config". +-- +-- That this module /compiles at all/ is the regression test: before the fix, +-- 'mkFreeFoil' and 'mkFreeFoilConversions' generated ill-typed code for @Let@ +-- and @LetRec@ (a pattern synonym whose signature disagreed with its arguments, +-- and conversions that gave the raw constructor the wrong number of arguments in +-- the wrong order). +module Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax where + +import qualified Control.Monad.Foil as Foil +import Control.Monad.Free.Foil.TH.MkFreeFoil +import Data.Bifunctor.TH +import Data.ZipMatchK +import Generics.Kind.TH (deriveGenericK) + +import Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config + +mkFreeFoil config + +deriveGenericK ''FFPattern +instance Foil.SinkableK FFPattern +instance Foil.HasNameBinders FFPattern +instance Foil.CoSinkable FFPattern +instance Foil.UnifiablePattern FFPattern + +deriveBifunctor ''TermSig +deriveBifoldable ''TermSig +deriveBitraversable ''TermSig + +deriveGenericK ''TermSig +instance ZipMatchK VarIdent where zipMatchWithK = zipMatchViaEq +instance ZipMatchK TermSig + +mkFreeFoilConversions config diff --git a/test/Spec.hs b/test/Spec.hs --- a/test/Spec.hs +++ b/test/Spec.hs @@ -1,2 +1,1 @@ -main :: IO () -main = putStrLn "Test suite not yet implemented" +{-# OPTIONS_GHC -F -pgmF hspec-discover #-}