{-# LANGUAGE MultiParamTypeClasses,
TypeFamilies,
UndecidableInstances #-}
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)
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)
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
(||)
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