diff --git a/ChangeLog.md b/ChangeLog.md --- a/ChangeLog.md +++ b/ChangeLog.md @@ -1,5 +1,36 @@ # CHANGELOG for `free-foil` +# 0.6.1 — 2026-10-27 + +This release lets `substitute`, `alphaEquiv` and `unsafeEqAST` specialise in client code, and fixes problems found by an audit of the documentation. One of the fixes changes the types of `unsinkAST` and `nameSetSubsetOfScope`, described first. + +Breaking changes: + +- `unsinkAST` requires `DExt n l` instead of `Distinct l`, and `nameSetSubsetOfScope` requires `Ext n l`: the scope `l` of the term (or set) must extend the scope `n` it is restricted to. Both compare raw identifiers, which identify a name only within one chain of scope extensions, so with unrelated scopes the answer was meaningless (see [#127](https://github.com/fizruk/free-foil/pull/127)). + - To migrate, bring `Ext n l` into scope where it is missing, e.g. with `assertExt` on the binder that leads from `n` to `l`, or from `withFresh` and `withThinnedNameBinderList`, which provide it. + +Changed: + +- `zipMatchWith1`, `zipMatch1`, `zipMatchWith2` and `zipMatch2` no longer require `Traversable` (or `Bitraversable`). `alphaEquiv`, `unsafeEqAST` and the functions behind them no longer require `Bitraversable` or `SinkableK`, and `alphaEquivRefreshed` requires `Bifunctor` instead of `Bitraversable`. None of them used these instances (see [#125](https://github.com/fizruk/free-foil/pull/125)). + +Fixes: + +- `alphaEquivRefreshed` compares patterns with `unifyPatternsIn`, as `alphaEquiv` does (through the new `unsafeEqASTIn`). It compared them with `unifyPatterns`, which compares binders only, so it accepted terms whose binders differ in a payload (such as a type annotation) that `alphaEquiv` rejects (see [#127](https://github.com/fizruk/free-foil/pull/127)). + +Performance: + +- `substitute`, `alphaEquiv`, `unsafeEqAST` and the functions behind them are `INLINE` wrappers around local loops, which take the instances from the wrapper. Inlined at a known signature, the loops use its instances directly. Before, they looked the instances up at every node, and a `SPECIALIZE` pragma in a client did not help: GHC split each function into a wrapper and a worker, since some of its dictionaries (such as `Distinct`) are never used at runtime, and the pragma reached only the wrapper. On the library's benchmarks, α-equivalence takes 0.54–0.91 of the time and normalisation 0.58–0.85 (see [#125](https://github.com/fizruk/free-foil/pull/125)). + +New: + +- `unsafeEqASTIn` and `unsafeEqScopedASTIn` compare two terms in one scope, like `unsafeEqAST`, but compare patterns with `unifyPatternsIn`, so the payloads of patterns are compared as well (see [#127](https://github.com/fizruk/free-foil/pull/127)). +- `unresolvedNamesWith` is `unresolvedNames` for the arguments of `tryConvertToASTWith`: it also takes the table of constants, so that the constants no longer count as unresolved (see [#127](https://github.com/fizruk/free-foil/pull/127)). +- `Control.Monad.Free.Foil.Internal` holds the implementation of `Control.Monad.Free.Foil`, which now has an export list. The loops behind α-equivalence, `unsafeEqAST` and `unsafeEqASTIn` (`AlphaEquivLoops`, `alphaEquivLoops`, `EqLoops`, `unsafeEqLoops`, `EqInLoops`, `unsafeEqInLoops`) are exported only from the internal module (see [#125](https://github.com/fizruk/free-foil/pull/125), [#127](https://github.com/fizruk/free-foil/pull/127)). + +Documentation: + +- Doc comments and README passages that the code contradicted are corrected, among them the equation given for `substituteRefreshed` and the `zipMatchK` example. Haddock links written through a module alias (such as `'Foil.sink'`) resolve, where in 0.6.0 they pointed to a nonexistent page (see [#126](https://github.com/fizruk/free-foil/pull/126)). + # 0.6.0 — 2026-10-26 This release lets `mkFreeFoil` generate most instances of a signature, and adds folds that traverse terms without rebuilding them. Several breaking changes come with it, described first. diff --git a/free-foil.cabal b/free-foil.cabal --- a/free-foil.cabal +++ b/free-foil.cabal @@ -1,11 +1,11 @@ cabal-version: 1.12 --- This file has been generated from package.yaml by hpack version 0.37.0. +-- This file has been generated from package.yaml by hpack version 0.39.1. -- -- see: https://github.com/sol/hpack name: free-foil -version: 0.6.0 +version: 0.6.1 synopsis: Efficient Type-Safe Capture-Avoiding Substitution for Free (Scoped Monads) description: Please see the README on GitHub at category: Parsing @@ -48,6 +48,7 @@ Control.Monad.Free.Foil.Binary Control.Monad.Free.Foil.Binary.TH Control.Monad.Free.Foil.Example + Control.Monad.Free.Foil.Internal Control.Monad.Free.Foil.TH Control.Monad.Free.Foil.TH.Convert Control.Monad.Free.Foil.TH.MkFreeFoil @@ -129,6 +130,7 @@ Control.Monad.Free.Foil.TH.MkFreeFoilSpec.PatternsSyntax Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Syntax Control.Monad.Free.Foil.TH.PatternTypesSpec + Control.Monad.Free.Foil.UnresolvedNamesSpec Data.ZipMatchK.SumProductSpec Data.ZipMatchK.THSpec SpecHook 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 @@ -1,8 +1,8 @@ -- | Main definitions of the foil that can be -- reused for specific implementations. -- --- The original description of this approach --- is described in the IFL 2022 paper by Maclaurin, Radul, and Paszke +-- This approach was originally described +-- in the IFL 2022 paper by Maclaurin, Radul, and Paszke -- [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224). -- This module also introduces 'CoSinkable' class, -- generalizing handling of patterns, as described in @@ -60,12 +60,6 @@ SinkableK(..), Sinkable(..), CoSinkable(..), - -- ** Transporting a pattern's payloads - PatternTransport, - verbatimTransport, - transportUnderBinder, - transportPayload, - transportName, HasNameBinders(getNameBinders), sink, sink1, @@ -76,6 +70,12 @@ composeNameBinderRenamings, fromNameBinderRenaming, extendRenamingNameBinder, + -- ** Transporting a pattern's payloads + PatternTransport, + verbatimTransport, + transportUnderBinder, + transportPayload, + transportName, -- * Safe substitutions Substitution, lookupSubst, 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 @@ -680,8 +680,12 @@ -- place a restriction is paid for: compare a term\'s support against the scope -- it is to be restricted to. -- +-- The scope @l@ of the set must extend @n@, since names are compared by their +-- raw identifiers, which identify a name only within one chain of scope +-- extensions. +-- -- @since 0.4.0 -nameSetSubsetOfScope :: NameSet l -> Scope n -> Bool +nameSetSubsetOfScope :: Ext n l => NameSet l -> Scope n -> Bool nameSetSubsetOfScope (UnsafeNameSet names) (UnsafeScope scope) = names `IntSet.isSubsetOf` scope @@ -1215,9 +1219,9 @@ -- pattern that carries them does: 'alphaEquivIn' asks for a 'Scope'. -- -- Note that the verdict speaks about binders, so an instance comparing - -- payloads has to apply the renaming the verdict prescribes before it - -- compares them, exactly as 'Control.Monad.Free.Foil.alphaEquivScoped' - -- applies it to the body of a scoped term. Two telescopes @(A : 𝕌) (x : A)@ + -- payloads has to take the renaming the verdict prescribes into account when + -- it compares them, as 'Control.Monad.Free.Foil.alphaEquivScoped' does for + -- the body of a scoped term. Two telescopes @(A : 𝕌) (x : A)@ -- and @(B : 𝕌) (y : B)@ are α-equivalent, and their second payloads are only -- equal once the first binders have been identified. -- @@ -2497,7 +2501,7 @@ cont (putBackRenamingK @_ @i rename' irename) (Field (unsafeCoerce x')) -- unsafeCoerce? -- | A field indexed by the innermost scope variable only, such as the body of --- 'Control.Monad.Free.Foil.ScopedAST'. Under a binder the traversal holds one +-- t'Control.Monad.Free.Foil.ScopedAST'. Under a binder the traversal holds one -- renaming per scope variable, so the field takes the innermost one, as -- @t'Field' ('Kon' f ':@:' 'Var' i)@ does. instance SinkableK (f a) => GSinkableK (Field (Kon f :@: Kon a :@: Var0)) where 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 @@ -116,7 +116,7 @@ toPatternConParams i p (param@(bang_, type_) : conParams) = case type_ of -- if the current component is a variable identifier - -- then treat it as a single name binder (see 'Foil.NameBinder') + -- then treat it as a single name binder (see t'Control.Monad.Foil.NameBinder') PeelConT tyName _tyParams | tyName == nameT -> do l <- newName ("n" <> show i) let type' = AppT (AppT (ConT ''Foil.NameBinder) (VarT p)) (VarT l) 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 @@ -14,7 +14,7 @@ import qualified Control.Monad.Foil as Foil import Control.Monad.Foil.TH.Util --- | Generate 'Foil.Sinkable' and 'Foil.CoSinkable' instances. +-- | Generate t'Control.Monad.Foil.Sinkable' and t'Control.Monad.Foil.CoSinkable' instances. -- -- @since 0.0.1 mkInstancesFoil @@ -83,7 +83,7 @@ where xi = mkName ("x" ++ show i) --- | Generate the 'Foil.CoSinkable' instance of the pattern type that +-- | Generate the t'Control.Monad.Foil.CoSinkable' instance of the pattern type that -- 'Control.Monad.Foil.TH.MkFoilData.mkFoilPattern' generates from a raw -- pattern type, given the raw types of identifiers and patterns. -- 'deriveCoSinkable' takes the scope-safe pattern type itself. @@ -143,7 +143,7 @@ xi = mkName ("x" ++ show i) -- The binders of the binding fields, in order, without going through - -- 'Foil.withPattern'. + -- 'Control.Monad.Foil.withPattern'. clauseNameBinderListOf :: Con -> Clause clauseNameBinderListOf (NormalC conName params) = Clause [ConP foilConName [] conParamPatterns] (NormalB body) [] @@ -201,7 +201,7 @@ where xi = mkName ("x" ++ show i) --- | Generate the 'Foil.CoSinkable' instance of a scope-safe pattern type. +-- | Generate the t'Control.Monad.Foil.CoSinkable' instance of a scope-safe pattern type. -- 'mkCoSinkableFoilPattern' takes the raw pattern type instead. -- -- > data Pat (n :: S) (l :: S) where @@ -210,9 +210,9 @@ -- > -- > deriveCoSinkable ''Pat -- --- A field is a 'Foil.NameBinder', a nested pattern, or a payload that +-- A field is a t'Control.Monad.Foil.NameBinder', a nested pattern, or a payload that -- mentions no scope. A payload indexed by a scope needs a hand-written --- instance (see 'Foil.transportPayload'). +-- instance (see 'Control.Monad.Foil.transportPayload'). -- -- @since 0.6.0 deriveCoSinkable :: Name -> Q [Dec] @@ -229,7 +229,7 @@ coSinkClauses <- mapM patternCoSinkabilityProofClause fields withPatClauses <- mapM patternWithPatternClause fields listClauses <- mapM patternNameBinderListOfClause fields - -- A pattern that nests itself has a recursive 'Foil.withPattern', which + -- A pattern that nests itself has a recursive 'Control.Monad.Foil.withPattern', which -- cannot inline. let recursive = or [ h == ConT patternT | (_, sorts) <- fields, PatternNested h <- sorts ] inline = [ PragmaD (InlineP 'Foil.withPattern Inline FunLike AllPhases) | not recursive ] @@ -243,8 +243,8 @@ -- | How a field of a pattern constructor takes part in its instance. data PatternField - = PatternBinder -- ^ A 'Foil.NameBinder'. - | PatternNested Type -- ^ A nested pattern, with its own 'Foil.CoSinkable'; its type's head. + = PatternBinder -- ^ A t'Control.Monad.Foil.NameBinder'. + | PatternNested Type -- ^ A nested pattern, with its own t'Control.Monad.Foil.CoSinkable'; its type's head. | PatternPayload -- ^ A field that mentions no scope. -- | The constructors of a pattern type, each with the sorts of its fields. @@ -305,7 +305,7 @@ PatternPayload -> False _ -> True --- | One 'Foil.coSinkabilityProof' clause: the binding fields are renamed in +-- | One 'Control.Monad.Foil.coSinkabilityProof' clause: the binding fields are renamed in -- turn, each with the renaming the previous one extended. patternCoSinkabilityProofClause :: (Name, [PatternField]) -> Q Clause patternCoSinkabilityProofClause (conName, sorts) = do @@ -323,10 +323,10 @@ body <- go rename (zip sorts xs) id return (Clause [VarP rename, ConP conName [] (map VarP xs), VarP cont] (NormalB body) []) --- | One 'Foil.withPattern' clause, in the form of +-- | One 'Control.Monad.Foil.withPattern' clause, in the form of -- 'Control.Monad.Free.Foil.TH.MkFreeFoil.mkFreeFoil': a binder field goes -- through @withBinder@ and extends the scope for the fields to its right, a --- nested pattern through its own 'Foil.withPattern', and the results compose +-- nested pattern through its own 'Control.Monad.Foil.withPattern', and the results compose -- left to right. patternWithPatternClause :: (Name, [PatternField]) -> Q Clause patternWithPatternClause (conName, sorts) = do @@ -368,13 +368,13 @@ [VarP withBinder, VarP unit_, VarP comp_, VarP scope, ConP conName [] (map VarP xs), VarP cont] (NormalB body) []) --- | One 'Foil.nameBinderListOf' clause: the binding fields, left to right. +-- | One 'Control.Monad.Foil.nameBinderListOf' clause: the binding fields, left to right. patternNameBinderListOfClause :: (Name, [PatternField]) -> Q Clause patternNameBinderListOfClause (conName, sorts) = do xs <- mapM (\i -> newName ("x" ++ show i)) [1 .. length sorts] let pats = [ if isBindingField s then VarP x else WildP | (s, x) <- zip sorts xs ] -- A binder is consed on directly. Only a nested pattern's list is - -- concatenated, since 'Foil.concatNameBinderLists' is recursive and + -- concatenated, since 'Control.Monad.Foil.concatNameBinderLists' is recursive and -- copies its first argument. list = \case [] -> ConE 'Foil.NameBinderListEmpty diff --git a/src/Control/Monad/Foil/Telescope.hs b/src/Control/Monad/Foil/Telescope.hs --- a/src/Control/Monad/Foil/Telescope.hs +++ b/src/Control/Monad/Foil/Telescope.hs @@ -144,8 +144,9 @@ -- unified? -- -- The verdict speaks about binders only, so the renaming it prescribes has to --- be applied before the payloads are compared, which is exactly what --- 'Control.Monad.Free.alphaEquivScoped' does to the body of a scoped term. +-- be applied before the payloads are compared, much as +-- 'Control.Monad.Free.Foil.alphaEquivScoped' takes it into account for the +-- body of a scoped term. -- Comparing them as they stand would report @(A : 𝕌) (x : A)@ and -- @(B : 𝕌) (y : B)@ as different, since the second payloads name different -- binders until the first ones have been identified. 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,1000 +1,61 @@ -{-# LANGUAGE DataKinds #-} -{-# LANGUAGE TypeOperators #-} -{-# LANGUAGE TypeFamilies #-} -{-# LANGUAGE DeriveAnyClass #-} -{-# LANGUAGE DeriveFoldable #-} -{-# LANGUAGE DeriveFunctor #-} -{-# LANGUAGE DeriveTraversable #-} -{-# LANGUAGE DeriveGeneric #-} -{-# LANGUAGE FlexibleContexts #-} -{-# LANGUAGE FlexibleInstances #-} -{-# LANGUAGE GADTs #-} -{-# LANGUAGE LambdaCase #-} -{-# LANGUAGE MultiParamTypeClasses #-} -{-# LANGUAGE PolyKinds #-} -{-# LANGUAGE QuantifiedConstraints #-} -{-# LANGUAGE RankNTypes #-} -{-# LANGUAGE ScopedTypeVariables #-} -{-# LANGUAGE StandaloneDeriving #-} -{-# LANGUAGE UndecidableInstances #-} --- | This module defines a variation of --- free scoped (relative) monads relying on the foil for --- the scope-safe efficient handling of the binders. --- --- See description of the approach in [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384). -module Control.Monad.Free.Foil where - -import Control.DeepSeq -import qualified Control.Monad.Foil.Internal as Foil -import Data.Bifoldable -import Data.Bitraversable -import Data.Bifunctor -import Data.ZipMatchK -import qualified Generics.Kind as Kind -import Generics.Kind (GenericK(..), Field, Exists, Var0, Var1, (:$:), Atom((:@:), Kon), (:+:), (:*:)) -import Data.IntMap.Strict (IntMap) -import qualified Data.IntMap.Strict as IntMap -import Data.Map (Map) -import qualified Data.Map as Map -import GHC.Generics (Generic) -import Unsafe.Coerce (unsafeCoerce) - --- | Scoped term under a (single) name binder. --- --- @since 0.0.1 -data ScopedAST binder sig n where - ScopedAST :: binder n l -> AST binder sig l -> ScopedAST binder sig n - --- INLINABLE, so that it specialises together with the instance for AST. -instance (forall x y. NFData (binder x y), forall l. NFData (AST binder sig l)) => NFData (ScopedAST binder sig n) where - {-# INLINABLE rnf #-} - rnf (ScopedAST binder body) = rnf binder `seq` rnf body - --- | A term, generated by a signature 'Bifunctor' @sig@, --- with (free) variables in scope @n@. --- --- @since 0.0.1 -data AST binder sig n where - -- | A (free) variable in scope @n@. - Var :: {-# UNPACK #-} !(Foil.Name n) -> AST binder sig n - -- | A non-variable syntactic construction specified by the signature 'Bifunctor' @sig@. - Node :: sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n - -deriving instance Generic (AST binder sig n) - --- | 'rnf' forces the names, the binders, and the nodes through the 'NFData' --- instance of the signature. GHC specialises it where the binder and the --- signature are known. On the λ-terms of the @nfdata@ benchmark, the --- specialised 'rnf' is about four times faster than the general one. -instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term)) - => NFData (AST binder sig n) where - -- Without a specialisation, each node is forced through dictionaries built - -- from the quantified constraints. The specialised rnf calls itself on the - -- subterms and inlines the signature's rnf. - {-# INLINABLE rnf #-} - rnf (Var name) = rnf name - rnf (Node node) = rnf node - -instance GenericK (ScopedAST binder sig) where - type RepK (ScopedAST binder sig) = - Exists Foil.S - (Field (Kon binder :@: Var1 :@: Var0) :*: Field (Kon AST :@: Kon binder :@: Kon sig :@: Var0)) - toK (Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)) = ScopedAST binder ast - fromK (ScopedAST binder ast) = Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast) - -instance GenericK (AST binder sig) where - type RepK (AST binder sig) = - Field (Foil.Name :$: Var0) - :+: Field (sig - :$: (Kon ScopedAST :@: Kon binder :@: Kon sig :@: Var0) - :@: (Kon AST :@: Kon binder :@: Kon sig :@: Var0)) - -instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (ScopedAST binder sig) -instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (AST binder sig) - -instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (ScopedAST binder sig) -instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (AST binder sig) - -instance Foil.InjectName (AST binder sig) where - injectName = Var - --- * Substitution - --- | Substitution for free (scoped monads). --- --- @since 0.0.1 -{-# INLINABLE substitute #-} -substitute - :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder) - => Foil.Scope o - -> Foil.Substitution (AST binder sig) i o - -> AST binder sig i - -> AST binder sig o -substitute scope subst term - -- An empty substitution maps every name to itself ('addRename' deletes - -- identity renames), so the result is the very term, and the coercion is - -- the one 'Foil.sink' performs. Substitutions go empty often: opening a - -- scoped term with its own binder's name is an identity rename, and under - -- a deterministic allocation policy a refreshed binder usually keeps its - -- name, deleting its entry. Binders that shadow the ambient scope are - -- left as they stand, as on the no-clash path below. A caller that wants - -- them refreshed asks 'substituteRefreshed'. - | Foil.nullSubst subst = unsafeCoerce term - | otherwise = go term - where - -- The substitution is known non-empty here, and it can only change - -- under a binder, so the walk between binders is unchecked and each - -- binder entry re-enters 'substitute', testing emptiness exactly once. - go = \case - Var name -> Foil.lookupSubst subst name - Node node -> Node (bimap f go node) - f (ScopedAST binder body) = - Foil.withRefreshedPattern scope binder $ \extendSubst binder' scope' -> - let subst' = extendSubst (Foil.sink subst) - body' = substitute scope' subst' body - in ScopedAST binder' body' - --- | Substitution for free (scoped monads). --- --- This is a version of 'substitute' that forces refreshing of all name binders, --- resulting in a term with normalized binders: --- --- > substituteRefreshed scope subst = refreshAST scope . subtitute scope subst --- --- In general, 'substitute' is more efficient since it does not always refresh binders. --- --- @since 0.0.3 -{-# INLINABLE substituteRefreshed #-} -substituteRefreshed - :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder) - => Foil.Scope 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.withFreshPattern scope binder $ \extendSubst binder' scope' -> - let subst' = extendSubst (Foil.sink subst) - body' = substituteRefreshed scope' subst' body - in ScopedAST binder' body' - --- | @'AST' sig@ is a monad relative to 'Foil.Name'. -instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) - => Foil.RelMonad Foil.Name (AST binder sig) where - rreturn = Var - rbind scope term subst = - case term of - Var name -> subst name - Node node -> Node (bimap g' g node) - where - g x = Foil.rbind scope x subst - g' (ScopedAST binder body) = - Foil.withRefreshedPattern' scope binder $ \extendSubst binder' scope' -> - let subst' = extendSubst subst - in ScopedAST binder' (Foil.rbind scope' body subst') - --- | Substitution for a single generalized pattern. --- --- @since 0.2.0 -{-# INLINABLE substitutePattern #-} -substitutePattern - :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder, Foil.SinkableK binder) - => Foil.Scope o -- ^ Resulting scope. - -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@. - -> binder' n i -- ^ Binders that extend scope @n@ to scope @i@. - -> [AST binder sig o] -- ^ A list of terms intended to serve as - -> AST binder sig i - -> AST binder sig o -substitutePattern scope env binders args body = - substitute scope env' body - where - env' = Foil.addSubstPattern env binders args - --- * Transformations between signatures - --- | Fold a term bottom-up into a scope-indexed carrier @r@. A variable goes --- through the first function, a scoped subterm through the second, given its --- binder and the fold of its body, and a node through the third, once its --- subterms are folded. The scope indices stay as they are, so the carrier --- can be another kind of term, as in 'hoistAST', or anything indexed by the --- scope, such as @'Const' Int@ for a node count. --- --- To change the binder type as well, map it in the second function: --- --- > foldAST Var (\binder body -> ScopedAST (toBinder binder) body) Node --- --- @since 0.6.0 -{-# INLINABLE foldAST #-} -foldAST - :: forall binder sig r s n. Bifunctor sig - => (forall m. Foil.Name m -> r m) -- ^ A variable. - -> (forall m l. binder m l -> r l -> s m) -- ^ A scoped subterm, from its binder and the fold of its body. - -> (forall m. sig (s m) (r m) -> r m) -- ^ A node, its subterms folded. - -> AST binder sig n - -> r n -foldAST var scoped node = go - where - go :: forall m. AST binder sig m -> r m - go (Var x) = var x - go (Node t) = node (bimap (\(ScopedAST binder body) -> scoped binder (go body)) go t) - --- | Change the signature of a term by a natural transformation of --- signatures, keeping the binders, as @hoistFree@ of the free package does --- for a free monad. Each node is rebuilt, so this costs a traversal. --- --- @since 0.6.0 -{-# INLINABLE hoistAST #-} -hoistAST - :: Bifunctor sig - => (forall a b. sig a b -> sig' a b) - -> AST binder sig n - -> AST binder sig' n -hoistAST f = foldAST Var ScopedAST (Node . f) - --- * \(\alpha\)-equivalence - --- | Refresh (force) all binders in a term, minimizing the used indices. --- --- @since 0.0.3 -{-# INLINABLE refreshAST #-} -refreshAST - :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder) - => Foil.Scope 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. --- --- @since 0.0.3 -{-# INLINABLE refreshScopedAST #-} -refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder) - => Foil.Scope n - -> ScopedAST binder sig n - -> ScopedAST binder sig n -refreshScopedAST scope (ScopedAST binder body) = - Foil.withFreshPattern scope binder $ \extendSubst binder' scope' -> - let subst = extendSubst (Foil.sink Foil.identitySubst) - in ScopedAST binder' (substituteRefreshed scope' subst body) - --- | \(\alpha\)-equivalence check for two terms in one scope --- via normalization of bound identifiers (via 'refreshAST'). --- --- Compared to 'alphaEquiv', this function renames every binder on both sides --- unconditionally, so it does strictly more work. It remains as an --- independent implementation of the same test. --- --- @since 0.0.3 -{-# INLINABLE alphaEquivRefreshed #-} -alphaEquivRefreshed - :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder) - => Foil.Scope n - -> AST binder sig n - -> AST binder sig n - -> Bool -alphaEquivRefreshed scope t1 t2 = refreshAST scope t1 `unsafeEqAST` refreshAST scope t2 - --- | A term is a scope-indexed value that can be compared up to α, which is what --- a pattern carrying terms as payloads needs of them. -instance (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.SinkableK binder) - => Foil.AlphaEquiv (AST binder sig) where - alphaEquivIn = alphaEquiv - --- | \(\alpha\)-equivalence check for two terms in one scope --- via unification of bound variables (via 'unifyNameBinders'). --- --- When two matching binders coincide, comparison continues with no work at --- all. When they differ, the prescribed renaming is /threaded down the --- recursion/ (see 'alphaEquivEnv') and consulted at variables only, so --- nothing is ever copied. Applying the renaming eagerly instead would --- materialise a renamed copy of the remaining body at every mismatched --- binder, which is quadratic on a chain of them. --- --- @since 0.0.3 -{-# INLINABLE alphaEquiv #-} -alphaEquiv - :: (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder) - => Foil.Scope n - -> AST binder sig n - -> AST binder sig n - -> Bool -alphaEquiv _scope (Var x) (Var y) = x == y -alphaEquiv scope (Node l) (Node r) = - case zipMatchWith2 (unit . alphaEquivScoped scope) (unit . alphaEquiv scope) l r of - Nothing -> False - Just _ -> True - where - unit f x = if f x then Just () else Nothing -alphaEquiv _ _ _ = False - --- | Same as 'alphaEquiv' but for scoped terms. --- --- While the binders of the two sides coincide, this runs with no renaming --- state at all. The first pair that differs switches to 'alphaEquivEnv', --- which threads the renamings down and switches back when they empty out. --- --- @since 0.0.3 -{-# INLINABLE alphaEquivScoped #-} -alphaEquivScoped - :: forall sig binder n. (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder) - => Foil.Scope n - -> ScopedAST binder sig n - -> ScopedAST binder sig n - -> Bool -alphaEquivScoped scope - (ScopedAST binder1 body1) - (ScopedAST binder2 body2) = - case Foil.unifyPatternsIn scope binder1 binder2 of - -- the binders coincide: compare the bodies as they stand - Foil.SameNameBinders{} -> -- after seeing this we know that body scopes are the same - case Foil.assertDistinct binder1 of - Foil.Distinct -> - let scope1 = Foil.extendScopePattern binder1 scope - in alphaEquiv scope1 body1 body2 - -- the left binder is renamed towards the right one - Foil.RenameLeftNameBinder _ rename1to2 -> - case Foil.assertDistinct binder2 of - Foil.Distinct -> - let scope2 = Foil.extendScopePattern binder2 scope - pairs = [ (Foil.nameId x, renamedId rename1to2 x) - | x <- Foil.namesOfPattern binder1 ] - in enterEnv pairs scope2 body1 body2 - -- the right binder is renamed towards the left one - Foil.RenameRightNameBinder _ rename2to1 -> - case Foil.assertDistinct binder1 of - Foil.Distinct -> - let scope1 = Foil.extendScopePattern binder1 scope - pairs = [ (renamedId rename2to1 y, Foil.nameId y) - | y <- Foil.namesOfPattern binder2 ] - in enterEnv pairs scope1 body1 body2 - -- both are renamed towards a unified pattern: pair the two sides' - -- names through the unified name each maps to - Foil.RenameBothBinders binder' rename1 rename2 -> - case Foil.assertDistinct binder' of - Foil.Distinct -> - let scope' = Foil.extendScopePattern binder' scope - leftU = IntMap.fromList - [ (renamedId rename1 x, Foil.nameId x) - | x <- Foil.namesOfPattern binder1 ] - rightU = IntMap.fromList - [ (renamedId rename2 y, Foil.nameId y) - | y <- Foil.namesOfPattern binder2 ] - pairs = IntMap.elems (IntMap.intersectionWith (,) leftU rightU) - in enterEnv pairs scope' body1 body2 - -- if we cannot unify patterns then scopes are not alpha-equivalent - Foil.NotUnifiable -> False - where - enterEnv - :: forall m l1 l2. Foil.Distinct m - => [(Int, Int)] -> Foil.Scope m - -> AST binder sig l1 -> AST binder sig l2 -> Bool - enterEnv pairs scope' = bindPairs 0 IntMap.empty IntMap.empty pairs scope' - --- | The raw name a verdict's renaming assigns to a pattern's name. --- --- @since 0.4.0 -renamedId :: (Foil.NameBinder n a -> Foil.NameBinder n b) -> Foil.Name a -> Int -renamedId rename = Foil.nameId . Foil.nameOf . rename . Foil.UnsafeNameBinder - --- | Bind the paired names of a binder pair. A pair whose names coincide --- shadows both sides identically and is deleted from the environments. A pair --- whose names differ binds both to one fresh level. Continues with --- 'alphaEquivEnv' on the bodies. --- --- @since 0.4.0 -bindPairs - :: forall sig binder m l1 l2. (Bitraversable sig, ZipMatchK sig, Foil.Distinct m, Foil.UnifiablePattern binder, Foil.SinkableK binder) - => Int -> IntMap Int -> IntMap Int -> [(Int, Int)] - -> Foil.Scope m - -> AST binder sig l1 -> AST binder sig l2 -> Bool -bindPairs lvl envL envR pairs scope body1 body2 = case pairs of - [] -> alphaEquivEnv lvl envL envR scope body1 body2 - ((x, y) : rest) - | x == y -> bindPairs lvl (IntMap.delete x envL) (IntMap.delete y envR) rest scope body1 body2 - | otherwise -> bindPairs (lvl + 1) (IntMap.insert x lvl envL) (IntMap.insert y lvl envR) rest scope body1 body2 - --- | The renaming-threading worker behind 'alphaEquiv': compare two terms --- under partial renamings of their names into shared /levels/. --- --- Each environment maps a raw name to the level of the binder pair that bound --- it on the comparison path, and a name outside its environment stands for --- itself. A variable occurrence then compares as a level against a level, or --- as a raw name against a raw name, and the two can never be conflated. This --- is what makes threading sound where applying a raw renaming at the variables --- would not be, since a renamed name could collide with one that passes --- through unchanged and happens to share the target spelling. Levels are also --- why no capture check is needed: a level is never a name, so there is nothing --- for a binder to capture. --- --- A binder pair whose names coincide /deletes/ those names from both --- environments, the pair shadowing both sides identically. When the --- environments empty out the comparison drops back to the stateless --- 'alphaEquiv', so only the region of the terms below a mismatched binder, --- and above the point where the mismatch is shadowed away, pays for the --- threading at all. --- --- The indices of the two terms are deliberately independent, in the style --- of 'unsafeEqAST': the terms are never renamed into a common scope, so --- no common index exists to give them. --- --- @since 0.4.0 -{-# INLINABLE alphaEquivEnv #-} -alphaEquivEnv - :: forall sig binder n n1 n2. (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder) - => Int -- ^ Next fresh level. - -> IntMap Int -- ^ Left renaming: raw name to the level that bound it. - -> IntMap Int -- ^ Right renaming. - -> Foil.Scope n -- ^ Scope along the unified path (consulted by 'Foil.unifyPatternsIn'). - -> AST binder sig n1 - -> AST binder sig n2 - -> Bool -alphaEquivEnv lvl envL envR scope t1 t2 - | IntMap.null envL && IntMap.null envR = - -- The renamings have emptied out (or never held anything): the - -- terms coincide raw-for-raw from here on, so compare them where - -- they stand. The coercion brings both indices to the scope's, - -- which is the unified path the comparison speaks of. - alphaEquiv scope (unsafeCoerce t1 :: AST binder sig n) (unsafeCoerce t2 :: AST binder sig n) - | otherwise = case (t1, t2) of - (Var x, Var y) -> - case (IntMap.lookup (Foil.nameId x) envL, IntMap.lookup (Foil.nameId y) envR) of - (Just k1, Just k2) -> k1 == k2 - (Nothing, Nothing) -> Foil.nameId x == Foil.nameId y - _ -> False - (Node l, Node r) -> - case zipMatchWith2 - (unit . alphaEquivScopedEnv lvl envL envR scope) - (unit . alphaEquivEnv lvl envL envR scope) l r of - Nothing -> False - Just _ -> True - _ -> False - where - unit f x = if f x then Just () else Nothing - --- | The scoped half of 'alphaEquivEnv': get the verdict from --- 'Foil.unifyPatternsIn', extend the environments as it prescribes, and --- recurse into the bodies as they stand. --- --- @since 0.4.0 -{-# INLINABLE alphaEquivScopedEnv #-} -alphaEquivScopedEnv - :: forall sig binder n n1 n2. (Bitraversable sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder) - => Int - -> IntMap Int - -> IntMap Int - -> Foil.Scope n - -> ScopedAST binder sig n1 - -> ScopedAST binder sig n2 - -> Bool -alphaEquivScopedEnv lvl envL envR scope scoped1 scoped2 = - -- The scoped terms are compared where they stand; the coercion only - -- brings their indices to the scope's, which is the unified path the - -- environments and the verdicts speak of. - case (unsafeCoerce scoped1 :: ScopedAST binder sig n, unsafeCoerce scoped2 :: ScopedAST binder sig n) of - (ScopedAST binder1 body1, ScopedAST binder2 body2) -> - case Foil.unifyPatternsIn scope binder1 binder2 of - -- the binders coincide: the pair shadows both sides identically - Foil.SameNameBinders{} -> - case Foil.assertDistinct binder1 of - Foil.Distinct -> - let scope' = Foil.extendScopePattern binder1 scope - names = map Foil.nameId (Foil.namesOfPattern binder1) - envL' = deleteAll names envL - envR' = deleteAll names envR - in alphaEquivEnv lvl envL' envR' scope' body1 body2 - -- the left binder is renamed towards the right one - Foil.RenameLeftNameBinder _ rename1to2 -> - case Foil.assertDistinct binder2 of - Foil.Distinct -> - let scope' = Foil.extendScopePattern binder2 scope - pairs = [ (Foil.nameId x, renamedId rename1to2 x) - | x <- Foil.namesOfPattern binder1 ] - in bindPairs lvl envL envR pairs scope' body1 body2 - -- the right binder is renamed towards the left one - Foil.RenameRightNameBinder _ rename2to1 -> - case Foil.assertDistinct binder1 of - Foil.Distinct -> - let scope' = Foil.extendScopePattern binder1 scope - pairs = [ (renamedId rename2to1 y, Foil.nameId y) - | y <- Foil.namesOfPattern binder2 ] - in bindPairs lvl envL envR pairs scope' body1 body2 - -- both are renamed towards a unified pattern: pair the two sides' - -- names through the unified name each maps to - Foil.RenameBothBinders binder' rename1 rename2 -> - case Foil.assertDistinct binder' of - Foil.Distinct -> - let scope' = Foil.extendScopePattern binder' scope - leftU = IntMap.fromList - [ (renamedId rename1 x, Foil.nameId x) - | x <- Foil.namesOfPattern binder1 ] - rightU = IntMap.fromList - [ (renamedId rename2 y, Foil.nameId y) - | y <- Foil.namesOfPattern binder2 ] - pairs = IntMap.elems (IntMap.intersectionWith (,) leftU rightU) - in bindPairs lvl envL envR pairs scope' body1 body2 - Foil.NotUnifiable -> False - where - deleteAll names env = case names of - [] -> env - (i : is) -> deleteAll is (IntMap.delete i env) - --- ** Unsafe equality checks - --- | /Unsafe/ equality check for two terms. --- This check ignores the possibility that two terms might have different --- scope extensions under binders (which might happen due to substitution --- under a binder in absence of name conflicts). --- --- @since 0.0.3 -{-# INLINABLE unsafeEqAST #-} -unsafeEqAST - :: (Bitraversable sig, ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l) - => AST binder sig n - -> AST binder sig l - -> Bool -unsafeEqAST (Var x) (Var y) = Foil.nameId x == Foil.nameId y -unsafeEqAST (Node t1) (Node t2) = - case zipMatchWith2 (unit . unsafeEqScopedAST) (unit . unsafeEqAST) t1 t2 of - Nothing -> False - Just _ -> True - where - unit f x = if f x then Just () else Nothing -unsafeEqAST _ _ = False - --- | A version of 'unsafeEqAST' for scoped terms. --- --- @since 0.0.3 -{-# INLINABLE unsafeEqScopedAST #-} -unsafeEqScopedAST - :: (Bitraversable sig, ZipMatchK 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 - [ Foil.unsafeEqPattern binder1 binder2 - , case (Foil.assertDistinct binder1, Foil.assertDistinct binder2) of - (Foil.Distinct, Foil.Distinct) -> body1 `unsafeEqAST` body2 - ] - --- * Converting to and from free foil - --- ** Convert to free foil - --- | An identifier a raw term mentions that the names given for conversion do --- not account for. --- --- Note what this does and does not carry. It cannot carry a position: the --- conversion functions are generic in the raw term and only ever see it through --- @toSig@, so a source location, if the syntax has one, is not theirs to read. --- What they do know, and a caller checking names beforehand does not, is which --- names were in scope /at the occurrence/, the binders passed on the way down --- included. That is what a \"did you mean\" needs. --- --- @since 0.4.0 -data UnresolvedName rawIdent = UnresolvedName - { unresolvedIdent :: rawIdent - -- ^ The identifier that did not resolve. - , unresolvedInScope :: [rawIdent] - -- ^ What was in scope where it occurred. - } deriving (Eq, Show, Functor, Foldable, Traversable) - --- | The identifiers a raw term mentions that a set of names cannot resolve, in --- the order they occur. --- --- This is 'unsafeConvertToAST' with the conversion left out, so it descends --- under binders in the same way and accounts for what they bind. --- --- @since 0.4.0 -unresolvedNames - :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n. - (Foil.Distinct n, Bifoldable sig, Ord rawIdent, Foil.CoSinkable binder) - => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) - -- ^ 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@. - -> rawTerm - -- ^ Raw term. - -> [UnresolvedName rawIdent] -unresolvedNames toSig fromRawPattern getScopedTerm = go - where - go :: forall x. Foil.Distinct x - => Foil.Scope x -> Map rawIdent (Foil.Name x) -> rawTerm -> [UnresolvedName rawIdent] - go scope names t = case toSig t of - Left x - | Map.member x names -> [] - | otherwise -> [UnresolvedName x (Map.keys names)] - Right node -> bifoldMap (goScoped scope names) (go scope names) node - - goScoped :: forall x. Foil.Distinct x - => Foil.Scope x -> Map rawIdent (Foil.Name x) - -> (rawPattern, rawScopedTerm) -> [UnresolvedName rawIdent] - goScoped scope names (pat, scopedTerm) = - fromRawPattern scope names pat $ \binder' names' -> - go (Foil.extendScopePattern binder' scope) names' (getScopedTerm scopedTerm) - --- | Convert a raw term into a scope-safe term, reporting the first identifier --- that does not resolve. --- --- One pass, short-circuiting at the first failure, so a term that resolves --- costs no more than 'unsafeConvertToAST' does. The report is complete for --- that one identifier, since 'unresolvedInScope' is built where the conversion --- fails and is never computed on the way through. --- --- A caller wanting /every/ unresolved identifier rather than the first pays a --- second pass for it, with 'unresolvedNames'. The successful path stays fast --- that way, and a failure can afford to be walked again for a better message. --- --- @since 0.4.0 -tryConvertToAST - :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n. - (Foil.Distinct n, Bitraversable sig, Ord rawIdent, - Foil.CoSinkable binder, Foil.SinkableK binder) - => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) - -- ^ 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@. - -> rawTerm - -- ^ Raw term. - -> Either (UnresolvedName rawIdent) (AST binder sig n) -tryConvertToAST toSig fromRawPattern getScopedTerm scope names = - tryConvertToASTWith toSig fromRawPattern getScopedTerm scope names Map.empty - --- | Convert a raw term into a scope-safe term, resolving some identifiers to --- whole terms rather than to variables. --- --- The extra table is what a language with /constants/ needs: an identifier that --- denotes a top-level declaration, a primitive, or an abbreviation stands for --- something that is not a variable, and resolving it during conversion is the --- only place where the binders are known. Doing it in a pass of one's own means --- writing a binder-aware traversal of the raw syntax by hand. --- --- Variables win: the table of names is consulted first, so a binder shadows an --- entry here, and an entry here shadows nothing. The table is sunk when going --- under a binder, exactly as the names are, so its entries may mention anything --- in scope where conversion started and need not be closed. --- --- @since 0.4.0 -tryConvertToASTWith - :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n. - (Foil.Distinct n, Bitraversable sig, Ord rawIdent, - Foil.CoSinkable binder, Foil.SinkableK binder) - => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) - -- ^ 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@. - -> Map rawIdent (AST binder sig n) - -- ^ Identifiers that denote a term rather than a variable. - -> rawTerm - -- ^ Raw term. - -> Either (UnresolvedName rawIdent) (AST binder sig n) -tryConvertToASTWith toSig fromRawPattern getScopedTerm = go - where - go :: forall x. Foil.Distinct x - => Foil.Scope x -> Map rawIdent (Foil.Name x) - -> Map rawIdent (AST binder sig x) -> rawTerm - -> Either (UnresolvedName rawIdent) (AST binder sig x) - go scope names terms t = case toSig t of - Left x -> case Map.lookup x names of - Just name -> Right (Var name) - Nothing -> case Map.lookup x terms of - Just term -> Right term - Nothing -> Left (UnresolvedName x (Map.keys names <> Map.keys terms)) - Right node -> - Node <$> bitraverse (goScoped scope names terms) (go scope names terms) node - - goScoped :: forall x. Foil.Distinct x - => Foil.Scope x -> Map rawIdent (Foil.Name x) - -> Map rawIdent (AST binder sig x) - -> (rawPattern, rawScopedTerm) - -> Either (UnresolvedName rawIdent) (ScopedAST binder sig x) - goScoped scope names terms (pat, scopedTerm) = - fromRawPattern scope names pat $ \binder' names' -> - ScopedAST binder' - <$> go (Foil.extendScopePattern binder' scope) names' - (Foil.sink1 terms) (getScopedTerm scopedTerm) - --- | Convert a raw term into a scope-safe term, calling 'error' on an --- identifier that does not resolve. --- --- Prefer 'tryConvertToAST', which reports such identifiers. This is for callers --- that have already established that every name resolves. --- --- @since 0.4.0 -unsafeConvertToAST - :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder) - => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) - -- ^ 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@. - -> rawTerm - -- ^ Raw term. - -> AST binder sig n -unsafeConvertToAST toSig fromRawPattern getScopedTerm scope names t = - case toSig t of - Left x -> - case Map.lookup x names of - Nothing -> error "undefined variable" - Just name -> Var name - Right node -> Node $ - bimap - (unsafeConvertToScopedAST toSig fromRawPattern getScopedTerm scope names) - (unsafeConvertToAST toSig fromRawPattern getScopedTerm scope names) - node - --- | Same as 'unsafeConvertToAST' but for scoped terms. --- --- @since 0.4.0 -unsafeConvertToScopedAST - :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder) - => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) - -- ^ 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) - -- ^ A pair of a pattern and a corresponding scoped term. - -> ScopedAST binder sig n -unsafeConvertToScopedAST toSig fromRawPattern getScopedTerm scope names (pat, scopedTerm) = - fromRawPattern scope names pat $ \binder' names' -> - let scope' = Foil.extendScopePattern binder' scope - in ScopedAST binder' (unsafeConvertToAST toSig fromRawPattern getScopedTerm scope' names' (getScopedTerm scopedTerm)) - --- ** Convert from free foil - --- | Convert a scope-safe term back into a raw term. --- --- @since 0.0.3 -convertFromAST - :: Bifunctor sig - => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm) - -- ^ Peel back one layer of syntax. - -> (rawIdent -> rawTerm) - -- ^ Convert identifier into a raw variable term. - -> (forall x y. binder x y -> rawPattern) - -- ^ Convert scope-safe pattern into a raw pattern. - -> (rawTerm -> rawScopedTerm) - -- ^ 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 $ - bimap - (convertFromScopedAST fromSig fromVar makePattern makeScoped f) - (convertFromAST fromSig fromVar makePattern makeScoped f) - node - --- | Same as 'convertFromAST' but for scoped terms. --- --- @since 0.0.3 -convertFromScopedAST - :: Bifunctor sig - => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm) - -- ^ Peel back one layer of syntax. - -> (rawIdent -> rawTerm) - -- ^ Convert identifier into a raw variable term. - -> (forall x y. binder x y -> rawPattern) - -- ^ Convert scope-safe pattern into a raw pattern. - -> (rawTerm -> 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 binder - , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body)) - --- | Convert a scope-safe term back into a raw term, naming the variables that --- occur /free in the whole term/ separately from the bound ones. --- --- 'convertFromAST' applies one naming function to every variable it meets, --- bound or free, and gives it only a raw name. That is often not enough, since --- raw names are not unique across scope indices: a binder inside a term may --- share one with a name of the ambient scope, so naming by raw name alone can --- print a bound variable as whatever the ambient scope calls that name. --- --- Keeping the typed name is what distinguishes them, and 'Foil.unsinkNamePattern' --- is the operation for it: composing one per binder on the way down builds a --- @'Foil.Name' x -> 'Maybe' ('Foil.Name' n)@ that answers exactly the question. --- --- @since 0.4.0 -convertFromASTWith - :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n. - (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder) - => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm) - -- ^ Peel back one layer of syntax. - -> (rawIdent -> rawTerm) - -- ^ Convert identifier into a raw variable term. - -> (forall x y. binder x y -> rawPattern) - -- ^ Convert scope-safe pattern into a raw pattern. - -> (rawTerm -> rawScopedTerm) - -- ^ Wrap raw term into a scoped term. - -> (Foil.Name n -> rawIdent) - -- ^ Name a variable that is free in the whole term. - -> (Int -> rawIdent) - -- ^ Name a bound variable, from its underlying integer identifier. - -> AST binder sig n - -- ^ Scope-safe term. - -> rawTerm -convertFromASTWith fromSig fromVar makePattern makeScoped freeName boundName = - go Just - where - go :: forall x. Foil.Distinct x - => (Foil.Name x -> Maybe (Foil.Name n)) -> AST binder sig x -> rawTerm - go unsink = \case - Var x -> fromVar $ case unsink x of - Just name -> freeName name - Nothing -> boundName (Foil.nameId x) - Node node -> fromSig (bimap (goScoped unsink) (go unsink) node) - - goScoped :: forall x. Foil.Distinct x - => (Foil.Name x -> Maybe (Foil.Name n)) - -> ScopedAST binder sig x -> (rawPattern, rawScopedTerm) - goScoped unsink (ScopedAST binder body) = - case Foil.assertDistinct binder of - Foil.Distinct -> - ( makePattern binder - , makeScoped - (go (\name -> Foil.unsinkNamePattern binder name >>= unsink) body) ) - --- ** Unsinking AST - --- | The support of a term: exactly the names that occur free in it. --- --- This is the annotation that co-de-Bruijn syntax carries intrinsically and --- that the foil, having global names and therefore free weakening, does not. --- Computing it is \(O(size)\); a client that restricts often should cache it. --- --- @since 0.4.0 -supportOf - :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) - => AST binder sig n -> Foil.NameSet n -supportOf = \case - Var name -> Foil.nameSetSingleton name - Node node -> bifoldMap supportOfScopedAST supportOf node - --- | The support of a scoped term, in the scope /outside/ its binder. --- --- @since 0.4.0 -supportOfScopedAST - :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) - => ScopedAST binder sig n -> Foil.NameSet n -supportOfScopedAST (ScopedAST binder body) = - case Foil.assertDistinct binder of - Foil.Distinct -> Foil.unsinkNameSet binder (supportOf body) - --- | Cut a term down to the scope of exactly the names it uses. --- --- This is the a-priori form of restriction, and the cheap one: the term --- inhabits the smaller scope /by construction/, so nothing is tested and --- nothing can fail. @'Foil.Ext' m n@ comes back with it, so the term can be --- 'Foil.sink'ed to where it came from for free. --- --- Verifying a declared dependency, such as a @uses@ clause or a module's --- parameters, is this plus a comparison: compute the scope a term really --- inhabits, and check the declared one against it. --- --- @since 0.4.0 -withRelevantScope - :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) - => AST binder sig n - -> (forall m. (Foil.Ext m n, Foil.Distinct m) - => Foil.Scope m -> AST binder sig m -> r) - -> r -withRelevantScope term cont = - Foil.withRestrictedScope (supportOf term) $ \scope -> - cont scope (unsafeCoerce term) - --- | Unsink an AST from a larger scope to a smaller scope. --- --- This is the a-posteriori form, and the one that has to be paid for: the --- term's support is computed and compared against the scope. When it succeeds --- the term itself is untouched, since restriction of a term that does inhabit --- the smaller scope is a coercion. --- --- @since 0.3.0 -unsinkAST - :: (Foil.Distinct l, Foil.CoSinkable binder, Bifoldable sig) - => Foil.Scope n -> AST binder sig l -> Maybe (AST binder sig n) -unsinkAST scope term - | Foil.nameSetSubsetOfScope (supportOf term) scope = Just (unsafeCoerce term) - | otherwise = Nothing - --- | Get the free variables of an AST. --- --- These come from 'supportOf', so they are distinct and in ascending order of --- their identifiers. --- --- @since 0.3.0 -freeVarsOf - :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) - => AST binder sig n -> [Foil.Name n] -freeVarsOf = Foil.nameSetToList . supportOf - --- | Get the free variables of a scoped AST, in the scope outside its binder. --- --- @since 0.3.0 -freeVarsOfScopedAST - :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) - => ScopedAST binder sig n -> [Foil.Name n] -freeVarsOfScopedAST = Foil.nameSetToList . supportOfScopedAST +-- | This module defines a variation of +-- free scoped (relative) monads relying on the foil for +-- the scope-safe efficient handling of the binders. +-- +-- See description of the approach in [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384). +module Control.Monad.Free.Foil ( + -- * Terms + AST(..), + ScopedAST(..), + + -- * Substitution + substitute, + substituteRefreshed, + substitutePattern, + + -- * Transformations between signatures + foldAST, + hoistAST, + + -- * \(\alpha\)-equivalence + refreshAST, + refreshScopedAST, + alphaEquivRefreshed, + alphaEquiv, + alphaEquivScoped, + renamedId, + bindPairs, + alphaEquivEnv, + alphaEquivScopedEnv, + + -- ** Unsafe equality checks + unsafeEqAST, + unsafeEqScopedAST, + unsafeEqASTIn, + unsafeEqScopedASTIn, + + -- * Converting to and from free foil + -- ** Convert to free foil + UnresolvedName(..), + unresolvedNames, + unresolvedNamesWith, + tryConvertToAST, + tryConvertToASTWith, + unsafeConvertToAST, + unsafeConvertToScopedAST, + + -- ** Convert from free foil + convertFromAST, + convertFromScopedAST, + convertFromASTWith, + + -- ** Unsinking AST + supportOf, + supportOfScopedAST, + withRelevantScope, + unsinkAST, + freeVarsOf, + freeVarsOfScopedAST, +) where + +import Control.Monad.Free.Foil.Internal diff --git a/src/Control/Monad/Free/Foil/Binary.hs b/src/Control/Monad/Free/Foil/Binary.hs --- a/src/Control/Monad/Free/Foil/Binary.hs +++ b/src/Control/Monad/Free/Foil/Binary.hs @@ -16,7 +16,7 @@ -- and nothing else in the library does. (The dependency this costs is -- @binary@, a GHC boot library.) -- --- Note that decoding /mints/ scope evidence: a 'Foil.Name' comes back at +-- Note that decoding /mints/ scope evidence: a t'Control.Monad.Foil.Name' comes back at -- whatever scope index the context asks for, and the existential scope -- under a binder is chosen arbitrarily. Thus the instances are a trust -- boundary, in the sense of 'Control.Monad.Foil.Blocks.checkExtScope'. The diff --git a/src/Control/Monad/Free/Foil/Internal.hs b/src/Control/Monad/Free/Foil/Internal.hs new file mode 100644 --- /dev/null +++ b/src/Control/Monad/Free/Foil/Internal.hs @@ -0,0 +1,1222 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE TypeOperators #-} +{-# LANGUAGE TypeFamilies #-} +{-# LANGUAGE DeriveAnyClass #-} +{-# LANGUAGE DeriveFoldable #-} +{-# LANGUAGE DeriveFunctor #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE DeriveGeneric #-} +{-# LANGUAGE FlexibleContexts #-} +{-# LANGUAGE FlexibleInstances #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE MultiParamTypeClasses #-} +{-# LANGUAGE PolyKinds #-} +{-# LANGUAGE QuantifiedConstraints #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE ScopedTypeVariables #-} +{-# LANGUAGE StandaloneDeriving #-} +{-# LANGUAGE UndecidableInstances #-} +-- | The implementation of "Control.Monad.Free.Foil", together with the +-- definitions it does not export, such as the loops behind α-equivalence. +-- Use "Control.Monad.Free.Foil" instead, unless you need those. +-- +-- @since 0.6.1 +module Control.Monad.Free.Foil.Internal where + +import Control.DeepSeq +import qualified Control.Monad.Foil.Internal as Foil +import Data.Bifoldable +import Data.Bitraversable +import Data.Bifunctor +import Data.ZipMatchK +import qualified Generics.Kind as Kind +import Generics.Kind (GenericK(..), Field, Exists, Var0, Var1, (:$:), Atom((:@:), Kon), (:+:), (:*:)) +import Data.IntMap.Strict (IntMap) +import qualified Data.IntMap.Strict as IntMap +import Data.Map (Map) +import qualified Data.Map as Map +import GHC.Generics (Generic) +import Unsafe.Coerce (unsafeCoerce) + +-- | Scoped term under a binder, which may be a pattern binding several names. +-- +-- @since 0.0.1 +data ScopedAST binder sig n where + ScopedAST :: binder n l -> AST binder sig l -> ScopedAST binder sig n + +-- INLINABLE, so that it specialises together with the instance for AST. +instance (forall x y. NFData (binder x y), forall l. NFData (AST binder sig l)) => NFData (ScopedAST binder sig n) where + {-# INLINABLE rnf #-} + rnf (ScopedAST binder body) = rnf binder `seq` rnf body + +-- | A term, generated by a signature 'Bifunctor' @sig@, +-- with (free) variables in scope @n@. +-- +-- @since 0.0.1 +data AST binder sig n where + -- | A (free) variable in scope @n@. + Var :: {-# UNPACK #-} !(Foil.Name n) -> AST binder sig n + -- | A non-variable syntactic construction specified by the signature 'Bifunctor' @sig@. + Node :: sig (ScopedAST binder sig n) (AST binder sig n) -> AST binder sig n + +deriving instance Generic (AST binder sig n) + +-- | 'rnf' forces the names, the binders, and the nodes through the 'NFData' +-- instance of the signature. GHC specialises it where the binder and the +-- signature are known. On the λ-terms of the @nfdata@ benchmark, the +-- specialised 'rnf' is about four times faster than the general one. +instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term)) + => NFData (AST binder sig n) where + -- Without a specialisation, each node is forced through dictionaries built + -- from the quantified constraints. The specialised rnf calls itself on the + -- subterms and inlines the signature's rnf. + {-# INLINABLE rnf #-} + rnf (Var name) = rnf name + rnf (Node node) = rnf node + +instance GenericK (ScopedAST binder sig) where + type RepK (ScopedAST binder sig) = + Exists Foil.S + (Field (Kon binder :@: Var1 :@: Var0) :*: Field (Kon AST :@: Kon binder :@: Kon sig :@: Var0)) + toK (Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast)) = ScopedAST binder ast + fromK (ScopedAST binder ast) = Kind.Exists (Kind.Field binder Kind.:*: Kind.Field ast) + +instance GenericK (AST binder sig) where + type RepK (AST binder sig) = + Field (Foil.Name :$: Var0) + :+: Field (sig + :$: (Kon ScopedAST :@: Kon binder :@: Kon sig :@: Var0) + :@: (Kon AST :@: Kon binder :@: Kon sig :@: Var0)) + +instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (ScopedAST binder sig) +instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.Sinkable (AST binder sig) + +instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (ScopedAST binder sig) +instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) => Foil.SinkableK (AST binder sig) + +instance Foil.InjectName (AST binder sig) where + injectName = Var + +-- * Substitution + +-- | Substitution for free (scoped monads). +-- +-- @since 0.0.1 +{-# INLINE substitute #-} +substitute + :: forall sig binder o i. (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder) + => Foil.Scope o + -> Foil.Substitution (AST binder sig) i o + -> AST binder sig i + -> AST binder sig o +substitute = goSubst + where + -- The loop is local and takes the instances from 'substitute', so once + -- 'substitute' is inlined at a known signature, the loop uses that + -- signature's instances directly. + goSubst + :: Foil.Distinct o' + => Foil.Scope o' + -> Foil.Substitution (AST binder sig) i' o' + -> AST binder sig i' + -> AST binder sig o' + goSubst scope subst term + -- An empty substitution maps every name to itself ('addRename' deletes + -- identity renames), so the result is the very term, and the coercion is + -- the one 'Control.Monad.Foil.sink' performs. Substitutions go empty often: opening a + -- scoped term with its own binder's name is an identity rename, and under + -- a deterministic allocation policy a refreshed binder usually keeps its + -- name, deleting its entry. Binders that shadow the ambient scope are + -- left as they stand, as on the no-clash path below. A caller that wants + -- them refreshed asks 'substituteRefreshed'. + | Foil.nullSubst subst = unsafeCoerce term + | otherwise = go term + where + -- The substitution is known non-empty here, and it can only change + -- under a binder, so the walk between binders is unchecked and each + -- binder entry re-enters 'goSubst', testing emptiness exactly once. + go = \case + Var name -> Foil.lookupSubst subst name + Node node -> Node (bimap f go node) + f (ScopedAST binder body) = + Foil.withRefreshedPattern scope binder $ \extendSubst binder' scope' -> + let subst' = extendSubst (Foil.sink subst) + body' = goSubst scope' subst' body + in ScopedAST binder' body' + +-- | A version of 'substitute' that refreshes every binder of the input term. +-- +-- The substituted terms are inserted as they are, so their binders are not +-- refreshed. Apply 'refreshAST' to the result to normalize all of its binders. +-- +-- In general, 'substitute' is more efficient since it does not always refresh binders. +-- +-- @since 0.0.3 +{-# INLINABLE substituteRefreshed #-} +substituteRefreshed + :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder, Foil.SinkableK binder) + => Foil.Scope 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.withFreshPattern scope binder $ \extendSubst binder' scope' -> + let subst' = extendSubst (Foil.sink subst) + body' = substituteRefreshed scope' subst' body + in ScopedAST binder' body' + +-- | @'AST' binder sig@ is a monad relative to t'Control.Monad.Foil.Name'. +instance (Bifunctor sig, Foil.CoSinkable binder, Foil.SinkableK binder) + => Foil.RelMonad Foil.Name (AST binder sig) where + rreturn = Var + rbind scope term subst = + case term of + Var name -> subst name + Node node -> Node (bimap g' g node) + where + g x = Foil.rbind scope x subst + g' (ScopedAST binder body) = + Foil.withRefreshedPattern' scope binder $ \extendSubst binder' scope' -> + let subst' = extendSubst subst + in ScopedAST binder' (Foil.rbind scope' body subst') + +-- | Substitute terms for the names a pattern binds in a body, and apply an +-- environment to the body's other names. +-- +-- @since 0.2.0 +{-# INLINABLE substitutePattern #-} +substitutePattern + :: (Bifunctor sig, Foil.Distinct o, Foil.CoSinkable binder', Foil.CoSinkable binder, Foil.SinkableK binder) + => Foil.Scope o -- ^ Resulting scope. + -> Foil.Substitution (AST binder sig) n o -- ^ Environment mapping names in scope @n@. + -> binder' n i -- ^ Binders that extend scope @n@ to scope @i@. + -> [AST binder sig o] -- ^ Terms for the bound names, in binding order ('error' if too few, extras ignored). + -> AST binder sig i + -> AST binder sig o +substitutePattern scope env binders args body = + substitute scope env' body + where + env' = Foil.addSubstPattern env binders args + +-- * Transformations between signatures + +-- | Fold a term bottom-up into a scope-indexed carrier @r@. A variable goes +-- through the first function, a scoped subterm through the second, given its +-- binder and the fold of its body, and a node through the third, once its +-- subterms are folded. The scope indices stay as they are, so the carrier +-- can be another kind of term, as in 'hoistAST', or anything indexed by the +-- scope, such as @'Const' Int@ for a node count. +-- +-- To change the binder type as well, map it in the second function: +-- +-- > foldAST Var (\binder body -> ScopedAST (toBinder binder) body) Node +-- +-- @since 0.6.0 +{-# INLINABLE foldAST #-} +foldAST + :: forall binder sig r s n. Bifunctor sig + => (forall m. Foil.Name m -> r m) -- ^ A variable. + -> (forall m l. binder m l -> r l -> s m) -- ^ A scoped subterm, from its binder and the fold of its body. + -> (forall m. sig (s m) (r m) -> r m) -- ^ A node, its subterms folded. + -> AST binder sig n + -> r n +foldAST var scoped node = go + where + go :: forall m. AST binder sig m -> r m + go (Var x) = var x + go (Node t) = node (bimap (\(ScopedAST binder body) -> scoped binder (go body)) go t) + +-- | Change the signature of a term by a natural transformation of +-- signatures, keeping the binders, as @hoistFree@ of the free package does +-- for a free monad. Each node is rebuilt, so this costs a traversal. +-- +-- @since 0.6.0 +{-# INLINABLE hoistAST #-} +hoistAST + :: Bifunctor sig + => (forall a b. sig a b -> sig' a b) + -> AST binder sig n + -> AST binder sig' n +hoistAST f = foldAST Var ScopedAST (Node . f) + +-- * \(\alpha\)-equivalence + +-- | Refresh (force) all binders in a term, minimizing the used indices. +-- +-- @since 0.0.3 +{-# INLINABLE refreshAST #-} +refreshAST + :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder) + => Foil.Scope 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. +-- +-- @since 0.0.3 +{-# INLINABLE refreshScopedAST #-} +refreshScopedAST :: (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder, Foil.SinkableK binder) + => Foil.Scope n + -> ScopedAST binder sig n + -> ScopedAST binder sig n +refreshScopedAST scope (ScopedAST binder body) = + Foil.withFreshPattern scope binder $ \extendSubst binder' scope' -> + let subst = extendSubst (Foil.sink Foil.identitySubst) + in ScopedAST binder' (substituteRefreshed scope' subst body) + +-- | \(\alpha\)-equivalence check for two terms in one scope +-- via normalization of bound identifiers (via 'refreshAST'). +-- +-- Compared to 'alphaEquiv', this function renames every binder on both sides +-- unconditionally, so it does strictly more work. It remains as an +-- independent implementation of the same test. Like 'alphaEquiv', it compares +-- patterns with 'Control.Monad.Foil.unifyPatternsIn', so the payloads of a +-- pattern are compared as well. +-- +-- @since 0.0.3 +{-# INLINABLE alphaEquivRefreshed #-} +alphaEquivRefreshed + :: (Bifunctor sig, ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder, Foil.SinkableK binder) + => Foil.Scope n + -> AST binder sig n + -> AST binder sig n + -> Bool +alphaEquivRefreshed scope t1 t2 = + unsafeEqASTIn scope (refreshAST scope t1) (refreshAST scope t2) + +-- | A term is a scope-indexed value that can be compared up to α, which is what +-- a pattern carrying terms as payloads needs of them. +instance (ZipMatchK sig, Foil.UnifiablePattern binder) + => Foil.AlphaEquiv (AST binder sig) where + alphaEquivIn = alphaEquiv + +-- | \(\alpha\)-equivalence check for two terms in one scope +-- via unification of bound variables (via 'unifyNameBinders'). +-- +-- When two matching binders coincide, comparison continues with no work at +-- all. When they differ, the prescribed renaming is /threaded down the +-- recursion/ (see 'alphaEquivEnv') and consulted at variables only, so +-- nothing is ever copied. Applying the renaming eagerly instead would +-- materialise a renamed copy of the remaining body at every mismatched +-- binder, which is quadratic on a chain of them. +-- +-- @since 0.0.3 +{-# INLINE alphaEquiv #-} +alphaEquiv + :: (ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder) + => Foil.Scope n + -> AST binder sig n + -> AST binder sig n + -> Bool +alphaEquiv = aeAlphaEquiv alphaEquivLoops + +-- | Same as 'alphaEquiv' but for scoped terms. +-- +-- While the binders of the two sides coincide, this runs with no renaming +-- state at all. The first pair that differs switches to 'alphaEquivEnv', +-- which threads the renamings down and switches back when they empty out. +-- +-- @since 0.0.3 +{-# INLINE alphaEquivScoped #-} +alphaEquivScoped + :: forall sig binder n. (ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder) + => Foil.Scope n + -> ScopedAST binder sig n + -> ScopedAST binder sig n + -> Bool +alphaEquivScoped = aeAlphaEquivScoped alphaEquivLoops + +-- | The raw name a verdict's renaming assigns to a pattern's name. +-- +-- @since 0.4.0 +renamedId :: (Foil.NameBinder n a -> Foil.NameBinder n b) -> Foil.Name a -> Int +renamedId rename = Foil.nameId . Foil.nameOf . rename . Foil.UnsafeNameBinder + +-- | Bind the paired names of a binder pair. A pair whose names coincide +-- shadows both sides identically and is deleted from the environments. A pair +-- whose names differ binds both to one fresh level. Continues with +-- 'alphaEquivEnv' on the bodies. +-- +-- @since 0.4.0 +{-# INLINE bindPairs #-} +bindPairs + :: forall sig binder m l1 l2. (ZipMatchK sig, Foil.Distinct m, Foil.UnifiablePattern binder) + => Int -> IntMap Int -> IntMap Int -> [(Int, Int)] + -> Foil.Scope m + -> AST binder sig l1 -> AST binder sig l2 -> Bool +bindPairs = aeBindPairs alphaEquivLoops + +-- | The renaming-threading worker behind 'alphaEquiv': compare two terms +-- under partial renamings of their names into shared /levels/. +-- +-- Each environment maps a raw name to the level of the binder pair that bound +-- it on the comparison path, and a name outside its environment stands for +-- itself. A variable occurrence then compares as a level against a level, or +-- as a raw name against a raw name, and the two can never be conflated. This +-- is what makes threading sound where applying a raw renaming at the variables +-- would not be, since a renamed name could collide with one that passes +-- through unchanged and happens to share the target spelling. Levels are also +-- why no capture check is needed: a level is never a name, so there is nothing +-- for a binder to capture. +-- +-- A binder pair whose names coincide /deletes/ those names from both +-- environments, the pair shadowing both sides identically. When the +-- environments empty out the comparison drops back to the stateless +-- 'alphaEquiv', so only the region of the terms below a mismatched binder, +-- and above the point where the mismatch is shadowed away, pays for the +-- threading at all. +-- +-- The indices of the two terms are deliberately independent, in the style +-- of 'unsafeEqAST': the terms are never renamed into a common scope, so +-- no common index exists to give them. +-- +-- @since 0.4.0 +{-# INLINE alphaEquivEnv #-} +alphaEquivEnv + :: forall sig binder n n1 n2. (ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder) + => Int -- ^ Next fresh level. + -> IntMap Int -- ^ Left renaming: raw name to the level that bound it. + -> IntMap Int -- ^ Right renaming. + -> Foil.Scope n -- ^ Scope along the unified path (consulted by 'Control.Monad.Foil.unifyPatternsIn'). + -> AST binder sig n1 + -> AST binder sig n2 + -> Bool +alphaEquivEnv = aeAlphaEquivEnv alphaEquivLoops + +-- | The scoped half of 'alphaEquivEnv': get the verdict from +-- 'Control.Monad.Foil.unifyPatternsIn', extend the environments as it prescribes, and +-- recurse into the bodies as they stand. +-- +-- @since 0.4.0 +{-# INLINE alphaEquivScopedEnv #-} +alphaEquivScopedEnv + :: forall sig binder n n1 n2. (ZipMatchK sig, Foil.Distinct n, Foil.UnifiablePattern binder) + => Int + -> IntMap Int + -> IntMap Int + -> Foil.Scope n + -> ScopedAST binder sig n1 + -> ScopedAST binder sig n2 + -> Bool +alphaEquivScopedEnv = aeAlphaEquivScopedEnv alphaEquivLoops + +-- | The mutually recursive loops behind α-equivalence, one field per +-- function above. +-- +-- @since 0.6.1 +data AlphaEquivLoops binder sig = AlphaEquivLoops + { aeAlphaEquiv :: forall n. Foil.Distinct n => Foil.Scope n -> AST binder sig n -> AST binder sig n -> Bool + , aeAlphaEquivScoped :: forall n. Foil.Distinct n => Foil.Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool + , aeBindPairs :: forall m l1 l2. Foil.Distinct m => Int -> IntMap Int -> IntMap Int -> [(Int, Int)] -> Foil.Scope m -> AST binder sig l1 -> AST binder sig l2 -> Bool + , aeAlphaEquivEnv :: forall n n1 n2. Foil.Distinct n => Int -> IntMap Int -> IntMap Int -> Foil.Scope n -> AST binder sig n1 -> AST binder sig n2 -> Bool + , aeAlphaEquivScopedEnv :: forall n n1 n2. Foil.Distinct n => Int -> IntMap Int -> IntMap Int -> Foil.Scope n -> ScopedAST binder sig n1 -> ScopedAST binder sig n2 -> Bool + } + +-- | The loops behind α-equivalence. They are local and take the instances +-- from this function, so once it is inlined at a known signature, they use +-- that signature's instances directly. A recursive function with class +-- constraints would instead be split by GHC into a wrapper and a worker +-- (some of its dictionaries, such as t'Control.Monad.Foil.Distinct', are never used at +-- runtime), and a client's @SPECIALIZE@ pragma would reach only the wrapper. +-- +-- @since 0.6.1 +{-# INLINE alphaEquivLoops #-} +alphaEquivLoops + :: forall sig binder. (ZipMatchK sig, Foil.UnifiablePattern binder) + => AlphaEquivLoops binder sig +alphaEquivLoops = AlphaEquivLoops goAlpha goScoped goPairs goEnv goScopedEnv + where + goAlpha + :: Foil.Distinct n + => Foil.Scope n + -> AST binder sig n + -> AST binder sig n + -> Bool + goAlpha _scope (Var x) (Var y) = x == y + goAlpha scope (Node l) (Node r) = + case zipMatchWith2 (unit . goScoped scope) (unit . goAlpha scope) l r of + Nothing -> False + Just _ -> True + where + unit f x = if f x then Just () else Nothing + goAlpha _ _ _ = False + + goScoped + :: forall n. Foil.Distinct n + => Foil.Scope n + -> ScopedAST binder sig n + -> ScopedAST binder sig n + -> Bool + goScoped scope + (ScopedAST binder1 body1) + (ScopedAST binder2 body2) = + case Foil.unifyPatternsIn scope binder1 binder2 of + -- the binders coincide: compare the bodies as they stand + Foil.SameNameBinders{} -> -- after seeing this we know that body scopes are the same + case Foil.assertDistinct binder1 of + Foil.Distinct -> + let scope1 = Foil.extendScopePattern binder1 scope + in goAlpha scope1 body1 body2 + -- the left binder is renamed towards the right one + Foil.RenameLeftNameBinder _ rename1to2 -> + case Foil.assertDistinct binder2 of + Foil.Distinct -> + let scope2 = Foil.extendScopePattern binder2 scope + pairs = [ (Foil.nameId x, renamedId rename1to2 x) + | x <- Foil.namesOfPattern binder1 ] + in enterEnv pairs scope2 body1 body2 + -- the right binder is renamed towards the left one + Foil.RenameRightNameBinder _ rename2to1 -> + case Foil.assertDistinct binder1 of + Foil.Distinct -> + let scope1 = Foil.extendScopePattern binder1 scope + pairs = [ (renamedId rename2to1 y, Foil.nameId y) + | y <- Foil.namesOfPattern binder2 ] + in enterEnv pairs scope1 body1 body2 + -- both are renamed towards a unified pattern: pair the two sides' + -- names through the unified name each maps to + Foil.RenameBothBinders binder' rename1 rename2 -> + case Foil.assertDistinct binder' of + Foil.Distinct -> + let scope' = Foil.extendScopePattern binder' scope + leftU = IntMap.fromList + [ (renamedId rename1 x, Foil.nameId x) + | x <- Foil.namesOfPattern binder1 ] + rightU = IntMap.fromList + [ (renamedId rename2 y, Foil.nameId y) + | y <- Foil.namesOfPattern binder2 ] + pairs = IntMap.elems (IntMap.intersectionWith (,) leftU rightU) + in enterEnv pairs scope' body1 body2 + -- if we cannot unify patterns then scopes are not alpha-equivalent + Foil.NotUnifiable -> False + where + enterEnv + :: forall m l1 l2. Foil.Distinct m + => [(Int, Int)] -> Foil.Scope m + -> AST binder sig l1 -> AST binder sig l2 -> Bool + enterEnv pairs scope' = goPairs 0 IntMap.empty IntMap.empty pairs scope' + + goPairs + :: forall m l1 l2. Foil.Distinct m + => Int -> IntMap Int -> IntMap Int -> [(Int, Int)] + -> Foil.Scope m + -> AST binder sig l1 -> AST binder sig l2 -> Bool + goPairs lvl envL envR pairs scope body1 body2 = case pairs of + [] -> goEnv lvl envL envR scope body1 body2 + ((x, y) : rest) + | x == y -> goPairs lvl (IntMap.delete x envL) (IntMap.delete y envR) rest scope body1 body2 + | otherwise -> goPairs (lvl + 1) (IntMap.insert x lvl envL) (IntMap.insert y lvl envR) rest scope body1 body2 + + goEnv + :: forall n n1 n2. Foil.Distinct n + => Int -- ^ Next fresh level. + -> IntMap Int -- ^ Left renaming: raw name to the level that bound it. + -> IntMap Int -- ^ Right renaming. + -> Foil.Scope n -- ^ Scope along the unified path (consulted by 'Control.Monad.Foil.unifyPatternsIn'). + -> AST binder sig n1 + -> AST binder sig n2 + -> Bool + goEnv lvl envL envR scope t1 t2 + | IntMap.null envL && IntMap.null envR = + -- The renamings have emptied out (or never held anything): the + -- terms coincide raw-for-raw from here on, so compare them where + -- they stand. The coercion brings both indices to the scope's, + -- which is the unified path the comparison speaks of. + goAlpha scope (unsafeCoerce t1 :: AST binder sig n) (unsafeCoerce t2 :: AST binder sig n) + | otherwise = case (t1, t2) of + (Var x, Var y) -> + case (IntMap.lookup (Foil.nameId x) envL, IntMap.lookup (Foil.nameId y) envR) of + (Just k1, Just k2) -> k1 == k2 + (Nothing, Nothing) -> Foil.nameId x == Foil.nameId y + _ -> False + (Node l, Node r) -> + case zipMatchWith2 + (unit . goScopedEnv lvl envL envR scope) + (unit . goEnv lvl envL envR scope) l r of + Nothing -> False + Just _ -> True + _ -> False + where + unit f x = if f x then Just () else Nothing + + goScopedEnv + :: forall n n1 n2. Foil.Distinct n + => Int + -> IntMap Int + -> IntMap Int + -> Foil.Scope n + -> ScopedAST binder sig n1 + -> ScopedAST binder sig n2 + -> Bool + goScopedEnv lvl envL envR scope scoped1 scoped2 = + -- The scoped terms are compared where they stand; the coercion only + -- brings their indices to the scope's, which is the unified path the + -- environments and the verdicts speak of. + case (unsafeCoerce scoped1 :: ScopedAST binder sig n, unsafeCoerce scoped2 :: ScopedAST binder sig n) of + (ScopedAST binder1 body1, ScopedAST binder2 body2) -> + case Foil.unifyPatternsIn scope binder1 binder2 of + -- the binders coincide: the pair shadows both sides identically + Foil.SameNameBinders{} -> + case Foil.assertDistinct binder1 of + Foil.Distinct -> + let scope' = Foil.extendScopePattern binder1 scope + names = map Foil.nameId (Foil.namesOfPattern binder1) + envL' = deleteAll names envL + envR' = deleteAll names envR + in goEnv lvl envL' envR' scope' body1 body2 + -- the left binder is renamed towards the right one + Foil.RenameLeftNameBinder _ rename1to2 -> + case Foil.assertDistinct binder2 of + Foil.Distinct -> + let scope' = Foil.extendScopePattern binder2 scope + pairs = [ (Foil.nameId x, renamedId rename1to2 x) + | x <- Foil.namesOfPattern binder1 ] + in goPairs lvl envL envR pairs scope' body1 body2 + -- the right binder is renamed towards the left one + Foil.RenameRightNameBinder _ rename2to1 -> + case Foil.assertDistinct binder1 of + Foil.Distinct -> + let scope' = Foil.extendScopePattern binder1 scope + pairs = [ (renamedId rename2to1 y, Foil.nameId y) + | y <- Foil.namesOfPattern binder2 ] + in goPairs lvl envL envR pairs scope' body1 body2 + -- both are renamed towards a unified pattern: pair the two sides' + -- names through the unified name each maps to + Foil.RenameBothBinders binder' rename1 rename2 -> + case Foil.assertDistinct binder' of + Foil.Distinct -> + let scope' = Foil.extendScopePattern binder' scope + leftU = IntMap.fromList + [ (renamedId rename1 x, Foil.nameId x) + | x <- Foil.namesOfPattern binder1 ] + rightU = IntMap.fromList + [ (renamedId rename2 y, Foil.nameId y) + | y <- Foil.namesOfPattern binder2 ] + pairs = IntMap.elems (IntMap.intersectionWith (,) leftU rightU) + in goPairs lvl envL envR pairs scope' body1 body2 + Foil.NotUnifiable -> False + where + deleteAll names env = case names of + [] -> env + (i : is) -> deleteAll is (IntMap.delete i env) + +-- ** Unsafe equality checks + +-- | /Unsafe/ equality check for two terms. Names are compared by their raw +-- identifiers, and patterns by 'Control.Monad.Foil.Internal.unsafeEqPattern', which uses the +-- binder-only 'Control.Monad.Foil.unifyPatterns'. Thus α-equivalent terms whose binders +-- differ compare unequal, so normalize both sides with 'refreshAST' first. +-- +-- @since 0.0.3 +{-# INLINE unsafeEqAST #-} +unsafeEqAST + :: (ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l) + => AST binder sig n + -> AST binder sig l + -> Bool +unsafeEqAST = eqAST unsafeEqLoops + +-- | A version of 'unsafeEqAST' for scoped terms. +-- +-- @since 0.0.3 +{-# INLINE unsafeEqScopedAST #-} +unsafeEqScopedAST + :: (ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n, Foil.Distinct l) + => ScopedAST binder sig n + -> ScopedAST binder sig l + -> Bool +unsafeEqScopedAST = eqScopedAST unsafeEqLoops + +-- | The two mutually recursive loops behind 'unsafeEqAST' and +-- 'unsafeEqScopedAST'. +-- +-- @since 0.6.1 +data EqLoops binder sig = EqLoops + { eqAST :: forall n l. (Foil.Distinct n, Foil.Distinct l) => AST binder sig n -> AST binder sig l -> Bool + , eqScopedAST :: forall n l. (Foil.Distinct n, Foil.Distinct l) => ScopedAST binder sig n -> ScopedAST binder sig l -> Bool + } + +-- | The loops behind 'unsafeEqAST' and 'unsafeEqScopedAST', local for the +-- same reason as those of 'alphaEquivLoops'. +-- +-- @since 0.6.1 +{-# INLINE unsafeEqLoops #-} +unsafeEqLoops + :: forall sig binder. (ZipMatchK sig, Foil.UnifiablePattern binder) + => EqLoops binder sig +unsafeEqLoops = EqLoops goAST goScoped + where + goAST :: forall n l. (Foil.Distinct n, Foil.Distinct l) => AST binder sig n -> AST binder sig l -> Bool + goAST (Var x) (Var y) = Foil.nameId x == Foil.nameId y + goAST (Node t1) (Node t2) = + case zipMatchWith2 (unit . goScoped) (unit . goAST) t1 t2 of + Nothing -> False + Just _ -> True + goAST _ _ = False + + goScoped :: forall n l. (Foil.Distinct n, Foil.Distinct l) => ScopedAST binder sig n -> ScopedAST binder sig l -> Bool + goScoped (ScopedAST binder1 body1) (ScopedAST binder2 body2) = and + [ Foil.unsafeEqPattern binder1 binder2 + , case (Foil.assertDistinct binder1, Foil.assertDistinct binder2) of + (Foil.Distinct, Foil.Distinct) -> body1 `goAST` body2 + ] + + unit f x = if f x then Just () else Nothing + +-- | /Unsafe/ equality check for two terms in one scope. Names are compared +-- directly, and patterns by 'Control.Monad.Foil.unifyPatternsIn', which must +-- find their binders the same. Thus α-equivalent terms whose binders differ +-- compare unequal, so normalize both sides with 'refreshAST' first, as +-- 'alphaEquivRefreshed' does. +-- +-- Unlike 'unsafeEqAST', this compares the payloads of patterns, which +-- 'Control.Monad.Foil.unifyPatternsIn' needs the scope for. +-- +-- @since 0.6.1 +{-# INLINE unsafeEqASTIn #-} +unsafeEqASTIn + :: (ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n) + => Foil.Scope n + -> AST binder sig n + -> AST binder sig n + -> Bool +unsafeEqASTIn = eqASTIn unsafeEqInLoops + +-- | A version of 'unsafeEqASTIn' for scoped terms. +-- +-- @since 0.6.1 +{-# INLINE unsafeEqScopedASTIn #-} +unsafeEqScopedASTIn + :: (ZipMatchK sig, Foil.UnifiablePattern binder, Foil.Distinct n) + => Foil.Scope n + -> ScopedAST binder sig n + -> ScopedAST binder sig n + -> Bool +unsafeEqScopedASTIn = eqScopedASTIn unsafeEqInLoops + +-- | The two mutually recursive loops behind 'unsafeEqASTIn' and +-- 'unsafeEqScopedASTIn'. +-- +-- @since 0.6.1 +data EqInLoops binder sig = EqInLoops + { eqASTIn :: forall n. Foil.Distinct n => Foil.Scope n -> AST binder sig n -> AST binder sig n -> Bool + , eqScopedASTIn :: forall n. Foil.Distinct n => Foil.Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool + } + +-- | The loops behind 'unsafeEqASTIn' and 'unsafeEqScopedASTIn', local for +-- the same reason as those of 'alphaEquivLoops'. +-- +-- @since 0.6.1 +{-# INLINE unsafeEqInLoops #-} +unsafeEqInLoops + :: forall sig binder. (ZipMatchK sig, Foil.UnifiablePattern binder) + => EqInLoops binder sig +unsafeEqInLoops = EqInLoops goAST goScoped + where + goAST :: forall n. Foil.Distinct n => Foil.Scope n -> AST binder sig n -> AST binder sig n -> Bool + goAST _ (Var x) (Var y) = x == y + goAST scope (Node t1) (Node t2) = + case zipMatchWith2 (unit . goScoped scope) (unit . goAST scope) t1 t2 of + Nothing -> False + Just _ -> True + goAST _ _ _ = False + + goScoped :: forall n. Foil.Distinct n => Foil.Scope n -> ScopedAST binder sig n -> ScopedAST binder sig n -> Bool + goScoped scope (ScopedAST binder1 body1) (ScopedAST binder2 body2) = + case Foil.unifyPatternsIn scope binder1 binder2 of + Foil.SameNameBinders{} -> case Foil.assertDistinct binder1 of + Foil.Distinct -> goAST (Foil.extendScopePattern binder1 scope) body1 body2 + _ -> False + + unit f x = if f x then Just () else Nothing + +-- * Converting to and from free foil + +-- ** Convert to free foil + +-- | An identifier a raw term mentions that the names given for conversion do +-- not account for. +-- +-- Note what this does and does not carry. It cannot carry a position: the +-- conversion functions are generic in the raw term and only ever see it through +-- @toSig@, so a source location, if the syntax has one, is not theirs to read. +-- What they do know, and a caller checking names beforehand does not, is which +-- names were in scope /at the occurrence/, the binders passed on the way down +-- included. That is what a \"did you mean\" needs. +-- +-- @since 0.4.0 +data UnresolvedName rawIdent = UnresolvedName + { unresolvedIdent :: rawIdent + -- ^ The identifier that did not resolve. + , unresolvedInScope :: [rawIdent] + -- ^ What was in scope where it occurred. + } deriving (Eq, Show, Functor, Foldable, Traversable) + +-- | The identifiers a raw term mentions that a set of names cannot resolve, in +-- the order they occur. +-- +-- This is 'unsafeConvertToAST' with the conversion left out, so it descends +-- under binders in the same way and accounts for what they bind. A caller +-- that converts with 'tryConvertToASTWith' should use 'unresolvedNamesWith' +-- instead, so that its constants do not count as unresolved. +-- +-- @since 0.4.0 +unresolvedNames + :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n. + (Foil.Distinct n, Bifoldable sig, Ord rawIdent, Foil.CoSinkable binder) + => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) + -- ^ 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@. + -> rawTerm + -- ^ Raw term. + -> [UnresolvedName rawIdent] +unresolvedNames toSig fromRawPattern getScopedTerm scope names = + unresolvedNamesWith toSig fromRawPattern getScopedTerm scope names Map.empty + +-- | The identifiers a raw term mentions that neither a set of names nor a +-- table of constants can resolve, in the order they occur. This is +-- 'unresolvedNames' for the arguments of 'tryConvertToASTWith': given the same +-- names and constants, it reports every identifier that +-- 'tryConvertToASTWith' would fail on, and the first of them is the one that +-- 'tryConvertToASTWith' reports. +-- +-- @since 0.6.1 +unresolvedNamesWith + :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n. + (Foil.Distinct n, Bifoldable sig, Ord rawIdent, Foil.CoSinkable binder) + => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) + -- ^ 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@. + -> Map rawIdent (AST binder sig n) + -- ^ Identifiers that denote a term rather than a variable. + -> rawTerm + -- ^ Raw term. + -> [UnresolvedName rawIdent] +unresolvedNamesWith toSig fromRawPattern getScopedTerm scope0 names0 terms = + go scope0 names0 + where + constants = Map.keys terms + + go :: forall x. Foil.Distinct x + => Foil.Scope x -> Map rawIdent (Foil.Name x) -> rawTerm -> [UnresolvedName rawIdent] + go scope names t = case toSig t of + Left x + | Map.member x names || Map.member x terms -> [] + | otherwise -> [UnresolvedName x (Map.keys names <> constants)] + Right node -> bifoldMap (goScoped scope names) (go scope names) node + + goScoped :: forall x. Foil.Distinct x + => Foil.Scope x -> Map rawIdent (Foil.Name x) + -> (rawPattern, rawScopedTerm) -> [UnresolvedName rawIdent] + goScoped scope names (pat, scopedTerm) = + fromRawPattern scope names pat $ \binder' names' -> + go (Foil.extendScopePattern binder' scope) names' (getScopedTerm scopedTerm) + +-- | Convert a raw term into a scope-safe term, reporting the first identifier +-- that does not resolve. +-- +-- One pass, short-circuiting at the first failure, so a term that resolves +-- costs no more than 'unsafeConvertToAST' does. The report is complete for +-- that one identifier, since 'unresolvedInScope' is built where the conversion +-- fails and is never computed on the way through. +-- +-- A caller wanting /every/ unresolved identifier rather than the first pays a +-- second pass for it, with 'unresolvedNames'. The successful path stays fast +-- that way, and a failure can afford to be walked again for a better message. +-- +-- @since 0.4.0 +tryConvertToAST + :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n. + (Foil.Distinct n, Bitraversable sig, Ord rawIdent, + Foil.CoSinkable binder, Foil.SinkableK binder) + => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) + -- ^ 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@. + -> rawTerm + -- ^ Raw term. + -> Either (UnresolvedName rawIdent) (AST binder sig n) +tryConvertToAST toSig fromRawPattern getScopedTerm scope names = + tryConvertToASTWith toSig fromRawPattern getScopedTerm scope names Map.empty + +-- | Convert a raw term into a scope-safe term, resolving some identifiers to +-- whole terms rather than to variables. +-- +-- The extra table is what a language with /constants/ needs: an identifier that +-- denotes a top-level declaration, a primitive, or an abbreviation stands for +-- something that is not a variable, and resolving it during conversion is the +-- only place where the binders are known. Doing it in a pass of one's own means +-- writing a binder-aware traversal of the raw syntax by hand. +-- +-- Variables win: the table of names is consulted first, so a binder shadows an +-- entry here, and an entry here shadows nothing. The table is sunk when going +-- under a binder, exactly as the names are, so its entries may mention anything +-- in scope where conversion started and need not be closed. +-- +-- @since 0.4.0 +tryConvertToASTWith + :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n. + (Foil.Distinct n, Bitraversable sig, Ord rawIdent, + Foil.CoSinkable binder, Foil.SinkableK binder) + => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) + -- ^ 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@. + -> Map rawIdent (AST binder sig n) + -- ^ Identifiers that denote a term rather than a variable. + -> rawTerm + -- ^ Raw term. + -> Either (UnresolvedName rawIdent) (AST binder sig n) +tryConvertToASTWith toSig fromRawPattern getScopedTerm = go + where + go :: forall x. Foil.Distinct x + => Foil.Scope x -> Map rawIdent (Foil.Name x) + -> Map rawIdent (AST binder sig x) -> rawTerm + -> Either (UnresolvedName rawIdent) (AST binder sig x) + go scope names terms t = case toSig t of + Left x -> case Map.lookup x names of + Just name -> Right (Var name) + Nothing -> case Map.lookup x terms of + Just term -> Right term + Nothing -> Left (UnresolvedName x (Map.keys names <> Map.keys terms)) + Right node -> + Node <$> bitraverse (goScoped scope names terms) (go scope names terms) node + + goScoped :: forall x. Foil.Distinct x + => Foil.Scope x -> Map rawIdent (Foil.Name x) + -> Map rawIdent (AST binder sig x) + -> (rawPattern, rawScopedTerm) + -> Either (UnresolvedName rawIdent) (ScopedAST binder sig x) + goScoped scope names terms (pat, scopedTerm) = + fromRawPattern scope names pat $ \binder' names' -> + ScopedAST binder' + <$> go (Foil.extendScopePattern binder' scope) names' + (Foil.sink1 terms) (getScopedTerm scopedTerm) + +-- | Convert a raw term into a scope-safe term, calling 'error' on an +-- identifier that does not resolve. +-- +-- Prefer 'tryConvertToAST', which reports such identifiers. This is for callers +-- that have already established that every name resolves. +-- +-- @since 0.4.0 +unsafeConvertToAST + :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder) + => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) + -- ^ 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@. + -> rawTerm + -- ^ Raw term. + -> AST binder sig n +unsafeConvertToAST toSig fromRawPattern getScopedTerm scope names t = + case toSig t of + Left x -> + case Map.lookup x names of + Nothing -> error "undefined variable" + Just name -> Var name + Right node -> Node $ + bimap + (unsafeConvertToScopedAST toSig fromRawPattern getScopedTerm scope names) + (unsafeConvertToAST toSig fromRawPattern getScopedTerm scope names) + node + +-- | Same as 'unsafeConvertToAST' but for scoped terms. +-- +-- @since 0.4.0 +unsafeConvertToScopedAST + :: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder) + => (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm)) + -- ^ 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) + -- ^ A pair of a pattern and a corresponding scoped term. + -> ScopedAST binder sig n +unsafeConvertToScopedAST toSig fromRawPattern getScopedTerm scope names (pat, scopedTerm) = + fromRawPattern scope names pat $ \binder' names' -> + let scope' = Foil.extendScopePattern binder' scope + in ScopedAST binder' (unsafeConvertToAST toSig fromRawPattern getScopedTerm scope' names' (getScopedTerm scopedTerm)) + +-- ** Convert from free foil + +-- | Convert a scope-safe term back into a raw term. +-- Use 'convertFromASTWith' to name free variables separately from bound ones. +-- +-- @since 0.0.3 +convertFromAST + :: Bifunctor sig + => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm) + -- ^ Peel back one layer of syntax. + -> (rawIdent -> rawTerm) + -- ^ Convert identifier into a raw variable term. + -> (forall x y. binder x y -> rawPattern) + -- ^ Convert scope-safe pattern into a raw pattern. + -> (rawTerm -> rawScopedTerm) + -- ^ Wrap raw term into a scoped term. + -> (Int -> rawIdent) + -- ^ Name a variable, bound or free, from its underlying integer 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 $ + bimap + (convertFromScopedAST fromSig fromVar makePattern makeScoped f) + (convertFromAST fromSig fromVar makePattern makeScoped f) + node + +-- | Same as 'convertFromAST' but for scoped terms. +-- +-- @since 0.0.3 +convertFromScopedAST + :: Bifunctor sig + => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm) + -- ^ Peel back one layer of syntax. + -> (rawIdent -> rawTerm) + -- ^ Convert identifier into a raw variable term. + -> (forall x y. binder x y -> rawPattern) + -- ^ Convert scope-safe pattern into a raw pattern. + -> (rawTerm -> rawScopedTerm) + -- ^ Wrap raw term into a scoped term. + -> (Int -> rawIdent) + -- ^ Name a variable, bound or free, from its underlying integer identifier. + -> ScopedAST binder sig n + -- ^ Scope-safe scoped term. + -> (rawPattern, rawScopedTerm) +convertFromScopedAST fromSig fromVar makePattern makeScoped f = \case + ScopedAST binder body -> + ( makePattern binder + , makeScoped (convertFromAST fromSig fromVar makePattern makeScoped f body)) + +-- | Convert a scope-safe term back into a raw term, naming the variables that +-- occur /free in the whole term/ separately from the bound ones. +-- +-- 'convertFromAST' applies one naming function to every variable it meets, +-- bound or free, and gives it only a raw name. That is often not enough, since +-- raw names are not unique across scope indices: a binder inside a term may +-- share one with a name of the ambient scope, so naming by raw name alone can +-- print a bound variable as whatever the ambient scope calls that name. +-- +-- Keeping the typed name is what distinguishes them, and 'Control.Monad.Foil.unsinkNamePattern' +-- is the operation for it: composing one per binder on the way down builds a +-- @t'Control.Monad.Foil.Name' x -> 'Maybe' ( t'Control.Monad.Foil.Name' n )@ that answers exactly the question. +-- +-- @since 0.4.0 +convertFromASTWith + :: forall sig binder rawIdent rawTerm rawPattern rawScopedTerm n. + (Bifunctor sig, Foil.Distinct n, Foil.CoSinkable binder) + => (sig (rawPattern, rawScopedTerm) rawTerm -> rawTerm) + -- ^ Peel back one layer of syntax. + -> (rawIdent -> rawTerm) + -- ^ Convert identifier into a raw variable term. + -> (forall x y. binder x y -> rawPattern) + -- ^ Convert scope-safe pattern into a raw pattern. + -> (rawTerm -> rawScopedTerm) + -- ^ Wrap raw term into a scoped term. + -> (Foil.Name n -> rawIdent) + -- ^ Name a variable that is free in the whole term. + -> (Int -> rawIdent) + -- ^ Name a bound variable, from its underlying integer identifier. + -> AST binder sig n + -- ^ Scope-safe term. + -> rawTerm +convertFromASTWith fromSig fromVar makePattern makeScoped freeName boundName = + go Just + where + go :: forall x. Foil.Distinct x + => (Foil.Name x -> Maybe (Foil.Name n)) -> AST binder sig x -> rawTerm + go unsink = \case + Var x -> fromVar $ case unsink x of + Just name -> freeName name + Nothing -> boundName (Foil.nameId x) + Node node -> fromSig (bimap (goScoped unsink) (go unsink) node) + + goScoped :: forall x. Foil.Distinct x + => (Foil.Name x -> Maybe (Foil.Name n)) + -> ScopedAST binder sig x -> (rawPattern, rawScopedTerm) + goScoped unsink (ScopedAST binder body) = + case Foil.assertDistinct binder of + Foil.Distinct -> + ( makePattern binder + , makeScoped + (go (\name -> Foil.unsinkNamePattern binder name >>= unsink) body) ) + +-- ** Unsinking AST + +-- | The support of a term: exactly the names that occur free in it. +-- +-- This is the annotation that co-de-Bruijn syntax carries intrinsically and +-- that the foil does not need for weakening, since 'Control.Monad.Foil.sink' is a coercion. +-- Computing it traverses the whole term, so a client that restricts often +-- should cache it. +-- +-- @since 0.4.0 +supportOf + :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) + => AST binder sig n -> Foil.NameSet n +supportOf = \case + Var name -> Foil.nameSetSingleton name + Node node -> bifoldMap supportOfScopedAST supportOf node + +-- | The support of a scoped term, in the scope /outside/ its binder. +-- +-- @since 0.4.0 +supportOfScopedAST + :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) + => ScopedAST binder sig n -> Foil.NameSet n +supportOfScopedAST (ScopedAST binder body) = + case Foil.assertDistinct binder of + Foil.Distinct -> Foil.unsinkNameSet binder (supportOf body) + +-- | Cut a term down to the scope of exactly the names it uses. +-- +-- The term's support is computed with 'supportOf', as in 'unsinkAST', but +-- nothing is tested and nothing can fail, since the term inhabits the +-- restricted scope by construction. @t'Control.Monad.Foil.Ext' m n@ comes back with it, so +-- the term can be 'Control.Monad.Foil.sink'ed to where it came from for free. +-- +-- Verifying a declared dependency, such as a @uses@ clause or a module's +-- parameters, is this plus a comparison: compute the scope a term really +-- inhabits, and check the declared one against it. +-- +-- @since 0.4.0 +withRelevantScope + :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) + => AST binder sig n + -> (forall m. (Foil.Ext m n, Foil.Distinct m) + => Foil.Scope m -> AST binder sig m -> r) + -> r +withRelevantScope term cont = + Foil.withRestrictedScope (supportOf term) $ \scope -> + cont scope (unsafeCoerce term) + +-- | Restrict a term from scope @l@ to a smaller scope @n@, if every name that +-- occurs free in it is in @n@. +-- +-- The scope @l@ must extend @n@, since names are compared by their raw +-- identifiers, which identify a name only within one chain of scope +-- extensions. On success the term is returned unchanged, since restricting a +-- term that does inhabit @n@ is a coercion. +-- +-- @since 0.3.0 +unsinkAST + :: (Foil.DExt n l, Foil.CoSinkable binder, Bifoldable sig) + => Foil.Scope n -> AST binder sig l -> Maybe (AST binder sig n) +unsinkAST scope term + | Foil.nameSetSubsetOfScope (supportOf term) scope = Just (unsafeCoerce term) + | otherwise = Nothing + +-- | Get the free variables of an AST. +-- +-- These come from 'supportOf', so they are distinct and in ascending order of +-- their identifiers. +-- +-- @since 0.3.0 +freeVarsOf + :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) + => AST binder sig n -> [Foil.Name n] +freeVarsOf = Foil.nameSetToList . supportOf + +-- | Get the free variables of a scoped AST, in the scope outside its binder. +-- +-- @since 0.3.0 +freeVarsOfScopedAST + :: (Foil.Distinct n, Foil.CoSinkable binder, Bifoldable sig) + => ScopedAST binder sig n -> [Foil.Name n] +freeVarsOfScopedAST = Foil.nameSetToList . supportOfScopedAST 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 @@ -81,21 +81,21 @@ data FreeFoilTermConfig = FreeFoilTermConfig { rawIdentName :: Name -- ^ The type name for the identifiers. - -- When identifiers occur in a term, they are converted to 'Foil.Name' (with an appropriate type-level scope parameter). - -- When identifiers occur in a pattern, they are converted to 'Foil.NameBinder' (with appropriate type-level scope parameters). + -- When identifiers occur in a term, they are converted to t'Control.Monad.Foil.Name' (with an appropriate type-level scope parameter). + -- When identifiers occur in a pattern, they are converted to t'Control.Monad.Foil.NameBinder' (with appropriate type-level scope parameters). , rawTermName :: Name -- ^ The type name for the term. - -- This will be the main recursive type to be converted into an 'Foil.AST'. + -- This will be the main recursive type to be converted into an t'Control.Monad.Free.Foil.AST'. , rawBindingName :: Name -- ^ The type name for the binders (patterns). - -- This will be the main binder type to used in 'Foil.AST'-representation of the terms. + -- This will be the main binder type to used in t'Control.Monad.Free.Foil.AST'-representation of the terms. , rawScopeName :: Name -- ^ The type name for the scoped term. - -- This will be replaced with either 'Foil.ScopedAST' (with outer scope) or 'Foil.AST' (with inner scope) + -- This will be replaced with either t'Control.Monad.Free.Foil.ScopedAST' (with outer scope) or t'Control.Monad.Free.Foil.AST' (with inner scope) -- depending on its occurrence in a regular (sub)term or some quantified syntax. , rawVarConName :: Name -- ^ The constructor name for the variables in a term. - -- This constructor will be replaced with the standard 'Foil.Var'. + -- This constructor will be replaced with the standard 'Control.Monad.Free.Foil.Var'. -- It is expected to have exactly one field of type 'rawIdentName'. , rawSubTermNames :: [Name] -- ^ Type names for subterm syntax. @@ -136,7 +136,7 @@ toFreeFoilNameTo FreeFoilConfig{..} name = mkName (freeFoilConvertToName (nameBase name)) -- | The name of the range-parametric sibling of a generated definition --- (see 'Foil.withFreshIn'): @toPatternIn@ beside @toPattern@. +-- (see 'Control.Monad.Foil.withFreshIn'): @toPatternIn@ beside @toPattern@. toNameIn :: Name -> Name toNameIn name = mkName (nameBase name ++ "In") @@ -378,7 +378,7 @@ -- -- It is when there is exactly one constructor, declared without an explicit -- @forall@ or context, and that constructor has exactly one field, which binds: --- an identifier (it becomes a 'Foil.NameBinder') or a nested binding type. A +-- an identifier (it becomes a t'Control.Monad.Foil.NameBinder') or a nested binding type. A -- field that binds gives the constructor the result type @T ... o i@ with -- distinct scope variables, as a newtype requires; a field that binds nothing -- gives @T ... o o@, which only a GADT can express. @@ -399,7 +399,7 @@ -- | 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. +-- lives inside the t'Control.Monad.Free.Foil.ScopedAST' of each scoped child. isBindingField :: FreeFoilConfig -> Type -> Bool isBindingField FreeFoilConfig{..} = \case PeelConT typeName _ | Just _ <- lookupBindingName typeName freeFoilTermConfigs -> True @@ -407,7 +407,7 @@ -- | Is this raw field a scoped-term field? -- --- Such a field becomes a 'Foil.ScopedAST', which carries a binder of its own. +-- Such a field becomes a t'Control.Monad.Free.Foil.ScopedAST', which carries a binder of its own. isScopeField :: FreeFoilConfig -> Type -> Bool isScopeField FreeFoilConfig{..} = \case PeelConT typeName _ | Just _ <- lookupScopeName typeName freeFoilTermConfigs -> True @@ -415,7 +415,7 @@ -- | What a raw binding constructor's field becomes in the scope-safe binding -- type. Mirrors the classification in 'toFreeFoilBindingCon': an identifier --- becomes a 'Foil.NameBinder' and threads the scope; a binding type becomes a +-- becomes a t'Control.Monad.Foil.NameBinder' and threads the scope; a binding type becomes a -- nested binding type and threads the scope; anything else is a payload that -- binds nothing. data BindingFieldSort = FieldBinder | FieldPattern | FieldPayload @@ -437,8 +437,8 @@ -- | Does this raw payload type mention anything that converts to a -- scope-indexed type in the binding type (a term, a scoped term, an -- identifier, or a nested binding under a type constructor)? Such a payload --- cannot be rebuilt by the generated 'Foil.CoSinkable' instance, rebuilding it --- at another scope being what 'Foil.transportPayload' exists for. Generation +-- cannot be rebuilt by the generated t'Control.Monad.Foil.CoSinkable' instance, rebuilding it +-- at another scope being what 'Control.Monad.Foil.transportPayload' exists for. Generation -- refuses such a payload, matching the GenericK-side refusal for derived -- patterns. mentionsScopeIndexed :: FreeFoilConfig -> Type -> Bool @@ -473,7 +473,7 @@ RecGadtC names types _retType -> [ (name, map (\(_, _, t) -> t) types) | name <- names ] ForallC _ _ con -> go con --- | One 'Foil.coSinkabilityProof' clause for a generated binding constructor: +-- | One 'Control.Monad.Foil.coSinkabilityProof' clause for a generated binding constructor: -- -- > coSinkabilityProof rename (Con x1 x2 x3) cont = -- > coSinkabilityProof rename x1 $ \rename' x1' -> @@ -481,7 +481,7 @@ -- > cont rename'' (Con x1' x2' x3) -- -- Binder and nested-pattern fields thread the renaming left to right (each via --- its own 'Foil.CoSinkable' instance); payload fields pass through untouched. +-- its own t'Control.Monad.Foil.CoSinkable' instance); payload fields pass through untouched. mkCoSinkabilityProofClause :: FreeFoilConfig -> (Name, [Type]) -> Q Clause mkCoSinkabilityProofClause config (rawConName, rawFieldTypes) = do let conName = toConName config rawConName @@ -508,7 +508,7 @@ body <- go rename (zip sorts xs) id return (Clause [VarP rename, ConP conName [] (map VarP xs), VarP cont] (NormalB body) []) --- | One 'Foil.withPattern' clause for a generated binding constructor: +-- | One 'Control.Monad.Foil.withPattern' clause for a generated binding constructor: -- -- > withPattern withBinder unit_ comp_ scope (Con x1 x2 x3) cont = -- > withBinder scope x1 $ \f1 x1' -> @@ -516,9 +516,9 @@ -- > in withPattern withBinder unit_ comp_ scope' x2 $ \f2 x2' scope'' -> -- > cont (comp_ f1 f2) (Con x1' x2' x3) scope'' -- --- A 'Foil.NameBinder' field is processed with @withBinder@ directly and +-- A t'Control.Monad.Foil.NameBinder' field is processed with @withBinder@ directly and -- extends the ambient scope for the fields to its right; a nested binding --- field recurses through its own 'Foil.withPattern', which hands the extended +-- field recurses through its own 'Control.Monad.Foil.withPattern', which hands the extended -- scope to its continuation. Results compose left to right with @comp_@; the -- final continuation receives the scope after the whole constructor, and a -- constructor that binds nothing hands @unit_@ and the ambient scope over. @@ -574,13 +574,13 @@ [VarP withBinder, VarP unit_, VarP comp_, VarP scope, ConP conName [] (map VarP xs), VarP cont] (NormalB body) []) --- | One 'Foil.nameBinderListOf' clause for a generated binding constructor: +-- | One 'Control.Monad.Foil.nameBinderListOf' clause for a generated binding constructor: -- -- > nameBinderListOf (Con x1 x2 _) = -- > concatNameBinderLists (nameBinderListOf x1) (nameBinderListOf x2) -- -- The binder and nested-pattern fields are listed left to right, in the order --- in which the 'Foil.withPattern' clause of 'mkWithPatternClause' visits them, +-- in which the 'Control.Monad.Foil.withPattern' clause of 'mkWithPatternClause' visits them, -- and payload fields are skipped. A constructor that binds nothing lists no -- binders. mkNameBinderListOfClause :: FreeFoilConfig -> (Name, [Type]) -> Q Clause @@ -592,7 +592,7 @@ | isBindingFieldSort sort = VarP x | otherwise = WildP -- A binder is consed on directly. Only a nested binding type's list is - -- concatenated, since 'Foil.concatNameBinderLists' is recursive and + -- concatenated, since 'Control.Monad.Foil.concatNameBinderLists' is recursive and -- copies its first argument. list = \case [] -> ConE 'Foil.NameBinderListEmpty @@ -829,7 +829,7 @@ -- /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; +-- in the free foil lives inside the t'Control.Monad.Free.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. -- @@ -1067,14 +1067,14 @@ (BindingNewtype, [newCon]) -> NewtypeD [] bindingName newParams Nothing newCon [] _ -> DataD [] bindingName newParams Nothing newCons [] - -- A concrete 'Foil.CoSinkable' instance for the generated binding type, + -- A concrete t'Control.Monad.Foil.CoSinkable' instance for the generated binding type, -- one clause per constructor, delegating to the fields' instances. The -- GenericK default routes every binder operation through a generic -- representation traversal, which costs a measurable constant per binder -- at runtime (see issue #82); the concrete instance removes it, and a -- client no longer declares (or hand-writes) the instance itself. The - -- instance lists its binders directly in 'Foil.nameBinderListOf', since - -- the default would go through the recursive 'Foil.withPattern'. + -- instance lists its binders directly in 'Control.Monad.Foil.nameBinderListOf', since + -- the default would go through the recursive 'Control.Monad.Foil.withPattern'. mkPatternCoSinkable FreeFoilTermConfig{..} = do (tvars, cons) <- reifyDataOrNewtype rawBindingName let bindingName = toFreeFoilName config rawBindingName diff --git a/src/Data/ZipMatchK.hs b/src/Data/ZipMatchK.hs --- a/src/Data/ZipMatchK.hs +++ b/src/Data/ZipMatchK.hs @@ -37,14 +37,14 @@ import Data.Coerce (coerce) import Data.Monoid (All (..), Any (..)) import Generics.Kind -import Data.Bitraversable import Data.ZipMatchK.Generic import Data.ZipMatchK.Mappings --- | Perform one level of equality testing for two values and pair up components using @(,)@: +-- | Perform one level of equality testing for two values and pair up +-- corresponding components using @(,)@, for every type parameter: -- --- > zipMatchK = zipMatchWithK (\x y -> Just (,) :^: M0) +-- > zipMatchK = zipMatchWithK pairMappings -- -- @since 0.2.0 zipMatchK :: forall f as bs. (ZipMatchK f, PairMappings as bs) => f :@@: as -> f :@@: bs -> Maybe (f :@@: ZipLoT as bs) @@ -68,29 +68,23 @@ -- | 'zipMatchWithK' specialised to functors. -- --- Note: 'Traversable' is a morally correct constraint here. --- -- @since 0.3.0 zipMatchWith1 - :: (Traversable f, ZipMatchK f) + :: ZipMatchK f => (a -> a' -> Maybe a'') -> f a -> f a' -> Maybe (f a'') zipMatchWith1 f = zipMatchWithK (f :^: M0) -- | 'zipMatchK' specialised to functors. -- --- Note: 'Traversable' is a morally correct constraint here. --- -- @since 0.3.0 -zipMatch1 :: (Traversable f, ZipMatchK f) => f a -> f a' -> Maybe (f (a, a')) +zipMatch1 :: ZipMatchK f => f a -> f a' -> Maybe (f (a, a')) zipMatch1 = zipMatchWith1 pairA -- | 'zipMatchWithK' specialised to bifunctors. -- --- Note: 'Bitraversable' is a morally correct constraint here. --- -- @since 0.3.0 zipMatchWith2 - :: (Bitraversable f, ZipMatchK f) + :: ZipMatchK f => (a -> a' -> Maybe a'') -> (b -> b' -> Maybe b'') -> f a b -> f a' b' -> Maybe (f a'' b'') @@ -98,10 +92,8 @@ -- | 'zipMatchK' specialised to bifunctors. -- --- Note: 'Bitraversable' is a morally correct constraint here. --- -- @since 0.3.0 -zipMatch2 :: (Bitraversable f, ZipMatchK f) => f a b -> f a' b' -> Maybe (f (a, a') (b, b')) +zipMatch2 :: ZipMatchK f => f a b -> f a' b' -> Maybe (f (a, a') (b, b')) zipMatch2 = zipMatchWith2 pairA pairA -- | 'zipMatchFoldK' specialised to functors. diff --git a/test/Control/Monad/Free/Foil/AlphaEquivSpec.hs b/test/Control/Monad/Free/Foil/AlphaEquivSpec.hs --- a/test/Control/Monad/Free/Foil/AlphaEquivSpec.hs +++ b/test/Control/Monad/Free/Foil/AlphaEquivSpec.hs @@ -1,10 +1,13 @@ {-# LANGUAGE DataKinds #-} {-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE FlexibleContexts #-} {-# LANGUAGE GADTs #-} +{-# LANGUAGE KindSignatures #-} {-# LANGUAGE LambdaCase #-} {-# LANGUAGE RankNTypes #-} {-# LANGUAGE ScopedTypeVariables #-} {-# LANGUAGE TemplateHaskell #-} +{-# LANGUAGE TypeFamilies #-} -- | Properties of 'alphaEquiv' with threaded renamings. -- @@ -28,6 +31,7 @@ unsafeAssertFresh) import Control.Monad.Free.Foil import Data.ZipMatchK.TH (deriveZipMatchK) +import Generics.Kind.TH (deriveGenericK) data LamSig scope term = App term term @@ -41,6 +45,48 @@ type Term = AST Foil.NameBinder LamSig +-- | A binder annotated with a name of the outer scope, as a binder may be +-- annotated with its type. Only 'Foil.unifyPatternsIn' compares the +-- annotations, as it does the payloads of a telescope. +data AnnBinder (n :: Foil.S) (l :: Foil.S) where + AnnBinder :: Foil.Name n -> Foil.NameBinder n l -> AnnBinder n l + +deriveGenericK ''AnnBinder +instance Foil.SinkableK AnnBinder + +-- | The annotation is a payload, so it is moved by hand (see +-- 'Foil.transportPayload'). +instance Foil.CoSinkable AnnBinder where + coSinkabilityProof rename (AnnBinder ann binder) cont = + Foil.coSinkabilityProof rename binder $ \rename' binder' -> + cont rename' (AnnBinder (rename ann) binder') + withPattern withBinder _unit _comp scope (AnnBinder ann binder) cont = + withBinder scope binder $ \fbinder binder' -> + cont fbinder + (AnnBinder (Foil.transportName Foil.verbatimTransport ann) binder') + (Foil.extendScope binder' scope) +instance Foil.UnifiablePattern AnnBinder where + unifyPatternsIn _scope l@(AnnBinder x _) r@(AnnBinder y _) + | x == y = Foil.unifyPatterns l r + | otherwise = Foil.NotUnifiable + +type AnnTerm = AST AnnBinder LamSig + +-- | λ(x : ann). x +annId :: Foil.Distinct n => Foil.Scope n -> Foil.Name n -> AnnTerm n +annId scope ann = Foil.withFresh scope $ \x -> + Node (Lam (ScopedAST (AnnBinder ann x) (Var (Foil.nameOf x)))) + +-- | Run a continuation in a scope with two names. +withTwoNames + :: (forall n. Foil.Distinct n => Foil.Scope n -> Foil.Name n -> Foil.Name n -> r) + -> r +withTwoNames cont = + Foil.withFresh Foil.emptyScope $ \a -> + let scope1 = Foil.extendScope a Foil.emptyScope + in Foil.withFresh scope1 $ \b -> + cont (Foil.extendScope b scope1) (Foil.sink (Foil.nameOf a)) (Foil.nameOf b) + -- * Hand-built terms with chosen binder names -- | A binder with a chosen raw name — either fresh for the scope, or @@ -121,7 +167,7 @@ renderShifted :: Int -> Skel -> Term Foil.VoidS renderShifted k s = go k Foil.emptyScope where - go :: Foil.Distinct n => Int -> Foil.Scope n -> Term Foil.VoidS + go :: (Foil.Distinct n, Foil.Ext Foil.VoidS n) => Int -> Foil.Scope n -> Term Foil.VoidS go 0 scope = fromMaybe (error "the term uses a dummy binder") (unsinkAST Foil.emptyScope (renderIn scope [] (case s of SLam{} -> s; _ -> SLam s))) @@ -159,6 +205,17 @@ let t1 = lam 7 (\_a -> lam 5 (\b -> Var b)) t2 = lam 5 (\_a -> lam 5 (\b -> Var b)) alphaEquiv Foil.emptyScope t1 t2 `shouldBe` True + + describe "binders with annotations" $ do + it "rejects λ(x : a). x against λ(x : b). x" $ + withTwoNames $ \scope a b -> + alphaEquiv scope (annId scope a) (annId scope b) `shouldBe` False + it "rejects λ(x : a). x against λ(x : b). x with alphaEquivRefreshed" $ + withTwoNames $ \scope a b -> + alphaEquivRefreshed scope (annId scope a) (annId scope b) `shouldBe` False + it "accepts λ(x : a). x against λ(y : a). y with alphaEquivRefreshed" $ + withTwoNames $ \scope a _ -> + alphaEquivRefreshed scope (annId scope a) (annId scope a) `shouldBe` True describe "agreement with alphaEquivRefreshed" $ do prop "on a term against its shifted rendering" $ \s (Positive k) -> diff --git a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs --- a/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs +++ b/test/Control/Monad/Free/Foil/TH/MkFreeFoilSpec.hs @@ -17,7 +17,7 @@ import Data.Bifunctor (bimap) import Data.Bitraversable (bitraverse) import Data.Monoid (Sum (..)) -import Data.ZipMatchK (Mappings (..), ZipMatchK (..)) +import Data.ZipMatchK (zipMatchWith2) import Test.Hspec import Control.Monad.Free.Foil.TH.MkFreeFoilSpec.Config @@ -50,8 +50,8 @@ it "force a term and its patterns" $ rnf (toTerm Foil.emptyScope Map.empty (Let (PatternVar x) identity (ScopedTerm (Var x)))) `shouldBe` () it "match equal constructors and reject different ones" $ do - zipMatchWithK (zipAdd :^: zipAdd :^: M0) (AppSig 1 2 :: TermSig Int Int) (AppSig 10 20) `shouldBe` Just (AppSig 11 22) - zipMatchWithK (zipAdd :^: zipAdd :^: M0) (AppSig 1 2 :: TermSig Int Int) (FunSig 3) `shouldBe` Nothing + zipMatchWith2 zipAdd zipAdd (AppSig 1 2 :: TermSig Int Int) (AppSig 10 20) `shouldBe` Just (AppSig 11 22) + zipMatchWith2 zipAdd zipAdd (AppSig 1 2 :: TermSig Int Int) (FunSig 3) `shouldBe` Nothing describe "a pattern adjacent to its scope (Fun)" $ it "round-trips, and the body still refers to the binder" $ diff --git a/test/Control/Monad/Free/Foil/UnresolvedNamesSpec.hs b/test/Control/Monad/Free/Foil/UnresolvedNamesSpec.hs new file mode 100644 --- /dev/null +++ b/test/Control/Monad/Free/Foil/UnresolvedNamesSpec.hs @@ -0,0 +1,74 @@ +{-# LANGUAGE DataKinds #-} +{-# LANGUAGE DeriveTraversable #-} +{-# LANGUAGE GADTs #-} +{-# LANGUAGE LambdaCase #-} +{-# LANGUAGE RankNTypes #-} +{-# LANGUAGE TemplateHaskell #-} + +-- | 'unresolvedNames' and 'unresolvedNamesWith' on a small raw λ-calculus, +-- against what 'tryConvertToASTWith' reports. +module Control.Monad.Free.Foil.UnresolvedNamesSpec (spec) where + +import Data.Bifunctor.TH +import Data.Map (Map) +import qualified Data.Map as Map +import Test.Hspec + +import qualified Control.Monad.Foil as Foil +import Control.Monad.Free.Foil +import Data.ZipMatchK.TH (deriveZipMatchK) + +data LamSig scope term + = App term term + | Lam scope + deriving (Functor, Foldable, Traversable) + +deriveBifunctor ''LamSig +deriveBifoldable ''LamSig +deriveBitraversable ''LamSig +deriveZipMatchK ''LamSig + +type Term = AST Foil.NameBinder LamSig + +data Raw = RVar String | RApp Raw Raw | RLam String Raw + +toSig :: Raw -> Either String (LamSig (String, Raw) Raw) +toSig = \case + RVar x -> Left x + RApp f a -> Right (App f a) + RLam x b -> Right (Lam (x, b)) + +fromRawPattern + :: Foil.Distinct n + => Foil.Scope n + -> Map String (Foil.Name n) + -> String + -> (forall l. Foil.DExt n l => Foil.NameBinder n l -> Map String (Foil.Name l) -> r) + -> r +fromRawPattern scope names x cont = Foil.withFresh scope $ \binder -> + cont binder (Map.insert x (Foil.nameOf binder) (fmap Foil.sink names)) + +-- | The constant @c@, which stands for λy. y. +constants :: Map String (Term Foil.VoidS) +constants = Map.singleton "c" $ Foil.withFresh Foil.emptyScope $ \y -> + Node (Lam (ScopedAST y (Var (Foil.nameOf y)))) + +-- | c (λx. x d) +raw :: Raw +raw = RApp (RVar "c") (RLam "x" (RApp (RVar "x") (RVar "d"))) + +spec :: Spec +spec = do + describe "unresolvedNames" $ + it "reports a constant as unresolved" $ + unresolvedNames toSig fromRawPattern id Foil.emptyScope Map.empty raw + `shouldBe` [UnresolvedName "c" [], UnresolvedName "d" ["x"]] + + describe "unresolvedNamesWith" $ do + it "resolves the constants" $ + unresolvedNamesWith toSig fromRawPattern id Foil.emptyScope Map.empty constants raw + `shouldBe` [UnresolvedName "d" ["x", "c"]] + it "reports first what tryConvertToASTWith reports" $ + either Just (const Nothing) + (tryConvertToASTWith toSig fromRawPattern id Foil.emptyScope Map.empty constants raw) + `shouldBe` Just (UnresolvedName "d" ["x", "c"]) diff --git a/test/laws/Control/Monad/Free/Foil/Laws.hs b/test/laws/Control/Monad/Free/Foil/Laws.hs --- a/test/laws/Control/Monad/Free/Foil/Laws.hs +++ b/test/laws/Control/Monad/Free/Foil/Laws.hs @@ -613,7 +613,7 @@ -- a free name by its raw identifier. Patterns are compared by the names -- they bind, listed by the given function, and not by their shape. alphaEqNameless - :: forall binder sig x y. (Bitraversable sig, ZipMatchK sig) + :: forall binder sig x y. ZipMatchK sig => PatternNames binder -> AST binder sig x -> AST binder sig y -> Bool alphaEqNameless binders = go 0 IntMap.empty IntMap.empty where