{-# LANGUAGE AllowAmbiguousTypes #-}
{-# LANGUAGE ConstraintKinds #-}
{-# LANGUAGE DeriveFunctor #-}
{-# LANGUAGE EmptyCase #-}
{-# LANGUAGE FlexibleContexts #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE LambdaCase #-}
{-# LANGUAGE MultiWayIf #-}
{-# LANGUAGE NamedFieldPuns #-}
{-# LANGUAGE NumericUnderscores #-}
{-# LANGUAGE OverloadedStrings #-}
{-# LANGUAGE PatternSynonyms #-}
{-# LANGUAGE RankNTypes #-}
{-# LANGUAGE ScopedTypeVariables #-}
{-# LANGUAGE TypeAbstractions #-}
{-# LANGUAGE TypeApplications #-}
{-# LANGUAGE TypeFamilies #-}
{-# LANGUAGE TypeOperators #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE NoFieldSelectors #-}
{-# OPTIONS_GHC -Wno-unused-do-bind #-}

module TypedSession.State.Pipeline (pipe, pipeWithTracer, genGraph, PipeResult (..)) 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 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 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) 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) 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, String, [BranchSt Creat r bst])
_) -> do
      inputIdx <- forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get @Int
      pure (inputIdx, id)
  , \(XBranchSt Creat, (bst, [[String]], 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
  )

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, String, [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, [[String]], 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, String, [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, [[String]], 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
internalError
    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
     , Show bst
     )
  => 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, Show bst) =>
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, String
_, [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
r, [[String]]
_, Protocol (GenConst r) r bst
prot)) ->
      if Protocol (GenConst r) r bst -> Bool
forall eta r bst. Protocol eta r bst -> Bool
isMsgExistBeforeNextTerm Protocol (GenConst r) r bst
prot
        then () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
        else forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError @(ProtocolError r bst) (String -> ProtocolError r bst
forall r bst. String -> ProtocolError r bst
MsgDoNotExistBeforeNextTerm (bst -> String
forall a. Show a => a -> String
show bst
r))
  , \(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 ()
  )

isMsgExistBeforeNextTerm :: Protocol eta r bst -> Bool
isMsgExistBeforeNextTerm :: forall eta r bst. Protocol eta r bst -> Bool
isMsgExistBeforeNextTerm = \case
  Msg{} :> Protocol eta r bst
_ -> Bool
True
  Label{} :> Protocol eta r bst
port -> Protocol eta r bst -> Bool
forall eta r bst. Protocol eta r bst -> Bool
isMsgExistBeforeNextTerm Protocol eta r bst
port
  Protocol eta r bst
_ -> Bool
False

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, String, [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, [[String]], 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 :: (Has (State (Set Int)) sig m) => C.SubMap -> XTraverse m (GenConst r) (GenConst r) r bst
replXTraverse :: forall (sig :: (* -> *) -> * -> *) (m :: * -> *) r bst.
Has (State (Set Int)) sig m =>
SubMap -> XTraverse m (GenConst r) (GenConst r) r bst
replXTraverse SubMap
sbm =
  ( \((([Int]
a, [Int]
b), (r
from, r
to), Int
i), (String, [[String]], r, r, Protocol (GenConst r) r bst)
_) -> do
      a' <- SubMap -> [Int] -> m [Int]
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State (Set Int)) sig m =>
SubMap -> [Int] -> m [Int]
replaceList SubMap
sbm [Int]
a
      b' <- replaceList sbm b
      pure ((a', b'), (from, to), i)
  , \(([Int]
xs, Int
i), (Int, Protocol (GenConst r) r bst)
_) -> do
      xs' <- SubMap -> [Int] -> m [Int]
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State (Set Int)) sig m =>
SubMap -> [Int] -> m [Int]
replaceList SubMap
sbm [Int]
xs
      pure (xs', i)
  , \(XBranch (GenConst r)
a, (r, String, [BranchSt (GenConst r) r bst])
_) -> do
      a' <- SubMap -> [Int] -> m [Int]
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State (Set Int)) sig m =>
SubMap -> [Int] -> m [Int]
replaceList SubMap
sbm [Int]
XBranch (GenConst r)
a
      pure (a', id)
  , \(XBranchSt (GenConst r),
 (bst, [[String]], 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
_) -> do
      xs' <- SubMap -> [Int] -> m [Int]
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State (Set Int)) sig m =>
SubMap -> [Int] -> m [Int]
replaceList SubMap
sbm [Int]
xs
      pure (xs', i)
  , \XTerminal (GenConst r)
xs -> SubMap -> [Int] -> m [Int]
forall (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State (Set Int)) sig m =>
SubMap -> [Int] -> m [Int]
replaceList SubMap
sbm [Int]
XTerminal (GenConst r)
xs
  )

verifyProtXFold
  :: forall r bst sig m
   . (Has (State (IntMap (r, r)) :+: Error (ProtocolError r bst)) sig m, Enum r, Eq r)
  => XFold m (GenConst r) r bst
verifyProtXFold :: forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (State (IntMap (r, r)) :+: Error (ProtocolError r bst)) sig m,
 Enum r, Eq r) =>
XFold m (GenConst r) r bst
verifyProtXFold =
  ( \((([Int]
is, [Int]
_), ft :: (r, r)
ft@(r
from, r
_to), Int
_), (String, [[String]], r, r, Protocol (GenConst r) r bst)
_) -> do
      let from' :: Int
from' = [Int]
is [Int] -> Int -> Int
forall a. HasCallStack => [a] -> Int -> a
!! r -> Int
forall a. Enum a => a -> Int
fromEnum r
from
      res <- forall s (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (State s) sig m =>
(s -> a) -> m a
gets @(IntMap (r, r)) (Int -> IntMap (r, r) -> Maybe (r, r)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
from')
      case res of
        Maybe (r, r)
Nothing -> (IntMap (r, r) -> IntMap (r, r)) -> m ()
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
(s -> s) -> m ()
modify (Int -> (r, r) -> IntMap (r, r) -> IntMap (r, r)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
from' (r, r)
ft)
        Just (r, r)
ft1 -> Bool -> m () -> m ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
when ((r, r)
ft1 (r, r) -> (r, r) -> Bool
forall a. Eq a => a -> a -> Bool
/= (r, r)
ft) (forall e (sig :: (* -> *) -> * -> *) (m :: * -> *) a.
Has (Throw e) sig m =>
e -> m a
throwError @(ProtocolError r bst) ProtocolError r bst
forall r bst. ProtocolError r bst
AStateOnlyBeUsedForTheSamePair)
  , \(XLabel (GenConst r), Int)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XBranch (GenConst r), (r, String, [BranchSt (GenConst r) r bst]))
_ -> (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 @(IntMap (r, r)))
  , \(XBranchSt (GenConst r),
 (bst, [[String]], 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 ()
  )

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, String
_, [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, [[String]], 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, String
_, [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, [[String]]
_, 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
_ String
_ [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, String, [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, [[String]], 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
  )

collAllMsgBAs :: (Has (Writer [(String, [T bst], [T bst])]) sig m) => XFold m (MsgT r bst) r bst
collAllMsgBAs :: forall bst (sig :: (* -> *) -> * -> *) (m :: * -> *) r.
Has (Writer [(String, [T bst], [T bst])]) sig m =>
XFold m (MsgT r bst) r bst
collAllMsgBAs =
  ( \(([T bst]
is, (r, r)
_, Int
_), (String
cname, [[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
      [(String, [T bst], [T bst])] -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Writer w) sig m =>
w -> m ()
tell [(String
cname, [T bst]
is, [T bst]
os)]
  , \(XLabel (MsgT r bst), Int)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XBranch (MsgT r bst), (r, String, [BranchSt (MsgT 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 (MsgT r bst),
 (bst, [[String]], Protocol (MsgT r bst) r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XGoto (MsgT r bst), Int)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \XTerminal (MsgT r bst)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  )

data PipeResult r bst = PipeResult
  { forall r bst. PipeResult r bst -> Protocol (MsgT r bst) r bst
msgT :: Protocol (MsgT r bst) r bst
  , forall r bst. PipeResult r bst -> Protocol (MsgT1 r bst) r bst
msgT1 :: Protocol (MsgT1 r bst) r bst
  , forall r bst. PipeResult r bst -> Set Int
dnySet :: Set Int
  , forall r bst. PipeResult r bst -> [Int]
stList :: [Int]
  , forall r bst.
PipeResult r bst -> [(String, [(bst, [[String]], T bst)])]
branchResultTypeInfo :: [(String, [(bst, [[String]], T bst)])]
  , forall r bst. PipeResult r bst -> [(r, String, T bst)]
branchFunList :: [(r, String, T bst)]
  , forall r bst. PipeResult r bst -> [(String, [T bst], [T bst])]
allMsgBATypes :: [(String, [T bst], [T bst])]
  }

genBranchResultTIXFold
  :: forall r bst sig m
   . ( Has (State String :+: Writer [(r, String, T bst)] :+: (State (Map String [(bst, [[String]], T bst)]))) sig m
     , Enum r
     )
  => XFold m (MsgT1 r bst) r bst
genBranchResultTIXFold :: forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has
   (State String
    :+: (Writer [(r, String, T bst)]
         :+: State (Map String [(bst, [[String]], T bst)])))
   sig
   m,
 Enum r) =>
XFold m (MsgT1 r bst) r bst
genBranchResultTIXFold =
  ( \(XMsg (MsgT1 r bst),
 (String, [[String]], r, r, Protocol (MsgT1 r bst) r bst))
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XLabel (MsgT1 r bst), Int)
_ -> () -> m ()
forall a. a -> m a
forall (f :: * -> *) a. Applicative f => a -> f a
pure ()
  , \(XBranch (MsgT1 r bst)
ts, (r
r, String
st, [BranchSt (MsgT1 r bst) r bst]
_)) -> do
      [(r, String, T bst)] -> m ()
forall w (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (Writer w) sig m =>
w -> m ()
tell [(r
r, String
st, [T bst]
XBranch (MsgT1 r bst)
ts [T bst] -> Int -> T bst
forall a. HasCallStack => [a] -> Int -> a
!! (r -> Int
forall a. Enum a => a -> Int
fromEnum r
r))]
      String -> m ()
forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
s -> m ()
put String
st
      (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 @String)
  , \(XBranchSt (MsgT1 r bst)
_, (bst
bst, [[String]]
args, Protocol (MsgT1 r bst) r bst
prot)) -> do
      case Protocol (MsgT1 r bst) r bst -> Maybe (T bst)
forall r bst. Protocol (MsgT1 r bst) r bst -> Maybe (T bst)
getNextT Protocol (MsgT1 r bst) r bst
prot of
        Maybe (T bst)
Nothing -> String -> m ()
forall a. HasCallStack => String -> a
error String
internalError
        Just T bst
t -> do
          name <- forall s (sig :: (* -> *) -> * -> *) (m :: * -> *).
Has (State s) sig m =>
m s
get @String
          modify @(Map String [(bst, [[String]], T bst)]) (Map.insertWith (<>) name [(bst, args, t)])
  , \(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 ()
  )

getNextT :: Protocol (MsgT1 r bst) r bst -> Maybe (T bst)
getNextT :: forall r bst. Protocol (MsgT1 r bst) r bst -> Maybe (T bst)
getNextT = \case
  Msg ((T bst
a, T bst
_, T bst
_), (r, r)
_, Int
_) String
_ [[String]]
_ r
_ r
_ :> Protocol (MsgT1 r bst) r bst
_ -> T bst -> Maybe (T bst)
forall a. a -> Maybe a
Just T bst
a
  Label{} :> Protocol (MsgT1 r bst) r bst
prot -> Protocol (MsgT1 r bst) r bst -> Maybe (T bst)
forall r bst. Protocol (MsgT1 r bst) r bst -> Maybe (T bst)
getNextT Protocol (MsgT1 r bst) r bst
prot
  Protocol (MsgT1 r bst) r bst
_ -> Maybe (T bst)
forall a. Maybe a
Nothing

pipe'
  :: forall r bst sig m
   . ( Has (Error (ProtocolError r bst)) sig m
     , Enum r
     , Bounded r
     , Eq r
     , Ord r
     , Show bst
     )
  => (Tracer r bst -> m ())
  -> Protocol Creat r bst
  -> m (PipeResult r bst)
pipe' :: forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Error (ProtocolError r bst)) sig m, Enum r, Bounded r, Eq r,
 Ord r, Show bst) =>
(Tracer r bst -> m ())
-> Protocol Creat r bst -> m (PipeResult r bst)
pipe' 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)
  idxProt <-
    ((Int, (Index, Protocol Idx r bst)) -> Protocol Idx r bst)
-> m (Int, (Index, Protocol Idx r bst)) -> m (Protocol Idx r bst)
forall a b. (a -> b) -> m a -> m b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap ((Index, Protocol Idx r bst) -> Protocol Idx r bst
forall a b. (a, b) -> b
snd ((Index, Protocol Idx r bst) -> Protocol Idx r bst)
-> ((Int, (Index, Protocol Idx r bst))
    -> (Index, Protocol Idx r bst))
-> (Int, (Index, Protocol Idx r bst))
-> Protocol Idx r bst
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Index, Protocol Idx r bst)) -> (Index, Protocol Idx r bst)
forall a b. (a, b) -> b
snd)
      (m (Int, (Index, Protocol Idx r bst)) -> m (Protocol Idx r bst))
-> (StateC Index (StateC Int m) (Protocol Idx r bst)
    -> m (Int, (Index, Protocol Idx r bst)))
-> StateC Index (StateC Int m) (Protocol Idx r bst)
-> m (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 m (Index, Protocol Idx r bst)
 -> m (Int, (Index, Protocol Idx r bst)))
-> (StateC Index (StateC Int m) (Protocol Idx r bst)
    -> StateC Int m (Index, Protocol Idx r bst))
-> StateC Index (StateC Int m) (Protocol Idx r bst)
-> 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
1_000_000)
      (StateC Index (StateC Int m) (Protocol Idx r bst)
 -> m (Protocol Idx r bst))
-> StateC Index (StateC Int m) (Protocol Idx r bst)
-> m (Protocol Idx r bst)
forall a b. (a -> b) -> a -> b
$ (XTraverse (StateC Index (StateC Int m)) Creat Idx r bst
-> Protocol Creat r bst
-> StateC Index (StateC 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 m)) Creat Idx r bst
forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (State Int :+: State Index) sig m, Enum r, Bounded r,
 Ord r) =>
XTraverse m Creat Idx r bst
addIdxXTraverse Protocol Creat r bst
prot0)
  trace (TracerProtocolIdx idxProt)
  prot1 <- xtraverse addNumsXTraverse idxProt
  trace (TracerProtocolAddNum prot1)
  prot2 <- xtraverse toGenConstrXTraverse prot1
  trace (TracerProtocolGenConst prot2)
  void
    . runState @(Map r CurrSt) (Map.fromList $ zip (rRange @r) (cycle [Decide]))
    . runState @r (error internalError)
    $ xfold checkProtXFold prot2
  (constraintList, _) <-
    runWriter @(Seq C.Constraint)
      . runState @(IntMap [Int]) (IntMap.empty)
      . runState @[Int] (error internalError)
      $ xfold genConstrXFold prot2
  trace (TracerConstraints constraintList)
  let sbm = [Constraint] -> SubMap
C.constrToSubMap ([Constraint] -> SubMap) -> [Constraint] -> SubMap
forall a b. (a -> b) -> a -> b
$ Seq Constraint -> [Constraint]
forall a. Seq a -> [a]
forall (t :: * -> *) a. Foldable t => t a -> [a]
toList Seq Constraint
constraintList
  (stSet, prot3) <- runState (Set.singleton (-1)) $ xtraverse (replXTraverse sbm) prot2
  trace (TracerSubMapAndStList (sbm, stSet))
  trace (TracerProtocolGenConstN prot3)
  verifyResult <- fst <$> runState @(IntMap (r, r)) (IntMap.empty) (xfold verifyProtXFold prot3)
  trace (TracerVerifyResult verifyResult)
  dnys <- fst <$> runState @((Set Int)) (Set.empty) (xfold collectBranchDynValXFold prot3)
  trace (TracerCollectBranchDynVal dnys)
  prot4 <-
    fmap snd
      . runReader @(Set Int) dnys
      . runState @bst (error internalError)
      $ (xtraverse genMsgTXTraverse prot3)
  trace (TracerProtocolMsgT prot4)
  allMsgBAs <- fst <$> runWriter @[(String, [T bst], [T bst])] (xfold collAllMsgBAs prot4)
  prot5 <- xtraverse genMsgT1XTraverse prot4
  trace (TracerProtocolMsgT1 prot5)
  (bfl, (_, (branchTIMap, _))) <-
    runWriter @[(r, String, T bst)]
      . runState @String (error internalError)
      . runState @(Map String [(bst, [[String]], T bst)]) Map.empty
      $ xfold genBranchResultTIXFold prot5
  trace (TracerBranchResultTI bfl branchTIMap)
  pure (PipeResult prot4 prot5 dnys (Set.toList stSet) (Map.toList branchTIMap) bfl allMsgBAs)

pipe
  :: forall r bst
   . (Enum r, Bounded r, Eq r, Ord r, Show bst)
  => Protocol Creat r bst
  -> Either
      (ProtocolError r bst)
      (PipeResult r bst)
pipe :: forall r bst.
(Enum r, Bounded r, Eq r, Ord r, Show bst) =>
Protocol Creat r bst
-> Either (ProtocolError r bst) (PipeResult r bst)
pipe Protocol Creat r bst
protocol =
  Identity (Either (ProtocolError r bst) (PipeResult r bst))
-> Either (ProtocolError r bst) (PipeResult r bst)
forall a. Identity a -> a
run (Identity (Either (ProtocolError r bst) (PipeResult r bst))
 -> Either (ProtocolError r bst) (PipeResult r bst))
-> Identity (Either (ProtocolError r bst) (PipeResult r bst))
-> Either (ProtocolError r bst) (PipeResult 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 (PipeResult r bst)
 -> Identity (Either (ProtocolError r bst) (PipeResult r bst)))
-> ErrorC (ProtocolError r bst) Identity (PipeResult r bst)
-> Identity (Either (ProtocolError r bst) (PipeResult 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 (PipeResult r bst)
forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Error (ProtocolError r bst)) sig m, Enum r, Bounded r, Eq r,
 Ord r, Show bst) =>
(Tracer r bst -> m ())
-> Protocol Creat r bst -> m (PipeResult r bst)
pipe' (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)

pipeWithTracer
  :: forall r bst
   . (Enum r, Bounded r, Eq r, Ord r, Show bst)
  => Protocol Creat r bst
  -> ( Seq (Tracer r bst)
     , Either
        (ProtocolError r bst)
        (PipeResult r bst)
     )
pipeWithTracer :: forall r bst.
(Enum r, Bounded r, Eq r, Ord r, Show bst) =>
Protocol Creat r bst
-> (Seq (Tracer r bst),
    Either (ProtocolError r bst) (PipeResult r bst))
pipeWithTracer Protocol Creat r bst
protocol =
  Identity
  (Seq (Tracer r bst),
   Either (ProtocolError r bst) (PipeResult r bst))
-> (Seq (Tracer r bst),
    Either (ProtocolError r bst) (PipeResult r bst))
forall a. Identity a -> a
run
    (Identity
   (Seq (Tracer r bst),
    Either (ProtocolError r bst) (PipeResult r bst))
 -> (Seq (Tracer r bst),
     Either (ProtocolError r bst) (PipeResult r bst)))
-> (ErrorC
      (ProtocolError r bst)
      (WriterC (Seq (Tracer r bst)) Identity)
      (PipeResult r bst)
    -> Identity
         (Seq (Tracer r bst),
          Either (ProtocolError r bst) (PipeResult r bst)))
-> ErrorC
     (ProtocolError r bst)
     (WriterC (Seq (Tracer r bst)) Identity)
     (PipeResult r bst)
-> (Seq (Tracer r bst),
    Either (ProtocolError r bst) (PipeResult 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) (PipeResult r bst))
 -> Identity
      (Seq (Tracer r bst),
       Either (ProtocolError r bst) (PipeResult r bst)))
-> (ErrorC
      (ProtocolError r bst)
      (WriterC (Seq (Tracer r bst)) Identity)
      (PipeResult r bst)
    -> WriterC
         (Seq (Tracer r bst))
         Identity
         (Either (ProtocolError r bst) (PipeResult r bst)))
-> ErrorC
     (ProtocolError r bst)
     (WriterC (Seq (Tracer r bst)) Identity)
     (PipeResult r bst)
-> Identity
     (Seq (Tracer r bst),
      Either (ProtocolError r bst) (PipeResult 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)
   (PipeResult r bst)
 -> (Seq (Tracer r bst),
     Either (ProtocolError r bst) (PipeResult r bst)))
-> ErrorC
     (ProtocolError r bst)
     (WriterC (Seq (Tracer r bst)) Identity)
     (PipeResult r bst)
-> (Seq (Tracer r bst),
    Either (ProtocolError r bst) (PipeResult 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)
     (PipeResult r bst)
forall r bst (sig :: (* -> *) -> * -> *) (m :: * -> *).
(Has (Error (ProtocolError r bst)) sig m, Enum r, Bounded r, Eq r,
 Ord r, Show bst) =>
(Tracer r bst -> m ())
-> Protocol Creat r bst -> m (PipeResult r bst)
pipe' (\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)

genGraph :: (Enum r, Bounded r, Show bst, Ord r, Show r) => PipeResult r bst -> String
genGraph :: forall r bst.
(Enum r, Bounded r, Show bst, Ord r, Show r) =>
PipeResult r bst -> String
genGraph PipeResult{Protocol (MsgT r bst) r bst
msgT :: forall r bst. PipeResult r bst -> Protocol (MsgT r bst) r bst
msgT :: Protocol (MsgT r bst) r bst
msgT} = Protocol (MsgT r bst) r bst -> String
forall r bst.
(Enum r, Bounded r, Ord r, Show bst, Show r) =>
Protocol (MsgT r bst) r bst -> String
runRender Protocol (MsgT r bst) r bst
msgT