{-# LANGUAGE MultiParamTypeClasses,
TypeFamilies,
UndecidableInstances #-}
module Parsley.Internal.Backend.InstructionAnalyser (coinsNeeded, relevancy, Length) where
import Data.Kind (Type)
import Parsley.Internal.Backend.Machine (Instr(..), MetaInstr(..))
import Parsley.Internal.Common.Indexed (cata4, Fix4, Const4(..))
import Parsley.Internal.Common.Vec (Vec(..), Nat(..), SNat(..), SingNat(..), zipWithVec, replicateVec)
coinsNeeded :: Fix4 (Instr o) xs n r a -> Int
coinsNeeded :: Fix4 (Instr o) xs n r a -> Int
coinsNeeded = (Int, Bool) -> Int
forall a b. (a, b) -> a
fst ((Int, Bool) -> Int)
-> (Fix4 (Instr o) xs n r a -> (Int, Bool))
-> Fix4 (Instr o) xs n r a
-> Int
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 (Int, Bool) xs n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 (Const4 (Int, Bool) xs n r a -> (Int, Bool))
-> (Fix4 (Instr o) xs n r a -> Const4 (Int, Bool) xs n r a)
-> Fix4 (Instr o) xs n r a
-> (Int, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall (i' :: [Type]) (j' :: Nat) k'.
Instr o (Const4 (Int, Bool)) i' j' k' a
-> Const4 (Int, Bool) i' j' k' a)
-> Fix4 (Instr o) xs n r a -> Const4 (Int, Bool) 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 ((Int, Bool) -> Const4 (Int, Bool) i' j' k' a
forall k1 k2 k3 k5 a (i :: k1) (j :: k2) (k4 :: k3) (l :: k5).
a -> Const4 a i j k4 l
Const4 ((Int, Bool) -> Const4 (Int, Bool) i' j' k' a)
-> (Instr o (Const4 (Int, Bool)) i' j' k' a -> (Int, Bool))
-> Instr o (Const4 (Int, Bool)) i' j' k' a
-> Const4 (Int, Bool) i' j' k' a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Instr o (Const4 (Int, Bool)) i' j' k' a -> (Int, Bool)
forall rep (o :: rep) (xs :: [Type]) (n :: Nat) r a.
Instr o (Const4 (Int, Bool)) xs n r a -> (Int, Bool)
alg)
where
algCatch :: (Int, Bool) -> (Int, Bool) -> (Int, Bool)
algCatch :: (Int, Bool) -> (Int, Bool) -> (Int, Bool)
algCatch (Int, Bool)
k (Int
_, Bool
True) = (Int, Bool)
k
algCatch (Int
_, Bool
True) (Int, Bool)
k = (Int, Bool)
k
algCatch (Int
k1, Bool
_) (Int
k2, Bool
_) = (Int -> Int -> Int
forall a. Ord a => a -> a -> a
min Int
k1 Int
k2, Bool
False)
alg :: Instr o (Const4 (Int, Bool)) xs n r a -> (Int, Bool)
alg :: Instr o (Const4 (Int, Bool)) xs n r a -> (Int, Bool)
alg Instr o (Const4 (Int, Bool)) xs n r a
Ret = (Int
0, Bool
False)
alg (Push Defunc x
_ (Const4 (Int, Bool)
k)) = ((Int, Bool) -> Int
forall a b. (a, b) -> a
fst (Int, Bool)
k, Bool
False)
alg (Pop Const4 (Int, Bool) xs n r a
k) = Const4 (Int, Bool) xs n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) xs n r a
k
alg (Lift2 Defunc (x -> y -> z)
_ Const4 (Int, Bool) (z : xs) n r a
k) = Const4 (Int, Bool) (z : xs) n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) (z : xs) n r a
k
alg (Sat Defunc (Char -> Bool)
_ (Const4 (Int, Bool)
k)) = ((Int, Bool) -> Int
forall a b. (a, b) -> a
fst (Int, Bool)
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1, (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd (Int, Bool)
k)
alg (Call MVar x
_ (Const4 (Int, Bool)
k)) = (Int
0, (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd (Int, Bool)
k)
alg (Jump MVar r
_) = (Int
0, Bool
False)
alg Instr o (Const4 (Int, Bool)) xs n r a
Empt = (Int
0, Bool
True)
alg (Commit Const4 (Int, Bool) xs n r a
k) = Const4 (Int, Bool) xs n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) xs n r a
k
alg (Catch Const4 (Int, Bool) xs ('Succ n) r a
k Const4 (Int, Bool) (o : xs) n r a
h) = (Int, Bool) -> (Int, Bool) -> (Int, Bool)
algCatch (Const4 (Int, Bool) xs ('Succ n) r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) xs ('Succ n) r a
k) (Const4 (Int, Bool) (o : xs) n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) (o : xs) n r a
h)
alg (Tell Const4 (Int, Bool) (o : xs) n r a
k) = Const4 (Int, Bool) (o : xs) n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) (o : xs) n r a
k
alg (Seek Const4 (Int, Bool) xs n r a
k) = Const4 (Int, Bool) xs n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) xs n r a
k
alg (Case Const4 (Int, Bool) (x : xs) n r a
p Const4 (Int, Bool) (y : xs) n r a
q) = (Int, Bool) -> (Int, Bool) -> (Int, Bool)
algCatch (Const4 (Int, Bool) (x : xs) n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) (x : xs) n r a
p) (Const4 (Int, Bool) (y : xs) n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) (y : xs) n r a
q)
alg (Choices [Defunc (x -> Bool)]
_ [Const4 (Int, Bool) xs n r a]
ks Const4 (Int, Bool) xs n r a
def) = (Const4 (Int, Bool) xs n r a -> (Int, Bool) -> (Int, Bool))
-> (Int, Bool) -> [Const4 (Int, Bool) xs n r a] -> (Int, Bool)
forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Int, Bool) -> (Int, Bool) -> (Int, Bool)
algCatch ((Int, Bool) -> (Int, Bool) -> (Int, Bool))
-> (Const4 (Int, Bool) xs n r a -> (Int, Bool))
-> Const4 (Int, Bool) xs n r a
-> (Int, Bool)
-> (Int, Bool)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Const4 (Int, Bool) xs n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4) (Const4 (Int, Bool) xs n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) xs n r a
def) [Const4 (Int, Bool) xs n r a]
ks
alg (Iter MVar Void
_ Const4 (Int, Bool) '[] One Void a
_ (Const4 (Int, Bool)
k)) = (Int
0, (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd (Int, Bool)
k)
alg (Join ΦVar x
_) = (Int
0, Bool
False)
alg (MkJoin ΦVar x
_ (Const4 (Int, Bool)
b) (Const4 (Int, Bool)
k)) = ((Int, Bool) -> Int
forall a b. (a, b) -> a
fst (Int, Bool)
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ (Int, Bool) -> Int
forall a b. (a, b) -> a
fst (Int, Bool)
b, (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd (Int, Bool)
k Bool -> Bool -> Bool
|| (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd (Int, Bool)
b)
alg (Swap Const4 (Int, Bool) (x : y : xs) n r a
k) = Const4 (Int, Bool) (x : y : xs) n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) (x : y : xs) n r a
k
alg (Dup Const4 (Int, Bool) (x : x : xs) n r a
k) = Const4 (Int, Bool) (x : x : xs) n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) (x : x : xs) n r a
k
alg (Make ΣVar x
_ Access
_ Const4 (Int, Bool) xs n r a
k) = Const4 (Int, Bool) xs n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) xs n r a
k
alg (Get ΣVar x
_ Access
_ Const4 (Int, Bool) (x : xs) n r a
k) = Const4 (Int, Bool) (x : xs) n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) (x : xs) n r a
k
alg (Put ΣVar x
_ Access
_ Const4 (Int, Bool) xs n r a
k) = Const4 (Int, Bool) xs n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) xs n r a
k
alg (LogEnter String
_ Const4 (Int, Bool) xs ('Succ ('Succ n)) r a
k) = Const4 (Int, Bool) xs ('Succ ('Succ n)) r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) xs ('Succ ('Succ n)) r a
k
alg (LogExit String
_ Const4 (Int, Bool) xs n r a
k) = Const4 (Int, Bool) xs n r a -> (Int, Bool)
forall a k1 (i :: k1) k2 (j :: k2) k3 (k4 :: k3) k5 (l :: k5).
Const4 a i j k4 l -> a
getConst4 Const4 (Int, Bool) xs n r a
k
alg (MetaInstr (AddCoins Int
_) (Const4 (Int, Bool)
k)) = (Int, Bool)
k
alg (MetaInstr (RefundCoins Int
n) (Const4 (Int, Bool)
k)) = (Int -> Int -> Int
forall a. Ord a => a -> a -> a
max ((Int, Bool) -> Int
forall a b. (a, b) -> a
fst (Int, Bool)
k Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
n) Int
0, (Int, Bool) -> Bool
forall a b. (a, b) -> b
snd (Int, Bool)
k)
alg (MetaInstr (DrainCoins Int
_) (Const4 (Int, Bool)
k)) = ((Int, Bool) -> Int
forall a b. (a, b) -> a
fst (Int, Bool)
k, Bool
False)
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 }
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 rep (o :: rep) (xs :: [Type]) (n :: Nat) r a.
Instr o RelevancyStack xs n r a
-> SNat (Length xs) -> Vec (Length xs) Bool
alg)
where
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 One 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 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 '[] One Void a
_ 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 (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 (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