content: {-# 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 = ($ sing) . getStack . cata4 (RelevancyStack . 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 { getStack :: SNat (Length xs) -> Vec (Length xs) Bool }
  
  zipRelevancy :: Vec n Bool -> Vec n Bool -> Vec n Bool
  zipRelevancy = zipWithVec (||)
  
  -- 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 Ret                _         = VCons True VNil
  alg (Push _ k)         n         = let VCons _ xs = getStack k (SSucc n) in xs
  alg (Pop k)            (SSucc n) = VCons False (getStack k n)
  alg (Lift2 _ k)        (SSucc n) = let VCons rel xs = getStack k n in VCons rel (VCons rel xs)
  alg (Sat _ k)          n         = let VCons _ xs = getStack k (SSucc n) in xs
  alg (Call _ k)         n         = let VCons _ xs = getStack k (SSucc n) in xs
  alg Empt               n         = replicateVec n False
  alg (Commit k)         n         = getStack k n
  alg (Catch k _)        n         = getStack k n
  alg (Tell k)           n         = let VCons _ xs = getStack k (SSucc n) in xs
  alg (Seek k)           (SSucc n) = VCons True (getStack k n)
  alg (Case p q)         n         = VCons True (let VCons _ xs = zipRelevancy (getStack p n) (getStack q n) in xs)
  alg (Choices _ ks def) (SSucc n) = VCons True (foldr (zipRelevancy . (`getStack` n)) (getStack def n) ks)
  alg (Iter _ _ h)       n         = let VCons _ xs = algHandler h (SSucc n) in xs
  alg (Join _)           (SSucc n) = VCons True (replicateVec n False)
  alg (MkJoin _ b _)     n         = let VCons _ xs = getStack b (SSucc n) in xs
  alg (Swap k)           n         = let VCons rel1 (VCons rel2 xs) = getStack k n in VCons rel2 (VCons rel1 xs)
  alg (Dup k)            n         = let VCons rel1 (VCons rel2 xs) = getStack k (SSucc n) in VCons (rel1 || rel2) xs
  alg (Make _ _ k)       (SSucc n) = VCons False (getStack k n)
  alg (Get _ _ k)        n         = let VCons _ xs = getStack k (SSucc n) in xs
  alg (Put _ _ k)        (SSucc n) = VCons False (getStack k n)
  alg (SelectPos _ k)    n         = let VCons _ xs = getStack k (SSucc n) in xs
  alg (LogEnter _ k)     n         = getStack k n
  alg (LogExit _ k)      n         = getStack k n
  alg (MetaInstr _ k)    n         = getStack k n
  
  algHandler :: Handler o RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
  algHandler (Same _ yes _ no) (SSucc n) = VCons True (let VCons _ xs = zipRelevancy (VCons False (getStack yes n)) (getStack no (SSucc n)) in xs)
  algHandler (Always _ k) n = getStack k n
  