{-# LANGUAGE PatternSynonyms #-}
{-|
Module      : Parsley.Internal.Backend.Analysis.Coins
Description : Coins analysis.
License     : BSD-3-Clause
Maintainer  : Jamie Willis
Stability   : experimental

Implements the analysis path required to determine how many tokens of input a given parser
is known to consume at /least/ in order to successfully execute. This provides the needed
metadata to perform the piggybank algorithm in the machine (see
"Parsley.Internal.Backend.Machine.Types.Context" for more information.)

@since 1.5.0.0
-}
module Parsley.Internal.Backend.Analysis.Coins (coinsNeeded, reclaimable) where

import Data.Bifunctor                   (first)
import Parsley.Internal.Backend.Machine (Instr(..), MetaInstr(..), Handler(..), Coins, plus1, minCoins, pattern Zero, minus, items)
import Parsley.Internal.Common.Indexed  (cata4, Fix4, Const4(..))

{-|
Calculate the number of tokens that will be consumed by a given machine.

@since 1.5.0.0
-}
coinsNeeded :: Fix4 (Instr o) xs n r a -> Coins
coinsNeeded :: forall o (xs :: [Type]) (n :: Nat) r a.
Fix4 (Instr o) xs n r a -> Coins
coinsNeeded = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
       (l :: k4).
Const4 a i j k5 l -> a
getConst4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall {k} {k1} {k2} {k3} a (i :: k) (j :: k1) (k4 :: k2)
       (l :: k3).
a -> Const4 a i j k4 l
Const4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o (xs :: [Type]) (n :: Nat) r a.
Bool -> Instr o (Const4 (Coins, Bool)) xs n r a -> (Coins, Bool)
alg Bool
True)

{-|
Calculate the number of tokens can be reclaimed by a lookAhead

@since 1.7.2.0
-}
reclaimable :: Fix4 (Instr o) xs n r a -> Coins
reclaimable :: forall o (xs :: [Type]) (n :: Nat) r a.
Fix4 (Instr o) xs n r a -> Coins
reclaimable = forall a b. (a, b) -> a
fst forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
       (l :: k4).
Const4 a i j k5 l -> a
getConst4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 (forall {k} {k1} {k2} {k3} a (i :: k) (j :: k1) (k4 :: k2)
       (l :: k3).
a -> Const4 a i j k4 l
Const4 forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall o (xs :: [Type]) (n :: Nat) r a.
Bool -> Instr o (Const4 (Coins, Bool)) xs n r a -> (Coins, Bool)
alg Bool
False)

algCatch :: (Coins, Bool) -> (Coins, Bool) -> (Coins, Bool)
-- if either of the two halves have an empty, then skip it
algCatch :: (Coins, Bool) -> (Coins, Bool) -> (Coins, Bool)
algCatch (Coins, Bool)
k (Coins
Zero, Bool
True) = (Coins, Bool)
k
algCatch (Coins
Zero, Bool
True) (Coins, Bool)
k = (Coins, Bool)
k
-- take the smaller of the two branches
algCatch (Coins
k1, Bool
_) (Coins
k2, Bool
_) = (Coins -> Coins -> Coins
minCoins Coins
k1 Coins
k2, Bool
False)

algHandler :: Handler o (Const4 (Coins, Bool)) xs n r a -> (Coins, Bool)
algHandler :: forall o (xs :: [Type]) (n :: Nat) r a.
Handler o (Const4 (Coins, Bool)) xs n r a -> (Coins, Bool)
algHandler (Same Bool
_ Const4 (Coins, Bool) xs1 n r a
yes Bool
_ Const4 (Coins, Bool) (o : xs1) n r a
no) = (Coins, Bool) -> (Coins, Bool) -> (Coins, Bool)
algCatch (forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
       (l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (Coins, Bool) xs1 n r a
yes) (forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
       (l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (Coins, Bool) (o : xs1) n r a
no)
algHandler (Always Bool
_ Const4 (Coins, Bool) (o : xs1) n r a
k) = forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
       (l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (Coins, Bool) (o : xs1) n r a
k

-- Bool represents if an empty is found in a branch (of a Catch)
-- This helps to get rid of `min` being used for `Try` where min is always 0
-- (The input is needed to /succeed/, so if one branch is doomed to fail it doesn't care about coins)
alg :: Bool -> Instr o (Const4 (Coins, Bool)) xs n r a -> (Coins, Bool)
-- All of these move control flow to somewhere else, and this means that there can be no factoring of
-- input across them, return or not: the properties of the foreign call are not known.
alg :: forall o (xs :: [Type]) (n :: Nat) r a.
Bool -> Instr o (Const4 (Coins, Bool)) xs n r a -> (Coins, Bool)
alg Bool
_     Instr o (Const4 (Coins, Bool)) xs n r a
Ret                                       = (Coins
Zero, Bool
False)
alg Bool
_     Call{}                                    = (Coins
Zero, Bool
False)
alg Bool
_     Iter{}                                    = (Coins
Zero, Bool
False)
alg Bool
_     Join{}                                    = (Coins
Zero, Bool
False) -- this is zero because a DrainCoins is generated just in front!
alg Bool
_     Instr o (Const4 (Coins, Bool)) xs n r a
Empt                                      = (Coins
Zero, Bool
True)
-- all of these instructions have no effect on the coins of their continuation, and are just transitive
alg Bool
_     (Push Defunc x
_ (Const4 (Coins, Bool)
k))                       = (Coins, Bool)
k
alg Bool
_     (Pop (Const4 (Coins, Bool)
k))                          = (Coins, Bool)
k
alg Bool
_     (Lift2 Defunc (x -> y -> z)
_ (Const4 (Coins, Bool)
k))                      = (Coins, Bool)
k
alg Bool
_     (Commit (Const4 (Coins, Bool)
k))                       = (Coins, Bool)
k
alg Bool
_     (Tell (Const4 (Coins, Bool)
k))                         = (Coins, Bool)
k
alg Bool
_     (Seek (Const4 (Coins, Bool)
k))                         = (Coins, Bool)
k
alg Bool
_     (MkJoin ΦVar x
_ Const4 (Coins, Bool) (x : xs) n r a
_ (Const4 (Coins, Bool)
k))                   = (Coins, Bool)
k
alg Bool
_     (Swap (Const4 (Coins, Bool)
k))                         = (Coins, Bool)
k
alg Bool
_     (Dup (Const4 (Coins, Bool)
k))                          = (Coins, Bool)
k
alg Bool
_     (Make ΣVar x
_ Access
_ (Const4 (Coins, Bool)
k))                     = (Coins, Bool)
k
alg Bool
_     (Get ΣVar x
_ Access
_ (Const4 (Coins, Bool)
k))                      = (Coins, Bool)
k
alg Bool
_     (SelectPos PosSelector
_ (Const4 (Coins, Bool)
k))                  = (Coins, Bool)
k
alg Bool
_     (LogEnter String
_ (Const4 (Coins, Bool)
k))                   = (Coins, Bool)
k
alg Bool
_     (LogExit String
_ (Const4 (Coins, Bool)
k))                    = (Coins, Bool)
k
alg Bool
_     (MetaInstr (AddCoins Coins
_) (Const4 (Coins, Bool)
k))       = (Coins, Bool)
k
-- cannot allow factoring through a put, because it could stop it from executing
-- but this is done in code gen via a Block, which can be disabled
alg Bool
_     (Put ΣVar x
_ Access
_ (Const4 (Coins, Bool)
k))                      = (Coins, Bool)
k
-- reading a character obviously contributes a single coin to the total along with its predicate
alg Bool
_     (Sat CharPred
p (Const4 (Coins, Bool)
k))                        = forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (CharPred -> Coins -> Coins
plus1 CharPred
p) (Coins, Bool)
k
alg Bool
_     (Catch Const4 (Coins, Bool) xs ('Succ n) r a
k Handler o (Const4 (Coins, Bool)) (o : xs) n r a
h)                               = (Coins, Bool) -> (Coins, Bool) -> (Coins, Bool)
algCatch (forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
       (l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (Coins, Bool) xs ('Succ n) r a
k) (forall o (xs :: [Type]) (n :: Nat) r a.
Handler o (Const4 (Coins, Bool)) xs n r a -> (Coins, Bool)
algHandler Handler o (Const4 (Coins, Bool)) (o : xs) n r a
h)
alg Bool
_     (Case Const4 (Coins, Bool) (x : xs1) n r a
p Const4 (Coins, Bool) (y : xs1) n r a
q)                                = (Coins, Bool) -> (Coins, Bool) -> (Coins, Bool)
algCatch (forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
       (l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (Coins, Bool) (x : xs1) n r a
p) (forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
       (l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (Coins, Bool) (y : xs1) n r a
q)
alg Bool
_     (Choices [Defunc (x -> Bool)]
_ [Const4 (Coins, Bool) xs1 n r a]
ks Const4 (Coins, Bool) xs1 n r a
def)                        = forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((Coins, Bool) -> (Coins, Bool) -> (Coins, Bool)
algCatch forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
       (l :: k4).
Const4 a i j k5 l -> a
getConst4) (forall {k1} {k2} {k3} {k4} a (i :: k1) (j :: k2) (k5 :: k3)
       (l :: k4).
Const4 a i j k5 l -> a
getConst4 Const4 (Coins, Bool) xs1 n r a
def) [Const4 (Coins, Bool) xs1 n r a]
ks
-- as these coins are refunded in `k`, they should be deducted from the required coins for `k`
alg Bool
_     (MetaInstr (RefundCoins Int
n) (Const4 (Coins, Bool)
k))    = forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (Coins -> Int -> Coins
`minus` Int
n) (Coins, Bool)
k -- TODO: minus could actually keep the predicate knowledge for intersection?
-- we want these propagated out so that they commute across a factored boundary
alg Bool
_     (MetaInstr (DrainCoins Int
n) Const4 (Coins, Bool) xs n r a
_)              = (Int -> Coins
items Int
n, Bool
False)
-- no point in propagating forward, these are at the front of a binding
alg Bool
_     (MetaInstr (GiveBursary Int
_) Const4 (Coins, Bool) xs n r a
_)             = (Coins
Zero, Bool
False)
-- this is the instruction that actions a cut by blocking all coins from traversing it
-- however, this can be disabled when processing a lookahead, unless its strong
alg Bool
False (MetaInstr (BlockCoins Bool
False) (Const4 (Coins, Bool)
k)) = (Coins, Bool)
k
alg Bool
_  (MetaInstr BlockCoins{} (Const4 (Coins, Bool)
k))          = forall (p :: Type -> Type -> Type) a b c.
Bifunctor p =>
(a -> b) -> p a c -> p b c
first (forall a b. a -> b -> a
const Coins
Zero) (Coins, Bool)
k