{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoFieldSelectors #-}

module TypedSession.State.Piple where

import Control.Algebra ((:+:))
import Control.Carrier.Error.Either (runError)
import Control.Carrier.Fresh.Strict
import Control.Carrier.Reader (runReader)
import Control.Carrier.State.Strict
import Control.Carrier.Writer.Strict (runWriter)
import Control.Effect.Error
import Control.Effect.Reader
import Control.Effect.Writer
import Control.Monad
import Data.Foldable (Foldable (toList), for_)
import Data.IntMap (IntMap)
import qualified Data.IntMap as IntMap
import qualified Data.List as L
import Data.Map (Map)
import qualified Data.Map as Map
import Data.Sequence (Seq)
import qualified Data.Sequence as Seq
import Data.Set (Set)
import qualified Data.Set as Set
import Prettyprinter
import qualified TypedSession.State.Constraint as C
import TypedSession.State.Render
import TypedSession.State.Type
import TypedSession.State.Utils

------------------------

newtype Index = Index Int deriving (Int -> Index -> ShowS
[Index] -> ShowS
Index -> String
(Int -> Index -> ShowS)
-> (Index -> String) -> ([Index] -> ShowS) -> Show Index
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> Index -> ShowS
showsPrec :: Int -> Index -> ShowS
$cshow :: Index -> String
show :: Index -> String
$cshowList :: [Index] -> ShowS
showList :: [Index] -> ShowS
Show, Index -> Index -> Bool
(Index -> Index -> Bool) -> (Index -> Index -> Bool) -> Eq Index
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: Index -> Index -> Bool
== :: Index -> Index -> Bool
$c/= :: Index -> Index -> Bool
/= :: Index -> Index -> Bool
Eq, Eq Index
Eq Index =>
(Index -> Index -> Ordering)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Bool)
-> (Index -> Index -> Index)
-> (Index -> Index -> Index)
-> Ord Index
Index -> Index -> Bool
Index -> Index -> Ordering
Index -> Index -> Index
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: Index -> Index -> Ordering
compare :: Index -> Index -> Ordering
$c< :: Index -> Index -> Bool
< :: Index -> Index -> Bool
$c<= :: Index -> Index -> Bool
<= :: Index -> Index -> Bool
$c> :: Index -> Index -> Bool
> :: Index -> Index -> Bool
$c>= :: Index -> Index -> Bool
>= :: Index -> Index -> Bool
$cmax :: Index -> Index -> Index
max :: Index -> Index -> Index
$cmin :: Index -> Index -> Index
min :: Index -> Index -> Index
Ord, Integer -> Index
Index -> Index
Index -> Index -> Index
(Index -> Index -> Index)
-> (Index -> Index -> Index)
-> (Index -> Index -> Index)
-> (Index -> Index)
-> (Index -> Index)
-> (Index -> Index)
-> (Integer -> Index)
-> Num Index
forall a.
(a -> a -> a)
-> (a -> a -> a)
-> (a -> a -> a)
-> (a -> a)
-> (a -> a)
-> (a -> a)
-> (Integer -> a)
-> Num a
$c+ :: Index -> Index -> Index
+ :: Index -> Index -> Index
$c- :: Index -> Index -> Index
- :: Index -> Index -> Index
$c* :: Index -> Index -> Index
* :: Index -> Index -> Index
$cnegate :: Index -> Index
negate :: Index -> Index
$cabs :: Index -> Index
abs :: Index -> Index
$csignum :: Index -> Index
signum :: Index -> Index
$cfromInteger :: Integer -> Index
fromInteger :: Integer -> Index
Num)

addIdxXTraverse
  :: forall r bst sig m
   . ( Has (State Int :+: State Index :+: State (Set Int) :+: Error (ProtocolError r bst)) sig m
     , Enum r
     , Bounded r
     , Ord r
     )
  => XTraverse m Creat Idx r bst
addIdxXTraverse :: forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has
   (State Int
    :+: (State Index
         :+: (State (Set Int) :+: Error (ProtocolError r bst))))
   sig
   m,
 Enum r, Bounded r, Ord r) =>
XTraverse m Creat Idx r bst
addIdxXTraverse =
  ( \(XMsg Creat, (String, [String], r, r, Protocol Creat r bst))
_ -> do
      inputIdx <- forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get @Int
      modify @Int (+ 1)
      Index idx <- get @Index
      modify @Index (+ 1)
      outputInx <- get @Int
      pure (inputIdx, outputInx, idx)
  , m Int -> ((), (Int, Protocol Creat r bst)) -> m Int
forall a b. a -> b -> a
const m Int
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get
  , \(XBranch Creat
_, (r, [BranchSt Creat r bst])
_) -> do
      inputIdx <- forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get @Int
      modify (Set.insert inputIdx)
      pure (inputIdx, id)
  , \(XBranchSt Creat, (bst, Protocol Creat r bst))
_ -> do
      Index -> m ()
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
s -> m ()
put (Int -> Index
Index Int
0)
      forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
(s -> s) -> m ()
modify @Int (Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1)
  , m Int -> ((), Int) -> m Int
forall a b. a -> b -> a
const m Int
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get
  , m Int -> () -> m Int
forall a b. a -> b -> a
const m Int
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get
  )

reRankXTraverse :: (Monad m) => IntMap Int -> XTraverse m Idx Idx r bst
reRankXTraverse :: forall (m :: * -> *) r bst.
Monad m =>
IntMap Int -> XTraverse m Idx Idx r bst
reRankXTraverse IntMap Int
sbm =
  ( \((Int
a, Int
b, Int
idx), (String, [String], r, r, Protocol Idx r bst)
_) -> (Int, Int, Int) -> m (Int, Int, Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntMap Int -> Int -> Int
replaceVal IntMap Int
sbm Int
a, IntMap Int -> Int -> Int
replaceVal IntMap Int
sbm Int
b, Int
idx)
  , \(XLabel Idx
xs, (Int, Protocol Idx r bst)
_) -> Int -> m Int
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntMap Int -> Int -> Int
replaceVal IntMap Int
sbm Int
XLabel Idx
xs)
  , \(XBranch Idx
a, (r, [BranchSt Idx r bst])
_) -> (Int, m (Protocol Idx r bst) -> m (Protocol Idx r bst))
-> m (Int, m (Protocol Idx r bst) -> m (Protocol Idx r bst))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntMap Int -> Int -> Int
replaceVal IntMap Int
sbm Int
XBranch Idx
a, m (Protocol Idx r bst) -> m (Protocol Idx r bst)
forall a. a -> a
id)
  , \(XBranchSt Idx, (bst, Protocol Idx r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XGoto Idx
xs, Int
_) -> Int -> m Int
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntMap Int -> Int -> Int
replaceVal IntMap Int
sbm Int
XGoto Idx
xs)
  , \XTerminal Idx
xs -> Int -> m Int
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntMap Int -> Int -> Int
replaceVal IntMap Int
sbm Int
XTerminal Idx
xs)
  )

addNumsXTraverse
  :: forall r bst sig m
   . ( Has (Error (ProtocolError r bst)) sig m
     , Enum r
     , Bounded r
     , Ord r
     )
  => XTraverse m Idx AddNums r bst
addNumsXTraverse :: forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Error (ProtocolError r bst)) sig m, Enum r, Bounded r,
 Ord r) =>
XTraverse m Idx AddNums r bst
addNumsXTraverse =
  let mkNums :: Int -> [Int]
mkNums Int
i =
        let sized :: Int
sized = r -> Int
forall a. Enum a => a -> Int
fromEnum (forall a. Bounded a => a
maxBound @r) Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1
         in (r -> Int) -> [r] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (\r
x -> Int
i Int -> Int -> Int
forall a. Num a => a -> a -> a
* Int
sized Int -> Int -> Int
forall a. Num a => a -> a -> a
+ r -> Int
forall a. Enum a => a -> Int
fromEnum r
x) (forall r. (Enum r, Bounded r) => [r]
rRange @r)
   in ( \((Int
va, Int
vb, Int
idx), (String, [String], r, r, Protocol Idx r bst)
_) -> ([Int], [Int], Int) -> m ([Int], [Int], Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> [Int]
mkNums Int
va, Int -> [Int]
mkNums Int
vb, Int
idx)
      , \(XLabel Idx
va, (Int, Protocol Idx r bst)
_) -> [Int] -> m [Int]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Int] -> m [Int]) -> [Int] -> m [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
mkNums Int
XLabel Idx
va
      , \(XBranch Idx
va, (r, [BranchSt Idx r bst])
_) -> ([Int], m (Protocol AddNums r bst) -> m (Protocol AddNums r bst))
-> m ([Int],
      m (Protocol AddNums r bst) -> m (Protocol AddNums r bst))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (Int -> [Int]
mkNums Int
XBranch Idx
va, m (Protocol AddNums r bst) -> m (Protocol AddNums r bst)
forall a. a -> a
id)
      , \(XBranchSt Idx, (bst, Protocol Idx r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
      , \(XGoto Idx
va, Int
_) -> [Int] -> m [Int]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Int] -> m [Int]) -> [Int] -> m [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
mkNums Int
XGoto Idx
va
      , \XTerminal Idx
va -> [Int] -> m [Int]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Int] -> m [Int]) -> [Int] -> m [Int]
forall a b. (a -> b) -> a -> b
$ Int -> [Int]
mkNums Int
XTerminal Idx
va
      )

toGenConstrXTraverse :: (Monad m) => XTraverse m AddNums (GenConst r) r bst
toGenConstrXTraverse :: forall (m :: * -> *) r bst.
Monad m =>
XTraverse m AddNums (GenConst r) r bst
toGenConstrXTraverse =
  ( \(([Int]
a, [Int]
b, Int
i), (String
_, [String]
_, r
from, r
to, Protocol AddNums r bst
_)) -> (([Int], [Int]), (r, r), Int) -> m (([Int], [Int]), (r, r), Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([Int]
a, [Int]
b), (r
from, r
to), Int
i)
  , \(XLabel AddNums
is, (Int
i, Protocol AddNums r bst
_)) -> ([Int], Int) -> m ([Int], Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Int]
XLabel AddNums
is, Int
i)
  , \(XBranch AddNums
xv, (r, [BranchSt AddNums r bst])
_) -> ([Int],
 m (Protocol (GenConst r) r bst) -> m (Protocol (GenConst r) r bst))
-> m ([Int],
      m (Protocol (GenConst r) r bst) -> m (Protocol (GenConst r) r bst))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Int]
XBranch AddNums
xv, m (Protocol (GenConst r) r bst) -> m (Protocol (GenConst r) r bst)
forall a. a -> a
id)
  , \(XBranchSt AddNums, (bst, Protocol AddNums r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XGoto AddNums
xs, Int
i) -> ([Int], Int) -> m ([Int], Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([Int]
XGoto AddNums
xs, Int
i)
  , \XTerminal AddNums
xv -> [Int] -> m [Int]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [Int]
XTerminal AddNums
xv
  )

data CurrSt = Decide | Undecide deriving (Int -> CurrSt -> ShowS
[CurrSt] -> ShowS
CurrSt -> String
(Int -> CurrSt -> ShowS)
-> (CurrSt -> String) -> ([CurrSt] -> ShowS) -> Show CurrSt
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
$cshowsPrec :: Int -> CurrSt -> ShowS
showsPrec :: Int -> CurrSt -> ShowS
$cshow :: CurrSt -> String
show :: CurrSt -> String
$cshowList :: [CurrSt] -> ShowS
showList :: [CurrSt] -> ShowS
Show, CurrSt -> CurrSt -> Bool
(CurrSt -> CurrSt -> Bool)
-> (CurrSt -> CurrSt -> Bool) -> Eq CurrSt
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
$c== :: CurrSt -> CurrSt -> Bool
== :: CurrSt -> CurrSt -> Bool
$c/= :: CurrSt -> CurrSt -> Bool
/= :: CurrSt -> CurrSt -> Bool
Eq, Eq CurrSt
Eq CurrSt =>
(CurrSt -> CurrSt -> Ordering)
-> (CurrSt -> CurrSt -> Bool)
-> (CurrSt -> CurrSt -> Bool)
-> (CurrSt -> CurrSt -> Bool)
-> (CurrSt -> CurrSt -> Bool)
-> (CurrSt -> CurrSt -> CurrSt)
-> (CurrSt -> CurrSt -> CurrSt)
-> Ord CurrSt
CurrSt -> CurrSt -> Bool
CurrSt -> CurrSt -> Ordering
CurrSt -> CurrSt -> CurrSt
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
$ccompare :: CurrSt -> CurrSt -> Ordering
compare :: CurrSt -> CurrSt -> Ordering
$c< :: CurrSt -> CurrSt -> Bool
< :: CurrSt -> CurrSt -> Bool
$c<= :: CurrSt -> CurrSt -> Bool
<= :: CurrSt -> CurrSt -> Bool
$c> :: CurrSt -> CurrSt -> Bool
> :: CurrSt -> CurrSt -> Bool
$c>= :: CurrSt -> CurrSt -> Bool
>= :: CurrSt -> CurrSt -> Bool
$cmax :: CurrSt -> CurrSt -> CurrSt
max :: CurrSt -> CurrSt -> CurrSt
$cmin :: CurrSt -> CurrSt -> CurrSt
min :: CurrSt -> CurrSt -> CurrSt
Ord)

getRCurrSt :: forall r sig m. (Has (State (Map r CurrSt)) sig m, Ord r) => r -> m CurrSt
getRCurrSt :: forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (State (Map r CurrSt)) sig m, Ord r) =>
r -> m CurrSt
getRCurrSt r
r =
  forall s (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (State s) sig m =>
(s -> a) -> m a
gets @(Map r CurrSt) (r -> Map r CurrSt -> Maybe CurrSt
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup r
r) m (Maybe CurrSt) -> (Maybe CurrSt -> m CurrSt) -> m CurrSt
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Maybe CurrSt
Nothing -> String -> m CurrSt
forall a. HasCallStack => String -> a
error String
"np"
    Just CurrSt
v -> CurrSt -> m CurrSt
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure CurrSt
v

restoreWrapper1 :: forall r sig m a. (Has (State (Map r CurrSt) :+: State r) sig m) => m a -> m a
restoreWrapper1 :: forall r (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (State (Map r CurrSt) :+: State r) sig m =>
m a -> m a
restoreWrapper1 m a
m = do
  s1 <- forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get @(Map r CurrSt)
  s2 <- get @r
  a <- m
  put s1
  put s2
  pure a

checkProtXFold
  :: forall r bst sig m
   . (Has (State (Map r CurrSt) :+: State r :+: Error (ProtocolError r bst)) sig m, Eq r, Ord r, Enum r, Bounded r)
  => XFold m (GenConst r) r bst
checkProtXFold :: forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has
   (State (Map r CurrSt)
    :+: (State r :+: Error (ProtocolError r bst)))
   sig
   m,
 Eq r, Ord r, Enum r, Bounded r) =>
XFold m (GenConst r) r bst
checkProtXFold =
  ( \((([Int], [Int])
_, (r
from, r
to), Int
idx), (String
msgName, [String]
_, r
_, r
_, Protocol (GenConst r) r bst
prot)) -> do
      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        r1 <- forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get @r
        if from == r1
          then pure ()
          else throwError @(ProtocolError r bst) (BranchFirstMsgMustHaveTheSameSender r1 msgName from)
      fromCurrSt <- r -> m CurrSt
forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (State (Map r CurrSt)) sig m, Ord r) =>
r -> m CurrSt
getRCurrSt r
from
      when (fromCurrSt == Undecide) (throwError @(ProtocolError r bst) (UndecideStateCanNotSendMsg msgName))
      modify (Map.insert to Decide)
      case prot of
        Terminal XTerminal (GenConst r)
_ -> do
          vals <- forall s (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (State s) sig m =>
(s -> a) -> m a
gets @(Map r CurrSt) Map r CurrSt -> [CurrSt]
forall k a. Map k a -> [a]
Map.elems
          when (any (/= Decide) vals) (throwError @(ProtocolError r bst) (TerminalNeedAllRoleDecide msgName))
        Protocol (GenConst r) r bst
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XLabel (GenConst r), Int)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XBranch (GenConst r)
_, (r
r1, [BranchSt (GenConst r) r bst]
ls)) -> do
      r1CurrSt <- r -> m CurrSt
forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (State (Map r CurrSt)) sig m, Ord r) =>
r -> m CurrSt
getRCurrSt r
r1
      when (r1CurrSt == Undecide) (throwError @(ProtocolError r bst) (UndecideStateCanNotStartBranch ls))
      for_ [r | r <- rRange, r /= r1] $ \r
r -> (Map r CurrSt -> Map r CurrSt) -> m ()
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
(s -> s) -> m ()
modify (r -> CurrSt -> Map r CurrSt -> Map r CurrSt
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert r
r CurrSt
Undecide)
      when (length ls < 1) (throwError @(ProtocolError r bst) BranchAtLeastOneBranch)
      put r1
      pure (restoreWrapper1 @r)
  , \(XBranchSt (GenConst r), (bst, Protocol (GenConst r) r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XGoto (GenConst r), Int)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \XTerminal (GenConst r)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  )

genConstrXFold
  :: forall r bst sig m
   . (Has (State (IntMap [Int]) :+: State [Int] :+: Writer (Seq C.Constraint) :+: Error (ProtocolError r bst)) sig m, Enum r)
  => XFold m (GenConst r) r bst
genConstrXFold :: forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has
   (State (IntMap [Int])
    :+: (State [Int]
         :+: (Writer (Seq Constraint) :+: Error (ProtocolError r bst))))
   sig
   m,
 Enum r) =>
XFold m (GenConst r) r bst
genConstrXFold =
  ( \((([Int]
is, [Int]
os), (r
from, r
to), Int
index), (String, [String], r, r, Protocol (GenConst r) r bst)
_) -> do
      let ifrom :: Int
ifrom = r -> Int
forall a. Enum a => a -> Int
fromEnum r
from
          ito :: Int
ito = r -> Int
forall a. Enum a => a -> Int
fromEnum r
to
          from' :: Int
from' = [Int]
is [Int] -> Int -> Int
forall a. HasCallStack => [a] -> Int -> a
!! Int
ifrom --- is
          to' :: Int
to' = [Int]
is [Int] -> Int -> Int
forall a. HasCallStack => [a] -> Int -> a
!! Int
ito ------- is
          deleteIndexFromTo :: [Int] -> [Int]
deleteIndexFromTo [Int]
ks =
            ((Int, Int) -> Int) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Int) -> Int
forall a b. (a, b) -> b
snd ([(Int, Int)] -> [Int]) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Int) -> Bool) -> [(Int, Int)] -> [(Int, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
idx, Int
_) -> Int
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
ifrom Bool -> Bool -> Bool
&& Int
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
ito) ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Int]
ks
          deleteIndexFrom :: [Int] -> [Int]
deleteIndexFrom [Int]
ks =
            ((Int, Int) -> Int) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (Int, Int) -> Int
forall a b. (a, b) -> b
snd ([(Int, Int)] -> [Int]) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Int) -> Bool) -> [(Int, Int)] -> [(Int, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
idx, Int
_) -> Int
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= Int
ifrom) ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Int]
ks

      Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when (Int
index Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== Int
0) (m () -> m ()) -> m () -> m ()
forall a b. (a -> b) -> a -> b
$ do
        branchSts <- forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get @[Int]
        tellSeq $ map (uncurry C.Constraint) $ zip (deleteIndexFrom branchSts) (deleteIndexFrom is)

      [Constraint] -> m ()
forall a (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Writer (Seq a)) sig m =>
[a] -> m ()
tellSeq ([Constraint] -> m ()) -> [Constraint] -> m ()
forall a b. (a -> b) -> a -> b
$
        Int -> Int -> Constraint
C.Constraint Int
from' Int
to'
          Constraint -> [Constraint] -> [Constraint]
forall a. a -> [a] -> [a]
: (Int -> Int -> Constraint) -> [Int] -> [Int] -> [Constraint]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Int -> Constraint
C.Constraint ([Int] -> [Int]
deleteIndexFromTo [Int]
is) ([Int] -> [Int]
deleteIndexFromTo [Int]
os)
  , \(([Int]
is, Int
i), Int
lb) ->
      (IntMap [Int] -> Maybe [Int]) -> m (Maybe [Int])
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (State s) sig m =>
(s -> a) -> m a
gets (forall a. Int -> IntMap a -> Maybe a
IntMap.lookup @[Int] Int
i) m (Maybe [Int]) -> (Maybe [Int] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Just [Int]
_ -> forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError @(ProtocolError r bst) (Int -> ProtocolError r bst
forall r bst. Int -> ProtocolError r bst
DefLabelMultTimes Int
lb)
        Maybe [Int]
Nothing -> (IntMap [Int] -> IntMap [Int]) -> m ()
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
(s -> s) -> m ()
modify (Int -> [Int] -> IntMap [Int] -> IntMap [Int]
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i [Int]
is)
  , \(XBranch (GenConst r)
is, (r, [BranchSt (GenConst r) r bst])
_) -> do
      [Int] -> m ()
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
s -> m ()
put [Int]
XBranch (GenConst r)
is
      (m () -> m ()) -> m (m () -> m ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (forall s (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (State s) sig m =>
m a -> m a
restoreWrapper @[Int])
  , \(XBranchSt (GenConst r), (bst, Protocol (GenConst r) r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(([Int]
xs, Int
i), Int
gt) -> do
      (IntMap [Int] -> Maybe [Int]) -> m (Maybe [Int])
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (State s) sig m =>
(s -> a) -> m a
gets (Int -> IntMap [Int] -> Maybe [Int]
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i) m (Maybe [Int]) -> (Maybe [Int] -> m ()) -> m ()
forall a b. m a -> (a -> m b) -> m b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        Maybe [Int]
Nothing -> forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError @(ProtocolError r bst) (Int -> ProtocolError r bst
forall r bst. Int -> ProtocolError r bst
LabelUndefined Int
gt)
        Just [Int]
ls -> [Constraint] -> m ()
forall a (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Writer (Seq a)) sig m =>
[a] -> m ()
tellSeq ([Constraint] -> m ()) -> [Constraint] -> m ()
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Constraint) -> [Int] -> [Int] -> [Constraint]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Int -> Constraint
C.Constraint [Int]
xs [Int]
ls
  , \(XTerminal (GenConst r)
xs) -> [Constraint] -> m ()
forall a (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Writer (Seq a)) sig m =>
[a] -> m ()
tellSeq ([Constraint] -> m ()) -> [Constraint] -> m ()
forall a b. (a -> b) -> a -> b
$ (Int -> Int -> Constraint) -> [Int] -> [Int] -> [Constraint]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith Int -> Int -> Constraint
C.Constraint [Int]
XTerminal (GenConst r)
xs ([Int] -> [Int]
forall a. HasCallStack => [a] -> [a]
cycle [-Int
1])
  )

replXTraverse :: (Monad m) => C.SubMap -> XTraverse m (GenConst r) (GenConst r) r bst
replXTraverse :: forall (m :: * -> *) r bst.
Monad m =>
IntMap Int -> XTraverse m (GenConst r) (GenConst r) r bst
replXTraverse IntMap Int
sbm =
  ( \((([Int]
a, [Int]
b), (r
from, r
to), Int
i), (String, [String], r, r, Protocol (GenConst r) r bst)
_) ->
      (([Int], [Int]), (r, r), Int) -> m (([Int], [Int]), (r, r), Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ((IntMap Int -> [Int] -> [Int]
replaceList IntMap Int
sbm [Int]
a, IntMap Int -> [Int] -> [Int]
replaceList IntMap Int
sbm [Int]
b), (r
from, r
to), Int
i)
  , \(([Int]
xs, Int
i), (Int, Protocol (GenConst r) r bst)
_) -> ([Int], Int) -> m ([Int], Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntMap Int -> [Int] -> [Int]
replaceList IntMap Int
sbm [Int]
xs, Int
i)
  , \(XBranch (GenConst r)
a, (r, [BranchSt (GenConst r) r bst])
_) -> ([Int],
 m (Protocol (GenConst r) r bst) -> m (Protocol (GenConst r) r bst))
-> m ([Int],
      m (Protocol (GenConst r) r bst) -> m (Protocol (GenConst r) r bst))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntMap Int -> [Int] -> [Int]
replaceList IntMap Int
sbm [Int]
XBranch (GenConst r)
a, m (Protocol (GenConst r) r bst) -> m (Protocol (GenConst r) r bst)
forall a. a -> a
id)
  , \(XBranchSt (GenConst r), (bst, Protocol (GenConst r) r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(([Int]
xs, Int
i), Int
_) -> ([Int], Int) -> m ([Int], Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntMap Int -> [Int] -> [Int]
replaceList IntMap Int
sbm [Int]
xs, Int
i)
  , \XTerminal (GenConst r)
xs -> [Int] -> m [Int]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (IntMap Int -> [Int] -> [Int]
replaceList IntMap Int
sbm [Int]
XTerminal (GenConst r)
xs)
  )

collectBranchDynValXFold :: (Has (State (Set Int)) sig m, Enum r) => XFold m (GenConst r) r bst
collectBranchDynValXFold :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) r bst.
(Has (State (Set Int)) sig m, Enum r) =>
XFold m (GenConst r) r bst
collectBranchDynValXFold =
  ( \(XMsg (GenConst r),
 (String, [String], r, r, Protocol (GenConst r) r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XLabel (GenConst r), Int)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XBranch (GenConst r)
ls, (r
r, [BranchSt (GenConst r) r bst]
_)) -> do
      let ls' :: [Int]
ls' = ((Int, Int) -> Int) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> [a] -> [b]
map (Int, Int) -> Int
forall a b. (a, b) -> b
snd ([(Int, Int)] -> [Int]) -> [(Int, Int)] -> [Int]
forall a b. (a -> b) -> a -> b
$ ((Int, Int) -> Bool) -> [(Int, Int)] -> [(Int, Int)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\(Int
i, Int
_) -> Int
i Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
/= r -> Int
forall a. Enum a => a -> Int
fromEnum r
r) ([(Int, Int)] -> [(Int, Int)]) -> [(Int, Int)] -> [(Int, Int)]
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Int]
XBranch (GenConst r)
ls
      (Set Int -> Set Int) -> m ()
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
(s -> s) -> m ()
modify (Set Int -> Set Int -> Set Int
forall a. Ord a => Set a -> Set a -> Set a
`Set.union` ([Int] -> Set Int
forall a. Ord a => [a] -> Set a
Set.fromList [Int]
ls'))
      (m () -> m ()) -> m (m () -> m ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure m () -> m ()
forall a. a -> a
id
  , \(XBranchSt (GenConst r), (bst, Protocol (GenConst r) r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XGoto (GenConst r), Int)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \XTerminal (GenConst r)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  )

genT
  :: forall bst sig m
   . (Has (Reader (Set Int) :+: State bst) sig m)
  => (bst -> Int -> T bst) -> Int -> m (T bst)
genT :: forall bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader (Set Int) :+: State bst) sig m =>
(bst -> Int -> T bst) -> Int -> m (T bst)
genT bst -> Int -> T bst
fun Int
i = do
  dynSet <- forall r (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader r) sig m =>
m r
ask @(Set Int)
  if i == -1
    then pure (TEnd)
    else
      if Set.member i dynSet
        then do
          bst <- get
          pure (fun bst i)
        else pure $ TNum i

genMsgTXTraverse
  :: forall r bst sig m
   . (Has (Reader (Set Int) :+: State bst) sig m, Enum r, Eq r, Bounded r)
  => XTraverse m (GenConst r) (MsgT r bst) r bst
genMsgTXTraverse :: forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Reader (Set Int) :+: State bst) sig m, Enum r, Eq r,
 Bounded r) =>
XTraverse m (GenConst r) (MsgT r bst) r bst
genMsgTXTraverse =
  ( \((([Int]
is, [Int]
_), (r
from, r
to), Int
vi), (String, [String], r, r, Protocol (GenConst r) r bst)
_) -> do
      is' <- [(r, Int)] -> ((r, Int) -> m (T bst)) -> m [T bst]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM ([r] -> [Int] -> [(r, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [r]
forall r. (Enum r, Bounded r) => [r]
rRange [Int]
is) (((r, Int) -> m (T bst)) -> m [T bst])
-> ((r, Int) -> m (T bst)) -> m [T bst]
forall a b. (a -> b) -> a -> b
$
        \(r
key, Int
i) -> forall bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader (Set Int) :+: State bst) sig m =>
(bst -> Int -> T bst) -> Int -> m (T bst)
genT @bst (\bst
bst1 Int
i1 -> if r
key r -> r -> Bool
forall a. Eq a => a -> a -> Bool
== r
from then Int -> bst -> T bst
forall bst. Int -> bst -> T bst
BstList Int
i1 bst
bst1 else Int -> T bst
forall bst. Int -> T bst
TAny Int
i1) Int
i
      pure (is', (from, to), vi)
  , \(([Int]
ls, Int
idx), (Int, Protocol (GenConst r) r bst)
_) -> do
      ls' <- (Int -> m (T bst)) -> [Int] -> m [T bst]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM ((bst -> Int -> T bst) -> Int -> m (T bst)
forall bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader (Set Int) :+: State bst) sig m =>
(bst -> Int -> T bst) -> Int -> m (T bst)
genT ((Int -> T bst) -> bst -> Int -> T bst
forall a b. a -> b -> a
const Int -> T bst
forall bst. Int -> T bst
TAny)) [Int]
ls
      pure (ls', idx)
  , \(XBranch (GenConst r)
ls, (r
r, [BranchSt (GenConst r) r bst]
_)) -> do
      ls' <- ((Int, Int) -> m (T bst)) -> [(Int, Int)] -> m [T bst]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (\(Int
idx, Int
v) -> (bst -> Int -> T bst) -> Int -> m (T bst)
forall bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader (Set Int) :+: State bst) sig m =>
(bst -> Int -> T bst) -> Int -> m (T bst)
genT (if Int
idx Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== r -> Int
forall a. Enum a => a -> Int
fromEnum r
r then (Int -> T bst) -> bst -> Int -> T bst
forall a b. a -> b -> a
const Int -> T bst
forall bst. Int -> T bst
TNum else ((Int -> T bst) -> bst -> Int -> T bst
forall a b. a -> b -> a
const Int -> T bst
forall bst. Int -> T bst
TAny)) Int
v) ([Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
0 ..] [Int]
XBranch (GenConst r)
ls)
      pure (ls', restoreWrapper @bst)
  , \(XBranchSt (GenConst r)
_, (bst
bst, Protocol (GenConst r) r bst
_)) -> bst -> m ()
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
s -> m ()
put bst
bst
  , \(([Int]
is, Int
i), Int
_) -> do
      is' <- (Int -> m (T bst)) -> [Int] -> m [T bst]
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
(a -> m b) -> t a -> m (t b)
forall (m :: * -> *) a b. Monad m => (a -> m b) -> [a] -> m [b]
mapM (forall bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Reader (Set Int) :+: State bst) sig m =>
(bst -> Int -> T bst) -> Int -> m (T bst)
genT @bst ((Int -> T bst) -> bst -> Int -> T bst
forall a b. a -> b -> a
const Int -> T bst
forall bst. Int -> T bst
TAny)) [Int]
is
      pure (is', i)
  , \XTerminal (GenConst r)
ls -> XTerminal (MsgT r bst) -> m (XTerminal (MsgT r bst))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (XTerminal (MsgT r bst) -> m (XTerminal (MsgT r bst)))
-> XTerminal (MsgT r bst) -> m (XTerminal (MsgT r bst))
forall a b. (a -> b) -> a -> b
$ (Int -> T bst) -> [Int] -> [T bst]
forall a b. (a -> b) -> [a] -> [b]
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap (T bst -> Int -> T bst
forall a b. a -> b -> a
const T bst
forall bst. T bst
TEnd) [Int]
XTerminal (GenConst r)
ls
  )

getFirstXV :: Protocol (MsgT r bst) r bst -> [T bst]
getFirstXV :: forall r bst. Protocol (MsgT r bst) r bst -> [T bst]
getFirstXV = \case
  Msg ([T bst]
xv, (r, r)
_, Int
_) String
_ [String]
_ r
_ r
_ :> Protocol (MsgT r bst) r bst
_ -> [T bst]
xv
  Label ([T bst]
xv, Int
_) Int
_ :> Protocol (MsgT r bst) r bst
_ -> [T bst]
xv
  Branch XBranch (MsgT r bst)
xv r
_ [BranchSt (MsgT r bst) r bst]
_ -> [T bst]
XBranch (MsgT r bst)
xv
  Goto ([T bst]
xv, Int
_) Int
_ -> [T bst]
xv
  Terminal XTerminal (MsgT r bst)
xv -> [T bst]
XTerminal (MsgT r bst)
xv

genMsgT1XTraverse :: (Monad m, Enum r) => XTraverse m (MsgT r bst) (MsgT1 r bst) r bst
genMsgT1XTraverse :: forall (m :: * -> *) r bst.
(Monad m, Enum r) =>
XTraverse m (MsgT r bst) (MsgT1 r bst) r bst
genMsgT1XTraverse =
  ( \(([T bst]
is, (r
from, r
to), Int
i), (String
_, [String]
_, r
_, r
_, Protocol (MsgT r bst) r bst
prot)) -> do
      let os :: [T bst]
os = Protocol (MsgT r bst) r bst -> [T bst]
forall r bst. Protocol (MsgT r bst) r bst -> [T bst]
getFirstXV Protocol (MsgT r bst) r bst
prot
          from' :: Int
from' = r -> Int
forall a. Enum a => a -> Int
fromEnum r
from
          to' :: Int
to' = r -> Int
forall a. Enum a => a -> Int
fromEnum r
to
      ((T bst, T bst, T bst), (r, r), Int)
-> m ((T bst, T bst, T bst), (r, r), Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (([T bst]
is [T bst] -> Int -> T bst
forall a. HasCallStack => [a] -> Int -> a
!! Int
from', [T bst]
os [T bst] -> Int -> T bst
forall a. HasCallStack => [a] -> Int -> a
!! Int
from', [T bst]
os [T bst] -> Int -> T bst
forall a. HasCallStack => [a] -> Int -> a
!! Int
to'), (r
from, r
to), Int
i)
  , \(XLabel (MsgT r bst)
a, (Int, Protocol (MsgT r bst) r bst)
_) -> ([T bst], Int) -> m ([T bst], Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([T bst], Int)
XLabel (MsgT r bst)
a
  , \(XBranch (MsgT r bst)
a, (r, [BranchSt (MsgT r bst) r bst])
_) -> ([T bst],
 m (Protocol (MsgT1 r bst) r bst)
 -> m (Protocol (MsgT1 r bst) r bst))
-> m ([T bst],
      m (Protocol (MsgT1 r bst) r bst)
      -> m (Protocol (MsgT1 r bst) r bst))
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([T bst]
XBranch (MsgT r bst)
a, m (Protocol (MsgT1 r bst) r bst)
-> m (Protocol (MsgT1 r bst) r bst)
forall a. a -> a
id)
  , \(XBranchSt (MsgT r bst)
a, (bst, Protocol (MsgT r bst) r bst)
_) -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
XBranchSt (MsgT r bst)
a
  , \(XGoto (MsgT r bst)
a, Int
_) -> ([T bst], Int) -> m ([T bst], Int)
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ([T bst], Int)
XGoto (MsgT r bst)
a
  , \XTerminal (MsgT r bst)
a -> [T bst] -> m [T bst]
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure [T bst]
XTerminal (MsgT r bst)
a
  )

data PipleResult r bst = PipleResult
  { forall r bst. PipleResult r bst -> Protocol (MsgT r bst) r bst
msgT :: Protocol (MsgT r bst) r bst
  , forall r bst. PipleResult r bst -> Protocol (MsgT1 r bst) r bst
msgT1 :: Protocol (MsgT1 r bst) r bst
  , forall r bst. PipleResult r bst -> Set Int
dnySet :: Set Int
  , forall r bst. PipleResult r bst -> (Int, Int)
stBound :: (Int, Int)
  }

reRank :: Set Int -> Int -> IntMap Int
reRank :: Set Int -> Int -> IntMap Int
reRank Set Int
branchValSet Int
maxSize =
  let allSet :: Set Int
allSet = Int -> Set Int -> Set Int
forall a. Ord a => a -> Set a -> Set a
Set.insert Int
0 Set Int
branchValSet
      restList :: [Int]
restList = [Int
i | Int
i <- [Int
0 .. Int
maxSize], Int
i Int -> Set Int -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.notMember` Set Int
allSet]
   in [(Int, Int)] -> IntMap Int
forall a. [(Int, a)] -> IntMap a
IntMap.fromList ([(Int, Int)] -> IntMap Int) -> [(Int, Int)] -> IntMap Int
forall a b. (a -> b) -> a -> b
$ [Int] -> [Int] -> [(Int, Int)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Set Int -> [Int]
forall a. Set a -> [a]
Set.toList Set Int
allSet [Int] -> [Int] -> [Int]
forall a. [a] -> [a] -> [a]
++ [Int]
restList) [Int
0 ..]

piple'
  :: forall r bst sig m
   . ( Has (Error (ProtocolError r bst)) sig m
     , Enum r
     , Bounded r
     , Eq r
     , Ord r
     )
  => (Tracer r bst -> m ())
  -> Protocol Creat r bst
  -> m (PipleResult r bst)
piple' :: forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Error (ProtocolError r bst)) sig m, Enum r, Bounded r, Eq r,
 Ord r) =>
(Tracer r bst -> m ())
-> Protocol Creat r bst -> m (PipleResult r bst)
piple' Tracer r bst -> m ()
trace Protocol Creat r bst
prot0 = do
  Tracer r bst -> m ()
trace (Protocol Creat r bst -> Tracer r bst
forall r bst. Protocol Creat r bst -> Tracer r bst
TracerProtocolCreat Protocol Creat r bst
prot0)
  (brSet, (maxSzie, (_, idxProt))) <-
    forall s (m :: * -> *) a. s -> StateC s m a -> m (s, a)
runState @(Set Int) Set Int
forall a. Set a
Set.empty
      (StateC (Set Int) m (Int, (Index, Protocol Idx r bst))
 -> m (Set Int, (Int, (Index, Protocol Idx r bst))))
-> (StateC
      Index (StateC Int (StateC (Set Int) m)) (Protocol Idx r bst)
    -> StateC (Set Int) m (Int, (Index, Protocol Idx r bst)))
-> StateC
     Index (StateC Int (StateC (Set Int) m)) (Protocol Idx r bst)
-> m (Set Int, (Int, (Index, Protocol Idx r bst)))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. s -> StateC s m a -> m (s, a)
runState @Int Int
0
      (StateC Int (StateC (Set Int) m) (Index, Protocol Idx r bst)
 -> StateC (Set Int) m (Int, (Index, Protocol Idx r bst)))
-> (StateC
      Index (StateC Int (StateC (Set Int) m)) (Protocol Idx r bst)
    -> StateC Int (StateC (Set Int) m) (Index, Protocol Idx r bst))
-> StateC
     Index (StateC Int (StateC (Set Int) m)) (Protocol Idx r bst)
-> StateC (Set Int) m (Int, (Index, Protocol Idx r bst))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall s (m :: * -> *) a. s -> StateC s m a -> m (s, a)
runState @Index (Int -> Index
Index Int
100)
      (StateC
   Index (StateC Int (StateC (Set Int) m)) (Protocol Idx r bst)
 -> m (Set Int, (Int, (Index, Protocol Idx r bst))))
-> StateC
     Index (StateC Int (StateC (Set Int) m)) (Protocol Idx r bst)
-> m (Set Int, (Int, (Index, Protocol Idx r bst)))
forall a b. (a -> b) -> a -> b
$ (XTraverse
  (StateC Index (StateC Int (StateC (Set Int) m))) Creat Idx r bst
-> Protocol Creat r bst
-> StateC
     Index (StateC Int (StateC (Set Int) m)) (Protocol Idx r bst)
forall (m :: * -> *) eta gama r bst.
Monad m =>
XTraverse m eta gama r bst
-> Protocol eta r bst -> m (Protocol gama r bst)
xtraverse XTraverse
  (StateC Index (StateC Int (StateC (Set Int) m))) Creat Idx r bst
forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has
   (State Int
    :+: (State Index
         :+: (State (Set Int) :+: Error (ProtocolError r bst))))
   sig
   m,
 Enum r, Bounded r, Ord r) =>
XTraverse m Creat Idx r bst
addIdxXTraverse Protocol Creat r bst
prot0)
  trace (TracerProtocolIdx idxProt)
  trace (TracerReRank (reRank brSet maxSzie))
  idxProt1 <- xtraverse (reRankXTraverse (reRank brSet maxSzie)) idxProt
  trace (TracerProtocolIdx idxProt1)
  prot1 <- xtraverse addNumsXTraverse idxProt1
  trace (TracerProtocolAddNum prot1)
  prot2 <- xtraverse toGenConstrXTraverse prot1
  trace (TracerProtocolGenConst prot2)
  void
    . runState @(Map r CurrSt) (Map.fromList $ zip (rRange @r) (cycle [Decide]))
    . runState @r undefined
    $ xfold checkProtXFold prot2
  (constraintList, _) <-
    runWriter @(Seq C.Constraint)
      . runState @(IntMap [Int]) (IntMap.empty)
      . runState @[Int] undefined
      $ xfold genConstrXFold prot2
  trace (TracerConstraints constraintList)
  let (sbm, stBound) = compressSubMap $ C.constrToSubMap $ toList constraintList
  trace (TracerSubMap sbm)
  prot3 <- xtraverse (replXTraverse sbm) prot2
  trace (TracerProtocolGenConstN prot3)
  dnys <- fst <$> runState @((Set Int)) (Set.empty) (xfold collectBranchDynValXFold prot3)
  trace (TracerCollectBranchDynVal dnys)
  prot4 <-
    fmap snd
      . runReader @(Set Int) dnys
      . runState @bst undefined
      $ (xtraverse genMsgTXTraverse prot3)
  trace (TracerProtocolMsgT prot4)
  prot5 <- xtraverse genMsgT1XTraverse prot4
  trace (TracerProtocolMsgT1 prot5)
  pure (PipleResult prot4 prot5 dnys stBound)

piple
  :: forall r bst
   . (Enum r, Bounded r, Eq r, Ord r)
  => Protocol Creat r bst
  -> Either
      (ProtocolError r bst)
      (PipleResult r bst)
piple :: forall r bst.
(Enum r, Bounded r, Eq r, Ord r) =>
Protocol Creat r bst
-> Either (ProtocolError r bst) (PipleResult r bst)
piple Protocol Creat r bst
protocol =
  Identity (Either (ProtocolError r bst) (PipleResult r bst))
-> Either (ProtocolError r bst) (PipleResult r bst)
forall a. Identity a -> a
run (Identity (Either (ProtocolError r bst) (PipleResult r bst))
 -> Either (ProtocolError r bst) (PipleResult r bst))
-> Identity (Either (ProtocolError r bst) (PipleResult r bst))
-> Either (ProtocolError r bst) (PipleResult r bst)
forall a b. (a -> b) -> a -> b
$ forall exc (m :: * -> *) a. ErrorC exc m a -> m (Either exc a)
runError @(ProtocolError r bst) (ErrorC (ProtocolError r bst) Identity (PipleResult r bst)
 -> Identity (Either (ProtocolError r bst) (PipleResult r bst)))
-> ErrorC (ProtocolError r bst) Identity (PipleResult r bst)
-> Identity (Either (ProtocolError r bst) (PipleResult r bst))
forall a b. (a -> b) -> a -> b
$ ((Tracer r bst -> ErrorC (ProtocolError r bst) Identity ())
-> Protocol Creat r bst
-> ErrorC (ProtocolError r bst) Identity (PipleResult r bst)
forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Error (ProtocolError r bst)) sig m, Enum r, Bounded r, Eq r,
 Ord r) =>
(Tracer r bst -> m ())
-> Protocol Creat r bst -> m (PipleResult r bst)
piple' (ErrorC (ProtocolError r bst) Identity ()
-> Tracer r bst -> ErrorC (ProtocolError r bst) Identity ()
forall a b. a -> b -> a
const (() -> ErrorC (ProtocolError r bst) Identity ()
forall a. a -> ErrorC (ProtocolError r bst) Identity a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ())) Protocol Creat r bst
protocol)

pipleWithTracer
  :: forall r bst
   . (Enum r, Bounded r, Eq r, Ord r)
  => Protocol Creat r bst
  -> ( Seq (Tracer r bst)
     , Either
        (ProtocolError r bst)
        (PipleResult r bst)
     )
pipleWithTracer :: forall r bst.
(Enum r, Bounded r, Eq r, Ord r) =>
Protocol Creat r bst
-> (Seq (Tracer r bst),
    Either (ProtocolError r bst) (PipleResult r bst))
pipleWithTracer Protocol Creat r bst
protocol =
  Identity
  (Seq (Tracer r bst),
   Either (ProtocolError r bst) (PipleResult r bst))
-> (Seq (Tracer r bst),
    Either (ProtocolError r bst) (PipleResult r bst))
forall a. Identity a -> a
run
    (Identity
   (Seq (Tracer r bst),
    Either (ProtocolError r bst) (PipleResult r bst))
 -> (Seq (Tracer r bst),
     Either (ProtocolError r bst) (PipleResult r bst)))
-> (ErrorC
      (ProtocolError r bst)
      (WriterC (Seq (Tracer r bst)) Identity)
      (PipleResult r bst)
    -> Identity
         (Seq (Tracer r bst),
          Either (ProtocolError r bst) (PipleResult r bst)))
-> ErrorC
     (ProtocolError r bst)
     (WriterC (Seq (Tracer r bst)) Identity)
     (PipleResult r bst)
-> (Seq (Tracer r bst),
    Either (ProtocolError r bst) (PipleResult r bst))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall w (m :: * -> *) a. Monoid w => WriterC w m a -> m (w, a)
runWriter @(Seq (Tracer r bst))
    (WriterC
   (Seq (Tracer r bst))
   Identity
   (Either (ProtocolError r bst) (PipleResult r bst))
 -> Identity
      (Seq (Tracer r bst),
       Either (ProtocolError r bst) (PipleResult r bst)))
-> (ErrorC
      (ProtocolError r bst)
      (WriterC (Seq (Tracer r bst)) Identity)
      (PipleResult r bst)
    -> WriterC
         (Seq (Tracer r bst))
         Identity
         (Either (ProtocolError r bst) (PipleResult r bst)))
-> ErrorC
     (ProtocolError r bst)
     (WriterC (Seq (Tracer r bst)) Identity)
     (PipleResult r bst)
-> Identity
     (Seq (Tracer r bst),
      Either (ProtocolError r bst) (PipleResult r bst))
forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall exc (m :: * -> *) a. ErrorC exc m a -> m (Either exc a)
runError @(ProtocolError r bst)
    (ErrorC
   (ProtocolError r bst)
   (WriterC (Seq (Tracer r bst)) Identity)
   (PipleResult r bst)
 -> (Seq (Tracer r bst),
     Either (ProtocolError r bst) (PipleResult r bst)))
-> ErrorC
     (ProtocolError r bst)
     (WriterC (Seq (Tracer r bst)) Identity)
     (PipleResult r bst)
-> (Seq (Tracer r bst),
    Either (ProtocolError r bst) (PipleResult r bst))
forall a b. (a -> b) -> a -> b
$ ((Tracer r bst
 -> ErrorC
      (ProtocolError r bst) (WriterC (Seq (Tracer r bst)) Identity) ())
-> Protocol Creat r bst
-> ErrorC
     (ProtocolError r bst)
     (WriterC (Seq (Tracer r bst)) Identity)
     (PipleResult r bst)
forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Error (ProtocolError r bst)) sig m, Enum r, Bounded r, Eq r,
 Ord r) =>
(Tracer r bst -> m ())
-> Protocol Creat r bst -> m (PipleResult r bst)
piple' (\Tracer r bst
w -> forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Writer w) sig m =>
w -> m ()
tell @(Seq (Tracer r bst)) (Tracer r bst -> Seq (Tracer r bst)
forall a. a -> Seq a
Seq.singleton Tracer r bst
w)) Protocol Creat r bst
protocol)

genDocXFold
  :: forall r bst ann sig m
   . ( Has (Writer [Doc ann]) sig m
     , Show r
     , Show bst
     )
  => String -> String -> XFold m (MsgT1 r bst) r bst
genDocXFold :: forall r bst ann (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Writer [Doc ann]) sig m, Show r, Show bst) =>
String -> String -> XFold m (MsgT1 r bst) r bst
genDocXFold String
rName String
protName =
  ( \( ((T bst
sendStart, T bst
sendEnd, T bst
recEnd), (r
from, r
to), Int
_)
      , (String
cons, [String]
args, r
_, r
_, Protocol (MsgT1 r bst) r bst
_)
      ) -> do
        forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Writer w) sig m =>
w -> m ()
tell @[Doc ann]
          [ String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
cons
              Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"::"
              Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
L.intercalate String
"->" [String]
args)
              Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (if [String] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [String]
args then Doc ann
forall ann. Doc ann
emptyDoc else Doc ann
"->")
              Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann
"Msg"
              Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty String
rName
              Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String
protName String -> ShowS
forall a. Semigroup a => a -> a -> a
<> String
"St")
              Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann
parens (String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ T bst -> String
forall a. Show a => a -> String
show T bst
sendStart)
              Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ Char
'\'' Char -> ShowS
forall a. a -> [a] -> [a]
: (r, T bst) -> String
forall a. Show a => a -> String
show (r
from, T bst
sendEnd))
              Doc ann -> Doc ann -> Doc ann
forall ann. Doc ann -> Doc ann -> Doc ann
<+> (String -> Doc ann
forall ann. String -> Doc ann
forall a ann. Pretty a => a -> Doc ann
pretty (String -> Doc ann) -> String -> Doc ann
forall a b. (a -> b) -> a -> b
$ Char
'\'' Char -> ShowS
forall a. a -> [a] -> [a]
: (r, T bst) -> String
forall a. Show a => a -> String
show (r
to, T bst
recEnd))
          ]
  , \(XLabel (MsgT1 r bst), Int)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XBranch (MsgT1 r bst), (r, [BranchSt (MsgT1 r bst) r bst]))
_ -> (m () -> m ()) -> m (m () -> m ())
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure (m () -> m ()
forall a. a -> a
id)
  , \(XBranchSt (MsgT1 r bst), (bst, Protocol (MsgT1 r bst) r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XGoto (MsgT1 r bst), Int)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \XTerminal (MsgT1 r bst)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  )

genDoc :: forall r bst ann. (Show r, Show bst) => String -> String -> Protocol (MsgT1 r bst) r bst -> [Doc ann]
genDoc :: forall r bst ann.
(Show r, Show bst) =>
String -> String -> Protocol (MsgT1 r bst) r bst -> [Doc ann]
genDoc String
rName String
protName Protocol (MsgT1 r bst) r bst
prot =
  ([Doc ann], ()) -> [Doc ann]
forall a b. (a, b) -> a
fst (([Doc ann], ()) -> [Doc ann]) -> ([Doc ann], ()) -> [Doc ann]
forall a b. (a -> b) -> a -> b
$ Identity ([Doc ann], ()) -> ([Doc ann], ())
forall a. Identity a -> a
run (Identity ([Doc ann], ()) -> ([Doc ann], ()))
-> Identity ([Doc ann], ()) -> ([Doc ann], ())
forall a b. (a -> b) -> a -> b
$ forall w (m :: * -> *) a. Monoid w => WriterC w m a -> m (w, a)
runWriter @[Doc ann] (XFold (WriterC [Doc ann] Identity) (MsgT1 r bst) r bst
-> Protocol (MsgT1 r bst) r bst -> WriterC [Doc ann] Identity ()
forall (m :: * -> *) eta r bst.
Monad m =>
XFold m eta r bst -> Protocol eta r bst -> m ()
xfold (forall r bst ann (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Writer [Doc ann]) sig m, Show r, Show bst) =>
String -> String -> XFold m (MsgT1 r bst) r bst
genDocXFold @r @bst @ann String
rName String
protName) Protocol (MsgT1 r bst) r bst
prot)