module Parsley.Internal.Backend.Optimiser (optimise) where

import Data.GADT.Compare                (geq)
import Data.Typeable                    ((:~:)(Refl))
import Parsley.Internal.Backend.Machine
import Parsley.Internal.Common.Indexed

-- We'll come back here later ;)
optimise :: Instr o (Fix4 (Instr o)) xs n r a -> Fix4 (Instr o) xs n r a
optimise :: Instr o (Fix4 (Instr o)) xs n r a -> Fix4 (Instr o) xs n r a
optimise (Push Defunc x
_ (In4 (Pop Fix4 (Instr o) xs n r a
m))) = Fix4 (Instr o) xs n r a
Fix4 (Instr o) xs n r a
m
optimise (Get ΣVar x
_ Access
_ (In4 (Pop Fix4 (Instr o) xs n r a
m))) = Fix4 (Instr o) xs n r a
Fix4 (Instr o) xs n r a
m
optimise (Dup (In4 (Pop Fix4 (Instr o) xs n r a
m))) = Fix4 (Instr o) xs n r a
Fix4 (Instr o) xs n r a
m
optimise (Dup (In4 (Swap Fix4 (Instr o) (x : y : xs) n r a
m))) = Instr o (Fix4 (Instr o)) (x : xs) n r a
-> Fix4 (Instr o) (x : xs) n r a
forall k k k k
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
f (Fix4 f) i j k l -> Fix4 f i j k l
In4 (Fix4 (Instr o) (x : x : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : xs) n r a
forall rep (k :: [Type] -> Nat -> Type -> Type -> Type) x
       (xs :: [Type]) (n :: Nat) r a (o :: rep).
k (x : x : xs) n r a -> Instr o k (x : xs) n r a
Dup Fix4 (Instr o) (x : x : xs) n r a
Fix4 (Instr o) (x : y : xs) n r a
m)
optimise (Get ΣVar x
r1 Access
a (In4 (Get ΣVar x
r2 Access
_ Fix4 (Instr o) (x : x : xs) n r a
m))) | Just x :~: x
Refl <- ΣVar x
r1 ΣVar x -> ΣVar x -> Maybe (x :~: x)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` ΣVar x
r2 = Instr o (Fix4 (Instr o)) xs n r a -> Fix4 (Instr o) xs n r a
forall k k k k
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
f (Fix4 f) i j k l -> Fix4 f i j k l
In4 (ΣVar x
-> Access
-> Fix4 (Instr o) (x : xs) n r a
-> Instr o (Fix4 (Instr o)) xs n r a
forall rep x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a (o :: rep).
ΣVar x -> Access -> k (x : xs) n r a -> Instr o k xs n r a
Get ΣVar x
r1 Access
a (Instr o (Fix4 (Instr o)) (x : xs) n r a
-> Fix4 (Instr o) (x : xs) n r a
forall k k k k
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
f (Fix4 f) i j k l -> Fix4 f i j k l
In4 (Fix4 (Instr o) (x : x : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : xs) n r a
forall rep (k :: [Type] -> Nat -> Type -> Type -> Type) x
       (xs :: [Type]) (n :: Nat) r a (o :: rep).
k (x : x : xs) n r a -> Instr o k (x : xs) n r a
Dup Fix4 (Instr o) (x : x : xs) n r a
Fix4 (Instr o) (x : x : xs) n r a
m)))
optimise (Put ΣVar x
r1 Access
a (In4 (Get ΣVar x
r2 Access
_ Fix4 (Instr o) (x : xs) n r a
m))) | Just x :~: x
Refl <- ΣVar x
r1 ΣVar x -> ΣVar x -> Maybe (x :~: x)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` ΣVar x
r2 = Instr o (Fix4 (Instr o)) (x : xs) n r a
-> Fix4 (Instr o) (x : xs) n r a
forall k k k k
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
f (Fix4 f) i j k l -> Fix4 f i j k l
In4 (Fix4 (Instr o) (x : x : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : xs) n r a
forall rep (k :: [Type] -> Nat -> Type -> Type -> Type) x
       (xs :: [Type]) (n :: Nat) r a (o :: rep).
k (x : x : xs) n r a -> Instr o k (x : xs) n r a
Dup (Instr o (Fix4 (Instr o)) (x : x : xs) n r a
-> Fix4 (Instr o) (x : x : xs) n r a
forall k k k k
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
f (Fix4 f) i j k l -> Fix4 f i j k l
In4 (ΣVar x
-> Access
-> Fix4 (Instr o) (x : xs) n r a
-> Instr o (Fix4 (Instr o)) (x : x : xs) n r a
forall rep x (k :: [Type] -> Nat -> Type -> Type -> Type)
       (xs :: [Type]) (n :: Nat) r a (o :: rep).
ΣVar x -> Access -> k xs n r a -> Instr o k (x : xs) n r a
Put ΣVar x
r1 Access
a Fix4 (Instr o) (x : xs) n r a
m)))
optimise (Get ΣVar x
r1 Access
_ (In4 (Put ΣVar x
r2 Access
_ Fix4 (Instr o) xs n r a
m))) | Just x :~: x
Refl <- ΣVar x
r1 ΣVar x -> ΣVar x -> Maybe (x :~: x)
forall k (f :: k -> Type) (a :: k) (b :: k).
GEq f =>
f a -> f b -> Maybe (a :~: b)
`geq` ΣVar x
r2 = Fix4 (Instr o) xs n r a
Fix4 (Instr o) xs n r a
m
optimise Instr o (Fix4 (Instr o)) xs n r a
m = Instr o (Fix4 (Instr o)) xs n r a -> Fix4 (Instr o) xs n r a
forall k k k k
       (f :: (k -> k -> k -> k -> Type) -> k -> k -> k -> k -> Type)
       (i :: k) (j :: k) (k :: k) (l :: k).
f (Fix4 f) i j k l -> Fix4 f i j k l
In4 Instr o (Fix4 (Instr o)) xs n r a
m