free-foil-0.4.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 qualified Control.Monad.Foil.Relative 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 a raw term into a scope-safe term.
--
-- @since 0.0.3
convertToAST
:: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)
=> (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (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)
-> (rawScopedTerm -> rawTerm)
-> Foil.Scope n
-> Map rawIdent (Foil.Name n)
-> rawTerm
-> AST binder sig n
convertToAST = unsafeConvertToAST
{-# DEPRECATED convertToAST "Renamed to unsafeConvertToAST, since it calls error on an unresolved identifier. Use tryConvertToAST to report them instead." #-}
-- | Same as 'convertToAST' but for scoped terms.
--
-- @since 0.0.3
convertToScopedAST
:: (Foil.Distinct n, Bifunctor sig, Ord rawIdent, Foil.CoSinkable binder)
=> (rawTerm -> Either rawIdent (sig (rawPattern, rawScopedTerm) rawTerm))
-> (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)
-> (rawScopedTerm -> rawTerm)
-> Foil.Scope n
-> Map rawIdent (Foil.Name n)
-> (rawPattern, rawScopedTerm)
-> ScopedAST binder sig n
convertToScopedAST = unsafeConvertToScopedAST
{-# DEPRECATED convertToScopedAST "Renamed to unsafeConvertToScopedAST, since it calls error on an unresolved identifier." #-}
-- ** 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