{-# 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(..),
        -- ** Entity-types
        Output, readOuts, 
        Mutable, 
        Inherited, giveINH, 
        Control, singleCTRL, 
        Input,
            -- ** IMSOS helpers
            applyFuncon, rewritten, rewriteTo, stepTo
                , compstep,
                norule, exception, sortErr, partialOp, internal, buildStep,
            -- *** 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, evalFuncons, stepTrans, emptyINH, Interactive(..), SimIO(..),
    -- * Values
        showValues, showFuncons, 
    -- * Funcon libraries
    FunconLibrary, libUnions, libEmpty, libUnion, libFromList,
    evalctxt2exception, ctxt2exception,
    )where


import Funcons.Types
import Funcons.RunOptions
import Funcons.Printer
import Funcons.Exceptions
import Funcons.Simulation

import Control.Arrow ((***))
import Control.Monad.Writer
import Data.Maybe (isJust, isNothing)
import Data.List (foldl')
import Data.Text (unpack)

import qualified Data.Map as M

---------------------------------------------------------------------
-- | A funcon library maps funcon names to their evaluation functions.
type FunconLibrary = M.Map Name EvalFunction

-- |
-- 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] 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 Funcons)

instance Show Rewritten where
    show (ValTerm v) = showValues v
    show (CompTerm _ _) = "<step>"

-- | Creates an empty 'FunconLibrary'.
libEmpty :: FunconLibrary
libEmpty = M.empty 

-- | Unites two 'FunconLibrary's.
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion = M.unionWithKey op
 where op k x _ = error ("duplicate funcon name: " ++ unpack k)

-- | Unites a list of 'FunconLibrary's.
libUnions :: [FunconLibrary] -> FunconLibrary
libUnions = foldl' libUnion libEmpty
 where op _ _ = error ("duplicate funcon name")

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

lookupFuncon :: Name -> Rewrite EvalFunction
lookupFuncon key = Rewrite $ \ctxt st -> 
    (case M.lookup key (funconlib ctxt) of
        Just f -> Right f
        _ -> case M.lookup key (builtin_funcons (run_opts ctxt)) of
               Just f -> Right (NullaryFuncon (rewriteTo f))
               _ -> error ("unknown funcon: "++ unpack key)
    , st, mempty)

---------------------------------------------------------------------------
data RewriteReader = RewriteReader  
                    { funconlib  :: FunconLibrary    
                    , ty_env     :: TypeEnv, run_opts :: RunOptions
                    , global_fct :: Funcons, local_fct :: Funcons }
data RewriteState = RewriteState {  }
emptyRewriteState = RewriteState 
data RewriteWriterr = RewriteWriterr { 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 {runRewrite :: (RewriteReader -> RewriteState -> 
                    (Either IException a, RewriteState, RewriteWriterr))}

instance Applicative Rewrite where
  pure = return
  (<*>) = ap

instance Functor Rewrite where
  fmap = liftM

instance Monad Rewrite  where
  return a = Rewrite (\_ st -> (Right a, st, mempty))

  (Rewrite f) >>= k = Rewrite (\ctxt st ->
                    let res1@(e_a1,st1,cs1) = f ctxt st
                     in case e_a1 of 
                          Left err  -> (Left err, st1, cs1)
                          Right a1  -> let (Rewrite h) = k a1
                                           (a2,st2,cs2) = h ctxt st1
                                        in (a2,st2,cs1 <> cs2))

instance Monoid RewriteWriterr where
    mempty = RewriteWriterr mempty
    (RewriteWriterr cs1) `mappend` (RewriteWriterr cs2) = RewriteWriterr (cs1 `mappend` cs2)

liftRewrite :: Rewrite a -> MSOS a
liftRewrite ev = MSOS $ \ctxt mut -> 
                let (e_a, est, ewr) = runRewrite ev (ereader ctxt) (estate mut)
                in return (e_a, mut {estate = est}, mempty { ewriter = ewr })

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

eval_else :: (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else prop [] def = def
eval_else prop (ev:evs) def = eval_catch ev >>= \case
    Right a -> return a
    Left (gf,lf,ie) | prop ie   -> eval_else prop evs def
                    | otherwise -> rewrite_rethrow (gf,lf,ie)

rewrite_rethrow :: IException -> Rewrite a
rewrite_rethrow ie = Rewrite $ \ctxt st -> (Left ie, st, mempty)

rewrite_throw :: IE -> Rewrite a
rewrite_throw ie = Rewrite $ \ctxt st -> 
    (Left (global_fct ctxt, local_fct ctxt, ie), st, mempty)

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

ctxt2exception :: IE -> MSOSReader -> IException
ctxt2exception ie ctxt = 
    (global_fct (ereader ctxt), local_fct (ereader ctxt), ie)


rewriteRules :: Funcons -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules f [] = norule f 
rewriteRules f (t1:ts) = Rewrite $ \ctxt st ->  
    let (rw_res, st', rw_cs) = runRewrite t1 ctxt st
    in case rw_res of
        Left ie| failsRule ie -> -- resets state 
                                 runRewrite (rewriteRules f ts) ctxt st 
        _                     -> (rw_res, st', rw_cs)

---------------------------------------------------------------------------
data MSOSReader = MSOSReader { ereader :: RewriteReader, inh_entities :: Inherited}
data MSOSWriter = MSOSWriter { ctrl_entities :: Control, out_entities :: Output
                             , ewriter :: RewriteWriterr }
data MSOSState m = MSOSState { inp_es :: Input m, mut_entities :: Mutable
                             , estate :: RewriteState }
emptyMSOSState :: MSOSState m
emptyMSOSState = MSOSState M.empty M.empty 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 'TypeEnv'), 
-- 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 { runMSOS :: 
                        forall m. Interactive m => 
                        (MSOSReader -> MSOSState m 
                        -> m (Either IException a, MSOSState m, MSOSWriter)) }

instance Applicative MSOS where
  pure = return
  (<*>) = ap

instance Functor MSOS where
  fmap = liftM

instance Monad MSOS  where
  return a = MSOS (\_ mut -> return (Right a,mut,mempty))

  (MSOS f) >>= k = MSOS (\ctxt mut -> do
                    res1@(e_a1,mut1,wr1) <- f ctxt mut 
                    case e_a1 of 
                      Left err  -> return (Left err, mut1, wr1)
                      Right a1  -> do   
                            let (MSOS h) = k a1
                            (a2,mut2,wr2) <- h ctxt mut1
                            return (a2,mut2,wr1 <> wr2))

instance Monoid MSOSWriter where
    mempty = MSOSWriter mempty mempty mempty
    (MSOSWriter x1 x2 x3) `mappend` (MSOSWriter y1 y2 y3) = 
        MSOSWriter (x1 `unionCTRL` y1) (x2 `unionOUT` y2) (x3 `mappend` y3) 

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

stepRules :: [MSOS Funcons] -> MSOS Funcons 
stepRules [] = msos_throw NoRule
stepRules (t1:ts) = MSOS $ \ctxt mut -> do 
    (e_ie_a, mut', wr) <- runMSOS t1 ctxt mut 
    case e_ie_a of
        Left ie | failsRule ie -> -- resets input & read/write entities
                                  runMSOS (stepRules ts) ctxt mut
        _                      -> return (e_ie_a, mut', 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 Funcons] -> Rewrite Rewritten
evalRules [] msoss = buildStep (stepRules msoss)
evalRules ((Rewrite rw_rules):rest) msoss = Rewrite $ \ctxt st -> 
    let (rw_res, st', cs) = rw_rules ctxt st
    in case rw_res of
        Left ie | failsRule ie  -> --resets counters and state 
                                    runRewrite (evalRules rest msoss) ctxt st
        _                       -> (rw_res, st', cs)

msos_throw :: IE -> MSOS b
msos_throw = liftRewrite . rewrite_throw 

---
giveOpts :: MSOS RunOptions 
giveOpts = MSOS $ \ctxt mut -> 
    return (Right (run_opts (ereader ctxt)), mut, mempty)

giveINH :: MSOS Inherited
giveINH = MSOS $ \ctxt mut -> return (Right (inh_entities ctxt), mut, mempty)

doRefocus :: MSOS Bool
doRefocus = MSOS $ \ctxt mut -> 
    return (Right $ do_refocus (run_opts (ereader ctxt)), mut, mempty)

modifyCTXT :: (MSOSReader -> MSOSReader) -> MSOS a -> MSOS a
modifyCTXT mod (MSOS f) = MSOS (\ctxt mut -> f (mod ctxt) mut)

modifyRewriteCTXT :: (RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT mod (Rewrite f) = Rewrite (f . mod)
-----------------
-- | a map storing the values of /inherited/ entities.
type Inherited       = M.Map Name Values 

emptyINH :: Inherited
emptyINH = M.empty 

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

emptyCTRL :: Control
emptyCTRL = M.empty

singleCTRL :: Name -> Values -> Control
singleCTRL k = M.singleton k . Just

unionCTRL = M.unionWithKey (error . err)
 where err key = "Two " ++ unpack key ++ " signals converging!"

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

unionOUT :: Output -> Output -> Output
unionOUT = M.unionWith (++)

emptyOUT :: Output 
emptyOUT = M.empty 

readOuts :: MSOS a -> MSOS (a, Output)
readOuts (MSOS f) = MSOS $ (\ctxt mut -> do 
    (e_a, mut1, wr1) <- f ctxt mut
    case e_a of 
        Left err -> return (Left err, mut1, wr1)
        Right a  -> return (Right (a,(out_entities wr1))
                            , mut1, wr1 { out_entities = mempty}))
-----------
-- | A map storing the values of /input/ entities.
type Input m = M.Map Name ([[Values]], Maybe (m Values))

-----------
-- steps, rewrites, restarts, refocus, delegations
data Counters = Counters !Int !Int !Int !Int !Int 

instance Monoid Counters where
    mempty = Counters 0 0 0 0 0
    (Counters x1 x2 x3 x4 x5) `mappend` (Counters y1 y2 y3 y4 y5) = 
        Counters (x1+y1) (x2+y2) (x3+y3) (x4+y4) (x5+y5)

emptyCounters :: Int -> Int -> Int -> Int -> Int -> MSOSWriter 
emptyCounters x1 x2 x3 x4 x5 = 
    mempty { ewriter = mempty {counters = Counters x1 x2 x3 x4 x5 }}

count_step :: MSOS ()
count_step = MSOS $ \_ mut -> return (Right (), mut, emptyCounters 1 0 0 0 0)

count_delegation :: MSOS ()
count_delegation = MSOS $ \_ mut -> return (Right (), mut, emptyCounters 0 0 0 0 1)

count_refocus = MSOS $ \_ mut -> return (Right (), mut, emptyCounters 0 0 0 1 0)

count_restart :: MSOS ()
count_restart = MSOS $ \_ mut -> return (Right (), mut, emptyCounters 0 0 1 0 0)

count_rewrite :: Rewrite ()
count_rewrite = Rewrite $ \_ st -> (Right (), st, mempty { counters = Counters 0 1 0 0 0 })

instance Show Counters where
    show (Counters steps rewrites restarts refocus delegations) = 
        "number of (restarts, rewrites, steps, refocus, premises): " ++ 
            show (restarts, rewrites, steps, refocus, delegations)

-- | 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 f = rewrite_throw 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 f str = rewrite_throw (SortErr 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 f str = rewrite_throw (PartialOp str) 

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

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


buildStep :: MSOS Funcons -> Rewrite Rewritten 
buildStep = buildStepCounter (return ()) -- does not count

buildStepCount :: MSOS Funcons -> Rewrite Rewritten
buildStepCount = buildStepCounter count_delegation

buildStepCounter :: MSOS () -> MSOS Funcons -> Rewrite Rewritten 
buildStepCounter counter mf = compstep (counter >> mf)

optRefocus :: MSOS Funcons -> MSOS Funcons
optRefocus stepper = doRefocus >>= \case
                        True    -> refocus stepper 
                        False   -> stepper 

refocus :: MSOS Funcons -> MSOS Funcons
refocus stepper -- stop refocussing when a signal has been raised
                = count_refocus >> if_violates_refocus stepper return continue
    where continue f | isVal f = return f
                     | otherwise = refocus (evalFuncons f)

stepRewritten :: Rewritten -> MSOS Funcons
stepRewritten (ValTerm v) = return (FValue v)
stepRewritten (CompTerm _ step) = count_step >> step

-- | Returns a value as a fully rewritten term. 
rewritten :: Values -> Rewrite Rewritten
rewritten = return . 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 f = count_rewrite >> rewriteFuncons f

-- | Yield a funcon term as the result of an 'MSOS' computation.
-- This function must be used instead of @return@. 
stepTo :: Funcons -> MSOS Funcons
stepTo f = return f

if_abruptly_terminates :: Bool -> MSOS Funcons -> (Funcons -> MSOS Funcons)
                            -> (Funcons -> MSOS Funcons) -> MSOS Funcons
if_abruptly_terminates care (MSOS fstep) abr no_abr = MSOS $ \ctxt mut ->
    fstep ctxt mut >>= \case
        (Right f', mut', wr') ->
            let failed     = any isJust (ctrl_entities wr')
                MSOS fstep | failed && care = abr f'
                           | otherwise      = no_abr f'
            in do (e_f'', mut'', wr'') <- fstep ctxt mut'
                  return (e_f'', mut'', wr' <> wr'')
        norule_res -> return norule_res

if_violates_refocus :: MSOS Funcons -> (Funcons -> MSOS Funcons)
                            -> (Funcons -> MSOS Funcons) -> MSOS Funcons
if_violates_refocus (MSOS fstep) viol no_viol = MSOS $ \ctxt mut ->
    fstep ctxt mut >>= \case
        (Right f', mut', wr') ->
            let violates = any isJust (ctrl_entities wr')
                            || any (not . null) (out_entities wr')
                            || any (isNothing . snd) (inp_es mut')
                MSOS fstep | violates    = viol f'
                           | otherwise   = no_viol f'
            in do (e_f'', mut'', wr'') <- fstep ctxt mut'
                  return (e_f'', mut'', wr' <> wr'')
        norule_res -> return norule_res

-- | Execute a premise as either a rewrite or a step.
-- Depending on whether rewrites were performed or a step was performed
-- 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   rewrite1 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 Funcons -> MSOS Funcons) -> 
                    Funcons -> Rewrite Rewritten
premiseEval vapp fapp f = rewriteFuncons f >>= \case
    ValTerm v       -> vapp v
    CompTerm _ step -> buildStepCount (optRefocus (fapp step))

premiseCont :: (Funcons -> Funcons) -> Funcons -> MSOS Funcons 
premiseCont app f = liftRewrite (rewriteFuncons f) >>= \case
    ValTerm v       -> msos_throw StepOnValue
    CompTerm _ step -> app <$> (count_delegation >> optRefocus step)

premiseStepApp :: (Funcons -> Funcons) -> Funcons -> MSOS Funcons
premiseStepApp app f = premiseCont app f

-- | Execute a computational step as a /premise/.
-- The result of the step is the returned funcon term. 
premiseStep :: Funcons -> MSOS Funcons
premiseStep = premiseStepApp id

----- main `step` function
evalFuncons :: Funcons -> MSOS Funcons
evalFuncons f = liftRewrite (rewriteFuncons f) >>= stepRewritten

rewriteFuncons :: Funcons -> Rewrite Rewritten 
rewriteFuncons f = modifyRewriteCTXT (\ctxt -> ctxt {local_fct = f}) (rewriteFuncons' f)
 where
    rewriteFuncons' (FValue v)   = return (ValTerm v) 
    rewriteFuncons' (FTuple fs)  = let fmops = tupleTypeTemplate fs 
                                in if any (isJust . snd) fmops
                                    then rewritten . typeVal =<< evalTupleType fmops
                                    else evalStrictSequence fs safe_tuple_val FTuple
    rewriteFuncons' (FList fs)   = evalStrictSequence fs List FList
    rewriteFuncons' (FSet fs)    = evalStrictSequence fs setval_ FSet
    rewriteFuncons' (FMap fs)    = evalStrictSequence fs mapval_ FMap
    rewriteFuncons' f@(FSortSeq s1 op)     =
        internal ("naked sequence-sort appearing outside of tuple-notation: " ++ showFuncons f)
    rewriteFuncons' (FSortComputes f1) = case f1 of
        (FValue (ComputationType (Type ty))) -> rewritten $ ComputationType $ ComputesType ty
        (FValue _) -> sortErr (FSortComputes f1) "=> not applied to a type"
        _ -> rewriteFuncons f1 >>= \case
                ValTerm v1 -> rewriteFuncons $ FSortComputes (FValue v1)
                CompTerm _ mf    -> compstep (FSortComputes <$> mf)
    rewriteFuncons' (FSortComputesFrom f1 f2) = case (f1,f2) of
        (FValue (ComputationType (Type ty1)),FValue (ComputationType (Type ty2))) 
            -> rewritten $ ComputationType (ComputesFromType ty1 ty2)
        (FValue _, FValue _) -> sortErr (FSortComputesFrom f1 f2) "=> not applied to types"
        (FValue (ComputationType (Type ty1)),_) 
            -> rewriteFuncons f2 >>= \case
                ValTerm v2 -> rewriteFuncons $ FSortComputesFrom f1 (FValue v2)
                CompTerm _ mf    -> compstep (FSortComputesFrom f1 <$> mf)
        (_,_) 
            -> rewriteFuncons f1 >>= \case
                ValTerm v1 -> rewriteFuncons $ FSortComputesFrom (FValue v1) f2
                CompTerm _ mf    -> compstep (flip FSortComputesFrom f2 <$> mf)
    rewriteFuncons' (FSortUnion s1 s2)   = case (s1, s2) of
        (FValue (ComputationType (Type t1))
            , FValue (ComputationType (Type t2))) -> rewritten $ typeVal $ Union t1 t2
        (FValue _, FValue _) -> sortErr (FSortUnion s1 s2) "sort-union not applied to two sorts"
        (FValue v1, _) -> do   rewriteFuncons s2 >>= \case
                                ValTerm v2 -> rewriteFuncons $ FSortUnion s1 (FValue v2)
                                CompTerm _ mf -> compstep (FSortUnion s1 <$> mf)
        _ -> do rewriteFuncons s1 >>= \case
                    ValTerm v -> rewriteFuncons $ FSortUnion (FValue v) s2
                    CompTerm _ mf   -> compstep (flip FSortUnion s2 <$> mf)
    rewriteFuncons' (FName nm)     = 
        do  mystepf <- lookupFuncon nm 
            case mystepf of 
                NullaryFuncon mystep -> mystep
                _ -> error ("funcon " ++ unpack nm ++ " not applied to any arguments")
    rewriteFuncons' (FApp nm arg)    = 
        do  mystepf <- lookupFuncon nm
            case mystepf of 
                NullaryFuncon _     -> exception (FApp nm arg) ("nullary funcon " ++ unpack nm ++ " applied to arguments")
                ValueOp mystep      -> rewriteFuncons arg >>= 
                                        \case ValTerm v -> mystep (tuple_unval v)
                                              CompTerm _ mf -> compstep (FApp nm <$> mf)
                StrictFuncon mystep -> rewriteFuncons arg >>=
                                        \case ValTerm v -> mystep (tuple_unval v)
                                              CompTerm _ mf -> compstep (FApp nm <$> mf)
                NonStrictFuncon mystep   -> case arg of
                                        FTuple fs -> mystep fs
                                        _ -> exception (FApp nm arg) ("lazy funcon " ++ unpack nm ++ " not applied to a tuple of arguments")
                PartiallyStrictFuncon strns mystep -> case arg of 
                    FTuple fs -> evalSequence strns fs mystep (applyFuncon nm)
                    _ -> exception (FApp nm arg) ("partially lazy funcon " ++ unpack nm ++ " not applied to a tuple of arguments")

--OPT: replace by specialised veriant of evalSequence
evalStrictSequence :: [Funcons] -> ([Values] -> Values) -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence args cont cons = 
    evalSequence (replicate (length args) Strict) args 
        (return . ValTerm . cont . map downcastValue) cons

evalSequence :: [Strictness] -> [Funcons] -> 
    ([Funcons] -> Rewrite Rewritten) -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalSequence strns args cont cons = 
    uncurry evalSeqAux $ map snd *** id $ span isDone (zip strns args)
 where  evalSeqAux :: [Funcons] -> [(Strictness, Funcons)] -> Rewrite Rewritten
        evalSeqAux vs [] = cont vs
        evalSeqAux vs ((_,f):fs) = premiseEval valueCont funconCont f
         where  valueCont v = do 
                    count_rewrite
                    evalSeqAux (vs++(FValue v:map snd othervs)) otherfs
                 where (othervs, otherfs) = span isDone fs
                funconCont stepf = do   f' <- stepf 
                                        stepTo (cons (vs++[f']++map snd fs))
        isDone (Strict, FValue _) = True
        isDone (NonStrict, _) = True
        isDone _ = 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 Funcons -> Rewrite Rewritten
compstep mf = Rewrite $ \ctxt st -> 
    let f0 = local_fct ctxt 
    in (Right (CompTerm f0 mf), st, mempty)

tupleTypeTemplate :: [Funcons] -> [(Funcons, Maybe SeqSortOp)]
tupleTypeTemplate = map aux
    where   aux (FSortSeq f op) = (f, Just op)
            aux f               = (f, Nothing)
            

evalTupleType :: [(Funcons,Maybe SeqSortOp)] -> Rewrite Types
evalTupleType = fmap Tuples . evalTupleType' 
    where
        evalTupleType' :: [(Funcons, Maybe SeqSortOp)] -> Rewrite [TTParam]
        evalTupleType' [] = return []
        evalTupleType' ((f,mop):fs) = rewriteFuncons f >>= \case
            ValTerm v -> case castType v of
              Just t -> ((t,mop):) <$> evalTupleType' fs 
              Nothing-> sortErr(FValue v)"non-type value appeared in type tuple"
            CompTerm _ _ -> 
                sortErr f"tuple type expressions may not contain compsteps"

--- transitive closure over steps
stepTrans :: RunOptions -> Int -> Funcons -> MSOS Funcons 
stepTrans opts i f
    | isVal f || maybe False ((<= i)) (max_restarts opts) = return f
    | otherwise = if_abruptly_terminates (do_abrupt_terminate opts) 
                    (stepAndOutput f) return continue
       where continue f' = do   count_restart
                                modifyCTXT setGlobal (stepTrans opts (i+1) f')
              where setGlobal ctxt = ctxt { ereader = 
                                             (ereader ctxt) {global_fct = f' }}
             stepAndOutput f = MSOS $ \ctxt mut -> 
                let MSOS stepper = evalFuncons f
                in do   (eres,mut',wr') <- stepper ctxt mut
                        mapM_ (uncurry fprint) 
                            [ (entity,val) 
                            | (entity, vals) <- M.assocs (out_entities wr')
                            , val <- vals ]
                        return (eres, mut', wr')