{-# LANGUAGE MultiParamTypeClasses,
             TypeFamilies,
             UndecidableInstances #-}
{-|
Module      : Parsley.Internal.Backend.Analysis.Relevancy
Description : Value relevancy analysis.
License     : BSD-3-Clause
Maintainer  : Jamie Willis
Stability   : experimental

Exposes an analysis that can determine whether each of the values present on the stack for a
given machine are actually used or not. This information may be useful in the future to calculate
whether a register is "dead" or not.

@since 1.5.0.0
-}
module Parsley.Internal.Backend.Analysis.Relevancy (relevancy, Length) where

import Data.Kind                        (Type)
import Parsley.Internal.Backend.Machine (Instr(..), Handler(..))
import Parsley.Internal.Common.Indexed  (cata4, Fix4)
import Parsley.Internal.Common.Vec      (Vec(..), Nat(..), SNat(..), SingNat(..), zipWithVec, replicateVec)

{-|
Provides a conservative estimate on whether or not each of the elements of the stack on
entry to a machine are actually used in the computation.

@since 1.5.0.0
-}
relevancy :: SingNat (Length xs) => Fix4 (Instr o) xs n r a -> Vec (Length xs) Bool
relevancy :: forall (xs :: [Type]) o (n :: Nat) r a.
SingNat (Length xs) =>
Fix4 (Instr o) xs n r a -> Vec (Length xs) Bool
relevancy = (forall a b. (a -> b) -> a -> b
$ forall (n :: Nat). SingNat n => SNat n
sing) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (f :: ([Type] -> Nat -> Type -> Type -> Type)
             -> [Type] -> Nat -> Type -> Type -> Type)
       (a :: [Type] -> Nat -> Type -> Type -> Type) (i :: [Type])
       (j :: Nat) k x.
IFunctor4 f =>
(forall (i' :: [Type]) (j' :: Nat) k'.
 f a i' j' k' x -> a i' j' k' x)
-> Fix4 f i j k x -> a i j k x
cata4 (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
(SNat (Length xs) -> Vec (Length xs) Bool)
-> RelevancyStack xs n r a
RelevancyStack forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o (xs :: [Type]) (n :: Nat) r a.
Instr o RelevancyStack xs n r a
-> SNat (Length xs) -> Vec (Length xs) Bool
alg)

{-|
Computes the length of a type-level list. Used to index a `Vec`.

@since 1.5.0.0
-}
type family Length (xs :: [Type]) :: Nat where
  Length '[] = Zero
  Length (_ : xs) = Succ (Length xs)

newtype RelevancyStack xs (n :: Nat) r a = RelevancyStack { forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack :: SNat (Length xs) -> Vec (Length xs) Bool }

zipRelevancy :: Vec n Bool -> Vec n Bool -> Vec n Bool
zipRelevancy :: forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
zipRelevancy = forall a b c (n :: Nat).
(a -> b -> c) -> Vec n a -> Vec n b -> Vec n c
zipWithVec Bool -> Bool -> Bool
(||)

-- This algorithm is over-approximating: join and ret aren't _always_ relevant
alg :: Instr o RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
alg :: forall o (xs :: [Type]) (n :: Nat) r a.
Instr o RelevancyStack xs n r a
-> SNat (Length xs) -> Vec (Length xs) Bool
alg Instr o RelevancyStack xs n r a
Ret                SNat (Length xs)
_         = forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
True forall a. Vec 'Zero a
VNil
alg (Push Defunc x
_ RelevancyStack (x : xs) n r a
k)         SNat (Length xs)
n         = let VCons Bool
_ Vec n1 Bool
Vec (Length xs) Bool
xs = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : xs) n r a
k (forall (n1 :: Nat). SNat n1 -> SNat ('Succ n1)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Pop RelevancyStack xs1 n r a
k)            (SSucc SNat n1
n) = forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
False (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs1 n r a
k SNat n1
n)
alg (Lift2 Defunc (x -> y -> z)
_ RelevancyStack (z : xs1) n r a
k)        (SSucc SNat n1
n) = let VCons Bool
rel Vec n1 Bool
Vec (Length xs1) Bool
xs = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (z : xs1) n r a
k SNat n1
n in forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
rel (forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
rel Vec (Length xs1) Bool
xs)
alg (Sat CharPred
_ RelevancyStack (Char : xs) ('Succ n1) r a
k)          SNat (Length xs)
n         = let VCons Bool
_ Vec n1 Bool
Vec (Length xs) Bool
xs = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (Char : xs) ('Succ n1) r a
k (forall (n1 :: Nat). SNat n1 -> SNat ('Succ n1)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Call MVar x
_ RelevancyStack (x : xs) ('Succ n1) r a
k)         SNat (Length xs)
n         = let VCons Bool
_ Vec n1 Bool
Vec (Length xs) Bool
xs = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : xs) ('Succ n1) r a
k (forall (n1 :: Nat). SNat n1 -> SNat ('Succ n1)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg Instr o RelevancyStack xs n r a
Empt               SNat (Length xs)
n         = forall (n :: Nat) a. SNat n -> a -> Vec n a
replicateVec SNat (Length xs)
n Bool
False
alg (Commit RelevancyStack xs n1 r a
k)         SNat (Length xs)
n         = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs n1 r a
k SNat (Length xs)
n
alg (Catch RelevancyStack xs ('Succ n) r a
k Handler o RelevancyStack (o : xs) n r a
_)        SNat (Length xs)
n         = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs ('Succ n) r a
k SNat (Length xs)
n
alg (Tell RelevancyStack (o : xs) n r a
k)           SNat (Length xs)
n         = let VCons Bool
_ Vec n1 Bool
Vec (Length xs) Bool
xs = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (o : xs) n r a
k (forall (n1 :: Nat). SNat n1 -> SNat ('Succ n1)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Seek RelevancyStack xs1 n r a
k)           (SSucc SNat n1
n) = forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
True (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs1 n r a
k SNat n1
n)
alg (Case RelevancyStack (x : xs1) n r a
p RelevancyStack (y : xs1) n r a
q)         SNat (Length xs)
n         = forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
True (let VCons Bool
_ Vec n1 Bool
Vec (Length xs1) Bool
xs = forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
zipRelevancy (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : xs1) n r a
p SNat (Length xs)
n) (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (y : xs1) n r a
q SNat (Length xs)
n) in Vec (Length xs1) Bool
xs)
alg (Choices [Defunc (x -> Bool)]
_ [RelevancyStack xs1 n r a]
ks RelevancyStack xs1 n r a
def) (SSucc SNat n1
n) = forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
True (forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
zipRelevancy forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
`getStack` SNat n1
n)) (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs1 n r a
def SNat n1
n) [RelevancyStack xs1 n r a]
ks)
alg (Iter MVar Void
_ RelevancyStack '[] One Void a
_ Handler o RelevancyStack (o : xs) n r a
h)       SNat (Length xs)
n         = let VCons Bool
_ Vec n1 Bool
Vec (Length xs) Bool
xs = forall o (xs :: [Type]) (n :: Nat) r a.
Handler o RelevancyStack xs n r a
-> SNat (Length xs) -> Vec (Length xs) Bool
algHandler Handler o RelevancyStack (o : xs) n r a
h (forall (n1 :: Nat). SNat n1 -> SNat ('Succ n1)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Join ΦVar x
_)           (SSucc SNat n1
n) = forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
True (forall (n :: Nat) a. SNat n -> a -> Vec n a
replicateVec SNat n1
n Bool
False)
alg (MkJoin ΦVar x
_ RelevancyStack (x : xs) n r a
b RelevancyStack xs n r a
_)     SNat (Length xs)
n         = let VCons Bool
_ Vec n1 Bool
Vec (Length xs) Bool
xs = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : xs) n r a
b (forall (n1 :: Nat). SNat n1 -> SNat ('Succ n1)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Swap RelevancyStack (x : y : xs1) n r a
k)           SNat (Length xs)
n         = let VCons Bool
rel1 (VCons Bool
rel2 Vec n1 Bool
Vec (Length xs1) Bool
xs) = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : y : xs1) n r a
k SNat (Length xs)
n in forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
rel2 (forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
rel1 Vec (Length xs1) Bool
xs)
alg (Dup RelevancyStack (x : x : xs1) n r a
k)            SNat (Length xs)
n         = let VCons Bool
rel1 (VCons Bool
rel2 Vec n1 Bool
Vec (Length xs1) Bool
xs) = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : x : xs1) n r a
k (forall (n1 :: Nat). SNat n1 -> SNat ('Succ n1)
SSucc SNat (Length xs)
n) in forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons (Bool
rel1 Bool -> Bool -> Bool
|| Bool
rel2) Vec (Length xs1) Bool
xs
alg (Make ΣVar x
_ Access
_ RelevancyStack xs1 n r a
k)       (SSucc SNat n1
n) = forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
False (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs1 n r a
k SNat n1
n)
alg (Get ΣVar x
_ Access
_ RelevancyStack (x : xs) n r a
k)        SNat (Length xs)
n         = let VCons Bool
_ Vec n1 Bool
Vec (Length xs) Bool
xs = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : xs) n r a
k (forall (n1 :: Nat). SNat n1 -> SNat ('Succ n1)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Put ΣVar x
_ Access
_ RelevancyStack xs1 n r a
k)        (SSucc SNat n1
n) = forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
False (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs1 n r a
k SNat n1
n)
alg (SelectPos PosSelector
_ RelevancyStack (Int : xs) n r a
k)    SNat (Length xs)
n         = let VCons Bool
_ Vec n1 Bool
Vec (Length xs) Bool
xs = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (Int : xs) n r a
k (forall (n1 :: Nat). SNat n1 -> SNat ('Succ n1)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (LogEnter String
_ RelevancyStack xs ('Succ ('Succ n1)) r a
k)     SNat (Length xs)
n         = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs ('Succ ('Succ n1)) r a
k SNat (Length xs)
n
alg (LogExit String
_ RelevancyStack xs n r a
k)      SNat (Length xs)
n         = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs n r a
k SNat (Length xs)
n
alg (MetaInstr MetaInstr n
_ RelevancyStack xs n r a
k)    SNat (Length xs)
n         = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs n r a
k SNat (Length xs)
n

algHandler :: Handler o RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
algHandler :: forall o (xs :: [Type]) (n :: Nat) r a.
Handler o RelevancyStack xs n r a
-> SNat (Length xs) -> Vec (Length xs) Bool
algHandler (Same Bool
_ RelevancyStack xs1 n r a
yes Bool
_ RelevancyStack (o : xs1) n r a
no) (SSucc SNat n1
n) = forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
True (let VCons Bool
_ Vec n1 Bool
Vec n1 Bool
xs = forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
zipRelevancy (forall a (n1 :: Nat). a -> Vec n1 a -> Vec ('Succ n1) a
VCons Bool
False (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs1 n r a
yes SNat n1
n)) (forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (o : xs1) n r a
no (forall (n1 :: Nat). SNat n1 -> SNat ('Succ n1)
SSucc SNat n1
n)) in Vec n1 Bool
xs)
algHandler (Always Bool
_ RelevancyStack (o : xs1) n r a
k) SNat (Length xs)
n = forall {k} {k} (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (o : xs1) n r a
k SNat (Length xs)
n