free-foil-0.6.1: src/Control/Monad/Free/Foil/Internal.hs
{-# 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