free-foil-0.5.0: src/Control/Monad/Free/Foil.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 #-}
-- | 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.Coerce (coerce)
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
instance (forall x y. NFData (binder x y), forall l. NFData (AST binder sig l)) => NFData (ScopedAST binder sig n) where
rnf (ScopedAST binder body) = rnf binder `seq` rnf body
-- | A term, generated by a signature 'Bifunctor' @sig@,
-- with (free) variables in scope @n@.
--
-- @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)
deriving instance (forall x y. NFData (binder x y), forall scope term. (NFData scope, NFData term) => NFData (sig scope term))
=> NFData (AST binder sig n)
instance 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
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
-- * \(\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 == coerce 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) = x == coerce 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