{-# 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, rewritesToValue, rewritesToValues, rewritesToType
          , emptyDCTRL, emptyINH, Interactive(..), SimIO(..)
          , rewriteToValErr, count_delegation, optRefocus
          , evalStrictSequence, rewriteStrictSequence, evalSequence,
    -- * 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.Maybe (isJust, isNothing, fromJust)
import Data.List (foldl', intercalate)
import Data.Text (unpack)
import Data.Semigroup

import qualified Data.Map as M

import System.IO.Unsafe
--trace p b = unsafePerformIO (putStrLn p >> return b) 
trace :: p -> p -> p
trace p
p p
b = p
b
traceLib :: FunconLibrary -> FunconLibrary
traceLib :: FunconLibrary -> FunconLibrary
traceLib FunconLibrary
lib = IO FunconLibrary -> FunconLibrary
forall a. IO a -> a
unsafePerformIO 
  (String -> IO ()
putStrLn ([String] -> String
unlines ((Text -> String) -> [Text] -> [String]
forall a b. (a -> b) -> [a] -> [b]
map Text -> String
unpack (FunconLibrary -> [Text]
forall k a. Map k a -> [k]
M.keys FunconLibrary
lib))) IO () -> IO FunconLibrary -> IO FunconLibrary
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> FunconLibrary -> IO FunconLibrary
forall (m :: * -> *) a. Monad m => a -> m a
return FunconLibrary
lib)


---------------------------------------------------------------------
-- | 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 Funcons]
vs = Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report Funcons
f Bool
seqRes (OpExpr Funcons -> EvalResult Funcons
forall t. HasValues t => OpExpr t -> EvalResult t
VAL.eval ([OpExpr Funcons] -> OpExpr Funcons
mkExpr ((Values Funcons -> OpExpr Funcons)
-> [Values Funcons] -> [OpExpr Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> OpExpr Funcons
forall t. Values t -> OpExpr t
ValExpr [Values Funcons]
vs))) 
        where f :: Funcons
f = [Funcons] -> Funcons
cons ((Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
vs)
fromNullaryValOp :: ([Funcons] -> Funcons) -> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromNullaryValOp :: ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromNullaryValOp [Funcons] -> Funcons
cons [OpExpr Funcons] -> OpExpr Funcons
mkExpr = Rewrite Rewritten -> EvalFunction
NullaryFuncon Rewrite Rewritten
op
  where op :: Rewrite Rewritten
op = Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report ([Funcons] -> Funcons
cons []) Bool
False (OpExpr Funcons -> EvalResult Funcons
forall t. HasValues t => OpExpr t -> EvalResult t
VAL.eval ([OpExpr Funcons] -> OpExpr Funcons
mkExpr []))

report :: Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report Funcons
f Bool
seqRes EvalResult Funcons
res = case EvalResult Funcons
res of
  Error OpExpr Funcons
_ (VAL.SortErr String
str)   -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f String
str
  Error OpExpr Funcons
_ (DomErr String
str)        -> ValueOp
rewrittens [] 
  Error OpExpr Funcons
_ (ArityErr String
str)      -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f String
str
  Error OpExpr Funcons
_ (ProjErr String
str)       -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f String
str
  Error OpExpr Funcons
_ (Normal (FValue Values Funcons
v)) -> Values Funcons -> Rewrite Rewritten
rewritten' Values Funcons
v
  Error OpExpr Funcons
_ (Normal Funcons
t)          -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
t
  Success (FValue (ADTVal Text
"null" [Funcons]
_)) -> ValueOp
rewrittens []
  Success (FValue Values Funcons
v)          -> Values Funcons -> Rewrite Rewritten
rewritten' Values Funcons
v
  Success Funcons
t                   -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
t
  where rewritten' :: Values Funcons -> Rewrite Rewritten
rewritten' Values Funcons
v | Bool
seqRes, ValSeq [Funcons]
fs <- Values Funcons
v, 
                        let mvs :: [Maybe (Values Funcons)]
mvs = (Funcons -> Maybe (Values Funcons))
-> [Funcons] -> [Maybe (Values Funcons)]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Maybe (Values Funcons)
forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
fs, (Maybe (Values Funcons) -> Bool)
-> [Maybe (Values Funcons)] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all Maybe (Values Funcons) -> Bool
forall a. Maybe a -> Bool
isJust [Maybe (Values Funcons)]
mvs
                        = ValueOp
rewrittens ((Maybe (Values Funcons) -> Values Funcons)
-> [Maybe (Values Funcons)] -> [Values Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Maybe (Values Funcons) -> Values Funcons
forall a. HasCallStack => Maybe a -> a
fromJust [Maybe (Values Funcons)]
mvs)
                     | Bool
otherwise = Values Funcons -> Rewrite Rewritten
rewritten Values Funcons
v
 
-- |
-- 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 -> String
show (ValTerm [Values Funcons]
vs) = [Values Funcons] -> String
showValuesSeq [Values Funcons]
vs
    show (CompTerm Funcons
_ MSOS StepRes
_) = String
"<step>"

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

-- | Unites two 'FunconLibrary's.
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion = (Text -> EvalFunction -> EvalFunction -> EvalFunction)
-> FunconLibrary -> FunconLibrary -> FunconLibrary
forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWithKey Text -> EvalFunction -> EvalFunction -> EvalFunction
forall p p a. Text -> p -> p -> a
op
 where op :: Text -> p -> p -> a
op Text
k p
x p
_ = String -> a
forall a. HasCallStack => String -> a
error (String
"duplicate funcon name: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
unpack Text
k)

-- | Right-based union of 'FunconLibrary's
libOverride :: FunconLibrary -> FunconLibrary -> FunconLibrary 
libOverride :: FunconLibrary -> FunconLibrary -> FunconLibrary
libOverride = (FunconLibrary -> FunconLibrary -> FunconLibrary)
-> FunconLibrary -> FunconLibrary -> FunconLibrary
forall a b c. (a -> b -> c) -> b -> a -> c
flip FunconLibrary -> FunconLibrary -> FunconLibrary
forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union 

-- | Unites a list of 'FunconLibrary's.
libUnions :: [FunconLibrary] -> FunconLibrary
libUnions :: [FunconLibrary] -> FunconLibrary
libUnions = (FunconLibrary -> FunconLibrary -> FunconLibrary)
-> FunconLibrary -> [FunconLibrary] -> FunconLibrary
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion FunconLibrary
libEmpty
 where op :: p -> p -> a
op p
_ p
_ = String -> a
forall a. HasCallStack => String -> a
error (String
"duplicate funcon name")

-- | Right-based union of list of 'FunconLibrary's
libOverrides :: [FunconLibrary] -> FunconLibrary
libOverrides :: [FunconLibrary] -> FunconLibrary
libOverrides = [FunconLibrary] -> FunconLibrary
forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions ([FunconLibrary] -> FunconLibrary)
-> ([FunconLibrary] -> [FunconLibrary])
-> [FunconLibrary]
-> FunconLibrary
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [FunconLibrary] -> [FunconLibrary]
forall a. [a] -> [a]
reverse

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

lookupFuncon :: Name -> Rewrite EvalFunction
lookupFuncon :: Text -> Rewrite EvalFunction
lookupFuncon Text
key = (RewriteReader
 -> RewriteState
 -> (Either IException EvalFunction, RewriteState, RewriteWriterr))
-> Rewrite EvalFunction
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
  -> RewriteState
  -> (Either IException EvalFunction, RewriteState, RewriteWriterr))
 -> Rewrite EvalFunction)
-> (RewriteReader
    -> RewriteState
    -> (Either IException EvalFunction, RewriteState, RewriteWriterr))
-> Rewrite EvalFunction
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> 
    (case Text -> FunconLibrary -> Maybe EvalFunction
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
key (RewriteReader -> FunconLibrary
funconlib RewriteReader
ctxt) of
        Just EvalFunction
f -> EvalFunction -> Either IException EvalFunction
forall a b. b -> Either a b
Right EvalFunction
f
        Maybe EvalFunction
_ -> case Text -> Map Text Funcons -> Maybe Funcons
forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Text
key (RunOptions -> Map Text Funcons
builtin_funcons (RewriteReader -> RunOptions
run_opts RewriteReader
ctxt)) of
               Just Funcons
f -> EvalFunction -> Either IException EvalFunction
forall a b. b -> Either a b
Right (Rewrite Rewritten -> EvalFunction
NullaryFuncon (Funcons -> Rewrite Rewritten
rewriteTo Funcons
f))
               Maybe Funcons
_ -> IException -> Either IException EvalFunction
forall a b. a -> Either a b
Left (IE -> RewriteReader -> IException
evalctxt2exception (String -> IE
Internal (String
"unknown funcon: "String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
unpack Text
key)) RewriteReader
ctxt)
    , RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty)

---------------------------------------------------------------------------
data RewriteReader = RewriteReader  
                    { RewriteReader -> FunconLibrary
funconlib  :: FunconLibrary    
                    , RewriteReader -> TypeRelation
ty_env     :: TypeRelation, RewriteReader -> RunOptions
run_opts :: RunOptions
                    , RewriteReader -> Funcons
global_fct :: Funcons, RewriteReader -> Funcons
local_fct :: Funcons }
data RewriteState = RewriteState {  }
emptyRewriteState :: RewriteState
emptyRewriteState = RewriteState
RewriteState 
data RewriteWriterr = RewriteWriterr { RewriteWriterr -> Counters
counters :: Counters }

-- | 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 {Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite :: (RewriteReader -> RewriteState -> 
                    (Either IException a, RewriteState, RewriteWriterr))}

instance Applicative Rewrite where
  pure :: a -> Rewrite a
pure = a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: Rewrite (a -> b) -> Rewrite a -> Rewrite b
(<*>) = Rewrite (a -> b) -> Rewrite a -> Rewrite b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Functor Rewrite where
  fmap :: (a -> b) -> Rewrite a -> Rewrite b
fmap = (a -> b) -> Rewrite a -> Rewrite b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

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

  (Rewrite RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f) >>= :: Rewrite a -> (a -> Rewrite b) -> Rewrite b
>>= a -> Rewrite b
k = (RewriteReader
 -> RewriteState
 -> (Either IException b, RewriteState, RewriteWriterr))
-> Rewrite b
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite (\RewriteReader
ctxt RewriteState
st ->
                    let res1 :: (Either IException a, RewriteState, RewriteWriterr)
res1@(Either IException a
e_a1,RewriteState
st1,RewriteWriterr
cs1) = RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f RewriteReader
ctxt RewriteState
st
                     in case Either IException a
e_a1 of 
                          Left IException
err  -> (IException -> Either IException b
forall a b. a -> Either a b
Left IException
err, RewriteState
st1, RewriteWriterr
cs1)
                          Right a
a1  -> let (Rewrite RewriteReader
-> RewriteState
-> (Either IException b, RewriteState, RewriteWriterr)
h) = a -> Rewrite b
k a
a1
                                           (Either IException b
a2,RewriteState
st2,RewriteWriterr
cs2) = RewriteReader
-> RewriteState
-> (Either IException b, RewriteState, RewriteWriterr)
h RewriteReader
ctxt RewriteState
st1
                                        in (Either IException b
a2,RewriteState
st2,RewriteWriterr
cs1 RewriteWriterr -> RewriteWriterr -> RewriteWriterr
forall a. Semigroup a => a -> a -> a
<> RewriteWriterr
cs2))

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

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

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

eval_catch :: Rewrite a -> Rewrite (Either IException a)
eval_catch :: Rewrite a -> Rewrite (Either IException a)
eval_catch Rewrite a
eval = (RewriteReader
 -> RewriteState
 -> (Either IException (Either IException a), RewriteState,
     RewriteWriterr))
-> Rewrite (Either IException a)
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
  -> RewriteState
  -> (Either IException (Either IException a), RewriteState,
      RewriteWriterr))
 -> Rewrite (Either IException a))
-> (RewriteReader
    -> RewriteState
    -> (Either IException (Either IException a), RewriteState,
        RewriteWriterr))
-> Rewrite (Either IException a)
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> 
    let (Either IException a
eval_res, RewriteState
st', RewriteWriterr
eval_cs) = Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite Rewrite a
eval RewriteReader
ctxt RewriteState
st
    in (Either IException a -> Either IException (Either IException a)
forall a b. b -> Either a b
Right Either IException a
eval_res, RewriteState
st', RewriteWriterr
eval_cs) 

eval_else :: (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else :: (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else IE -> Bool
prop [] Rewrite a
def = Rewrite a
def
eval_else IE -> Bool
prop (Rewrite a
ev:[Rewrite a]
evs) Rewrite a
def = Rewrite a -> Rewrite (Either IException a)
forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch Rewrite a
ev Rewrite (Either IException a)
-> (Either IException a -> Rewrite a) -> Rewrite a
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    Right a
a -> a -> Rewrite a
forall (m :: * -> *) a. Monad m => a -> m a
return a
a
    Left (Funcons
gf,Funcons
lf,IE
ie) | IE -> Bool
prop IE
ie   -> (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
forall a. (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else IE -> Bool
prop [Rewrite a]
evs Rewrite a
def
                    | Bool
otherwise -> IException -> Rewrite a
forall a. IException -> Rewrite a
rewrite_rethrow (Funcons
gf,Funcons
lf,IE
ie)

rewrite_rethrow :: IException -> Rewrite a
rewrite_rethrow :: IException -> Rewrite a
rewrite_rethrow IException
ie = (RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
  -> RewriteState
  -> (Either IException a, RewriteState, RewriteWriterr))
 -> Rewrite a)
-> (RewriteReader
    -> RewriteState
    -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> (IException -> Either IException a
forall a b. a -> Either a b
Left IException
ie, RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty)

rewrite_throw :: IE -> Rewrite a
rewrite_throw :: IE -> Rewrite a
rewrite_throw IE
ie = (RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
  -> RewriteState
  -> (Either IException a, RewriteState, RewriteWriterr))
 -> Rewrite a)
-> (RewriteReader
    -> RewriteState
    -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> (IException -> Either IException a
forall a b. a -> Either a b
Left (IE -> RewriteReader -> IException
evalctxt2exception IE
ie RewriteReader
ctxt), RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty)

evalctxt2exception :: IE -> RewriteReader -> IException
evalctxt2exception :: IE -> RewriteReader -> IException
evalctxt2exception IE
ie RewriteReader
ctxt = (RewriteReader -> Funcons
global_fct RewriteReader
ctxt, RewriteReader -> Funcons
local_fct RewriteReader
ctxt, IE
ie)

ctxt2exception :: IE -> MSOSReader m -> IException
ctxt2exception :: IE -> MSOSReader m -> IException
ctxt2exception IE
ie MSOSReader m
ctxt = 
    (RewriteReader -> Funcons
global_fct (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt), RewriteReader -> Funcons
local_fct (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt), IE
ie)

rewriteRules :: [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules = [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' []
rewriteRules' :: [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' :: [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' [IException]
errs [] = IE -> Rewrite Rewritten
forall a. IE -> Rewrite a
rewrite_throw ([IException] -> IE
NoMoreBranches [IException]
errs)
rewriteRules' [IException]
errs (Rewrite Rewritten
t1:[Rewrite Rewritten]
ts) = (RewriteReader
 -> RewriteState
 -> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
  -> RewriteState
  -> (Either IException Rewritten, RewriteState, RewriteWriterr))
 -> Rewrite Rewritten)
-> (RewriteReader
    -> RewriteState
    -> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->  
    let (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
rw_cs) = Rewrite Rewritten
-> RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite Rewrite Rewritten
t1 RewriteReader
ctxt RewriteState
st
    in case Either IException Rewritten
rw_res of
        Left IException
ie| IException -> Bool
failsRule IException
ie -> -- resets state 
                                 String
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall p p. p -> p -> p
trace (IException -> String
showIException IException
ie) ((Either IException Rewritten, RewriteState, RewriteWriterr)
 -> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall a b. (a -> b) -> a -> b
$ Rewrite Rewritten
-> RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite (do
                                  Rewrite ()
count_backtrack_in
                                  Counters -> Rewrite ()
addToRCounter (RewriteWriterr -> Counters
counters RewriteWriterr
rw_cs)
                                  [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' (IException
ieIException -> [IException] -> [IException]
forall a. a -> [a] -> [a]
:[IException]
errs) [Rewrite Rewritten]
ts) RewriteReader
ctxt RewriteState
st 
        Either IException Rewritten
_                     -> (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
rw_cs)

---------------------------------------------------------------------------
data MSOSReader m = MSOSReader{ MSOSReader m -> RewriteReader
ereader :: RewriteReader 
                              , MSOSReader m -> Inherited
inh_entities :: Inherited
                              , MSOSReader m -> DownControl
dctrl_entities :: DownControl
                              , MSOSReader m -> Text -> m Funcons
def_fread :: Name -> m Funcons}
data MSOSWriter = MSOSWriter { MSOSWriter -> DownControl
ctrl_entities :: Control, MSOSWriter -> Inherited
out_entities :: Output
                             , MSOSWriter -> RewriteWriterr
ewriter :: RewriteWriterr }
data MSOSState m = MSOSState { MSOSState m -> Input m
inp_es :: Input m, MSOSState m -> Mutable
mut_entities :: Mutable
                             , MSOSState m -> RewriteState
estate :: RewriteState }
emptyMSOSState :: MSOSState m
emptyMSOSState :: MSOSState m
emptyMSOSState = Input m -> Mutable -> RewriteState -> MSOSState m
forall (m :: * -> *).
Input m -> Mutable -> RewriteState -> MSOSState m
MSOSState Input m
forall k a. Map k a
M.empty Mutable
forall k a. Map k a
M.empty RewriteState
emptyRewriteState

-- | 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 { MSOS a
-> forall (m :: * -> *).
   Interactive m =>
   MSOSReader m
   -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS :: 
                        forall m. Interactive m => 
                        (MSOSReader m -> MSOSState m 
                        -> m (Either IException a, MSOSState m, MSOSWriter)) }

instance Applicative MSOS where
  pure :: a -> MSOS a
pure = a -> MSOS a
forall (m :: * -> *) a. Monad m => a -> m a
return
  <*> :: MSOS (a -> b) -> MSOS a -> MSOS b
(<*>) = MSOS (a -> b) -> MSOS a -> MSOS b
forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap

instance Functor MSOS where
  fmap :: (a -> b) -> MSOS a -> MSOS b
fmap = (a -> b) -> MSOS a -> MSOS b
forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM

instance Monad MSOS  where
  return :: a -> MSOS a
return a
a = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS (\MSOSReader m
_ MSOSState m
mut -> (Either IException a, MSOSState m, MSOSWriter)
-> m (Either IException a, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (a -> Either IException a
forall a b. b -> Either a b
Right a
a,MSOSState m
mut,MSOSWriter
forall a. Monoid a => a
mempty))

  (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f) >>= :: MSOS a -> (a -> MSOS b) -> MSOS b
>>= a -> MSOS b
k = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter))
-> MSOS b
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS (\MSOSReader m
ctxt MSOSState m
mut -> do
                    res1 :: (Either IException a, MSOSState m, MSOSWriter)
res1@(Either IException a
e_a1,MSOSState m
mut1,MSOSWriter
wr1) <- MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f MSOSReader m
ctxt MSOSState m
mut 
                    case Either IException a
e_a1 of 
                      Left IException
err  -> (Either IException b, MSOSState m, MSOSWriter)
-> m (Either IException b, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (IException -> Either IException b
forall a b. a -> Either a b
Left IException
err, MSOSState m
mut1, MSOSWriter
wr1)
                      Right a
a1  -> do   
                            let (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter)
h) = a -> MSOS b
k a
a1
                            (Either IException b
a2,MSOSState m
mut2,MSOSWriter
wr2) <- MSOSReader m
-> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter)
h MSOSReader m
ctxt MSOSState m
mut1
                            (Either IException b, MSOSState m, MSOSWriter)
-> m (Either IException b, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException b
a2,MSOSState m
mut2,MSOSWriter
wr1 MSOSWriter -> MSOSWriter -> MSOSWriter
forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr2))

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

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

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

-- | A map storing the values of /mutable/ entities.
type Mutable      = M.Map Name Values

stepRules :: [IException] -> [MSOS StepRes] -> MSOS StepRes
stepRules = ([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
NoMoreBranches Rewrite ()
count_backtrack_in

stepARules :: ([IException] -> IE) -> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules :: ([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
fexc Rewrite ()
_ [IException]
errs [] = IE -> MSOS StepRes
forall b. IE -> MSOS b
msos_throw ([IException] -> IE
fexc [IException]
errs)
stepARules [IException] -> IE
fexc Rewrite ()
counter [IException]
errs (MSOS StepRes
t1:[MSOS StepRes]
ts) = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m
 -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
  Interactive m =>
  MSOSReader m
  -> MSOSState m
  -> m (Either IException StepRes, MSOSState m, MSOSWriter))
 -> MSOS StepRes)
-> (forall (m :: * -> *).
    Interactive m =>
    MSOSReader m
    -> MSOSState m
    -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> do 
    (Either IException StepRes
e_ie_a, MSOSState m
mut', MSOSWriter
wr) <- MSOS StepRes
-> MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall a.
MSOS a
-> forall (m :: * -> *).
   Interactive m =>
   MSOSReader m
   -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS MSOS StepRes
t1 MSOSReader m
ctxt MSOSState m
mut 
    case Either IException StepRes
e_ie_a of
        Left IException
ie | IException -> Bool
failsRule IException
ie -> -- resets input & read/write entities
                                  String
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall p p. p -> p -> p
trace (IException -> String
showIException IException
ie) (m (Either IException StepRes, MSOSState m, MSOSWriter)
 -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall a b. (a -> b) -> a -> b
$ MSOS StepRes
-> MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall a.
MSOS a
-> forall (m :: * -> *).
   Interactive m =>
   MSOSReader m
   -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS (do
                                    Rewrite () -> MSOS ()
forall a. Rewrite a -> MSOS a
liftRewrite Rewrite ()
counter
                                    Counters -> MSOS ()
addToCounter (RewriteWriterr -> Counters
counters (MSOSWriter -> RewriteWriterr
ewriter MSOSWriter
wr))
                                    ([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
fexc Rewrite ()
counter ([IException]
errs[IException] -> [IException] -> [IException]
forall a. [a] -> [a] -> [a]
++[IException
ie]) [MSOS StepRes]
ts) MSOSReader m
ctxt MSOSState m
mut
        Either IException StepRes
_                      -> (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_ie_a, MSOSState m
mut', MSOSWriter
wr)

-- | 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 RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
rw_rules):[Rewrite Rewritten]
rest) [MSOS StepRes]
msoss = (RewriteReader
 -> RewriteState
 -> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
  -> RewriteState
  -> (Either IException Rewritten, RewriteState, RewriteWriterr))
 -> Rewrite Rewritten)
-> (RewriteReader
    -> RewriteState
    -> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> 
    let (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
wo) = RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
rw_rules RewriteReader
ctxt RewriteState
st
    in case Either IException Rewritten
rw_res of
        Left IException
ie | IException -> Bool
failsRule IException
ie  -> --resets counters and state 
                                   String
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall p p. p -> p -> p
trace (IException -> String
showIException IException
ie) ((Either IException Rewritten, RewriteState, RewriteWriterr)
 -> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall a b. (a -> b) -> a -> b
$ Rewrite Rewritten
-> RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite (do
                                      Rewrite ()
count_backtrack_out
                                      Counters -> Rewrite ()
addToRCounter (RewriteWriterr -> Counters
counters RewriteWriterr
wo)
                                      [IException]
-> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules' (IException
ieIException -> [IException] -> [IException]
forall a. a -> [a] -> [a]
:[IException]
errs) [Rewrite Rewritten]
rest [MSOS StepRes]
msoss) RewriteReader
ctxt RewriteState
st
        Either IException Rewritten
_                       -> (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
wo)

msos_throw :: IE -> MSOS b
msos_throw :: IE -> MSOS b
msos_throw = Rewrite b -> MSOS b
forall a. Rewrite a -> MSOS a
liftRewrite (Rewrite b -> MSOS b) -> (IE -> Rewrite b) -> IE -> MSOS b
forall b c a. (b -> c) -> (a -> b) -> a -> c
. IE -> Rewrite b
forall a. IE -> Rewrite a
rewrite_throw 

---
giveOpts :: MSOS RunOptions 
giveOpts :: MSOS RunOptions
giveOpts = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m
 -> m (Either IException RunOptions, MSOSState m, MSOSWriter))
-> MSOS RunOptions
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
  Interactive m =>
  MSOSReader m
  -> MSOSState m
  -> m (Either IException RunOptions, MSOSState m, MSOSWriter))
 -> MSOS RunOptions)
-> (forall (m :: * -> *).
    Interactive m =>
    MSOSReader m
    -> MSOSState m
    -> m (Either IException RunOptions, MSOSState m, MSOSWriter))
-> MSOS RunOptions
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> 
    (Either IException RunOptions, MSOSState m, MSOSWriter)
-> m (Either IException RunOptions, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (RunOptions -> Either IException RunOptions
forall a b. b -> Either a b
Right (RewriteReader -> RunOptions
run_opts (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt)), MSOSState m
mut, MSOSWriter
forall a. Monoid a => a
mempty)

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

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

doRefocus :: MSOS Bool
doRefocus :: MSOS Bool
doRefocus = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m
 -> m (Either IException Bool, MSOSState m, MSOSWriter))
-> MSOS Bool
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
  Interactive m =>
  MSOSReader m
  -> MSOSState m
  -> m (Either IException Bool, MSOSState m, MSOSWriter))
 -> MSOS Bool)
-> (forall (m :: * -> *).
    Interactive m =>
    MSOSReader m
    -> MSOSState m
    -> m (Either IException Bool, MSOSState m, MSOSWriter))
-> MSOS Bool
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> 
    (Either IException Bool, MSOSState m, MSOSWriter)
-> m (Either IException Bool, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Bool -> Either IException Bool
forall a b. b -> Either a b
Right (Bool -> Either IException Bool) -> Bool -> Either IException Bool
forall a b. (a -> b) -> a -> b
$ RunOptions -> Bool
do_refocus (RewriteReader -> RunOptions
run_opts (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt)), MSOSState m
mut, MSOSWriter
forall a. Monoid a => a
mempty)

modifyRewriteCTXT :: (RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT :: (RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT RewriteReader -> RewriteReader
mod (Rewrite RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f) = (RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f (RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> (RewriteReader -> RewriteReader)
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteReader -> RewriteReader
mod)

modifyRewriteReader :: (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader :: (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader RewriteReader -> RewriteReader
mod (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f) = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS (MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f (MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> (MSOSReader m -> MSOSReader m)
-> MSOSReader m
-> MSOSState m
-> m (Either IException a, MSOSState m, MSOSWriter)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MSOSReader m -> MSOSReader m
forall (m :: * -> *). MSOSReader m -> MSOSReader m
mod')
  where mod' :: MSOSReader m -> MSOSReader m
mod' MSOSReader m
ctxt = MSOSReader m
ctxt { ereader :: RewriteReader
ereader = RewriteReader -> RewriteReader
mod (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) }
-----------------
-- | a map storing the values of /inherited/ entities.
type Inherited       = M.Map Name [Values]

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

      
----------
-- | a map storing the values of /control/ entities.
type Control = M.Map Name (Maybe Values)
type DownControl = M.Map Name (Maybe Values)

emptyDCTRL :: DownControl
emptyDCTRL :: DownControl
emptyDCTRL = DownControl
forall k a. Map k a
M.empty

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

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

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

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

unionOUT :: Output -> Output -> Output
unionOUT :: Inherited -> Inherited -> Inherited
unionOUT = ([Values Funcons] -> [Values Funcons] -> [Values Funcons])
-> Inherited -> Inherited -> Inherited
forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith [Values Funcons] -> [Values Funcons] -> [Values Funcons]
forall a. [a] -> [a] -> [a]
(++)

emptyOUT :: Output 
emptyOUT :: Inherited
emptyOUT = Inherited
forall k a. Map k a
M.empty 

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

instance Monoid Counters where
    mempty :: Counters
mempty = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0
    (Counters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8) mappend :: Counters -> Counters -> Counters
`mappend` (Counters Int
y1 Int
y2 Int
y3 Int
y4 Int
y5 Int
y6 Int
y7 Int
y8) = 
        Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters (Int
x1Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y1) (Int
x2Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y2) (Int
x3Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y3) (Int
x4Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y4) (Int
x5Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y5) (Int
x6Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y6) (Int
x7Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y7) (Int
x8Int -> Int -> Int
forall a. Num a => a -> a -> a
+Int
y8)

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

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

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

count_step :: MSOS ()
count_step :: MSOS ()
count_step = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m
 -> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
  Interactive m =>
  MSOSReader m
  -> MSOSState m
  -> m (Either IException (), MSOSState m, MSOSWriter))
 -> MSOS ())
-> (forall (m :: * -> *).
    Interactive m =>
    MSOSReader m
    -> MSOSState m
    -> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> (Either IException (), MSOSState m, MSOSWriter)
-> m (Either IException (), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Either IException ()
forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
1 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0)

count_delegation :: MSOS ()
count_delegation :: MSOS ()
count_delegation = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m
 -> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
  Interactive m =>
  MSOSReader m
  -> MSOSState m
  -> m (Either IException (), MSOSState m, MSOSWriter))
 -> MSOS ())
-> (forall (m :: * -> *).
    Interactive m =>
    MSOSReader m
    -> MSOSState m
    -> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> (Either IException (), MSOSState m, MSOSWriter)
-> m (Either IException (), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Either IException ()
forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
0 Int
0 Int
0 Int
0 Int
0 Int
1 Int
0 Int
0)

count_refocus :: MSOS ()
count_refocus = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m
 -> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
  Interactive m =>
  MSOSReader m
  -> MSOSState m
  -> m (Either IException (), MSOSState m, MSOSWriter))
 -> MSOS ())
-> (forall (m :: * -> *).
    Interactive m =>
    MSOSReader m
    -> MSOSState m
    -> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> (Either IException (), MSOSState m, MSOSWriter)
-> m (Either IException (), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Either IException ()
forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
0 Int
0 Int
0 Int
0 Int
1 Int
0 Int
0 Int
0)

count_restart :: MSOS ()
count_restart :: MSOS ()
count_restart = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m
 -> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
  Interactive m =>
  MSOSReader m
  -> MSOSState m
  -> m (Either IException (), MSOSState m, MSOSWriter))
 -> MSOS ())
-> (forall (m :: * -> *).
    Interactive m =>
    MSOSReader m
    -> MSOSState m
    -> m (Either IException (), MSOSState m, MSOSWriter))
-> MSOS ()
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> (Either IException (), MSOSState m, MSOSWriter)
-> m (Either IException (), MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (() -> Either IException ()
forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
0 Int
0 Int
0 Int
1 Int
0 Int
0 Int
0 Int
0)

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

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

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

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

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

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

-- | 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 :: Funcons -> Rewrite a
norule Funcons
f = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw ([IException] -> IE
NoRule [])

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

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

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

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

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

buildStepCount :: MSOS StepRes -> Rewrite Rewritten
buildStepCount :: MSOS StepRes -> Rewrite Rewritten
buildStepCount = MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter MSOS ()
count_delegation

buildStepCounter :: MSOS () -> MSOS StepRes -> Rewrite Rewritten 
buildStepCounter :: MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter MSOS ()
counter MSOS StepRes
mf = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS ()
counter MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes
mf)

optRefocus :: MSOS StepRes -> MSOS StepRes
optRefocus :: MSOS StepRes -> MSOS StepRes
optRefocus MSOS StepRes
stepper = MSOS Bool
doRefocus MSOS Bool -> (Bool -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                        Bool
True    -> MSOS StepRes -> MSOS StepRes
refocus MSOS StepRes
stepper 
                        Bool
False   -> MSOS StepRes
stepper 

refocus :: MSOS StepRes -> MSOS StepRes
refocus :: MSOS StepRes -> MSOS StepRes
refocus MSOS StepRes
stepper -- stop refocussing when a signal has been raised
                = MSOS ()
count_refocus MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_violates_refocus MSOS StepRes
stepper StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return StepRes -> MSOS StepRes
continue
    where continue :: StepRes -> MSOS StepRes
continue = \case
            Right [Values Funcons]
vs  -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values Funcons] -> StepRes
forall a b. b -> Either a b
Right [Values Funcons]
vs)
            Left Funcons
f    -> 
              Rewrite Rewritten -> MSOS Rewritten
forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) MSOS Rewritten -> (Rewritten -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values Funcons
v] -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values Funcons] -> StepRes
forall a b. b -> Either a b
Right [Values Funcons
v])
                ValTerm [Values Funcons]
vs  -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return (Funcons -> StepRes
forall a b. a -> Either a b
Left Funcons
f) -- undo rewrites and accept last step
                Rewritten
res         -> MSOS StepRes -> MSOS StepRes
refocus (MSOS StepRes -> MSOS StepRes) -> MSOS StepRes -> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ Rewritten -> MSOS StepRes
stepRewritten Rewritten
res

stepRewritten :: Rewritten -> MSOS StepRes 
stepRewritten :: Rewritten -> MSOS StepRes
stepRewritten (ValTerm [Values Funcons]
vs) = StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values Funcons] -> StepRes
forall a b. b -> Either a b
Right [Values Funcons]
vs)
stepRewritten (CompTerm Funcons
f MSOS StepRes
step) = (RewriteReader -> RewriteReader) -> MSOS StepRes -> MSOS StepRes
forall a. (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader RewriteReader -> RewriteReader
mod (MSOS ()
count_step MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes
step)
  where mod :: RewriteReader -> RewriteReader
mod RewriteReader
ctxt = RewriteReader
ctxt {local_fct :: Funcons
local_fct = Funcons
f}

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

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

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

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

-- | Yield a funcon term as the result of an 'MSOS' computation.
-- This function must be used instead of @return@. 
stepTo :: Funcons -> MSOS StepRes 
stepTo :: Funcons -> MSOS StepRes
stepTo = StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return (StepRes -> MSOS StepRes)
-> (Funcons -> StepRes) -> Funcons -> MSOS StepRes
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Funcons -> StepRes
forall a b. a -> Either a b
Left

-- | Yield a sequence of funcon terms as the result of a computation.
-- This is only valid when all terms rewrite to a value
stepSeqTo :: [Funcons] -> MSOS StepRes
stepSeqTo :: [Funcons] -> MSOS StepRes
stepSeqTo [Funcons]
fs = [Values Funcons] -> StepRes
forall a b. b -> Either a b
Right ([Values Funcons] -> StepRes)
-> MSOS [Values Funcons] -> MSOS StepRes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> Rewrite [Values Funcons] -> MSOS [Values Funcons]
forall a. Rewrite a -> MSOS a
liftRewrite ([Funcons] -> Rewrite [Values Funcons]
rewriteStrictSequence [Funcons]
fs)

if_abruptly_terminates :: Bool -> MSOS StepRes -> (StepRes -> MSOS StepRes)
                            -> (StepRes -> MSOS StepRes) -> MSOS StepRes
if_abruptly_terminates :: Bool
-> MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_abruptly_terminates Bool
care (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep) StepRes -> MSOS StepRes
abr StepRes -> MSOS StepRes
no_abr = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m
 -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
  Interactive m =>
  MSOSReader m
  -> MSOSState m
  -> m (Either IException StepRes, MSOSState m, MSOSWriter))
 -> MSOS StepRes)
-> (forall (m :: * -> *).
    Interactive m =>
    MSOSReader m
    -> MSOSState m
    -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
    MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut m (Either IException StepRes, MSOSState m, MSOSWriter)
-> ((Either IException StepRes, MSOSState m, MSOSWriter)
    -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        (Right StepRes
f', MSOSState m
mut', MSOSWriter
wr') ->
            let failed :: Bool
failed     = (Maybe (Values Funcons) -> Bool) -> DownControl -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe (Values Funcons) -> Bool
forall a. Maybe a -> Bool
isJust (MSOSWriter -> DownControl
ctrl_entities MSOSWriter
wr')
                MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep | Bool
failed Bool -> Bool -> Bool
&& Bool
care = StepRes -> MSOS StepRes
abr StepRes
f'
                           | Bool
otherwise      = StepRes -> MSOS StepRes
no_abr StepRes
f'
            in do (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr'') <- MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut'
                  (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr' MSOSWriter -> MSOSWriter -> MSOSWriter
forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr'')
        (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res -> (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res

-- TODO is input test accurate? 
-- TODO We should also find changes to mutable entities
if_violates_refocus :: MSOS StepRes -> (StepRes -> MSOS StepRes)
                            -> (StepRes -> MSOS StepRes) -> MSOS StepRes
if_violates_refocus :: MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_violates_refocus (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep) StepRes -> MSOS StepRes
viol StepRes -> MSOS StepRes
no_viol = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m
 -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
  Interactive m =>
  MSOSReader m
  -> MSOSState m
  -> m (Either IException StepRes, MSOSState m, MSOSWriter))
 -> MSOS StepRes)
-> (forall (m :: * -> *).
    Interactive m =>
    MSOSReader m
    -> MSOSState m
    -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
    MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut m (Either IException StepRes, MSOSState m, MSOSWriter)
-> ((Either IException StepRes, MSOSState m, MSOSWriter)
    -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
        (Right StepRes
f', MSOSState m
mut', MSOSWriter
wr') ->
            let violates :: Bool
violates = (Maybe (Values Funcons) -> Bool) -> DownControl -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any Maybe (Values Funcons) -> Bool
forall a. Maybe a -> Bool
isJust (MSOSWriter -> DownControl
ctrl_entities MSOSWriter
wr')
                            Bool -> Bool -> Bool
|| ([Values Funcons] -> Bool) -> Inherited -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not (Bool -> Bool)
-> ([Values Funcons] -> Bool) -> [Values Funcons] -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (MSOSWriter -> Inherited
out_entities MSOSWriter
wr')
                            Bool -> Bool -> Bool
|| (([[Values Funcons]], Maybe (m Funcons)) -> Bool)
-> Map Text ([[Values Funcons]], Maybe (m Funcons)) -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Maybe (m Funcons) -> Bool
forall a. Maybe a -> Bool
isNothing (Maybe (m Funcons) -> Bool)
-> (([[Values Funcons]], Maybe (m Funcons)) -> Maybe (m Funcons))
-> ([[Values Funcons]], Maybe (m Funcons))
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ([[Values Funcons]], Maybe (m Funcons)) -> Maybe (m Funcons)
forall a b. (a, b) -> b
snd) (MSOSState m -> Map Text ([[Values Funcons]], Maybe (m Funcons))
forall (m :: * -> *). MSOSState m -> Input m
inp_es MSOSState m
mut')
--                            || any isJust (dctrl_entities ctxt)
                MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep | Bool
violates    = StepRes -> MSOS StepRes
viol StepRes
f'
                           | Bool
otherwise   = StepRes -> MSOS StepRes
no_viol StepRes
f'
            in do (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr'') <- MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut'
                  (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr' MSOSWriter -> MSOSWriter -> MSOSWriter
forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr'')
        (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res -> (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res

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

-- | Execute a computational step as a /premise/.
-- The result of the step is the returned funcon term. 
premiseStepApp :: (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp :: (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp StepRes -> StepRes
app Funcons
f = Rewrite Rewritten -> MSOS Rewritten
forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) MSOS Rewritten -> (Rewritten -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ValTerm [Values Funcons]
vs      -> IE -> MSOS StepRes
forall b. IE -> MSOS b
msos_throw ([Values Funcons] -> IE
StepOnValue [Values Funcons]
vs)
    CompTerm Funcons
_ MSOS StepRes
step -> StepRes -> StepRes
app (StepRes -> StepRes) -> MSOS StepRes -> MSOS StepRes
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSOS ()
count_delegation MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes -> MSOS StepRes
optRefocus MSOS StepRes
step)

premiseStep :: Funcons -> MSOS StepRes 
premiseStep :: Funcons -> MSOS StepRes
premiseStep = (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp StepRes -> StepRes
forall a. a -> a
id 

----- main `step` function
evalFuncons :: Funcons -> MSOS StepRes 
evalFuncons :: Funcons -> MSOS StepRes
evalFuncons Funcons
f = Rewrite Rewritten -> MSOS Rewritten
forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) MSOS Rewritten -> (Rewritten -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rewritten -> MSOS StepRes
stepRewritten

rewritesToType :: Funcons -> Rewrite Types
rewritesToType :: Funcons -> Rewrite Types
rewritesToType Funcons
f = do
  Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f Rewrite Rewritten -> (Rewritten -> Rewrite Types) -> Rewrite Types
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
    ValTerm [v :: Values Funcons
v@(ComputationType ComputationTypes Funcons
_)] -> Types -> Rewrite Types
forall (m :: * -> *) a. Monad m => a -> m a
return (Values Funcons -> Types
forall t. Values t -> Types t
downcastValueType Values Funcons
v)
    Rewritten
_                               -> Rewrite Types
forall a. Rewrite a
rewriteToValErr

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

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

rewriteToValErr :: Rewrite a
rewriteToValErr = IE -> Rewrite a
forall a. IE -> Rewrite a
rewrite_throw (IE -> Rewrite a) -> IE -> Rewrite a
forall a b. (a -> b) -> a -> b
$ 
  String -> IE
SideCondFail String
"side-condition/entity-value/annotation evaluation requires step"

rewriteFunconsWcount :: Funcons -> Rewrite Rewritten
rewriteFunconsWcount :: Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f = Rewrite ()
count_rewrite_attempt Rewrite () -> Rewrite Rewritten -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f

rewriteFuncons :: Funcons -> Rewrite Rewritten 
rewriteFuncons :: Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f = (RewriteReader -> RewriteReader)
-> Rewrite Rewritten -> Rewrite Rewritten
forall a.
(RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT (\RewriteReader
ctxt -> RewriteReader
ctxt{local_fct :: Funcons
local_fct = Funcons
f}) (Funcons -> Rewrite Rewritten
rewriteFuncons' Funcons
f)
 where
    rewriteFuncons' :: Funcons -> Rewrite Rewritten
rewriteFuncons' (FValue Values Funcons
v)   = Rewritten -> Rewrite Rewritten
forall (m :: * -> *) a. Monad m => a -> m a
return ([Values Funcons] -> Rewritten
ValTerm [Values Funcons
v]) 
{-    rewriteFuncons' (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 Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> ([Values Funcons] -> Values Funcons) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Values Funcons
setval_) [Funcons] -> Funcons
FSet
    rewriteFuncons' (FMap [Funcons]
fs)    = [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
fs (Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> ([Values Funcons] -> Values Funcons) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Values Funcons
mapval_) [Funcons] -> Funcons
FMap
    rewriteFuncons' f :: Funcons
f@(FBinding Funcons
fk [Funcons]
fv) = [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence (Funcons
fkFuncons -> [Funcons] -> [Funcons]
forall a. a -> [a] -> [a]
:[Funcons]
fv) (Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> ([Values Funcons] -> Values Funcons) -> ValueOp
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values Funcons] -> Values Funcons
forall t. HasValues t => [Values t] -> Values t
tuple) [Funcons] -> Funcons
mkBinding 
      where mkBinding :: [Funcons] -> Funcons
mkBinding (Funcons
k:[Funcons]
fvs) = Funcons -> [Funcons] -> Funcons
FBinding Funcons
k [Funcons]
fvs
            mkBinding [Funcons]
_       = String -> Funcons
forall a. HasCallStack => String -> a
error String
"invalid binding-notation"
    rewriteFuncons' f :: Funcons
f@(FSortPower Funcons
s1 Funcons
fn) = case (Funcons
s1,Funcons
fn) of 
      (FValue mty :: Values Funcons
mty@(ComputationType ComputationTypes Funcons
_), FValue Values Funcons
v) 
        | Nat Integer
n <- Values Funcons -> Values Funcons
forall t. Values t -> Values t
upcastNaturals Values Funcons
v -> 
                  ValueOp
rewrittens (Int -> Values Funcons -> [Values Funcons]
forall a. Int -> a -> [a]
replicate (Integer -> Int
forall a. Num a => Integer -> a
fromInteger Integer
n) (ComputationTypes Funcons -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType (Types -> ComputationTypes Funcons
forall t. Types t -> ComputationTypes t
Type (Values Funcons -> Types
forall t. Values t -> Types t
downcastValueType Values Funcons
mty))))
      (FValue Values Funcons
mty, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
fn Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
            ValTerm [Values Funcons
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortPower Funcons
s1 (Values Funcons -> Funcons
FValue Values Funcons
v)
            ValTerm [Values Funcons]
_   -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f String
"second operand of ^ cannot compute a sequence"
            CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortPower Funcons
s1) MSOS StepRes
mf
                where ie :: IE
ie = String -> IE
SortErr String
"^_ multiadic argument" 
      (Funcons, Funcons)
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values Funcons
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortPower (Values Funcons -> Funcons
FValue Values Funcons
v) Funcons
fn
            ValTerm [Values Funcons]
_   -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr Funcons
f String
"first operand of ^ cannot compute a sequence"
            CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie ((Funcons -> Funcons -> Funcons) -> Funcons -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortPower Funcons
fn) MSOS StepRes
mf
              where ie :: IE
ie = String -> IE
SortErr String
"_^ multiadic argument"
    rewriteFuncons' f :: Funcons
f@(FSortSeq Funcons
s1 SeqSortOp
op)     = case Funcons
s1 of 
      (FValue (ComputationType (Type Types
ty))) -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ComputationTypes Funcons -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType (ComputationTypes Funcons -> Values Funcons)
-> ComputationTypes Funcons -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Types -> ComputationTypes Funcons
forall t. Types t -> ComputationTypes t
Type (Types -> ComputationTypes Funcons)
-> Types -> ComputationTypes Funcons
forall a b. (a -> b) -> a -> b
$ Types -> SeqSortOp -> Types
forall t. Types t -> SeqSortOp -> Types t
AnnotatedType Types
ty SeqSortOp
op
      (FValue Values Funcons
_) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> SeqSortOp -> Funcons
FSortSeq Funcons
s1 SeqSortOp
op) String
"sort-sequence operator not on type"
      Funcons
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values Funcons
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> SeqSortOp -> Funcons
FSortSeq (Values Funcons -> Funcons
FValue Values Funcons
v1) SeqSortOp
op
            ValTerm [Values Funcons]
vs   -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> SeqSortOp -> Funcons
FSortSeq Funcons
s1 SeqSortOp
op) String
"operand of sort-sequence operator cannot compute a sequence"
            CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie ((Funcons -> SeqSortOp -> Funcons)
-> SeqSortOp -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> SeqSortOp -> Funcons
FSortSeq SeqSortOp
op) MSOS StepRes
mf
              where ie :: IE
ie = String -> IE
SortErr String
"sort-sequence operator, multiadic argument"
    rewriteFuncons' (FSortComputes Funcons
f1) = case Funcons
f1 of
        (FValue (ComputationType (Type Types
ty))) -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ComputationTypes Funcons -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType (ComputationTypes Funcons -> Values Funcons)
-> ComputationTypes Funcons -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Types -> ComputationTypes Funcons
forall t. Types t -> ComputationTypes t
ComputesType Types
ty
        (FValue Values Funcons
_) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons
FSortComputes Funcons
f1) String
"=> not applied to a type"
        Funcons
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values Funcons
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
FSortComputes (Values Funcons -> Funcons
FValue Values Funcons
v1)
                ValTerm [Values Funcons]
vs   -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons
FSortComputes Funcons
f1) String
"operand of => cannot compute a sequence"
                CompTerm Funcons
_ MSOS StepRes
mf    -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie Funcons -> Funcons
FSortComputes MSOS StepRes
mf
                  where ie :: IE
ie = String -> IE
SortErr String
"=>_ multiadic argument"
    rewriteFuncons' (FSortComputesFrom Funcons
f1 Funcons
f2) = case (Funcons
f1,Funcons
f2) of
        (FValue (ComputationType (Type Types
ty1)),FValue (ComputationType (Type Types
ty2))) 
            -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ComputationTypes Funcons -> Values Funcons
forall t. ComputationTypes t -> Values t
ComputationType (Types -> Types -> ComputationTypes Funcons
forall t. Types t -> Types t -> ComputationTypes t
ComputesFromType Types
ty1 Types
ty2)
        (FValue Values Funcons
_, FValue Values Funcons
_) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) String
"=> not applied to types"
        (FValue (ComputationType (Type Types
ty1)),Funcons
_) 
            -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f2 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values Funcons
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 (Values Funcons -> Funcons
FValue Values Funcons
v2)
                ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) String
"second operand of => cannot compute a sequence"
                CompTerm Funcons
_ MSOS StepRes
mf    -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1) MSOS StepRes
mf
                  where ie :: IE
ie = String -> IE
SortErr String
"_=>_ multiadic operand (2)"
        (Funcons
_,Funcons
_) 
            -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values Funcons
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortComputesFrom (Values Funcons -> Funcons
FValue Values Funcons
v1) Funcons
f2
                ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) String
"_=>_ multiadic operand (1)"
                CompTerm Funcons
_ MSOS StepRes
mf    -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie ((Funcons -> Funcons -> Funcons) -> Funcons -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f2) MSOS StepRes
mf
                  where ie :: IE
ie = String -> IE
SortErr String
"_=>_ multiadic operand (1)"
    rewriteFuncons' (FSortUnion Funcons
s1 Funcons
s2)   = case (Funcons
s1, Funcons
s2) of
        (FValue (ComputationType (Type Types
t1))
            , FValue (ComputationType (Type Types
t2))) -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values Funcons
typeVal (Types -> Values Funcons) -> Types -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Types -> Types -> Types
forall t. Types t -> Types t -> Types t
Union Types
t1 Types
t2
        (FValue Values Funcons
_, FValue Values Funcons
_) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) String
"sort-union not applied to two sorts"
        (FValue Values Funcons
v1, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s2 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values Funcons
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 (Values Funcons -> Funcons
FValue Values Funcons
v2)
            ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) String
"sort-union multiadic argument (2)"
            CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1) MSOS StepRes
mf
              where ie :: IE
ie = String -> IE
SortErr String
"sort-union multiadic argument (2)"
        (Funcons, Funcons)
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values Funcons
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortUnion (Values Funcons -> Funcons
FValue Values Funcons
v) Funcons
s2
                ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) String
"sort-union multiadic argument (1)"
                CompTerm Funcons
_ MSOS StepRes
mf   -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie ((Funcons -> Funcons -> Funcons) -> Funcons -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortUnion Funcons
s2) MSOS StepRes
mf
                  where ie :: IE
ie = String -> IE
SortErr String
"sort-union multiadic argument (1)"
    rewriteFuncons' (FSortInter Funcons
s1 Funcons
s2)   = case (Funcons
s1, Funcons
s2) of
        (FValue (ComputationType (Type Types
t1))
            , FValue (ComputationType (Type Types
t2))) -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values Funcons
typeVal (Types -> Values Funcons) -> Types -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Types -> Types -> Types
forall t. Types t -> Types t -> Types t
Intersection Types
t1 Types
t2
        (FValue Values Funcons
_, FValue Values Funcons
_) -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) String
"sort-intersection not applied to two sorts"
        (FValue Values Funcons
v1, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s2 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
            ValTerm [Values Funcons
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 (Values Funcons -> Funcons
FValue Values Funcons
v2)
            ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) String
"sort-intersection multiadic argument (2)" 
            CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1) MSOS StepRes
mf
              where ie :: IE
ie = String -> IE
SortErr String
"sort-intersection multiadic argument (2)"
        (Funcons, Funcons)
_ -> do Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                    ValTerm [Values Funcons
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortInter (Values Funcons -> Funcons
FValue Values Funcons
v1) Funcons
s2
                    ValTerm [Values Funcons]
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) String
"sort-intersection multiadic argument (1)" 
                    CompTerm Funcons
_ MSOS StepRes
mf   -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie ((Funcons -> Funcons -> Funcons) -> Funcons -> Funcons -> Funcons
forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortInter Funcons
s2) MSOS StepRes
mf
                      where ie :: IE
ie = String -> IE
SortErr String
"sort-intersection multiadic argument (1)"
    rewriteFuncons' (FSortComplement Funcons
s1) = case Funcons
s1 of 
      FValue (ComputationType (Type Types
t1)) -> Values Funcons -> Rewrite Rewritten
rewritten (Values Funcons -> Rewrite Rewritten)
-> Values Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Types -> Values Funcons
typeVal (Types -> Values Funcons) -> Types -> Values Funcons
forall a b. (a -> b) -> a -> b
$ Types -> Types
forall t. Types t -> Types t
Complement Types
t1
      FValue Values Funcons
_ -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons
FSortComplement Funcons
s1) String
"sort-complement not applied to a sort" 
      Funcons
_ -> do Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 Rewrite Rewritten
-> (Rewritten -> Rewrite Rewritten) -> Rewrite Rewritten
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
                ValTerm [Values Funcons
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons (Funcons -> Rewrite Rewritten) -> Funcons -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
FSortComplement (Values Funcons -> Funcons
FValue Values Funcons
v)
                ValTerm [Values Funcons]
vs -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
sortErr (Funcons -> Funcons
FSortComplement Funcons
s1) String
"sort-complement multiadic argument"
                CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie Funcons -> Funcons
FSortComplement MSOS StepRes
mf
                  where ie :: IE
ie = String -> IE
SortErr String
"sort-complement multiadic argument"
    rewriteFuncons' (FName Text
nm) = 
        do  EvalFunction
mystepf <- Text -> Rewrite EvalFunction
lookupFuncon Text
nm 
            case EvalFunction
mystepf of 
                NullaryFuncon Rewrite Rewritten
mystep -> Rewrite Rewritten
mystep
                StrictFuncon ValueOp
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons' (Text -> [Funcons] -> Funcons
FApp Text
nm [])
                ValueOp ValueOp
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons' (Text -> [Funcons] -> Funcons
FApp Text
nm [])
                EvalFunction
_ -> String -> Rewrite Rewritten
forall a. HasCallStack => String -> a
error (String
"funcon " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
unpack Text
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" not applied to any arguments")
    rewriteFuncons' (FApp Text
nm [Funcons]
arg)    = 
        do  EvalFunction
mystepf <- Text -> Rewrite EvalFunction
lookupFuncon Text
nm
            case EvalFunction
mystepf of 
                NullaryFuncon Rewrite Rewritten
_     -> Funcons -> String -> Rewrite Rewritten
forall a. Funcons -> String -> Rewrite a
exception (Text -> [Funcons] -> Funcons
FApp Text
nm [Funcons]
arg) (String
"nullary funcon " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Text -> String
unpack Text
nm String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
" applied to arguments: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ ([Funcons] -> String
showFunconsSeq [Funcons]
arg))
                ValueOp ValueOp
mystep      -> [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
arg ValueOp
mystep (Text -> [Funcons] -> Funcons
applyFuncon Text
nm)
                StrictFuncon ValueOp
mystep -> [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
arg ValueOp
mystep (Text -> [Funcons] -> Funcons
applyFuncon Text
nm)
                NonStrictFuncon [Funcons] -> Rewrite Rewritten
mystep -> [Funcons] -> Rewrite Rewritten
mystep [Funcons]
arg
                PartiallyStrictFuncon [Strictness]
strns Strictness
strn [Funcons] -> Rewrite Rewritten
mystep -> 
                  [Strictness]
-> [Funcons]
-> ([Funcons] -> Rewrite Rewritten)
-> ([Funcons] -> Funcons)
-> Rewrite Rewritten
evalSequence ([Strictness]
strns [Strictness] -> [Strictness] -> [Strictness]
forall a. [a] -> [a] -> [a]
++ Strictness -> [Strictness]
forall a. a -> [a]
repeat Strictness
strn) [Funcons]
arg [Funcons] -> Rewrite Rewritten
mystep (Text -> [Funcons] -> Funcons
applyFuncon Text
nm)

rewriteStrictSequence :: [Funcons] -> Rewrite [Values] 
rewriteStrictSequence :: [Funcons] -> Rewrite [Values Funcons]
rewriteStrictSequence [Funcons]
fs = case [Funcons]
rest of 
  []      -> [Values Funcons] -> Rewrite [Values Funcons]
forall (m :: * -> *) a. Monad m => a -> m a
return ((Funcons -> Values Funcons) -> [Funcons] -> [Values Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values Funcons
downcastValue [Funcons]
vs)
  (Funcons
x:[Funcons]
xs)  -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
x Rewrite Rewritten
-> (Rewritten -> Rewrite [Values Funcons])
-> Rewrite [Values Funcons]
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
    ValTerm [Values Funcons]
vs'    -> [Funcons] -> Rewrite [Values Funcons]
rewriteStrictSequence ([Funcons]
vs[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++(Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
vs'[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++[Funcons]
xs)
    CompTerm Funcons
f0 MSOS StepRes
mf -> String -> Rewrite [Values Funcons]
forall a. String -> Rewrite a
internal (String
"step on sequence of computations: " String -> ShowS
forall a. [a] -> [a] -> [a]
++ [Funcons] -> String
forall a. Show a => a -> String
show [Funcons]
fs)
  where ([Funcons]
vs, [Funcons]
rest) = (Funcons -> Bool) -> [Funcons] -> ([Funcons], [Funcons])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not (Bool -> Bool) -> (Funcons -> Bool) -> Funcons -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Funcons -> Bool
hasStep) [Funcons]
fs

--OPT: replace by specialised variant of evalSequence
evalStrictSequence :: [Funcons] -> ([Values] -> Rewrite Rewritten) -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence :: [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
args ValueOp
cont [Funcons] -> Funcons
cons = 
    [Strictness]
-> [Funcons]
-> ([Funcons] -> Rewrite Rewritten)
-> ([Funcons] -> Funcons)
-> Rewrite Rewritten
evalSequence (Int -> Strictness -> [Strictness]
forall a. Int -> a -> [a]
replicate ([Funcons] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Funcons]
args) Strictness
Strict) [Funcons]
args 
        (ValueOp
cont ValueOp
-> ([Funcons] -> [Values Funcons])
-> [Funcons]
-> Rewrite Rewritten
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Funcons -> Values Funcons) -> [Funcons] -> [Values Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values Funcons
downcastValue) [Funcons] -> Funcons
cons

evalSequence :: [Strictness] -> [Funcons] -> 
    ([Funcons] -> Rewrite Rewritten) -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalSequence :: [Strictness]
-> [Funcons]
-> ([Funcons] -> Rewrite Rewritten)
-> ([Funcons] -> Funcons)
-> Rewrite Rewritten
evalSequence [Strictness]
strns [Funcons]
args [Funcons] -> Rewrite Rewritten
cont [Funcons] -> Funcons
cons = 
    ([Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten)
-> ([Funcons], [(Strictness, Funcons)]) -> Rewrite Rewritten
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten
evalSeqAux (([Funcons], [(Strictness, Funcons)]) -> Rewrite Rewritten)
-> ([Funcons], [(Strictness, Funcons)]) -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ ((Strictness, Funcons) -> Funcons)
-> [(Strictness, Funcons)] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map (Strictness, Funcons) -> Funcons
forall a b. (a, b) -> b
snd ([(Strictness, Funcons)] -> [Funcons])
-> ([(Strictness, Funcons)] -> [(Strictness, Funcons)])
-> ([(Strictness, Funcons)], [(Strictness, Funcons)])
-> ([Funcons], [(Strictness, Funcons)])
forall (a :: * -> * -> *) b c b' c'.
Arrow a =>
a b c -> a b' c' -> a (b, b') (c, c')
*** [(Strictness, Funcons)] -> [(Strictness, Funcons)]
forall a. a -> a
id (([(Strictness, Funcons)], [(Strictness, Funcons)])
 -> ([Funcons], [(Strictness, Funcons)]))
-> ([(Strictness, Funcons)], [(Strictness, Funcons)])
-> ([Funcons], [(Strictness, Funcons)])
forall a b. (a -> b) -> a -> b
$ ((Strictness, Funcons) -> Bool)
-> [(Strictness, Funcons)]
-> ([(Strictness, Funcons)], [(Strictness, Funcons)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Strictness, Funcons) -> Bool
isDone ([Strictness] -> [Funcons] -> [(Strictness, Funcons)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Strictness]
strns [Funcons]
args)
 where  unmatched :: [Funcons]
unmatched = Int -> [Funcons] -> [Funcons]
forall a. Int -> [a] -> [a]
drop ([Strictness] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Strictness]
strns) [Funcons]
args
        evalSeqAux :: [Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten
        evalSeqAux :: [Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten
evalSeqAux [Funcons]
vs [] = [Funcons] -> Rewrite Rewritten
cont [Funcons]
vs
        evalSeqAux [Funcons]
vs ((Strictness
_,Funcons
f):[(Strictness, Funcons)]
fs) = ValueOp
-> (MSOS StepRes -> MSOS StepRes) -> Funcons -> Rewrite Rewritten
premiseEval ValueOp
valueCont MSOS StepRes -> MSOS StepRes
funconCont Funcons
f
         where  valueCont :: ValueOp
valueCont [Values Funcons]
vs' = do 
                    Rewrite ()
count_rewrite
                    [Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten
evalSeqAux ([Funcons]
vs[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++((Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
vs' [Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++ ((Strictness, Funcons) -> Funcons)
-> [(Strictness, Funcons)] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map (Strictness, Funcons) -> Funcons
forall a b. (a, b) -> b
snd [(Strictness, Funcons)]
othervs)) [(Strictness, Funcons)]
otherfs
                 where ([(Strictness, Funcons)]
othervs, [(Strictness, Funcons)]
otherfs) = ((Strictness, Funcons) -> Bool)
-> [(Strictness, Funcons)]
-> ([(Strictness, Funcons)], [(Strictness, Funcons)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Strictness, Funcons) -> Bool
isDone [(Strictness, Funcons)]
fs
                funconCont :: MSOS StepRes -> MSOS StepRes
funconCont MSOS StepRes
stepf = MSOS StepRes
stepf MSOS StepRes -> (StepRes -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case  
                  Left Funcons
f' -> Funcons -> MSOS StepRes
stepTo ([Funcons] -> Funcons
cons ([Funcons]
vs[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++[Funcons
f'][Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++((Strictness, Funcons) -> Funcons)
-> [(Strictness, Funcons)] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map (Strictness, Funcons) -> Funcons
forall a b. (a, b) -> b
snd [(Strictness, Funcons)]
fs))
                  Right [Values Funcons]
vs' -> Funcons -> MSOS StepRes
stepTo ([Funcons] -> Funcons
cons ([Funcons]
vs[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++((Values Funcons -> Funcons) -> [Values Funcons] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map Values Funcons -> Funcons
FValue [Values Funcons]
vs')[Funcons] -> [Funcons] -> [Funcons]
forall a. [a] -> [a] -> [a]
++((Strictness, Funcons) -> Funcons)
-> [(Strictness, Funcons)] -> [Funcons]
forall a b. (a -> b) -> [a] -> [b]
map (Strictness, Funcons) -> Funcons
forall a b. (a, b) -> b
snd [(Strictness, Funcons)]
fs))
        isDone :: (Strictness, Funcons) -> Bool
isDone (Strictness
Strict, FValue Values Funcons
_) = Bool
True
        isDone (Strictness
NonStrict, Funcons
_) = Bool
True
        isDone (Strictness, Funcons)
_ = Bool
False

-- | Yield an 'MSOS' computation as a fully rewritten term.
-- This function must be used in order to access entities in the definition
-- of funcons.
compstep :: MSOS StepRes -> Rewrite Rewritten
compstep :: MSOS StepRes -> Rewrite Rewritten
compstep MSOS StepRes
mf = (RewriteReader
 -> RewriteState
 -> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a.
(RewriteReader
 -> RewriteState
 -> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite ((RewriteReader
  -> RewriteState
  -> (Either IException Rewritten, RewriteState, RewriteWriterr))
 -> Rewrite Rewritten)
-> (RewriteReader
    -> RewriteState
    -> (Either IException Rewritten, RewriteState, RewriteWriterr))
-> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> 
    let f0 :: Funcons
f0 = RewriteReader -> Funcons
local_fct RewriteReader
ctxt 
    in (Rewritten -> Either IException Rewritten
forall a b. b -> Either a b
Right (Funcons -> MSOS StepRes -> Rewritten
CompTerm Funcons
f0 MSOS StepRes
mf), RewriteState
st, RewriteWriterr
forall a. Monoid a => a
mempty)

--- transitive closure over steps
stepTrans :: RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans :: RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans RunOptions
opts Int
i StepRes
res = case StepRes
res of 
  Right [Values Funcons]
vs -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return StepRes
res
  Left Funcons
f | Bool -> (Int -> Bool) -> Maybe Int -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
<= Int
i)) (RunOptions -> Maybe Int
max_restarts RunOptions
opts) -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return StepRes
res
         | Bool
otherwise -> Bool
-> MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_abruptly_terminates (RunOptions -> Bool
do_abrupt_terminate RunOptions
opts) 
                          (Funcons -> MSOS StepRes
stepAndOutput Funcons
f) StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return StepRes -> MSOS StepRes
continue
       where continue :: StepRes -> MSOS StepRes
continue StepRes
res = MSOS ()
count_restart MSOS () -> MSOS StepRes -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans RunOptions
opts (Int
iInt -> Int -> Int
forall a. Num a => a -> a -> a
+Int
1) StepRes
res
             stepAndOutput :: Funcons -> MSOS StepRes
             stepAndOutput :: Funcons -> MSOS StepRes
stepAndOutput Funcons
f = (forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m
 -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a.
(forall (m :: * -> *).
 Interactive m =>
 MSOSReader m
 -> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS ((forall (m :: * -> *).
  Interactive m =>
  MSOSReader m
  -> MSOSState m
  -> m (Either IException StepRes, MSOSState m, MSOSWriter))
 -> MSOS StepRes)
-> (forall (m :: * -> *).
    Interactive m =>
    MSOSReader m
    -> MSOSState m
    -> m (Either IException StepRes, MSOSState m, MSOSWriter))
-> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> 
                let MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper' = Funcons -> MSOS StepRes
evalFuncons Funcons
f
                    stepper :: MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper MSOSReader m
ctxt MSOSState m
mut = MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper' (MSOSReader m -> MSOSReader m
forall (m :: * -> *). MSOSReader m -> MSOSReader m
setGlobal MSOSReader m
ctxt) MSOSState m
mut
                    setGlobal :: MSOSReader m -> MSOSReader m
setGlobal MSOSReader m
ctxt = MSOSReader m
ctxt 
                            { ereader :: RewriteReader
ereader = (MSOSReader m -> RewriteReader
forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) {global_fct :: Funcons
global_fct = Funcons
f }}
                in do   (Either IException StepRes
eres,MSOSState m
mut',MSOSWriter
wr') <- MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper MSOSReader m
ctxt MSOSState m
mut
                        ((Text, Values Funcons) -> m ())
-> [(Text, Values Funcons)] -> m ()
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ ((Text -> Values Funcons -> m ()) -> (Text, Values Funcons) -> m ()
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry Text -> Values Funcons -> m ()
forall (m :: * -> *).
Interactive m =>
Text -> Values Funcons -> m ()
fprint) 
                            [ (Text
entity,Values Funcons
val) 
                            | (Text
entity, [Values Funcons]
vals) <- Inherited -> [(Text, [Values Funcons])]
forall k a. Map k a -> [(k, a)]
M.assocs (MSOSWriter -> Inherited
out_entities MSOSWriter
wr')
                            , Values Funcons
val <- [Values Funcons]
vals ]
                        (Either IException StepRes, MSOSState m, MSOSWriter)
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
eres, MSOSState m
mut', MSOSWriter
wr')


toStepRes :: Funcons -> StepRes
toStepRes :: Funcons -> StepRes
toStepRes (FValue Values Funcons
v)  = [Values Funcons] -> StepRes
forall a b. b -> Either a b
Right [Values Funcons
v]
toStepRes Funcons
f           = Funcons -> StepRes
forall a b. a -> Either a b
Left Funcons
f

flattenApplyWithExc :: IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc :: IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie Funcons -> Funcons
app MSOS StepRes
m = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS StepRes -> Rewrite Rewritten)
-> MSOS StepRes -> Rewrite Rewritten
forall a b. (a -> b) -> a -> b
$ MSOS StepRes
m MSOS StepRes -> (StepRes -> MSOS StepRes) -> MSOS StepRes
forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case 
    Left Funcons
f    -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return (StepRes -> MSOS StepRes) -> StepRes -> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ Funcons -> StepRes
forall a b. a -> Either a b
Left (Funcons -> StepRes) -> Funcons -> StepRes
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
app Funcons
f
    Right [Values Funcons
v] -> StepRes -> MSOS StepRes
forall (m :: * -> *) a. Monad m => a -> m a
return (StepRes -> MSOS StepRes) -> StepRes -> MSOS StepRes
forall a b. (a -> b) -> a -> b
$ Funcons -> StepRes
forall a b. a -> Either a b
Left (Funcons -> StepRes) -> Funcons -> StepRes
forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
app (Values Funcons -> Funcons
FValue Values Funcons
v)
    Right [Values Funcons]
vs  -> IE -> MSOS StepRes
forall b. IE -> MSOS b
msos_throw IE
ie