{-# OPTIONS_GHC -fno-warn-orphans #-}
module Agda.Compiler.Treeless.Subst where
import qualified Data.Map as Map
import Data.Map (Map)
import Data.Maybe
import Data.Semigroup ( Semigroup, (<>), All(..), Any(..) )
import Agda.Syntax.Treeless
import Agda.TypeChecking.Substitute
import Agda.Utils.Impossible
instance DeBruijn TTerm where
deBruijnVar :: Int -> TTerm
deBruijnVar = Int -> TTerm
TVar
deBruijnView :: TTerm -> Maybe Int
deBruijnView (TVar Int
i) = Int -> Maybe Int
forall a. a -> Maybe a
Just Int
i
deBruijnView TTerm
_ = Maybe Int
forall a. Maybe a
Nothing
instance Subst TTerm where
type SubstArg TTerm = TTerm
applySubst :: Substitution' (SubstArg TTerm) -> TTerm -> TTerm
applySubst Substitution' (SubstArg TTerm)
IdS = TTerm -> TTerm
forall a. a -> a
id
applySubst Substitution' (SubstArg TTerm)
rho = \case
t :: TTerm
t@TDef{} -> TTerm
t
t :: TTerm
t@TLit{} -> TTerm
t
t :: TTerm
t@TCon{} -> TTerm
t
t :: TTerm
t@TPrim{} -> TTerm
t
t :: TTerm
t@TUnit{} -> TTerm
t
t :: TTerm
t@TSort{} -> TTerm
t
t :: TTerm
t@TErased{} -> TTerm
t
t :: TTerm
t@TError{} -> TTerm
t
TVar Int
i -> Substitution' TTerm -> Int -> TTerm
forall a. EndoSubst a => Substitution' a -> Int -> a
lookupS Substitution' TTerm
Substitution' (SubstArg TTerm)
rho Int
i
TApp TTerm
f [TTerm]
ts -> TTerm -> [TTerm] -> TTerm
tApp (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg TTerm)
rho TTerm
f) (Substitution' (SubstArg [TTerm]) -> [TTerm] -> [TTerm]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [TTerm])
Substitution' (SubstArg TTerm)
rho [TTerm]
ts)
TLam TTerm
b -> TTerm -> TTerm
TLam (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' TTerm -> Substitution' TTerm
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 Substitution' TTerm
Substitution' (SubstArg TTerm)
rho) TTerm
b)
TLet TTerm
e TTerm
b -> TTerm -> TTerm -> TTerm
TLet (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg TTerm)
rho TTerm
e) (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' TTerm -> Substitution' TTerm
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
1 Substitution' TTerm
Substitution' (SubstArg TTerm)
rho) TTerm
b)
TCase Int
i CaseInfo
t TTerm
d [TAlt]
bs ->
case Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg TTerm)
rho (Int -> TTerm
TVar Int
i) of
TVar Int
j -> Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
j CaseInfo
t (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg TTerm)
rho TTerm
d) (Substitution' (SubstArg [TAlt]) -> [TAlt] -> [TAlt]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg [TAlt])
Substitution' (SubstArg TTerm)
rho [TAlt]
bs)
TTerm
e -> TTerm -> TTerm -> TTerm
TLet TTerm
e (TTerm -> TTerm) -> TTerm -> TTerm
forall a b. (a -> b) -> a -> b
$ Int -> CaseInfo -> TTerm -> [TAlt] -> TTerm
TCase Int
0 CaseInfo
t (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' TTerm
Substitution' (SubstArg TTerm)
rho' TTerm
d) (Substitution' (SubstArg [TAlt]) -> [TAlt] -> [TAlt]
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' TTerm
Substitution' (SubstArg [TAlt])
rho' [TAlt]
bs)
where rho' :: Substitution' TTerm
rho' = Int -> Substitution' TTerm -> Substitution' TTerm
forall a. Int -> Substitution' a -> Substitution' a
wkS Int
1 Substitution' TTerm
Substitution' (SubstArg TTerm)
rho
TCoerce TTerm
e -> TTerm -> TTerm
TCoerce (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg TTerm)
rho TTerm
e)
where
tApp :: TTerm -> [TTerm] -> TTerm
tApp (TPrim TPrim
PSeq) [TTerm
TErased, TTerm
b] = TTerm
b
tApp TTerm
f [TTerm]
ts = TTerm -> [TTerm] -> TTerm
TApp TTerm
f [TTerm]
ts
instance Subst TAlt where
type SubstArg TAlt = TTerm
applySubst :: Substitution' (SubstArg TAlt) -> TAlt -> TAlt
applySubst Substitution' (SubstArg TAlt)
rho (TACon QName
c Int
i TTerm
b) = QName -> Int -> TTerm -> TAlt
TACon QName
c Int
i (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Int -> Substitution' TTerm -> Substitution' TTerm
forall a. Int -> Substitution' a -> Substitution' a
liftS Int
i Substitution' TTerm
Substitution' (SubstArg TAlt)
rho) TTerm
b)
applySubst Substitution' (SubstArg TAlt)
rho (TALit Literal
l TTerm
b) = Literal -> TTerm -> TAlt
TALit Literal
l (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg TAlt)
Substitution' (SubstArg TTerm)
rho TTerm
b)
applySubst Substitution' (SubstArg TAlt)
rho (TAGuard TTerm
g TTerm
b) = TTerm -> TTerm -> TAlt
TAGuard (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg TAlt)
Substitution' (SubstArg TTerm)
rho TTerm
g) (Substitution' (SubstArg TTerm) -> TTerm -> TTerm
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst Substitution' (SubstArg TAlt)
Substitution' (SubstArg TTerm)
rho TTerm
b)
newtype UnderLambda = UnderLambda Any
deriving (UnderLambda -> UnderLambda -> Bool
(UnderLambda -> UnderLambda -> Bool)
-> (UnderLambda -> UnderLambda -> Bool) -> Eq UnderLambda
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: UnderLambda -> UnderLambda -> Bool
== :: UnderLambda -> UnderLambda -> Bool
$c/= :: UnderLambda -> UnderLambda -> Bool
/= :: UnderLambda -> UnderLambda -> Bool
Eq, Eq UnderLambda
Eq UnderLambda =>
(UnderLambda -> UnderLambda -> Ordering)
-> (UnderLambda -> UnderLambda -> Bool)
-> (UnderLambda -> UnderLambda -> Bool)
-> (UnderLambda -> UnderLambda -> Bool)
-> (UnderLambda -> UnderLambda -> Bool)
-> (UnderLambda -> UnderLambda -> UnderLambda)
-> (UnderLambda -> UnderLambda -> UnderLambda)
-> Ord UnderLambda
UnderLambda -> UnderLambda -> Bool
UnderLambda -> UnderLambda -> Ordering
UnderLambda -> UnderLambda -> UnderLambda
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
$ccompare :: UnderLambda -> UnderLambda -> Ordering
compare :: UnderLambda -> UnderLambda -> Ordering
$c< :: UnderLambda -> UnderLambda -> Bool
< :: UnderLambda -> UnderLambda -> Bool
$c<= :: UnderLambda -> UnderLambda -> Bool
<= :: UnderLambda -> UnderLambda -> Bool
$c> :: UnderLambda -> UnderLambda -> Bool
> :: UnderLambda -> UnderLambda -> Bool
$c>= :: UnderLambda -> UnderLambda -> Bool
>= :: UnderLambda -> UnderLambda -> Bool
$cmax :: UnderLambda -> UnderLambda -> UnderLambda
max :: UnderLambda -> UnderLambda -> UnderLambda
$cmin :: UnderLambda -> UnderLambda -> UnderLambda
min :: UnderLambda -> UnderLambda -> UnderLambda
Ord, Int -> UnderLambda -> ShowS
[UnderLambda] -> ShowS
UnderLambda -> String
(Int -> UnderLambda -> ShowS)
-> (UnderLambda -> String)
-> ([UnderLambda] -> ShowS)
-> Show UnderLambda
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> UnderLambda -> ShowS
showsPrec :: Int -> UnderLambda -> ShowS
$cshow :: UnderLambda -> String
show :: UnderLambda -> String
$cshowList :: [UnderLambda] -> ShowS
showList :: [UnderLambda] -> ShowS
Show, NonEmpty UnderLambda -> UnderLambda
UnderLambda -> UnderLambda -> UnderLambda
(UnderLambda -> UnderLambda -> UnderLambda)
-> (NonEmpty UnderLambda -> UnderLambda)
-> (forall b. Integral b => b -> UnderLambda -> UnderLambda)
-> Semigroup UnderLambda
forall b. Integral b => b -> UnderLambda -> UnderLambda
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: UnderLambda -> UnderLambda -> UnderLambda
<> :: UnderLambda -> UnderLambda -> UnderLambda
$csconcat :: NonEmpty UnderLambda -> UnderLambda
sconcat :: NonEmpty UnderLambda -> UnderLambda
$cstimes :: forall b. Integral b => b -> UnderLambda -> UnderLambda
stimes :: forall b. Integral b => b -> UnderLambda -> UnderLambda
Semigroup, Semigroup UnderLambda
UnderLambda
Semigroup UnderLambda =>
UnderLambda
-> (UnderLambda -> UnderLambda -> UnderLambda)
-> ([UnderLambda] -> UnderLambda)
-> Monoid UnderLambda
[UnderLambda] -> UnderLambda
UnderLambda -> UnderLambda -> UnderLambda
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: UnderLambda
mempty :: UnderLambda
$cmappend :: UnderLambda -> UnderLambda -> UnderLambda
mappend :: UnderLambda -> UnderLambda -> UnderLambda
$cmconcat :: [UnderLambda] -> UnderLambda
mconcat :: [UnderLambda] -> UnderLambda
Monoid)
newtype SeqArg = SeqArg All
deriving (SeqArg -> SeqArg -> Bool
(SeqArg -> SeqArg -> Bool)
-> (SeqArg -> SeqArg -> Bool) -> Eq SeqArg
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: SeqArg -> SeqArg -> Bool
== :: SeqArg -> SeqArg -> Bool
$c/= :: SeqArg -> SeqArg -> Bool
/= :: SeqArg -> SeqArg -> Bool
Eq, Eq SeqArg
Eq SeqArg =>
(SeqArg -> SeqArg -> Ordering)
-> (SeqArg -> SeqArg -> Bool)
-> (SeqArg -> SeqArg -> Bool)
-> (SeqArg -> SeqArg -> Bool)
-> (SeqArg -> SeqArg -> Bool)
-> (SeqArg -> SeqArg -> SeqArg)
-> (SeqArg -> SeqArg -> SeqArg)
-> Ord SeqArg
SeqArg -> SeqArg -> Bool
SeqArg -> SeqArg -> Ordering
SeqArg -> SeqArg -> SeqArg
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
$ccompare :: SeqArg -> SeqArg -> Ordering
compare :: SeqArg -> SeqArg -> Ordering
$c< :: SeqArg -> SeqArg -> Bool
< :: SeqArg -> SeqArg -> Bool
$c<= :: SeqArg -> SeqArg -> Bool
<= :: SeqArg -> SeqArg -> Bool
$c> :: SeqArg -> SeqArg -> Bool
> :: SeqArg -> SeqArg -> Bool
$c>= :: SeqArg -> SeqArg -> Bool
>= :: SeqArg -> SeqArg -> Bool
$cmax :: SeqArg -> SeqArg -> SeqArg
max :: SeqArg -> SeqArg -> SeqArg
$cmin :: SeqArg -> SeqArg -> SeqArg
min :: SeqArg -> SeqArg -> SeqArg
Ord, Int -> SeqArg -> ShowS
[SeqArg] -> ShowS
SeqArg -> String
(Int -> SeqArg -> ShowS)
-> (SeqArg -> String) -> ([SeqArg] -> ShowS) -> Show SeqArg
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> SeqArg -> ShowS
showsPrec :: Int -> SeqArg -> ShowS
$cshow :: SeqArg -> String
show :: SeqArg -> String
$cshowList :: [SeqArg] -> ShowS
showList :: [SeqArg] -> ShowS
Show, NonEmpty SeqArg -> SeqArg
SeqArg -> SeqArg -> SeqArg
(SeqArg -> SeqArg -> SeqArg)
-> (NonEmpty SeqArg -> SeqArg)
-> (forall b. Integral b => b -> SeqArg -> SeqArg)
-> Semigroup SeqArg
forall b. Integral b => b -> SeqArg -> SeqArg
forall a.
(a -> a -> a)
-> (NonEmpty a -> a)
-> (forall b. Integral b => b -> a -> a)
-> Semigroup a
$c<> :: SeqArg -> SeqArg -> SeqArg
<> :: SeqArg -> SeqArg -> SeqArg
$csconcat :: NonEmpty SeqArg -> SeqArg
sconcat :: NonEmpty SeqArg -> SeqArg
$cstimes :: forall b. Integral b => b -> SeqArg -> SeqArg
stimes :: forall b. Integral b => b -> SeqArg -> SeqArg
Semigroup, Semigroup SeqArg
SeqArg
Semigroup SeqArg =>
SeqArg
-> (SeqArg -> SeqArg -> SeqArg)
-> ([SeqArg] -> SeqArg)
-> Monoid SeqArg
[SeqArg] -> SeqArg
SeqArg -> SeqArg -> SeqArg
forall a.
Semigroup a =>
a -> (a -> a -> a) -> ([a] -> a) -> Monoid a
$cmempty :: SeqArg
mempty :: SeqArg
$cmappend :: SeqArg -> SeqArg -> SeqArg
mappend :: SeqArg -> SeqArg -> SeqArg
$cmconcat :: [SeqArg] -> SeqArg
mconcat :: [SeqArg] -> SeqArg
Monoid)
data Occurs = Occurs Int UnderLambda SeqArg
deriving (Occurs -> Occurs -> Bool
(Occurs -> Occurs -> Bool)
-> (Occurs -> Occurs -> Bool) -> Eq Occurs
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Occurs -> Occurs -> Bool
== :: Occurs -> Occurs -> Bool
$c/= :: Occurs -> Occurs -> Bool
/= :: Occurs -> Occurs -> Bool
Eq, Eq Occurs
Eq Occurs =>
(Occurs -> Occurs -> Ordering)
-> (Occurs -> Occurs -> Bool)
-> (Occurs -> Occurs -> Bool)
-> (Occurs -> Occurs -> Bool)
-> (Occurs -> Occurs -> Bool)
-> (Occurs -> Occurs -> Occurs)
-> (Occurs -> Occurs -> Occurs)
-> Ord Occurs
Occurs -> Occurs -> Bool
Occurs -> Occurs -> Ordering
Occurs -> Occurs -> Occurs
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
$ccompare :: Occurs -> Occurs -> Ordering
compare :: Occurs -> Occurs -> Ordering
$c< :: Occurs -> Occurs -> Bool
< :: Occurs -> Occurs -> Bool
$c<= :: Occurs -> Occurs -> Bool
<= :: Occurs -> Occurs -> Bool
$c> :: Occurs -> Occurs -> Bool
> :: Occurs -> Occurs -> Bool
$c>= :: Occurs -> Occurs -> Bool
>= :: Occurs -> Occurs -> Bool
$cmax :: Occurs -> Occurs -> Occurs
max :: Occurs -> Occurs -> Occurs
$cmin :: Occurs -> Occurs -> Occurs
min :: Occurs -> Occurs -> Occurs
Ord, Int -> Occurs -> ShowS
[Occurs] -> ShowS
Occurs -> String
(Int -> Occurs -> ShowS)
-> (Occurs -> String) -> ([Occurs] -> ShowS) -> Show Occurs
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Occurs -> ShowS
showsPrec :: Int -> Occurs -> ShowS
$cshow :: Occurs -> String
show :: Occurs -> String
$cshowList :: [Occurs] -> ShowS
showList :: [Occurs] -> ShowS
Show)
once :: Occurs
once :: Occurs
once = Int -> UnderLambda -> SeqArg -> Occurs
Occurs Int
1 UnderLambda
forall a. Monoid a => a
mempty (All -> SeqArg
SeqArg (All -> SeqArg) -> All -> SeqArg
forall a b. (a -> b) -> a -> b
$ Bool -> All
All Bool
False)
inSeq :: Occurs -> Occurs
inSeq :: Occurs -> Occurs
inSeq (Occurs Int
n UnderLambda
l SeqArg
_) = Int -> UnderLambda -> SeqArg -> Occurs
Occurs Int
n UnderLambda
l SeqArg
forall a. Monoid a => a
mempty
underLambda :: Occurs -> Occurs
underLambda :: Occurs -> Occurs
underLambda Occurs
o = Occurs
o Occurs -> Occurs -> Occurs
forall a. Semigroup a => a -> a -> a
<> Int -> UnderLambda -> SeqArg -> Occurs
Occurs Int
0 (Any -> UnderLambda
UnderLambda (Any -> UnderLambda) -> Any -> UnderLambda
forall a b. (a -> b) -> a -> b
$ Bool -> Any
Any Bool
True) SeqArg
forall a. Monoid a => a
mempty
instance Semigroup Occurs where
Occurs Int
a UnderLambda
k SeqArg
s <> :: Occurs -> Occurs -> Occurs
<> Occurs Int
b UnderLambda
l SeqArg
t = Int -> UnderLambda -> SeqArg -> Occurs
Occurs (Int
a Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
b) (UnderLambda
k UnderLambda -> UnderLambda -> UnderLambda
forall a. Semigroup a => a -> a -> a
<> UnderLambda
l) (SeqArg
s SeqArg -> SeqArg -> SeqArg
forall a. Semigroup a => a -> a -> a
<> SeqArg
t)
instance Monoid Occurs where
mempty :: Occurs
mempty = Int -> UnderLambda -> SeqArg -> Occurs
Occurs Int
0 UnderLambda
forall a. Monoid a => a
mempty SeqArg
forall a. Monoid a => a
mempty
mappend :: Occurs -> Occurs -> Occurs
mappend = Occurs -> Occurs -> Occurs
forall a. Semigroup a => a -> a -> a
(<>)
class HasFree a where
freeVars :: a -> Map Int Occurs
freeIn :: HasFree a => Int -> a -> Bool
freeIn :: forall a. HasFree a => Int -> a -> Bool
freeIn Int
i a
x = Int -> Map Int Occurs -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Int
i (a -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars a
x)
occursIn :: HasFree a => Int -> a -> Occurs
occursIn :: forall a. HasFree a => Int -> a -> Occurs
occursIn Int
i a
x = Occurs -> Maybe Occurs -> Occurs
forall a. a -> Maybe a -> a
fromMaybe Occurs
forall a. Monoid a => a
mempty (Maybe Occurs -> Occurs) -> Maybe Occurs -> Occurs
forall a b. (a -> b) -> a -> b
$ Int -> Map Int Occurs -> Maybe Occurs
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Int
i (a -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars a
x)
instance HasFree Int where
freeVars :: Int -> Map Int Occurs
freeVars Int
x = Int -> Occurs -> Map Int Occurs
forall k a. k -> a -> Map k a
Map.singleton Int
x Occurs
once
instance HasFree a => HasFree [a] where
freeVars :: [a] -> Map Int Occurs
freeVars [a]
xs = (Occurs -> Occurs -> Occurs) -> [Map Int Occurs] -> Map Int Occurs
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
(a -> a -> a) -> f (Map k a) -> Map k a
Map.unionsWith Occurs -> Occurs -> Occurs
forall a. Monoid a => a -> a -> a
mappend ([Map Int Occurs] -> Map Int Occurs)
-> [Map Int Occurs] -> Map Int Occurs
forall a b. (a -> b) -> a -> b
$ (a -> Map Int Occurs) -> [a] -> [Map Int Occurs]
forall a b. (a -> b) -> [a] -> [b]
map a -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars [a]
xs
instance (HasFree a, HasFree b) => HasFree (a, b) where
freeVars :: (a, b) -> Map Int Occurs
freeVars (a
x, b
y) = (Occurs -> Occurs -> Occurs)
-> Map Int Occurs -> Map Int Occurs -> Map Int Occurs
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
Map.unionWith Occurs -> Occurs -> Occurs
forall a. Monoid a => a -> a -> a
mappend (a -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars a
x) (b -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars b
y)
data Binder a = Binder Int a
instance HasFree a => HasFree (Binder a) where
freeVars :: Binder a -> Map Int Occurs
freeVars (Binder Int
0 a
x) = a -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars a
x
freeVars (Binder Int
k a
x) = (Int -> Occurs -> Bool) -> Map Int Occurs -> Map Int Occurs
forall k a. (k -> a -> Bool) -> Map k a -> Map k a
Map.filterWithKey (\ Int
k Occurs
_ -> Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>= Int
0) (Map Int Occurs -> Map Int Occurs)
-> Map Int Occurs -> Map Int Occurs
forall a b. (a -> b) -> a -> b
$ (Int -> Int) -> Map Int Occurs -> Map Int Occurs
forall k1 k2 a. (k1 -> k2) -> Map k1 a -> Map k2 a
Map.mapKeysMonotonic (Int -> Int -> Int
forall a. Num a => a -> a -> a
subtract Int
k) (Map Int Occurs -> Map Int Occurs)
-> Map Int Occurs -> Map Int Occurs
forall a b. (a -> b) -> a -> b
$ a -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars a
x
newtype InSeq a = InSeq a
instance HasFree a => HasFree (InSeq a) where
freeVars :: InSeq a -> Map Int Occurs
freeVars (InSeq a
x) = Occurs -> Occurs
inSeq (Occurs -> Occurs) -> Map Int Occurs -> Map Int Occurs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> a -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars a
x
instance HasFree TTerm where
freeVars :: TTerm -> Map Int Occurs
freeVars = \case
TDef{} -> Map Int Occurs
forall k a. Map k a
Map.empty
TLit{} -> Map Int Occurs
forall k a. Map k a
Map.empty
TCon{} -> Map Int Occurs
forall k a. Map k a
Map.empty
TPrim{} -> Map Int Occurs
forall k a. Map k a
Map.empty
TUnit{} -> Map Int Occurs
forall k a. Map k a
Map.empty
TSort{} -> Map Int Occurs
forall k a. Map k a
Map.empty
TErased{} -> Map Int Occurs
forall k a. Map k a
Map.empty
TError{} -> Map Int Occurs
forall k a. Map k a
Map.empty
TVar Int
i -> Int -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars Int
i
TApp (TPrim TPrim
PSeq) [TVar Int
x, TTerm
b] -> (InSeq Int, TTerm) -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars (Int -> InSeq Int
forall a. a -> InSeq a
InSeq Int
x, TTerm
b)
TApp TTerm
f [TTerm]
ts -> (TTerm, [TTerm]) -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars (TTerm
f, [TTerm]
ts)
TLam TTerm
b -> Occurs -> Occurs
underLambda (Occurs -> Occurs) -> Map Int Occurs -> Map Int Occurs
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Binder TTerm -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars (Int -> TTerm -> Binder TTerm
forall a. Int -> a -> Binder a
Binder Int
1 TTerm
b)
TLet TTerm
e TTerm
b -> (TTerm, Binder TTerm) -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars (TTerm
e, Int -> TTerm -> Binder TTerm
forall a. Int -> a -> Binder a
Binder Int
1 TTerm
b)
TCase Int
i CaseInfo
_ TTerm
d [TAlt]
bs -> (Int, (TTerm, [TAlt])) -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars (Int
i, (TTerm
d, [TAlt]
bs))
TCoerce TTerm
t -> TTerm -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars TTerm
t
instance HasFree TAlt where
freeVars :: TAlt -> Map Int Occurs
freeVars = \case
TACon QName
_ Int
i TTerm
b -> Binder TTerm -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars (Int -> TTerm -> Binder TTerm
forall a. Int -> a -> Binder a
Binder Int
i TTerm
b)
TALit Literal
_ TTerm
b -> TTerm -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars TTerm
b
TAGuard TTerm
g TTerm
b -> (TTerm, TTerm) -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars (TTerm
g, TTerm
b)
tryStrengthen :: (HasFree a, Subst a) => Int -> a -> Maybe a
tryStrengthen :: forall a. (HasFree a, Subst a) => Int -> a -> Maybe a
tryStrengthen Int
n a
t =
case Map Int Occurs -> Maybe ((Int, Occurs), Map Int Occurs)
forall k a. Map k a -> Maybe ((k, a), Map k a)
Map.minViewWithKey (a -> Map Int Occurs
forall a. HasFree a => a -> Map Int Occurs
freeVars a
t) of
Just ((Int
i, Occurs
_), Map Int Occurs
_) | Int
i Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
< Int
n -> Maybe a
forall a. Maybe a
Nothing
Maybe ((Int, Occurs), Map Int Occurs)
_ -> a -> Maybe a
forall a. a -> Maybe a
Just (a -> Maybe a) -> a -> Maybe a
forall a b. (a -> b) -> a -> b
$ Substitution' (SubstArg a) -> a -> a
forall a. Subst a => Substitution' (SubstArg a) -> a -> a
applySubst (Impossible -> Int -> Substitution' (SubstArg a)
forall a. Impossible -> Int -> Substitution' a
strengthenS Impossible
HasCallStack => Impossible
impossible Int
n) a
t