funcons-tools-0.2.0.16: 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(..),
StepRes, toStepRes,
-- ** Entity-types
Output, readOuts,
Mutable,
Inherited, giveINH,
Control, singleCTRL, giveCTRL,
Input,
-- ** IMSOS helpers
applyFuncon, rewritten, rewriteTo, rewriteSeqTo, stepTo, stepSeqTo,rewrittens,
compstep,
norule, exception, sortErr, partialOp, internal, buildStep, sidecond,
-- *** Congruence rules
premiseStepApp, premiseStep, premiseEval,
-- ** Pattern Matching
SeqSortOp(..),
rewriteRules, stepRules, evalRules, MSOSState(..), emptyMSOSState, emptyRewriteState, MSOSReader(..),RewriteReader(..),showIException, MSOSWriter(..), RewriteWriterr(..),
-- * Evaluation funcons TODO internal usage only (by Funcons.Tools)
Rewritten(..), rewriteFuncons, rewriteFunconsWcount, evalFuncons
, stepTrans, stepAndOutput, rewritesToValue, rewritesToValues, rewritesToType
, emptyDCTRL, emptyINH, Interactive(..), SimIO(..)
, rewriteToValErr, count_delegation, optRefocus
, evalStrictSequence, rewriteStrictSequence, evalSequence
, maybe_randomSelect, maybe_randomRemove,
-- * Values
showTypes, showSorts, showValues, showValuesSeq, showFuncons, showFunconsSeq,traceLib,
-- * Funcon libraries
FunconLibrary, libUnions, libOverrides, libEmpty, libUnion, libOverride, Funcons.MSOS.libFromList,
evalctxt2exception, ctxt2exception, fromSeqValOp, fromNullaryValOp, fromValOp,
-- * Counters
displayCounters, counterKeys, ppCounters,
)where
import Funcons.Types
import Funcons.RunOptions
import Funcons.Printer
import Funcons.Exceptions
import Funcons.Simulation
import qualified Funcons.Operations as VAL
import Control.Monad (liftM, ap)
import Data.Function (on)
import Data.Maybe (isJust, isNothing, fromJust)
import Data.List (foldl', intercalate, partition, sortBy)
import Data.Text (unpack)
import qualified Data.Map as M
import System.Random
import System.IO.Unsafe
--trace p b = unsafePerformIO (putStrLn p >> return b)
trace p b = b
traceLib :: FunconLibrary -> FunconLibrary
traceLib lib = unsafePerformIO
(putStrLn (unlines (map unpack (M.keys lib))) >> return lib)
---------------------------------------------------------------------
-- | A funcon library maps funcon names to their evaluation functions.
type FunconLibrary = M.Map Name EvalFunction
fromValOp = fromAbsValOp False
fromSeqValOp = fromAbsValOp True
fromAbsValOp :: Bool -> ([Funcons] -> Funcons) -> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromAbsValOp seqRes cons mkExpr = ValueOp op
where op vs = report f seqRes (VAL.eval (mkExpr (map ValExpr vs)))
where f = cons (map FValue vs)
fromNullaryValOp :: ([Funcons] -> Funcons) -> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromNullaryValOp cons mkExpr = NullaryFuncon op
where op = report (cons []) False (VAL.eval (mkExpr []))
report :: Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report f seqRes res = case res of
Error _ dres -> reportResult dres
Success (FValue (ADTVal "null" _)) -> rewrittens []
Success (FValue v) -> rewritten' v
Success t -> rewriteFuncons t
EvalResults ress -> maybe_randomSelect NDValueOperations ress >>=
report f seqRes
where rewritten' v | seqRes, ValSeq fs <- v,
let mvs = map project fs, all isJust mvs
= rewrittens (map fromJust mvs)
| otherwise = rewritten v
reportResult dres = case dres of
(VAL.SortErr str) -> sortErr f str
(DomErr str) -> rewrittens []
(ArityErr str) -> sortErr f str
(ProjErr str) -> sortErr f str
(Normal (FValue v)) -> rewritten' v
(Normal t) -> rewriteFuncons t
(Nondeterministic ress) -> case ress of
[] -> sortErr f "nondeterminism: empty"
_ -> randomSelect ress >>= reportResult
-- |
-- Evaluation functions capture the operational behaviour of a funcon.
-- Evaluation functions come in multiple flavours, each with a different
-- treatment of the arguments of the funcon.
-- Before the application of an evaluation funcon, any argument may be
-- evaluated, depending on the 'Strictness' of the argument.
data EvalFunction =
-- | Funcons for which arguments are /not/ evaluated.
NonStrictFuncon NonStrictFuncon
-- | Strict funcons whose arguments are evaluated.
| StrictFuncon StrictFuncon
-- | Funcons for which /some/ arguments are evaluated.
| PartiallyStrictFuncon [Strictness] Strictness NonStrictFuncon
-- | Synonym for 'StrictFuncon', for value operations.
| ValueOp ValueOp
-- | Funcons without any arguments.
| NullaryFuncon NullaryFuncon
-- | Type synonym for the evaluation function of strict funcons.
-- The evaluation function of a 'StrictFuncon' receives fully evaluated arguments.
type StrictFuncon = [Values] -> Rewrite Rewritten
-- | Type synonym for the evaluation function of fully non-strict funcons.
type NonStrictFuncon = [Funcons] -> Rewrite Rewritten
-- | Type synonym for the evaluation function of non-strict funcons.
type PartiallyStrictFuncon = NonStrictFuncon
-- | Type synonym for value operations.
type ValueOp = StrictFuncon
-- | Type synonym for the evaluation functions of nullary funcons.
type NullaryFuncon = Rewrite Rewritten
-- | Denotes whether an argument of a funcon should be evaluated or not.
data Strictness = Strict | NonStrict
-- | After a term is fully rewritten it is either a value or a
-- term that requires a computational step to proceed.
-- This types forms the interface between syntactic rewrites and
-- computational steps.
data Rewritten =
-- | Fully rewritten to a value.
ValTerm [Values]
-- | Fully rewritten to a term and the step required to continue evaluation.
| CompTerm Funcons (MSOS StepRes)
-- | A single step on a funcon term produces either a funcon term
-- or a (possibly empty or unary) sequence of values
type StepRes = Either Funcons [Values]
instance Show Rewritten where
show (ValTerm vs) = showValuesSeq vs
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)
-- | Right-based union of 'FunconLibrary's
libOverride :: FunconLibrary -> FunconLibrary -> FunconLibrary
libOverride = flip M.union
-- | Unites a list of 'FunconLibrary's.
libUnions :: [FunconLibrary] -> FunconLibrary
libUnions = foldl' libUnion libEmpty
where op _ _ = error ("duplicate funcon name")
-- | Right-based union of list of 'FunconLibrary's
libOverrides :: [FunconLibrary] -> FunconLibrary
libOverrides = M.unions . reverse
-- | 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))
_ -> Left (evalctxt2exception (Internal ("unknown funcon: "++ unpack key)) ctxt)
, st, mempty)
---------------------------------------------------------------------------
data RewriteReader = RewriteReader
{ funconlib :: FunconLibrary
, ty_env :: TypeRelation, run_opts :: RunOptions
, global_fct :: Funcons, local_fct :: Funcons }
data RewriteState = RewriteState { random_gen :: StdGen }
emptyRewriteState = RewriteState (mkStdGen 0)
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 a = Rewrite (\_ st -> (Right a, st, mempty))
(<*>) = ap
instance Functor Rewrite where
fmap = liftM
instance Monad Rewrite where
(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 Semigroup RewriteWriterr where
(RewriteWriterr cs1) <> (RewriteWriterr cs2) = RewriteWriterr (cs1 <> cs2)
instance Monoid RewriteWriterr where
mempty = RewriteWriterr mempty
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 (evalctxt2exception ie ctxt), st, mempty)
evalctxt2exception :: IE -> RewriteReader -> IException
evalctxt2exception ie ctxt = (global_fct ctxt, local_fct ctxt, ie)
ctxt2exception :: IE -> MSOSReader m -> IException
ctxt2exception ie ctxt =
(global_fct (ereader ctxt), local_fct (ereader ctxt), ie)
rewriteRules = rewriteRules' []
rewriteRules' :: [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' errs [] = rewrite_throw (NoMoreBranches errs)
rewriteRules' errs (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
trace (showIException ie) $ runRewrite (do
count_backtrack_in
addToRCounter (counters rw_cs)
rewriteRules' (ie:errs) ts) ctxt st
_ -> (rw_res, st', rw_cs)
---------------------------------------------------------------------------
data MSOSReader m = MSOSReader{ ereader :: RewriteReader
, inh_entities :: Inherited
, dctrl_entities :: DownControl
, def_fread :: Name -> m Funcons}
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 :: Int -> MSOSState m
emptyMSOSState seed =
MSOSState M.empty M.empty (emptyRewriteState { random_gen = mkStdGen seed })
-- | Monadic type for the propagation of semantic entities and meta-information
-- on the evaluation of funcons. The meta-information includes a library
-- of funcons (see 'FunconLibrary'), a typing environment (see 'TypeRelation'),
-- runtime options, etc.
--
-- The semantic entities are divided into five classes:
--
-- * inherited entities, propagated similar to values of a reader monad.
--
-- * mutable entities, propagated similar to values of a state monad.
--
-- * output entities, propagation similar to values of a write monad.
--
-- * control entities, similar to output entities except only a single control /signal/
-- can be emitted at once (signals do not form a monoid).
--
-- * input entities, propagated like values of a state monad, but access like
-- value of a reader monad. This package provides simulated input/outout
-- and real interaction via the 'IO' monad. See "Funcons.Tools".
--
-- For each entity class a map is propagated, mapping entity names to values.
-- This enables modular access to the entities.
newtype MSOS a = MSOS { runMSOS ::
forall m. Interactive m =>
(MSOSReader m -> MSOSState m
-> m (Either IException a, MSOSState m, MSOSWriter)) }
instance Applicative MSOS where
pure a = MSOS (\_ mut -> return (Right a,mut,mempty))
(<*>) = ap
instance Functor MSOS where
fmap = liftM
instance Monad MSOS where
(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 MonadFail MSOS where
fail = liftRewrite . internal
instance Semigroup MSOSWriter where
(MSOSWriter x1 x2 x3) <> (MSOSWriter y1 y2 y3) =
MSOSWriter (x1 `unionCTRL` y1) (x2 `unionOUT` y2) (x3 `mappend` y3)
instance Monoid MSOSWriter where
mempty = MSOSWriter mempty mempty mempty
-- | A map storing the values of /mutable/ entities.
type Mutable = M.Map Name [Values]
stepRules = stepARules NoMoreBranches count_backtrack_in
stepARules :: ([IException] -> IE) -> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules fexc _ errs [] = msos_throw (fexc errs)
stepARules fexc counter errs ts =
liftRewrite (maybe_randomRemove NDRuleSelection ts) >>=
\(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
trace (showIException ie) $ runMSOS (do
liftRewrite counter
addToCounter (counters (ewriter wr))
stepARules fexc counter (errs++[ie]) 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 = evalRules' []
evalRules' :: [IException] -> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules' errs [] msoss = buildStep (stepARules NoRule count_backtrack_out errs msoss)
evalRules' errs rules msoss =
maybe_randomRemove NDRuleSelection rules >>= \((Rewrite rw_rules),rest) ->
Rewrite $ \ctxt st ->
let (rw_res, st', wo) = rw_rules ctxt st
in case rw_res of
Left ie | failsRule ie -> --resets counters and state
trace (showIException ie) $ runRewrite (do
count_backtrack_out
addToRCounter (counters wo)
evalRules' (ie:errs) rest msoss) ctxt st
_ -> (rw_res, st', wo)
msos_throw :: IE -> MSOS b
msos_throw = liftRewrite . rewrite_throw
---
giveOpts :: Rewrite RunOptions
giveOpts = Rewrite $ \ctxt mut -> (Right (run_opts ctxt), mut, mempty)
giveINH :: MSOS Inherited
giveINH = MSOS $ \ctxt mut -> return (Right (inh_entities ctxt), mut, mempty)
giveCTRL :: MSOS DownControl
giveCTRL = MSOS $ \ctxt mut -> return (Right (dctrl_entities ctxt), mut, mempty)
doRefocus :: MSOS Bool
doRefocus = MSOS $ \ctxt mut ->
return (Right $ do_refocus (run_opts (ereader ctxt)), mut, mempty)
modifyRewriteCTXT :: (RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT mod (Rewrite f) = Rewrite (f . mod)
modifyRewriteReader :: (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader mod (MSOS f) = MSOS (f . mod')
where mod' ctxt = ctxt { ereader = mod (ereader ctxt) }
maybe_randomRemove :: SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove _ [] = randomRemove []
maybe_randomRemove src xs@(x:xs') = do
opts <- giveOpts
if src `elem` get_nd_sources opts then randomRemove xs
else return (x, xs')
-- | Uses the random number generator of Rewrite to randomly select
-- an element of a given list. The element is returned, together
-- with the list from which the element has been removed
-- Raises an internal exception if given an empty list
randomRemove :: [a] -> Rewrite (a, [a])
randomRemove [] = internal "randomRemove: empty list"
randomRemove [x]= return (x, [])
randomRemove xs = Rewrite $ \_ mut ->
let gen = random_gen mut
(i, gen') = next gen
index = i `mod` (length xs)
elem = xs !! index
rest = take index xs ++ drop (index + 1) xs
in (Right (elem, rest), mut {random_gen = gen'}, mempty )
maybe_randomSelect src xs = fst <$> maybe_randomRemove src xs
randomSelect xs = fst <$> randomRemove xs
{-
randomSelect :: [a] -> Rewrite a
randomSelect xs = Rewrite $ \_ mut ->
let gen = random_gen mut
(_, top) = genRange gen
unit = fromIntegral top / fromIntegral (length xs)
(i, gen') = next gen
index = round (fromIntegral i / unit)
in (Right (xs !! index), mut {random_gen = gen'}, mempty )
-}
-----------------
-- | a map storing the values of /inherited/ entities.
type Inherited = M.Map Name [Values]
emptyINH :: Inherited
emptyINH = 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 = M.empty
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 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 x1 x2 x3 x4 x5 x6 x7 x8) <> (Counters y1 y2 y3 y4 y5 y6 y7 y8) =
Counters (x1+y1) (x2+y2) (x3+y3) (x4+y4) (x5+y5) (x6+y6) (x7+y7) (x8+y8)
instance Monoid Counters where
mempty = Counters 0 0 0 0 0 0 0 0
emptyCounters x1 x2 x3 x4 x5 x6 x7 x8 =
mempty { ewriter = mempty {counters = Counters x1 x2 x3 x4 x5 x6 x7 x8}}
addToCounter :: Counters -> MSOS ()
addToCounter cs = MSOS $ \_ mut -> return (Right(), mut, mempty { ewriter = mempty { counters = cs } })
addToRCounter :: Counters -> Rewrite ()
addToRCounter cs = Rewrite $ \_ mut -> (Right(), mut, mempty { counters = cs })
count_step :: MSOS ()
count_step = MSOS $ \_ mut -> return (Right (), mut, emptyCounters 1 0 0 0 0 0 0 0)
count_delegation :: MSOS ()
count_delegation = MSOS $ \_ mut -> return (Right (), mut, emptyCounters 0 0 0 0 0 1 0 0)
count_refocus = MSOS $ \_ mut -> return (Right (), mut, emptyCounters 0 0 0 0 1 0 0 0)
count_restart :: MSOS ()
count_restart = MSOS $ \_ mut -> return (Right (), mut, emptyCounters 0 0 0 1 0 0 0 0)
count_rewrite :: Rewrite ()
count_rewrite = Rewrite $ \_ st -> (Right (), st, mempty { counters = Counters 0 1 0 0 0 0 0 0})
count_rewrite_attempt :: Rewrite ()
count_rewrite_attempt = Rewrite $ \_ st -> (Right (), st, mempty { counters = Counters 0 0 1 0 0 0 0 0})
count_backtrack_out :: Rewrite ()
count_backtrack_out = Rewrite $ \_ st -> (Right (), st, mempty { counters = Counters 0 0 0 0 0 0 1 0 })
count_backtrack_in :: Rewrite ()
count_backtrack_in = Rewrite $ \_ st -> (Right (), st, mempty { counters = Counters 0 0 0 0 0 0 0 1 })
ppCounters cs =
"number of (" ++ counterKeys ++ "): (" ++ displayCounters cs ++ ")"
counterKeys :: String
counterKeys = "restarts,rewrites,(attempts),steps,refocus,premises,backtracking(outer),backtracking(inner)"
displayCounters (Counters steps rewrites rattempts restarts refocus delegations bout bin) =
intercalate "," $
map show [restarts, rewrites, rattempts, steps, refocus, delegations, bout, 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 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)
sidecond :: String -> Rewrite a
sidecond str = rewrite_throw (SideCondFail str)
buildStep :: MSOS StepRes -> Rewrite Rewritten
buildStep = buildStepCounter (return ()) -- does not count
buildStepCount :: MSOS StepRes -> Rewrite Rewritten
buildStepCount = buildStepCounter count_delegation
buildStepCounter :: MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter counter mf = compstep (counter >> mf)
optRefocus :: MSOS StepRes -> MSOS StepRes
optRefocus stepper = doRefocus >>= \case
True -> refocus stepper
False -> stepper
refocus :: MSOS StepRes -> MSOS StepRes
refocus stepper -- stop refocussing when a signal has been raised
= count_refocus >> if_violates_refocus stepper return continue
where continue = \case
Right vs -> return (Right vs)
Left f ->
liftRewrite (rewriteFuncons f) >>= \case
ValTerm [v] -> return (Right [v])
ValTerm vs -> return (Left f) -- undo rewrites and accept last step
res -> refocus $ stepRewritten res
stepRewritten :: Rewritten -> MSOS StepRes
stepRewritten (ValTerm vs) = return (Right vs)
stepRewritten (CompTerm f step) = modifyRewriteReader mod (count_step >> step)
where mod ctxt = ctxt {local_fct = f}
-- | Returns a value as a fully rewritten term.
rewritten :: Values -> Rewrite Rewritten
rewritten = return . ValTerm . (:[])
rewrittens :: [Values] -> Rewrite Rewritten
rewrittens = 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 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 fs = count_rewrite >> (ValTerm <$> rewriteStrictSequence 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 = return . 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 fs = Right <$> liftRewrite (rewriteStrictSequence fs)
if_abruptly_terminates :: Bool -> MSOS StepRes -> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes) -> MSOS StepRes
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
-- 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 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')
-- || any isJust (dctrl_entities ctxt)
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 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 vapp fapp f = rewriteFuncons f >>= \case
ValTerm vs -> vapp vs
CompTerm _ step -> buildStepCount (optRefocus (fapp 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 app f = liftRewrite (rewriteFuncons f) >>= \case
ValTerm vs -> msos_throw (StepOnValue vs)
CompTerm _ step -> app <$> (count_delegation >> optRefocus step)
premiseStep :: Funcons -> MSOS StepRes
premiseStep = premiseStepApp id
----- main `step` function
evalFuncons :: Funcons -> MSOS StepRes
evalFuncons f = liftRewrite (rewriteFuncons f) >>= stepRewritten
rewritesToType :: Funcons -> Rewrite Types
rewritesToType f = do
rewriteFunconsWcount f >>= \case
ValTerm [v@(ComputationType _)] -> return (downcastValueType v)
_ -> rewriteToValErr
rewritesToValue :: Funcons -> Rewrite Values
rewritesToValue f = do
rewriteFunconsWcount f >>= \case
ValTerm [v] -> return v
_ -> rewriteToValErr
rewritesToValues :: Funcons -> Rewrite [Values]
rewritesToValues f = do
rewriteFunconsWcount f >>= \case
ValTerm vs -> return vs
_ -> rewriteToValErr
rewriteToValErr = rewrite_throw $
SideCondFail "side-condition/entity-value/annotation evaluation requires step"
rewriteFunconsWcount :: Funcons -> Rewrite Rewritten
rewriteFunconsWcount f = count_rewrite_attempt >> rewriteFuncons f
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
-- 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 fs) = evalStrictSequence fs (rewritten . setval_) FSet
rewriteFuncons' (FMap fs) = evalStrictSequence fs (rewritten . mapval_) FMap
rewriteFuncons' f@(FBinding fk fv) = evalStrictSequence (fk:fv) (rewritten . tuple) mkBinding
where mkBinding (k:fvs) = FBinding k fvs
mkBinding _ = error "invalid binding-notation"
rewriteFuncons' f@(FSortPower s1 fn) = case (s1,fn) of
(FValue mty@(ComputationType _), FValue v)
| Nat n <- upcastNaturals v ->
rewrittens (replicate (fromInteger n) (ComputationType (Type (downcastValueType mty))))
(FValue mty, _) -> rewriteFuncons fn >>= \case
ValTerm [v] -> rewriteFuncons $ FSortPower s1 (FValue v)
ValTerm _ -> sortErr f "second operand of ^ cannot compute a sequence"
CompTerm _ mf -> flattenApplyWithExc ie (FSortPower s1) mf
where ie = SortErr "^_ multiadic argument"
_ -> rewriteFuncons s1 >>= \case
ValTerm [v] -> rewriteFuncons $ FSortPower (FValue v) fn
ValTerm _ -> sortErr f "first operand of ^ cannot compute a sequence"
CompTerm _ mf -> flattenApplyWithExc ie (flip FSortPower fn) mf
where ie = SortErr "_^ multiadic argument"
rewriteFuncons' f@(FSortSeq s1 op) = case s1 of
(FValue (ComputationType (Type ty))) -> rewritten $ ComputationType $ Type $ AnnotatedType ty op
(FValue _) -> sortErr (FSortSeq s1 op) "sort-sequence operator not on type"
_ -> rewriteFuncons s1 >>= \case
ValTerm [v1] -> rewriteFuncons $ FSortSeq (FValue v1) op
ValTerm vs -> sortErr (FSortSeq s1 op) "operand of sort-sequence operator cannot compute a sequence"
CompTerm _ mf -> flattenApplyWithExc ie (flip FSortSeq op) mf
where ie = SortErr "sort-sequence operator, multiadic argument"
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)
ValTerm vs -> sortErr (FSortComputes f1) "operand of => cannot compute a sequence"
CompTerm _ mf -> flattenApplyWithExc ie FSortComputes mf
where ie = SortErr "=>_ multiadic argument"
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)
ValTerm _ -> sortErr (FSortComputesFrom f1 f2) "second operand of => cannot compute a sequence"
CompTerm _ mf -> flattenApplyWithExc ie (FSortComputesFrom f1) mf
where ie = SortErr "_=>_ multiadic operand (2)"
(_,_)
-> rewriteFuncons f1 >>= \case
ValTerm [v1] -> rewriteFuncons $ FSortComputesFrom (FValue v1) f2
ValTerm _ -> sortErr (FSortComputesFrom f1 f2) "_=>_ multiadic operand (1)"
CompTerm _ mf -> flattenApplyWithExc ie (flip FSortComputesFrom f2) mf
where ie = SortErr "_=>_ multiadic operand (1)"
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, _) -> rewriteFuncons s2 >>= \case
ValTerm [v2] -> rewriteFuncons $ FSortUnion s1 (FValue v2)
ValTerm _ -> sortErr (FSortUnion s1 s2) "sort-union multiadic argument (2)"
CompTerm _ mf -> flattenApplyWithExc ie (FSortUnion s1) mf
where ie = SortErr "sort-union multiadic argument (2)"
_ -> rewriteFuncons s1 >>= \case
ValTerm [v] -> rewriteFuncons $ FSortUnion (FValue v) s2
ValTerm _ -> sortErr (FSortUnion s1 s2) "sort-union multiadic argument (1)"
CompTerm _ mf -> flattenApplyWithExc ie (flip FSortUnion s2) mf
where ie = SortErr "sort-union multiadic argument (1)"
rewriteFuncons' (FSortInter s1 s2) = case (s1, s2) of
(FValue (ComputationType (Type t1))
, FValue (ComputationType (Type t2))) -> rewritten $ typeVal $ Intersection t1 t2
(FValue _, FValue _) -> sortErr (FSortInter s1 s2) "sort-intersection not applied to two sorts"
(FValue v1, _) -> rewriteFuncons s2 >>= \case
ValTerm [v2] -> rewriteFuncons $ FSortInter s1 (FValue v2)
ValTerm _ -> sortErr (FSortInter s1 s2) "sort-intersection multiadic argument (2)"
CompTerm _ mf -> flattenApplyWithExc ie (FSortInter s1) mf
where ie = SortErr "sort-intersection multiadic argument (2)"
_ -> do rewriteFuncons s1 >>= \case
ValTerm [v1] -> rewriteFuncons $ FSortInter (FValue v1) s2
ValTerm _ -> sortErr (FSortInter s1 s2) "sort-intersection multiadic argument (1)"
CompTerm _ mf -> flattenApplyWithExc ie (flip FSortInter s2) mf
where ie = SortErr "sort-intersection multiadic argument (1)"
rewriteFuncons' (FSortComplement s1) = case s1 of
FValue (ComputationType (Type t1)) -> rewritten $ typeVal $ Complement t1
FValue _ -> sortErr (FSortComplement s1) "sort-complement not applied to a sort"
_ -> do rewriteFuncons s1 >>= \case
ValTerm [v] -> rewriteFuncons $ FSortComplement (FValue v)
ValTerm vs -> sortErr (FSortComplement s1) "sort-complement multiadic argument"
CompTerm _ mf -> flattenApplyWithExc ie FSortComplement mf
where ie = SortErr "sort-complement multiadic argument"
rewriteFuncons' (FName nm) =
do mystepf <- lookupFuncon nm
case mystepf of
NullaryFuncon mystep -> mystep
StrictFuncon _ -> rewriteFuncons' (FApp nm [])
ValueOp _ -> rewriteFuncons' (FApp nm [])
_ -> 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: " ++ (showFunconsSeq arg))
ValueOp mystep -> evalStrictSequence arg mystep (applyFuncon nm)
StrictFuncon mystep -> evalStrictSequence arg mystep (applyFuncon nm)
NonStrictFuncon mystep -> mystep arg
PartiallyStrictFuncon strns strn mystep ->
evalSequence (strns ++ repeat strn) arg mystep (applyFuncon nm)
rewriteStrictSequence :: [Funcons] -> Rewrite [Values]
rewriteStrictSequence fs = case rest of
[] -> return (map downcastValue vs)
(x:xs) -> rewriteFuncons x >>= \case
ValTerm vs' -> rewriteStrictSequence (vs++map FValue vs'++xs)
CompTerm f0 mf -> internal ("step on sequence of computations: " ++ show fs)
where (vs, rest) = span (not . hasStep) fs
--OPT: replace by specialised variant of evalSequence
evalStrictSequence :: [Funcons] -> ([Values] -> Rewrite Rewritten) -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence args cont cons =
evalSequence (replicate (length args) Strict) args
(cont . map downcastValue) cons
evalSequence :: [Strictness] -> [Funcons] ->
([Funcons] -> Rewrite Rewritten) -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalSequence strns args cont cons = do
let args_map :: [(Int, (Strictness, Funcons))]
args_map = zip [1..] (zip strns args)
let evalSeqAux args_done args_undone
| null args_undone = cont (map (snd . snd) (sorter args_done))
| otherwise = do
((i,(_,f)), args_undone') <-
maybe_randomRemove NDInterleaving args_undone
let valueCont vs = do
count_rewrite
evalSeqAux args_done' (map bump args_undone')
where args_done' = filter ((<i) . fst) args_done ++
zip [i..] ((zip (replicate (length vs) Strict)
(map FValue vs))) ++
map bump (filter ((>i) . fst) args_done)
bump (k,v) | k > i = (k + length vs - 1, v)
| otherwise = (k,v)
let funconCont stepf = stepf >>= \case
Left f' -> stepTo (cons (remakeArgs args_done [f'] args_undone'))
Right vs' -> stepTo (cons (remakeArgs args_done (map FValue vs') args_undone'))
where remakeArgs m1 l1 m2 =
map (snd . snd) (sorter (filter ((<i) . fst) (m1++m2))) ++ l1 ++
map (snd . snd) (sorter (filter ((>i) . fst) (m1++m2)))
premiseEval valueCont funconCont f
uncurry evalSeqAux (partition (isDone . snd) args_map)
where isDone (NonStrict, _) = True
isDone (Strict, FValue _) = True
isDone (Strict,_) = False
sorter :: [(Int, b)] -> [(Int, b)]
sorter = sortBy (compare `on` fst)
-- | Yield an 'MSOS' computation as a fully rewritten term.
-- This function must be used in order to access entities in the definition
-- of funcons.
compstep :: MSOS StepRes -> Rewrite Rewritten
compstep mf = Rewrite $ \ctxt st ->
let f0 = local_fct ctxt
in (Right (CompTerm f0 mf), st, mempty)
--- transitive closure over steps
stepTrans :: RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans opts i res = case res of
Right vs -> return res
Left f | maybe False ((<= i)) (max_restarts opts) -> return res
| otherwise -> if_abruptly_terminates (do_abrupt_terminate opts)
(stepAndOutput f) return continue
where continue res = count_restart >> stepTrans opts (i+1) res
stepAndOutput :: Funcons -> MSOS StepRes
stepAndOutput f = MSOS $ \ctxt mut ->
let MSOS stepper' = evalFuncons f
stepper ctxt mut = stepper' (setGlobal ctxt) mut
setGlobal ctxt = ctxt
{ ereader = (ereader ctxt) {global_fct = 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')
toStepRes :: Funcons -> StepRes
toStepRes (FValue v) = Right [v]
toStepRes f = Left f
flattenApplyWithExc :: IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc ie app m = compstep $ m >>= \case
Left f -> return $ Left $ app f
Right [v] -> return $ Left $ app (FValue v)
Right vs -> msos_throw ie