funcons-tools-0.1.0.0: src/Funcons/MSOS.hs
{-# 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')