{-# LANGUAGE ImplicitParams,
             LambdaCase,
             PatternSynonyms,
             ViewPatterns #-}
{-|
Module      : Parsley.Internal.Frontend.Optimiser
Description : Combinator law optimisation.
License     : BSD-3-Clause
Maintainer  : Jamie Willis
Stability   : experimental

Exposes the `optimise` algebra, which is used for optimisations based on the laws of parsers.

@since 1.0.0.0
-}
module Parsley.Internal.Frontend.Optimiser (optimise) where

import Prelude hiding                      ((<$>))
import Parsley.Internal.Common             (Fix(In), Quapplicative(..))
import Parsley.Internal.Core.CombinatorAST (Combinator(..))
import Parsley.Internal.Core.Defunc        (Defunc(..), pattern FLIP_H, pattern COMPOSE_H, pattern FLIP_CONST, pattern UNIT)

import qualified Parsley.Internal.Opt   as Opt

pattern (:<$>:) :: Defunc (a -> b) -> Fix Combinator a -> Combinator (Fix Combinator) b
pattern f $b:<$>: :: forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
$m:<$>: :: forall {r} {b}.
Combinator (Fix Combinator) b
-> (forall {a}. Defunc (a -> b) -> Fix Combinator a -> r)
-> ((# #) -> r)
-> r
:<$>: p = In (Pure f) :<*>: p
pattern (:$>:) :: Fix Combinator a -> Defunc b -> Combinator (Fix Combinator) b
pattern p $b:$>: :: forall b a.
Fix Combinator a -> Defunc b -> Combinator (Fix Combinator) b
$m:$>: :: forall {r} {b}.
Combinator (Fix Combinator) b
-> (forall {a}. Fix Combinator a -> Defunc b -> r)
-> ((# #) -> r)
-> r
:$>: x = p :*>: In (Pure x)
pattern (:<$:) :: Defunc a -> Fix Combinator b -> Combinator (Fix Combinator) a
pattern x $b:<$: :: forall a b.
Defunc a -> Fix Combinator b -> Combinator (Fix Combinator) a
$m:<$: :: forall {r} {a}.
Combinator (Fix Combinator) a
-> (forall {b}. Defunc a -> Fix Combinator b -> r)
-> ((# #) -> r)
-> r
:<$: p = In (Pure x) :<*: p

{-|
Optimises a `Combinator` tree according to the various laws of parsers. See the source
for which laws are being utilised.

@since 1.0.0.0
-}
optimise :: (?flags :: Opt.Flags) => Combinator (Fix Combinator) a -> Fix Combinator a
optimise :: forall a.
(?flags::Flags) =>
Combinator (Fix Combinator) a -> Fix Combinator a
optimise
  | Flags -> Bool
Opt.lawBasedOptimisations ?flags::Flags
?flags = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt
  | Bool
otherwise                        = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In
  where
    opt :: Combinator (Fix Combinator) a -> Fix Combinator a
    -- DESTRUCTIVE OPTIMISATION
    -- Right Absorption Law: empty <*> u               = empty
    opt :: forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (In Combinator (Fix Combinator) (a1 -> a)
Empty :<*>: Fix Combinator a1
_)                             = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty
    -- Failure Weakening Law: u <*> empty              = u *> empty
    opt (Fix Combinator (a1 -> a)
u :<*>: In Combinator (Fix Combinator) a1
Empty)                             = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator (a1 -> a)
u forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty)
    -- Right Absorption Law: empty *> u                = empty
    opt (In Combinator (Fix Combinator) a1
Empty :*>: Fix Combinator a
_)                              = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty
    -- Right Absorption Law: empty <* u                = empty
    opt (In Combinator (Fix Combinator) a
Empty :<*: Fix Combinator b
_)                              = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty
    -- Failure Weakening Law: u <* empty               = u *> empty
    opt (Fix Combinator a
u :<*: In Combinator (Fix Combinator) b
Empty)                              = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator a
u forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty)
    -- Branch Absorption Law: branch empty p q          = empty
    opt (Branch (In Combinator (Fix Combinator) (Either a1 b)
Empty) Fix Combinator (a1 -> a)
_ Fix Combinator (b -> a)
_)                        = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty
    -- Branch Weakening Law: branch b empty empty      = b *> empty
    opt (Branch Fix Combinator (Either a1 b)
b (In Combinator (Fix Combinator) (a1 -> a)
Empty) (In Combinator (Fix Combinator) (b -> a)
Empty))               = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator (Either a1 b)
b forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty)
    -- Match Absorption Law: match _ empty _ def       = def
    opt (Match (In Combinator (Fix Combinator) a1
Empty) [Defunc (a1 -> Bool)]
_ [Fix Combinator a]
_ Fix Combinator a
def)                     = Fix Combinator a
def
    -- Match Weakening Law: match _ p (const empty) empty = p *> empty
    opt (Match Fix Combinator a1
p [Defunc (a1 -> Bool)]
_ [Fix Combinator a]
qs (In Combinator (Fix Combinator) a
Empty))
      | forall (t :: Type -> Type) a.
Foldable t =>
(a -> Bool) -> t a -> Bool
all (\case {In Combinator (Fix Combinator) a
Empty -> Bool
True; Fix Combinator a
_ -> Bool
False}) [Fix Combinator a]
qs = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator a1
p forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty)
    -- APPLICATIVE OPTIMISATION
    -- Identity Law: id <$> u                          = u
    opt (Defunc (a -> a)
ID :<$>: Fix Combinator a
u)                                   = Fix Combinator a
u
    -- Flip const optimisation: flip const <$> u       = u *> pure id
    opt (Defunc (a -> a)
FLIP_CONST :<$>: Fix Combinator a
u)                           = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator a
u forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure forall a1. Defunc (a1 -> a1)
ID))
    -- Homomorphism Law: pure f <*> pure x             = pure (f x)
    opt (Defunc (a -> a)
f :<$>: In (Pure Defunc a
x))                          = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure (forall a1 a. Defunc (a1 -> a) -> Defunc a1 -> Defunc a
APP_H Defunc (a -> a)
f Defunc a
x))
    -- NOTE: This is basically a shortcut, it can be caught by the Composition Law and Homomorphism law
    -- Functor Composition Law: f <$> (g <$> p)        = (f . g) <$> p
    opt (Defunc (a -> a)
f :<$>: In (Defunc (a -> a)
g :<$>: Fix Combinator a
p))                       = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall z x y b c a.
((x -> y -> z) ~ ((b -> c) -> (a -> b) -> a -> c)) =>
Defunc x -> Defunc y -> Defunc z
COMPOSE_H Defunc (a -> a)
f Defunc (a -> a)
g forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
:<$>: Fix Combinator a
p)
    -- Composition Law: u <*> (v <*> w)                = (.) <$> u <*> v <*> w
    opt (Fix Combinator (a1 -> a)
u :<*>: In (Fix Combinator (a1 -> a1)
v :<*>: Fix Combinator a1
w))                       = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall b c a1. Defunc ((b -> c) -> (a1 -> b) -> a1 -> c)
COMPOSE forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
:<$>: Fix Combinator (a1 -> a)
u) forall (k :: Type -> Type) a1 a.
k (a1 -> a) -> k a1 -> Combinator k a
:<*>: Fix Combinator (a1 -> a1)
v) forall (k :: Type -> Type) a1 a.
k (a1 -> a) -> k a1 -> Combinator k a
:<*>: Fix Combinator a1
w)
    -- Definition of *>
    opt (In (Defunc (a -> a1 -> a)
FLIP_CONST :<$>: Fix Combinator a
p) :<*>: Fix Combinator a1
q)              = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a
p forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: Fix Combinator a1
q)
    -- Definition of <*
    opt (In (Defunc (a -> a1 -> a)
CONST :<$>: Fix Combinator a
p) :<*>: Fix Combinator a1
q)                   = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a
p forall (k :: Type -> Type) a b. k a -> k b -> Combinator k a
:<*: Fix Combinator a1
q)
    -- Reassociation Law 1: (u *> v) <*> w             = u *> (v <*> w)
    opt (In (Fix Combinator a1
u :*>: Fix Combinator (a1 -> a)
v) :<*>: Fix Combinator a1
w)                        = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator a1
u forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator (a1 -> a)
v forall (k :: Type -> Type) a1 a.
k (a1 -> a) -> k a1 -> Combinator k a
:<*>: Fix Combinator a1
w))
    -- Interchange Law: u <*> pure x                   = pure ($ x) <*> u
    opt (Fix Combinator (a1 -> a)
u :<*>: In (Pure Defunc a1
x))                          = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a1 a. Defunc (a1 -> a) -> Defunc a1 -> Defunc a
APP_H (forall y x a b c.
((x -> y) ~ ((a -> b -> c) -> b -> a -> c)) =>
Defunc x -> Defunc y
FLIP_H forall a1. Defunc (a1 -> a1)
ID) Defunc a1
x forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
:<$>: Fix Combinator (a1 -> a)
u)
    -- Right Absorption Law: (f <$> p) *> q            = p *> q
    opt (In (Defunc (a -> a1)
_ :<$>: Fix Combinator a
p) :*>: Fix Combinator a
q)                        = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a
p forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: Fix Combinator a
q)
    -- Left Absorption Law: p <* (f <$> q)             = p <* q
    opt (Fix Combinator a
p :<*: (In (Defunc (a -> b)
_ :<$>: Fix Combinator a
q)))                      = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a
p forall (k :: Type -> Type) a b. k a -> k b -> Combinator k a
:<*: Fix Combinator a
q)
    -- Reassociation Law 2: u <*> (v <* w)             = (u <*> v) <* w
    opt (Fix Combinator (a1 -> a)
u :<*>: In (Fix Combinator a1
v :<*: Fix Combinator b
w))                        = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator (a1 -> a)
u forall (k :: Type -> Type) a1 a.
k (a1 -> a) -> k a1 -> Combinator k a
:<*>: Fix Combinator a1
v) forall (k :: Type -> Type) a b. k a -> k b -> Combinator k a
:<*: Fix Combinator b
w)
    -- Reassociation Law 3: u <*> (v $> x)             = (u <*> pure x) <* v
    opt (Fix Combinator (a1 -> a)
u :<*>: In (Fix Combinator a
v :$>: Defunc a1
x))                        = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator (a1 -> a)
u forall (k :: Type -> Type) a1 a.
k (a1 -> a) -> k a1 -> Combinator k a
:<*>: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure Defunc a1
x)) forall (k :: Type -> Type) a b. k a -> k b -> Combinator k a
:<*: Fix Combinator a
v)
    -- ALTERNATIVE OPTIMISATION
    -- Left Catch Law: pure x <|> u                    = pure x
    opt (p :: Fix Combinator a
p@(In (Pure Defunc a
_)) :<|>: Fix Combinator a
_)                      = Fix Combinator a
p
    -- Left Neutral Law: empty <|> u                   = u
    opt (In Combinator (Fix Combinator) a
Empty :<|>: Fix Combinator a
u)                             = Fix Combinator a
u
    -- Right Neutral Law: u <|> empty                  = u
    opt (Fix Combinator a
u :<|>: In Combinator (Fix Combinator) a
Empty)                             = Fix Combinator a
u
    -- Associativity Law: (u <|> v) <|> w              = u <|> (v <|> w)
    opt (In (Fix Combinator a
u :<|>: Fix Combinator a
v) :<|>: Fix Combinator a
w)                       = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a
u forall (k :: Type -> Type) a. k a -> k a -> Combinator k a
:<|>: forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator a
v forall (k :: Type -> Type) a. k a -> k a -> Combinator k a
:<|>: Fix Combinator a
w))
    -- SEQUENCING OPTIMISATION
    -- Identity law: pure x *> u                       = u
    opt (In (Pure Defunc a1
_) :*>: Fix Combinator a
u)                           = Fix Combinator a
u
    -- Identity law: (u $> x) *> v                     = u *> v
    opt (In (Fix Combinator a
u :$>: Defunc a1
_) :*>: Fix Combinator a
v)                         = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (Fix Combinator a
u forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: Fix Combinator a
v)
    -- Associativity Law: u *> (v *> w)                = (u *> v) *> w
    opt (Fix Combinator a1
u :*>: In (Fix Combinator a1
v :*>: Fix Combinator a
w))                         = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator a1
u forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: Fix Combinator a1
v) forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: Fix Combinator a
w)
    -- Identity law: u <* pure x                       = u
    opt (Fix Combinator a
u :<*: In (Pure Defunc b
_))                           = Fix Combinator a
u
    -- Identity law: u <* (v $> x)                     = u <* v
    opt (Fix Combinator a
u :<*: In (Fix Combinator a
v :$>: Defunc b
_))                         = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator a
u forall (k :: Type -> Type) a b. k a -> k b -> Combinator k a
:<*: Fix Combinator a
v)
    -- Commutativity Law: x <$ u                       = u $> x
    opt (Defunc a
x :<$: Fix Combinator b
u)                                     = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator b
u forall b a.
Fix Combinator a -> Defunc b -> Combinator (Fix Combinator) b
:$>: Defunc a
x)
    -- Associativity Law (u <* v) <* w                 = u <* (v <* w)
    opt (In (Fix Combinator a
u :<*: Fix Combinator b
v) :<*: Fix Combinator b
w)                         = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator a
u forall (k :: Type -> Type) a b. k a -> k b -> Combinator k a
:<*: forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator b
v forall (k :: Type -> Type) a b. k a -> k b -> Combinator k a
:<*: Fix Combinator b
w))
    -- Pure lookahead: lookAhead (pure x)              = pure x
    opt (LookAhead p :: Fix Combinator a
p@(In (Pure Defunc a
_)))                    = Fix Combinator a
p
    -- Dead lookahead: lookAhead empty                 = empty
    opt (LookAhead p :: Fix Combinator a
p@(In Combinator (Fix Combinator) a
Empty))                       = Fix Combinator a
p
    -- Pure negative-lookahead: notFollowedBy (pure x) = empty
    opt (NotFollowedBy (In (Pure Defunc a1
_)))                  = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty
    -- Dead negative-lookahead: notFollowedBy empty    = unit
    opt (NotFollowedBy (In Combinator (Fix Combinator) a1
Empty))                     = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure Defunc ()
UNIT)
    -- Double Negation Law: notFollowedBy . notFollowedBy = lookAhead . try . void
    opt (NotFollowedBy (In (NotFollowedBy Fix Combinator a1
p)))         = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a. k a -> Combinator k a
LookAhead (forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall (k :: Type -> Type) a. k a -> Combinator k a
Try Fix Combinator a1
p) forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure Defunc ()
UNIT))))
    -- Zero Consumption Law: notFollowedBy (try p)     = notFollowedBy p
    opt (NotFollowedBy (In (Try Fix Combinator a1
p)))                   = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a1. k a1 -> Combinator k ()
NotFollowedBy Fix Combinator a1
p)
    -- Idempotence Law: lookAhead . lookAhead          = lookAhead
    opt (LookAhead (In (LookAhead Fix Combinator a
p)))                 = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall (k :: Type -> Type) a. k a -> Combinator k a
LookAhead Fix Combinator a
p)
    -- Right Identity Law: notFollowedBy . lookAhead   = notFollowedBy
    opt (NotFollowedBy (In (LookAhead Fix Combinator a1
p)))             = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a1. k a1 -> Combinator k ()
NotFollowedBy Fix Combinator a1
p)
    -- Left Identity Law: lookAhead . notFollowedBy    = notFollowedBy
    opt (LookAhead (In (NotFollowedBy Fix Combinator a1
p)))             = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall (k :: Type -> Type) a1. k a1 -> Combinator k ()
NotFollowedBy Fix Combinator a1
p)
    -- Transparency Law: notFollowedBy (try p <|> q)   = notFollowedBy p *> notFollowedBy q
    opt (NotFollowedBy (In (In (Try Fix Combinator a1
p) :<|>: Fix Combinator a1
q)))      = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a1. k a1 -> Combinator k ()
NotFollowedBy Fix Combinator a1
p) forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a1. k a1 -> Combinator k ()
NotFollowedBy Fix Combinator a1
q))
    -- Distributivity Law: lookAhead p <|> lookAhead q = lookAhead (try p <|> q)
    opt (In (LookAhead Fix Combinator a
p) :<|>: In (LookAhead Fix Combinator a
q))      = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a. k a -> Combinator k a
LookAhead (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall (k :: Type -> Type) a. k a -> Combinator k a
Try Fix Combinator a
p) forall (k :: Type -> Type) a. k a -> k a -> Combinator k a
:<|>: Fix Combinator a
q)))
    -- Interchange Law: lookAhead (p $> x)             = lookAhead p $> x
    opt (LookAhead (In (Fix Combinator a
p :$>: Defunc a
x)))                    = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a. k a -> Combinator k a
LookAhead Fix Combinator a
p) forall b a.
Fix Combinator a -> Defunc b -> Combinator (Fix Combinator) b
:$>: Defunc a
x)
    -- Interchange law: lookAhead (f <$> p)            = f <$> lookAhead p
    opt (LookAhead (In (Defunc (a -> a)
f :<$>: Fix Combinator a
p)))                   = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Defunc (a -> a)
f forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
:<$>: forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a. k a -> Combinator k a
LookAhead Fix Combinator a
p))
    -- Absorption Law: p <*> notFollowedBy q           = (p <*> unit) <* notFollowedBy q
    opt (Fix Combinator (a1 -> a)
p :<*>: In (NotFollowedBy Fix Combinator a1
q))                 = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator (a1 -> a)
p forall (k :: Type -> Type) a1 a.
k (a1 -> a) -> k a1 -> Combinator k a
:<*>: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure Defunc ()
UNIT)) forall (k :: Type -> Type) a b. k a -> k b -> Combinator k a
:<*: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall (k :: Type -> Type) a1. k a1 -> Combinator k ()
NotFollowedBy Fix Combinator a1
q))
    -- Idempotence Law: notFollowedBy (p $> x)         = notFollowedBy p
    opt (NotFollowedBy (In (Fix Combinator a
p :$>: Defunc a1
_)))                = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a1. k a1 -> Combinator k ()
NotFollowedBy Fix Combinator a
p)
    -- Idempotence Law: notFollowedBy (f <$> p)        = notFollowedBy p
    opt (NotFollowedBy (In (Defunc (a -> a1)
_ :<$>: Fix Combinator a
p)))               = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a1. k a1 -> Combinator k ()
NotFollowedBy Fix Combinator a
p)
    -- Interchange Law: try (p $> x)                   = try p $> x
    opt (Try (In (Fix Combinator a
p :$>: Defunc a
x)))                          = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a. k a -> Combinator k a
Try Fix Combinator a
p) forall b a.
Fix Combinator a -> Defunc b -> Combinator (Fix Combinator) b
:$>: Defunc a
x)
    -- Interchange law: try (f <$> p)                  = f <$> try p
    opt (Try (In (Defunc (a -> a)
f :<$>: Fix Combinator a
p)))                         = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Defunc (a -> a)
f forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
:<$>: forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a. k a -> Combinator k a
Try Fix Combinator a
p))
    -- pure Left law: branch (pure (Left x)) p q       = p <*> pure x
    opt (Branch (In (Pure l :: Defunc (Either a1 b)
l@(forall (q :: Type -> Type) a. Quapplicative q => q a -> a
_val -> Left a1
x))) Fix Combinator (a1 -> a)
p Fix Combinator (b -> a)
_)    = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator (a1 -> a)
p forall (k :: Type -> Type) a1 a.
k (a1 -> a) -> k a1 -> Combinator k a
:<*>: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure (forall (q :: Type -> Type) a. Quapplicative q => a -> Code a -> q a
makeQ a1
x Code Q a1
qx))) where qx :: Code Q a1
qx = [||case $$(_code l) of Left x -> x||]
    -- pure Right law: branch (pure (Right x)) p q     = q <*> pure x
    opt (Branch (In (Pure r :: Defunc (Either a1 b)
r@(forall (q :: Type -> Type) a. Quapplicative q => q a -> a
_val -> Right b
x))) Fix Combinator (a1 -> a)
_ Fix Combinator (b -> a)
q)   = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator (b -> a)
q forall (k :: Type -> Type) a1 a.
k (a1 -> a) -> k a1 -> Combinator k a
:<*>: forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure (forall (q :: Type -> Type) a. Quapplicative q => a -> Code a -> q a
makeQ b
x Code Q b
qx))) where qx :: Code Q b
qx = [||case $$(_code r) of Right x -> x||]
    -- Generalised Identity law: branch b (pure f) (pure g) = either f g <$> b
    opt (Branch Fix Combinator (Either a1 b)
b (In (Pure Defunc (a1 -> a)
f)) (In (Pure Defunc (b -> a)
g)))         = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (q :: Type -> Type) a. Quapplicative q => a -> Code a -> q a
makeQ (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either (forall (q :: Type -> Type) a. Quapplicative q => q a -> a
_val Defunc (a1 -> a)
f) (forall (q :: Type -> Type) a. Quapplicative q => q a -> a
_val Defunc (b -> a)
g)) [||either $$(_code f) $$(_code g)||] forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
:<$>: Fix Combinator (Either a1 b)
b)
    -- Interchange law: branch (x *> y) p q            = x *> branch y p q
    opt (Branch (In (Fix Combinator a1
x :*>: Fix Combinator (Either a1 b)
y)) Fix Combinator (a1 -> a)
p Fix Combinator (b -> a)
q)                   = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Fix Combinator a1
x forall (k :: Type -> Type) a1 a. k a1 -> k a -> Combinator k a
:*>: forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a1 b a.
k (Either a1 b) -> k (a1 -> a) -> k (b -> a) -> Combinator k a
Branch Fix Combinator (Either a1 b)
y Fix Combinator (a1 -> a)
p Fix Combinator (b -> a)
q))
    -- Negated Branch law: branch b p empty            = branch (swapEither <$> b) empty p
    opt (Branch Fix Combinator (Either a1 b)
b Fix Combinator (a1 -> a)
p (In Combinator (Fix Combinator) (b -> a)
Empty))                        = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall (k :: Type -> Type) a1 b a.
k (Either a1 b) -> k (a1 -> a) -> k (b -> a) -> Combinator k a
Branch (forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure (forall (q :: Type -> Type) a. Quapplicative q => a -> Code a -> q a
makeQ (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a b. b -> Either a b
Right forall a b. a -> Either a b
Left) [||either Right Left||])) forall (k :: Type -> Type) a1 a.
k (a1 -> a) -> k a1 -> Combinator k a
:<*>: Fix Combinator (Either a1 b)
b)) (forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty) Fix Combinator (a1 -> a)
p)
    -- Branch Fusion law: branch (branch b empty (pure f)) empty k     = branch (g <$> b) empty k where g is a monad transforming (>>= f)
    opt (Branch (In (Branch Fix Combinator (Either a1 b)
b (In Combinator (Fix Combinator) (a1 -> Either a1 b)
Empty) (In (Pure Defunc (b -> Either a1 b)
f)))) (In Combinator (Fix Combinator) (a1 -> a)
Empty) Fix Combinator (b -> a)
k) = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a1 b a.
k (Either a1 b) -> k (a1 -> a) -> k (b -> a) -> Combinator k a
Branch (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall a (k :: Type -> Type). Defunc a -> Combinator k a
Pure (forall (q :: Type -> Type) a. Quapplicative q => a -> Code a -> q a
makeQ Either a1 b -> Either () b
g Code Q (Either a1 b -> Either () b)
qg)) forall (k :: Type -> Type) a1 a.
k (a1 -> a) -> k a1 -> Combinator k a
:<*>: Fix Combinator (Either a1 b)
b)) (forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In forall (k :: Type -> Type) a. Combinator k a
Empty) Fix Combinator (b -> a)
k)
      where
        g :: Either a1 b -> Either () b
g (Left a1
_) = forall a b. a -> Either a b
Left ()
        g (Right b
x) = case forall (q :: Type -> Type) a. Quapplicative q => q a -> a
_val Defunc (b -> Either a1 b)
f b
x of
          Left a1
_ -> forall a b. a -> Either a b
Left ()
          Right b
x -> forall a b. b -> Either a b
Right b
x
        qg :: Code Q (Either a1 b -> Either () b)
qg = [||\case Left _ -> Left ()
                      Right x -> case $$(_code f) x of
                                   Left _ -> Left ()
                                   Right y -> Right y||]
    -- Distributivity Law: f <$> branch b p q           = branch b ((f .) <$> p) ((f .) <$> q)
    opt (Defunc (a -> a)
f :<$>: In (Branch Fix Combinator (Either a1 b)
b Fix Combinator (a1 -> a)
p Fix Combinator (b -> a)
q))                     = forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall (k :: Type -> Type) a1 b a.
k (Either a1 b) -> k (a1 -> a) -> k (b -> a) -> Combinator k a
Branch Fix Combinator (Either a1 b)
b (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a1 a. Defunc (a1 -> a) -> Defunc a1 -> Defunc a
APP_H forall b c a1. Defunc ((b -> c) -> (a1 -> b) -> a1 -> c)
COMPOSE Defunc (a -> a)
f forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
:<$>: Fix Combinator (a1 -> a)
p)) (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (forall a1 a. Defunc (a1 -> a) -> Defunc a1 -> Defunc a
APP_H forall b c a1. Defunc ((b -> c) -> (a1 -> b) -> a1 -> c)
COMPOSE Defunc (a -> a)
f forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
:<$>: Fix Combinator (b -> a)
q)))
    -- pure Match law: match vs (pure x) f def          = if elem x vs then f x else def
    opt (Match (In (Pure Defunc a1
x)) [Defunc (a1 -> Bool)]
fs [Fix Combinator a]
qs Fix Combinator a
def)                 = forall (t :: Type -> Type) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\(Defunc (a1 -> Bool)
f, Fix Combinator a
q) Fix Combinator a
k -> if forall (q :: Type -> Type) a. Quapplicative q => q a -> a
_val Defunc (a1 -> Bool)
f (forall (q :: Type -> Type) a. Quapplicative q => q a -> a
_val Defunc a1
x) then Fix Combinator a
q else Fix Combinator a
k) Fix Combinator a
def (forall a b. [a] -> [b] -> [(a, b)]
zip [Defunc (a1 -> Bool)]
fs [Fix Combinator a]
qs)
    -- Distributivity Law: f <$> match vs p g def       = match vs p ((f <$>) . g) (f <$> def)
    opt (Defunc (a -> a)
f :<$>: (In (Match Fix Combinator a1
p [Defunc (a1 -> Bool)]
fs [Fix Combinator a]
qs Fix Combinator a
def)))              = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In (forall (k :: Type -> Type) a1 a.
k a1 -> [Defunc (a1 -> Bool)] -> [k a] -> k a -> Combinator k a
Match Fix Combinator a1
p [Defunc (a1 -> Bool)]
fs (forall a b. (a -> b) -> [a] -> [b]
map (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Defunc (a -> a)
f forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
:<$>:)) [Fix Combinator a]
qs) (forall a. Combinator (Fix Combinator) a -> Fix Combinator a
opt (Defunc (a -> a)
f forall b a.
Defunc (a -> b)
-> Fix Combinator a -> Combinator (Fix Combinator) b
:<$>: Fix Combinator a
def)))
    opt Combinator (Fix Combinator) a
p                                               = forall {k} (f :: (k -> Type) -> k -> Type) (a :: k).
f (Fix f) a -> Fix f a
In Combinator (Fix Combinator) a
p