{-# LANGUAGE LambdaCase, OverloadedStrings, Rank2Types, TupleSections
, FlexibleInstances #-}
module Funcons.MSOS (
MSOS(..), Rewrite(..), liftRewrite, rewrite_rethrow, rewrite_throw, eval_catch, msos_throw,
EvalFunction(..), Strictness(..), StrictFuncon, PartiallyStrictFuncon,
NonStrictFuncon, ValueOp, NullaryFuncon, RewriteState(..),
StepRes, toStepRes,
Output, readOuts,
Mutable,
Inherited, giveINH,
Control, singleCTRL, giveCTRL,
Input,
applyFuncon, rewritten, rewriteTo, rewriteSeqTo, stepTo, stepSeqTo,rewrittens,
compstep,
norule, exception, sortErr, partialOp, internal, buildStep, sidecond,
premiseStepApp, premiseStep, premiseEval,
SeqSortOp(..),
rewriteRules, stepRules, evalRules, MSOSState(..), emptyMSOSState, emptyRewriteState, MSOSReader(..),RewriteReader(..),showIException, MSOSWriter(..), RewriteWriterr(..),
Rewritten(..), rewriteFuncons, rewriteFunconsWcount, evalFuncons
, stepTrans, rewritesToValue, rewritesToValues, rewritesToType
, emptyDCTRL, emptyINH, Interactive(..), SimIO(..)
, rewriteToValErr, count_delegation, optRefocus
, evalStrictSequence, rewriteStrictSequence, evalSequence,
showTypes, showSorts, showValues, showValuesSeq, showFuncons, showFunconsSeq,traceLib,
FunconLibrary, libUnions, libOverrides, libEmpty, libUnion, libOverride, Funcons.MSOS.libFromList,
evalctxt2exception, ctxt2exception, fromSeqValOp, fromNullaryValOp, fromValOp,
displayCounters, counterKeys, ppCounters,
)where
import Funcons.Types
import Funcons.RunOptions
import Funcons.Printer
import Funcons.Exceptions
import Funcons.Simulation
import qualified Funcons.Operations as VAL
import Control.Applicative
import Control.Arrow ((***))
import Control.Monad.Writer hiding ((<>))
import Control.Monad.Fail
import Data.Maybe (isJust, isNothing, fromJust)
import Data.List (foldl', intercalate)
import Data.Text (unpack)
import Data.Semigroup
import qualified Data.Map as M
import System.IO.Unsafe
trace :: p -> p -> p
trace p
p p
b = p
b
traceLib :: FunconLibrary -> FunconLibrary
traceLib :: FunconLibrary -> FunconLibrary
traceLib FunconLibrary
lib = IO FunconLibrary -> FunconLibrary
forall a. IO a -> a
unsafePerformIO
(String -> IO ()
putStrLn ([String] -> String
unlines ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
unpack (FunconLibrary -> [Text]
forall k a. Map k a -> [k]
M.keys FunconLibrary
lib))) IO () -> IO FunconLibrary -> IO FunconLibrary
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FunconLibrary -> IO FunconLibrary
forall (m :: * -> *) a. Monad m => a -> m a
return FunconLibrary
lib)
type FunconLibrary = M.Map Name EvalFunction
fromValOp :: ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromValOp = Bool
-> ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons)
-> EvalFunction
fromAbsValOp Bool
False
fromSeqValOp :: ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromSeqValOp = Bool
-> ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons)
-> EvalFunction
fromAbsValOp Bool
True
fromAbsValOp :: Bool -> ([Funcons] -> Funcons) -> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromAbsValOp :: Bool
-> ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons)
-> EvalFunction
fromAbsValOp Bool
seqRes [Funcons] -> Funcons
cons [OpExpr Funcons] -> OpExpr Funcons
mkExpr = ValueOp -> EvalFunction
ValueOp ValueOp
op
where op :: ValueOp
op [Values Funcons]
vs = Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report Funcons
f Bool
seqRes (OpExpr Funcons -> EvalResult Funcons
forall t. HasValues t => OpExpr t -> EvalResult t
VAL.eval ([OpExpr Funcons] -> OpExpr Funcons
mkExpr ((Values Funcons -> OpExpr Funcons)
-> [Values Funcons] -> [OpExpr Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> OpExpr Funcons
forall t. Values t -> OpExpr t
ValExpr [Values Funcons]
vs)))
where f :: Funcons
f = [Funcons] -> Funcons
cons ((Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
vs)
fromNullaryValOp :: ([Funcons] -> Funcons) -> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromNullaryValOp :: ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromNullaryValOp [Funcons] -> Funcons
cons [OpExpr Funcons] -> OpExpr Funcons
mkExpr = Rewrite Rewritten -> EvalFunction
NullaryFuncon Rewrite Rewritten
op
where op :: Rewrite Rewritten
op = Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report ([Funcons] -> Funcons
cons []) Bool
False (OpExpr Funcons -> EvalResult Funcons
forall t. HasValues t => OpExpr t -> EvalResult t
VAL.eval ([OpExpr Funcons] -> OpExpr Funcons
mkExpr []))
report :: Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report Funcons
f Bool
seqRes EvalResult Funcons
res = case EvalResult Funcons
res of
Error OpExpr Funcons
_ (VAL.SortErr String
str) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f String
str
Error OpExpr Funcons
_ (DomErr String
str) -> ValueOp
rewrittens []
Error OpExpr Funcons
_ (ArityErr String
str) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f String
str
Error OpExpr Funcons
_ (ProjErr String
str) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f String
str
Error OpExpr Funcons
_ (Normal (FValue Values Funcons
v)) -> Values Funcons -> Rewrite Rewritten
rewritten' Values Funcons
v
Error OpExpr Funcons
_ (Normal Funcons
t) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
t
Success (FValue (ADTVal Text
"null" [Funcons]
_)) -> ValueOp
rewrittens []
Success (FValue Values Funcons
v) -> Values Funcons -> Rewrite Rewritten
rewritten' Values Funcons
v
Success Funcons
t -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
t
where rewritten' :: Values Funcons -> Rewrite Rewritten
rewritten' Values Funcons
v | Bool
seqRes, ValSeq [Funcons]
fs <- Values Funcons
v,
let mvs :: [Maybe (Values Funcons)]
mvs = (Funcons -> Maybe (Values Funcons))
-> [Funcons] -> [Maybe (Values Funcons)]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Maybe (Values Funcons)
forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
fs, (Maybe (Values Funcons) -> Bool)
-> [Maybe (Values Funcons)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe (Values Funcons) -> Bool
forall a. Maybe a -> Bool
isJust [Maybe (Values Funcons)]
mvs
= ValueOp
rewrittens ((Maybe (Values Funcons) -> Values Funcons)
-> [Maybe (Values Funcons)] -> [Values Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Maybe (Values Funcons) -> Values Funcons
forall a. HasCallStack => Maybe a -> a
fromJust [Maybe (Values Funcons)]
mvs)
| Bool
otherwise = Values Funcons -> Rewrite Rewritten
rewritten Values Funcons
v
data EvalFunction =
NonStrictFuncon NonStrictFuncon
| StrictFuncon StrictFuncon
| PartiallyStrictFuncon [Strictness] Strictness NonStrictFuncon
| ValueOp ValueOp
| NullaryFuncon NullaryFuncon
type StrictFuncon = [Values] -> Rewrite Rewritten
type NonStrictFuncon = [Funcons] -> Rewrite Rewritten
type PartiallyStrictFuncon = NonStrictFuncon
type ValueOp = StrictFuncon
type NullaryFuncon = Rewrite Rewritten
data Strictness = Strict | NonStrict
data Rewritten =
ValTerm [Values]
| CompTerm Funcons (MSOS StepRes)
type StepRes = Either Funcons [Values]
instance Show Rewritten where
show :: Rewritten -> String
show (ValTerm [Values Funcons]
vs) = [Values Funcons] -> String
showValuesSeq [Values Funcons]
vs
show (CompTerm Funcons
_ MSOS StepRes
_) = String
"<step>"
libEmpty :: FunconLibrary
libEmpty :: FunconLibrary
libEmpty = FunconLibrary
forall k a. Map k a
M.empty
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion = (Text -> EvalFunction -> EvalFunction -> EvalFunction)
-> FunconLibrary -> FunconLibrary -> FunconLibrary
forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWithKey Text -> EvalFunction -> EvalFunction -> EvalFunction
forall p p a. Text -> p -> p -> a
op
where op :: Text -> p -> p -> a
op Text
k p
x p
_ = String -> a
forall a. HasCallStack => String -> a
error (String
"duplicate funcon name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
unpack Text
k)
libOverride :: FunconLibrary -> FunconLibrary -> FunconLibrary
libOverride :: FunconLibrary -> FunconLibrary -> FunconLibrary
libOverride = (FunconLibrary -> FunconLibrary -> FunconLibrary)
-> FunconLibrary -> FunconLibrary -> FunconLibrary
forall a b c. (a -> b -> c) -> b -> a -> c
flip FunconLibrary -> FunconLibrary -> FunconLibrary
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union
libUnions :: [FunconLibrary] -> FunconLibrary
libUnions :: [FunconLibrary] -> FunconLibrary
libUnions = (FunconLibrary -> FunconLibrary -> FunconLibrary)
-> FunconLibrary -> [FunconLibrary] -> FunconLibrary
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion FunconLibrary
libEmpty
where op :: p -> p -> a
op p
_ p
_ = String -> a
forall a. HasCallStack => String -> a
error (String
"duplicate funcon name")
libOverrides :: [FunconLibrary] -> FunconLibrary
libOverrides :: [FunconLibrary] -> FunconLibrary
libOverrides = [FunconLibrary] -> FunconLibrary
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions ([FunconLibrary] -> FunconLibrary)
-> ([FunconLibrary] -> [FunconLibrary])
-> [FunconLibrary]
-> FunconLibrary
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FunconLibrary] -> [FunconLibrary]
forall a. [a] -> [a]
reverse
libFromList :: [(Name, EvalFunction)] -> FunconLibrary
libFromList :: [(Text, EvalFunction)] -> FunconLibrary
libFromList = [(Text, EvalFunction)] -> FunconLibrary
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
lookupFuncon :: Name -> Rewrite EvalFunction
lookupFuncon :: Text -> Rewrite EvalFunction
lookupFuncon Text
key = (RewriteReader
-> RewriteState
-> (Either IException EvalFunction, RewriteState, RewriteWriterr))
-> Rewrite EvalFunction
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException EvalFunction, RewriteState, RewriteWriterr))
-> Rewrite EvalFunction)
-> (RewriteReader
-> RewriteState
-> (Either IException EvalFunction, RewriteState, RewriteWriterr))
-> Rewrite EvalFunction
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->
(case Text -> FunconLibrary -> Maybe EvalFunction
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
key (RewriteReader -> FunconLibrary
funconlib RewriteReader
ctxt) of
Just EvalFunction
f -> EvalFunction -> Either IException EvalFunction
forall a b. b -> Either a b
Right EvalFunction
f
Maybe EvalFunction
_ -> case Text -> Map Text Funcons -> Maybe Funcons
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
key (RunOptions -> Map Text Funcons
builtin_funcons (RewriteReader -> RunOptions
run_opts RewriteReader
ctxt)) of
Just Funcons
f -> EvalFunction -> Either IException EvalFunction
forall a b. b -> Either a b
Right (Rewrite Rewritten -> EvalFunction
NullaryFuncon (Funcons -> Rewrite Rewritten
rewriteTo Funcons
f))
Maybe Funcons
_ -> IException -> Either IException EvalFunction
forall a b. a -> Either a b
Left (IE -> RewriteReader -> IException
evalctxt2exception (String -> IE
Internal (String
"unknown funcon: "String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
unpack Text
key)) RewriteReader
ctxt)
, RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty)
data RewriteReader = RewriteReader
{ RewriteReader -> FunconLibrary
funconlib :: FunconLibrary
, RewriteReader -> TypeRelation
ty_env :: TypeRelation, RewriteReader -> RunOptions
run_opts :: RunOptions
, RewriteReader -> Funcons
global_fct :: Funcons, RewriteReader -> Funcons
local_fct :: Funcons }
data RewriteState = RewriteState { }
emptyRewriteState :: RewriteState
emptyRewriteState = RewriteState
RewriteState
data RewriteWriterr = RewriteWriterr { RewriteWriterr -> Counters
counters :: Counters }
newtype Rewrite a= Rewrite {Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite :: (RewriteReader -> RewriteState ->
(Either IException a, RewriteState, RewriteWriterr))}
instance Applicative Rewrite where
pure :: a -> Rewrite a
pure = a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: Rewrite (a -> b) -> Rewrite a -> Rewrite b
(<*>) = Rewrite (a -> b) -> Rewrite a -> Rewrite b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Functor Rewrite where
fmap :: (a -> b) -> Rewrite a -> Rewrite b
fmap = (a -> b) -> Rewrite a -> Rewrite b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance Monad Rewrite where
return :: a -> Rewrite a
return a
a = (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite (\RewriteReader
_ RewriteState
st -> (a -> Either IException a
forall a b. b -> Either a b
Right a
a, RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty))
(Rewrite RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f) >>= :: Rewrite a -> (a -> Rewrite b) -> Rewrite b
>>= a -> Rewrite b
k = (RewriteReader
-> RewriteState
-> (Either IException b, RewriteState, RewriteWriterr))
-> Rewrite b
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite (\RewriteReader
ctxt RewriteState
st ->
let res1 :: (Either IException a, RewriteState, RewriteWriterr)
res1@(Either IException a
e_a1,RewriteState
st1,RewriteWriterr
cs1) = RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f RewriteReader
ctxt RewriteState
st
in case Either IException a
e_a1 of
Left IException
err -> (IException -> Either IException b
forall a b. a -> Either a b
Left IException
err, RewriteState
st1, RewriteWriterr
cs1)
Right a
a1 -> let (Rewrite RewriteReader
-> RewriteState
-> (Either IException b, RewriteState, RewriteWriterr)
h) = a -> Rewrite b
k a
a1
(Either IException b
a2,RewriteState
st2,RewriteWriterr
cs2) = RewriteReader
-> RewriteState
-> (Either IException b, RewriteState, RewriteWriterr)
h RewriteReader
ctxt RewriteState
st1
in (Either IException b
a2,RewriteState
st2,RewriteWriterr
cs1 RewriteWriterr -> RewriteWriterr -> RewriteWriterr
forall a. Semigroup a => a -> a -> a
<> RewriteWriterr
cs2))
instance Semigroup RewriteWriterr where
<> :: RewriteWriterr -> RewriteWriterr -> RewriteWriterr
(<>) = RewriteWriterr -> RewriteWriterr -> RewriteWriterr
forall a. Monoid a => a -> a -> a
mappend
instance Monoid RewriteWriterr where
mempty :: RewriteWriterr
mempty = Counters -> RewriteWriterr
RewriteWriterr Counters
forall a. Monoid a => a
mempty
(RewriteWriterr Counters
cs1) mappend :: RewriteWriterr -> RewriteWriterr -> RewriteWriterr
`mappend` (RewriteWriterr Counters
cs2) = Counters -> RewriteWriterr
RewriteWriterr (Counters
cs1 Counters -> Counters -> Counters
forall a. Monoid a => a -> a -> a
`mappend` Counters
cs2)
liftRewrite :: Rewrite a -> MSOS a
liftRewrite :: Rewrite a -> MSOS a
liftRewrite Rewrite a
ev = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a)
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
let (Either IException a
e_a, RewriteState
est, RewriteWriterr
ewr) = Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite Rewrite a
ev (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) (MSOSState m -> RewriteState
forall (m :: * -> *). MSOSState m -> RewriteState
estate MSOSState m
mut)
in (Either IException a, MSOSState m, MSOSWriter)
-> m (Either IException a, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException a
e_a, MSOSState m
mut {estate :: RewriteState
estate = RewriteState
est}, MSOSWriter
forall a. Monoid a => a
mempty { ewriter :: RewriteWriterr
ewriter = RewriteWriterr
ewr })
eval_catch :: Rewrite a -> Rewrite (Either IException a)
eval_catch :: Rewrite a -> Rewrite (Either IException a)
eval_catch Rewrite a
eval = (RewriteReader
-> RewriteState
-> (Either IException (Either IException a), RewriteState,
RewriteWriterr))
-> Rewrite (Either IException a)
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException (Either IException a), RewriteState,
RewriteWriterr))
-> Rewrite (Either IException a))
-> (RewriteReader
-> RewriteState
-> (Either IException (Either IException a), RewriteState,
RewriteWriterr))
-> Rewrite (Either IException a)
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->
let (Either IException a
eval_res, RewriteState
st', RewriteWriterr
eval_cs) = Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite Rewrite a
eval RewriteReader
ctxt RewriteState
st
in (Either IException a -> Either IException (Either IException a)
forall a b. b -> Either a b
Right Either IException a
eval_res, RewriteState
st', RewriteWriterr
eval_cs)
eval_else :: (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else :: (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else IE -> Bool
prop [] Rewrite a
def = Rewrite a
def
eval_else IE -> Bool
prop (Rewrite a
ev:[Rewrite a]
evs) Rewrite a
def = Rewrite a -> Rewrite (Either IException a)
forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch Rewrite a
ev Rewrite (Either IException a)
-> (Either IException a -> Rewrite a) -> Rewrite a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Right a
a -> a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
Left (Funcons
gf,Funcons
lf,IE
ie) | IE -> Bool
prop IE
ie -> (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
forall a. (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else IE -> Bool
prop [Rewrite a]
evs Rewrite a
def
| Bool
otherwise -> IException -> Rewrite a
forall a. IException -> Rewrite a
rewrite_rethrow (Funcons
gf,Funcons
lf,IE
ie)
rewrite_rethrow :: IException -> Rewrite a
rewrite_rethrow :: IException -> Rewrite a
rewrite_rethrow IException
ie = (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a)
-> (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> (IException -> Either IException a
forall a b. a -> Either a b
Left IException
ie, RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty)
rewrite_throw :: IE -> Rewrite a
rewrite_throw :: IE -> Rewrite a
rewrite_throw IE
ie = (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a)
-> (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> (IException -> Either IException a
forall a b. a -> Either a b
Left (IE -> RewriteReader -> IException
evalctxt2exception IE
ie RewriteReader
ctxt), RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty)
evalctxt2exception :: IE -> RewriteReader -> IException
evalctxt2exception :: IE -> RewriteReader -> IException
evalctxt2exception IE
ie RewriteReader
ctxt = (RewriteReader -> Funcons
global_fct RewriteReader
ctxt, RewriteReader -> Funcons
local_fct RewriteReader
ctxt, IE
ie)
ctxt2exception :: IE -> MSOSReader m -> IException
ctxt2exception :: IE -> MSOSReader m -> IException
ctxt2exception IE
ie MSOSReader m
ctxt =
(RewriteReader -> Funcons
global_fct (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt), RewriteReader -> Funcons
local_fct (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt), IE
ie)
rewriteRules :: [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules = [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' []
rewriteRules' :: [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' :: [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' [IException]
errs [] = IE -> Rewrite Rewritten
forall a. IE -> Rewrite a
rewrite_throw ([IException] -> IE
NoMoreBranches [IException]
errs)
rewriteRules' [IException]
errs (Rewrite Rewritten
t1:[Rewrite Rewritten]
ts) = (RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten)
-> (RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->
let (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
rw_cs) = Rewrite Rewritten
-> RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite Rewrite Rewritten
t1 RewriteReader
ctxt RewriteState
st
in case Either IException Rewritten
rw_res of
Left IException
ie| IException -> Bool
failsRule IException
ie ->
String
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall p p. p -> p -> p
trace (IException -> String
showIException IException
ie) ((Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall a b. (a -> b) -> a -> b
$ Rewrite Rewritten
-> RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite (do
Rewrite ()
count_backtrack_in
Counters -> Rewrite ()
addToRCounter (RewriteWriterr -> Counters
counters RewriteWriterr
rw_cs)
[IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' (IException
ieIException -> [IException] -> [IException]
forall a. a -> [a] -> [a]
:[IException]
errs) [Rewrite Rewritten]
ts) RewriteReader
ctxt RewriteState
st
Either IException Rewritten
_ -> (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
rw_cs)
data MSOSReader m = MSOSReader{ MSOSReader m -> RewriteReader
ereader :: RewriteReader
, MSOSReader m -> Inherited
inh_entities :: Inherited
, MSOSReader m -> DownControl
dctrl_entities :: DownControl
, MSOSReader m -> Text -> m Funcons
def_fread :: Name -> m Funcons}
data MSOSWriter = MSOSWriter { MSOSWriter -> DownControl
ctrl_entities :: Control, MSOSWriter -> Inherited
out_entities :: Output
, MSOSWriter -> RewriteWriterr
ewriter :: RewriteWriterr }
data MSOSState m = MSOSState { MSOSState m -> Input m
inp_es :: Input m, MSOSState m -> Mutable
mut_entities :: Mutable
, MSOSState m -> RewriteState
estate :: RewriteState }
emptyMSOSState :: MSOSState m
emptyMSOSState :: MSOSState m
emptyMSOSState = Input m -> Mutable -> RewriteState -> MSOSState m
forall (m :: * -> *).
Input m -> Mutable -> RewriteState -> MSOSState m
MSOSState Input m
forall k a. Map k a
M.empty Mutable
forall k a. Map k a
M.empty RewriteState
emptyRewriteState
newtype MSOS a = MSOS { MSOS a
-> forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS ::
forall m. Interactive m =>
(MSOSReader m -> MSOSState m
-> m (Either IException a, MSOSState m, MSOSWriter)) }
instance Applicative MSOS where
pure :: a -> MSOS a
pure = a -> MSOS a
forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: MSOS (a -> b) -> MSOS a -> MSOS b
(<*>) = MSOS (a -> b) -> MSOS a -> MSOS b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Functor MSOS where
fmap :: (a -> b) -> MSOS a -> MSOS b
fmap = (a -> b) -> MSOS a -> MSOS b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance Monad MSOS where
return :: a -> MSOS a
return a
a = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS (\MSOSReader m
_ MSOSState m
mut -> (Either IException a, MSOSState m, MSOSWriter)
-> m (Either IException a, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Either IException a
forall a b. b -> Either a b
Right a
a,MSOSState m
mut,MSOSWriter
forall a. Monoid a => a
mempty))
(MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f) >>= :: MSOS a -> (a -> MSOS b) -> MSOS b
>>= a -> MSOS b
k = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter))
-> MSOS b
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS (\MSOSReader m
ctxt MSOSState m
mut -> do
res1 :: (Either IException a, MSOSState m, MSOSWriter)
res1@(Either IException a
e_a1,MSOSState m
mut1,MSOSWriter
wr1) <- MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f MSOSReader m
ctxt MSOSState m
mut
case Either IException a
e_a1 of
Left IException
err -> (Either IException b, MSOSState m, MSOSWriter)
-> m (Either IException b, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (IException -> Either IException b
forall a b. a -> Either a b
Left IException
err, MSOSState m
mut1, MSOSWriter
wr1)
Right a
a1 -> do
let (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter)
h) = a -> MSOS b
k a
a1
(Either IException b
a2,MSOSState m
mut2,MSOSWriter
wr2) <- MSOSReader m
-> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter)
h MSOSReader m
ctxt MSOSState m
mut1
(Either IException b, MSOSState m, MSOSWriter)
-> m (Either IException b, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException b
a2,MSOSState m
mut2,MSOSWriter
wr1 MSOSWriter -> MSOSWriter -> MSOSWriter
forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr2))
instance MonadFail MSOS where
fail :: String -> MSOS a
fail = Rewrite a -> MSOS a
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite a -> MSOS a) -> (String -> Rewrite a) -> String -> MSOS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. String -> Rewrite a
forall a. String -> Rewrite a
internal
instance Semigroup MSOSWriter where
<> :: MSOSWriter -> MSOSWriter -> MSOSWriter
(<>) = MSOSWriter -> MSOSWriter -> MSOSWriter
forall a. Monoid a => a -> a -> a
mappend
instance Monoid MSOSWriter where
mempty :: MSOSWriter
mempty = DownControl -> Inherited -> RewriteWriterr -> MSOSWriter
MSOSWriter DownControl
forall a. Monoid a => a
mempty Inherited
forall a. Monoid a => a
mempty RewriteWriterr
forall a. Monoid a => a
mempty
(MSOSWriter DownControl
x1 Inherited
x2 RewriteWriterr
x3) mappend :: MSOSWriter -> MSOSWriter -> MSOSWriter
`mappend` (MSOSWriter DownControl
y1 Inherited
y2 RewriteWriterr
y3) =
DownControl -> Inherited -> RewriteWriterr -> MSOSWriter
MSOSWriter (DownControl
x1 DownControl -> DownControl -> DownControl
forall a. Map Text a -> Map Text a -> Map Text a
`unionCTRL` DownControl
y1) (Inherited
x2 Inherited -> Inherited -> Inherited
`unionOUT` Inherited
y2) (RewriteWriterr
x3 RewriteWriterr -> RewriteWriterr -> RewriteWriterr
forall a. Monoid a => a -> a -> a
`mappend` RewriteWriterr
y3)
type Mutable = M.Map Name Values
stepRules :: [IException] -> [MSOS StepRes] -> MSOS StepRes
stepRules = ([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
NoMoreBranches Rewrite ()
count_backtrack_in
stepARules :: ([IException] -> IE) -> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules :: ([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
fexc Rewrite ()
_ [IException]
errs [] = IE -> MSOS StepRes
forall b. IE -> MSOS b
msos_throw ([IException] -> IE
fexc [IException]
errs)
stepARules [IException] -> IE
fexc Rewrite ()
counter [IException]
errs (MSOS StepRes
t1:[MSOS StepRes]
ts) = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes)
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> do
(Either IException StepRes
e_ie_a, MSOSState m
mut', MSOSWriter
wr) <- MSOS StepRes
-> MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall a.
MSOS a
-> forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS MSOS StepRes
t1 MSOSReader m
ctxt MSOSState m
mut
case Either IException StepRes
e_ie_a of
Left IException
ie | IException -> Bool
failsRule IException
ie ->
String
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall p p. p -> p -> p
trace (IException -> String
showIException IException
ie) (m (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall a b. (a -> b) -> a -> b
$ MSOS StepRes
-> MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall a.
MSOS a
-> forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS (do
Rewrite () -> MSOS ()
forall a. Rewrite a -> MSOS a
liftRewrite Rewrite ()
counter
Counters -> MSOS ()
addToCounter (RewriteWriterr -> Counters
counters (MSOSWriter -> RewriteWriterr
ewriter MSOSWriter
wr))
([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
fexc Rewrite ()
counter ([IException]
errs[IException] -> [IException] -> [IException]
forall a. [a] -> [a] -> [a]
++[IException
ie]) [MSOS StepRes]
ts) MSOSReader m
ctxt MSOSState m
mut
Either IException StepRes
_ -> (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_ie_a, MSOSState m
mut', MSOSWriter
wr)
evalRules :: [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules = [IException]
-> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules' []
evalRules' :: [IException] -> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules' :: [IException]
-> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules' [IException]
errs [] [MSOS StepRes]
msoss = MSOS StepRes -> Rewrite Rewritten
buildStep (([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
NoRule Rewrite ()
count_backtrack_out [IException]
errs [MSOS StepRes]
msoss)
evalRules' [IException]
errs ((Rewrite RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
rw_rules):[Rewrite Rewritten]
rest) [MSOS StepRes]
msoss = (RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten)
-> (RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->
let (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
wo) = RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
rw_rules RewriteReader
ctxt RewriteState
st
in case Either IException Rewritten
rw_res of
Left IException
ie | IException -> Bool
failsRule IException
ie ->
String
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall p p. p -> p -> p
trace (IException -> String
showIException IException
ie) ((Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall a b. (a -> b) -> a -> b
$ Rewrite Rewritten
-> RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite (do
Rewrite ()
count_backtrack_out
Counters -> Rewrite ()
addToRCounter (RewriteWriterr -> Counters
counters RewriteWriterr
wo)
[IException]
-> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules' (IException
ieIException -> [IException] -> [IException]
forall a. a -> [a] -> [a]
:[IException]
errs) [Rewrite Rewritten]
rest [MSOS StepRes]
msoss) RewriteReader
ctxt RewriteState
st
Either IException Rewritten
_ -> (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
wo)
msos_throw :: IE -> MSOS b
msos_throw :: IE -> MSOS b
msos_throw = Rewrite b -> MSOS b
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite b -> MSOS b) -> (IE -> Rewrite b) -> IE -> MSOS b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IE -> Rewrite b
forall a. IE -> Rewrite a
rewrite_throw
giveOpts :: MSOS RunOptions
giveOpts :: MSOS RunOptions
giveOpts = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException RunOptions, MSOSState m, MSOSWriter))
-> MSOS RunOptions
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException RunOptions, MSOSState m, MSOSWriter))
-> MSOS RunOptions)
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException RunOptions, MSOSState m, MSOSWriter))
-> MSOS RunOptions
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
(Either IException RunOptions, MSOSState m, MSOSWriter)
-> m (Either IException RunOptions, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (RunOptions -> Either IException RunOptions
forall a b. b -> Either a b
Right (RewriteReader -> RunOptions
run_opts (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt)), MSOSState m
mut, MSOSWriter
forall a. Monoid a => a
mempty)
giveINH :: MSOS Inherited
giveINH :: MSOS Inherited
giveINH = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException Inherited, MSOSState m, MSOSWriter))
-> MSOS Inherited
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException Inherited, MSOSState m, MSOSWriter))
-> MSOS Inherited)
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException Inherited, MSOSState m, MSOSWriter))
-> MSOS Inherited
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> (Either IException Inherited, MSOSState m, MSOSWriter)
-> m (Either IException Inherited, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Inherited -> Either IException Inherited
forall a b. b -> Either a b
Right (MSOSReader m -> Inherited
forall (m :: * -> *). MSOSReader m -> Inherited
inh_entities MSOSReader m
ctxt), MSOSState m
mut, MSOSWriter
forall a. Monoid a => a
mempty)
giveCTRL :: MSOS DownControl
giveCTRL :: MSOS DownControl
giveCTRL = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException DownControl, MSOSState m, MSOSWriter))
-> MSOS DownControl
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException DownControl, MSOSState m, MSOSWriter))
-> MSOS DownControl)
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException DownControl, MSOSState m, MSOSWriter))
-> MSOS DownControl
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> (Either IException DownControl, MSOSState m, MSOSWriter)
-> m (Either IException DownControl, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (DownControl -> Either IException DownControl
forall a b. b -> Either a b
Right (MSOSReader m -> DownControl
forall (m :: * -> *). MSOSReader m -> DownControl
dctrl_entities MSOSReader m
ctxt), MSOSState m
mut, MSOSWriter
forall a. Monoid a => a
mempty)
doRefocus :: MSOS Bool
doRefocus :: MSOS Bool
doRefocus = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException Bool, MSOSState m, MSOSWriter))
-> MSOS Bool
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException Bool, MSOSState m, MSOSWriter))
-> MSOS Bool)
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException Bool, MSOSState m, MSOSWriter))
-> MSOS Bool
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
(Either IException Bool, MSOSState m, MSOSWriter)
-> m (Either IException Bool, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Either IException Bool
forall a b. b -> Either a b
Right (Bool -> Either IException Bool) -> Bool -> Either IException Bool
forall a b. (a -> b) -> a -> b
$ RunOptions -> Bool
do_refocus (RewriteReader -> RunOptions
run_opts (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt)), MSOSState m
mut, MSOSWriter
forall a. Monoid a => a
mempty)
modifyRewriteCTXT :: (RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT :: (RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT RewriteReader -> RewriteReader
mod (Rewrite RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f) = (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> (RewriteReader -> RewriteReader)
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteReader -> RewriteReader
mod)
modifyRewriteReader :: (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader :: (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader RewriteReader -> RewriteReader
mod (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f) = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS (MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f (MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> (MSOSReader m -> MSOSReader m)
-> MSOSReader m
-> MSOSState m
-> m (Either IException a, MSOSState m, MSOSWriter)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MSOSReader m -> MSOSReader m
forall (m :: * -> *). MSOSReader m -> MSOSReader m
mod')
where mod' :: MSOSReader m -> MSOSReader m
mod' MSOSReader m
ctxt = MSOSReader m
ctxt { ereader :: RewriteReader
ereader = RewriteReader -> RewriteReader
mod (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) }
type Inherited = M.Map Name [Values]
emptyINH :: Inherited
emptyINH :: Inherited
emptyINH = Inherited
forall k a. Map k a
M.empty
type Control = M.Map Name (Maybe Values)
type DownControl = M.Map Name (Maybe Values)
emptyDCTRL :: DownControl
emptyDCTRL :: DownControl
emptyDCTRL = DownControl
forall k a. Map k a
M.empty
emptyCTRL :: Control
emptyCTRL :: DownControl
emptyCTRL = DownControl
forall k a. Map k a
M.empty
singleCTRL :: Name -> Values -> Control
singleCTRL :: Text -> Values Funcons -> DownControl
singleCTRL Text
k = Text -> Maybe (Values Funcons) -> DownControl
forall k a. k -> a -> Map k a
M.singleton Text
k (Maybe (Values Funcons) -> DownControl)
-> (Values Funcons -> Maybe (Values Funcons))
-> Values Funcons
-> DownControl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Values Funcons -> Maybe (Values Funcons)
forall a. a -> Maybe a
Just
unionCTRL :: Map Text a -> Map Text a -> Map Text a
unionCTRL = (Text -> a -> a -> a) -> Map Text a -> Map Text a -> Map Text a
forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWithKey (String -> a -> a -> a
forall a. HasCallStack => String -> a
error (String -> a -> a -> a) -> (Text -> String) -> Text -> a -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Text -> String
err)
where err :: Text -> String
err Text
key = String
"Two " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
unpack Text
key String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" signals converging!"
type Output = M.Map Name [Values]
unionOUT :: Output -> Output -> Output
unionOUT :: Inherited -> Inherited -> Inherited
unionOUT = ([Values Funcons] -> [Values Funcons] -> [Values Funcons])
-> Inherited -> Inherited -> Inherited
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith [Values Funcons] -> [Values Funcons] -> [Values Funcons]
forall a. [a] -> [a] -> [a]
(++)
emptyOUT :: Output
emptyOUT :: Inherited
emptyOUT = Inherited
forall k a. Map k a
M.empty
readOuts :: MSOS a -> MSOS (a, Output)
readOuts :: MSOS a -> MSOS (a, Inherited)
readOuts (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f) = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (a, Inherited), MSOSState m, MSOSWriter))
-> MSOS (a, Inherited)
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (a, Inherited), MSOSState m, MSOSWriter))
-> MSOS (a, Inherited))
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (a, Inherited), MSOSState m, MSOSWriter))
-> MSOS (a, Inherited)
forall a b. (a -> b) -> a -> b
$ (\MSOSReader m
ctxt MSOSState m
mut -> do
(Either IException a
e_a, MSOSState m
mut1, MSOSWriter
wr1) <- MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f MSOSReader m
ctxt MSOSState m
mut
case Either IException a
e_a of
Left IException
err -> (Either IException (a, Inherited), MSOSState m, MSOSWriter)
-> m (Either IException (a, Inherited), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (IException -> Either IException (a, Inherited)
forall a b. a -> Either a b
Left IException
err, MSOSState m
mut1, MSOSWriter
wr1)
Right a
a -> (Either IException (a, Inherited), MSOSState m, MSOSWriter)
-> m (Either IException (a, Inherited), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return ((a, Inherited) -> Either IException (a, Inherited)
forall a b. b -> Either a b
Right (a
a,(MSOSWriter -> Inherited
out_entities MSOSWriter
wr1))
, MSOSState m
mut1, MSOSWriter
wr1 { out_entities :: Inherited
out_entities = Inherited
forall a. Monoid a => a
mempty}))
type Input m = M.Map Name ([[Values]], Maybe (m Funcons))
data Counters = Counters !Int !Int !Int !Int !Int !Int !Int !Int
instance Semigroup Counters where
<> :: Counters -> Counters -> Counters
(<>) = Counters -> Counters -> Counters
forall a. Monoid a => a -> a -> a
mappend
instance Monoid Counters where
mempty :: Counters
mempty = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0
(Counters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8) mappend :: Counters -> Counters -> Counters
`mappend` (Counters Int
y1 Int
y2 Int
y3 Int
y4 Int
y5 Int
y6 Int
y7 Int
y8) =
Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters (Int
x1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y1) (Int
x2Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y2) (Int
x3Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y3) (Int
x4Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y4) (Int
x5Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y5) (Int
x6Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y6) (Int
x7Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y7) (Int
x8Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y8)
emptyCounters :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8 =
MSOSWriter
forall a. Monoid a => a
mempty { ewriter :: RewriteWriterr
ewriter = RewriteWriterr
forall a. Monoid a => a
mempty {counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8}}
addToCounter :: Counters -> MSOS ()
addToCounter :: Counters -> MSOS ()
addToCounter Counters
cs = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ())
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> (Either IException (), MSOSState m, MSOSWriter)
-> m (Either IException (), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Either IException ()
forall a b. b -> Either a b
Right(), MSOSState m
mut, MSOSWriter
forall a. Monoid a => a
mempty { ewriter :: RewriteWriterr
ewriter = RewriteWriterr
forall a. Monoid a => a
mempty { counters :: Counters
counters = Counters
cs } })
addToRCounter :: Counters -> Rewrite ()
addToRCounter :: Counters -> Rewrite ()
addToRCounter Counters
cs = (RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ()
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ())
-> (RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ()
forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
mut -> (() -> Either IException ()
forall a b. b -> Either a b
Right(), RewriteState
mut, RewriteWriterr
forall a. Monoid a => a
mempty { counters :: Counters
counters = Counters
cs })
count_step :: MSOS ()
count_step :: MSOS ()
count_step = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ())
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> (Either IException (), MSOSState m, MSOSWriter)
-> m (Either IException (), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Either IException ()
forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
1 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0)
count_delegation :: MSOS ()
count_delegation :: MSOS ()
count_delegation = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ())
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> (Either IException (), MSOSState m, MSOSWriter)
-> m (Either IException (), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Either IException ()
forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
0 Int
0 Int
0 Int
0 Int
0 Int
1 Int
0 Int
0)
count_refocus :: MSOS ()
count_refocus = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ())
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> (Either IException (), MSOSState m, MSOSWriter)
-> m (Either IException (), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Either IException ()
forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
0 Int
0 Int
0 Int
0 Int
1 Int
0 Int
0 Int
0)
count_restart :: MSOS ()
count_restart :: MSOS ()
count_restart = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ())
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> (Either IException (), MSOSState m, MSOSWriter)
-> m (Either IException (), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Either IException ()
forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
0 Int
0 Int
0 Int
1 Int
0 Int
0 Int
0 Int
0)
count_rewrite :: Rewrite ()
count_rewrite :: Rewrite ()
count_rewrite = (RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ()
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ())
-> (RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ()
forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (() -> Either IException ()
forall a b. b -> Either a b
Right (), RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
1 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0})
count_rewrite_attempt :: Rewrite ()
count_rewrite_attempt :: Rewrite ()
count_rewrite_attempt = (RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ()
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ())
-> (RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ()
forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (() -> Either IException ()
forall a b. b -> Either a b
Right (), RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
1 Int
0 Int
0 Int
0 Int
0 Int
0})
count_backtrack_out :: Rewrite ()
count_backtrack_out :: Rewrite ()
count_backtrack_out = (RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ()
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ())
-> (RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ()
forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (() -> Either IException ()
forall a b. b -> Either a b
Right (), RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
1 Int
0 })
count_backtrack_in :: Rewrite ()
count_backtrack_in :: Rewrite ()
count_backtrack_in = (RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ()
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ())
-> (RewriteReader
-> RewriteState
-> (Either IException (), RewriteState, RewriteWriterr))
-> Rewrite ()
forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (() -> Either IException ()
forall a b. b -> Either a b
Right (), RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
1 })
ppCounters :: Counters -> String
ppCounters Counters
cs =
String
"number of (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
counterKeys String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
"): (" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Counters -> String
displayCounters Counters
cs String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
")"
counterKeys :: String
counterKeys = String
"restarts,rewrites,(attempts),steps,refocus,premises,backtracking(outer),backtracking(inner)"
displayCounters :: Counters -> String
displayCounters (Counters Int
steps Int
rewrites Int
rattempts Int
restarts Int
refocus Int
delegations Int
bout Int
bin) =
String -> [String] -> String
forall a. [a] -> [[a]] -> [a]
intercalate String
"," ([String] -> String) -> [String] -> String
forall a b. (a -> b) -> a -> b
$
(Int -> String) -> [Int] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Int -> String
forall a. Show a => a -> String
show [Int
restarts, Int
rewrites, Int
rattempts, Int
steps, Int
refocus, Int
delegations, Int
bout, Int
bin]
norule :: Funcons -> Rewrite a
norule :: Funcons -> Rewrite a
norule Funcons
f = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw ([IException] -> IE
NoRule [])
sortErr :: Funcons -> String -> Rewrite a
sortErr :: Funcons -> String -> Rewrite a
sortErr Funcons
f String
str = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw (String -> IE
SortErr String
str)
partialOp :: Funcons -> String -> Rewrite a
partialOp :: Funcons -> String -> Rewrite a
partialOp Funcons
f String
str = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw (String -> IE
PartialOp String
str)
exception :: Funcons -> String -> Rewrite a
exception :: Funcons -> String -> Rewrite a
exception Funcons
f String
str = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw (String -> IE
Err String
str)
internal :: String -> Rewrite a
internal :: String -> Rewrite a
internal String
str = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw (String -> IE
Internal String
str)
sidecond :: String -> Rewrite a
sidecond :: String -> Rewrite a
sidecond String
str = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw (String -> IE
SideCondFail String
str)
buildStep :: MSOS StepRes -> Rewrite Rewritten
buildStep :: MSOS StepRes -> Rewrite Rewritten
buildStep = MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter (() -> MSOS ()
forall (m :: * -> *) a. Monad m => a -> m a
return ())
buildStepCount :: MSOS StepRes -> Rewrite Rewritten
buildStepCount :: MSOS StepRes -> Rewrite Rewritten
buildStepCount = MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter MSOS ()
count_delegation
buildStepCounter :: MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter :: MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter MSOS ()
counter MSOS StepRes
mf = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS ()
counter MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes
mf)
optRefocus :: MSOS StepRes -> MSOS StepRes
optRefocus :: MSOS StepRes -> MSOS StepRes
optRefocus MSOS StepRes
stepper = MSOS Bool
doRefocus MSOS Bool -> (Bool -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> MSOS StepRes -> MSOS StepRes
refocus MSOS StepRes
stepper
Bool
False -> MSOS StepRes
stepper
refocus :: MSOS StepRes -> MSOS StepRes
refocus :: MSOS StepRes -> MSOS StepRes
refocus MSOS StepRes
stepper
= MSOS ()
count_refocus MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_violates_refocus MSOS StepRes
stepper StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return StepRes -> MSOS StepRes
continue
where continue :: StepRes -> MSOS StepRes
continue = \case
Right [Values Funcons]
vs -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values Funcons] -> StepRes
forall a b. b -> Either a b
Right [Values Funcons]
vs)
Left Funcons
f ->
Rewrite Rewritten -> MSOS Rewritten
forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) MSOS Rewritten -> (Rewritten -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v] -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values Funcons] -> StepRes
forall a b. b -> Either a b
Right [Values Funcons
v])
ValTerm [Values Funcons]
vs -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return (Funcons -> StepRes
forall a b. a -> Either a b
Left Funcons
f)
Rewritten
res -> MSOS StepRes -> MSOS StepRes
refocus (MSOS StepRes -> MSOS StepRes) -> MSOS StepRes -> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ Rewritten -> MSOS StepRes
stepRewritten Rewritten
res
stepRewritten :: Rewritten -> MSOS StepRes
stepRewritten :: Rewritten -> MSOS StepRes
stepRewritten (ValTerm [Values Funcons]
vs) = StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values Funcons] -> StepRes
forall a b. b -> Either a b
Right [Values Funcons]
vs)
stepRewritten (CompTerm Funcons
f MSOS StepRes
step) = (RewriteReader -> RewriteReader) -> MSOS StepRes -> MSOS StepRes
forall a. (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader RewriteReader -> RewriteReader
mod (MSOS ()
count_step MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes
step)
where mod :: RewriteReader -> RewriteReader
mod RewriteReader
ctxt = RewriteReader
ctxt {local_fct :: Funcons
local_fct = Funcons
f}
rewritten :: Values -> Rewrite Rewritten
rewritten :: Values Funcons -> Rewrite Rewritten
rewritten = Rewritten -> Rewrite Rewritten
forall (m :: * -> *) a. Monad m => a -> m a
return (Rewritten -> Rewrite Rewritten)
-> (Values Funcons -> Rewritten)
-> Values Funcons
-> Rewrite Rewritten
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Rewritten
ValTerm ([Values Funcons] -> Rewritten)
-> (Values Funcons -> [Values Funcons])
-> Values Funcons
-> Rewritten
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Values Funcons -> [Values Funcons] -> [Values Funcons]
forall a. a -> [a] -> [a]
:[])
rewrittens :: [Values] -> Rewrite Rewritten
rewrittens :: ValueOp
rewrittens = Rewritten -> Rewrite Rewritten
forall (m :: * -> *) a. Monad m => a -> m a
return (Rewritten -> Rewrite Rewritten)
-> ([Values Funcons] -> Rewritten) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Rewritten
ValTerm
rewriteTo :: Funcons -> Rewrite Rewritten
rewriteTo :: Funcons -> Rewrite Rewritten
rewriteTo Funcons
f = Rewrite ()
count_rewrite Rewrite () -> Rewrite Rewritten -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f
rewriteSeqTo :: [Funcons] -> Rewrite Rewritten
rewriteSeqTo :: [Funcons] -> Rewrite Rewritten
rewriteSeqTo [Funcons]
fs = Rewrite ()
count_rewrite Rewrite () -> Rewrite Rewritten -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([Values Funcons] -> Rewritten
ValTerm ([Values Funcons] -> Rewritten)
-> Rewrite [Values Funcons] -> Rewrite Rewritten
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Funcons] -> Rewrite [Values Funcons]
rewriteStrictSequence [Funcons]
fs)
stepTo :: Funcons -> MSOS StepRes
stepTo :: Funcons -> MSOS StepRes
stepTo = StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return (StepRes -> MSOS StepRes)
-> (Funcons -> StepRes) -> Funcons -> MSOS StepRes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Funcons -> StepRes
forall a b. a -> Either a b
Left
stepSeqTo :: [Funcons] -> MSOS StepRes
stepSeqTo :: [Funcons] -> MSOS StepRes
stepSeqTo [Funcons]
fs = [Values Funcons] -> StepRes
forall a b. b -> Either a b
Right ([Values Funcons] -> StepRes)
-> MSOS [Values Funcons] -> MSOS StepRes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rewrite [Values Funcons] -> MSOS [Values Funcons]
forall a. Rewrite a -> MSOS a
liftRewrite ([Funcons] -> Rewrite [Values Funcons]
rewriteStrictSequence [Funcons]
fs)
if_abruptly_terminates :: Bool -> MSOS StepRes -> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes) -> MSOS StepRes
if_abruptly_terminates :: Bool
-> MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_abruptly_terminates Bool
care (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep) StepRes -> MSOS StepRes
abr StepRes -> MSOS StepRes
no_abr = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes)
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut m (Either IException StepRes, MSOSState m, MSOSWriter)
-> ((Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
(Right StepRes
f', MSOSState m
mut', MSOSWriter
wr') ->
let failed :: Bool
failed = (Maybe (Values Funcons) -> Bool) -> DownControl -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe (Values Funcons) -> Bool
forall a. Maybe a -> Bool
isJust (MSOSWriter -> DownControl
ctrl_entities MSOSWriter
wr')
MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep | Bool
failed Bool -> Bool -> Bool
&& Bool
care = StepRes -> MSOS StepRes
abr StepRes
f'
| Bool
otherwise = StepRes -> MSOS StepRes
no_abr StepRes
f'
in do (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr'') <- MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut'
(Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr' MSOSWriter -> MSOSWriter -> MSOSWriter
forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr'')
(Either IException StepRes, MSOSState m, MSOSWriter)
norule_res -> (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res
if_violates_refocus :: MSOS StepRes -> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes) -> MSOS StepRes
if_violates_refocus :: MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_violates_refocus (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep) StepRes -> MSOS StepRes
viol StepRes -> MSOS StepRes
no_viol = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes)
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut m (Either IException StepRes, MSOSState m, MSOSWriter)
-> ((Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
(Right StepRes
f', MSOSState m
mut', MSOSWriter
wr') ->
let violates :: Bool
violates = (Maybe (Values Funcons) -> Bool) -> DownControl -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe (Values Funcons) -> Bool
forall a. Maybe a -> Bool
isJust (MSOSWriter -> DownControl
ctrl_entities MSOSWriter
wr')
Bool -> Bool -> Bool
|| ([Values Funcons] -> Bool) -> Inherited -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool)
-> ([Values Funcons] -> Bool) -> [Values Funcons] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (MSOSWriter -> Inherited
out_entities MSOSWriter
wr')
Bool -> Bool -> Bool
|| (([[Values Funcons]], Maybe (m Funcons)) -> Bool)
-> Map Text ([[Values Funcons]], Maybe (m Funcons)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe (m Funcons) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (m Funcons) -> Bool)
-> (([[Values Funcons]], Maybe (m Funcons)) -> Maybe (m Funcons))
-> ([[Values Funcons]], Maybe (m Funcons))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([[Values Funcons]], Maybe (m Funcons)) -> Maybe (m Funcons)
forall a b. (a, b) -> b
snd) (MSOSState m -> Map Text ([[Values Funcons]], Maybe (m Funcons))
forall (m :: * -> *). MSOSState m -> Input m
inp_es MSOSState m
mut')
MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep | Bool
violates = StepRes -> MSOS StepRes
viol StepRes
f'
| Bool
otherwise = StepRes -> MSOS StepRes
no_viol StepRes
f'
in do (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr'') <- MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut'
(Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr' MSOSWriter -> MSOSWriter -> MSOSWriter
forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr'')
(Either IException StepRes, MSOSState m, MSOSWriter)
norule_res -> (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res
premiseEval :: ([Values] -> Rewrite Rewritten) -> (MSOS StepRes -> MSOS StepRes) ->
Funcons -> Rewrite Rewritten
premiseEval :: ValueOp
-> (MSOS StepRes -> MSOS StepRes) -> Funcons -> Rewrite Rewritten
premiseEval ValueOp
vapp MSOS StepRes -> MSOS StepRes
fapp Funcons
f = Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons]
vs -> ValueOp
vapp [Values Funcons]
vs
CompTerm Funcons
_ MSOS StepRes
step -> MSOS StepRes -> Rewrite Rewritten
buildStepCount (MSOS StepRes -> MSOS StepRes
optRefocus (MSOS StepRes -> MSOS StepRes
fapp MSOS StepRes
step))
premiseStepApp :: (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp :: (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp StepRes -> StepRes
app Funcons
f = Rewrite Rewritten -> MSOS Rewritten
forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) MSOS Rewritten -> (Rewritten -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons]
vs -> IE -> MSOS StepRes
forall b. IE -> MSOS b
msos_throw ([Values Funcons] -> IE
StepOnValue [Values Funcons]
vs)
CompTerm Funcons
_ MSOS StepRes
step -> StepRes -> StepRes
app (StepRes -> StepRes) -> MSOS StepRes -> MSOS StepRes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSOS ()
count_delegation MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes -> MSOS StepRes
optRefocus MSOS StepRes
step)
premiseStep :: Funcons -> MSOS StepRes
premiseStep :: Funcons -> MSOS StepRes
premiseStep = (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp StepRes -> StepRes
forall a. a -> a
id
evalFuncons :: Funcons -> MSOS StepRes
evalFuncons :: Funcons -> MSOS StepRes
evalFuncons Funcons
f = Rewrite Rewritten -> MSOS Rewritten
forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) MSOS Rewritten -> (Rewritten -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rewritten -> MSOS StepRes
stepRewritten
rewritesToType :: Funcons -> Rewrite Types
rewritesToType :: Funcons -> Rewrite Types
rewritesToType Funcons
f = do
Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f Rewrite Rewritten -> (Rewritten -> Rewrite Types) -> Rewrite Types
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [v :: Values Funcons
v@(ComputationType ComputationTypes Funcons
_)] -> Types -> Rewrite Types
forall (m :: * -> *) a. Monad m => a -> m a
return (Values Funcons -> Types
forall t. Values t -> Types t
downcastValueType Values Funcons
v)
Rewritten
_ -> Rewrite Types
forall a. Rewrite a
rewriteToValErr
rewritesToValue :: Funcons -> Rewrite Values
rewritesToValue :: Funcons -> Rewrite (Values Funcons)
rewritesToValue Funcons
f = do
Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f Rewrite Rewritten
-> (Rewritten -> Rewrite (Values Funcons))
-> Rewrite (Values Funcons)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v] -> Values Funcons -> Rewrite (Values Funcons)
forall (m :: * -> *) a. Monad m => a -> m a
return Values Funcons
v
Rewritten
_ -> Rewrite (Values Funcons)
forall a. Rewrite a
rewriteToValErr
rewritesToValues :: Funcons -> Rewrite [Values]
rewritesToValues :: Funcons -> Rewrite [Values Funcons]
rewritesToValues Funcons
f = do
Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f Rewrite Rewritten
-> (Rewritten -> Rewrite [Values Funcons])
-> Rewrite [Values Funcons]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons]
vs -> [Values Funcons] -> Rewrite [Values Funcons]
forall (m :: * -> *) a. Monad m => a -> m a
return [Values Funcons]
vs
Rewritten
_ -> Rewrite [Values Funcons]
forall a. Rewrite a
rewriteToValErr
rewriteToValErr :: Rewrite a
rewriteToValErr = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw (IE -> Rewrite a) -> IE -> Rewrite a
forall a b. (a -> b) -> a -> b
$
String -> IE
SideCondFail String
"side-condition/entity-value/annotation evaluation requires step"
rewriteFunconsWcount :: Funcons -> Rewrite Rewritten
rewriteFunconsWcount :: Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f = Rewrite ()
count_rewrite_attempt Rewrite () -> Rewrite Rewritten -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f
rewriteFuncons :: Funcons -> Rewrite Rewritten
rewriteFuncons :: Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f = (RewriteReader -> RewriteReader)
-> Rewrite Rewritten -> Rewrite Rewritten
forall a.
(RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT (\RewriteReader
ctxt -> RewriteReader
ctxt{local_fct :: Funcons
local_fct = Funcons
f}) (Funcons -> Rewrite Rewritten
rewriteFuncons' Funcons
f)
where
rewriteFuncons' :: Funcons -> Rewrite Rewritten
rewriteFuncons' (FValue Values Funcons
v) = Rewritten -> Rewrite Rewritten
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values Funcons] -> Rewritten
ValTerm [Values Funcons
v])
rewriteFuncons' (FSet [Funcons]
fs) = [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
fs (Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> ([Values Funcons] -> Values Funcons) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Values Funcons
setval_) [Funcons] -> Funcons
FSet
rewriteFuncons' (FMap [Funcons]
fs) = [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
fs (Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> ([Values Funcons] -> Values Funcons) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Values Funcons
mapval_) [Funcons] -> Funcons
FMap
rewriteFuncons' f :: Funcons
f@(FBinding Funcons
fk [Funcons]
fv) = [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence (Funcons
fkFuncons -> [Funcons] -> [Funcons]
forall a. a -> [a] -> [a]
:[Funcons]
fv) (Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> ([Values Funcons] -> Values Funcons) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Values Funcons
forall t. HasValues t => [Values t] -> Values t
tuple) [Funcons] -> Funcons
mkBinding
where mkBinding :: [Funcons] -> Funcons
mkBinding (Funcons
k:[Funcons]
fvs) = Funcons -> [Funcons] -> Funcons
FBinding Funcons
k [Funcons]
fvs
mkBinding [Funcons]
_ = String -> Funcons
forall a. HasCallStack => String -> a
error String
"invalid binding-notation"
rewriteFuncons' f :: Funcons
f@(FSortPower Funcons
s1 Funcons
fn) = case (Funcons
s1,Funcons
fn) of
(FValue mty :: Values Funcons
mty@(ComputationType ComputationTypes Funcons
_), FValue Values Funcons
v)
| Nat Integer
n <- Values Funcons -> Values Funcons
forall t. Values t -> Values t
upcastNaturals Values Funcons
v ->
ValueOp
rewrittens (Int -> Values Funcons -> [Values Funcons]
forall a. Int -> a -> [a]
replicate (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) (ComputationTypes Funcons -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType (Types -> ComputationTypes Funcons
forall t. Types t -> ComputationTypes t
Type (Values Funcons -> Types
forall t. Values t -> Types t
downcastValueType Values Funcons
mty))))
(FValue Values Funcons
mty, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
fn Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortPower Funcons
s1 (Values Funcons -> Funcons
FValue Values Funcons
v)
ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f String
"second operand of ^ cannot compute a sequence"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortPower Funcons
s1) MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"^_ multiadic argument"
(Funcons, Funcons)
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortPower (Values Funcons -> Funcons
FValue Values Funcons
v) Funcons
fn
ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f String
"first operand of ^ cannot compute a sequence"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie ((Funcons -> Funcons -> Funcons) -> Funcons -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortPower Funcons
fn) MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"_^ multiadic argument"
rewriteFuncons' f :: Funcons
f@(FSortSeq Funcons
s1 SeqSortOp
op) = case Funcons
s1 of
(FValue (ComputationType (Type Types
ty))) -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ComputationTypes Funcons -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType (ComputationTypes Funcons -> Values Funcons)
-> ComputationTypes Funcons -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Types -> ComputationTypes Funcons
forall t. Types t -> ComputationTypes t
Type (Types -> ComputationTypes Funcons)
-> Types -> ComputationTypes Funcons
forall a b. (a -> b) -> a -> b
$ Types -> SeqSortOp -> Types
forall t. Types t -> SeqSortOp -> Types t
AnnotatedType Types
ty SeqSortOp
op
(FValue Values Funcons
_) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> SeqSortOp -> Funcons
FSortSeq Funcons
s1 SeqSortOp
op) String
"sort-sequence operator not on type"
Funcons
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> SeqSortOp -> Funcons
FSortSeq (Values Funcons -> Funcons
FValue Values Funcons
v1) SeqSortOp
op
ValTerm [Values Funcons]
vs -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> SeqSortOp -> Funcons
FSortSeq Funcons
s1 SeqSortOp
op) String
"operand of sort-sequence operator cannot compute a sequence"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie ((Funcons -> SeqSortOp -> Funcons)
-> SeqSortOp -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> SeqSortOp -> Funcons
FSortSeq SeqSortOp
op) MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"sort-sequence operator, multiadic argument"
rewriteFuncons' (FSortComputes Funcons
f1) = case Funcons
f1 of
(FValue (ComputationType (Type Types
ty))) -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ComputationTypes Funcons -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType (ComputationTypes Funcons -> Values Funcons)
-> ComputationTypes Funcons -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Types -> ComputationTypes Funcons
forall t. Types t -> ComputationTypes t
ComputesType Types
ty
(FValue Values Funcons
_) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons
FSortComputes Funcons
f1) String
"=> not applied to a type"
Funcons
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
FSortComputes (Values Funcons -> Funcons
FValue Values Funcons
v1)
ValTerm [Values Funcons]
vs -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons
FSortComputes Funcons
f1) String
"operand of => cannot compute a sequence"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie Funcons -> Funcons
FSortComputes MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"=>_ multiadic argument"
rewriteFuncons' (FSortComputesFrom Funcons
f1 Funcons
f2) = case (Funcons
f1,Funcons
f2) of
(FValue (ComputationType (Type Types
ty1)),FValue (ComputationType (Type Types
ty2)))
-> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ComputationTypes Funcons -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType (Types -> Types -> ComputationTypes Funcons
forall t. Types t -> Types t -> ComputationTypes t
ComputesFromType Types
ty1 Types
ty2)
(FValue Values Funcons
_, FValue Values Funcons
_) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) String
"=> not applied to types"
(FValue (ComputationType (Type Types
ty1)),Funcons
_)
-> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f2 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 (Values Funcons -> Funcons
FValue Values Funcons
v2)
ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) String
"second operand of => cannot compute a sequence"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1) MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"_=>_ multiadic operand (2)"
(Funcons
_,Funcons
_)
-> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortComputesFrom (Values Funcons -> Funcons
FValue Values Funcons
v1) Funcons
f2
ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) String
"_=>_ multiadic operand (1)"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie ((Funcons -> Funcons -> Funcons) -> Funcons -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f2) MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"_=>_ multiadic operand (1)"
rewriteFuncons' (FSortUnion Funcons
s1 Funcons
s2) = case (Funcons
s1, Funcons
s2) of
(FValue (ComputationType (Type Types
t1))
, FValue (ComputationType (Type Types
t2))) -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values Funcons
typeVal (Types -> Values Funcons) -> Types -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Types -> Types -> Types
forall t. Types t -> Types t -> Types t
Union Types
t1 Types
t2
(FValue Values Funcons
_, FValue Values Funcons
_) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) String
"sort-union not applied to two sorts"
(FValue Values Funcons
v1, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s2 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 (Values Funcons -> Funcons
FValue Values Funcons
v2)
ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) String
"sort-union multiadic argument (2)"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1) MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"sort-union multiadic argument (2)"
(Funcons, Funcons)
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortUnion (Values Funcons -> Funcons
FValue Values Funcons
v) Funcons
s2
ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) String
"sort-union multiadic argument (1)"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie ((Funcons -> Funcons -> Funcons) -> Funcons -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortUnion Funcons
s2) MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"sort-union multiadic argument (1)"
rewriteFuncons' (FSortInter Funcons
s1 Funcons
s2) = case (Funcons
s1, Funcons
s2) of
(FValue (ComputationType (Type Types
t1))
, FValue (ComputationType (Type Types
t2))) -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values Funcons
typeVal (Types -> Values Funcons) -> Types -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Types -> Types -> Types
forall t. Types t -> Types t -> Types t
Intersection Types
t1 Types
t2
(FValue Values Funcons
_, FValue Values Funcons
_) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) String
"sort-intersection not applied to two sorts"
(FValue Values Funcons
v1, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s2 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 (Values Funcons -> Funcons
FValue Values Funcons
v2)
ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) String
"sort-intersection multiadic argument (2)"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1) MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"sort-intersection multiadic argument (2)"
(Funcons, Funcons)
_ -> do Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortInter (Values Funcons -> Funcons
FValue Values Funcons
v1) Funcons
s2
ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) String
"sort-intersection multiadic argument (1)"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie ((Funcons -> Funcons -> Funcons) -> Funcons -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortInter Funcons
s2) MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"sort-intersection multiadic argument (1)"
rewriteFuncons' (FSortComplement Funcons
s1) = case Funcons
s1 of
FValue (ComputationType (Type Types
t1)) -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values Funcons
typeVal (Types -> Values Funcons) -> Types -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Types -> Types
forall t. Types t -> Types t
Complement Types
t1
FValue Values Funcons
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons
FSortComplement Funcons
s1) String
"sort-complement not applied to a sort"
Funcons
_ -> do Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
FSortComplement (Values Funcons -> Funcons
FValue Values Funcons
v)
ValTerm [Values Funcons]
vs -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons
FSortComplement Funcons
s1) String
"sort-complement multiadic argument"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie Funcons -> Funcons
FSortComplement MSOS StepRes
mf
where ie :: IE
ie = String -> IE
SortErr String
"sort-complement multiadic argument"
rewriteFuncons' (FName Text
nm) =
do EvalFunction
mystepf <- Text -> Rewrite EvalFunction
lookupFuncon Text
nm
case EvalFunction
mystepf of
NullaryFuncon Rewrite Rewritten
mystep -> Rewrite Rewritten
mystep
StrictFuncon ValueOp
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons' (Text -> [Funcons] -> Funcons
FApp Text
nm [])
ValueOp ValueOp
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons' (Text -> [Funcons] -> Funcons
FApp Text
nm [])
EvalFunction
_ -> String -> Rewrite Rewritten
forall a. HasCallStack => String -> a
error (String
"funcon " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
unpack Text
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not applied to any arguments")
rewriteFuncons' (FApp Text
nm [Funcons]
arg) =
do EvalFunction
mystepf <- Text -> Rewrite EvalFunction
lookupFuncon Text
nm
case EvalFunction
mystepf of
NullaryFuncon Rewrite Rewritten
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
exception (Text -> [Funcons] -> Funcons
FApp Text
nm [Funcons]
arg) (String
"nullary funcon " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
unpack Text
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" applied to arguments: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Funcons] -> String
showFunconsSeq [Funcons]
arg))
ValueOp ValueOp
mystep -> [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
arg ValueOp
mystep (Text -> [Funcons] -> Funcons
applyFuncon Text
nm)
StrictFuncon ValueOp
mystep -> [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
arg ValueOp
mystep (Text -> [Funcons] -> Funcons
applyFuncon Text
nm)
NonStrictFuncon [Funcons] -> Rewrite Rewritten
mystep -> [Funcons] -> Rewrite Rewritten
mystep [Funcons]
arg
PartiallyStrictFuncon [Strictness]
strns Strictness
strn [Funcons] -> Rewrite Rewritten
mystep ->
[Strictness]
-> [Funcons]
-> ([Funcons] -> Rewrite Rewritten)
-> ([Funcons] -> Funcons)
-> Rewrite Rewritten
evalSequence ([Strictness]
strns [Strictness] -> [Strictness] -> [Strictness]
forall a. [a] -> [a] -> [a]
++ Strictness -> [Strictness]
forall a. a -> [a]
repeat Strictness
strn) [Funcons]
arg [Funcons] -> Rewrite Rewritten
mystep (Text -> [Funcons] -> Funcons
applyFuncon Text
nm)
rewriteStrictSequence :: [Funcons] -> Rewrite [Values]
rewriteStrictSequence :: [Funcons] -> Rewrite [Values Funcons]
rewriteStrictSequence [Funcons]
fs = case [Funcons]
rest of
[] -> [Values Funcons] -> Rewrite [Values Funcons]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Funcons -> Values Funcons) -> [Funcons] -> [Values Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values Funcons
downcastValue [Funcons]
vs)
(Funcons
x:[Funcons]
xs) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
x Rewrite Rewritten
-> (Rewritten -> Rewrite [Values Funcons])
-> Rewrite [Values Funcons]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values Funcons]
vs' -> [Funcons] -> Rewrite [Values Funcons]
rewriteStrictSequence ([Funcons]
vs[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++(Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
vs'[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++[Funcons]
xs)
CompTerm Funcons
f0 MSOS StepRes
mf -> String -> Rewrite [Values Funcons]
forall a. String -> Rewrite a
internal (String
"step on sequence of computations: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Funcons] -> String
forall a. Show a => a -> String
show [Funcons]
fs)
where ([Funcons]
vs, [Funcons]
rest) = (Funcons -> Bool) -> [Funcons] -> ([Funcons], [Funcons])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not (Bool -> Bool) -> (Funcons -> Bool) -> Funcons -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Funcons -> Bool
hasStep) [Funcons]
fs
evalStrictSequence :: [Funcons] -> ([Values] -> Rewrite Rewritten) -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence :: [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
args ValueOp
cont [Funcons] -> Funcons
cons =
[Strictness]
-> [Funcons]
-> ([Funcons] -> Rewrite Rewritten)
-> ([Funcons] -> Funcons)
-> Rewrite Rewritten
evalSequence (Int -> Strictness -> [Strictness]
forall a. Int -> a -> [a]
replicate ([Funcons] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Funcons]
args) Strictness
Strict) [Funcons]
args
(ValueOp
cont ValueOp
-> ([Funcons] -> [Values Funcons])
-> [Funcons]
-> Rewrite Rewritten
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Funcons -> Values Funcons) -> [Funcons] -> [Values Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values Funcons
downcastValue) [Funcons] -> Funcons
cons
evalSequence :: [Strictness] -> [Funcons] ->
([Funcons] -> Rewrite Rewritten) -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalSequence :: [Strictness]
-> [Funcons]
-> ([Funcons] -> Rewrite Rewritten)
-> ([Funcons] -> Funcons)
-> Rewrite Rewritten
evalSequence [Strictness]
strns [Funcons]
args [Funcons] -> Rewrite Rewritten
cont [Funcons] -> Funcons
cons =
([Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten)
-> ([Funcons], [(Strictness, Funcons)]) -> Rewrite Rewritten
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten
evalSeqAux (([Funcons], [(Strictness, Funcons)]) -> Rewrite Rewritten)
-> ([Funcons], [(Strictness, Funcons)]) -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ((Strictness, Funcons) -> Funcons)
-> [(Strictness, Funcons)] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map (Strictness, Funcons) -> Funcons
forall a b. (a, b) -> b
snd ([(Strictness, Funcons)] -> [Funcons])
-> ([(Strictness, Funcons)] -> [(Strictness, Funcons)])
-> ([(Strictness, Funcons)], [(Strictness, Funcons)])
-> ([Funcons], [(Strictness, Funcons)])
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [(Strictness, Funcons)] -> [(Strictness, Funcons)]
forall a. a -> a
id (([(Strictness, Funcons)], [(Strictness, Funcons)])
-> ([Funcons], [(Strictness, Funcons)]))
-> ([(Strictness, Funcons)], [(Strictness, Funcons)])
-> ([Funcons], [(Strictness, Funcons)])
forall a b. (a -> b) -> a -> b
$ ((Strictness, Funcons) -> Bool)
-> [(Strictness, Funcons)]
-> ([(Strictness, Funcons)], [(Strictness, Funcons)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Strictness, Funcons) -> Bool
isDone ([Strictness] -> [Funcons] -> [(Strictness, Funcons)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Strictness]
strns [Funcons]
args)
where unmatched :: [Funcons]
unmatched = Int -> [Funcons] -> [Funcons]
forall a. Int -> [a] -> [a]
drop ([Strictness] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Strictness]
strns) [Funcons]
args
evalSeqAux :: [Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten
evalSeqAux :: [Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten
evalSeqAux [Funcons]
vs [] = [Funcons] -> Rewrite Rewritten
cont [Funcons]
vs
evalSeqAux [Funcons]
vs ((Strictness
_,Funcons
f):[(Strictness, Funcons)]
fs) = ValueOp
-> (MSOS StepRes -> MSOS StepRes) -> Funcons -> Rewrite Rewritten
premiseEval ValueOp
valueCont MSOS StepRes -> MSOS StepRes
funconCont Funcons
f
where valueCont :: ValueOp
valueCont [Values Funcons]
vs' = do
Rewrite ()
count_rewrite
[Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten
evalSeqAux ([Funcons]
vs[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++((Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
vs' [Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++ ((Strictness, Funcons) -> Funcons)
-> [(Strictness, Funcons)] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map (Strictness, Funcons) -> Funcons
forall a b. (a, b) -> b
snd [(Strictness, Funcons)]
othervs)) [(Strictness, Funcons)]
otherfs
where ([(Strictness, Funcons)]
othervs, [(Strictness, Funcons)]
otherfs) = ((Strictness, Funcons) -> Bool)
-> [(Strictness, Funcons)]
-> ([(Strictness, Funcons)], [(Strictness, Funcons)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Strictness, Funcons) -> Bool
isDone [(Strictness, Funcons)]
fs
funconCont :: MSOS StepRes -> MSOS StepRes
funconCont MSOS StepRes
stepf = MSOS StepRes
stepf MSOS StepRes -> (StepRes -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left Funcons
f' -> Funcons -> MSOS StepRes
stepTo ([Funcons] -> Funcons
cons ([Funcons]
vs[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++[Funcons
f'][Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++((Strictness, Funcons) -> Funcons)
-> [(Strictness, Funcons)] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map (Strictness, Funcons) -> Funcons
forall a b. (a, b) -> b
snd [(Strictness, Funcons)]
fs))
Right [Values Funcons]
vs' -> Funcons -> MSOS StepRes
stepTo ([Funcons] -> Funcons
cons ([Funcons]
vs[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++((Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
vs')[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++((Strictness, Funcons) -> Funcons)
-> [(Strictness, Funcons)] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map (Strictness, Funcons) -> Funcons
forall a b. (a, b) -> b
snd [(Strictness, Funcons)]
fs))
isDone :: (Strictness, Funcons) -> Bool
isDone (Strictness
Strict, FValue Values Funcons
_) = Bool
True
isDone (Strictness
NonStrict, Funcons
_) = Bool
True
isDone (Strictness, Funcons)
_ = Bool
False
compstep :: MSOS StepRes -> Rewrite Rewritten
compstep :: MSOS StepRes -> Rewrite Rewritten
compstep MSOS StepRes
mf = (RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten)
-> (RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->
let f0 :: Funcons
f0 = RewriteReader -> Funcons
local_fct RewriteReader
ctxt
in (Rewritten -> Either IException Rewritten
forall a b. b -> Either a b
Right (Funcons -> MSOS StepRes -> Rewritten
CompTerm Funcons
f0 MSOS StepRes
mf), RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty)
stepTrans :: RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans :: RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans RunOptions
opts Int
i StepRes
res = case StepRes
res of
Right [Values Funcons]
vs -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return StepRes
res
Left Funcons
f | Bool -> (Int -> Bool) -> Maybe Int -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i)) (RunOptions -> Maybe Int
max_restarts RunOptions
opts) -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return StepRes
res
| Bool
otherwise -> Bool
-> MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_abruptly_terminates (RunOptions -> Bool
do_abrupt_terminate RunOptions
opts)
(Funcons -> MSOS StepRes
stepAndOutput Funcons
f) StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return StepRes -> MSOS StepRes
continue
where continue :: StepRes -> MSOS StepRes
continue StepRes
res = MSOS ()
count_restart MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans RunOptions
opts (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) StepRes
res
stepAndOutput :: Funcons -> MSOS StepRes
stepAndOutput :: Funcons -> MSOS StepRes
stepAndOutput Funcons
f = (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes)
-> (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
let MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper' = Funcons -> MSOS StepRes
evalFuncons Funcons
f
stepper :: MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper MSOSReader m
ctxt MSOSState m
mut = MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper' (MSOSReader m -> MSOSReader m
forall (m :: * -> *). MSOSReader m -> MSOSReader m
setGlobal MSOSReader m
ctxt) MSOSState m
mut
setGlobal :: MSOSReader m -> MSOSReader m
setGlobal MSOSReader m
ctxt = MSOSReader m
ctxt
{ ereader :: RewriteReader
ereader = (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) {global_fct :: Funcons
global_fct = Funcons
f }}
in do (Either IException StepRes
eres,MSOSState m
mut',MSOSWriter
wr') <- MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper MSOSReader m
ctxt MSOSState m
mut
((Text, Values Funcons) -> m ())
-> [(Text, Values Funcons)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Text -> Values Funcons -> m ()) -> (Text, Values Funcons) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Values Funcons -> m ()
forall (m :: * -> *).
Interactive m =>
Text -> Values Funcons -> m ()
fprint)
[ (Text
entity,Values Funcons
val)
| (Text
entity, [Values Funcons]
vals) <- Inherited -> [(Text, [Values Funcons])]
forall k a. Map k a -> [(k, a)]
M.assocs (MSOSWriter -> Inherited
out_entities MSOSWriter
wr')
, Values Funcons
val <- [Values Funcons]
vals ]
(Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
eres, MSOSState m
mut', MSOSWriter
wr')
toStepRes :: Funcons -> StepRes
toStepRes :: Funcons -> StepRes
toStepRes (FValue Values Funcons
v) = [Values Funcons] -> StepRes
forall a b. b -> Either a b
Right [Values Funcons
v]
toStepRes Funcons
f = Funcons -> StepRes
forall a b. a -> Either a b
Left Funcons
f
flattenApplyWithExc :: IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc :: IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie Funcons -> Funcons
app MSOS StepRes
m = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS StepRes -> Rewrite Rewritten)
-> MSOS StepRes -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ MSOS StepRes
m MSOS StepRes -> (StepRes -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left Funcons
f -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return (StepRes -> MSOS StepRes) -> StepRes -> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ Funcons -> StepRes
forall a b. a -> Either a b
Left (Funcons -> StepRes) -> Funcons -> StepRes
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
app Funcons
f
Right [Values Funcons
v] -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return (StepRes -> MSOS StepRes) -> StepRes -> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ Funcons -> StepRes
forall a b. a -> Either a b
Left (Funcons -> StepRes) -> Funcons -> StepRes
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
app (Values Funcons -> Funcons
FValue Values Funcons
v)
Right [Values Funcons]
vs -> IE -> MSOS StepRes
forall b. IE -> MSOS b
msos_throw IE
ie