{-# 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
(<>)


-- Andreas, 2019-07-10: this free variable computation should be rewritten
-- in the style of TypeChecking.Free.Lazy.
-- https://github.com/agda/agda/commit/03eb3945114a4ccdb449f22d69db8d6eaa4699b8#commitcomment-34249120

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)

-- | Strenghtening.
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