{-# LANGUAGE LambdaCase, OverloadedStrings, Rank2Types, TupleSections   
             , FlexibleInstances #-}

module Funcons.MSOS (
    -- * Making steps
    MSOS(..), Rewrite(..), liftRewrite, rewrite_rethrow, rewrite_throw, eval_catch, msos_throw, 
        EvalFunction(..), Strictness(..), StrictFuncon, PartiallyStrictFuncon, 
            NonStrictFuncon, ValueOp, NullaryFuncon, RewriteState(..),
            StepRes, toStepRes,
        -- ** Entity-types
        Output, readOuts, 
        Mutable, 
        Inherited, giveINH, 
        Control, singleCTRL, giveCTRL, 
        Input,
            -- ** IMSOS helpers
            applyFuncon, rewritten, rewriteTo, rewriteSeqTo, stepTo, stepSeqTo,rewrittens,
                compstep,
                norule, exception, sortErr, partialOp, internal, buildStep, sidecond,
            -- *** Congruence rules
            premiseStepApp, premiseStep, premiseEval,
        -- ** Pattern Matching
        SeqSortOp(..),
                        rewriteRules, stepRules, evalRules, MSOSState(..), emptyMSOSState, emptyRewriteState, MSOSReader(..),RewriteReader(..),showIException, MSOSWriter(..), RewriteWriterr(..),
    -- * Evaluation funcons TODO internal usage only (by Funcons.Tools)
        Rewritten(..), rewriteFuncons, rewriteFunconsWcount, evalFuncons
          , stepTrans, stepAndOutput, rewritesToValue, rewritesToValues, rewritesToType
          , emptyDCTRL, emptyINH, Interactive(..), SimIO(..)
          , rewriteToValErr, count_delegation, optRefocus
          , evalStrictSequence, rewriteStrictSequence, evalSequence
          , maybe_randomSelect, maybe_randomRemove,
    -- * Values
        showTypes, showSorts, showValues, showValuesSeq, showFuncons, showFunconsSeq,traceLib,
    -- * Funcon libraries
    FunconLibrary, libUnions, libOverrides, libEmpty, libUnion, libOverride, Funcons.MSOS.libFromList,
    evalctxt2exception, ctxt2exception, fromSeqValOp, fromNullaryValOp, fromValOp,
    -- * Counters
    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.Monad (liftM, ap)
import Data.Function (on)
import Data.Maybe (isJust, isNothing, fromJust)
import Data.List (foldl', intercalate, partition, sortBy)
import Data.Text (unpack)

import qualified Data.Map as M

import System.Random
import System.IO.Unsafe

--trace p b = unsafePerformIO (putStrLn p >> return b) 
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 
  ([Char] -> IO ()
putStrLn ([[Char]] -> [Char]
unlines ((Name -> [Char]) -> [Name] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Name -> [Char]
unpack (FunconLibrary -> [Name]
forall k a. Map k a -> [k]
M.keys FunconLibrary
lib))) IO () -> IO FunconLibrary -> IO FunconLibrary
forall a b. IO a -> IO b -> IO b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FunconLibrary -> IO FunconLibrary
forall a. a -> IO a
forall (m :: * -> *) a. Monad m => a -> m a
return FunconLibrary
lib)


---------------------------------------------------------------------
-- | A funcon library maps funcon names to their evaluation functions.
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]
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 -> OpExpr Funcons) -> [Values] -> [OpExpr Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> OpExpr Funcons
forall t. Values t -> OpExpr t
ValExpr [Values]
vs))) 
        where f :: Funcons
f = [Funcons] -> Funcons
cons ((Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
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 -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report Funcons
f Bool
seqRes EvalResult Funcons
res = case EvalResult Funcons
res of
  Error OpExpr Funcons
_ Result Funcons
dres                -> Result Funcons -> Rewrite Rewritten
reportResult Result Funcons
dres
  Success (FValue (ADTVal Name
"null" [Funcons]
_)) -> ValueOp
rewrittens []
  Success (FValue Values
v)          -> Values -> Rewrite Rewritten
rewritten' Values
v
  Success Funcons
t                   -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
t
  EvalResults [EvalResult Funcons]
ress            -> SourceOfND -> [EvalResult Funcons] -> Rewrite (EvalResult Funcons)
forall {b}. SourceOfND -> [b] -> Rewrite b
maybe_randomSelect SourceOfND
NDValueOperations [EvalResult Funcons]
ress Rewrite (EvalResult Funcons)
-> (EvalResult Funcons -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 
                                  Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report Funcons
f Bool
seqRes 
  where rewritten' :: Values -> Rewrite Rewritten
rewritten' Values
v | Bool
seqRes, ValSeq [Funcons]
fs <- Values
v, 
                        let mvs :: [Maybe Values]
mvs = (Funcons -> Maybe Values) -> [Funcons] -> [Maybe Values]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Maybe Values
forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
fs, (Maybe Values -> Bool) -> [Maybe Values] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe Values -> Bool
forall a. Maybe a -> Bool
isJust [Maybe Values]
mvs
                        = ValueOp
rewrittens ((Maybe Values -> Values) -> [Maybe Values] -> [Values]
forall a b. (a -> b) -> [a] -> [b]
map Maybe Values -> Values
forall a. HasCallStack => Maybe a -> a
fromJust [Maybe Values]
mvs)
                     | Bool
otherwise = Values -> Rewrite Rewritten
rewritten Values
v
        reportResult :: Result Funcons -> Rewrite Rewritten
reportResult Result Funcons
dres = case Result Funcons
dres of 
          (VAL.SortErr [Char]
str)   -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
str
          (DomErr [Char]
str)        -> ValueOp
rewrittens [] 
          (ArityErr [Char]
str)      -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
str
          (ProjErr [Char]
str)       -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
str
          (Normal (FValue Values
v)) -> Values -> Rewrite Rewritten
rewritten' Values
v
          (Normal Funcons
t)          -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
t
          (Nondeterministic [Result Funcons]
ress) -> case [Result Funcons]
ress of 
            []    -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
"nondeterminism: empty"
            [Result Funcons]
_     -> [Result Funcons] -> Rewrite (Result Funcons)
forall {b}. [b] -> Rewrite b
randomSelect [Result Funcons]
ress Rewrite (Result Funcons)
-> (Result Funcons -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Result Funcons -> Rewrite Rewritten
reportResult

-- |
-- Evaluation functions capture the operational behaviour of a funcon.
-- Evaluation functions come in multiple flavours, each with a different
-- treatment of the arguments of the funcon.
-- Before the application of an evaluation funcon, any argument may be
-- evaluated, depending on the 'Strictness' of the argument.
data EvalFunction   = 
                    -- | Funcons for which arguments are /not/ evaluated.
                      NonStrictFuncon NonStrictFuncon 
                    -- | Strict funcons whose arguments are evaluated.
                    | StrictFuncon StrictFuncon
                    -- | Funcons for which /some/ arguments are evaluated.
                    | PartiallyStrictFuncon [Strictness] Strictness NonStrictFuncon
                    -- | Synonym for 'StrictFuncon', for value operations.
                    | ValueOp ValueOp
                    -- | Funcons without any arguments.
                    | NullaryFuncon NullaryFuncon
-- | Type synonym for the evaluation function of strict funcons.
-- The evaluation function of a 'StrictFuncon' receives fully evaluated arguments.
type StrictFuncon           = [Values] -> Rewrite Rewritten
-- | Type synonym for the evaluation function of fully non-strict funcons.
type NonStrictFuncon        = [Funcons] -> Rewrite Rewritten
-- | Type synonym for the evaluation function of non-strict funcons.
type PartiallyStrictFuncon  = NonStrictFuncon 
-- | Type synonym for value operations.
type ValueOp                = StrictFuncon
-- | Type synonym for the evaluation functions of nullary funcons.
type NullaryFuncon          = Rewrite Rewritten
-- | Denotes whether an argument of a funcon should be evaluated or not.
data Strictness             = Strict | NonStrict

-- | After a term is fully rewritten it is either a value or a 
-- term that requires a computational step to proceed.
-- This types forms the interface between syntactic rewrites and 
-- computational steps.
data Rewritten = 
    -- | Fully rewritten to a value.
    ValTerm [Values]
    -- | Fully rewritten to a term and the step required to continue evaluation.
    | CompTerm Funcons (MSOS StepRes)

-- | A single step on a funcon term produces either a funcon term 
-- or a (possibly empty or unary) sequence of values
type StepRes = Either Funcons [Values]

instance Show Rewritten where
    show :: Rewritten -> [Char]
show (ValTerm [Values]
vs) = [Values] -> [Char]
showValuesSeq [Values]
vs
    show (CompTerm Funcons
_ MSOS StepRes
_) = [Char]
"<step>"

-- | Creates an empty 'FunconLibrary'.
libEmpty :: FunconLibrary
libEmpty :: FunconLibrary
libEmpty = FunconLibrary
forall k a. Map k a
M.empty 

-- | Unites two 'FunconLibrary's.
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion = (Name -> 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 Name -> EvalFunction -> EvalFunction -> EvalFunction
forall {p} {p} {a}. Name -> p -> p -> a
op
 where op :: Name -> p -> p -> a
op Name
k p
x p
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"duplicate funcon name: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
k)

-- | Right-based union of 'FunconLibrary's
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 

-- | Unites a list of 'FunconLibrary's.
libUnions :: [FunconLibrary] -> FunconLibrary
libUnions :: [FunconLibrary] -> FunconLibrary
libUnions = (FunconLibrary -> FunconLibrary -> FunconLibrary)
-> FunconLibrary -> [FunconLibrary] -> FunconLibrary
forall b a. (b -> a -> b) -> b -> [a] -> b
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
_ = [Char] -> a
forall a. HasCallStack => [Char] -> a
error ([Char]
"duplicate funcon name")

-- | Right-based union of list of 'FunconLibrary's
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

-- | Creates a 'FunconLibrary' from a list.
libFromList :: [(Name, EvalFunction)] -> FunconLibrary
libFromList :: [(Name, EvalFunction)] -> FunconLibrary
libFromList = [(Name, EvalFunction)] -> FunconLibrary
forall k a. Ord k => [(k, a)] -> Map k a
M.fromList

lookupFuncon :: Name -> Rewrite EvalFunction
lookupFuncon :: Name -> Rewrite EvalFunction
lookupFuncon Name
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 Name -> FunconLibrary -> Maybe EvalFunction
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
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 Name -> Map Name Funcons -> Maybe Funcons
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
key (RunOptions -> Map Name 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 ([Char] -> IE
Internal ([Char]
"unknown funcon: "[Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
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 { RewriteState -> StdGen
random_gen :: StdGen }
emptyRewriteState :: RewriteState
emptyRewriteState = StdGen -> RewriteState
RewriteState (Int -> StdGen
mkStdGen Int
0)
data RewriteWriterr = RewriteWriterr { RewriteWriterr -> Counters
counters :: Counters }

-- | Monadic type for the implicit propagation of meta-information on
-- the evaluation of funcon terms (no semantic entities). 
-- It is separated from 'MSOS' to ensure
-- that side-effects (access or modification of semantic entities) can not
-- occur during syntactic rewrites.
newtype Rewrite a= Rewrite {forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite :: (RewriteReader -> RewriteState -> 
                    (Either IException a, RewriteState, RewriteWriterr))}

instance Applicative Rewrite where
  pure :: forall a. a -> Rewrite a
pure 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))
  <*> :: forall a b. 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 :: forall a b. (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
  (Rewrite RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f) >>= :: forall a b. 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 Counters
cs1) <> :: RewriteWriterr -> RewriteWriterr -> RewriteWriterr
<> (RewriteWriterr Counters
cs2) = Counters -> RewriteWriterr
RewriteWriterr (Counters
cs1 Counters -> Counters -> Counters
forall a. Semigroup a => a -> a -> a
<> Counters
cs2)

instance Monoid RewriteWriterr where
    mempty :: RewriteWriterr
mempty = Counters -> RewriteWriterr
RewriteWriterr Counters
forall a. Monoid a => a
mempty

liftRewrite :: Rewrite a -> MSOS a
liftRewrite :: forall a. 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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException a
e_a, MSOSState m
mut {estate = est}, MSOSWriter
forall a. Monoid a => a
mempty { ewriter = ewr })

eval_catch :: Rewrite a -> Rewrite (Either IException a)
eval_catch :: forall a. 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 :: forall a. (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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right a
a -> a -> Rewrite a
forall 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 :: forall a. 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 :: forall a. 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 :: forall (m :: * -> *). 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 -> -- resets state 
                                 [Char]
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall {p} {p}. p -> p -> p
trace (IException -> [Char]
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{ forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader :: RewriteReader 
                              , forall (m :: * -> *). MSOSReader m -> Inherited
inh_entities :: Inherited
                              , forall (m :: * -> *). MSOSReader m -> DownControl
dctrl_entities :: DownControl
                              , forall (m :: * -> *). MSOSReader m -> Name -> 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 { forall (m :: * -> *). MSOSState m -> Input m
inp_es :: Input m, forall (m :: * -> *). MSOSState m -> Inherited
mut_entities :: Mutable
                             , forall (m :: * -> *). MSOSState m -> RewriteState
estate :: RewriteState }
emptyMSOSState :: Int -> MSOSState m
emptyMSOSState :: forall (m :: * -> *). Int -> MSOSState m
emptyMSOSState Int
seed = 
  Input m -> Inherited -> RewriteState -> MSOSState m
forall (m :: * -> *).
Input m -> Inherited -> RewriteState -> MSOSState m
MSOSState Input m
forall k a. Map k a
M.empty Inherited
forall k a. Map k a
M.empty (RewriteState
emptyRewriteState { random_gen = mkStdGen seed })

-- | Monadic type for the propagation of semantic entities and meta-information
-- on the evaluation of funcons. The meta-information includes a library 
-- of funcons (see 'FunconLibrary'), a typing environment (see 'TypeRelation'), 
-- runtime options, etc.
--
-- The semantic entities are divided into five classes:
--
-- * inherited entities, propagated similar to values of a reader monad.
--
-- * mutable entities, propagated similar to values of a state monad.
--
-- * output entities, propagation similar to values of a write monad.
--
-- * control entities, similar to output entities except only a single control /signal/
--      can be emitted at once (signals do not form a monoid).
--
-- * input entities, propagated like values of a state monad, but access like
--  value of a reader monad. This package provides simulated input/outout 
--  and real interaction via the 'IO' monad. See "Funcons.Tools".
--
-- For each entity class a map is propagated, mapping entity names to values.
-- This enables modular access to the entities.
newtype MSOS a = MSOS { forall a.
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 :: forall a. a -> MSOS a
pure 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 a. a -> m a
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))
  <*> :: forall a b. 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 :: forall a b. (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
  (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f) >>= :: forall a b. 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 a. a -> m a
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 a. a -> m a
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 :: forall a. [Char] -> MSOS a
fail = Rewrite a -> MSOS a
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite a -> MSOS a) -> ([Char] -> Rewrite a) -> [Char] -> MSOS a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Char] -> Rewrite a
forall a. [Char] -> Rewrite a
internal 

instance Semigroup MSOSWriter where
  (MSOSWriter DownControl
x1 Inherited
x2 RewriteWriterr
x3) <> :: MSOSWriter -> MSOSWriter -> MSOSWriter
<> (MSOSWriter DownControl
y1 Inherited
y2 RewriteWriterr
y3) = 
      DownControl -> Inherited -> RewriteWriterr -> MSOSWriter
MSOSWriter (DownControl
x1 DownControl -> DownControl -> DownControl
forall {a}. Map Name a -> Map Name a -> Map Name 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) 

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

-- | A map storing the values of /mutable/ entities.
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]
ts = 
 Rewrite (MSOS StepRes, [MSOS StepRes])
-> MSOS (MSOS StepRes, [MSOS StepRes])
forall a. Rewrite a -> MSOS a
liftRewrite (SourceOfND
-> [MSOS StepRes] -> Rewrite (MSOS StepRes, [MSOS StepRes])
forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
NDRuleSelection [MSOS StepRes]
ts) MSOS (MSOS StepRes, [MSOS StepRes])
-> ((MSOS StepRes, [MSOS StepRes]) -> MSOS StepRes) -> MSOS StepRes
forall a b. MSOS a -> (a -> MSOS b) -> MSOS b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 
  \(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
-> forall (m :: * -> *).
   Interactive m =>
   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 -> -- resets input & read/write entities
                                  [Char]
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall {p} {p}. p -> p -> p
trace (IException -> [Char]
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
-> forall (m :: * -> *).
   Interactive m =>
   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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_ie_a, MSOSState m
mut', MSOSWriter
wr)

-- | Function 'evalRules' implements a backtracking procedure.
-- It receives two lists of alternatives as arguments, the first
-- containing all rewrite rules of a funcon and the second all step rules.
-- The first successful rule is the only rule fully executed.
-- A rule is /unsuccessful/ if it throws an exception. Some of these
-- exceptions (partial operation, sort error or pattern-match failure)
-- cause the next alternative to be tried. Other exceptions 
-- (different forms of internal errors) will be propagated further.
-- All side-effects of attempting a rule are discarded when a rule turns
-- out not to be applicable.
-- 
-- First all rewrite rules are attempted, therefore avoiding performing
-- a step until it is absolutely necessary. This is a valid strategy
-- as valid (I)MSOS rules can be considered in any order.
--
-- When no rules are successfully executed to completetion a 
-- 'no rule exception' is thrown.
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 Rewritten]
rules [MSOS StepRes]
msoss = 
 SourceOfND
-> [Rewrite Rewritten]
-> Rewrite (Rewrite Rewritten, [Rewrite Rewritten])
forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
NDRuleSelection [Rewrite Rewritten]
rules Rewrite (Rewrite Rewritten, [Rewrite Rewritten])
-> ((Rewrite Rewritten, [Rewrite Rewritten]) -> Rewrite Rewritten)
-> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \((Rewrite RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
rw_rules),[Rewrite Rewritten]
rest) -> 
  (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  -> --resets counters and state 
                                   [Char]
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall {p} {p}. p -> p -> p
trace (IException -> [Char]
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 :: forall b. 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 :: Rewrite RunOptions 
giveOpts :: Rewrite RunOptions
giveOpts = (RewriteReader
 -> RewriteState
 -> (Either IException RunOptions, RewriteState, RewriteWriterr))
-> Rewrite RunOptions
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
  -> RewriteState
  -> (Either IException RunOptions, RewriteState, RewriteWriterr))
 -> Rewrite RunOptions)
-> (RewriteReader
    -> RewriteState
    -> (Either IException RunOptions, RewriteState, RewriteWriterr))
-> Rewrite RunOptions
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
mut -> (RunOptions -> Either IException RunOptions
forall a b. b -> Either a b
Right (RewriteReader -> RunOptions
run_opts RewriteReader
ctxt), RewriteState
mut, RewriteWriterr
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 a. a -> m a
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 a. a -> m a
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 a. a -> m a
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 :: forall a.
(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 :: forall a. (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 = mod (ereader ctxt) }

maybe_randomRemove :: SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove :: forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
_ [] = [a] -> Rewrite (a, [a])
forall a. [a] -> Rewrite (a, [a])
randomRemove []
maybe_randomRemove SourceOfND
src xs :: [a]
xs@(a
x:[a]
xs') = do
  RunOptions
opts <- Rewrite RunOptions
giveOpts
  if SourceOfND
src SourceOfND -> [SourceOfND] -> Bool
forall a. Eq a => a -> [a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` RunOptions -> [SourceOfND]
get_nd_sources RunOptions
opts then [a] -> Rewrite (a, [a])
forall a. [a] -> Rewrite (a, [a])
randomRemove [a]
xs
                                    else (a, [a]) -> Rewrite (a, [a])
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, [a]
xs')

-- | Uses the random number generator of Rewrite to randomly select
-- an element of a given list. The element is returned, together
-- with the list from which the element has been removed
-- Raises an internal exception if given an empty list
randomRemove :: [a] -> Rewrite (a, [a])
randomRemove :: forall a. [a] -> Rewrite (a, [a])
randomRemove [] = [Char] -> Rewrite (a, [a])
forall a. [Char] -> Rewrite a
internal [Char]
"randomRemove: empty list"
randomRemove [a
x]= (a, [a]) -> Rewrite (a, [a])
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, [])
randomRemove [a]
xs = (RewriteReader
 -> RewriteState
 -> (Either IException (a, [a]), RewriteState, RewriteWriterr))
-> Rewrite (a, [a])
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
  -> RewriteState
  -> (Either IException (a, [a]), RewriteState, RewriteWriterr))
 -> Rewrite (a, [a]))
-> (RewriteReader
    -> RewriteState
    -> (Either IException (a, [a]), RewriteState, RewriteWriterr))
-> Rewrite (a, [a])
forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
mut -> 
  let gen :: StdGen
gen       = RewriteState -> StdGen
random_gen RewriteState
mut 
      (Int
i, StdGen
gen') = StdGen -> (Int, StdGen)
forall g. RandomGen g => g -> (Int, g)
next StdGen
gen
      index :: Int
index     = Int
i Int -> Int -> Int
forall a. Integral a => a -> a -> a
`mod` ([a] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs)
      elem :: a
elem      = [a]
xs [a] -> Int -> a
forall a. HasCallStack => [a] -> Int -> a
!! Int
index 
      rest :: [a]
rest      = Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
take Int
index [a]
xs [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ Int -> [a] -> [a]
forall a. Int -> [a] -> [a]
drop (Int
index Int -> Int -> Int
forall a. Num a => a -> a -> a
+ Int
1) [a]
xs 
  in ((a, [a]) -> Either IException (a, [a])
forall a b. b -> Either a b
Right (a
elem, [a]
rest), RewriteState
mut {random_gen = gen'}, RewriteWriterr
forall a. Monoid a => a
mempty )

maybe_randomSelect :: SourceOfND -> [b] -> Rewrite b
maybe_randomSelect SourceOfND
src [b]
xs = (b, [b]) -> b
forall a b. (a, b) -> a
fst ((b, [b]) -> b) -> Rewrite (b, [b]) -> Rewrite b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> SourceOfND -> [b] -> Rewrite (b, [b])
forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
src [b]
xs
randomSelect :: [b] -> Rewrite b
randomSelect [b]
xs = (b, [b]) -> b
forall a b. (a, b) -> a
fst ((b, [b]) -> b) -> Rewrite (b, [b]) -> Rewrite b
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [b] -> Rewrite (b, [b])
forall a. [a] -> Rewrite (a, [a])
randomRemove [b]
xs

{-
randomSelect :: [a] -> Rewrite a
randomSelect xs = Rewrite $ \_ mut -> 
  let gen       = random_gen mut 
      (_, top)  = genRange gen
      unit      = fromIntegral top / fromIntegral (length xs)
      (i, gen') = next gen
      index     = round (fromIntegral i / unit)
  in (Right (xs !! index), mut {random_gen = gen'}, mempty )
-}

-----------------
-- | a map storing the values of /inherited/ entities.
type Inherited       = M.Map Name [Values]

emptyINH :: Inherited
emptyINH :: Inherited
emptyINH = Inherited
forall k a. Map k a
M.empty 

      
----------
-- | a map storing the values of /control/ entities.
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 :: Name -> Values -> DownControl
singleCTRL Name
k = Name -> Maybe Values -> DownControl
forall k a. k -> a -> Map k a
M.singleton Name
k (Maybe Values -> DownControl)
-> (Values -> Maybe Values) -> Values -> DownControl
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Values -> Maybe Values
forall a. a -> Maybe a
Just

unionCTRL :: Map Name a -> Map Name a -> Map Name a
unionCTRL = (Name -> a -> a -> a) -> Map Name a -> Map Name a -> Map Name a
forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWithKey ([Char] -> a -> a -> a
forall a. HasCallStack => [Char] -> a
error ([Char] -> a -> a -> a) -> (Name -> [Char]) -> Name -> a -> a -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
err)
 where err :: Name -> [Char]
err Name
key = [Char]
"Two " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
key [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" signals converging!"

-----------
-- | a map storing the values of /output/ entities.
type Output      = M.Map Name [Values]

unionOUT :: Output -> Output -> Output
unionOUT :: Inherited -> Inherited -> Inherited
unionOUT = ([Values] -> [Values] -> [Values])
-> Inherited -> Inherited -> Inherited
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith [Values] -> [Values] -> [Values]
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 :: forall a. 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 a. a -> m a
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 a. a -> m a
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 = mempty}))
-----------
-- | A map storing the values of /input/ entities.
type Input m = M.Map Name ([[Values]], Maybe (m Funcons))

-----------
-- steps, rewrites, restarts, refocus, delegations, backtracking (outer/inner)
data Counters = Counters !Int !Int !Int !Int !Int !Int !Int !Int 

instance Semigroup Counters where
  (Counters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8) <> :: Counters -> Counters -> Counters
<> (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)

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

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 = mempty {counters = Counters x1 x2 x3 x4 x5 x6 x7 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 a. a -> m a
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 = mempty { 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 = 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 a. a -> m a
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 a. a -> m a
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 a. a -> m a
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 a. a -> m a
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 0 1 0 0 0 0 0 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 0 0 1 0 0 0 0 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 0 0 0 0 0 0 1 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 0 0 0 0 0 0 0 1 })

ppCounters :: Counters -> [Char]
ppCounters Counters
cs =
 [Char]
"number of (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
counterKeys [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
"): (" [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Counters -> [Char]
displayCounters Counters
cs [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
")"

counterKeys :: String
counterKeys :: [Char]
counterKeys = [Char]
"restarts,rewrites,(attempts),steps,refocus,premises,backtracking(outer),backtracking(inner)"
displayCounters :: Counters -> [Char]
displayCounters (Counters Int
steps Int
rewrites Int
rattempts Int
restarts Int
refocus Int
delegations Int
bout Int
bin) = 
  [Char] -> [[Char]] -> [Char]
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," ([[Char]] -> [Char]) -> [[Char]] -> [Char]
forall a b. (a -> b) -> a -> b
$ 
    (Int -> [Char]) -> [Int] -> [[Char]]
forall a b. (a -> b) -> [a] -> [b]
map Int -> [Char]
forall a. Show a => a -> [Char]
show [Int
restarts, Int
rewrites, Int
rattempts, Int
steps, Int
refocus, Int
delegations, Int
bout, Int
bin]

-- | Yields an error signaling that no rule is applicable.
-- The funcon term argument may be used to provide a useful error message.
norule :: Funcons -> Rewrite a
norule :: forall a. Funcons -> Rewrite a
norule Funcons
f = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw ([IException] -> IE
NoRule [])

-- | Yields an error signaling that a sort error was encountered.
-- These errors render a rule /inapplicable/ and a next rule is attempted
-- when a backtracking procedure like 'evalRules' is applied.
-- The funcon term argument may be used to provide a useful error message.
sortErr :: Funcons -> String -> Rewrite a
sortErr :: forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
str = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
SortErr [Char]
str)

-- | Yields an error signaling that a partial operation was applied
-- to a value outside of its domain (e.g. division by zero). 
-- These errors render a rule /inapplicable/ and a next rule is attempted
-- when a backtracking procedure like 'evalRules' is applied.
-- The funcon term argument may be used to provide a useful error message.
partialOp :: Funcons -> String -> Rewrite a
partialOp :: forall a. Funcons -> [Char] -> Rewrite a
partialOp Funcons
f [Char]
str = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PartialOp [Char]
str) 

exception :: Funcons -> String -> Rewrite a
exception :: forall a. Funcons -> [Char] -> Rewrite a
exception Funcons
f [Char]
str = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
Err [Char]
str)

internal :: String -> Rewrite a
internal :: forall a. [Char] -> Rewrite a
internal [Char]
str = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
Internal [Char]
str)

sidecond :: String -> Rewrite a
sidecond :: forall a. [Char] -> Rewrite a
sidecond [Char]
str = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
SideCondFail [Char]
str)

buildStep :: MSOS StepRes -> Rewrite Rewritten 
buildStep :: MSOS StepRes -> Rewrite Rewritten
buildStep = MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter (() -> MSOS ()
forall a. a -> MSOS a
forall (m :: * -> *) a. Monad m => a -> m a
return ()) -- does not count

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 a b. MSOS a -> MSOS b -> MSOS b
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 a b. MSOS a -> (a -> MSOS b) -> MSOS b
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 -- stop refocussing when a signal has been raised
                = MSOS ()
count_refocus MSOS () -> MSOS StepRes -> MSOS StepRes
forall a b. MSOS a -> MSOS b -> MSOS b
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 a. a -> MSOS a
forall (m :: * -> *) a. Monad m => a -> m a
return StepRes -> MSOS StepRes
continue
    where continue :: StepRes -> MSOS StepRes
continue = \case
            Right [Values]
vs  -> StepRes -> MSOS StepRes
forall a. a -> MSOS a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values] -> StepRes
forall a b. b -> Either a b
Right [Values]
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 a b. MSOS a -> (a -> MSOS b) -> MSOS b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v] -> StepRes -> MSOS StepRes
forall a. a -> MSOS a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values] -> StepRes
forall a b. b -> Either a b
Right [Values
v])
                ValTerm [Values]
vs  -> StepRes -> MSOS StepRes
forall a. a -> MSOS a
forall (m :: * -> *) a. Monad m => a -> m a
return (Funcons -> StepRes
forall a b. a -> Either a b
Left Funcons
f) -- undo rewrites and accept last step
                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]
vs) = StepRes -> MSOS StepRes
forall a. a -> MSOS a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values] -> StepRes
forall a b. b -> Either a b
Right [Values]
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 a b. MSOS a -> MSOS b -> MSOS b
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 = f}

-- | Returns a value as a fully rewritten term. 
rewritten :: Values -> Rewrite Rewritten
rewritten :: Values -> Rewrite Rewritten
rewritten = Rewritten -> Rewrite Rewritten
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rewritten -> Rewrite Rewritten)
-> (Values -> Rewritten) -> Values -> Rewrite Rewritten
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Rewritten
ValTerm ([Values] -> Rewritten)
-> (Values -> [Values]) -> Values -> Rewritten
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Values -> [Values] -> [Values]
forall a. a -> [a] -> [a]
:[])

rewrittens :: [Values] -> Rewrite Rewritten
rewrittens :: ValueOp
rewrittens = Rewritten -> Rewrite Rewritten
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return (Rewritten -> Rewrite Rewritten)
-> ([Values] -> Rewritten) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Rewritten
ValTerm

-- | Yield a funcon term as the result of a syntactic rewrite.
-- This function must be used instead of @return@.
-- The given term is fully rewritten.
rewriteTo :: Funcons -> Rewrite Rewritten -- only rewrites, no possible signal
rewriteTo :: Funcons -> Rewrite Rewritten
rewriteTo Funcons
f = Rewrite ()
count_rewrite Rewrite () -> Rewrite Rewritten -> Rewrite Rewritten
forall a b. Rewrite a -> Rewrite b -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f

-- | Yield a sequence of funcon terms as the result of a rewrite.
-- This is only valid when all terms rewrite to a value
rewriteSeqTo :: [Funcons] -> Rewrite Rewritten
rewriteSeqTo :: [Funcons] -> Rewrite Rewritten
rewriteSeqTo [Funcons]
fs = Rewrite ()
count_rewrite Rewrite () -> Rewrite Rewritten -> Rewrite Rewritten
forall a b. Rewrite a -> Rewrite b -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([Values] -> Rewritten
ValTerm ([Values] -> Rewritten) -> Rewrite [Values] -> Rewrite Rewritten
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Funcons] -> Rewrite [Values]
rewriteStrictSequence [Funcons]
fs)

-- | Yield a funcon term as the result of an 'MSOS' computation.
-- This function must be used instead of @return@. 
stepTo :: Funcons -> MSOS StepRes 
stepTo :: Funcons -> MSOS StepRes
stepTo = StepRes -> MSOS StepRes
forall a. a -> MSOS a
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

-- | Yield a sequence of funcon terms as the result of a computation.
-- This is only valid when all terms rewrite to a value
stepSeqTo :: [Funcons] -> MSOS StepRes
stepSeqTo :: [Funcons] -> MSOS StepRes
stepSeqTo [Funcons]
fs = [Values] -> StepRes
forall a b. b -> Either a b
Right ([Values] -> StepRes) -> MSOS [Values] -> MSOS StepRes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rewrite [Values] -> MSOS [Values]
forall a. Rewrite a -> MSOS a
liftRewrite ([Funcons] -> Rewrite [Values]
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 a b. m a -> (a -> m b) -> m b
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 -> Bool) -> DownControl -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe Values -> 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 a. a -> m a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res

-- TODO is input test accurate? 
-- TODO We should also find changes to mutable entities
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 a b. m a -> (a -> m b) -> m b
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 -> Bool) -> DownControl -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe Values -> Bool
forall a. Maybe a -> Bool
isJust (MSOSWriter -> DownControl
ctrl_entities MSOSWriter
wr')
                            Bool -> Bool -> Bool
|| ([Values] -> Bool) -> Inherited -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool) -> ([Values] -> Bool) -> [Values] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (MSOSWriter -> Inherited
out_entities MSOSWriter
wr')
                            Bool -> Bool -> Bool
|| (([[Values]], Maybe (m Funcons)) -> Bool)
-> Map Name ([[Values]], 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]], Maybe (m Funcons)) -> Maybe (m Funcons))
-> ([[Values]], Maybe (m Funcons))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([[Values]], Maybe (m Funcons)) -> Maybe (m Funcons)
forall a b. (a, b) -> b
snd) (MSOSState m -> Map Name ([[Values]], Maybe (m Funcons))
forall (m :: * -> *). MSOSState m -> Input m
inp_es MSOSState m
mut')
--                            || any isJust (dctrl_entities ctxt)
                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 a. a -> m a
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 a. a -> m a
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res

-- | Execute a premise as either a rewrite or a step.
-- Depending on whether only rewrites are necessary to yield a value,
-- or whether a computational step is necessary,
-- a different continuation is applied (first and second argument).
-- Example usage:
--
-- @
-- stepScope :: NonStrictFuncon --strict in first argument
-- stepScope [FValue (Map e1), x] = premiseEval x rule1 step1 
--  where   rule1 v  = rewritten v
--          step1 stepX = do   
--              Map e0  <- getInh "environment"
--              x'      <- withInh "environment" (Map (union e1 e0)) stepX
--              stepTo (scope_ [FValue e1, x'])
-- @
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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ValTerm [Values]
vs      -> ValueOp
vapp [Values]
vs
    CompTerm Funcons
_ MSOS StepRes
step -> MSOS StepRes -> Rewrite Rewritten
buildStepCount (MSOS StepRes -> MSOS StepRes
optRefocus (MSOS StepRes -> MSOS StepRes
fapp MSOS StepRes
step))

-- | Execute a computational step as a /premise/.
-- The result of the step is the returned funcon term. 
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 a b. MSOS a -> (a -> MSOS b) -> MSOS b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ValTerm [Values]
vs      -> IE -> MSOS StepRes
forall b. IE -> MSOS b
msos_throw ([Values] -> IE
StepOnValue [Values]
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 a b. MSOS a -> MSOS b -> MSOS b
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 

----- main `step` function
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 a b. MSOS a -> (a -> MSOS b) -> MSOS b
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 a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ValTerm [v :: Values
v@(ComputationType ComputationTypes Funcons
_)] -> Types -> Rewrite Types
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return (Values -> Types
forall t. Values t -> Types t
downcastValueType Values
v)
    Rewritten
_                               -> Rewrite Types
forall {a}. Rewrite a
rewriteToValErr

rewritesToValue :: Funcons -> Rewrite Values
rewritesToValue :: Funcons -> Rewrite Values
rewritesToValue Funcons
f = do
  Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f Rewrite Rewritten
-> (Rewritten -> Rewrite Values) -> Rewrite Values
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ValTerm [Values
v]   -> Values -> Rewrite Values
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return Values
v
    Rewritten
_             -> Rewrite Values
forall {a}. Rewrite a
rewriteToValErr

rewritesToValues :: Funcons -> Rewrite [Values]
rewritesToValues :: Funcons -> Rewrite [Values]
rewritesToValues Funcons
f = do
  Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f Rewrite Rewritten
-> (Rewritten -> Rewrite [Values]) -> Rewrite [Values]
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ValTerm [Values]
vs  -> [Values] -> Rewrite [Values]
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return [Values]
vs
    Rewritten
_           -> Rewrite [Values]
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
$ 
  [Char] -> IE
SideCondFail [Char]
"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 a b. Rewrite a -> Rewrite b -> Rewrite b
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 = f}) (Funcons -> Rewrite Rewritten
rewriteFuncons' Funcons
f)
 where
    rewriteFuncons' :: Funcons -> Rewrite Rewritten
rewriteFuncons' (FValue Values
v)   = Rewritten -> Rewrite Rewritten
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values] -> Rewritten
ValTerm [Values
v]) 
{-    rewriteFuncons' (FTuple fs)  = 
      let fmops = tupleTypeTemplate fs 
      in if any (isJust . snd) fmops
          -- sequence contains a sequence-operator, thus is a sequence of sorts  
          then rewritten . typeVal =<< evalTupleType fmops
          -- regular sequence 
          else evalStrictSequence fs (rewritten . safe_tuple_val) FTuple
-}
--    rewriteFuncons' (FList fs)   = evalStrictSequence fs (rewritten . List) FList
    rewriteFuncons' (FSet [Funcons]
fs)    = [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
fs (Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> ([Values] -> Values) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Values
setval_) [Funcons] -> Funcons
FSet
    rewriteFuncons' (FMap [Funcons]
fs)    = [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
fs (Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> ([Values] -> Values) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Values
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 -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> ([Values] -> Values) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Values
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]
_       = [Char] -> Funcons
forall a. HasCallStack => [Char] -> a
error [Char]
"invalid binding-notation"
    rewriteFuncons' f :: Funcons
f@(FSortPower Funcons
s1 Funcons
fn) = case (Funcons
s1,Funcons
fn) of 
      (FValue mty :: Values
mty@(ComputationType ComputationTypes Funcons
_), FValue Values
v) 
        | Nat Integer
n <- Values -> Values
forall t. Values t -> Values t
upcastNaturals Values
v -> 
                  ValueOp
rewrittens (Int -> Values -> [Values]
forall a. Int -> a -> [a]
replicate (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) (ComputationTypes Funcons -> Values
forall t. ComputationTypes t -> Values t
ComputationType (Types -> ComputationTypes Funcons
forall t. Types t -> ComputationTypes t
Type (Values -> Types
forall t. Values t -> Types t
downcastValueType Values
mty))))
      (FValue Values
mty, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
fn Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
            ValTerm [Values
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
FValue Values
v)
            ValTerm [Values]
_   -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
"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 = [Char] -> IE
SortErr [Char]
"^_ multiadic argument" 
      (Funcons, Funcons)
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortPower (Values -> Funcons
FValue Values
v) Funcons
fn
            ValTerm [Values]
_   -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
"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 = [Char] -> IE
SortErr [Char]
"_^ multiadic argument"
    rewriteFuncons' f :: Funcons
f@(FSortSeq Funcons
s1 SeqSortOp
op)     = case Funcons
s1 of 
      (FValue (ComputationType (Type Types
ty))) -> Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ComputationTypes Funcons -> Values
forall t. ComputationTypes t -> Values t
ComputationType (ComputationTypes Funcons -> Values)
-> ComputationTypes Funcons -> Values
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 -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> SeqSortOp -> Funcons
FSortSeq Funcons
s1 SeqSortOp
op) [Char]
"sort-sequence operator not on type"
      Funcons
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> SeqSortOp -> Funcons
FSortSeq (Values -> Funcons
FValue Values
v1) SeqSortOp
op
            ValTerm [Values]
vs   -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> SeqSortOp -> Funcons
FSortSeq Funcons
s1 SeqSortOp
op) [Char]
"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 = [Char] -> IE
SortErr [Char]
"sort-sequence operator, multiadic argument"
    rewriteFuncons' (FSortComputes Funcons
f1) = case Funcons
f1 of
        (FValue (ComputationType (Type Types
ty))) -> Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ComputationTypes Funcons -> Values
forall t. ComputationTypes t -> Values t
ComputationType (ComputationTypes Funcons -> Values)
-> ComputationTypes Funcons -> Values
forall a b. (a -> b) -> a -> b
$ Types -> ComputationTypes Funcons
forall t. Types t -> ComputationTypes t
ComputesType Types
ty
        (FValue Values
_) -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons
FSortComputes Funcons
f1) [Char]
"=> not applied to a type"
        Funcons
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
FSortComputes (Values -> Funcons
FValue Values
v1)
                ValTerm [Values]
vs   -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons
FSortComputes Funcons
f1) [Char]
"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 = [Char] -> IE
SortErr [Char]
"=>_ 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 -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ComputationTypes Funcons -> Values
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
_, FValue Values
_) -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) [Char]
"=> not applied to types"
        (FValue (ComputationType (Type Types
ty1)),Funcons
_) 
            -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f2 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
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
FValue Values
v2)
                ValTerm [Values]
_ -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) [Char]
"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 = [Char] -> IE
SortErr [Char]
"_=>_ multiadic operand (2)"
        (Funcons
_,Funcons
_) 
            -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortComputesFrom (Values -> Funcons
FValue Values
v1) Funcons
f2
                ValTerm [Values]
_ -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) [Char]
"_=>_ 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 = [Char] -> IE
SortErr [Char]
"_=>_ 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 -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal (Types -> Values) -> Types -> Values
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
_, FValue Values
_) -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) [Char]
"sort-union not applied to two sorts"
        (FValue Values
v1, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s2 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values
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
FValue Values
v2)
            ValTerm [Values]
_ -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) [Char]
"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 = [Char] -> IE
SortErr [Char]
"sort-union multiadic argument (2)"
        (Funcons, Funcons)
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortUnion (Values -> Funcons
FValue Values
v) Funcons
s2
                ValTerm [Values]
_ -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) [Char]
"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 = [Char] -> IE
SortErr [Char]
"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 -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal (Types -> Values) -> Types -> Values
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
_, FValue Values
_) -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) [Char]
"sort-intersection not applied to two sorts"
        (FValue Values
v1, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s2 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values
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
FValue Values
v2)
            ValTerm [Values]
_ -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) [Char]
"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 = [Char] -> IE
SortErr [Char]
"sort-intersection multiadic argument (2)"
        (Funcons, Funcons)
_ -> do Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                    ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortInter (Values -> Funcons
FValue Values
v1) Funcons
s2
                    ValTerm [Values]
_ -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) [Char]
"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 = [Char] -> IE
SortErr [Char]
"sort-intersection multiadic argument (1)"
    rewriteFuncons' (FSortComplement Funcons
s1) = case Funcons
s1 of 
      FValue (ComputationType (Type Types
t1)) -> Values -> Rewrite Rewritten
rewritten (Values -> Rewrite Rewritten) -> Values -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal (Types -> Values) -> Types -> Values
forall a b. (a -> b) -> a -> b
$ Types -> Types
forall t. Types t -> Types t
Complement Types
t1
      FValue Values
_ -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons
FSortComplement Funcons
s1) [Char]
"sort-complement not applied to a sort" 
      Funcons
_ -> do Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
FSortComplement (Values -> Funcons
FValue Values
v)
                ValTerm [Values]
vs -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons
FSortComplement Funcons
s1) [Char]
"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 = [Char] -> IE
SortErr [Char]
"sort-complement multiadic argument"
    rewriteFuncons' (FName Name
nm) = 
        do  EvalFunction
mystepf <- Name -> Rewrite EvalFunction
lookupFuncon Name
nm 
            case EvalFunction
mystepf of 
                NullaryFuncon Rewrite Rewritten
mystep -> Rewrite Rewritten
mystep
                StrictFuncon ValueOp
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons' (Name -> [Funcons] -> Funcons
FApp Name
nm [])
                ValueOp ValueOp
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons' (Name -> [Funcons] -> Funcons
FApp Name
nm [])
                EvalFunction
_ -> [Char] -> Rewrite Rewritten
forall a. HasCallStack => [Char] -> a
error ([Char]
"funcon " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
nm [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" not applied to any arguments")
    rewriteFuncons' (FApp Name
nm [Funcons]
arg)    = 
        do  EvalFunction
mystepf <- Name -> Rewrite EvalFunction
lookupFuncon Name
nm
            case EvalFunction
mystepf of 
                NullaryFuncon Rewrite Rewritten
_     -> Funcons -> [Char] -> Rewrite Rewritten
forall a. Funcons -> [Char] -> Rewrite a
exception (Name -> [Funcons] -> Funcons
FApp Name
nm [Funcons]
arg) ([Char]
"nullary funcon " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
nm [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Char]
" applied to arguments: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Funcons] -> [Char]
showFunconsSeq [Funcons]
arg))
                ValueOp ValueOp
mystep      -> [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
arg ValueOp
mystep (Name -> [Funcons] -> Funcons
applyFuncon Name
nm)
                StrictFuncon ValueOp
mystep -> [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
arg ValueOp
mystep (Name -> [Funcons] -> Funcons
applyFuncon Name
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 (Name -> [Funcons] -> Funcons
applyFuncon Name
nm)

rewriteStrictSequence :: [Funcons] -> Rewrite [Values] 
rewriteStrictSequence :: [Funcons] -> Rewrite [Values]
rewriteStrictSequence [Funcons]
fs = case [Funcons]
rest of 
  []      -> [Values] -> Rewrite [Values]
forall a. a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return ((Funcons -> Values) -> [Funcons] -> [Values]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values
downcastValue [Funcons]
vs)
  (Funcons
x:[Funcons]
xs)  -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
x Rewrite Rewritten
-> (Rewritten -> Rewrite [Values]) -> Rewrite [Values]
forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
    ValTerm [Values]
vs'    -> [Funcons] -> Rewrite [Values]
rewriteStrictSequence ([Funcons]
vs[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++(Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs'[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++[Funcons]
xs)
    CompTerm Funcons
f0 MSOS StepRes
mf -> [Char] -> Rewrite [Values]
forall a. [Char] -> Rewrite a
internal ([Char]
"step on sequence of computations: " [Char] -> ShowS
forall a. [a] -> [a] -> [a]
++ [Funcons] -> [Char]
forall a. Show a => a -> [Char]
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

--OPT: replace by specialised variant of evalSequence
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 a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Funcons]
args) Strictness
Strict) [Funcons]
args 
        (ValueOp
cont ValueOp
-> ([Funcons] -> [Values]) -> [Funcons] -> Rewrite Rewritten
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Funcons -> Values) -> [Funcons] -> [Values]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values
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 = do
    let args_map :: [(Int, (Strictness, Funcons))]
        args_map :: [(Int, (Strictness, Funcons))]
args_map = [Int] -> [(Strictness, Funcons)] -> [(Int, (Strictness, Funcons))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] ([Strictness] -> [Funcons] -> [(Strictness, Funcons)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Strictness]
strns [Funcons]
args)

    let evalSeqAux :: [(Int, (Strictness, Funcons))]
-> [(Int, (Strictness, Funcons))] -> Rewrite Rewritten
evalSeqAux [(Int, (Strictness, Funcons))]
args_done [(Int, (Strictness, Funcons))]
args_undone 
          | [(Int, (Strictness, Funcons))] -> Bool
forall a. [a] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, (Strictness, Funcons))]
args_undone = [Funcons] -> Rewrite Rewritten
cont (((Int, (Strictness, Funcons)) -> Funcons)
-> [(Int, (Strictness, Funcons))] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map ((Strictness, Funcons) -> Funcons
forall a b. (a, b) -> b
snd ((Strictness, Funcons) -> Funcons)
-> ((Int, (Strictness, Funcons)) -> (Strictness, Funcons))
-> (Int, (Strictness, Funcons))
-> Funcons
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Strictness, Funcons)) -> (Strictness, Funcons)
forall a b. (a, b) -> b
snd) ([(Int, (Strictness, Funcons))] -> [(Int, (Strictness, Funcons))]
forall b. [(Int, b)] -> [(Int, b)]
sorter [(Int, (Strictness, Funcons))]
args_done))
          | Bool
otherwise        = do
              ((Int
i,(Strictness
_,Funcons
f)), [(Int, (Strictness, Funcons))]
args_undone') <- 
                SourceOfND
-> [(Int, (Strictness, Funcons))]
-> Rewrite
     ((Int, (Strictness, Funcons)), [(Int, (Strictness, Funcons))])
forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
NDInterleaving [(Int, (Strictness, Funcons))]
args_undone
              let valueCont :: ValueOp
valueCont [Values]
vs = do 
                    Rewrite ()
count_rewrite 
                    [(Int, (Strictness, Funcons))]
-> [(Int, (Strictness, Funcons))] -> Rewrite Rewritten
evalSeqAux [(Int, (Strictness, Funcons))]
args_done' (((Int, (Strictness, Funcons)) -> (Int, (Strictness, Funcons)))
-> [(Int, (Strictness, Funcons))] -> [(Int, (Strictness, Funcons))]
forall a b. (a -> b) -> [a] -> [b]
map (Int, (Strictness, Funcons)) -> (Int, (Strictness, Funcons))
forall {b}. (Int, b) -> (Int, b)
bump [(Int, (Strictness, Funcons))]
args_undone')
                    where args_done' :: [(Int, (Strictness, Funcons))]
args_done' = ((Int, (Strictness, Funcons)) -> Bool)
-> [(Int, (Strictness, Funcons))] -> [(Int, (Strictness, Funcons))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
i) (Int -> Bool)
-> ((Int, (Strictness, Funcons)) -> Int)
-> (Int, (Strictness, Funcons))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Strictness, Funcons)) -> Int
forall a b. (a, b) -> a
fst) [(Int, (Strictness, Funcons))]
args_done [(Int, (Strictness, Funcons))]
-> [(Int, (Strictness, Funcons))] -> [(Int, (Strictness, Funcons))]
forall a. [a] -> [a] -> [a]
++
                                        [Int] -> [(Strictness, Funcons)] -> [(Int, (Strictness, Funcons))]
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
i..] (([Strictness] -> [Funcons] -> [(Strictness, Funcons)]
forall a b. [a] -> [b] -> [(a, b)]
zip (Int -> Strictness -> [Strictness]
forall a. Int -> a -> [a]
replicate ([Values] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values]
vs) Strictness
Strict) 
                                                          ((Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs))) [(Int, (Strictness, Funcons))]
-> [(Int, (Strictness, Funcons))] -> [(Int, (Strictness, Funcons))]
forall a. [a] -> [a] -> [a]
++
                                       ((Int, (Strictness, Funcons)) -> (Int, (Strictness, Funcons)))
-> [(Int, (Strictness, Funcons))] -> [(Int, (Strictness, Funcons))]
forall a b. (a -> b) -> [a] -> [b]
map (Int, (Strictness, Funcons)) -> (Int, (Strictness, Funcons))
forall {b}. (Int, b) -> (Int, b)
bump (((Int, (Strictness, Funcons)) -> Bool)
-> [(Int, (Strictness, Funcons))] -> [(Int, (Strictness, Funcons))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
i) (Int -> Bool)
-> ((Int, (Strictness, Funcons)) -> Int)
-> (Int, (Strictness, Funcons))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Strictness, Funcons)) -> Int
forall a b. (a, b) -> a
fst) [(Int, (Strictness, Funcons))]
args_done)
                          bump :: (Int, b) -> (Int, b)
bump (Int
k,b
v) | Int
k Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> Int
i      = (Int
k Int -> Int -> Int
forall a. Num a => a -> a -> a
+ [Values] -> Int
forall a. [a] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values]
vs Int -> Int -> Int
forall a. Num a => a -> a -> a
- Int
1, b
v)
                                     | Bool
otherwise  = (Int
k,b
v)
              let funconCont :: MSOS StepRes -> MSOS StepRes
funconCont MSOS StepRes
stepf = MSOS StepRes
stepf MSOS StepRes -> (StepRes -> MSOS StepRes) -> MSOS StepRes
forall a b. MSOS a -> (a -> MSOS b) -> MSOS b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
                    Left Funcons
f' -> Funcons -> MSOS StepRes
stepTo ([Funcons] -> Funcons
cons ([(Int, (Strictness, Funcons))]
-> [Funcons] -> [(Int, (Strictness, Funcons))] -> [Funcons]
forall {a} {a}. [(Int, (a, a))] -> [a] -> [(Int, (a, a))] -> [a]
remakeArgs [(Int, (Strictness, Funcons))]
args_done [Funcons
f'] [(Int, (Strictness, Funcons))]
args_undone'))
                    Right [Values]
vs' -> Funcons -> MSOS StepRes
stepTo ([Funcons] -> Funcons
cons ([(Int, (Strictness, Funcons))]
-> [Funcons] -> [(Int, (Strictness, Funcons))] -> [Funcons]
forall {a} {a}. [(Int, (a, a))] -> [a] -> [(Int, (a, a))] -> [a]
remakeArgs [(Int, (Strictness, Funcons))]
args_done ((Values -> Funcons) -> [Values] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs') [(Int, (Strictness, Funcons))]
args_undone'))
                   where remakeArgs :: [(Int, (a, a))] -> [a] -> [(Int, (a, a))] -> [a]
remakeArgs [(Int, (a, a))]
m1 [a]
l1 [(Int, (a, a))]
m2 =  
                          ((Int, (a, a)) -> a) -> [(Int, (a, a))] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ((a, a) -> a
forall a b. (a, b) -> b
snd ((a, a) -> a) -> ((Int, (a, a)) -> (a, a)) -> (Int, (a, a)) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (a, a)) -> (a, a)
forall a b. (a, b) -> b
snd) ([(Int, (a, a))] -> [(Int, (a, a))]
forall b. [(Int, b)] -> [(Int, b)]
sorter (((Int, (a, a)) -> Bool) -> [(Int, (a, a))] -> [(Int, (a, a))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<Int
i) (Int -> Bool) -> ((Int, (a, a)) -> Int) -> (Int, (a, a)) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (a, a)) -> Int
forall a b. (a, b) -> a
fst) ([(Int, (a, a))]
m1[(Int, (a, a))] -> [(Int, (a, a))] -> [(Int, (a, a))]
forall a. [a] -> [a] -> [a]
++[(Int, (a, a))]
m2))) [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++ [a]
l1 [a] -> [a] -> [a]
forall a. [a] -> [a] -> [a]
++
                          ((Int, (a, a)) -> a) -> [(Int, (a, a))] -> [a]
forall a b. (a -> b) -> [a] -> [b]
map ((a, a) -> a
forall a b. (a, b) -> b
snd ((a, a) -> a) -> ((Int, (a, a)) -> (a, a)) -> (Int, (a, a)) -> a
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (a, a)) -> (a, a)
forall a b. (a, b) -> b
snd) ([(Int, (a, a))] -> [(Int, (a, a))]
forall b. [(Int, b)] -> [(Int, b)]
sorter (((Int, (a, a)) -> Bool) -> [(Int, (a, a))] -> [(Int, (a, a))]
forall a. (a -> Bool) -> [a] -> [a]
filter ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
>Int
i) (Int -> Bool) -> ((Int, (a, a)) -> Int) -> (Int, (a, a)) -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (a, a)) -> Int
forall a b. (a, b) -> a
fst) ([(Int, (a, a))]
m1[(Int, (a, a))] -> [(Int, (a, a))] -> [(Int, (a, a))]
forall a. [a] -> [a] -> [a]
++[(Int, (a, a))]
m2)))

              ValueOp
-> (MSOS StepRes -> MSOS StepRes) -> Funcons -> Rewrite Rewritten
premiseEval ValueOp
valueCont MSOS StepRes -> MSOS StepRes
funconCont Funcons
f          
    ([(Int, (Strictness, Funcons))]
 -> [(Int, (Strictness, Funcons))] -> Rewrite Rewritten)
-> ([(Int, (Strictness, Funcons))], [(Int, (Strictness, Funcons))])
-> Rewrite Rewritten
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [(Int, (Strictness, Funcons))]
-> [(Int, (Strictness, Funcons))] -> Rewrite Rewritten
evalSeqAux (((Int, (Strictness, Funcons)) -> Bool)
-> [(Int, (Strictness, Funcons))]
-> ([(Int, (Strictness, Funcons))], [(Int, (Strictness, Funcons))])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((Strictness, Funcons) -> Bool
isDone ((Strictness, Funcons) -> Bool)
-> ((Int, (Strictness, Funcons)) -> (Strictness, Funcons))
-> (Int, (Strictness, Funcons))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Int, (Strictness, Funcons)) -> (Strictness, Funcons)
forall a b. (a, b) -> b
snd) [(Int, (Strictness, Funcons))]
args_map)
 where  isDone :: (Strictness, Funcons) -> Bool
isDone (Strictness
NonStrict, Funcons
_)     = Bool
True
        isDone (Strictness
Strict, FValue Values
_) = Bool
True
        isDone (Strictness
Strict,Funcons
_)         = Bool
False
        sorter :: [(Int, b)] -> [(Int, b)]
        sorter :: forall b. [(Int, b)] -> [(Int, b)]
sorter = ((Int, b) -> (Int, b) -> Ordering) -> [(Int, b)] -> [(Int, b)]
forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (Int -> Int -> Ordering
forall a. Ord a => a -> a -> Ordering
compare (Int -> Int -> Ordering)
-> ((Int, b) -> Int) -> (Int, b) -> (Int, b) -> Ordering
forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` (Int, b) -> Int
forall a b. (a, b) -> a
fst)

-- | Yield an 'MSOS' computation as a fully rewritten term.
-- This function must be used in order to access entities in the definition
-- of funcons.
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)

--- transitive closure over steps
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]
vs -> StepRes -> MSOS StepRes
forall a. a -> MSOS a
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 a. a -> MSOS a
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 a. a -> MSOS a
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 a b. MSOS a -> MSOS b -> MSOS b
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 = (ereader ctxt) {global_fct = 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
           ((Name, Values) -> m ()) -> [(Name, Values)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Name -> Values -> m ()) -> (Name, Values) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Name -> Values -> m ()
forall (m :: * -> *). Interactive m => Name -> Values -> m ()
fprint) 
               [ (Name
entity,Values
val) 
               | (Name
entity, [Values]
vals) <- Inherited -> [(Name, [Values])]
forall k a. Map k a -> [(k, a)]
M.assocs (MSOSWriter -> Inherited
out_entities MSOSWriter
wr')
               , Values
val <- [Values]
vals ]
           (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall a. a -> m a
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
v)  = [Values] -> StepRes
forall a b. b -> Either a b
Right [Values
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 a b. MSOS a -> (a -> MSOS b) -> MSOS b
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
    Left Funcons
f    -> StepRes -> MSOS StepRes
forall a. a -> MSOS a
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
v] -> StepRes -> MSOS StepRes
forall a. a -> MSOS a
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
FValue Values
v)
    Right [Values]
vs  -> IE -> MSOS StepRes
forall b. IE -> MSOS b
msos_throw IE
ie