{-# 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
to' :: Int
to' = [Int]
is [Int] -> Int -> Int
forall a. HasCallStack => [a] -> Int -> a
!! Int
ito
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