{-# LANGUAGE TupleSections #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE CPP #-}
{-# LANGUAGE InstanceSigs #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE GADTs #-}
{-# LANGUAGE KindSignatures #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE StandaloneDeriving #-}

{-# OPTIONS_GHC -Wall #-}
{-# OPTIONS_GHC -Wno-unused-imports #-} -- TEMP

-- | Stack-based VM as a category, enabling compilation from Haskell.

module ConCat.StackVM where

import Prelude hiding (id,(.),curry,uncurry,const)

import ConCat.Misc ((:*),(:+))
import qualified ConCat.Category as C
import ConCat.AltCat

{--------------------------------------------------------------------
    Stack functions (for specification)
--------------------------------------------------------------------}

newtype StackFun a b = SF (forall z. a :* z -> b :* z)

unSF :: StackFun a b -> forall z. a :* z -> b :* z
unSF :: forall a b. StackFun a b -> forall z. (a :* z) -> b :* z
unSF (SF forall z. (a :* z) -> b :* z
h) = (a :* z) -> b :* z
forall z. (a :* z) -> b :* z
h

inSF :: ((forall z. a :* z -> b :* z) -> (forall z. c :* z -> d :* z))
     -> StackFun a b -> StackFun c d
inSF :: forall a b c d.
((forall z. (a :* z) -> b :* z) -> forall z. (c :* z) -> d :* z)
-> StackFun a b -> StackFun c d
inSF (forall z. (a :* z) -> b :* z) -> forall z. (c :* z) -> d :* z
w (SF forall z. (a :* z) -> b :* z
h) = (forall z. (c :* z) -> d :* z) -> StackFun c d
forall a b. (forall z. (a :* z) -> b :* z) -> StackFun a b
SF ((forall z. (a :* z) -> b :* z) -> forall z. (c :* z) -> d :* z
w (a :* z) -> b :* z
forall z. (a :* z) -> b :* z
h)

inSF2 :: ((forall z. a :* z -> b :* z) -> (forall z. c :* z -> d :* z) -> (forall z. p :* z -> q :* z))
      -> StackFun a b -> StackFun c d -> StackFun p q
inSF2 :: forall a b c d p q.
((forall z. (a :* z) -> b :* z)
 -> (forall z. (c :* z) -> d :* z) -> forall z. (p :* z) -> q :* z)
-> StackFun a b -> StackFun c d -> StackFun p q
inSF2 (forall z. (a :* z) -> b :* z)
-> (forall z. (c :* z) -> d :* z) -> forall z. (p :* z) -> q :* z
w (SF forall z. (a :* z) -> b :* z
h) (SF forall z. (c :* z) -> d :* z
k) = (forall z. (p :* z) -> q :* z) -> StackFun p q
forall a b. (forall z. (a :* z) -> b :* z) -> StackFun a b
SF ((forall z. (a :* z) -> b :* z)
-> (forall z. (c :* z) -> d :* z) -> forall z. (p :* z) -> q :* z
w (a :* z) -> b :* z
forall z. (a :* z) -> b :* z
h (c :* z) -> d :* z
forall z. (c :* z) -> d :* z
k)

-- | The semantic functor that specifies 'StackFun'.
stackFun :: (a -> b) -> StackFun a b
stackFun :: forall a b. (a -> b) -> StackFun a b
stackFun a -> b
f = (forall z. (a :* z) -> b :* z) -> StackFun a b
forall a b. (forall z. (a :* z) -> b :* z) -> StackFun a b
SF ((a -> b) -> (a, z) -> (b, z)
forall (k :: * -> * -> *) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first a -> b
f)
{-# INLINE stackFun #-}

evalStackFun :: StackFun a b -> (a -> b)
evalStackFun :: forall a b. StackFun a b -> a -> b
evalStackFun (SF forall z. (a :* z) -> b :* z
f) = Prod (->) b (Unit (->)) -> b
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k (Prod k a (Unit (->))) a
rcounit (Prod (->) b (Unit (->)) -> b)
-> (a -> Prod (->) b (Unit (->))) -> a -> b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Prod (->) a (Unit (->)) -> Prod (->) b (Unit (->))
forall z. (a :* z) -> b :* z
f (Prod (->) a (Unit (->)) -> Prod (->) b (Unit (->)))
-> (a -> Prod (->) a (Unit (->))) -> a -> Prod (->) b (Unit (->))
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. a -> Prod (->) a (Unit (->))
forall (k :: * -> * -> *) a.
(UnitCat k, Ok k a) =>
k a (Prod k a (Unit (->)))
runit
-- evalStackFun (SF f) a = fst (f (a,()))
-- evalStackFun (SF f) a = b
--  where
--    (b,()) = f (a,())

instance Category StackFun where
  id :: forall a. Ok StackFun a => StackFun a a
id = (a -> a) -> StackFun a a
forall a b. (a -> b) -> StackFun a b
stackFun a -> a
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id
  SF forall z. (b :* z) -> c :* z
g . :: forall b c a.
Ok3 StackFun a b c =>
StackFun b c -> StackFun a b -> StackFun a c
. SF forall z. (a :* z) -> b :* z
f = (forall z. (a :* z) -> c :* z) -> StackFun a c
forall a b. (forall z. (a :* z) -> b :* z) -> StackFun a b
SF ((b :* z) -> c :* z
forall z. (b :* z) -> c :* z
g ((b :* z) -> c :* z) -> ((a :* z) -> b :* z) -> (a :* z) -> c :* z
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (a :* z) -> b :* z
forall z. (a :* z) -> b :* z
f)
  -- (.) = inSF2 (.)
  {-# INLINE id #-}
  {-# INLINE (.) #-}

instance AssociativePCat StackFun where
  lassocP :: forall a b c.
Ok3 StackFun a b c =>
StackFun
  (Prod StackFun a (Prod StackFun b c))
  (Prod StackFun (Prod StackFun a b) c)
lassocP = (Prod StackFun a (Prod StackFun b c)
 -> Prod StackFun (Prod StackFun a b) c)
-> StackFun
     (Prod StackFun a (Prod StackFun b c))
     (Prod StackFun (Prod StackFun a b) c)
forall a b. (a -> b) -> StackFun a b
stackFun Prod StackFun a (Prod StackFun b c)
-> Prod StackFun (Prod StackFun a b) c
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
lassocP
  rassocP :: forall a b c.
Ok3 StackFun a b c =>
StackFun
  (Prod StackFun (Prod StackFun a b) c)
  (Prod StackFun a (Prod StackFun b c))
rassocP = (Prod StackFun (Prod StackFun a b) c
 -> Prod StackFun a (Prod StackFun b c))
-> StackFun
     (Prod StackFun (Prod StackFun a b) c)
     (Prod StackFun a (Prod StackFun b c))
forall a b. (a -> b) -> StackFun a b
stackFun Prod StackFun (Prod StackFun a b) c
-> Prod StackFun a (Prod StackFun b c)
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
rassocP
  {-# INLINE lassocP #-}
  {-# INLINE rassocP #-}

instance MonoidalPCat StackFun where
  -- first = inSF inRassocP -- okay
  -- first (SF f) = SF (inRassocP f)
  first :: forall a a' b.
Ok3 StackFun a b a' =>
StackFun a a' -> StackFun (Prod StackFun a b) (Prod StackFun a' b)
first (SF forall z. (a :* z) -> a' :* z
f) = (forall z. (Prod StackFun a b :* z) -> Prod StackFun a' b :* z)
-> StackFun (Prod StackFun a b) (Prod StackFun a' b)
forall a b. (forall z. (a :* z) -> b :* z) -> StackFun a b
SF (Prod (->) a' (Prod (->) b z) -> (Prod StackFun a' b, z)
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
lassocP (Prod (->) a' (Prod (->) b z) -> (Prod StackFun a' b, z))
-> ((Prod StackFun a b, z) -> Prod (->) a' (Prod (->) b z))
-> (Prod StackFun a b, z)
-> (Prod StackFun a' b, z)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. Prod (->) a (Prod (->) b z) -> Prod (->) a' (Prod (->) b z)
forall z. (a :* z) -> a' :* z
f (Prod (->) a (Prod (->) b z) -> Prod (->) a' (Prod (->) b z))
-> ((Prod StackFun a b, z) -> Prod (->) a (Prod (->) b z))
-> (Prod StackFun a b, z)
-> Prod (->) a' (Prod (->) b z)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Prod StackFun a b, z) -> Prod (->) a (Prod (->) b z)
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
rassocP)
  -- first (SF f) = SF lassocP . SF f . SF rassocP -- doesn't type-check
  second :: forall a b b'.
Ok3 StackFun a b b' =>
StackFun b b' -> StackFun (Prod StackFun a b) (Prod StackFun a b')
second = StackFun b b' -> StackFun (a :* b) (a :* b')
forall (k :: * -> * -> *) a b d.
(MonoidalPCat k, BraidedPCat k, Ok3 k a b d) =>
k b d -> k (a :* b) (a :* d)
secondFirst
  StackFun a c
f *** :: forall a b c d.
Ok4 StackFun a b c d =>
StackFun a c
-> StackFun b d -> StackFun (Prod StackFun a b) (Prod StackFun c d)
*** StackFun b d
g = StackFun b d -> StackFun (Prod StackFun c b) (Prod StackFun c d)
forall (k :: * -> * -> *) a b d.
(MonoidalPCat k, Ok3 k a b d) =>
k b d -> k (Prod k a b) (Prod k a d)
second StackFun b d
g StackFun (Prod StackFun c b) (Prod StackFun c d)
-> StackFun (Prod StackFun a b) (Prod StackFun c b)
-> StackFun (Prod StackFun a b) (Prod StackFun c d)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. StackFun a c -> StackFun (Prod StackFun a b) (Prod StackFun c b)
forall (k :: * -> * -> *) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first StackFun a c
f
  {-# INLINE first #-}
  {-# INLINE second #-}
  {-# INLINE (***) #-}

instance BraidedPCat StackFun where
  swapP :: forall a b.
Ok2 StackFun a b =>
StackFun (Prod StackFun a b) (Prod StackFun b a)
swapP = (Prod StackFun a b -> Prod StackFun b a)
-> StackFun (Prod StackFun a b) (Prod StackFun b a)
forall a b. (a -> b) -> StackFun a b
stackFun Prod StackFun a b -> Prod StackFun b a
forall (k :: * -> * -> *) a b.
(BraidedPCat k, Ok2 k a b) =>
k (Prod k a b) (Prod k b a)
swapP
  {-# INLINE swapP #-}

instance ProductCat StackFun where
  exl :: forall a b. Ok2 StackFun a b => StackFun (Prod StackFun a b) a
exl = (Prod StackFun a b -> a) -> StackFun (Prod StackFun a b) a
forall a b. (a -> b) -> StackFun a b
stackFun Prod StackFun a b -> a
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl
  exr :: forall a b. Ok2 StackFun a b => StackFun (Prod StackFun a b) b
exr = (Prod StackFun a b -> b) -> StackFun (Prod StackFun a b) b
forall a b. (a -> b) -> StackFun a b
stackFun Prod StackFun a b -> b
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr
  dup :: forall a. Ok StackFun a => StackFun a (Prod StackFun a a)
dup = (a -> Prod StackFun a a) -> StackFun a (Prod StackFun a a)
forall a b. (a -> b) -> StackFun a b
stackFun a -> Prod StackFun a a
forall (k :: * -> * -> *) a.
(ProductCat k, Ok k a) =>
k a (Prod k a a)
dup
  {-# INLINE exl #-}
  {-# INLINE exr #-}
  {-# INLINE dup #-}

instance TerminalCat StackFun where
  it :: forall a. Ok StackFun a => StackFun a (Unit (->))
it = (a -> Unit (->)) -> StackFun a (Unit (->))
forall a b. (a -> b) -> StackFun a b
stackFun a -> Unit (->)
forall (k :: * -> * -> *) a.
(TerminalCat k, Ok k a) =>
k a (Unit (->))
it
  {-# INLINE it #-}

instance UnitCat StackFun

instance MonoidalSCat StackFun where
  -- SF f +++ SF g = SF (inDistr (f +++ g))
  SF forall z. (c :* z) -> a :* z
f +++ :: forall a b c d.
Ok4 StackFun a b c d =>
StackFun c a
-> StackFun d b
-> StackFun (Coprod StackFun c d) (Coprod StackFun a b)
+++ SF forall z. (d :* z) -> b :* z
g = (forall z. (Coprod StackFun c d :* z) -> Coprod StackFun a b :* z)
-> StackFun (Coprod StackFun c d) (Coprod StackFun a b)
forall a b. (forall z. (a :* z) -> b :* z) -> StackFun a b
SF (((a :* z) :+ (b :* z)) -> (Coprod StackFun a b, z)
forall (k :: * -> * -> *) u v b.
(MonoidalPCat k, MCoproductCat k, Ok3 k u v b) =>
k ((u :* b) :+ (v :* b)) ((u :+ v) :* b)
undistr (((a :* z) :+ (b :* z)) -> (Coprod StackFun a b, z))
-> ((Coprod StackFun c d, z) -> (a :* z) :+ (b :* z))
-> (Coprod StackFun c d, z)
-> (Coprod StackFun a b, z)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Prod (->) c z -> a :* z
forall z. (c :* z) -> a :* z
f (Prod (->) c z -> a :* z)
-> (Prod (->) d z -> b :* z)
-> Coprod (->) (Prod (->) c z) (Prod (->) d z)
-> (a :* z) :+ (b :* z)
forall (k :: * -> * -> *) a b c d.
(MonoidalSCat k, Ok4 k a b c d) =>
k c a -> k d b -> k (Coprod k c d) (Coprod k a b)
+++ Prod (->) d z -> b :* z
forall z. (d :* z) -> b :* z
g) (Coprod (->) (Prod (->) c z) (Prod (->) d z)
 -> (a :* z) :+ (b :* z))
-> ((Coprod StackFun c d, z)
    -> Coprod (->) (Prod (->) c z) (Prod (->) d z))
-> (Coprod StackFun c d, z)
-> (a :* z) :+ (b :* z)
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (Coprod StackFun c d, z)
-> Coprod (->) (Prod (->) c z) (Prod (->) d z)
forall (k :: * -> * -> *) u v b.
(DistribCat k, Ok3 k u v b) =>
k (Prod k (Coprod k u v) b) (Coprod k (Prod k u b) (Prod k v b))
distr)
  -- (+++) = inSF2 (\ f g -> inDistr (f +++ g))
  {-# INLINE (+++) #-}

-- The validity of this (+++) definition relies on the following fact:
-- 
--   first (f +++ g) = inDistr (first f +++ first g)
-- 
-- See proof in 2018-06-11 notes.

instance BraidedSCat StackFun where
  swapS :: forall a b.
Ok2 StackFun a b =>
StackFun (Coprod StackFun a b) (Coprod StackFun b a)
swapS = (Coprod StackFun a b -> Coprod StackFun b a)
-> StackFun (Coprod StackFun a b) (Coprod StackFun b a)
forall a b. (a -> b) -> StackFun a b
stackFun Coprod StackFun a b -> Coprod StackFun b a
forall (k :: * -> * -> *) a b.
(BraidedSCat k, Ok2 k a b) =>
k (Coprod k a b) (Coprod k b a)
swapS
  {-# INLINE swapS #-}

instance CoproductCat StackFun where
  inl :: forall a b. Ok2 StackFun a b => StackFun a (Coprod StackFun a b)
inl = (a -> Coprod StackFun a b) -> StackFun a (Coprod StackFun a b)
forall a b. (a -> b) -> StackFun a b
stackFun a -> Coprod StackFun a b
forall (k :: * -> * -> *) a b.
(CoproductCat k, Ok2 k a b) =>
k a (Coprod k a b)
inl
  inr :: forall a b. Ok2 StackFun a b => StackFun b (Coprod StackFun a b)
inr = (b -> Coprod StackFun a b) -> StackFun b (Coprod StackFun a b)
forall a b. (a -> b) -> StackFun a b
stackFun b -> Coprod StackFun a b
forall (k :: * -> * -> *) a b.
(CoproductCat k, Ok2 k a b) =>
k b (Coprod k a b)
inr
  jam :: forall a. Ok StackFun a => StackFun (Coprod StackFun a a) a
jam = (Coprod StackFun a a -> a) -> StackFun (Coprod StackFun a a) a
forall a b. (a -> b) -> StackFun a b
stackFun Coprod StackFun a a -> a
forall (k :: * -> * -> *) a.
(CoproductCat k, Ok k a) =>
k (Coprod k a a) a
jam
  {-# INLINE inl #-}
  {-# INLINE inr #-}
  {-# INLINE jam #-}

instance DistribCat StackFun where
  distl :: forall a u v.
Ok3 StackFun a u v =>
StackFun
  (Prod StackFun a (Coprod StackFun u v))
  (Coprod StackFun (Prod StackFun a u) (Prod StackFun a v))
distl = (Prod StackFun a (Coprod StackFun u v)
 -> Coprod StackFun (Prod StackFun a u) (Prod StackFun a v))
-> StackFun
     (Prod StackFun a (Coprod StackFun u v))
     (Coprod StackFun (Prod StackFun a u) (Prod StackFun a v))
forall a b. (a -> b) -> StackFun a b
stackFun Prod StackFun a (Coprod StackFun u v)
-> Coprod StackFun (Prod StackFun a u) (Prod StackFun a v)
forall (k :: * -> * -> *) a u v.
(DistribCat k, Ok3 k a u v) =>
k (Prod k a (Coprod k u v)) (Coprod k (Prod k a u) (Prod k a v))
distl
  distr :: forall u v b.
Ok3 StackFun u v b =>
StackFun
  (Prod StackFun (Coprod StackFun u v) b)
  (Coprod StackFun (Prod StackFun u b) (Prod StackFun v b))
distr = (Prod StackFun (Coprod StackFun u v) b
 -> Coprod StackFun (Prod StackFun u b) (Prod StackFun v b))
-> StackFun
     (Prod StackFun (Coprod StackFun u v) b)
     (Coprod StackFun (Prod StackFun u b) (Prod StackFun v b))
forall a b. (a -> b) -> StackFun a b
stackFun Prod StackFun (Coprod StackFun u v) b
-> Coprod StackFun (Prod StackFun u b) (Prod StackFun v b)
forall (k :: * -> * -> *) u v b.
(DistribCat k, Ok3 k u v b) =>
k (Prod k (Coprod k u v) b) (Coprod k (Prod k u b) (Prod k v b))
distr
  {-# INLINE distl #-}
  {-# INLINE distr #-}

instance ClosedCat StackFun where
  apply :: forall a b.
Ok2 StackFun a b =>
StackFun (Prod StackFun (Exp StackFun a b) a) b
apply = (Prod StackFun (Exp StackFun a b) a -> b)
-> StackFun (Prod StackFun (Exp StackFun a b) a) b
forall a b. (a -> b) -> StackFun a b
stackFun Prod StackFun (Exp StackFun a b) a -> b
forall (k :: * -> * -> *) a b.
(ClosedCat k, Ok2 k a b) =>
k (Prod k (Exp k a b) a) b
apply
  curry :: forall a b c.
Ok3 StackFun a b c =>
StackFun (Prod StackFun a b) c -> StackFun a (Exp StackFun b c)
curry StackFun (Prod StackFun a b) c
sf = (a -> Exp StackFun b c) -> StackFun a (Exp StackFun b c)
forall a b. (a -> b) -> StackFun a b
stackFun ((Prod StackFun a b -> c) -> a -> Exp StackFun b c
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k (Prod k a b) c -> k a (Exp k b c)
curry (StackFun (Prod StackFun a b) c -> Prod StackFun a b -> c
forall a b. StackFun a b -> a -> b
evalStackFun StackFun (Prod StackFun a b) c
sf))
  uncurry :: forall a b c.
Ok3 StackFun a b c =>
StackFun a (Exp StackFun b c) -> StackFun (Prod StackFun a b) c
uncurry StackFun a (Exp StackFun b c)
sf = (Prod StackFun a b -> c) -> StackFun (Prod StackFun a b) c
forall a b. (a -> b) -> StackFun a b
stackFun ((a -> Exp StackFun b c) -> Prod StackFun a b -> c
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k a (Exp k b c) -> k (Prod k a b) c
uncurry (StackFun a (Exp StackFun b c) -> a -> Exp StackFun b c
forall a b. StackFun a b -> a -> b
evalStackFun StackFun a (Exp StackFun b c)
sf))
  {-# INLINE apply #-}
  {-# INLINE curry #-}
  {-# INLINE uncurry #-}

{--------------------------------------------------------------------
    Stack programs
--------------------------------------------------------------------}

data Prim :: * -> * -> * where
  Swap :: Prim (a :* b) (b :* a)
  Exl :: Prim (a :* b) a
  Exr :: Prim (a :* b) b
  Dup :: Prim a (a :* a)
  Const :: Show b => b -> Prim a b
  Negate :: Num a => Prim a a
  Add, Sub, Mul :: Num a => Prim (a :* a) a
  PowI :: Num a => Prim (a :* Int) a
  -- Experiment
  -- (:+++) :: StackProg a c -> StackProg b d -> Prim (a :+ b) (c :+ d)
  (:+++) :: StackOps a c -> StackOps b d -> Prim (a :+ b) (c :+ d)
  Apply :: Prim ((a -> b) :* a) b
  Curry :: StackProg (a :* b) c -> Prim a (b -> c)

deriving instance Show (Prim a b)

-- instance Show (Prim a b) where
--   show Swap      = "swapP"
--   show Exl       = "exl"
--   show Exr       = "exr"
--   show Dup       = "dup"
--   show (Const b) = show b
--   show Negate    = "negateC"
--   show Add       = "addC"
--   show Sub       = "subC"
--   show Mul       = "mulC"
--   show PowI      = "powIC"

-- TODO: showsPrec for Const

-- Alternatively use Syn

evalPrim :: Prim a b -> (a -> b)
evalPrim :: forall a b. Prim a b -> a -> b
evalPrim Prim a b
Exl       = a -> b
(b, b) -> b
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) a
exl
evalPrim Prim a b
Exr       = a -> b
(a, b) -> b
forall (k :: * -> * -> *) a b.
(ProductCat k, Ok2 k a b) =>
k (Prod k a b) b
exr
evalPrim Prim a b
Dup       = a -> b
a -> (a, a)
forall (k :: * -> * -> *) a.
(ProductCat k, Ok k a) =>
k a (Prod k a a)
dup
evalPrim (Const b
b) = b -> a -> b
forall (k :: * -> * -> *) b a. (ConstCat k b, Ok k a) => b -> k a b
const b
b
evalPrim Prim a b
Negate    = a -> a
a -> b
forall (k :: * -> * -> *) a. NumCat k a => k a a
negateC
evalPrim Prim a b
Add       = a -> b
(b, b) -> b
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
addC
evalPrim Prim a b
Sub       = a -> b
(b, b) -> b
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
subC
evalPrim Prim a b
Mul       = a -> b
(b, b) -> b
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
mulC
evalPrim Prim a b
PowI      = a -> b
(b, Int) -> b
forall (k :: * -> * -> *) a.
(NumCat k a, Ok k Int) =>
k (Prod k a Int) a
powIC
evalPrim Prim a b
Swap      = a -> b
(a, b) -> (b, a)
forall (k :: * -> * -> *) a b.
(BraidedPCat k, Ok2 k a b) =>
k (Prod k a b) (Prod k b a)
swapP
-- evalPrim (f :+++ g) = evalProg f +++ evalProg g
evalPrim (StackOps a c
f :+++ StackOps b d
g) = StackOps a c -> a -> c
forall a b. StackOps a b -> a -> b
evalStackOps StackOps a c
f (a -> c) -> (b -> d) -> Either a b -> Either c d
forall (k :: * -> * -> *) a b c d.
(MonoidalSCat k, Ok4 k a b c d) =>
k c a -> k d b -> k (Coprod k c d) (Coprod k a b)
+++ StackOps b d -> b -> d
forall a b. StackOps a b -> a -> b
evalStackOps StackOps b d
g
evalPrim Prim a b
Apply     = a -> b
(a -> b, a) -> b
forall (k :: * -> * -> *) a b.
(ClosedCat k, Ok2 k a b) =>
k (Prod k (Exp k a b) a) b
apply
evalPrim (Curry StackProg (a :* b) c
p) = ((a :* b) -> c) -> a -> b -> c
forall (k :: * -> * -> *) a b c.
(ClosedCat k, Ok3 k a b c) =>
k (Prod k a b) c -> k a (Exp k b c)
curry (StackProg (a :* b) c -> (a :* b) -> c
forall a b. StackProg a b -> a -> b
evalProg StackProg (a :* b) c
p)

data StackOp :: * -> * -> * where
  Pure :: Prim a b -> StackOp (a :* z) (b :* z)
  Push :: StackOp ((a :* b) :* z) (a :* (b :* z))
  Pop  :: StackOp (a :* (b :* z)) ((a :* b) :* z)

instance Show (StackOp a b) where
  show :: StackOp a b -> String
show (Pure Prim a b
op) = Prim a b -> String
forall a. Show a => a -> String
show Prim a b
op
  show StackOp a b
Push      = String
"Push"
  show StackOp a b
Pop       = String
"Pop"

instance Show2 StackOp where show2 :: forall a b. StackOp a b -> String
show2 = StackOp a b -> String
forall a. Show a => a -> String
show

evalStackOp :: StackOp u v -> (u -> v)
evalStackOp :: forall u v. StackOp u v -> u -> v
evalStackOp (Pure Prim a b
f) = (a -> b) -> (a, z) -> (b, z)
forall (k :: * -> * -> *) a c b.
(MonoidalPCat k, Ok3 k a b c) =>
k a c -> k (Prod k a b) (Prod k c b)
first (Prim a b -> a -> b
forall a b. Prim a b -> a -> b
evalPrim Prim a b
f)
evalStackOp StackOp u v
Push     = u -> v
(a :* b, z) -> (a, b :* z)
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k (Prod k a b) c) (Prod k a (Prod k b c))
rassocP
evalStackOp StackOp u v
Pop      = u -> v
(a, b :* z) -> (a :* b, z)
forall (k :: * -> * -> *) a b c.
(AssociativePCat k, Ok3 k a b c) =>
k (Prod k a (Prod k b c)) (Prod k (Prod k a b) c)
lassocP

infixr 5 :<
data StackOps :: * -> * -> * where
  Nil  :: StackOps a a
  (:<) :: StackOp a b -> StackOps b c -> StackOps a c

toList :: forall z a b. (forall u v. StackOp u v -> z) -> StackOps a b -> [z]
toList :: forall z a b. (forall u v. StackOp u v -> z) -> StackOps a b -> [z]
toList forall u v. StackOp u v -> z
f = StackOps a b -> [z]
forall p q. StackOps p q -> [z]
go
 where
   go :: StackOps p q -> [z]
   go :: forall p q. StackOps p q -> [z]
go StackOps p q
Nil         = []
   go (StackOp p b
op :< StackOps b q
ops) = StackOp p b -> z
forall u v. StackOp u v -> z
f StackOp p b
op z -> [z] -> [z]
forall a. a -> [a] -> [a]
: StackOps b q -> [z]
forall p q. StackOps p q -> [z]
go StackOps b q
ops

instance Show (StackOps a b) where
  show :: StackOps a b -> String
show = [Exists2 StackOp] -> String
forall a. Show a => a -> String
show ([Exists2 StackOp] -> String)
-> (StackOps a b -> [Exists2 StackOp]) -> StackOps a b -> String
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (forall u v. StackOp u v -> Exists2 StackOp)
-> StackOps a b -> [Exists2 StackOp]
forall z a b. (forall u v. StackOp u v -> z) -> StackOps a b -> [z]
toList StackOp u v -> Exists2 StackOp
forall u v. StackOp u v -> Exists2 StackOp
forall (k :: * -> * -> *) a b. k a b -> Exists2 k
Exists2

evalStackOps :: StackOps a b -> (a -> b)
evalStackOps :: forall a b. StackOps a b -> a -> b
evalStackOps StackOps a b
Nil          = a -> a
a -> b
forall (k :: * -> * -> *) a. (Category k, Ok k a) => k a a
id
evalStackOps (StackOp a b
op :< StackOps b b
rest) = StackOps b b -> b -> b
forall a b. StackOps a b -> a -> b
evalStackOps StackOps b b
rest (b -> b) -> (a -> b) -> a -> b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. StackOp a b -> a -> b
forall u v. StackOp u v -> u -> v
evalStackOp StackOp a b
op

infixr 5 ++*
(++*) :: StackOps a b -> StackOps b c -> StackOps a c
StackOps a b
Nil ++* :: forall a b c. StackOps a b -> StackOps b c -> StackOps a c
++* StackOps b c
ops'         = StackOps a c
StackOps b c
ops'
(StackOp a b
op :< StackOps b b
ops) ++* StackOps b c
ops' = StackOp a b
op StackOp a b -> StackOps b c -> StackOps a c
forall a b c. StackOp a b -> StackOps b c -> StackOps a c
:< (StackOps b b
ops StackOps b b -> StackOps b c -> StackOps b c
forall a b c. StackOps a b -> StackOps b c -> StackOps a c
++* StackOps b c
ops')

data StackProg a b = SP { forall a b. StackProg a b -> forall z. StackOps (a :* z) (b :* z)
unSP :: forall z. StackOps (a :* z) (b :* z) }

instance Show (StackProg a b) where
  show :: StackProg a b -> String
show (SP forall z. StackOps (a :* z) (b :* z)
ops) = StackOps (a :* Any) (b :* Any) -> String
forall a. Show a => a -> String
show StackOps (a :* Any) (b :* Any)
forall z. StackOps (a :* z) (b :* z)
ops

instance Category StackProg where
  id :: forall a. Ok StackProg a => StackProg a a
id  = (forall z. StackOps (a :* z) (a :* z)) -> StackProg a a
forall a b. (forall z. StackOps (a :* z) (b :* z)) -> StackProg a b
SP StackOps (a :* z) (a :* z)
forall a. StackOps a a
forall z. StackOps (a :* z) (a :* z)
Nil
  SP forall z. StackOps (b :* z) (c :* z)
g . :: forall b c a.
Ok3 StackProg a b c =>
StackProg b c -> StackProg a b -> StackProg a c
. SP forall z. StackOps (a :* z) (b :* z)
f = (forall z. StackOps (a :* z) (c :* z)) -> StackProg a c
forall a b. (forall z. StackOps (a :* z) (b :* z)) -> StackProg a b
SP (StackOps (a :* z) (b :* z)
forall z. StackOps (a :* z) (b :* z)
f StackOps (a :* z) (b :* z)
-> StackOps (b :* z) (c :* z) -> StackOps (a :* z) (c :* z)
forall a b c. StackOps a b -> StackOps b c -> StackOps a c
++* StackOps (b :* z) (c :* z)
forall z. StackOps (b :* z) (c :* z)
g)

-- stackOp :: StackOp a b -> StackProg a b
-- stackOp op = SP (op :< Nil)

primProg :: Prim a b -> StackProg a b
primProg :: forall a b. Prim a b -> StackProg a b
primProg Prim a b
p = (forall z. StackOps (a :* z) (b :* z)) -> StackProg a b
forall a b. (forall z. StackOps (a :* z) (b :* z)) -> StackProg a b
SP (Prim a b -> StackOp (a :* z) (b :* z)
forall b c z. Prim b c -> StackOp (b :* z) (c :* z)
Pure Prim a b
p StackOp (a :* z) (b :* z)
-> StackOps (b :* z) (b :* z) -> StackOps (a :* z) (b :* z)
forall a b c. StackOp a b -> StackOps b c -> StackOps a c
:< StackOps (b :* z) (b :* z)
forall a. StackOps a a
Nil)

-- firstP :: StackProg a c -> StackProg (a :* b) (c :* b)
-- firstP (SP ops) = SP (Push :< ops ++* Pop :< Nil)

-- TODO: tweak StackOps so we can postpone flattening.

instance ProductCat StackProg where
  exl :: forall a b. Ok2 StackProg a b => StackProg (Prod StackFun a b) a
exl = Prim (Prod StackProg a b) a -> StackProg (Prod StackProg a b) a
forall a b. Prim a b -> StackProg a b
primProg Prim (Prod StackProg a b) a
forall a b. Prim (a :* b) a
Exl
  exr :: forall a b. Ok2 StackProg a b => StackProg (Prod StackFun a b) b
exr = Prim (Prod StackProg a b) b -> StackProg (Prod StackProg a b) b
forall a b. Prim a b -> StackProg a b
primProg Prim (Prod StackProg a b) b
forall b b. Prim (b :* b) b
Exr
  dup :: forall a. Ok StackProg a => StackProg a (Prod StackFun a a)
dup = Prim a (Prod StackProg a a) -> StackProg a (Prod StackProg a a)
forall a b. Prim a b -> StackProg a b
primProg Prim a (Prod StackProg a a)
forall a. Prim a (a :* a)
Dup

instance MonoidalPCat StackProg where
  -- first  = firstP
  first :: forall a a' b.
Ok3 StackProg a b a' =>
StackProg a a'
-> StackProg (Prod StackFun a b) (Prod StackFun a' b)
first (SP forall z. StackOps (a :* z) (a' :* z)
ops) = (forall z.
 StackOps (Prod StackProg a b :* z) (Prod StackProg a' b :* z))
-> StackProg (Prod StackProg a b) (Prod StackProg a' b)
forall a b. (forall z. StackOps (a :* z) (b :* z)) -> StackProg a b
SP (StackOp (Prod StackProg a b :* z) (a :* (b :* z))
forall b c z. StackOp ((b :* c) :* z) (b :* (c :* z))
Push StackOp (Prod StackProg a b :* z) (a :* (b :* z))
-> StackOps (a :* (b :* z)) (Prod StackProg a' b :* z)
-> StackOps (Prod StackProg a b :* z) (Prod StackProg a' b :* z)
forall a b c. StackOp a b -> StackOps b c -> StackOps a c
:< StackOps (a :* (b :* z)) (a' :* (b :* z))
forall z. StackOps (a :* z) (a' :* z)
ops StackOps (a :* (b :* z)) (a' :* (b :* z))
-> StackOps (a' :* (b :* z)) (Prod StackProg a' b :* z)
-> StackOps (a :* (b :* z)) (Prod StackProg a' b :* z)
forall a b c. StackOps a b -> StackOps b c -> StackOps a c
++* StackOp (a' :* (b :* z)) (Prod StackProg a' b :* z)
forall b c z. StackOp (b :* (c :* z)) ((b :* c) :* z)
Pop StackOp (a' :* (b :* z)) (Prod StackProg a' b :* z)
-> StackOps (Prod StackProg a' b :* z) (Prod StackProg a' b :* z)
-> StackOps (a' :* (b :* z)) (Prod StackProg a' b :* z)
forall a b c. StackOp a b -> StackOps b c -> StackOps a c
:< StackOps (Prod StackProg a' b :* z) (Prod StackProg a' b :* z)
forall a. StackOps a a
Nil)
  second :: forall a b b'.
Ok3 StackProg a b b' =>
StackProg b b'
-> StackProg (Prod StackFun a b) (Prod StackFun a b')
second = StackProg b b' -> StackProg (a :* b) (a :* b')
forall (k :: * -> * -> *) a b d.
(MonoidalPCat k, BraidedPCat k, Ok3 k a b d) =>
k b d -> k (a :* b) (a :* d)
secondFirst
  *** :: forall a b c d.
Ok4 StackProg a b c d =>
StackProg a c
-> StackProg b d
-> StackProg (Prod StackFun a b) (Prod StackFun c d)
(***)  = StackProg a c -> StackProg b d -> StackProg (a :* b) (c :* d)
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (a :* b) (c :* d)
crossSecondFirst

-- instance MonoidalSCat StackProg where
--   -- SP f +++ SP g = SP (inDistr (f +++ g))
--   SP f +++ SP g = SP (undistr . (f +++ g) . distr)
--   -- (+++) = inSP2 (\ f g -> inDistr (f +++ g))
--   {-# INLINE (+++) #-}

-- SP f :: StackProg a c
-- SP g :: StackProg b d

-- f :: StackOps (a :* z) (c :* z)
-- g :: StackOps (b :* z) (d :* z)

instance Show b => ConstCat StackProg b where
  const :: forall a.
Ok StackProg a =>
ConstObj StackProg b -> StackProg a (ConstObj StackProg b)
const ConstObj StackProg b
b = Prim a (ConstObj StackProg b) -> StackProg a (ConstObj StackProg b)
forall a b. Prim a b -> StackProg a b
primProg (ConstObj StackProg b -> Prim a (ConstObj StackProg b)
forall b a. Show b => b -> Prim a b
Const ConstObj StackProg b
b)

instance TerminalCat     StackProg
instance UnitCat         StackProg
instance AssociativePCat StackProg
instance BraidedPCat     StackProg where swapP :: forall a b.
Ok2 StackProg a b =>
StackProg (Prod StackFun a b) (Prod StackFun b a)
swapP = Prim (Prod StackProg a b) (Prod StackProg b a)
-> StackProg (Prod StackProg a b) (Prod StackProg b a)
forall a b. Prim a b -> StackProg a b
primProg Prim (Prod StackProg a b) (Prod StackProg b a)
forall b c. Prim (b :* c) (c :* b)
Swap
  
-- Alternatively, remove Swap and use default in BraidedPCat, though Swap makes
-- for shorter programs.

-- data StackProg a b = SP { unSP :: forall z. StackOps (a :* z) (b :* z) }

instance ClosedCat StackProg where
  apply :: forall a b.
Ok2 StackProg a b =>
StackProg (Prod StackFun (Exp StackFun a b) a) b
apply = Prim (Prod StackProg (Exp StackProg a b) a) b
-> StackProg (Prod StackProg (Exp StackProg a b) a) b
forall a b. Prim a b -> StackProg a b
primProg Prim (Prod StackProg (Exp StackProg a b) a) b
forall b b. Prim ((b -> b) :* b) b
Apply
  curry :: forall a b c.
Ok3 StackProg a b c =>
StackProg (Prod StackFun a b) c -> StackProg a (Exp StackFun b c)
curry StackProg (Prod StackProg a b) c
p = Prim a (Exp StackProg b c) -> StackProg a (Exp StackProg b c)
forall a b. Prim a b -> StackProg a b
primProg (StackProg (Prod StackProg a b) c -> Prim a (Exp StackProg b c)
forall a b c. StackProg (a :* b) c -> Prim a (b -> c)
Curry StackProg (Prod StackProg a b) c
p)

instance Num a => NumCat StackProg a where
  negateC :: StackProg a a
negateC = Prim a a -> StackProg a a
forall a b. Prim a b -> StackProg a b
primProg Prim a a
forall a. Num a => Prim a a
Negate
  addC :: StackProg (Prod StackProg a a) a
addC    = Prim (Prod StackProg a a) a -> StackProg (Prod StackProg a a) a
forall a b. Prim a b -> StackProg a b
primProg Prim (Prod StackProg a a) a
forall a. Num a => Prim (a :* a) a
Add
  subC :: StackProg (Prod StackProg a a) a
subC    = Prim (Prod StackProg a a) a -> StackProg (Prod StackProg a a) a
forall a b. Prim a b -> StackProg a b
primProg Prim (Prod StackProg a a) a
forall a. Num a => Prim (a :* a) a
Sub
  mulC :: StackProg (Prod StackProg a a) a
mulC    = Prim (Prod StackProg a a) a -> StackProg (Prod StackProg a a) a
forall a b. Prim a b -> StackProg a b
primProg Prim (Prod StackProg a a) a
forall a. Num a => Prim (a :* a) a
Mul
  powIC :: Ok StackProg Int => StackProg (Prod StackProg a Int) a
powIC   = Prim (Prod StackProg a Int) a -> StackProg (Prod StackProg a Int) a
forall a b. Prim a b -> StackProg a b
primProg Prim (Prod StackProg a Int) a
forall a. Num a => Prim (a :* Int) a
PowI

{--------------------------------------------------------------------
    Relate StackProg to StackFun
--------------------------------------------------------------------}

-- The semantic homomorphism used to derive instances for StackProg.
progFun :: StackProg a b -> StackFun a b
progFun :: forall a b. StackProg a b -> StackFun a b
progFun (SP forall z. StackOps (a :* z) (b :* z)
ops) = (forall z. (a :* z) -> b :* z) -> StackFun a b
forall a b. (forall z. (a :* z) -> b :* z) -> StackFun a b
SF (StackOps (a :* z) (b :* z) -> (a :* z) -> b :* z
forall a b. StackOps a b -> a -> b
evalStackOps StackOps (a :* z) (b :* z)
forall z. StackOps (a :* z) (b :* z)
ops)

evalProg :: StackProg a b -> (a -> b)
evalProg :: forall a b. StackProg a b -> a -> b
evalProg = StackFun a b -> a -> b
forall a b. StackFun a b -> a -> b
evalStackFun (StackFun a b -> a -> b)
-> (StackProg a b -> StackFun a b) -> StackProg a b -> a -> b
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. StackProg a b -> StackFun a b
forall a b. StackProg a b -> StackFun a b
progFun

-- evalProg (SP ops) = rcounit . evalStackOps ops . runit
-- evalProg (SP ops) a = fst (evalStackOps ops (a,()))

{--------------------------------------------------------------------
    Miscellany
--------------------------------------------------------------------}

data Exists2 k = forall a b. Exists2 (a `k` b)

instance Show2 k => Show (Exists2 k) where show :: Exists2 k -> String
show (Exists2 k a b
f) = k a b -> String
forall a b. k a b -> String
forall {k} {k1} (k2 :: k -> k1 -> *) (a :: k) (b :: k1).
Show2 k2 =>
k2 a b -> String
show2 k a b
f

{--------------------------------------------------------------------
    Examples
--------------------------------------------------------------------}

-- evalProg t1 (7,5) --> -12
t1 :: StackProg (Int :* Int) Int
t1 :: StackProg (Prod StackProg Int Int) Int
t1 = StackProg (Prod StackProg Int Int) Int
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
addC StackProg (Prod StackProg Int Int) Int
-> StackProg (Prod StackProg Int Int) (Prod StackProg Int Int)
-> StackProg (Prod StackProg Int Int) Int
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (StackProg Int Int
forall (k :: * -> * -> *) a. NumCat k a => k a a
negateC StackProg Int Int
-> StackProg Int Int
-> StackProg (Prod StackProg Int Int) (Prod StackProg Int Int)
forall (k :: * -> * -> *) a b c d.
(MonoidalPCat k, Ok4 k a b c d) =>
k a c -> k b d -> k (a :* b) (c :* d)
*** StackProg Int Int
forall (k :: * -> * -> *) a. NumCat k a => k a a
negateC)

-- evalProg t2 7 --> -14
t2 :: StackProg Int Int
t2 :: StackProg Int Int
t2 = StackProg (Prod StackProg Int Int) Int
forall (k :: * -> * -> *) a. NumCat k a => k (Prod k a a) a
addC StackProg (Prod StackProg Int Int) Int
-> StackProg Int (Prod StackProg Int Int) -> StackProg Int Int
forall (k :: * -> * -> *) b c a.
(Category k, Ok3 k a b c) =>
k b c -> k a b -> k a c
. (StackProg Int Int
forall (k :: * -> * -> *) a. NumCat k a => k a a
negateC StackProg Int Int
-> StackProg Int Int -> StackProg Int (Prod StackProg Int Int)
forall (k :: * -> * -> *) a c d.
(MProductCat k, Ok3 k a c d) =>
k a c -> k a d -> k a (Prod k c d)
&&& StackProg Int Int
forall (k :: * -> * -> *) a. NumCat k a => k a a
negateC)