{-# 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.Applicative
import Control.Arrow ((***))
import Control.Monad.Writer hiding ((<>))
import Control.Monad.Fail
import Data.Function (on)
import Data.Maybe (isJust, isNothing, fromJust)
import Data.List (foldl', intercalate, partition, sortBy)
import Data.Text (unpack)
import Data.Semigroup

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 = forall a. IO a -> a
unsafePerformIO 
  ([Char] -> IO ()
putStrLn ([[Char]] -> [Char]
unlines (forall a b. (a -> b) -> [a] -> [b]
map Name -> [Char]
unpack (forall k a. Map k a -> [k]
M.keys FunconLibrary
lib))) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> 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 (forall t. HasValues t => OpExpr t -> EvalResult t
VAL.eval ([OpExpr Funcons] -> OpExpr Funcons
mkExpr (forall a b. (a -> b) -> [a] -> [b]
map forall t. Values t -> OpExpr t
ValExpr [Values]
vs))) 
        where f :: Funcons
f = [Funcons] -> Funcons
cons (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 (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            -> forall {b}. SourceOfND -> [b] -> Rewrite b
maybe_randomSelect SourceOfND
NDValueOperations [EvalResult Funcons]
ress 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 = forall a b. (a -> b) -> [a] -> [b]
map forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
fs, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isJust [Maybe Values]
mvs
                        = ValueOp
rewrittens (forall a b. (a -> b) -> [a] -> [b]
map 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)   -> forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
str
          (DomErr [Char]
str)        -> ValueOp
rewrittens [] 
          (ArityErr [Char]
str)      -> forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
str
          (ProjErr [Char]
str)       -> 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 
            []    -> forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
"nondeterminism: empty"
            [Result Funcons]
_     -> forall {b}. [b] -> Rewrite b
randomSelect [Result Funcons]
ress 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 = forall k a. Map k a
M.empty 

-- | Unites two 'FunconLibrary's.
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion = forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWithKey forall {p} {p} {a}. Name -> p -> p -> a
op
 where op :: Name -> p -> p -> a
op Name
k p
x p
_ = forall a. HasCallStack => [Char] -> a
error ([Char]
"duplicate funcon name: " 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 = forall a b c. (a -> b -> c) -> b -> a -> c
flip 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 = 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
_ = 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 = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse

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

lookupFuncon :: Name -> Rewrite EvalFunction
lookupFuncon :: Name -> Rewrite EvalFunction
lookupFuncon Name
key = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> 
    (case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
key (RewriteReader -> FunconLibrary
funconlib RewriteReader
ctxt) of
        Just EvalFunction
f -> forall a b. b -> Either a b
Right EvalFunction
f
        Maybe EvalFunction
_ -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
key (RunOptions -> BuiltinFunconsOptions
builtin_funcons (RewriteReader -> RunOptions
run_opts RewriteReader
ctxt)) of
               Just Funcons
f -> forall a b. b -> Either a b
Right (Rewrite Rewritten -> EvalFunction
NullaryFuncon (Funcons -> Rewrite Rewritten
rewriteTo Funcons
f))
               Maybe Funcons
_ -> forall a b. a -> Either a b
Left (IE -> RewriteReader -> IException
evalctxt2exception ([Char] -> IE
Internal ([Char]
"unknown funcon: "forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
key)) RewriteReader
ctxt)
    , RewriteState
st, 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 = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a 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 = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Monad Rewrite  where
  return :: forall a. a -> Rewrite a
return a
a = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite (\RewriteReader
_ RewriteState
st -> (forall a b. b -> Either a b
Right a
a, RewriteState
st, forall a. Monoid a => a
mempty))

  (Rewrite RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f) >>= :: forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
>>= a -> Rewrite b
k = 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  -> (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 forall a. Semigroup a => a -> a -> a
<> RewriteWriterr
cs2))

instance Semigroup RewriteWriterr where
  <> :: RewriteWriterr -> RewriteWriterr -> RewriteWriterr
(<>) = forall a. Monoid a => a -> a -> a
mappend

instance Monoid RewriteWriterr where
    mempty :: RewriteWriterr
mempty = Counters -> RewriteWriterr
RewriteWriterr forall a. Monoid a => a
mempty
    (RewriteWriterr Counters
cs1) mappend :: RewriteWriterr -> RewriteWriterr -> RewriteWriterr
`mappend` (RewriteWriterr Counters
cs2) = Counters -> RewriteWriterr
RewriteWriterr (Counters
cs1 forall a. Monoid a => a -> a -> a
`mappend` Counters
cs2)

liftRewrite :: Rewrite a -> MSOS a
liftRewrite :: forall a. Rewrite a -> MSOS a
liftRewrite Rewrite a
ev = forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> 
                let (Either IException a
e_a, RewriteState
est, RewriteWriterr
ewr) = forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite Rewrite a
ev (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) (forall (m :: * -> *). MSOSState m -> RewriteState
estate MSOSState m
mut)
                in forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException a
e_a, MSOSState m
mut {estate :: RewriteState
estate = RewriteState
est}, forall a. Monoid a => a
mempty { ewriter :: RewriteWriterr
ewriter = RewriteWriterr
ewr })

eval_catch :: Rewrite a -> Rewrite (Either IException a)
eval_catch :: forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch Rewrite a
eval = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> 
    let (Either IException a
eval_res, RewriteState
st', RewriteWriterr
eval_cs) = forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite Rewrite a
eval RewriteReader
ctxt RewriteState
st
    in (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 = forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch Rewrite a
ev forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right a
a -> forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    Left (Funcons
gf,Funcons
lf,IE
ie) | IE -> Bool
prop IE
ie   -> forall a. (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else IE -> Bool
prop [Rewrite a]
evs Rewrite a
def
                    | Bool
otherwise -> 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 = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> (forall a b. a -> Either a b
Left IException
ie, RewriteState
st, forall a. Monoid a => a
mempty)

rewrite_throw :: IE -> Rewrite a
rewrite_throw :: forall a. IE -> Rewrite a
rewrite_throw IE
ie = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> (forall a b. a -> Either a b
Left (IE -> RewriteReader -> IException
evalctxt2exception IE
ie RewriteReader
ctxt), RewriteState
st, 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 (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt), RewriteReader -> Funcons
local_fct (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 [] = forall a. IE -> Rewrite a
rewrite_throw ([IException] -> IE
NoMoreBranches [IException]
errs)
rewriteRules' [IException]
errs (Rewrite Rewritten
t1:[Rewrite Rewritten]
ts) = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->  
    let (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
rw_cs) = 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 
                                 forall {p} {p}. p -> p -> p
trace (IException -> [Char]
showIException IException
ie) forall a b. (a -> b) -> a -> b
$ 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
ieforall 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 = 
  forall (m :: * -> *).
Input m -> Inherited -> RewriteState -> MSOSState m
MSOSState forall k a. Map k a
M.empty forall k a. Map k a
M.empty (RewriteState
emptyRewriteState { random_gen :: StdGen
random_gen = Int -> StdGen
mkStdGen Int
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 = forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: forall a 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 = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Monad MSOS  where
  return :: forall a. a -> MSOS a
return a
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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right a
a,MSOSState m
mut,forall a. Monoid a => a
mempty))

  (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 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) <- 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  -> forall (m :: * -> *) a. Monad m => a -> m a
return (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) <- forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter)
h MSOSReader m
ctxt MSOSState m
mut1
                            forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException b
a2,MSOSState m
mut2,MSOSWriter
wr1 forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr2))

instance MonadFail MSOS where
  fail :: forall a. [Char] -> MSOS a
fail = forall a. Rewrite a -> MSOS a
liftRewrite forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> Rewrite a
internal 

instance Semigroup MSOSWriter where
  <> :: MSOSWriter -> MSOSWriter -> MSOSWriter
(<>) = forall a. Monoid a => a -> a -> a
mappend

instance Monoid MSOSWriter where
    mempty :: MSOSWriter
mempty = DownControl -> Inherited -> RewriteWriterr -> MSOSWriter
MSOSWriter forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
    (MSOSWriter DownControl
x1 Inherited
x2 RewriteWriterr
x3) mappend :: MSOSWriter -> MSOSWriter -> MSOSWriter
`mappend` (MSOSWriter DownControl
y1 Inherited
y2 RewriteWriterr
y3) = 
        DownControl -> Inherited -> RewriteWriterr -> MSOSWriter
MSOSWriter (DownControl
x1 forall {a}. Map Name a -> Map Name a -> Map Name a
`unionCTRL` DownControl
y1) (Inherited
x2 Inherited -> Inherited -> Inherited
`unionOUT` Inherited
y2) (RewriteWriterr
x3 forall a. Monoid a => a -> a -> a
`mappend` RewriteWriterr
y3) 

-- | 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 [] = forall b. IE -> MSOS b
msos_throw ([IException] -> IE
fexc [IException]
errs)
stepARules [IException] -> IE
fexc Rewrite ()
counter [IException]
errs [MSOS StepRes]
ts = 
 forall a. Rewrite a -> MSOS a
liftRewrite (forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
NDRuleSelection [MSOS StepRes]
ts) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= 
  \(MSOS StepRes
t1,[MSOS StepRes]
ts) -> forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS 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) <- 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
                                  forall {p} {p}. p -> p -> p
trace (IException -> [Char]
showIException IException
ie) forall a b. (a -> b) -> a -> b
$ forall a.
MSOS a
-> forall (m :: * -> *).
   Interactive m =>
   MSOSReader m
   -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS (do
                                    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]
errsforall a. [a] -> [a] -> [a]
++[IException
ie]) [MSOS StepRes]
ts) MSOSReader m
ctxt MSOSState m
mut
        Either IException StepRes
_                      -> 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 = 
 forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
NDRuleSelection [Rewrite Rewritten]
rules 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) -> 
  forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite 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 
                                   forall {p} {p}. p -> p -> p
trace (IException -> [Char]
showIException IException
ie) forall a b. (a -> b) -> a -> b
$ 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
ieforall 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 = forall a. Rewrite a -> MSOS a
liftRewrite forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IE -> Rewrite a
rewrite_throw 

---

giveOpts :: Rewrite RunOptions 
giveOpts :: Rewrite RunOptions
giveOpts = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
mut -> (forall a b. b -> Either a b
Right (RewriteReader -> RunOptions
run_opts RewriteReader
ctxt), RewriteState
mut, forall a. Monoid a => a
mempty)

giveINH :: MSOS Inherited
giveINH :: MSOS Inherited
giveINH = forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (forall (m :: * -> *). MSOSReader m -> Inherited
inh_entities MSOSReader m
ctxt), MSOSState m
mut, forall a. Monoid a => a
mempty)

giveCTRL :: MSOS DownControl 
giveCTRL :: MSOS DownControl
giveCTRL = forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (forall (m :: * -> *). MSOSReader m -> DownControl
dctrl_entities MSOSReader m
ctxt), MSOSState m
mut, forall a. Monoid a => a
mempty)

doRefocus :: MSOS Bool
doRefocus :: MSOS Bool
doRefocus = forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> 
    forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ RunOptions -> Bool
do_refocus (RewriteReader -> RunOptions
run_opts (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt)), MSOSState m
mut, 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) = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f 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 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)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {m :: * -> *}. MSOSReader m -> MSOSReader m
mod')
  where mod' :: MSOSReader m -> MSOSReader m
mod' MSOSReader m
ctxt = MSOSReader m
ctxt { ereader :: RewriteReader
ereader = RewriteReader -> RewriteReader
mod (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) }

maybe_randomRemove :: SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove :: forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
_ [] = 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 forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` RunOptions -> [SourceOfND]
get_nd_sources RunOptions
opts then forall a. [a] -> Rewrite (a, [a])
randomRemove [a]
xs
                                    else 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 [] = forall a. [Char] -> Rewrite a
internal [Char]
"randomRemove: empty list"
randomRemove [a
x]= forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, [])
randomRemove [a]
xs = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
mut -> 
  let gen :: StdGen
gen       = RewriteState -> StdGen
random_gen RewriteState
mut 
      (Int
i, StdGen
gen') = forall g. RandomGen g => g -> (Int, g)
next StdGen
gen
      index :: Int
index     = Int
i forall a. Integral a => a -> a -> a
`mod` (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs)
      elem :: a
elem      = [a]
xs forall a. [a] -> Int -> a
!! Int
index 
      rest :: [a]
rest      = forall a. Int -> [a] -> [a]
take Int
index [a]
xs forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
drop (Int
index forall a. Num a => a -> a -> a
+ Int
1) [a]
xs 
  in (forall a b. b -> Either a b
Right (a
elem, [a]
rest), RewriteState
mut {random_gen :: StdGen
random_gen = StdGen
gen'}, forall a. Monoid a => a
mempty )

maybe_randomSelect :: SourceOfND -> [b] -> Rewrite b
maybe_randomSelect SourceOfND
src [b]
xs = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
src [b]
xs
randomSelect :: [b] -> Rewrite b
randomSelect [b]
xs = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f 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 = 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 = forall k a. Map k a
M.empty

emptyCTRL :: Control
emptyCTRL :: DownControl
emptyCTRL = forall k a. Map k a
M.empty

singleCTRL :: Name -> Values -> Control
singleCTRL :: Name -> Values -> DownControl
singleCTRL Name
k = forall k a. k -> a -> Map k a
M.singleton Name
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just

unionCTRL :: Map Name a -> Map Name a -> Map Name a
unionCTRL = forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWithKey (forall a. HasCallStack => [Char] -> a
error forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
err)
 where err :: Name -> [Char]
err Name
key = [Char]
"Two " forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
key 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 = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. [a] -> [a] -> [a]
(++)

emptyOUT :: Output 
emptyOUT :: Inherited
emptyOUT = 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 a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ (\MSOSReader m
ctxt MSOSState m
mut -> do 
    (Either IException a
e_a, MSOSState m
mut1, MSOSWriter
wr1) <- 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left IException
err, MSOSState m
mut1, MSOSWriter
wr1)
        Right a
a  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (a
a,(MSOSWriter -> Inherited
out_entities MSOSWriter
wr1))
                            , MSOSState m
mut1, MSOSWriter
wr1 { out_entities :: Inherited
out_entities = forall a. Monoid a => a
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 -> Counters -> Counters
(<>) = forall a. Monoid a => a -> a -> a
mappend

instance Monoid Counters where
    mempty :: Counters
mempty = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0
    (Counters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8) mappend :: Counters -> Counters -> Counters
`mappend` (Counters Int
y1 Int
y2 Int
y3 Int
y4 Int
y5 Int
y6 Int
y7 Int
y8) = 
        Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters (Int
x1forall a. Num a => a -> a -> a
+Int
y1) (Int
x2forall a. Num a => a -> a -> a
+Int
y2) (Int
x3forall a. Num a => a -> a -> a
+Int
y3) (Int
x4forall a. Num a => a -> a -> a
+Int
y4) (Int
x5forall a. Num a => a -> a -> a
+Int
y5) (Int
x6forall a. Num a => a -> a -> a
+Int
y6) (Int
x7forall a. Num a => a -> a -> a
+Int
y7) (Int
x8forall a. Num a => a -> a -> a
+Int
y8)

emptyCounters :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8 = 
    forall a. Monoid a => a
mempty { ewriter :: RewriteWriterr
ewriter = forall a. Monoid a => a
mempty {counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8}}

addToCounter :: Counters -> MSOS ()
addToCounter :: Counters -> MSOS ()
addToCounter Counters
cs = forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right(), MSOSState m
mut, forall a. Monoid a => a
mempty { ewriter :: RewriteWriterr
ewriter = forall a. Monoid a => a
mempty { counters :: Counters
counters = Counters
cs } })

addToRCounter :: Counters -> Rewrite () 
addToRCounter :: Counters -> Rewrite ()
addToRCounter Counters
cs = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
mut -> (forall a b. b -> Either a b
Right(), RewriteState
mut, forall a. Monoid a => a
mempty { counters :: Counters
counters = Counters
cs })

count_step :: MSOS ()
count_step :: MSOS ()
count_step = forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (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 a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (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 a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (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 a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (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 = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (forall a b. b -> Either a b
Right (), RewriteState
st, forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
1 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0})

count_rewrite_attempt :: Rewrite ()
count_rewrite_attempt :: Rewrite ()
count_rewrite_attempt = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (forall a b. b -> Either a b
Right (), RewriteState
st, forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
1 Int
0 Int
0 Int
0 Int
0 Int
0})

count_backtrack_out :: Rewrite ()
count_backtrack_out :: Rewrite ()
count_backtrack_out = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (forall a b. b -> Either a b
Right (), RewriteState
st, forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
1 Int
0 })

count_backtrack_in :: Rewrite ()
count_backtrack_in :: Rewrite ()
count_backtrack_in = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (forall a b. b -> Either a b
Right (), RewriteState
st, forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
1 })

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

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) = 
  forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," forall a b. (a -> b) -> a -> b
$ 
    forall a b. (a -> b) -> [a] -> [b]
map 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 = 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 = 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 = 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 = 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 = 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 = 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 (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 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 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 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 forall (m :: * -> *) a. Monad m => a -> m a
return StepRes -> MSOS StepRes
continue
    where continue :: StepRes -> MSOS StepRes
continue = \case
            Right [Values]
vs  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [Values]
vs)
            Left Funcons
f    -> 
              forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [Values
v])
                ValTerm [Values]
vs  -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left Funcons
f) -- undo rewrites and accept last step
                Rewritten
res         -> MSOS StepRes -> MSOS StepRes
refocus 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) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [Values]
vs)
stepRewritten (CompTerm Funcons
f MSOS StepRes
step) = forall a. (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader RewriteReader -> RewriteReader
mod (MSOS ()
count_step forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes
step)
  where mod :: RewriteReader -> RewriteReader
mod RewriteReader
ctxt = RewriteReader
ctxt {local_fct :: Funcons
local_fct = Funcons
f}

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

rewrittens :: [Values] -> Rewrite Rewritten
rewrittens :: ValueOp
rewrittens = forall (m :: * -> *) a. Monad m => a -> m a
return 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 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 forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([Values] -> Rewritten
ValTerm 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 = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> 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 a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
    forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut 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     = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any 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'') <- forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut'
                  forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr' forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr'')
        (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res -> 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 a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
    forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut 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 = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Maybe a -> Bool
isJust (MSOSWriter -> DownControl
ctrl_entities MSOSWriter
wr')
                            Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (MSOSWriter -> Inherited
out_entities MSOSWriter
wr')
                            Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (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'') <- forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut'
                  forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr' forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr'')
        (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res -> 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 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 = forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ValTerm [Values]
vs      -> forall b. IE -> MSOS b
msos_throw ([Values] -> IE
StepOnValue [Values]
vs)
    CompTerm Funcons
_ MSOS StepRes
step -> StepRes -> StepRes
app forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSOS ()
count_delegation 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 forall a. a -> a
id 

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

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

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

rewriteToValErr :: Rewrite a
rewriteToValErr = forall a. IE -> Rewrite a
rewrite_throw 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 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 = forall a.
(RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT (\RewriteReader
ctxt -> RewriteReader
ctxt{local_fct :: Funcons
local_fct = Funcons
f}) (Funcons -> Rewrite Rewritten
rewriteFuncons' Funcons
f)
 where
    rewriteFuncons' :: Funcons -> Rewrite Rewritten
rewriteFuncons' (FValue Values
v)   = 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 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 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
fkforall a. a -> [a] -> [a]
:[Funcons]
fv) (Values -> Rewrite Rewritten
rewritten forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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]
_       = 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 <- forall t. Values t -> Values t
upcastNaturals Values
v -> 
                  ValueOp
rewrittens (forall a. Int -> a -> [a]
replicate (forall a. Num a => Integer -> a
fromInteger Integer
n) (forall t. ComputationTypes t -> Values t
ComputationType (forall t. Types t -> ComputationTypes t
Type (forall t. Values t -> Types t
downcastValueType Values
mty))))
      (FValue Values
mty, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
fn forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
            ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortPower Funcons
s1 (Values -> Funcons
FValue Values
v)
            ValTerm [Values]
_   -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortPower (Values -> Funcons
FValue Values
v) Funcons
fn
            ValTerm [Values]
_   -> 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 (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 forall a b. (a -> b) -> a -> b
$ forall t. ComputationTypes t -> Values t
ComputationType forall a b. (a -> b) -> a -> b
$ forall t. Types t -> ComputationTypes t
Type forall a b. (a -> b) -> a -> b
$ forall t. Types t -> SeqSortOp -> Types t
AnnotatedType Types
ty SeqSortOp
op
      (FValue Values
_) -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> SeqSortOp -> Funcons
FSortSeq (Values -> Funcons
FValue Values
v1) SeqSortOp
op
            ValTerm [Values]
vs   -> 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 (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 forall a b. (a -> b) -> a -> b
$ forall t. ComputationTypes t -> Values t
ComputationType forall a b. (a -> b) -> a -> b
$ forall t. Types t -> ComputationTypes t
ComputesType Types
ty
        (FValue Values
_) -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
FSortComputes (Values -> Funcons
FValue Values
v1)
                ValTerm [Values]
vs   -> 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 forall a b. (a -> b) -> a -> b
$ forall t. ComputationTypes t -> Values t
ComputationType (forall t. Types t -> Types t -> ComputationTypes t
ComputesFromType Types
ty1 Types
ty2)
        (FValue Values
_, FValue Values
_) -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 (Values -> Funcons
FValue Values
v2)
                ValTerm [Values]
_ -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortComputesFrom (Values -> Funcons
FValue Values
v1) Funcons
f2
                ValTerm [Values]
_ -> 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 (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 forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal forall a b. (a -> b) -> a -> b
$ forall t. Types t -> Types t -> Types t
Union Types
t1 Types
t2
        (FValue Values
_, FValue Values
_) -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 (Values -> Funcons
FValue Values
v2)
            ValTerm [Values]
_ -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortUnion (Values -> Funcons
FValue Values
v) Funcons
s2
                ValTerm [Values]
_ -> 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 (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 forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal forall a b. (a -> b) -> a -> b
$ forall t. Types t -> Types t -> Types t
Intersection Types
t1 Types
t2
        (FValue Values
_, FValue Values
_) -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 (Values -> Funcons
FValue Values
v2)
            ValTerm [Values]
_ -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                    ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortInter (Values -> Funcons
FValue Values
v1) Funcons
s2
                    ValTerm [Values]
_ -> 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 (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 forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal forall a b. (a -> b) -> a -> b
$ forall t. Types t -> Types t
Complement Types
t1
      FValue Values
_ -> 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
FSortComplement (Values -> Funcons
FValue Values
v)
                ValTerm [Values]
vs -> 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
_ -> forall a. HasCallStack => [Char] -> a
error ([Char]
"funcon " forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
nm 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
_     -> forall a. Funcons -> [Char] -> Rewrite a
exception (Name -> [Funcons] -> Funcons
FApp Name
nm [Funcons]
arg) ([Char]
"nullary funcon " forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
nm forall a. [a] -> [a] -> [a]
++ [Char]
" applied to arguments: " 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 forall a. [a] -> [a] -> [a]
++ 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 
  []      -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values
downcastValue [Funcons]
vs)
  (Funcons
x:[Funcons]
xs)  -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
    ValTerm [Values]
vs'    -> [Funcons] -> Rewrite [Values]
rewriteStrictSequence ([Funcons]
vsforall a. [a] -> [a] -> [a]
++forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs'forall a. [a] -> [a] -> [a]
++[Funcons]
xs)
    CompTerm Funcons
f0 MSOS StepRes
mf -> forall a. [Char] -> Rewrite a
internal ([Char]
"step on sequence of computations: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Funcons]
fs)
  where ([Funcons]
vs, [Funcons]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not 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 (forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Funcons]
args) Strictness
Strict) [Funcons]
args 
        (ValueOp
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] (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 
          | forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, (Strictness, Funcons))]
args_undone = [Funcons] -> Rewrite Rewritten
cont (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (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') <- 
                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' (forall a b. (a -> b) -> [a] -> [b]
map forall {b}. (Int, b) -> (Int, b)
bump [(Int, (Strictness, Funcons))]
args_undone')
                    where args_done' :: [(Int, (Strictness, Funcons))]
args_done' = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
<Int
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Int, (Strictness, Funcons))]
args_done forall a. [a] -> [a] -> [a]
++
                                        forall a b. [a] -> [b] -> [(a, b)]
zip [Int
i..] ((forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values]
vs) Strictness
Strict) 
                                                          (forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs))) forall a. [a] -> [a] -> [a]
++
                                       forall a b. (a -> b) -> [a] -> [b]
map forall {b}. (Int, b) -> (Int, b)
bump (forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
>Int
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Int, (Strictness, Funcons))]
args_done)
                          bump :: (Int, b) -> (Int, b)
bump (Int
k,b
v) | Int
k forall a. Ord a => a -> a -> Bool
> Int
i      = (Int
k forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values]
vs 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 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
                    Left Funcons
f' -> Funcons -> MSOS StepRes
stepTo ([Funcons] -> Funcons
cons (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 (forall {a} {a}. [(Int, (a, a))] -> [a] -> [(Int, (a, a))] -> [a]
remakeArgs [(Int, (Strictness, Funcons))]
args_done (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 =  
                          forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall {b}. [(Int, b)] -> [(Int, b)]
sorter (forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
<Int
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) ([(Int, (a, a))]
m1forall a. [a] -> [a] -> [a]
++[(Int, (a, a))]
m2))) forall a. [a] -> [a] -> [a]
++ [a]
l1 forall a. [a] -> [a] -> [a]
++
                          forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall {b}. [(Int, b)] -> [(Int, b)]
sorter (forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
>Int
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) ([(Int, (a, a))]
m1forall 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          
    forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [(Int, (Strictness, Funcons))]
-> [(Int, (Strictness, Funcons))] -> Rewrite Rewritten
evalSeqAux (forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((Strictness, Funcons) -> Bool
isDone forall b c a. (b -> c) -> (a -> b) -> a -> c
. 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 a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` 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 = forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> 
    let f0 :: Funcons
f0 = RewriteReader -> Funcons
local_fct RewriteReader
ctxt 
    in (forall a b. b -> Either a b
Right (Funcons -> MSOS StepRes -> Rewritten
CompTerm Funcons
f0 MSOS StepRes
mf), RewriteState
st, 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 -> forall (m :: * -> *) a. Monad m => a -> m a
return StepRes
res
  Left Funcons
f | forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((forall a. Ord a => a -> a -> Bool
<= Int
i)) (RunOptions -> Maybe Int
max_restarts RunOptions
opts) -> 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) forall (m :: * -> *) a. Monad m => a -> m a
return StepRes -> MSOS StepRes
continue
       where continue :: StepRes -> MSOS StepRes
continue StepRes
res = MSOS ()
count_restart forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans RunOptions
opts (Int
iforall a. Num a => a -> a -> a
+Int
1) StepRes
res

stepAndOutput :: Funcons -> MSOS StepRes
stepAndOutput :: Funcons -> MSOS StepRes
stepAndOutput Funcons
f = forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS 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 = forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper' (forall {m :: * -> *}. MSOSReader m -> MSOSReader m
setGlobal MSOSReader m
ctxt) MSOSState m
mut
       setGlobal :: MSOSReader m -> MSOSReader m
setGlobal MSOSReader m
ctxt = MSOSReader m
ctxt 
               { ereader :: RewriteReader
ereader = (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) {global_fct :: Funcons
global_fct = Funcons
f }}
   in do   (Either IException StepRes
eres,MSOSState m
mut',MSOSWriter
wr') <- forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper MSOSReader m
ctxt MSOSState m
mut
           forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (m :: * -> *). Interactive m => Name -> Values -> m ()
fprint) 
               [ (Name
entity,Values
val) 
               | (Name
entity, [Values]
vals) <- forall k a. Map k a -> [(k, a)]
M.assocs (MSOSWriter -> Inherited
out_entities MSOSWriter
wr')
               , Values
val <- [Values]
vals ]
           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)  = forall a b. b -> Either a b
Right [Values
v]
toStepRes Funcons
f           = 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 forall a b. (a -> b) -> a -> b
$ MSOS StepRes
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
    Left Funcons
f    -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
app Funcons
f
    Right [Values
v] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
app (Values -> Funcons
FValue Values
v)
    Right [Values]
vs  -> forall b. IE -> MSOS b
msos_throw IE
ie