{-# 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) -- These were refunded, so deduct
    alg (MetaInstr (DrainCoins Int
_) (Const4 (Int, Bool)
k))  = ((Int, Bool) -> Int
forall a b. (a, b) -> a
fst (Int, Bool)
k, Bool
False)

{- TODO
  Live Value Analysis
  -------------------

  This analysis is designed to clean up dead registers:
    * Instead of the state laws on the Combinator AST, this should catch these cases
    * By performing it here we have ready access to the control flow information
    * We'll perform global register analysis

  State Laws:
    * get *> get = get = get <* get
    * put (pure x) *> get = put (pure x) *> pure x
    * put get = pure ()
    * put x *> put (pure y) = x *> put (pure y) = put x <* put (pure y)
    -->
    * Get . Pop . Get = Get = Get . Get . Pop -- Captured by relevancy analysis
    * Get . Get = Get . Dup Subsumes the above (Dup . Pop = id, Dup . Swap = Dup)
    * px . Put . Push () . Pop . Get = px . Dup . Put . Push () . Pop -- ??? (this law is better than above)
    * Get . Put . Push () = Push () -- ??? Improved relevancy analysis?
    * px . Put . Push () . Pop . py . Put . Push () = px . Pop . Push () . Pop . py . Put . Push () = px . Put . Push () . py . Put . Push () . Pop -- Captured by dead register analysis

  Best case scenario is that we can capture all of the above optimisations
  without a need to explicitly implement them.

  Idea 1) recurse through the machine and mark branches with their liveIn set
          if a register is not liveIn after a Put instruction it can be removed
          Get r gens r
          Put r kills r
  Idea 2) recurse through the machine and collect relevancy data:
          a value on the stack is relevant if it is consumed by `Lift2` or `Case`, etc
          it is irrelevant if consumed by Pop
          if Get produces an irrelevant operand, it can be replaced by Push BOTTOM
          Dup disjoins the relevancy of the top two elements of the stack
          Swap switches the relevancy of the top two elements of the stack
  Idea 3) recurse through the machine and collect everUsed information
          if a register is never used, then the Make instruction can be removed
-}

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
(||)

    -- 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 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