{-# 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 #-}
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
data S
= VoidS
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
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)
nameId :: Name l -> Id
nameId :: forall (l :: S). Name l -> RawName
nameId (UnsafeName RawName
i) = RawName
i
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)
emptyScope :: Scope VoidS
emptyScope :: Scope 'VoidS
emptyScope = RawScope -> Scope 'VoidS
forall (n :: S). RawScope -> Scope n
UnsafeScope RawScope
IntSet.empty
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
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)
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)
newtype ExtendScope n l (o :: S) (o' :: S) = ExtendScope (Scope n -> Scope l)
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
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)
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
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)
newtype NamesOf (n :: S) l (o :: S) (o' :: S) = NamesOf [Name l]
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 []
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)
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))
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)
withFreshPattern
:: (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)
=> Scope o
-> pattern n l
-> (forall o'. DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> 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')
withRefreshed
:: Distinct o
=> Scope o
-> Name i
-> (forall o'. DExt o o' => NameBinder o o' -> r)
-> 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
withRefreshedPattern
:: (Distinct o, CoSinkable pattern, Sinkable e, InjectName e)
=> Scope o
-> pattern n l
-> (forall o'. DExt o o' => (Substitution e n o -> Substitution e l o') -> pattern o o' -> r)
-> 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')
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')
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)
newtype WithRefreshedPattern e n l o o' = WithRefreshedPattern (Substitution e n o -> Substitution e l o')
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
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)
newtype WithRefreshedPattern' e n l (o :: S) (o' :: S) = WithRefreshedPattern' ((Name n -> e o) -> Name l -> e o')
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))
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)
data DistinctEvidence (n :: S) where
Distinct :: Distinct n => DistinctEvidence n
data ExtEvidence (n :: S) (l :: S) where
Ext :: Ext n l => ExtEvidence n l
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
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
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)
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)
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)
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")
pattern n l
pat
(\(UnsinkName Name l -> Maybe (Name n)
unsink) pattern n o'
_ -> Name l -> Maybe (Name n)
unsink)
newtype UnsinkName n l (o :: S) (o' :: S) = UnsinkName (Name l -> Maybe (Name n))
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
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)
data UnifyNameBinders (pattern :: S -> S -> Type) n l r where
SameNameBinders
:: NameBinders n l
-> UnifyNameBinders pattern n l l
RenameLeftNameBinder
:: NameBinders n r
-> (NameBinder n l -> NameBinder n r)
-> UnifyNameBinders pattern n l r
RenameRightNameBinder
:: NameBinders n l
-> (NameBinder n r -> NameBinder n l)
-> UnifyNameBinders pattern n l r
RenameBothBinders
:: NameBinders n lr
-> (NameBinder n l -> NameBinder n lr)
-> (NameBinder n r -> NameBinder n lr)
-> UnifyNameBinders pattern n l r
NotUnifiable :: UnifyNameBinders pattern n l r
unifyNameBinders
:: forall i l r pattern. Distinct i
=> NameBinder i l
-> NameBinder i r
-> 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))
| 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')
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)
andThenUnifyPatterns
:: (UnifiablePattern pattern, Distinct l, Distinct l')
=> UnifyNameBinders pattern n l l'
-> (pattern l r, pattern l' r')
-> 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)
andThenUnifyNameBinders
:: (UnifiablePattern pattern, Distinct l, Distinct l')
=> UnifyNameBinders pattern n l l'
-> (NameBinder l r, NameBinder l' r')
-> 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)
newtype NameBinders (n :: S) (l :: S) = UnsafeNameBinders IntSet
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)
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
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
nameBindersSingleton :: NameBinder n l -> NameBinders n l
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)))
data NameBinderList n l where
NameBinderListEmpty :: NameBinderList n n
NameBinderListCons
:: NameBinder n i
-> NameBinderList i l
-> NameBinderList n l
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)
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')
data V2 (n :: S) (l :: S)
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
data U2 (n :: S) (l :: S) where
U2 :: U2 n n
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
class CoSinkable pattern => UnifiablePattern pattern where
unifyPatterns :: Distinct n => pattern n l -> pattern n r -> UnifyNameBinders pattern n l r
class UnifiableInPattern a where
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
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
class Sinkable (e :: S -> Type) where
sinkabilityProof
:: (Name n -> Name l)
-> e n
-> e l
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
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
extendRenaming
:: CoSinkable pattern
=> (Name n -> Name n')
-> pattern n l
-> (forall l'. (Name l -> Name l') -> pattern n' l' -> r )
-> 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)
extendNameBinderRenaming
:: CoSinkable pattern
=> (NameBinder i n -> NameBinder i n')
-> pattern n l
-> (forall l'. (NameBinder n' l -> NameBinder n' l') -> pattern n' l' -> r )
-> 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)
composeNameBinderRenamings
:: (NameBinder n i -> NameBinder n i')
-> (NameBinder i' l -> NameBinder i' 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
(.))
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
extendRenamingNameBinder
:: (Name n -> Name n')
-> NameBinder n l
-> (forall l'. (Name l -> Name l') -> NameBinder n' l' -> r )
-> 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)
class CoSinkable (pattern :: S -> S -> Type) where
coSinkabilityProof
:: (Name n -> Name n')
-> pattern n l
-> (forall l'. (Name l -> Name l') -> pattern n' l' -> r)
-> r
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')
-> (forall x z z'. DExt z z' => f x x z z')
-> (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'')
-> Scope o
-> pattern n l
-> (forall o'. DExt o o' => f n l o o' -> pattern o o' -> r)
-> 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
newtype Substitution (e :: S -> Type) (i :: S) (o :: S) =
UnsafeSubstitution (IntMap (e o))
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)
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
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)
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)
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)
newtype NameMap (n :: S) a = NameMap { forall (n :: S) a. NameMap n a -> IntMap a
getNameMap :: IntMap a }
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
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
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)
type Id = Int
type RawName = Id
type RawScope = IntSet
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
rawMember :: RawName -> RawScope -> Bool
rawMember :: RawName -> RawScope -> Bool
rawMember = RawName -> RawScope -> Bool
IntSet.member
class ExtEndo (n :: S)
class (ExtEndo n => ExtEndo l ) => Ext (n :: S) (l :: S)
instance ( ExtEndo n => ExtEndo l ) => Ext n l
class Distinct (n :: S)
instance Distinct VoidS
type DExt n l = (Distinct l, Ext n l)
class InjectName (e :: S -> Type) where
injectName :: Name n -> e n