Circ.hs

{-# LANGUAGE GADTs, KindSignatures, DataKinds, TypeOperators, PolyKinds,
    StandaloneDeriving, ScopedTypeVariables #-}

module Circ where

import Data.List
import Data.List.Extra
import Data.Function
import Data.Traversable
import Control.Applicative
import Control.Arrow
import Control.Monad

import BigArray

data Tuply :: * -> * where
  Oney   :: Tuply ()
  Booly  :: Tuply Bool
  (:*:) :: Tuply s -> Tuply t -> Tuply (s, t)
deriving instance Show (Tuply t)
deriving instance Eq (Tuply t)
infixr 4 :*:

class (Show i, Ord i) => TUPLY i where
  tuply :: Tuply i

instance TUPLY () where
  tuply = Oney

instance TUPLY Bool where
  tuply = Booly

instance (TUPLY s, TUPLY t) => TUPLY (s, t) where
  tuply = tuply :*: tuply

tuples :: Tuply t -> [t]
tuples Oney = [()]
tuples Booly = [False, True]
tuples (s :*: t) = (,) <$> tuples s <*> tuples t

data Table :: * -> * -> * where
  Ret   :: x -> Table () x
  Cond  :: x -> x -> Table Bool x
  Curry :: Table s (Table t x) -> Table (s, t) x
deriving instance Show x => Show (Table t x)
deriving instance Eq x => Eq (Table t x)
instance Ord x => Ord (Table t x) where
  compare (Ret x) (Ret y) = compare x y
  compare (Cond x0 y0) (Cond x1 y1) = compare (x0, y0) (x1, y1)
  compare (Curry f) (Curry g) = compare f g

($$) :: Table s x -> s -> x
Ret x    $$ ()      = x
Cond f t $$ False   = f
Cond f t $$ True    = t
Curry f  $$ (s, t)  = f $$ s $$ t
infixl 3 $$

instance Traversable (Table i) where
  traverse f (Ret s)      = Ret <$> f s
  traverse f (Cond s0 s1) = Cond <$> f s0 <*> f s1
  traverse f (Curry st)   = Curry <$> traverse (traverse f) st

instance Foldable (Table i) where foldMap = foldMapDefault
instance Functor (Table i) where fmap = fmapDefault

lambda :: TUPLY s => (s -> x) -> Table s x
lambda = lambdaEx tuply

lambdaEx :: Tuply s -> (s -> x) -> Table s x
lambdaEx Oney      f = Ret (f ())
lambdaEx Booly     f = Cond (f False) (f True)
lambdaEx (s :*: t) f = Curry (lambdaEx s $ \ u -> lambdaEx t $ \ v -> f (u, v))

instance TUPLY i => Applicative (Table i) where
  pure x   = lambda $ \ _ -> x
  f <*> s  = lambda $ \ i -> (f $$ i) (s $$ i)

type Component s i o = Table (s, i) (s, o)

comb :: TUPLY i => (i -> o) -> Component () i o
comb f = lambda $ \ ((), i) -> ((), f i)

(-$) :: Component () i o -> i -> o
f -$ i = snd (f $$ ((), i))

gNAND :: Component () (Bool, Bool) Bool
gNAND = comb $ (not . uncurry (&&))

gDFF :: Component Bool Bool Bool
gDFF = lambda $ \ (q, d) -> (d, q)

gNOT :: Component () Bool Bool
gNOT = comb $ \ b -> gNAND -$ (b, b)

gAND :: Component () (Bool, Bool) Bool
gAND = comb $ \ x -> case x of
  (a, b) -> z where
    c = gNAND -$ (a, b)
    z = gNOT  -$ c

gOR ::  Component () (Bool, Bool) Bool
gOR = comb $ \ x -> case x of
  (a, b) -> z where
    a' = gNOT  -$ a
    b' = gNOT  -$ b
    z  = gNAND -$ (a', b')

gMUX :: Component () (Bool, (Bool, Bool)) Bool
gMUX = comb $ \ x -> case x of
  (c, (b0, b1)) -> z where
    c' = gNOT -$ c
    x  = gAND -$ (c', b0)
    y  = gAND -$ (c,  b1)
    z  = gOR  -$ (x, y)

gJKFF :: Component Bool (Bool, Bool) Bool
gJKFF = lambda $ \ x -> case x of
  (q, (j, k)) -> (q', d') where
    (q', d') = gDFF $$ (q, d)
    k' = gNOT -$ k
    d  = gMUX -$ (q, (j, k'))

gXOR :: Component () (Bool, Bool) Bool
gXOR = comb $ \ x -> case x of
  (a, b) -> z where
    z  = gMUX -$ (a, (b, b'))
    b' = gNOT -$ b

gTFF0 :: Component Bool Bool Bool
gTFF0 = lambda $ \ x -> case x of
  (q, t) -> (q', d') where
    (q', d') = gDFF $$ (q, d)
    d        = gXOR -$ (q, t)

gTFF1 :: Component Bool Bool Bool
gTFF1 = lambda $ \ x -> case x of
  (q, t) -> (q', jk') where
    (q', jk') = gJKFF $$ (q, (t, t))

gCOUNT2 :: Component (Bool, Bool) () (Bool, Bool)
gCOUNT2 = lambda $ \ x -> case x of
  ((q2, q1), ()) -> ((q2', q1'), (t2', t1')) where
    (q1', t1') = gTFF0 $$ (q1, True)
    (q2', t2') = gTFF0 $$ (q2, t1')

gCOUNT3 :: Component (Bool, (Bool, Bool)) () (Bool, (Bool, Bool))
gCOUNT3 = lambda $ \ x -> case x of
  ((q4, (q2, q1)), ()) -> ((q4', (q2', q1')), (t4', (t2', t1'))) where
    (q1', t1') = gTFF0 $$ (q1, True)
    (q2', t2') = gTFF0 $$ (q2, t1')
    (q4', t4') = gTFF0 $$ (q4, t4)
    t4         = gAND  -$ (t2', t1')

gCOUNT2' :: Component (Bool, (Bool, Bool)) () (Bool, Bool)
gCOUNT2' = lambda $ \ x -> case x of
  sv -> (s, t21') where
    (s, (_, t21')) = gCOUNT3 $$ sv


data PART = P | PART :+: PART deriving (Show, Eq)

{-
data PARTy :: PART -> * where
  Py :: PARTy P
  (:++:) :: PARTy p -> PARTy q -> PARTy (p :+: q)
deriving instance Show (PARTy p)
deriving instance Eq (PARTy p)
-}

data Parted :: PART -> * -> * where
  Part :: [x] -> Parted P x
  Sep  :: Parted p x -> Parted q x -> Parted (p :+: q) x
deriving instance Show x => Show (Parted p x)
deriving instance Eq x => Eq (Parted p x)

similar :: Parted p x -> Parted q y -> Bool
similar (Part _) (Part _) = True
similar (Sep a b) (Sep c d) = similar a c && similar b d
similar _ _ = False

data Pos :: PART -> * where
  X :: Pos P
  L :: Pos p -> Pos (p :+: q)
  R :: Pos q -> Pos (p :+: q)
deriving instance Show (Pos p)
deriving instance Eq (Pos p)
instance Ord (Pos p) where
  compare X X = EQ
  compare (L x) (L y) = compare x y
  compare (L x) (R y) = LT
  compare (R x) (L y) = GT
  compare (R x) (R y) = compare x y

unL :: Pos (p :+: q) -> Maybe (Pos p)
unL (L x) = Just x
unL (R y) = Nothing

unR :: Pos (p :+: q) -> Maybe (Pos q)
unR (L y) = Nothing
unR (R x) = Just x

part :: Parted p x -> Pos p -> [x]
part (Part xs) X = xs
part (Sep ps qs) (L x) = part ps x
part (Sep ps qs) (R x) = part qs x

data Partition :: * -> * where
  Partition :: Parted p t -> Table t (Pos p) -> Partition t
  -- invariant: Partition ts f satisfies
  --   elem t (part ts x) = True  <=>  f $$ t = x
deriving instance Show t => Show (Partition t)

allInOne :: TUPLY t => Partition t
allInOne = allInOneEx tuply

allInOneEx :: Tuply t -> Partition t
allInOneEx ty = Partition (Part (tuples ty)) (lambdaEx ty $ \ _ -> X)

refine :: forall t x. (Eq t, Ord x, TUPLY t) => Partition t -> (t -> x) -> Partition t
refine (Partition p f) ob = case refineSub (SubPartition p (Just . (f $$))) ob of
  SubPartition q g -> Partition q (lambda $ \ t -> case g t of Just x -> x)

data SubPartition :: * -> * where
  SubPartition :: Parted p t -> (t -> Maybe (Pos p)) -> SubPartition t
  -- invariant: SubPartition ts f satisfies
  --   elem t (part ts x) = True  <=>  f t = Just x

pairSub :: SubPartition t -> SubPartition t -> SubPartition t
pairSub (SubPartition p f) (SubPartition q g) = SubPartition (Sep p q) $ \ t ->
  L <$> f t <|> R <$> g t

refineSub :: forall t x. (Eq t, Ord x) => SubPartition t -> (t -> x) -> SubPartition t
refineSub (SubPartition (Part ts) f) ob = subPartition (groupSortOn ob ts)
refineSub (SubPartition (Sep p q) f) ob = pairSub
  (refineSub (SubPartition p (unL <=< f)) ob)
  (refineSub (SubPartition q (unR <=< f)) ob)

deal :: [x] -> ([x], [x])
deal [] = ([], [])
deal (x : xs) = (x : zs, ys) where (ys, zs) = deal xs

subPartition :: Eq t => [[t]] -> SubPartition t
subPartition [ts] = SubPartition (Part ts) $ \ t -> if elem t ts then Just X else Nothing
subPartition tss = uncurry pairSub . (subPartition *** subPartition) $ deal tss

analyse :: forall s i o. (Eq s, Ord o, TUPLY s, TUPLY i) => Component s i o -> Partition s
analyse c = iter start where
  start :: Partition s
  start = refine allInOne $ \ s -> lambda $ \ i -> snd (c $$ (s, i))
  iter :: Partition s -> Partition s
  iter x@(Partition p f) = case refine x next of
      y@(Partition q _)
        | similar p q -> y
        | otherwise -> iter y
    where next s = lambda $ \ i -> f $$ (fst (c $$ (s, i)))

data Machine :: * -> * -> * -> * where
  Machine :: TUPLY i =>
    Parted p s -> [(Table i o, [(Pos p, Table i (Pos p))])] -> Machine s i o
instance (Show s, Show o) => Show (Machine s i o) where
  show (Machine p a) = concat ["Machine (", show p, ") (", show a, ")"]

machine :: forall s i o. (Eq s, Ord o, TUPLY s, TUPLY i) =>
           Component s i o -> Machine s i o
machine c = case analyse c of
    Partition p f -> Machine p (foldMapArr (:[]) (go p f))
  where
    go :: Parted p s -> Table s (Pos q) -> Arr (Table i o) [(Pos p, Table i (Pos q))]
    go (Part (s : _)) f = single ( lambda $ \ i -> snd (c $$ (s, i))
                                 , [(X, lambda $ \ i -> f $$ fst (c $$ (s, i)))]
                                 )
    go (Sep p q) f = fmap (fmap (L *** id)) (go p f) <> fmap (fmap (R *** id)) (go q f)

picks :: [x] -> [(x, [x])]
picks [] = []
picks (x : xs) = (x, xs) : [(y, x : ys) | (y, ys) <- picks xs]

mkBisim :: forall b s t i. (Eq b, Ord s, Eq t, TUPLY i) =>
           Arr s t -> [(b, [(s, Table i s)])] -> [(b, [(t, Table i t)])] -> [Arr s t]
mkBisim r [] [] = return r
mkBisim r ((b, sfs) : bsfss) ((b', tgs) : btgss) | b == b' = do
  (r, sfs, tgs) <- precook r sfs tgs
  r <- guess r sfs tgs
  mkBisim r bsfss btgss
  where
    precook r [] tgs = [(r, [], tgs)]
    precook r (sf@(s, f) : sfs) tgs = case findArr s r of
      Nothing -> do
        (r, sfs, tgs) <- precook r sfs tgs
        return (r, sf : sfs, tgs)
      Just t -> case [(g, tgs') | ((t', g), tgs') <- picks tgs] of
        [(g, tgs)] -> do
          r <- foldr ((<=<) . match) return ((,) <$> f <*> g) r
          precook r sfs tgs
        _ -> []
    match :: (s, t) -> Arr s t -> [Arr s t]
    match (s, t) r = case findArr s r of
      Just t' -> if t == t' then return r else []
      Nothing -> return (insertArr (s, t) r)
    guess r [] [] = return r
    guess r ((s, f) : sfs) tgs = do
      ((t, g), tgs) <- picks tgs
      r <- foldr ((<=<) . match) return ((,) <$> f <*> g) r
      (r, sfs, tgs) <- precook (insertArr (s, t) r) sfs tgs
      guess r sfs tgs
mkBisim r _ _ = []

data Bisims :: * -> * -> * -> * -> * where
  Bisims :: (Parted p s, [(Table i o, [(Pos p, Table i (Pos p))])]) ->
            (Parted q t, [(Table i o, [(Pos q, Table i (Pos q))])]) ->
            [Arr (Pos p) (Pos q)] ->
            Bisims s t i o
instance (Show s, Show t, Show o) => Show (Bisims s t i o) where
  show (Bisims lm rm bs) = concat
    ["Bisims (", show lm, ") (", show rm, ") (", show bs, ")"]

bisimulations :: (TUPLY s, TUPLY t, TUPLY i, Ord o) =>
  Component s i o -> Component t i o -> Bisims s t i o
bisimulations c d = case (machine c, machine d) of
  (Machine p lm, Machine q rm) -> Bisims (p, lm) (q, rm) (mkBisim emptyArr lm rm)