{-# LANGUAGE BlockArguments             #-}
{-# LANGUAGE ConstraintKinds            #-}
{-# LANGUAGE DataKinds                  #-}
{-# LANGUAGE EmptyCase                  #-}
{-# LANGUAGE FlexibleInstances          #-}
{-# LANGUAGE GADTs                      #-}
{-# LANGUAGE KindSignatures             #-}
{-# LANGUAGE LambdaCase                 #-}
{-# LANGUAGE MultiParamTypeClasses      #-}
{-# LANGUAGE QuantifiedConstraints      #-}
{-# LANGUAGE RankNTypes                 #-}
{-# LANGUAGE ScopedTypeVariables        #-}
{-# LANGUAGE TypeApplications           #-}
{-# LANGUAGE UndecidableInstances       #-}
{-# OPTIONS_GHC -Wno-incomplete-patterns #-}
{-# OPTIONS_GHC -Wno-unrecognised-pragmas #-}
{-# LANGUAGE DerivingStrategies         #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# OPTIONS_GHC -Wno-redundant-constraints #-}
{-# LANGUAGE DefaultSignatures          #-}
-- | Main definitions of the foil that can be
-- reused for specific implementations.
-- This is an internal module, so it also contains implementation details of the foil.
--
-- The original description of this approach
-- is described in the IFL 2022 paper by Maclaurin, Radul, and Paszke
-- [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224).
-- This module also introduces 'CoSinkable' class,
-- generalizing handling of patterns, as described in
-- [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384).
--
-- Since the representation of scopes and substitutions
-- is either 'IntMap' or 'IntSet', many of the operations
-- have a worst-case complexity of \(O(\min(n,W))\).
-- This means that the operation can become linear in the size of the scope \(n\) with a maximum of \(W\)
-- — the number of bits in an 'Int' (32 or 64).
module Control.Monad.Foil.Internal where

import           Control.DeepSeq (NFData (..))
import           Data.Coerce     (coerce)
import           Data.IntMap
import qualified Data.IntMap     as IntMap
import           Data.IntSet
import qualified Data.IntSet     as IntSet
import           Data.Kind       (Type)
import           Unsafe.Coerce

-- * Safe types and operations

-- | 'S' is a data kind of scope indices.
data S
  = VoidS -- ^ 'VoidS' is the only explicit scope available to the users, representing an empty scope.
          -- All other scopes are represented with type variables,
          -- bound in rank-2 polymophic functions like 'withFreshBinder'.

-- | A safe scope, indexed by a type-level scope index 'n'.
newtype Scope (n :: S) = UnsafeScope RawScope
  deriving newtype Scope n -> ()
(Scope n -> ()) -> NFData (Scope n)
forall a. (a -> ()) -> NFData a
forall (n :: S). Scope n -> ()
$crnf :: forall (n :: S). Scope n -> ()
rnf :: Scope n -> ()
NFData

-- | A name in a safe scope, indexed by a type-level scope index 'n'.
newtype Name (n :: S) = UnsafeName RawName
  deriving newtype (Name n -> ()
(Name n -> ()) -> NFData (Name n)
forall a. (a -> ()) -> NFData a
forall (n :: S). Name n -> ()
$crnf :: forall (n :: S). Name n -> ()
rnf :: Name n -> ()
NFData, Name n -> Name n -> Bool
(Name n -> Name n -> Bool)
-> (Name n -> Name n -> Bool) -> Eq (Name n)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: S). Name n -> Name n -> Bool
$c== :: forall (n :: S). Name n -> Name n -> Bool
== :: Name n -> Name n -> Bool
$c/= :: forall (n :: S). Name n -> Name n -> Bool
/= :: Name n -> Name n -> Bool
Eq, Eq (Name n)
Eq (Name n) =>
(Name n -> Name n -> Ordering)
-> (Name n -> Name n -> Bool)
-> (Name n -> Name n -> Bool)
-> (Name n -> Name n -> Bool)
-> (Name n -> Name n -> Bool)
-> (Name n -> Name n -> Name n)
-> (Name n -> Name n -> Name n)
-> Ord (Name n)
Name n -> Name n -> Bool
Name n -> Name n -> Ordering
Name n -> Name n -> Name n
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (n :: S). Eq (Name n)
forall (n :: S). Name n -> Name n -> Bool
forall (n :: S). Name n -> Name n -> Ordering
forall (n :: S). Name n -> Name n -> Name n
$ccompare :: forall (n :: S). Name n -> Name n -> Ordering
compare :: Name n -> Name n -> Ordering
$c< :: forall (n :: S). Name n -> Name n -> Bool
< :: Name n -> Name n -> Bool
$c<= :: forall (n :: S). Name n -> Name n -> Bool
<= :: Name n -> Name n -> Bool
$c> :: forall (n :: S). Name n -> Name n -> Bool
> :: Name n -> Name n -> Bool
$c>= :: forall (n :: S). Name n -> Name n -> Bool
>= :: Name n -> Name n -> Bool
$cmax :: forall (n :: S). Name n -> Name n -> Name n
max :: Name n -> Name n -> Name n
$cmin :: forall (n :: S). Name n -> Name n -> Name n
min :: Name n -> Name n -> Name n
Ord, RawName -> Name n -> ShowS
[Name n] -> ShowS
Name n -> String
(RawName -> Name n -> ShowS)
-> (Name n -> String) -> ([Name n] -> ShowS) -> Show (Name n)
forall a.
(RawName -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: S). RawName -> Name n -> ShowS
forall (n :: S). [Name n] -> ShowS
forall (n :: S). Name n -> String
$cshowsPrec :: forall (n :: S). RawName -> Name n -> ShowS
showsPrec :: RawName -> Name n -> ShowS
$cshow :: forall (n :: S). Name n -> String
show :: Name n -> String
$cshowList :: forall (n :: S). [Name n] -> ShowS
showList :: [Name n] -> ShowS
Show)

-- | Convert 'Name' into an identifier.
-- This may be useful for printing and debugging.
nameId :: Name l -> Id
nameId :: forall (l :: S). Name l -> RawName
nameId (UnsafeName RawName
i) = RawName
i

-- | A name binder is a name that extends scope @n@ to a (larger) scope @l@.
newtype NameBinder (n :: S) (l :: S) =
  UnsafeNameBinder (Name l)
    deriving newtype (NameBinder n l -> ()
(NameBinder n l -> ()) -> NFData (NameBinder n l)
forall a. (a -> ()) -> NFData a
forall (n :: S) (l :: S). NameBinder n l -> ()
$crnf :: forall (n :: S) (l :: S). NameBinder n l -> ()
rnf :: NameBinder n l -> ()
NFData, NameBinder n l -> NameBinder n l -> Bool
(NameBinder n l -> NameBinder n l -> Bool)
-> (NameBinder n l -> NameBinder n l -> Bool)
-> Eq (NameBinder n l)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall (n :: S) (l :: S). NameBinder n l -> NameBinder n l -> Bool
$c== :: forall (n :: S) (l :: S). NameBinder n l -> NameBinder n l -> Bool
== :: NameBinder n l -> NameBinder n l -> Bool
$c/= :: forall (n :: S) (l :: S). NameBinder n l -> NameBinder n l -> Bool
/= :: NameBinder n l -> NameBinder n l -> Bool
Eq, Eq (NameBinder n l)
Eq (NameBinder n l) =>
(NameBinder n l -> NameBinder n l -> Ordering)
-> (NameBinder n l -> NameBinder n l -> Bool)
-> (NameBinder n l -> NameBinder n l -> Bool)
-> (NameBinder n l -> NameBinder n l -> Bool)
-> (NameBinder n l -> NameBinder n l -> Bool)
-> (NameBinder n l -> NameBinder n l -> NameBinder n l)
-> (NameBinder n l -> NameBinder n l -> NameBinder n l)
-> Ord (NameBinder n l)
NameBinder n l -> NameBinder n l -> Bool
NameBinder n l -> NameBinder n l -> Ordering
NameBinder n l -> NameBinder n l -> NameBinder n l
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
forall (n :: S) (l :: S). Eq (NameBinder n l)
forall (n :: S) (l :: S). NameBinder n l -> NameBinder n l -> Bool
forall (n :: S) (l :: S).
NameBinder n l -> NameBinder n l -> Ordering
forall (n :: S) (l :: S).
NameBinder n l -> NameBinder n l -> NameBinder n l
$ccompare :: forall (n :: S) (l :: S).
NameBinder n l -> NameBinder n l -> Ordering
compare :: NameBinder n l -> NameBinder n l -> Ordering
$c< :: forall (n :: S) (l :: S). NameBinder n l -> NameBinder n l -> Bool
< :: NameBinder n l -> NameBinder n l -> Bool
$c<= :: forall (n :: S) (l :: S). NameBinder n l -> NameBinder n l -> Bool
<= :: NameBinder n l -> NameBinder n l -> Bool
$c> :: forall (n :: S) (l :: S). NameBinder n l -> NameBinder n l -> Bool
> :: NameBinder n l -> NameBinder n l -> Bool
$c>= :: forall (n :: S) (l :: S). NameBinder n l -> NameBinder n l -> Bool
>= :: NameBinder n l -> NameBinder n l -> Bool
$cmax :: forall (n :: S) (l :: S).
NameBinder n l -> NameBinder n l -> NameBinder n l
max :: NameBinder n l -> NameBinder n l -> NameBinder n l
$cmin :: forall (n :: S) (l :: S).
NameBinder n l -> NameBinder n l -> NameBinder n l
min :: NameBinder n l -> NameBinder n l -> NameBinder n l
Ord, RawName -> NameBinder n l -> ShowS
[NameBinder n l] -> ShowS
NameBinder n l -> String
(RawName -> NameBinder n l -> ShowS)
-> (NameBinder n l -> String)
-> ([NameBinder n l] -> ShowS)
-> Show (NameBinder n l)
forall a.
(RawName -> a -> ShowS)
-> (a -> String) -> ([a] -> ShowS) -> Show a
forall (n :: S) (l :: S). RawName -> NameBinder n l -> ShowS
forall (n :: S) (l :: S). [NameBinder n l] -> ShowS
forall (n :: S) (l :: S). NameBinder n l -> String
$cshowsPrec :: forall (n :: S) (l :: S). RawName -> NameBinder n l -> ShowS
showsPrec :: RawName -> NameBinder n l -> ShowS
$cshow :: forall (n :: S) (l :: S). NameBinder n l -> String
show :: NameBinder n l -> String
$cshowList :: forall (n :: S) (l :: S). [NameBinder n l] -> ShowS
showList :: [NameBinder n l] -> ShowS
Show)

-- | An empty scope (without any names).
emptyScope :: Scope VoidS
emptyScope :: Scope 'VoidS
emptyScope = RawScope -> Scope 'VoidS
forall (n :: S). RawScope -> Scope n
UnsafeScope RawScope
IntSet.empty

-- | A runtime check for potential name capture.
member :: Name l -> Scope n -> Bool
member :: forall (l :: S) (n :: S). Name l -> Scope n -> Bool
member (UnsafeName RawName
name) (UnsafeScope RawScope
s) = RawName -> RawScope -> Bool
rawMember RawName
name RawScope
s

-- ** Extending scopes

-- | \(O(\min(n,W))\).
-- Extend a scope with one name (safely).
-- Note that as long as the foil is used as intended,
-- the name binder is guaranteed to introduce a name
-- that does not appear in the initial scope.
extendScope :: NameBinder n l -> Scope n -> Scope l
extendScope :: forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
extendScope (UnsafeNameBinder (UnsafeName RawName
name)) (UnsafeScope RawScope
scope) =
  RawScope -> Scope l
forall (n :: S). RawScope -> Scope n
UnsafeScope (RawName -> RawScope -> RawScope
IntSet.insert RawName
name RawScope
scope)

-- | Extend scope with variables inside a pattern.
-- This is a more flexible version of 'extendScope'.
extendScopePattern
  :: (Distinct n, CoSinkable pattern)
  => pattern n l -> Scope n -> Scope l
extendScopePattern :: forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern pattern n l
pat Scope n
scope = (forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     ExtendScope x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S).
    DExt z z' =>
    ExtendScope x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    ExtendScope x y z z'
    -> ExtendScope y y' z' z'' -> ExtendScope x y' z z'')
-> Scope n
-> pattern n l
-> (forall (o' :: S).
    DExt n o' =>
    ExtendScope n l n o' -> pattern n o' -> Scope l)
-> Scope l
forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
forall (pattern :: S -> S -> *) (o :: S)
       (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
(CoSinkable pattern, Distinct o) =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
withPattern
  (\Scope z
_scope' NameBinder x y
binder forall (z' :: S).
DExt z z' =>
ExtendScope x y z z' -> NameBinder z z' -> r'
k ->
    NameBinder x y -> (DExt z Any => NameBinder z Any -> r') -> r'
forall (n :: S) (l :: S) (n' :: S) (l' :: S) r.
NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r
unsafeAssertFresh NameBinder x y
binder ((DExt z Any => NameBinder z Any -> r') -> r')
-> (DExt z Any => NameBinder z Any -> r') -> r'
forall a b. (a -> b) -> a -> b
$ \NameBinder z Any
binder' ->
      ExtendScope x y z Any -> NameBinder z Any -> r'
forall (z' :: S).
DExt z z' =>
ExtendScope x y z z' -> NameBinder z z' -> r'
k ((Scope x -> Scope y) -> ExtendScope x y z Any
forall (n :: S) (l :: S) (o :: S) (o' :: S).
(Scope n -> Scope l) -> ExtendScope n l o o'
ExtendScope (NameBinder x y -> Scope x -> Scope y
forall (n :: S) (l :: S). NameBinder n l -> Scope n -> Scope l
extendScope NameBinder x y
binder)) NameBinder z Any
binder')
  ExtendScope x x z z'
forall (n :: S) (o :: S) (o' :: S). ExtendScope n n o o'
forall (x :: S) (z :: S) (z' :: S).
DExt z z' =>
ExtendScope x x z z'
idExtendScope
  ExtendScope x y z z'
-> ExtendScope y y' z' z'' -> ExtendScope x y' z z''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
ExtendScope x y z z'
-> ExtendScope y y' z' z'' -> ExtendScope x y' z z''
forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S).
ExtendScope n i o o'
-> ExtendScope i l o' o'' -> ExtendScope n l o o''
compExtendScope
  Scope n
scope
  pattern n l
pat
  (\(ExtendScope Scope n -> Scope l
extend) pattern n o'
_ -> Scope n -> Scope l
extend Scope n
scope)

-- | Auxiliary data structure for scope extension. Used in 'extendScopePattern'.
newtype ExtendScope n l (o :: S) (o' :: S) = ExtendScope (Scope n -> Scope l)

-- | Identity scope extension (no extension).
idExtendScope :: ExtendScope n n o o'
idExtendScope :: forall (n :: S) (o :: S) (o' :: S). ExtendScope n n o o'
idExtendScope = (Scope n -> Scope n) -> ExtendScope n n o o'
forall (n :: S) (l :: S) (o :: S) (o' :: S).
(Scope n -> Scope l) -> ExtendScope n l o o'
ExtendScope Scope n -> Scope n
forall a. a -> a
id

-- | Compose scope extensions.
compExtendScope
  :: ExtendScope n i o o'
  -> ExtendScope i l o' o''
  -> ExtendScope n l o o''
compExtendScope :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S).
ExtendScope n i o o'
-> ExtendScope i l o' o'' -> ExtendScope n l o o''
compExtendScope (ExtendScope Scope n -> Scope i
f) (ExtendScope Scope i -> Scope l
g)
  = (Scope n -> Scope l) -> ExtendScope n l o o''
forall (n :: S) (l :: S) (o :: S) (o' :: S).
(Scope n -> Scope l) -> ExtendScope n l o o'
ExtendScope (Scope i -> Scope l
g (Scope i -> Scope l) -> (Scope n -> Scope i) -> Scope n -> Scope l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Scope n -> Scope i
f)

-- ** Collecting new names

-- | Extract name from a name binder.
nameOf :: NameBinder n l -> Name l
nameOf :: forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf (UnsafeNameBinder Name l
name) = Name l
name

-- | Extract names from a pattern.
-- This is a more flexible version of 'namesOf'.
namesOfPattern
  :: forall pattern n l. (Distinct n, CoSinkable pattern) => pattern n l -> [Name l]
namesOfPattern :: forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> [Name l]
namesOfPattern pattern n l
pat = forall (pattern :: S -> S -> *) (o :: S)
       (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
(CoSinkable pattern, Distinct o) =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
withPattern @_ @n
  (\Scope z
_scope' NameBinder x y
binder forall (z' :: S).
DExt z z' =>
NamesOf x y z z' -> NameBinder z z' -> r'
k ->
    NameBinder x y -> (DExt z Any => NameBinder z Any -> r') -> r'
forall (n :: S) (l :: S) (n' :: S) (l' :: S) r.
NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r
unsafeAssertFresh NameBinder x y
binder ((DExt z Any => NameBinder z Any -> r') -> r')
-> (DExt z Any => NameBinder z Any -> r') -> r'
forall a b. (a -> b) -> a -> b
$ \NameBinder z Any
binder' ->
      NamesOf x y z Any -> NameBinder z Any -> r'
forall (z' :: S).
DExt z z' =>
NamesOf x y z z' -> NameBinder z z' -> r'
k ([Name y] -> NamesOf x y z Any
forall (n :: S) (l :: S) (o :: S) (o' :: S).
[Name l] -> NamesOf n l o o'
NamesOf [NameBinder x y -> Name y
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder x y
binder]) NameBinder z Any
binder')
  NamesOf x x z z'
forall (n :: S) (o :: S) (o' :: S). NamesOf n n o o'
forall (x :: S) (z :: S) (z' :: S). DExt z z' => NamesOf x x z z'
idNamesOf NamesOf x y z z' -> NamesOf y y' z' z'' -> NamesOf x y' z z''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
NamesOf x y z z' -> NamesOf y y' z' z'' -> NamesOf x y' z z''
forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S).
NamesOf n i o o' -> NamesOf i l o' o'' -> NamesOf n l o o''
compNamesOf (String -> Scope n
forall a. HasCallStack => String -> a
error String
"impossible") pattern n l
pat
  (\(NamesOf [Name l]
names) pattern n o'
_ -> [Name l]
names)

-- | Auxiliary structure collecting names in scope @l@ that extend scope @n@.
-- Used in 'namesOfPattern'.
newtype NamesOf (n :: S) l (o :: S) (o' :: S) = NamesOf [Name l]

-- | Empty list of names in scope @n@.
idNamesOf :: NamesOf n n o o'
idNamesOf :: forall (n :: S) (o :: S) (o' :: S). NamesOf n n o o'
idNamesOf = [Name n] -> NamesOf n n o o'
forall (n :: S) (l :: S) (o :: S) (o' :: S).
[Name l] -> NamesOf n l o o'
NamesOf []

-- | Concatenation of names, resulting in a list of names in @l@ that extend scope @n@.
compNamesOf :: NamesOf n i o o' -> NamesOf i l o' o'' -> NamesOf n l o o''
compNamesOf :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S).
NamesOf n i o o' -> NamesOf i l o' o'' -> NamesOf n l o o''
compNamesOf (NamesOf [Name i]
xs) (NamesOf [Name l]
ys) =
  [Name l] -> NamesOf n l o o''
forall (n :: S) (l :: S) (o :: S) (o' :: S).
[Name l] -> NamesOf n l o o'
NamesOf ([Name i] -> [Name l]
forall a b. Coercible a b => a -> b
coerce [Name i]
xs [Name l] -> [Name l] -> [Name l]
forall a. [a] -> [a] -> [a]
++ [Name l]
ys)

-- ** Refreshing binders

-- | Allocate a fresh binder for a given scope.
withFreshBinder
  :: Scope n
  -> (forall l. NameBinder n l -> r) -> r
withFreshBinder :: forall (n :: S) r.
Scope n -> (forall (l :: S). NameBinder n l -> r) -> r
withFreshBinder (UnsafeScope RawScope
scope) forall (l :: S). NameBinder n l -> r
cont =
  NameBinder n Any -> r
forall (l :: S). NameBinder n l -> r
cont NameBinder n Any
binder
  where
    binder :: NameBinder n Any
binder = Name Any -> NameBinder n Any
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder (RawName -> Name Any
forall (n :: S). RawName -> Name n
UnsafeName (RawScope -> RawName
rawFreshName RawScope
scope))

-- | Safely produce a fresh name binder with respect to a given scope.
withFresh
  :: Distinct n => Scope n
  -> (forall l. DExt n l => NameBinder n l -> r) -> r
withFresh :: forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
withFresh Scope n
scope forall (l :: S). DExt n l => NameBinder n l -> r
cont = Scope n -> (forall (l :: S). NameBinder n l -> r) -> r
forall (n :: S) r.
Scope n -> (forall (l :: S). NameBinder n l -> r) -> r
withFreshBinder Scope n
scope (NameBinder n l -> (DExt n Any => NameBinder n Any -> r) -> r
forall (n :: S) (l :: S) (n' :: S) (l' :: S) r.
NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r
`unsafeAssertFresh` DExt n Any => NameBinder n Any -> r
NameBinder n Any -> r
forall (l :: S). DExt n l => NameBinder n l -> r
cont)

-- | Rename a given pattern into a fresh version of it to extend a given scope.
--
-- This is similar to 'withRefreshPattern', except here renaming always takes place.
withFreshPattern
  :: (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)
  => Scope o      -- ^ Ambient scope.
  -> pattern n l  -- ^ Pattern to refresh (if it clashes with the ambient scope).
  -> (forall o'. DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
  -- ^ Continuation, accepting the refreshed pattern.
  -> r
withFreshPattern :: forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
       (l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
withFreshPattern Scope o
scope pattern n l
pattern forall (o' :: S).
DExt o o' =>
(Substitution e n o -> Substitution e l o') -> pattern o o' -> r
cont = (forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     WithRefreshedPattern e x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S).
    DExt z z' =>
    WithRefreshedPattern e x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    WithRefreshedPattern e x y z z'
    -> WithRefreshedPattern e y y' z' z''
    -> WithRefreshedPattern e x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    WithRefreshedPattern e n l o o' -> pattern o o' -> r)
-> r
forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
forall (pattern :: S -> S -> *) (o :: S)
       (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
(CoSinkable pattern, Distinct o) =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
withPattern
  (\Scope z
scope' NameBinder x y
binder forall (z' :: S).
DExt z z' =>
WithRefreshedPattern e x y z z' -> NameBinder z z' -> r'
f -> Scope z
-> (forall (l :: S). DExt z l => NameBinder z l -> r') -> r'
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
withFresh Scope z
scope'
    (\NameBinder z l
binder' -> WithRefreshedPattern e x y z l -> NameBinder z l -> r'
forall (z' :: S).
DExt z z' =>
WithRefreshedPattern e x y z z' -> NameBinder z z' -> r'
f ((Substitution e x z -> Substitution e y l)
-> WithRefreshedPattern e x y z l
forall (e :: S -> *) (n :: S) (l :: S) (o :: S) (o' :: S).
(Substitution e n o -> Substitution e l o')
-> WithRefreshedPattern e n l o o'
WithRefreshedPattern (\Substitution e x z
subst -> Substitution e x l
-> NameBinder x y -> Name l -> Substitution e y l
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
InjectName e =>
Substitution e i o
-> NameBinder i i' -> Name o -> Substitution e i' o
addRename (Substitution e x z -> Substitution e x l
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink Substitution e x z
subst) NameBinder x y
binder (NameBinder z l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder z l
binder'))) NameBinder z l
binder'))
  WithRefreshedPattern e x x z z'
forall (x :: S) (z :: S) (z' :: S).
DExt z z' =>
WithRefreshedPattern e x x z z'
forall (e :: S -> *) (o :: S) (o' :: S) (n :: S).
(Sinkable e, DExt o o') =>
WithRefreshedPattern e n n o o'
idWithRefreshedPattern
  WithRefreshedPattern e x y z z'
-> WithRefreshedPattern e y y' z' z''
-> WithRefreshedPattern e x y' z z''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
WithRefreshedPattern e x y z z'
-> WithRefreshedPattern e y y' z' z''
-> WithRefreshedPattern e x y' z z''
forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> *) (n :: S)
       (i :: S) (l :: S).
(DExt o o', DExt o' o'') =>
WithRefreshedPattern e n i o o'
-> WithRefreshedPattern e i l o' o''
-> WithRefreshedPattern e n l o o''
compWithRefreshedPattern
  Scope o
scope
  pattern n l
pattern
  (\(WithRefreshedPattern Substitution e n o -> Substitution e l o'
f) pattern o o'
pattern' -> (Substitution e n o -> Substitution e l o') -> pattern o o' -> r
forall (o' :: S).
DExt o o' =>
(Substitution e n o -> Substitution e l o') -> pattern o o' -> r
cont Substitution e n o -> Substitution e l o'
f pattern o o'
pattern')

-- | Safely rename (if necessary) a given name to extend a given scope.
-- This is similar to 'withFresh', except if the name does not clash with
-- the scope, it can be used immediately, without renaming.
withRefreshed
  :: Distinct o
  => Scope o    -- ^ Ambient scope.
  -> Name i     -- ^ Name to refresh (if it clashes with the ambient scope).
  -> (forall o'. DExt o o' => NameBinder o o' -> r)
  -- ^ Continuation, accepting the refreshed name.
  -> r
withRefreshed :: forall (o :: S) (i :: S) r.
Distinct o =>
Scope o
-> Name i
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r)
-> r
withRefreshed scope :: Scope o
scope@(UnsafeScope RawScope
rawScope) name :: Name i
name@(UnsafeName RawName
rawName) forall (o' :: S). DExt o o' => NameBinder o o' -> r
cont
  | RawName -> RawScope -> Bool
IntSet.member RawName
rawName RawScope
rawScope = Scope o
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r) -> r
forall (n :: S) r.
Distinct n =>
Scope n -> (forall (l :: S). DExt n l => NameBinder n l -> r) -> r
withFresh Scope o
scope NameBinder o l -> r
forall (o' :: S). DExt o o' => NameBinder o o' -> r
cont
  | Bool
otherwise = NameBinder Any i -> (DExt o Any => NameBinder o Any -> r) -> r
forall (n :: S) (l :: S) (n' :: S) (l' :: S) r.
NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r
unsafeAssertFresh (Name i -> NameBinder Any i
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder Name i
name) DExt o Any => NameBinder o Any -> r
NameBinder o Any -> r
forall (o' :: S). DExt o o' => NameBinder o o' -> r
cont

-- | Safely rename (if necessary) a given pattern to extend a given scope.
-- This is similar to 'withFreshPattern', except if a name in the pattern
-- does not clash with the scope, it can be used immediately, without renaming.
--
-- This is a more general version of 'withRefreshed'.
withRefreshedPattern
  :: (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)
  => Scope o      -- ^ Ambient scope.
  -> pattern n l  -- ^ Pattern to refresh (if it clashes with the ambient scope).
  -> (forall o'. DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
  -- ^ Continuation, accepting the refreshed pattern.
  -> r
withRefreshedPattern :: forall (o :: S) (pattern :: S -> S -> *) (e :: S -> *) (n :: S)
       (l :: S) r.
(Distinct o, CoSinkable pattern, Sinkable e, InjectName e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> r
withRefreshedPattern Scope o
scope pattern n l
pattern forall (o' :: S).
DExt o o' =>
(Substitution e n o -> Substitution e l o') -> pattern o o' -> r
cont = (forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     WithRefreshedPattern e x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S).
    DExt z z' =>
    WithRefreshedPattern e x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    WithRefreshedPattern e x y z z'
    -> WithRefreshedPattern e y y' z' z''
    -> WithRefreshedPattern e x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    WithRefreshedPattern e n l o o' -> pattern o o' -> r)
-> r
forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
forall (pattern :: S -> S -> *) (o :: S)
       (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
(CoSinkable pattern, Distinct o) =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
withPattern
  (\Scope z
scope' NameBinder x y
binder forall (z' :: S).
DExt z z' =>
WithRefreshedPattern e x y z z' -> NameBinder z z' -> r'
f -> Scope z
-> Name y
-> (forall (o' :: S). DExt z o' => NameBinder z o' -> r')
-> r'
forall (o :: S) (i :: S) r.
Distinct o =>
Scope o
-> Name i
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r)
-> r
withRefreshed Scope z
scope' (NameBinder x y -> Name y
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder x y
binder)
    (\NameBinder z o'
binder' -> WithRefreshedPattern e x y z o' -> NameBinder z o' -> r'
forall (z' :: S).
DExt z z' =>
WithRefreshedPattern e x y z z' -> NameBinder z z' -> r'
f ((Substitution e x z -> Substitution e y o')
-> WithRefreshedPattern e x y z o'
forall (e :: S -> *) (n :: S) (l :: S) (o :: S) (o' :: S).
(Substitution e n o -> Substitution e l o')
-> WithRefreshedPattern e n l o o'
WithRefreshedPattern (\Substitution e x z
subst -> Substitution e x o'
-> NameBinder x y -> Name o' -> Substitution e y o'
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
InjectName e =>
Substitution e i o
-> NameBinder i i' -> Name o -> Substitution e i' o
addRename (Substitution e x z -> Substitution e x o'
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink Substitution e x z
subst) NameBinder x y
binder (NameBinder z o' -> Name o'
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder z o'
binder'))) NameBinder z o'
binder'))
  WithRefreshedPattern e x x z z'
forall (x :: S) (z :: S) (z' :: S).
DExt z z' =>
WithRefreshedPattern e x x z z'
forall (e :: S -> *) (o :: S) (o' :: S) (n :: S).
(Sinkable e, DExt o o') =>
WithRefreshedPattern e n n o o'
idWithRefreshedPattern
  WithRefreshedPattern e x y z z'
-> WithRefreshedPattern e y y' z' z''
-> WithRefreshedPattern e x y' z z''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
WithRefreshedPattern e x y z z'
-> WithRefreshedPattern e y y' z' z''
-> WithRefreshedPattern e x y' z z''
forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> *) (n :: S)
       (i :: S) (l :: S).
(DExt o o', DExt o' o'') =>
WithRefreshedPattern e n i o o'
-> WithRefreshedPattern e i l o' o''
-> WithRefreshedPattern e n l o o''
compWithRefreshedPattern
  Scope o
scope
  pattern n l
pattern
  (\(WithRefreshedPattern Substitution e n o -> Substitution e l o'
f) pattern o o'
pattern' -> (Substitution e n o -> Substitution e l o') -> pattern o o' -> r
forall (o' :: S).
DExt o o' =>
(Substitution e n o -> Substitution e l o') -> pattern o o' -> r
cont Substitution e n o -> Substitution e l o'
f pattern o o'
pattern')

-- | Refresh (if needed) bound variables introduced in a pattern.
--
-- This is a version of 'withRefreshedPattern' that uses functional renamings instead of 'Substitution'.
withRefreshedPattern'
  :: (CoSinkable pattern, Distinct o, InjectName e, Sinkable e)
  => Scope o
  -> pattern n l
  -> (forall o'. DExt o o' => ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r) -> r
withRefreshedPattern' :: forall (pattern :: S -> S -> *) (o :: S) (e :: S -> *) (n :: S)
       (l :: S) r.
(CoSinkable pattern, Distinct o, InjectName e, Sinkable e) =>
Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r)
-> r
withRefreshedPattern' Scope o
scope pattern n l
pattern forall (o' :: S).
DExt o o' =>
((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r
cont = (forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     WithRefreshedPattern' e x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S).
    DExt z z' =>
    WithRefreshedPattern' e x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    WithRefreshedPattern' e x y z z'
    -> WithRefreshedPattern' e y y' z' z''
    -> WithRefreshedPattern' e x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S).
    DExt o o' =>
    WithRefreshedPattern' e n l o o' -> pattern o o' -> r)
-> r
forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
forall (pattern :: S -> S -> *) (o :: S)
       (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
(CoSinkable pattern, Distinct o) =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
withPattern
  (\Scope z
scope' NameBinder x y
binder forall (z' :: S).
DExt z z' =>
WithRefreshedPattern' e x y z z' -> NameBinder z z' -> r'
f -> Scope z
-> Name y
-> (forall (o' :: S). DExt z o' => NameBinder z o' -> r')
-> r'
forall (o :: S) (i :: S) r.
Distinct o =>
Scope o
-> Name i
-> (forall (o' :: S). DExt o o' => NameBinder o o' -> r)
-> r
withRefreshed Scope z
scope' (NameBinder x y -> Name y
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder x y
binder)
    (\NameBinder z o'
binder' ->
      let k :: (Name x -> e z) -> Name y -> e o'
k Name x -> e z
subst Name y
name = case NameBinder x y -> Name y -> Maybe (Name x)
forall (n :: S) (l :: S).
NameBinder n l -> Name l -> Maybe (Name n)
unsinkName NameBinder x y
binder Name y
name of
              Maybe (Name x)
Nothing    -> Name o' -> e o'
forall (n :: S). Name n -> e n
forall (e :: S -> *) (n :: S). InjectName e => Name n -> e n
injectName (NameBinder z o' -> Name o'
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder z o'
binder')
              Just Name x
name' -> e z -> e o'
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink (Name x -> e z
subst Name x
name')
       in WithRefreshedPattern' e x y z o' -> NameBinder z o' -> r'
forall (z' :: S).
DExt z z' =>
WithRefreshedPattern' e x y z z' -> NameBinder z z' -> r'
f (((Name x -> e z) -> Name y -> e o')
-> WithRefreshedPattern' e x y z o'
forall (e :: S -> *) (n :: S) (l :: S) (o :: S) (o' :: S).
((Name n -> e o) -> Name l -> e o')
-> WithRefreshedPattern' e n l o o'
WithRefreshedPattern' (Name x -> e z) -> Name y -> e o'
k) NameBinder z o'
binder'))
  WithRefreshedPattern' e x x z z'
forall (x :: S) (z :: S) (z' :: S).
DExt z z' =>
WithRefreshedPattern' e x x z z'
forall (e :: S -> *) (o :: S) (o' :: S) (n :: S).
(Sinkable e, DExt o o') =>
WithRefreshedPattern' e n n o o'
idWithRefreshedPattern'
  WithRefreshedPattern' e x y z z'
-> WithRefreshedPattern' e y y' z' z''
-> WithRefreshedPattern' e x y' z z''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
WithRefreshedPattern' e x y z z'
-> WithRefreshedPattern' e y y' z' z''
-> WithRefreshedPattern' e x y' z z''
forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> *) (n :: S)
       (i :: S) (l :: S).
(DExt o o', DExt o' o'') =>
WithRefreshedPattern' e n i o o'
-> WithRefreshedPattern' e i l o' o''
-> WithRefreshedPattern' e n l o o''
compWithRefreshedPattern'
  Scope o
scope
  pattern n l
pattern
  (\(WithRefreshedPattern' (Name n -> e o) -> Name l -> e o'
f) pattern o o'
pattern' -> ((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r
forall (o' :: S).
DExt o o' =>
((Name n -> e o) -> Name l -> e o') -> pattern o o' -> r
cont (Name n -> e o) -> Name l -> e o'
f pattern o o'
pattern')

-- | Unsafely declare that a given name (binder)
-- is already fresh in any scope @n'@.
unsafeAssertFresh :: forall n l n' l' r. NameBinder n l
  -> (DExt n' l' => NameBinder n' l' -> r) -> r
unsafeAssertFresh :: forall (n :: S) (l :: S) (n' :: S) (l' :: S) r.
NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r
unsafeAssertFresh NameBinder n l
binder DExt n' l' => NameBinder n' l' -> r
cont =
  case forall (n :: S). DistinctEvidence n
unsafeDistinct @l' of
    DistinctEvidence l'
Distinct -> case forall (n :: S) (l :: S). ExtEvidence n l
unsafeExt @n' @l' of
      ExtEvidence n' l'
Ext -> DExt n' l' => NameBinder n' l' -> r
NameBinder n' l' -> r
cont (NameBinder n l -> NameBinder n' l'
forall a b. a -> b
unsafeCoerce NameBinder n l
binder)

-- | Auxiliary structure to accumulate substitution extensions
-- produced when refreshing a pattern.
-- Used in 'withRefreshedPattern' and 'withFreshPattern'.
newtype WithRefreshedPattern e n l o o' = WithRefreshedPattern (Substitution e n o -> Substitution e l o')

-- | Trivial substitution (coercion via 'sink').
idWithRefreshedPattern :: (Sinkable e, DExt o o') => WithRefreshedPattern e n n o o'
idWithRefreshedPattern :: forall (e :: S -> *) (o :: S) (o' :: S) (n :: S).
(Sinkable e, DExt o o') =>
WithRefreshedPattern e n n o o'
idWithRefreshedPattern = (Substitution e n o -> Substitution e n o')
-> WithRefreshedPattern e n n o o'
forall (e :: S -> *) (n :: S) (l :: S) (o :: S) (o' :: S).
(Substitution e n o -> Substitution e l o')
-> WithRefreshedPattern e n l o o'
WithRefreshedPattern Substitution e n o -> Substitution e n o'
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink

-- | Composition of substitution extensions.
compWithRefreshedPattern
  :: (DExt o o', DExt o' o'')
  => WithRefreshedPattern e n i o o'
  -> WithRefreshedPattern e i l o' o''
  -> WithRefreshedPattern e n l o o''
compWithRefreshedPattern :: forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> *) (n :: S)
       (i :: S) (l :: S).
(DExt o o', DExt o' o'') =>
WithRefreshedPattern e n i o o'
-> WithRefreshedPattern e i l o' o''
-> WithRefreshedPattern e n l o o''
compWithRefreshedPattern (WithRefreshedPattern Substitution e n o -> Substitution e i o'
f) (WithRefreshedPattern Substitution e i o' -> Substitution e l o''
g) =
  (Substitution e n o -> Substitution e l o'')
-> WithRefreshedPattern e n l o o''
forall (e :: S -> *) (n :: S) (l :: S) (o :: S) (o' :: S).
(Substitution e n o -> Substitution e l o')
-> WithRefreshedPattern e n l o o'
WithRefreshedPattern (Substitution e i o' -> Substitution e l o''
g (Substitution e i o' -> Substitution e l o'')
-> (Substitution e n o -> Substitution e i o')
-> Substitution e n o
-> Substitution e l o''
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Substitution e n o -> Substitution e i o'
f)

-- | Auxiliary structure to accumulate substitution extensions
-- produced when refreshing a pattern.
-- Similar to 'WithRefreshedPattern', except here substitutions are represented as functions.
-- Used in 'withRefreshedPattern''.
newtype WithRefreshedPattern' e n l (o :: S) (o' :: S) = WithRefreshedPattern' ((Name n -> e o) -> Name l -> e o')

-- | Trivial substitution extension (coercion via 'sink').
idWithRefreshedPattern' :: (Sinkable e, DExt o o') => WithRefreshedPattern' e n n o o'
idWithRefreshedPattern' :: forall (e :: S -> *) (o :: S) (o' :: S) (n :: S).
(Sinkable e, DExt o o') =>
WithRefreshedPattern' e n n o o'
idWithRefreshedPattern' = ((Name n -> e o) -> Name n -> e o')
-> WithRefreshedPattern' e n n o o'
forall (e :: S -> *) (n :: S) (l :: S) (o :: S) (o' :: S).
((Name n -> e o) -> Name l -> e o')
-> WithRefreshedPattern' e n l o o'
WithRefreshedPattern' (\Name n -> e o
f Name n
n -> e o -> e o'
forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink (Name n -> e o
f Name n
n))

-- | Composition of substitution extensions.
compWithRefreshedPattern'
  :: (DExt o o', DExt o' o'')
  => WithRefreshedPattern' e n i o o'
  -> WithRefreshedPattern' e i l o' o''
  -> WithRefreshedPattern' e n l o o''
compWithRefreshedPattern' :: forall (o :: S) (o' :: S) (o'' :: S) (e :: S -> *) (n :: S)
       (i :: S) (l :: S).
(DExt o o', DExt o' o'') =>
WithRefreshedPattern' e n i o o'
-> WithRefreshedPattern' e i l o' o''
-> WithRefreshedPattern' e n l o o''
compWithRefreshedPattern' (WithRefreshedPattern' (Name n -> e o) -> Name i -> e o'
f) (WithRefreshedPattern' (Name i -> e o') -> Name l -> e o''
g) =
  ((Name n -> e o) -> Name l -> e o'')
-> WithRefreshedPattern' e n l o o''
forall (e :: S -> *) (n :: S) (l :: S) (o :: S) (o' :: S).
((Name n -> e o) -> Name l -> e o')
-> WithRefreshedPattern' e n l o o'
WithRefreshedPattern' ((Name i -> e o') -> Name l -> e o''
g ((Name i -> e o') -> Name l -> e o'')
-> ((Name n -> e o) -> Name i -> e o')
-> (Name n -> e o)
-> Name l
-> e o''
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Name n -> e o) -> Name i -> e o'
f)

-- ** Extracting proofs from binders and patterns

-- | Evidence that scope @n@ contains distinct names.
data DistinctEvidence (n :: S) where
  Distinct :: Distinct n => DistinctEvidence n

-- | Evidence that scope @l@ extends scope @n@.
data ExtEvidence (n :: S) (l :: S) where
  Ext :: Ext n l => ExtEvidence n l

-- | A distinct scope extended with a 'NameBinder' is also distinct.
assertDistinct :: (Distinct n, CoSinkable pattern) => pattern n l -> DistinctEvidence l
assertDistinct :: forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct pattern n l
_ = DistinctEvidence l
forall (n :: S). DistinctEvidence n
unsafeDistinct

-- | A distinct scope extended with a 'NameBinder' is also distinct.
assertExt :: CoSinkable pattern => pattern n l -> ExtEvidence n l
assertExt :: forall (pattern :: S -> S -> *) (n :: S) (l :: S).
CoSinkable pattern =>
pattern n l -> ExtEvidence n l
assertExt pattern n l
_ = ExtEvidence n l
forall (n :: S) (l :: S). ExtEvidence n l
unsafeExt

-- | Unsafely declare that scope @n@ is distinct.
-- Used in 'unsafeAssertFresh'.
unsafeDistinct :: DistinctEvidence n
unsafeDistinct :: forall (n :: S). DistinctEvidence n
unsafeDistinct = DistinctEvidence 'VoidS -> DistinctEvidence n
forall a b. a -> b
unsafeCoerce (DistinctEvidence 'VoidS
forall (n :: S). Distinct n => DistinctEvidence n
Distinct :: DistinctEvidence VoidS)

-- | Unsafely declare that scope @l@ extends scope @n@.
-- Used in 'unsafeAssertFresh'.
unsafeExt :: ExtEvidence n l
unsafeExt :: forall (n :: S) (l :: S). ExtEvidence n l
unsafeExt = ExtEvidence 'VoidS 'VoidS -> ExtEvidence n l
forall a b. a -> b
unsafeCoerce (ExtEvidence 'VoidS 'VoidS
forall (n :: S) (l :: S). Ext n l => ExtEvidence n l
Ext :: ExtEvidence VoidS VoidS)

-- ** Unsinking names

-- | Try coercing the name back to the (smaller) scope,
-- given a binder that extends that scope.
unsinkName :: NameBinder n l -> Name l -> Maybe (Name n)
unsinkName :: forall (n :: S) (l :: S).
NameBinder n l -> Name l -> Maybe (Name n)
unsinkName NameBinder n l
binder name :: Name l
name@(UnsafeName RawName
raw)
  | NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder n l
binder Name l -> Name l -> Bool
forall a. Eq a => a -> a -> Bool
== Name l
name = Maybe (Name n)
forall a. Maybe a
Nothing
  | Bool
otherwise = Name n -> Maybe (Name n)
forall a. a -> Maybe a
Just (RawName -> Name n
forall (n :: S). RawName -> Name n
UnsafeName RawName
raw)

-- | Check if a name in the extended context
-- is introduced in a pattern or comes from the outer scope @n@.
--
-- This is a generalization of 'unsinkName'.
unsinkNamePattern
  :: forall pattern n l. (Distinct n, CoSinkable pattern)
  => pattern n l -> Name l -> Maybe (Name n)
unsinkNamePattern :: forall (pattern :: S -> S -> *) (n :: S) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Name l -> Maybe (Name n)
unsinkNamePattern pattern n l
pat = forall (pattern :: S -> S -> *) (o :: S)
       (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
(CoSinkable pattern, Distinct o) =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
withPattern @_ @n
  (\Scope z
_scope' NameBinder x y
binder forall (z' :: S).
DExt z z' =>
UnsinkName x y z z' -> NameBinder z z' -> r'
k ->
      NameBinder x y -> (DExt z Any => NameBinder z Any -> r') -> r'
forall (n :: S) (l :: S) (n' :: S) (l' :: S) r.
NameBinder n l -> (DExt n' l' => NameBinder n' l' -> r) -> r
unsafeAssertFresh NameBinder x y
binder ((DExt z Any => NameBinder z Any -> r') -> r')
-> (DExt z Any => NameBinder z Any -> r') -> r'
forall a b. (a -> b) -> a -> b
$ \NameBinder z Any
binder' ->
        UnsinkName x y z Any -> NameBinder z Any -> r'
forall (z' :: S).
DExt z z' =>
UnsinkName x y z z' -> NameBinder z z' -> r'
k ((Name y -> Maybe (Name x)) -> UnsinkName x y z Any
forall (n :: S) (l :: S) (o :: S) (o' :: S).
(Name l -> Maybe (Name n)) -> UnsinkName n l o o'
UnsinkName (NameBinder x y -> Name y -> Maybe (Name x)
forall (n :: S) (l :: S).
NameBinder n l -> Name l -> Maybe (Name n)
unsinkName NameBinder x y
binder)) NameBinder z Any
binder')
  UnsinkName x x z z'
forall (n :: S) (o :: S) (o' :: S). UnsinkName n n o o'
forall (x :: S) (z :: S) (z' :: S).
DExt z z' =>
UnsinkName x x z z'
idUnsinkName
  UnsinkName x y z z'
-> UnsinkName y y' z' z'' -> UnsinkName x y' z z''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
UnsinkName x y z z'
-> UnsinkName y y' z' z'' -> UnsinkName x y' z z''
forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S).
UnsinkName n i o o'
-> UnsinkName i l o' o'' -> UnsinkName n l o o''
compUnsinkName
  (String -> Scope n
forall a. HasCallStack => String -> a
error String
"impossible")  -- scope is not used, but has to be provided in general
  pattern n l
pat
  (\(UnsinkName Name l -> Maybe (Name n)
unsink) pattern n o'
_ -> Name l -> Maybe (Name n)
unsink)

-- | Auxiliary structure for unsinking names.
-- Used in 'unsinkNamePattern'.
newtype UnsinkName n l (o :: S) (o' :: S) = UnsinkName (Name l -> Maybe (Name n))

-- | Trivial unsinking. If no scope extension took place, any name is free (since it cannot be bound by anything).
idUnsinkName :: UnsinkName n n o o'
idUnsinkName :: forall (n :: S) (o :: S) (o' :: S). UnsinkName n n o o'
idUnsinkName = (Name n -> Maybe (Name n)) -> UnsinkName n n o o'
forall (n :: S) (l :: S) (o :: S) (o' :: S).
(Name l -> Maybe (Name n)) -> UnsinkName n l o o'
UnsinkName Name n -> Maybe (Name n)
forall a. a -> Maybe a
Just

-- | Composition of unsinking for nested binders/patterns.
compUnsinkName
  :: UnsinkName n i o o'
  -> UnsinkName i l o' o''
  -> UnsinkName n l o o''
compUnsinkName :: forall (n :: S) (i :: S) (o :: S) (o' :: S) (l :: S) (o'' :: S).
UnsinkName n i o o'
-> UnsinkName i l o' o'' -> UnsinkName n l o o''
compUnsinkName (UnsinkName Name i -> Maybe (Name n)
f) (UnsinkName Name l -> Maybe (Name i)
g)
  = (Name l -> Maybe (Name n)) -> UnsinkName n l o o''
forall (n :: S) (l :: S) (o :: S) (o' :: S).
(Name l -> Maybe (Name n)) -> UnsinkName n l o o'
UnsinkName (\Name l
name -> Name l -> Maybe (Name i)
g Name l
name Maybe (Name i) -> (Name i -> Maybe (Name n)) -> Maybe (Name n)
forall a b. Maybe a -> (a -> Maybe b) -> Maybe b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Name i -> Maybe (Name n)
f)

-- * Unification of binders

-- | Unification result for two binders,
-- extending some common scope to scopes @l@ and @r@ respectively.
--
-- Due to the implementation of the foil, we can often rename binders efficiently,
-- by renaming binders only in one of the two unified terms.
data UnifyNameBinders (pattern :: S -> S -> Type) n l r where
  -- | Binders are the same, proving that type parameters @l@ and @r@
  -- are in fact equivalent.
  SameNameBinders
    :: NameBinders n l  -- ^ /Unordered/ set of binders in the unified pattern (from any of the original patterns).
    -> UnifyNameBinders pattern n l l
  -- | It is possible to safely rename the left binder
  -- to match the right one.
  RenameLeftNameBinder
    :: NameBinders n r                    -- ^ /Unordered/ set of binders in the unified pattern (the binders from the right pattern).
    -> (NameBinder n l -> NameBinder n r) -- ^ Binder renaming for the left pattern.
    -> UnifyNameBinders pattern n l r
  -- | It is possible to safely rename the right binder
  -- to match the left one.
  RenameRightNameBinder
    :: NameBinders n l                    -- ^ /Unordered/ set of binders in the unified pattern (the binders from the left pattern).
    -> (NameBinder n r -> NameBinder n l) -- ^ Binder renaming for the right pattern.
    -> UnifyNameBinders pattern n l r
  -- | It is necessary to rename both binders.
  RenameBothBinders
    :: NameBinders n lr                     -- ^ /Unordered/ set of binders in the unified pattern
    -> (NameBinder n l -> NameBinder n lr)  -- ^ Binder renaming for the left pattern.
    -> (NameBinder n r -> NameBinder n lr)  -- ^ Binder renaming for the right pattern.
    -> UnifyNameBinders pattern n l r
  -- | Cannot unify to (sub)patterns.
  NotUnifiable :: UnifyNameBinders pattern n l r

-- | Unify binders either by asserting that they are the same,
-- or by providing a /safe/ renaming function to convert one binder to another.
unifyNameBinders
  :: forall i l r pattern. Distinct i
  => NameBinder i l -- ^ Left pattern.
  -> NameBinder i r -- ^ Right pattern.
  -> UnifyNameBinders pattern i l r
unifyNameBinders :: forall (i :: S) (l :: S) (r :: S) (pattern :: S -> S -> *).
Distinct i =>
NameBinder i l -> NameBinder i r -> UnifyNameBinders pattern i l r
unifyNameBinders l :: NameBinder i l
l@(UnsafeNameBinder (UnsafeName RawName
i1)) r :: NameBinder i r
r@(UnsafeNameBinder (UnsafeName RawName
i2))
  | RawName
i1 RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName
i2  = case NameBinder i l -> DistinctEvidence l
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> DistinctEvidence l
assertDistinct NameBinder i l
l of
      DistinctEvidence l
Distinct -> UnifyNameBinders Any i l l -> UnifyNameBinders pattern i l r
forall a b. a -> b
unsafeCoerce (NameBinders i l -> UnifyNameBinders Any i l l
forall (n :: S) (l :: S) (pattern :: S -> S -> *).
NameBinders n l -> UnifyNameBinders pattern n l l
SameNameBinders (NameBinder i l -> NameBinders i l
forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l
nameBindersSingleton NameBinder i l
l))  -- equal names extend scopes equally
  | RawName
i1 RawName -> RawName -> Bool
forall a. Ord a => a -> a -> Bool
< RawName
i2   = NameBinders i l
-> (NameBinder i r -> NameBinder i l)
-> UnifyNameBinders pattern i l r
forall (n :: S) (l :: S) (r :: S) (pattern :: S -> S -> *).
NameBinders n l
-> (NameBinder n r -> NameBinder n l)
-> UnifyNameBinders pattern n l r
RenameRightNameBinder (NameBinder i l -> NameBinders i l
forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l
nameBindersSingleton NameBinder i l
l) ((NameBinder i r -> NameBinder i l)
 -> UnifyNameBinders pattern i l r)
-> (NameBinder i r -> NameBinder i l)
-> UnifyNameBinders pattern i l r
forall a b. (a -> b) -> a -> b
$ \(UnsafeNameBinder (UnsafeName RawName
i'')) ->
      if RawName
i'' RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName
i2 then Name l -> NameBinder i l
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder (RawName -> Name l
forall (n :: S). RawName -> Name n
UnsafeName RawName
i1) else Name l -> NameBinder i l
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder (RawName -> Name l
forall (n :: S). RawName -> Name n
UnsafeName RawName
i'')
  | Bool
otherwise = NameBinders i r
-> (NameBinder i l -> NameBinder i r)
-> UnifyNameBinders pattern i l r
forall (n :: S) (r :: S) (l :: S) (pattern :: S -> S -> *).
NameBinders n r
-> (NameBinder n l -> NameBinder n r)
-> UnifyNameBinders pattern n l r
RenameLeftNameBinder (NameBinder i r -> NameBinders i r
forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l
nameBindersSingleton NameBinder i r
r) ((NameBinder i l -> NameBinder i r)
 -> UnifyNameBinders pattern i l r)
-> (NameBinder i l -> NameBinder i r)
-> UnifyNameBinders pattern i l r
forall a b. (a -> b) -> a -> b
$ \(UnsafeNameBinder (UnsafeName RawName
i')) ->
      if RawName
i'  RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName
i1 then Name r -> NameBinder i r
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder (RawName -> Name r
forall (n :: S). RawName -> Name n
UnsafeName RawName
i2) else Name r -> NameBinder i r
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder (RawName -> Name r
forall (n :: S). RawName -> Name n
UnsafeName RawName
i')

-- | Unsafely merge results of unification for nested binders/patterns.
-- Used in 'andThenUnifyPatterns'.
unsafeMergeUnifyBinders :: UnifyNameBinders pattern a a' a'' -> UnifyNameBinders pattern a''' b' b'' -> UnifyNameBinders pattern a b' b''
unsafeMergeUnifyBinders :: forall (pattern :: S -> S -> *) (a :: S) (a' :: S) (a'' :: S)
       (a''' :: S) (b' :: S) (b'' :: S).
UnifyNameBinders pattern a a' a''
-> UnifyNameBinders pattern a''' b' b''
-> UnifyNameBinders pattern a b' b''
unsafeMergeUnifyBinders = \case

  SameNameBinders NameBinders a a'
x -> \case
    SameNameBinders NameBinders a''' b'
y -> NameBinders a b' -> UnifyNameBinders pattern a b' b'
forall (n :: S) (l :: S) (pattern :: S -> S -> *).
NameBinders n l -> UnifyNameBinders pattern n l l
SameNameBinders (NameBinders a a'
x NameBinders a a' -> NameBinders a''' b' -> NameBinders a b'
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b'
y)
    RenameLeftNameBinder NameBinders a''' b''
y NameBinder a''' b' -> NameBinder a''' b''
f -> NameBinders a b''
-> (NameBinder a b' -> NameBinder a b'')
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (r :: S) (l :: S) (pattern :: S -> S -> *).
NameBinders n r
-> (NameBinder n l -> NameBinder n r)
-> UnifyNameBinders pattern n l r
RenameLeftNameBinder (NameBinders a a'
x NameBinders a a' -> NameBinders a''' b'' -> NameBinders a b''
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b''
y) ((NameBinder a''' b' -> NameBinder a''' b'')
-> NameBinder a b' -> NameBinder a b''
forall a b. a -> b
unsafeCoerce NameBinder a''' b' -> NameBinder a''' b''
f)
    RenameRightNameBinder NameBinders a''' b'
y NameBinder a''' b'' -> NameBinder a''' b'
g -> NameBinders a b'
-> (NameBinder a b'' -> NameBinder a b')
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (l :: S) (r :: S) (pattern :: S -> S -> *).
NameBinders n l
-> (NameBinder n r -> NameBinder n l)
-> UnifyNameBinders pattern n l r
RenameRightNameBinder (NameBinders a a'
x NameBinders a a' -> NameBinders a''' b' -> NameBinders a b'
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b'
y) ((NameBinder a''' b'' -> NameBinder a''' b')
-> NameBinder a b'' -> NameBinder a b'
forall a b. a -> b
unsafeCoerce NameBinder a''' b'' -> NameBinder a''' b'
g)
    RenameBothBinders NameBinders a''' lr
y NameBinder a''' b' -> NameBinder a''' lr
f NameBinder a''' b'' -> NameBinder a''' lr
g -> NameBinders a Any
-> (NameBinder a b' -> NameBinder a Any)
-> (NameBinder a b'' -> NameBinder a Any)
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (i :: S) (l :: S) (r :: S)
       (pattern :: S -> S -> *).
NameBinders n i
-> (NameBinder n l -> NameBinder n i)
-> (NameBinder n r -> NameBinder n i)
-> UnifyNameBinders pattern n l r
RenameBothBinders (NameBinders a a'
x NameBinders a a' -> NameBinders a''' lr -> NameBinders a Any
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' lr
y) ((NameBinder a''' b' -> NameBinder a''' lr)
-> NameBinder a b' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b' -> NameBinder a''' lr
f) ((NameBinder a''' b'' -> NameBinder a''' lr)
-> NameBinder a b'' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b'' -> NameBinder a''' lr
g)
    UnifyNameBinders pattern a''' b' b''
NotUnifiable -> UnifyNameBinders pattern a b' b''
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
UnifyNameBinders pattern n l r
NotUnifiable

  RenameLeftNameBinder NameBinders a a''
x NameBinder a a' -> NameBinder a a''
f -> \case
    SameNameBinders NameBinders a''' b'
y -> NameBinders a b''
-> (NameBinder a b' -> NameBinder a b'')
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (r :: S) (l :: S) (pattern :: S -> S -> *).
NameBinders n r
-> (NameBinder n l -> NameBinder n r)
-> UnifyNameBinders pattern n l r
RenameLeftNameBinder (NameBinders a a''
x NameBinders a a'' -> NameBinders a''' b' -> NameBinders a b''
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b'
y) ((NameBinder a a' -> NameBinder a a'')
-> NameBinder a b' -> NameBinder a b''
forall a b. a -> b
unsafeCoerce NameBinder a a' -> NameBinder a a''
f)
    RenameLeftNameBinder NameBinders a''' b''
y NameBinder a''' b' -> NameBinder a''' b''
g -> NameBinders a b''
-> (NameBinder a b' -> NameBinder a b'')
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (r :: S) (l :: S) (pattern :: S -> S -> *).
NameBinders n r
-> (NameBinder n l -> NameBinder n r)
-> UnifyNameBinders pattern n l r
RenameLeftNameBinder (NameBinders a a''
x NameBinders a a'' -> NameBinders a''' b'' -> NameBinders a b''
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b''
y) ((NameBinder a a' -> NameBinder a a'') -> Any -> NameBinder a b''
forall a b. a -> b
unsafeCoerce NameBinder a a' -> NameBinder a a''
f (Any -> NameBinder a b'')
-> (NameBinder a b' -> Any) -> NameBinder a b' -> NameBinder a b''
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameBinder a''' b' -> NameBinder a''' b'')
-> NameBinder a b' -> Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b' -> NameBinder a''' b''
g)
    RenameRightNameBinder NameBinders a''' b'
y NameBinder a''' b'' -> NameBinder a''' b'
g -> NameBinders a Any
-> (NameBinder a b' -> NameBinder a Any)
-> (NameBinder a b'' -> NameBinder a Any)
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (i :: S) (l :: S) (r :: S)
       (pattern :: S -> S -> *).
NameBinders n i
-> (NameBinder n l -> NameBinder n i)
-> (NameBinder n r -> NameBinder n i)
-> UnifyNameBinders pattern n l r
RenameBothBinders (NameBinders a a''
x NameBinders a a'' -> NameBinders a''' b' -> NameBinders a Any
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b'
y) ((NameBinder a a' -> NameBinder a a'')
-> NameBinder a b' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a' -> NameBinder a a''
f) ((NameBinder a''' b'' -> NameBinder a''' b')
-> NameBinder a b'' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b'' -> NameBinder a''' b'
g)
    RenameBothBinders NameBinders a''' lr
y NameBinder a''' b' -> NameBinder a''' lr
f' NameBinder a''' b'' -> NameBinder a''' lr
g -> NameBinders a Any
-> (NameBinder a b' -> NameBinder a Any)
-> (NameBinder a b'' -> NameBinder a Any)
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (i :: S) (l :: S) (r :: S)
       (pattern :: S -> S -> *).
NameBinders n i
-> (NameBinder n l -> NameBinder n i)
-> (NameBinder n r -> NameBinder n i)
-> UnifyNameBinders pattern n l r
RenameBothBinders (NameBinders a a''
x NameBinders a a'' -> NameBinders a''' lr -> NameBinders a Any
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' lr
y) ((NameBinder a a' -> NameBinder a a'') -> Any -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a' -> NameBinder a a''
f (Any -> NameBinder a Any)
-> (NameBinder a b' -> Any) -> NameBinder a b' -> NameBinder a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameBinder a''' b' -> NameBinder a''' lr)
-> NameBinder a b' -> Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b' -> NameBinder a''' lr
f') ((NameBinder a''' b'' -> NameBinder a''' lr)
-> NameBinder a b'' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b'' -> NameBinder a''' lr
g)
    UnifyNameBinders pattern a''' b' b''
NotUnifiable -> UnifyNameBinders pattern a b' b''
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
UnifyNameBinders pattern n l r
NotUnifiable

  RenameRightNameBinder NameBinders a a'
x NameBinder a a'' -> NameBinder a a'
g -> \case
    SameNameBinders NameBinders a''' b'
y -> NameBinders a b'
-> (NameBinder a b'' -> NameBinder a b')
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (l :: S) (r :: S) (pattern :: S -> S -> *).
NameBinders n l
-> (NameBinder n r -> NameBinder n l)
-> UnifyNameBinders pattern n l r
RenameRightNameBinder (NameBinders a a'
x NameBinders a a' -> NameBinders a''' b' -> NameBinders a b'
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b'
y) ((NameBinder a a'' -> NameBinder a a')
-> NameBinder a b'' -> NameBinder a b'
forall a b. a -> b
unsafeCoerce NameBinder a a'' -> NameBinder a a'
g)
    RenameLeftNameBinder NameBinders a''' b''
y NameBinder a''' b' -> NameBinder a''' b''
f -> NameBinders a Any
-> (NameBinder a b' -> NameBinder a Any)
-> (NameBinder a b'' -> NameBinder a Any)
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (i :: S) (l :: S) (r :: S)
       (pattern :: S -> S -> *).
NameBinders n i
-> (NameBinder n l -> NameBinder n i)
-> (NameBinder n r -> NameBinder n i)
-> UnifyNameBinders pattern n l r
RenameBothBinders (NameBinders a a'
x NameBinders a a' -> NameBinders a''' b'' -> NameBinders a Any
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b''
y) ((NameBinder a''' b' -> NameBinder a''' b'')
-> NameBinder a b' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b' -> NameBinder a''' b''
f) ((NameBinder a a'' -> NameBinder a a')
-> NameBinder a b'' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a'' -> NameBinder a a'
g)
    RenameRightNameBinder NameBinders a''' b'
y NameBinder a''' b'' -> NameBinder a''' b'
g' -> NameBinders a b'
-> (NameBinder a b'' -> NameBinder a b')
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (l :: S) (r :: S) (pattern :: S -> S -> *).
NameBinders n l
-> (NameBinder n r -> NameBinder n l)
-> UnifyNameBinders pattern n l r
RenameRightNameBinder (NameBinders a a'
x NameBinders a a' -> NameBinders a''' b' -> NameBinders a b'
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b'
y) ((NameBinder a a'' -> NameBinder a a') -> Any -> NameBinder a b'
forall a b. a -> b
unsafeCoerce NameBinder a a'' -> NameBinder a a'
g (Any -> NameBinder a b')
-> (NameBinder a b'' -> Any) -> NameBinder a b'' -> NameBinder a b'
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameBinder a''' b'' -> NameBinder a''' b')
-> NameBinder a b'' -> Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b'' -> NameBinder a''' b'
g')
    RenameBothBinders NameBinders a''' lr
y NameBinder a''' b' -> NameBinder a''' lr
f NameBinder a''' b'' -> NameBinder a''' lr
g' -> NameBinders a Any
-> (NameBinder a b' -> NameBinder a Any)
-> (NameBinder a b'' -> NameBinder a Any)
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (i :: S) (l :: S) (r :: S)
       (pattern :: S -> S -> *).
NameBinders n i
-> (NameBinder n l -> NameBinder n i)
-> (NameBinder n r -> NameBinder n i)
-> UnifyNameBinders pattern n l r
RenameBothBinders (NameBinders a a'
x NameBinders a a' -> NameBinders a''' lr -> NameBinders a Any
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' lr
y) ((NameBinder a''' b' -> NameBinder a''' lr)
-> NameBinder a b' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b' -> NameBinder a''' lr
f) ((NameBinder a a'' -> NameBinder a a') -> Any -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a'' -> NameBinder a a'
g (Any -> NameBinder a Any)
-> (NameBinder a b'' -> Any)
-> NameBinder a b''
-> NameBinder a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameBinder a''' b'' -> NameBinder a''' lr)
-> NameBinder a b'' -> Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b'' -> NameBinder a''' lr
g')
    UnifyNameBinders pattern a''' b' b''
NotUnifiable -> UnifyNameBinders pattern a b' b''
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
UnifyNameBinders pattern n l r
NotUnifiable

  RenameBothBinders NameBinders a lr
x NameBinder a a' -> NameBinder a lr
f NameBinder a a'' -> NameBinder a lr
g -> \case
    SameNameBinders NameBinders a''' b'
y -> NameBinders a Any
-> (NameBinder a b' -> NameBinder a Any)
-> (NameBinder a b'' -> NameBinder a Any)
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (i :: S) (l :: S) (r :: S)
       (pattern :: S -> S -> *).
NameBinders n i
-> (NameBinder n l -> NameBinder n i)
-> (NameBinder n r -> NameBinder n i)
-> UnifyNameBinders pattern n l r
RenameBothBinders (NameBinders a lr
x NameBinders a lr -> NameBinders a''' b' -> NameBinders a Any
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b'
y) ((NameBinder a a' -> NameBinder a lr)
-> NameBinder a b' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a' -> NameBinder a lr
f) ((NameBinder a a'' -> NameBinder a lr)
-> NameBinder a b'' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a'' -> NameBinder a lr
g)
    RenameLeftNameBinder NameBinders a''' b''
y NameBinder a''' b' -> NameBinder a''' b''
f' -> NameBinders a Any
-> (NameBinder a b' -> NameBinder a Any)
-> (NameBinder a b'' -> NameBinder a Any)
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (i :: S) (l :: S) (r :: S)
       (pattern :: S -> S -> *).
NameBinders n i
-> (NameBinder n l -> NameBinder n i)
-> (NameBinder n r -> NameBinder n i)
-> UnifyNameBinders pattern n l r
RenameBothBinders (NameBinders a lr
x NameBinders a lr -> NameBinders a''' b'' -> NameBinders a Any
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b''
y) ((NameBinder a a' -> NameBinder a lr) -> Any -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a' -> NameBinder a lr
f (Any -> NameBinder a Any)
-> (NameBinder a b' -> Any) -> NameBinder a b' -> NameBinder a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameBinder a''' b' -> NameBinder a''' b'')
-> NameBinder a b' -> Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b' -> NameBinder a''' b''
f') ((NameBinder a a'' -> NameBinder a lr)
-> NameBinder a b'' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a'' -> NameBinder a lr
g)
    RenameRightNameBinder NameBinders a''' b'
y NameBinder a''' b'' -> NameBinder a''' b'
g' -> NameBinders a Any
-> (NameBinder a b' -> NameBinder a Any)
-> (NameBinder a b'' -> NameBinder a Any)
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (i :: S) (l :: S) (r :: S)
       (pattern :: S -> S -> *).
NameBinders n i
-> (NameBinder n l -> NameBinder n i)
-> (NameBinder n r -> NameBinder n i)
-> UnifyNameBinders pattern n l r
RenameBothBinders (NameBinders a lr
x NameBinders a lr -> NameBinders a''' b' -> NameBinders a Any
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' b'
y) ((NameBinder a a' -> NameBinder a lr)
-> NameBinder a b' -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a' -> NameBinder a lr
f) ((NameBinder a a'' -> NameBinder a lr) -> Any -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a'' -> NameBinder a lr
g (Any -> NameBinder a Any)
-> (NameBinder a b'' -> Any)
-> NameBinder a b''
-> NameBinder a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameBinder a''' b'' -> NameBinder a''' b')
-> NameBinder a b'' -> Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b'' -> NameBinder a''' b'
g')
    RenameBothBinders NameBinders a''' lr
y NameBinder a''' b' -> NameBinder a''' lr
f' NameBinder a''' b'' -> NameBinder a''' lr
g' -> NameBinders a Any
-> (NameBinder a b' -> NameBinder a Any)
-> (NameBinder a b'' -> NameBinder a Any)
-> UnifyNameBinders pattern a b' b''
forall (n :: S) (i :: S) (l :: S) (r :: S)
       (pattern :: S -> S -> *).
NameBinders n i
-> (NameBinder n l -> NameBinder n i)
-> (NameBinder n r -> NameBinder n i)
-> UnifyNameBinders pattern n l r
RenameBothBinders (NameBinders a lr
x NameBinders a lr -> NameBinders a''' lr -> NameBinders a Any
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
`unsafeMergeNameBinders` NameBinders a''' lr
y) ((NameBinder a a' -> NameBinder a lr) -> Any -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a' -> NameBinder a lr
f (Any -> NameBinder a Any)
-> (NameBinder a b' -> Any) -> NameBinder a b' -> NameBinder a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameBinder a''' b' -> NameBinder a''' lr)
-> NameBinder a b' -> Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b' -> NameBinder a''' lr
f') ((NameBinder a a'' -> NameBinder a lr) -> Any -> NameBinder a Any
forall a b. a -> b
unsafeCoerce NameBinder a a'' -> NameBinder a lr
g (Any -> NameBinder a Any)
-> (NameBinder a b'' -> Any)
-> NameBinder a b''
-> NameBinder a Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (NameBinder a''' b'' -> NameBinder a''' lr)
-> NameBinder a b'' -> Any
forall a b. a -> b
unsafeCoerce NameBinder a''' b'' -> NameBinder a''' lr
g')
    UnifyNameBinders pattern a''' b' b''
NotUnifiable -> UnifyNameBinders pattern a b' b''
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
UnifyNameBinders pattern n l r
NotUnifiable

  UnifyNameBinders pattern a a' a''
NotUnifiable -> UnifyNameBinders pattern a b' b''
-> UnifyNameBinders pattern a''' b' b''
-> UnifyNameBinders pattern a b' b''
forall a b. a -> b -> a
const (UnifyNameBinders pattern a b' b''
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
UnifyNameBinders pattern n l r
NotUnifiable)

-- | Chain unification of nested patterns.
andThenUnifyPatterns
  :: (UnifiablePattern pattern, Distinct l, Distinct l')
  => UnifyNameBinders pattern n l l'    -- ^ Unifying action for some outer patterns.
  -> (pattern l r, pattern l' r')       -- ^ Two nested patterns (cannot be unified directly since they extend different scopes).
  -> UnifyNameBinders pattern n r r'
andThenUnifyPatterns :: forall (pattern :: S -> S -> *) (l :: S) (l' :: S) (n :: S)
       (r :: S) (r' :: S).
(UnifiablePattern pattern, Distinct l, Distinct l') =>
UnifyNameBinders pattern n l l'
-> (pattern l r, pattern l' r') -> UnifyNameBinders pattern n r r'
andThenUnifyPatterns UnifyNameBinders pattern n l l'
u (pattern l r
l, pattern l' r'
r) = UnifyNameBinders pattern n l l'
-> UnifyNameBinders pattern l' r r'
-> UnifyNameBinders pattern n r r'
forall (pattern :: S -> S -> *) (a :: S) (a' :: S) (a'' :: S)
       (a''' :: S) (b' :: S) (b'' :: S).
UnifyNameBinders pattern a a' a''
-> UnifyNameBinders pattern a''' b' b''
-> UnifyNameBinders pattern a b' b''
unsafeMergeUnifyBinders UnifyNameBinders pattern n l l'
u (pattern l' r -> pattern l' r' -> UnifyNameBinders pattern l' r r'
forall (n :: S) (l :: S) (r :: S).
Distinct n =>
pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
unifyPatterns (pattern l r -> pattern l' r
forall a b. a -> b
unsafeCoerce pattern l r
l) pattern l' r'
r)

-- | Chain unification of nested patterns with 'NameBinder's.
andThenUnifyNameBinders
  :: (UnifiablePattern pattern, Distinct l, Distinct l')
  => UnifyNameBinders pattern n l l'    -- ^ Unifying action for some outer patterns.
  -> (NameBinder l r, NameBinder l' r') -- ^ Two nested binders (cannot be unified directly since they extend different scopes).
  -> UnifyNameBinders pattern n r r'
andThenUnifyNameBinders :: forall (pattern :: S -> S -> *) (l :: S) (l' :: S) (n :: S)
       (r :: S) (r' :: S).
(UnifiablePattern pattern, Distinct l, Distinct l') =>
UnifyNameBinders pattern n l l'
-> (NameBinder l r, NameBinder l' r')
-> UnifyNameBinders pattern n r r'
andThenUnifyNameBinders UnifyNameBinders pattern n l l'
u (NameBinder l r
l, NameBinder l' r'
r) = UnifyNameBinders pattern n l l'
-> UnifyNameBinders pattern l' r r'
-> UnifyNameBinders pattern n r r'
forall (pattern :: S -> S -> *) (a :: S) (a' :: S) (a'' :: S)
       (a''' :: S) (b' :: S) (b'' :: S).
UnifyNameBinders pattern a a' a''
-> UnifyNameBinders pattern a''' b' b''
-> UnifyNameBinders pattern a b' b''
unsafeMergeUnifyBinders UnifyNameBinders pattern n l l'
u (NameBinder l' r
-> NameBinder l' r' -> UnifyNameBinders pattern l' r r'
forall (i :: S) (l :: S) (r :: S) (pattern :: S -> S -> *).
Distinct i =>
NameBinder i l -> NameBinder i r -> UnifyNameBinders pattern i l r
unifyNameBinders (NameBinder l r -> NameBinder l' r
forall a b. a -> b
unsafeCoerce NameBinder l r
l) NameBinder l' r'
r)

-- | An /unordered/ collection of 'NameBinder's, that together extend scope @n@ to scope @l@.
--
-- For an ordered version see 'NameBinderList'.
newtype NameBinders (n :: S) (l :: S) = UnsafeNameBinders IntSet

-- | /Unsafely/ merge sets of binders (via set union).
unsafeMergeNameBinders :: NameBinders a b -> NameBinders c d -> NameBinders n l
unsafeMergeNameBinders :: forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
unsafeMergeNameBinders (UnsafeNameBinders RawScope
x) (UnsafeNameBinders RawScope
y) = RawScope -> NameBinders n l
forall (n :: S) (l :: S). RawScope -> NameBinders n l
UnsafeNameBinders (RawScope
x RawScope -> RawScope -> RawScope
forall a. Semigroup a => a -> a -> a
<> RawScope
y)

-- | An empty set of binders keeps the scope as is.
emptyNameBinders :: NameBinders n n
emptyNameBinders :: forall (n :: S). NameBinders n n
emptyNameBinders = RawScope -> NameBinders n n
forall (n :: S) (l :: S). RawScope -> NameBinders n l
UnsafeNameBinders RawScope
IntSet.empty

-- | Composition of sets of binders.
mergeNameBinders :: NameBinders n i -> NameBinders i l -> NameBinders n l
mergeNameBinders :: forall (n :: S) (i :: S) (l :: S).
NameBinders n i -> NameBinders i l -> NameBinders n l
mergeNameBinders = NameBinders n i -> NameBinders i l -> NameBinders n l
forall (a :: S) (b :: S) (c :: S) (d :: S) (n :: S) (l :: S).
NameBinders a b -> NameBinders c d -> NameBinders n l
unsafeMergeNameBinders

-- | A singleton name binder set.
nameBindersSingleton :: NameBinder n l -> NameBinders n l
nameBindersSingleton :: forall (n :: S) (l :: S). NameBinder n l -> NameBinders n l
nameBindersSingleton NameBinder n l
binder = RawScope -> NameBinders n l
forall (n :: S) (l :: S). RawScope -> NameBinders n l
UnsafeNameBinders (RawName -> RawScope
IntSet.singleton (Name l -> RawName
forall (l :: S). Name l -> RawName
nameId (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder n l
binder)))

-- | An /ordered/ collection (list) of 'NameBinder's, that together extend scope @n@ to scope @l@.
--
-- For an unordered version see 'NameBinders'.
data NameBinderList n l where
  -- | An empty list of binders keeps the scope as is.
  NameBinderListEmpty :: NameBinderList n n
  -- | A non-empty list of binders.
  NameBinderListCons
    :: NameBinder n i       -- ^ Outermost binder.
    -> NameBinderList i l   -- ^ Remaining list of binders.
    -> NameBinderList n l

-- | Convert an unordered set of name binders into an ordered list (with some order).
nameBindersList :: NameBinders n l -> NameBinderList n l
nameBindersList :: forall (n :: S) (l :: S). NameBinders n l -> NameBinderList n l
nameBindersList (UnsafeNameBinders RawScope
names) = [RawName] -> NameBinderList n l
forall {i :: S} {l :: S}. [RawName] -> NameBinderList i l
go (RawScope -> [RawName]
IntSet.toList RawScope
names)
  where
    go :: [RawName] -> NameBinderList i l
go []     = NameBinderList Any Any -> NameBinderList i l
forall a b. a -> b
unsafeCoerce NameBinderList Any Any
forall (n :: S). NameBinderList n n
NameBinderListEmpty
    go (RawName
x:[RawName]
xs) = NameBinder i i -> NameBinderList i l -> NameBinderList i l
forall (n :: S) (i :: S) (l :: S).
NameBinder n i -> NameBinderList i l -> NameBinderList n l
NameBinderListCons (Name i -> NameBinder i i
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder (RawName -> Name i
forall (n :: S). RawName -> Name n
UnsafeName RawName
x)) ([RawName] -> NameBinderList i l
go [RawName]
xs)

-- | Convert an ordered list of name binders into an unordered set.
fromNameBindersList :: NameBinderList n l -> NameBinders n l
fromNameBindersList :: forall (n :: S) (l :: S). NameBinderList n l -> NameBinders n l
fromNameBindersList = RawScope -> NameBinders n l
forall (n :: S) (l :: S). RawScope -> NameBinders n l
UnsafeNameBinders (RawScope -> NameBinders n l)
-> (NameBinderList n l -> RawScope)
-> NameBinderList n l
-> NameBinders n l
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [RawName] -> RawScope
IntSet.fromList ([RawName] -> RawScope)
-> (NameBinderList n l -> [RawName])
-> NameBinderList n l
-> RawScope
forall b c a. (b -> c) -> (a -> b) -> a -> c
. NameBinderList n l -> [RawName]
forall (n :: S) (l :: S). NameBinderList n l -> [RawName]
go
  where
    go :: NameBinderList n l -> [RawName]
    go :: forall (n :: S) (l :: S). NameBinderList n l -> [RawName]
go NameBinderList n l
NameBinderListEmpty                 = []
    go (NameBinderListCons NameBinder n i
binder NameBinderList i l
binders) = Name i -> RawName
forall (l :: S). Name l -> RawName
nameId (NameBinder n i -> Name i
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder n i
binder) RawName -> [RawName] -> [RawName]
forall a. a -> [a] -> [a]
: NameBinderList i l -> [RawName]
forall (n :: S) (l :: S). NameBinderList n l -> [RawName]
go NameBinderList i l
binders

instance CoSinkable NameBinders where
  coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> NameBinders n l
-> (forall (l' :: S).
    (Name l -> Name l') -> NameBinders n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
_rename (UnsafeNameBinders RawScope
names) forall (l' :: S). (Name l -> Name l') -> NameBinders n' l' -> r
cont =
    (Name l -> Name Any) -> NameBinders n' Any -> r
forall (l' :: S). (Name l -> Name l') -> NameBinders n' l' -> r
cont Name l -> Name Any
forall a b. a -> b
unsafeCoerce (RawScope -> NameBinders n' Any
forall (n :: S) (l :: S). RawScope -> NameBinders n l
UnsafeNameBinders RawScope
names)

  withPattern :: forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> NameBinders n l
-> (forall (o' :: S).
    DExt o o' =>
    f n l o o' -> NameBinders o o' -> r)
-> r
withPattern forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withBinder forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
unit forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
comp Scope o
scope NameBinders n l
binders forall (o' :: S). DExt o o' => f n l o o' -> NameBinders o o' -> r
cont =
    (forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> NameBinderList n l
-> (forall {o' :: S}.
    DExt o o' =>
    f n l o o' -> NameBinderList o o' -> r)
-> r
forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> NameBinderList n l
-> (forall (o' :: S).
    DExt o o' =>
    f n l o o' -> NameBinderList o o' -> r)
-> r
forall (pattern :: S -> S -> *) (o :: S)
       (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
(CoSinkable pattern, Distinct o) =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
withPattern Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withBinder f x x z z'
forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
unit f x y z z' -> f y y' z' z'' -> f x y' z z''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
comp Scope o
scope (NameBinders n l -> NameBinderList n l
forall (n :: S) (l :: S). NameBinders n l -> NameBinderList n l
nameBindersList NameBinders n l
binders) ((forall {o' :: S}.
  DExt o o' =>
  f n l o o' -> NameBinderList o o' -> r)
 -> r)
-> (forall {o' :: S}.
    DExt o o' =>
    f n l o o' -> NameBinderList o o' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \f n l o o'
f NameBinderList o o'
binders' ->
      f n l o o' -> NameBinders o o' -> r
forall (o' :: S). DExt o o' => f n l o o' -> NameBinders o o' -> r
cont f n l o o'
f (NameBinderList o o' -> NameBinders o o'
forall (n :: S) (l :: S). NameBinderList n l -> NameBinders n l
fromNameBindersList NameBinderList o o'
binders')

instance CoSinkable NameBinderList where
  coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> NameBinderList n l
-> (forall (l' :: S).
    (Name l -> Name l') -> NameBinderList n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
rename NameBinderList n l
NameBinderListEmpty forall (l' :: S). (Name l -> Name l') -> NameBinderList n' l' -> r
cont = (Name l -> Name n') -> NameBinderList n' n' -> r
forall (l' :: S). (Name l -> Name l') -> NameBinderList n' l' -> r
cont Name n -> Name n'
Name l -> Name n'
rename NameBinderList n' n'
forall (n :: S). NameBinderList n n
NameBinderListEmpty
  coSinkabilityProof Name n -> Name n'
rename (NameBinderListCons NameBinder n i
binder NameBinderList i l
binders) forall (l' :: S). (Name l -> Name l') -> NameBinderList n' l' -> r
cont =
    (Name n -> Name n')
-> NameBinder n i
-> (forall {l' :: S}. (Name i -> Name l') -> NameBinder n' l' -> r)
-> r
forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> NameBinder n l
-> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r)
-> r
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
rename NameBinder n i
binder ((forall {l' :: S}. (Name i -> Name l') -> NameBinder n' l' -> r)
 -> r)
-> (forall {l' :: S}. (Name i -> Name l') -> NameBinder n' l' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \Name i -> Name l'
rename' NameBinder n' l'
binder' ->
      (Name i -> Name l')
-> NameBinderList i l
-> (forall {l' :: S}.
    (Name l -> Name l') -> NameBinderList l' l' -> r)
-> r
forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> NameBinderList n l
-> (forall (l' :: S).
    (Name l -> Name l') -> NameBinderList n' l' -> r)
-> r
forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
coSinkabilityProof Name i -> Name l'
rename' NameBinderList i l
binders ((forall {l' :: S}.
  (Name l -> Name l') -> NameBinderList l' l' -> r)
 -> r)
-> (forall {l' :: S}.
    (Name l -> Name l') -> NameBinderList l' l' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \Name l -> Name l'
rename'' NameBinderList l' l'
binders' ->
        (Name l -> Name l') -> NameBinderList n' l' -> r
forall (l' :: S). (Name l -> Name l') -> NameBinderList n' l' -> r
cont Name l -> Name l'
rename'' (NameBinder n' l' -> NameBinderList l' l' -> NameBinderList n' l'
forall (n :: S) (i :: S) (l :: S).
NameBinder n i -> NameBinderList i l -> NameBinderList n l
NameBinderListCons NameBinder n' l'
binder' NameBinderList l' l'
binders')

  withPattern :: forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> NameBinderList n l
-> (forall (o' :: S).
    DExt o o' =>
    f n l o o' -> NameBinderList o o' -> r)
-> r
withPattern forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withBinder forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
unit forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
comp Scope o
scope NameBinderList n l
binders forall (o' :: S).
DExt o o' =>
f n l o o' -> NameBinderList o o' -> r
cont = case NameBinderList n l
binders of
    NameBinderList n l
NameBinderListEmpty -> f n l o o -> NameBinderList o o -> r
forall (o' :: S).
DExt o o' =>
f n l o o' -> NameBinderList o o' -> r
cont f n l o o
f l l o o
forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
unit NameBinderList o o
forall (n :: S). NameBinderList n n
NameBinderListEmpty
    NameBinderListCons NameBinder n i
x NameBinderList i l
xs ->
      Scope o
-> NameBinder n i
-> (forall {z' :: S}.
    DExt o z' =>
    f n i o z' -> NameBinder o z' -> r)
-> r
forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withBinder Scope o
scope NameBinder n i
x ((forall {z' :: S}.
  DExt o z' =>
  f n i o z' -> NameBinder o z' -> r)
 -> r)
-> (forall {z' :: S}.
    DExt o z' =>
    f n i o z' -> NameBinder o z' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \f n i o z'
f NameBinder o z'
x' ->
        let scope' :: Scope z'
scope' = NameBinder o z' -> Scope o -> Scope z'
forall (n :: S) (pattern :: S -> S -> *) (l :: S).
(Distinct n, CoSinkable pattern) =>
pattern n l -> Scope n -> Scope l
extendScopePattern NameBinder o z'
x' Scope o
scope
        in (forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope z'
-> NameBinderList i l
-> (forall {o' :: S}.
    DExt z' o' =>
    f i l z' o' -> NameBinderList z' o' -> r)
-> r
forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> NameBinderList n l
-> (forall (o' :: S).
    DExt o o' =>
    f n l o o' -> NameBinderList o o' -> r)
-> r
forall (pattern :: S -> S -> *) (o :: S)
       (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
(CoSinkable pattern, Distinct o) =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> pattern n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> pattern o o' -> r)
-> r
withPattern Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
withBinder f x x z z'
forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
unit f x y z z' -> f y y' z' z'' -> f x y' z z''
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
comp Scope z'
scope' NameBinderList i l
xs ((forall {o' :: S}.
  DExt z' o' =>
  f i l z' o' -> NameBinderList z' o' -> r)
 -> r)
-> (forall {o' :: S}.
    DExt z' o' =>
    f i l z' o' -> NameBinderList z' o' -> r)
-> r
forall a b. (a -> b) -> a -> b
$ \f i l z' o'
f' NameBinderList z' o'
xs' ->
            f n l o o' -> NameBinderList o o' -> r
forall (o' :: S).
DExt o o' =>
f n l o o' -> NameBinderList o o' -> r
cont (f n i o z' -> f i l z' o' -> f n l o o'
forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
comp f n i o z'
f f i l z' o'
f') (NameBinder o z' -> NameBinderList z' o' -> NameBinderList o o'
forall (n :: S) (i :: S) (l :: S).
NameBinder n i -> NameBinderList i l -> NameBinderList n l
NameBinderListCons NameBinder o z'
x' NameBinderList z' o'
xs')

-- ** Pattern combinators

-- | An empty pattern type specifies zero possibilities for patterns.
--
-- This type can be used to specify that patterns are not possible.
data V2 (n :: S) (l :: S)

-- | Since 'V2' values logically don't exist, this witnesses the logical reasoning tool of "ex falso quodlibet".
absurd2 :: V2 n l -> a
absurd2 :: forall (n :: S) (l :: S) a. V2 n l -> a
absurd2 V2 n l
v2 = case V2 n l
v2 of {}

instance CoSinkable V2 where
  coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> V2 n l
-> (forall (l' :: S). (Name l -> Name l') -> V2 n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
_ V2 n l
v2 forall (l' :: S). (Name l -> Name l') -> V2 n' l' -> r
_ = V2 n l -> r
forall (n :: S) (l :: S) a. V2 n l -> a
absurd2 V2 n l
v2
  withPattern :: forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> V2 n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> V2 o o' -> r)
-> r
withPattern forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
_ forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
_ forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
_ Scope o
_ V2 n l
v2 forall (o' :: S). DExt o o' => f n l o o' -> V2 o o' -> r
_ = V2 n l -> r
forall (n :: S) (l :: S) a. V2 n l -> a
absurd2 V2 n l
v2
instance UnifiablePattern V2 where
  unifyPatterns :: forall (n :: S) (l :: S) (r :: S).
Distinct n =>
V2 n l -> V2 n r -> UnifyNameBinders V2 n l r
unifyPatterns = V2 n l -> V2 n r -> UnifyNameBinders V2 n l r
forall (n :: S) (l :: S) a. V2 n l -> a
absurd2

-- | A unit pattern type corresponds to a wildcard pattern.
data U2 (n :: S) (l :: S) where
  U2 :: U2 n n  -- ^ Wildcard patten does not modify the scope.

instance CoSinkable U2 where
  coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> U2 n l
-> (forall (l' :: S). (Name l -> Name l') -> U2 n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
rename U2 n l
U2 forall (l' :: S). (Name l -> Name l') -> U2 n' l' -> r
cont = (Name l -> Name n') -> U2 n' n' -> r
forall (l' :: S). (Name l -> Name l') -> U2 n' l' -> r
cont Name n -> Name n'
Name l -> Name n'
rename U2 n' n'
forall (n :: S). U2 n n
U2
  withPattern :: forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> U2 n l
-> (forall (o' :: S). DExt o o' => f n l o o' -> U2 o o' -> r)
-> r
withPattern forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
_withBinder forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
unit forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
_combine Scope o
_scope U2 n l
U2 forall (o' :: S). DExt o o' => f n l o o' -> U2 o o' -> r
cont = f n l o o -> U2 o o -> r
forall (o' :: S). DExt o o' => f n l o o' -> U2 o o' -> r
cont f n l o o
f l l o o
forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
unit U2 o o
forall (n :: S). U2 n n
U2
instance UnifiablePattern U2 where
  unifyPatterns :: forall (n :: S) (l :: S) (r :: S).
Distinct n =>
U2 n l -> U2 n r -> UnifyNameBinders U2 n l r
unifyPatterns U2 n l
U2 U2 n r
U2 = NameBinders n l -> UnifyNameBinders U2 n l l
forall (n :: S) (l :: S) (pattern :: S -> S -> *).
NameBinders n l -> UnifyNameBinders pattern n l l
SameNameBinders NameBinders n n
NameBinders n l
forall (n :: S). NameBinders n n
emptyNameBinders

-- ** Unifiable patterns

-- | A pattern type is unifiable if it is possible to match two
-- patterns and decide how to rename binders.
class CoSinkable pattern => UnifiablePattern pattern where
  -- | Unify two patterns and decide which binders need to be renamed.
  unifyPatterns :: Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r

-- | Unification of values in patterns.
-- By default, 'Eq' instance is used, but it may be useful to ignore
-- some data in pattens (such as location annotations).
class UnifiableInPattern a where
  -- | Unify non-binding components of a pattern.
  unifyInPattern :: a -> a -> Bool
  default unifyInPattern :: Eq a => a -> a -> Bool
  unifyInPattern = a -> a -> Bool
forall a. Eq a => a -> a -> Bool
(==)

instance UnifiablePattern NameBinder where
  unifyPatterns :: forall (n :: S) (l :: S) (r :: S).
Distinct n =>
NameBinder n l
-> NameBinder n r -> UnifyNameBinders NameBinder n l r
unifyPatterns = NameBinder n l
-> NameBinder n r -> UnifyNameBinders NameBinder n l r
forall (i :: S) (l :: S) (r :: S) (pattern :: S -> S -> *).
Distinct i =>
NameBinder i l -> NameBinder i r -> UnifyNameBinders pattern i l r
unifyNameBinders

-- | The easiest way to compare two patterns is to check if they are the same.
-- This function is labelled /unsafe/, since we generally are interested in proper α-equivalence
-- instead of direct equality.
unsafeEqPattern :: (UnifiablePattern pattern, Distinct n) => pattern n l -> pattern n' l' -> Bool
unsafeEqPattern :: forall (pattern :: S -> S -> *) (n :: S) (l :: S) (n' :: S)
       (l' :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n' l' -> Bool
unsafeEqPattern pattern n l
l pattern n' l'
r =
  case pattern n l -> pattern n Any -> UnifyNameBinders pattern n l Any
forall (n :: S) (l :: S) (r :: S).
Distinct n =>
pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
forall (pattern :: S -> S -> *) (n :: S) (l :: S) (r :: S).
(UnifiablePattern pattern, Distinct n) =>
pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
unifyPatterns pattern n l
l (pattern n' l' -> pattern n Any
forall a b. a -> b
unsafeCoerce pattern n' l'
r) of
    SameNameBinders{} -> Bool
True
    UnifyNameBinders pattern n l Any
_                 -> Bool
False

-- * Safe sinking

-- | Sinking an expression from scope @n@ into a (usualy extended) scope @l@,
-- given the renaming (injection from scope @n@ to scope @l@).
class Sinkable (e :: S -> Type) where
  -- | An implementation of this method that typechecks
  -- proves to the compiler that the expression is indeed
  -- 'Sinkable'. However, instead of this implementation, 'sink'
  -- should be used at all call sites for efficiency.
  sinkabilityProof
    :: (Name n -> Name l)   -- ^ Map names from scope @n@ to a (possibly larger) scope @l@.
    -> e n                  -- ^ Expression with free variables in scope @n@.
    -> e l

-- | Sinking a 'Name' is as simple as applying the renaming.
instance Sinkable Name where
  sinkabilityProof :: forall (n :: S) (l :: S). (Name n -> Name l) -> Name n -> Name l
sinkabilityProof Name n -> Name l
rename = Name n -> Name l
rename

-- | Efficient version of 'sinkabilityProof'.
-- In fact, once 'sinkabilityProof' typechecks,
-- it is safe to 'sink' by coercion.
-- See Section 3.5 in [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224) for the details.
sink :: (Sinkable e, DExt n l) => e n -> e l
sink :: forall (e :: S -> *) (n :: S) (l :: S).
(Sinkable e, DExt n l) =>
e n -> e l
sink = e n -> e l
forall a b. a -> b
unsafeCoerce

-- | Extend renaming when going under a 'CoSinkable' pattern (generalized binder).
-- Note that the scope under pattern is independent of the codomain of the renaming.
--
-- This function is used to go under binders when implementing 'sinkabilityProof'
-- and is both a generalization of 'extendRenamingNameBinder' and an efficient implementation of 'coSinkabilityProof'.
extendRenaming
  :: CoSinkable pattern
  => (Name n -> Name n')  -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@.
  -> pattern n l          -- ^ A pattern that extends scope @n@ to another scope @l@.
  -> (forall l'. (Name l -> Name l') -> pattern n' l' -> r )
  -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)
  -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.
  -> r
extendRenaming :: forall (pattern :: S -> S -> *) (n :: S) (n' :: S) (l :: S) r.
CoSinkable pattern =>
(Name n -> Name n')
-> pattern n l
-> (forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r)
-> r
extendRenaming Name n -> Name n'
_ pattern n l
pattern forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r
cont =
  (Name l -> Name Any) -> pattern n' Any -> r
forall (l' :: S). (Name l -> Name l') -> pattern n' l' -> r
cont Name l -> Name Any
forall a b. a -> b
unsafeCoerce (pattern n l -> pattern n' Any
forall a b. a -> b
unsafeCoerce pattern n l
pattern)

-- | Extend renaming of binders when going under a 'CoSinkable' pattern (generalized binder).
-- Note that the scope under pattern is independent of the codomain of the renaming.
extendNameBinderRenaming
  :: CoSinkable pattern
  => (NameBinder i n -> NameBinder i n')  -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@.
  -> pattern n l          -- ^ A pattern that extends scope @n@ to another scope @l@.
  -> (forall l'. (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r )
  -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)
  -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.
  -> r
extendNameBinderRenaming :: forall (pattern :: S -> S -> *) (i :: S) (n :: S) (n' :: S)
       (l :: S) r.
CoSinkable pattern =>
(NameBinder i n -> NameBinder i n')
-> pattern n l
-> (forall (l' :: S).
    (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r)
-> r
extendNameBinderRenaming NameBinder i n -> NameBinder i n'
_ pattern n l
pattern forall (l' :: S).
(NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r
cont =
  (NameBinder n' l -> NameBinder n' Any) -> pattern n' Any -> r
forall (l' :: S).
(NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r
cont NameBinder n' l -> NameBinder n' Any
forall a b. a -> b
unsafeCoerce (pattern n l -> pattern n' Any
forall a b. a -> b
unsafeCoerce pattern n l
pattern)

-- | Safely compose renamings of name binders.
-- The underlying implementation is
composeNameBinderRenamings
  :: (NameBinder n i -> NameBinder n i')    -- ^ Rename binders extending scope @n@ from @i@ to @i'@.
  -> (NameBinder i' l -> NameBinder i' l')  -- ^ Rename binders extending scope @i'@ from @l@ to @l'@.
  -> (NameBinder n l -> NameBinder n l')
composeNameBinderRenamings :: forall (n :: S) (i :: S) (i' :: S) (l :: S) (l' :: S).
(NameBinder n i -> NameBinder n i')
-> (NameBinder i' l -> NameBinder i' l')
-> NameBinder n l
-> NameBinder n l'
composeNameBinderRenamings = ((Any -> Any) -> (Any -> Any) -> Any -> Any)
-> (NameBinder n i -> NameBinder n i')
-> (NameBinder i' l -> NameBinder i' l')
-> NameBinder n l
-> NameBinder n l'
forall a b. a -> b
unsafeCoerce (((Any -> Any) -> (Any -> Any) -> Any -> Any)
-> (Any -> Any) -> (Any -> Any) -> Any -> Any
forall a b c. (a -> b -> c) -> b -> a -> c
flip (Any -> Any) -> (Any -> Any) -> Any -> Any
forall b c a. (b -> c) -> (a -> b) -> a -> c
(.))

-- | Convert renaming of name binders into renaming of names in the inner scopes.
fromNameBinderRenaming :: (NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming :: forall (n :: S) (l :: S) (l' :: S).
(NameBinder n l -> NameBinder n l') -> Name l -> Name l'
fromNameBinderRenaming = (NameBinder n l -> NameBinder n l') -> Name l -> Name l'
forall a b. Coercible a b => a -> b
coerce

-- | Extend renaming when going under a 'NameBinder'.
-- Note that the scope under binder is independent of the codomain of the renaming.
--
-- Semantically, this function may need to rename the binder (resulting in the new scope @l'@),
-- to make sure it does not clash with scope @n'@.
-- However, as it turns out, the foil makes it safe
-- to implement this function as a coercion.
-- See Appendix A in [«The Foil: Capture-Avoiding Substitution With No Sharp Edges»](https://doi.org/10.1145/3587216.3587224) for the details.
--
-- This function is used to go under binders when implementing 'sinkabilityProof'.
-- A generalization of this function is 'extendRenaming' (which is an efficient version of 'coSinkabilityProof').
extendRenamingNameBinder
  :: (Name n -> Name n')  -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@.
  -> NameBinder n l       -- ^ A name binder that extends scope @n@ to another scope @l@.
  -> (forall l'. (Name l -> Name l') -> NameBinder n' l' -> r )
  -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)
  -- and a (possibly refreshed) binder that extends @n'@ to @l'@.
  -> r
extendRenamingNameBinder :: forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> NameBinder n l
-> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r)
-> r
extendRenamingNameBinder Name n -> Name n'
_ (UnsafeNameBinder Name l
name) forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r
cont =
  (Name l -> Name l) -> NameBinder n' l -> r
forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r
cont Name l -> Name l
forall a b. a -> b
unsafeCoerce (Name l -> NameBinder n' l
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder Name l
name)

-- | 'CoSinkable' is to patterns (generalized binders)
-- what 'Sinkable' is to expressions.
--
-- See Section 2.3 of [«Free Foil: Generating Efficient and Scope-Safe Abstract Syntax»](https://arxiv.org/abs/2405.16384) for more details.
class CoSinkable (pattern :: S -> S -> Type) where
  -- | An implementation of this method that typechecks
  -- proves to the compiler that the pattern is indeed
  -- 'CoSinkable'. However, instead of this implementation,
  -- 'extendRenaming' should be used at all call sites for efficiency.
  coSinkabilityProof
    :: (Name n -> Name n')  -- ^ Map names from scope @n@ to a (possibly larger) scope @n'@.
    -> pattern n l          -- ^ A pattern that extends scope @n@ to another scope @l@.
    -> (forall l'. (Name l -> Name l') -> pattern n' l' -> r)
    -- ^ A continuation, accepting an extended renaming from @l@ to @l'@ (which itself extends @n'@)
    -- and a (possibly refreshed) pattern that extends @n'@ to @l'@.
    -> r

  -- | Generalized processing of a pattern.
  --
  -- You can see 'withPattern' as a CPS-style traversal over the binders in a pattern.
  withPattern
    :: Distinct o
    => (forall x y z r'. Distinct z => Scope z -> NameBinder x y -> (forall z'. DExt z z' => f x y z z' -> NameBinder z z' -> r') -> r')
    -- ^ Processing of a single 'NameBinder', this will be applied to each binder in a pattern.
    -> (forall x z z'. DExt z z' => f x x z z')
    -- ^ Result in case no binders are present. This can be seen as scope-indexed 'mempty'.
    -> (forall x y y' z z' z''. (DExt z z', DExt z' z'') => f x y z z' -> f y y' z' z'' -> f x y' z z'')
    -- ^ Composition of results for nested binders/patterns. This can be seen as scope-indexed 'mappend'.
    -> Scope o
    -- ^ Ambient scope.
    -> pattern n l
    -- ^ Pattern to process.
    -> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)
    -- ^ Continuation, accepting result for the entire pattern and a (possibly refreshed) pattern.
    -> r

instance CoSinkable NameBinder where
  coSinkabilityProof :: forall (n :: S) (n' :: S) (l :: S) r.
(Name n -> Name n')
-> NameBinder n l
-> (forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r)
-> r
coSinkabilityProof Name n -> Name n'
_rename (UnsafeNameBinder Name l
name) forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r
cont =
    (Name l -> Name l) -> NameBinder n' l -> r
forall (l' :: S). (Name l -> Name l') -> NameBinder n' l' -> r
cont Name l -> Name l
forall a b. a -> b
unsafeCoerce (Name l -> NameBinder n' l
forall (n :: S) (l :: S). Name l -> NameBinder n l
UnsafeNameBinder Name l
name)

  withPattern :: forall (o :: S) (f :: S -> S -> S -> S -> *) (n :: S) (l :: S) r.
Distinct o =>
(forall (x :: S) (y :: S) (z :: S) r'.
 Distinct z =>
 Scope z
 -> NameBinder x y
 -> (forall (z' :: S).
     DExt z z' =>
     f x y z z' -> NameBinder z z' -> r')
 -> r')
-> (forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z')
-> (forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S)
           (z'' :: S).
    (DExt z z', DExt z' z'') =>
    f x y z z' -> f y y' z' z'' -> f x y' z z'')
-> Scope o
-> NameBinder n l
-> (forall (o' :: S).
    DExt o o' =>
    f n l o o' -> NameBinder o o' -> r)
-> r
withPattern forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
f forall (x :: S) (z :: S) (z' :: S). DExt z z' => f x x z z'
_ forall (x :: S) (y :: S) (y' :: S) (z :: S) (z' :: S) (z'' :: S).
(DExt z z', DExt z' z'') =>
f x y z z' -> f y y' z' z'' -> f x y' z z''
_ = Scope o
-> NameBinder n l
-> (forall (z' :: S).
    DExt o z' =>
    f n l o z' -> NameBinder o z' -> r)
-> r
forall (x :: S) (y :: S) (z :: S) r'.
Distinct z =>
Scope z
-> NameBinder x y
-> (forall (z' :: S).
    DExt z z' =>
    f x y z z' -> NameBinder z z' -> r')
-> r'
f

-- * Safe substitions

-- | A substitution is a mapping from names in scope @i@
-- to expressions @e o@ in scope @o@.
newtype Substitution (e :: S -> Type) (i :: S) (o :: S) =
  UnsafeSubstitution (IntMap (e o))

-- | Apply substitution to a given name.
lookupSubst :: InjectName e => Substitution e i o -> Name i -> e o
lookupSubst :: forall (e :: S -> *) (i :: S) (o :: S).
InjectName e =>
Substitution e i o -> Name i -> e o
lookupSubst (UnsafeSubstitution IntMap (e o)
env) (UnsafeName RawName
name) =
    case RawName -> IntMap (e o) -> Maybe (e o)
forall a. RawName -> IntMap a -> Maybe a
IntMap.lookup RawName
name IntMap (e o)
env of
        Just e o
ex -> e o
ex
        Maybe (e o)
Nothing -> Name o -> e o
forall (n :: S). Name n -> e n
forall (e :: S -> *) (n :: S). InjectName e => Name n -> e n
injectName (RawName -> Name o
forall (n :: S). RawName -> Name n
UnsafeName RawName
name)

-- | Identity substitution maps all names to expresion-variables.
identitySubst
  :: InjectName e => Substitution e i i
identitySubst :: forall (e :: S -> *) (i :: S). InjectName e => Substitution e i i
identitySubst = IntMap (e i) -> Substitution e i i
forall (e :: S -> *) (i :: S) (o :: S).
IntMap (e o) -> Substitution e i o
UnsafeSubstitution IntMap (e i)
forall a. IntMap a
IntMap.empty

-- | Extend substitution with a particular mapping.
addSubst
  :: Substitution e i o
  -> NameBinder i i'
  -> e o
  -> Substitution e i' o
addSubst :: forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
addSubst (UnsafeSubstitution IntMap (e o)
env) (UnsafeNameBinder (UnsafeName RawName
name)) e o
ex
  = IntMap (e o) -> Substitution e i' o
forall (e :: S -> *) (i :: S) (o :: S).
IntMap (e o) -> Substitution e i o
UnsafeSubstitution (RawName -> e o -> IntMap (e o) -> IntMap (e o)
forall a. RawName -> a -> IntMap a -> IntMap a
IntMap.insert RawName
name e o
ex IntMap (e o)
env)

-- | Add variable renaming to a substitution.
-- This includes the performance optimization of eliding names mapped to themselves.
addRename :: InjectName e => Substitution e i o -> NameBinder i i' -> Name o -> Substitution e i' o
addRename :: forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
InjectName e =>
Substitution e i o
-> NameBinder i i' -> Name o -> Substitution e i' o
addRename s :: Substitution e i o
s@(UnsafeSubstitution IntMap (e o)
env) b :: NameBinder i i'
b@(UnsafeNameBinder (UnsafeName RawName
name1)) n :: Name o
n@(UnsafeName RawName
name2)
    | RawName
name1 RawName -> RawName -> Bool
forall a. Eq a => a -> a -> Bool
== RawName
name2 = IntMap (e o) -> Substitution e i' o
forall (e :: S -> *) (i :: S) (o :: S).
IntMap (e o) -> Substitution e i o
UnsafeSubstitution (RawName -> IntMap (e o) -> IntMap (e o)
forall a. RawName -> IntMap a -> IntMap a
IntMap.delete RawName
name1 IntMap (e o)
env)
    | Bool
otherwise = Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
forall (e :: S -> *) (i :: S) (o :: S) (i' :: S).
Substitution e i o -> NameBinder i i' -> e o -> Substitution e i' o
addSubst Substitution e i o
s NameBinder i i'
b (Name o -> e o
forall (n :: S). Name n -> e n
forall (e :: S -> *) (n :: S). InjectName e => Name n -> e n
injectName Name o
n)

-- | Substitutions are sinkable as long as corresponding expressions are.
instance (Sinkable e) => Sinkable (Substitution e i) where
  sinkabilityProof :: forall (n :: S) (l :: S).
(Name n -> Name l) -> Substitution e i n -> Substitution e i l
sinkabilityProof Name n -> Name l
rename (UnsafeSubstitution IntMap (e n)
env) =
    IntMap (e l) -> Substitution e i l
forall (e :: S -> *) (i :: S) (o :: S).
IntMap (e o) -> Substitution e i o
UnsafeSubstitution ((e n -> e l) -> IntMap (e n) -> IntMap (e l)
forall a b. (a -> b) -> IntMap a -> IntMap b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Name n -> Name l) -> e n -> e l
forall (n :: S) (l :: S). (Name n -> Name l) -> e n -> e l
forall (e :: S -> *) (n :: S) (l :: S).
Sinkable e =>
(Name n -> Name l) -> e n -> e l
sinkabilityProof Name n -> Name l
rename) IntMap (e n)
env)

-- * 'Name' maps

-- | A /total/ map from names in scope @n@ to elements of type @a@.
newtype NameMap (n :: S) a = NameMap { forall (n :: S) a. NameMap n a -> IntMap a
getNameMap :: IntMap a }

-- | An empty map belongs in the empty scope.
emptyNameMap :: NameMap VoidS a
emptyNameMap :: forall a. NameMap 'VoidS a
emptyNameMap = IntMap a -> NameMap 'VoidS a
forall (n :: S) a. IntMap a -> NameMap n a
NameMap IntMap a
forall a. IntMap a
IntMap.empty

-- | Looking up a name should always succeed.
--
-- Note that since 'Name' is 'Sinkable', you can lookup a name from scope @n@ in a 'NameMap' for scope @l@ whenever @l@ extends @n@.
lookupName :: Name n -> NameMap n a -> a
lookupName :: forall (n :: S) a. Name n -> NameMap n a -> a
lookupName Name n
name (NameMap IntMap a
m) =
  case RawName -> IntMap a -> Maybe a
forall a. RawName -> IntMap a -> Maybe a
IntMap.lookup (Name n -> RawName
forall (l :: S). Name l -> RawName
nameId Name n
name) IntMap a
m of
    Maybe a
Nothing -> String -> a
forall a. HasCallStack => String -> a
error String
"impossible: unknown name in a NameMap"
    Just a
x  -> a
x

-- | Extending a map with a single mapping.
--
-- Note that the scope parameter of the result differs from the initial map.
addNameBinder :: NameBinder n l -> a -> NameMap n a -> NameMap l a
addNameBinder :: forall (n :: S) (l :: S) a.
NameBinder n l -> a -> NameMap n a -> NameMap l a
addNameBinder NameBinder n l
name a
x (NameMap IntMap a
m) = IntMap a -> NameMap l a
forall (n :: S) a. IntMap a -> NameMap n a
NameMap (RawName -> a -> IntMap a -> IntMap a
forall a. RawName -> a -> IntMap a -> IntMap a
IntMap.insert (Name l -> RawName
forall (l :: S). Name l -> RawName
nameId (NameBinder n l -> Name l
forall (n :: S) (l :: S). NameBinder n l -> Name l
nameOf NameBinder n l
name)) a
x IntMap a
m)

-- * Raw types and operations

-- | We will use 'Int' for efficient representation of identifiers.
type Id = Int

-- | Raw name is simply an identifier.
type RawName = Id

-- | A raw scope is a set of raw names.
type RawScope = IntSet

-- | \(O(\min(n, W))\).
-- Generate a fresh raw name that
-- does not appear in a given raw scope.
rawFreshName :: RawScope -> RawName
rawFreshName :: RawScope -> RawName
rawFreshName RawScope
scope | RawScope -> Bool
IntSet.null RawScope
scope = RawName
0
                   | Bool
otherwise = RawScope -> RawName
IntSet.findMax RawScope
scope RawName -> RawName -> RawName
forall a. Num a => a -> a -> a
+ RawName
1

-- | Check if a raw name is contained in a raw scope.
rawMember :: RawName -> RawScope -> Bool
rawMember :: RawName -> RawScope -> Bool
rawMember = RawName -> RawScope -> Bool
IntSet.member

-- * Constraints

-- | Every scope is a (trivial) extension of itself.
--
-- __Important__: this class exists to assist tracking scope extensions
-- for type variables of kind 'S'.
-- Users of the foil are not supposed to implement any instances of 'ExtEndo'.
class ExtEndo (n :: S)

-- | Some scopes are extensions of other scopes.
--
-- __Important__: this class exists to assist tracking scope extensions
-- for type variables of kind 'S'.
-- Users of the foil are not supposed to implement any instances of 'Ext'.
class (ExtEndo n => ExtEndo l ) => Ext (n :: S) (l :: S)
instance ( ExtEndo n => ExtEndo l ) => Ext n l

-- | Scopes with distinct names.
--
-- __Important__: this class exists to explicitly
-- mark scopes with distinct names.
-- Users of the foil are not supposed to implement any instances of 'Distinct'.
class Distinct (n :: S)
instance Distinct VoidS

-- | Scope extensions with distinct names.
type DExt n l = (Distinct l, Ext n l)

-- | Instances of this typeclass possess the ability to inject names.
-- Usually, this is a variable data constructor.
class InjectName (e :: S -> Type) where
  -- | Inject names into expressions.
  injectName :: Name n -> e n