{-# 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 :: Fix4 (Instr o) xs n r a -> Vec (Length xs) Bool
relevancy = ((SNat (Length xs) -> Vec (Length xs) Bool)
-> SNat (Length xs) -> Vec (Length xs) Bool
forall a b. (a -> b) -> a -> b
$ SNat (Length xs)
forall (n :: Nat). SingNat n => SNat n
sing) ((SNat (Length xs) -> Vec (Length xs) Bool)
 -> Vec (Length xs) Bool)
-> (Fix4 (Instr o) xs n r a
    -> SNat (Length xs) -> Vec (Length xs) Bool)
-> Fix4 (Instr o) xs n r a
-> Vec (Length xs) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack (RelevancyStack xs n r a
 -> SNat (Length xs) -> Vec (Length xs) Bool)
-> (Fix4 (Instr o) xs n r a -> RelevancyStack xs n r a)
-> Fix4 (Instr o) xs n r a
-> SNat (Length xs)
-> Vec (Length xs) Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (i' :: [Type]) (j' :: Nat) k'.
 Instr o RelevancyStack i' j' k' a -> RelevancyStack i' j' k' a)
-> Fix4 (Instr o) xs n r a -> RelevancyStack xs n r a
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 ((SNat (Length i') -> Vec (Length i') Bool)
-> RelevancyStack i' j' k' a
forall k k (xs :: [Type]) (n :: Nat) (r :: k) (a :: k).
(SNat (Length xs) -> Vec (Length xs) Bool)
-> RelevancyStack xs n r a
RelevancyStack ((SNat (Length i') -> Vec (Length i') Bool)
 -> RelevancyStack i' j' k' a)
-> (Instr o RelevancyStack i' j' k' a
    -> SNat (Length i') -> Vec (Length i') Bool)
-> Instr o RelevancyStack i' j' k' a
-> RelevancyStack i' j' k' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr o RelevancyStack i' j' k' a
-> SNat (Length i') -> Vec (Length i') Bool
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 { 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 :: Vec n Bool -> Vec n Bool -> Vec n Bool
zipRelevancy = (Bool -> Bool -> Bool) -> Vec n Bool -> Vec n Bool -> Vec n Bool
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 :: 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)
_         = Bool -> Vec 'Zero Bool -> Vec ('Succ 'Zero) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
True Vec 'Zero Bool
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 n Bool
xs = RelevancyStack (x : xs) n r a
-> SNat (Length (x : xs)) -> Vec (Length (x : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : xs) n r a
k (SNat (Length xs) -> SNat ('Succ (Length xs))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Pop RelevancyStack xs n r a
k)            (SSucc SNat n
n) = Bool -> Vec n Bool -> Vec ('Succ n) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
False (RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs n r a
k SNat n
SNat (Length xs)
n)
alg (Lift2 Defunc (x -> y -> z)
_ RelevancyStack (z : xs) n r a
k)        (SSucc SNat n
n) = let VCons Bool
rel Vec n Bool
xs = RelevancyStack (z : xs) n r a
-> SNat (Length (z : xs)) -> Vec (Length (z : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (z : xs) n r a
k SNat n
SNat (Length (z : xs))
n in Bool
-> Vec ('Succ (Length xs)) Bool
-> Vec ('Succ ('Succ (Length xs))) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
rel (Bool -> Vec (Length xs) Bool -> Vec ('Succ (Length xs)) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
rel Vec (Length xs) Bool
xs)
alg (Sat Defunc (Char -> Bool)
_ RelevancyStack (Char : xs) ('Succ n) r a
k)          SNat (Length xs)
n         = let VCons Bool
_ Vec n Bool
xs = RelevancyStack (Char : xs) ('Succ n) r a
-> SNat (Length (Char : xs)) -> Vec (Length (Char : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (Char : xs) ('Succ n) r a
k (SNat (Length xs) -> SNat ('Succ (Length xs))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Call MVar x
_ RelevancyStack (x : xs) ('Succ n) r a
k)         SNat (Length xs)
n         = let VCons Bool
_ Vec n Bool
xs = RelevancyStack (x : xs) ('Succ n) r a
-> SNat (Length (x : xs)) -> Vec (Length (x : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : xs) ('Succ n) r a
k (SNat (Length xs) -> SNat ('Succ (Length xs))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Jump MVar r
_)           SNat (Length xs)
_         = Vec (Length xs) Bool
forall a. Vec 'Zero a
VNil
alg Instr o RelevancyStack xs n r a
Empt               SNat (Length xs)
n         = SNat (Length xs) -> Bool -> Vec (Length xs) Bool
forall (n :: Nat) a. SNat n -> a -> Vec n a
replicateVec SNat (Length xs)
n Bool
False
alg (Commit RelevancyStack xs n r a
k)         SNat (Length xs)
n         = RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) 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 (Catch RelevancyStack xs ('Succ n) r a
k Handler o RelevancyStack (o : xs) n r a
_)        SNat (Length xs)
n         = RelevancyStack xs ('Succ n) r a
-> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) 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 n Bool
xs = RelevancyStack (o : xs) n r a
-> SNat (Length (o : xs)) -> Vec (Length (o : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (o : xs) n r a
k (SNat (Length xs) -> SNat ('Succ (Length xs))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Seek RelevancyStack xs n r a
k)           (SSucc SNat n
n) = Bool -> Vec n Bool -> Vec ('Succ n) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
True (RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs n r a
k SNat n
SNat (Length xs)
n)
alg (Case RelevancyStack (x : xs) n r a
p RelevancyStack (y : xs) n r a
q)         SNat (Length xs)
n         = Bool -> Vec (Length xs) Bool -> Vec ('Succ (Length xs)) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
True (let VCons Bool
_ Vec n Bool
xs = Vec ('Succ (Length xs)) Bool
-> Vec ('Succ (Length xs)) Bool -> Vec ('Succ (Length xs)) Bool
forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
zipRelevancy (RelevancyStack (x : xs) n r a
-> SNat (Length (x : xs)) -> Vec (Length (x : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : xs) n r a
p SNat (Length xs)
SNat (Length (x : xs))
n) (RelevancyStack (y : xs) n r a
-> SNat (Length (y : xs)) -> Vec (Length (y : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (y : xs) n r a
q SNat (Length xs)
SNat (Length (y : xs))
n) in Vec (Length xs) Bool
xs)
alg (Choices [Defunc (x -> Bool)]
_ [RelevancyStack xs n r a]
ks RelevancyStack xs n r a
def) (SSucc SNat n
n) = Bool -> Vec n Bool -> Vec ('Succ n) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
True ((RelevancyStack xs n r a -> Vec n Bool -> Vec n Bool)
-> Vec n Bool -> [RelevancyStack xs n r a] -> Vec n Bool
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (Vec n Bool -> Vec n Bool -> Vec n Bool
forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
zipRelevancy (Vec n Bool -> Vec n Bool -> Vec n Bool)
-> (RelevancyStack xs n r a -> Vec n Bool)
-> RelevancyStack xs n r a
-> Vec n Bool
-> Vec n Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
`getStack` SNat n
SNat (Length xs)
n)) (RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs n r a
def SNat n
SNat (Length xs)
n) [RelevancyStack xs n r a]
ks)
alg (Iter MVar Void
_ RelevancyStack '[] ('Succ 'Zero) Void a
_ Handler o RelevancyStack (o : xs) n r a
h)       SNat (Length xs)
n         = let VCons Bool
_ Vec n Bool
xs = Handler o RelevancyStack (o : xs) n r a
-> SNat (Length (o : xs)) -> Vec (Length (o : xs)) Bool
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 (SNat (Length xs) -> SNat ('Succ (Length xs))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Join ΦVar x
_)           (SSucc SNat n
n) = Bool -> Vec n Bool -> Vec ('Succ n) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
True (SNat n -> Bool -> Vec n Bool
forall (n :: Nat) a. SNat n -> a -> Vec n a
replicateVec SNat n
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 n Bool
xs = RelevancyStack (x : xs) n r a
-> SNat (Length (x : xs)) -> Vec (Length (x : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : xs) n r a
b (SNat (Length xs) -> SNat ('Succ (Length xs))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Swap RelevancyStack (x : y : xs) n r a
k)           SNat (Length xs)
n         = let VCons Bool
rel1 (VCons Bool
rel2 Vec n Bool
xs) = RelevancyStack (x : y : xs) n r a
-> SNat (Length (x : y : xs)) -> Vec (Length (x : y : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : y : xs) n r a
k SNat (Length xs)
SNat (Length (x : y : xs))
n in Bool
-> Vec ('Succ (Length xs)) Bool
-> Vec ('Succ ('Succ (Length xs))) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
rel2 (Bool -> Vec (Length xs) Bool -> Vec ('Succ (Length xs)) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
rel1 Vec (Length xs) Bool
xs)
alg (Dup RelevancyStack (x : x : xs) n r a
k)            SNat (Length xs)
n         = let VCons Bool
rel1 (VCons Bool
rel2 Vec n Bool
xs) = RelevancyStack (x : x : xs) n r a
-> SNat (Length (x : x : xs)) -> Vec (Length (x : x : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : x : xs) n r a
k (SNat ('Succ (Length xs)) -> SNat ('Succ ('Succ (Length xs)))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat ('Succ (Length xs))
SNat (Length xs)
n) in Bool -> Vec (Length xs) Bool -> Vec ('Succ (Length xs)) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons (Bool
rel1 Bool -> Bool -> Bool
|| Bool
rel2) Vec (Length xs) Bool
xs
alg (Make ΣVar x
_ Access
_ RelevancyStack xs n r a
k)       (SSucc SNat n
n) = Bool -> Vec n Bool -> Vec ('Succ n) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
False (RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs n r a
k SNat n
SNat (Length xs)
n)
alg (Get ΣVar x
_ Access
_ RelevancyStack (x : xs) n r a
k)        SNat (Length xs)
n         = let VCons Bool
_ Vec n Bool
xs = RelevancyStack (x : xs) n r a
-> SNat (Length (x : xs)) -> Vec (Length (x : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (x : xs) n r a
k (SNat (Length xs) -> SNat ('Succ (Length xs))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (Put ΣVar x
_ Access
_ RelevancyStack xs n r a
k)        (SSucc SNat n
n) = Bool -> Vec n Bool -> Vec ('Succ n) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
False (RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs n r a
k SNat n
SNat (Length xs)
n)
alg (SelectPos PosSelector
_ RelevancyStack (Int : xs) n r a
k)    SNat (Length xs)
n         = let VCons Bool
_ Vec n Bool
xs = RelevancyStack (Int : xs) n r a
-> SNat (Length (Int : xs)) -> Vec (Length (Int : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (Int : xs) n r a
k (SNat (Length xs) -> SNat ('Succ (Length xs))
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat (Length xs)
n) in Vec (Length xs) Bool
xs
alg (LogEnter String
_ RelevancyStack xs ('Succ ('Succ n)) r a
k)     SNat (Length xs)
n         = RelevancyStack xs ('Succ ('Succ n)) r a
-> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs ('Succ ('Succ n)) r a
k SNat (Length xs)
n
alg (LogExit String
_ RelevancyStack xs n r a
k)      SNat (Length xs)
n         = RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) 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         = RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) 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 :: Handler o RelevancyStack xs n r a
-> SNat (Length xs) -> Vec (Length xs) Bool
algHandler (Same Bool
_ RelevancyStack xs n r a
yes Bool
_ RelevancyStack (o : xs) n r a
no) (SSucc SNat n
n) = Bool -> Vec n Bool -> Vec ('Succ n) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
True (let VCons Bool
_ Vec n Bool
xs = Vec ('Succ n) Bool -> Vec ('Succ n) Bool -> Vec ('Succ n) Bool
forall (n :: Nat). Vec n Bool -> Vec n Bool -> Vec n Bool
zipRelevancy (Bool -> Vec n Bool -> Vec ('Succ n) Bool
forall a (n :: Nat). a -> Vec n a -> Vec ('Succ n) a
VCons Bool
False (RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack xs n r a
yes SNat n
SNat (Length xs)
n)) (RelevancyStack (o : xs) n r a
-> SNat (Length (o : xs)) -> Vec (Length (o : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (o : xs) n r a
no (SNat n -> SNat ('Succ n)
forall (n :: Nat). SNat n -> SNat ('Succ n)
SSucc SNat n
n)) in Vec n Bool
xs)
algHandler (Always Bool
_ RelevancyStack (o : xs) n r a
k) SNat (Length xs)
n = RelevancyStack (o : xs) n r a
-> SNat (Length (o : xs)) -> Vec (Length (o : xs)) Bool
forall (xs :: [Type]) (n :: Nat) k (r :: k) k (a :: k).
RelevancyStack xs n r a -> SNat (Length xs) -> Vec (Length xs) Bool
getStack RelevancyStack (o : xs) n r a
k SNat (Length xs)
SNat (Length (o : xs))
n