{-# LANGUAGE LambdaCase, OverloadedStrings, Rank2Types, TupleSections
, FlexibleInstances #-}
module Funcons.MSOS (
MSOS(..), Rewrite(..), liftRewrite, rewrite_rethrow, rewrite_throw, eval_catch, msos_throw,
EvalFunction(..), Strictness(..), StrictFuncon, PartiallyStrictFuncon,
NonStrictFuncon, ValueOp, NullaryFuncon, RewriteState(..),
StepRes, toStepRes,
Output, readOuts,
Mutable,
Inherited, giveINH,
Control, singleCTRL, giveCTRL,
Input,
applyFuncon, rewritten, rewriteTo, rewriteSeqTo, stepTo, stepSeqTo,rewrittens,
compstep,
norule, exception, sortErr, partialOp, internal, buildStep, sidecond,
premiseStepApp, premiseStep, premiseEval,
SeqSortOp(..),
rewriteRules, stepRules, evalRules, MSOSState(..), emptyMSOSState, emptyRewriteState, MSOSReader(..),RewriteReader(..),showIException, MSOSWriter(..), RewriteWriterr(..),
Rewritten(..), rewriteFuncons, rewriteFunconsWcount, evalFuncons
, stepTrans, stepAndOutput, rewritesToValue, rewritesToValues, rewritesToType
, emptyDCTRL, emptyINH, Interactive(..), SimIO(..)
, rewriteToValErr, count_delegation, optRefocus
, evalStrictSequence, rewriteStrictSequence, evalSequence
, maybe_randomSelect, maybe_randomRemove,
showTypes, showSorts, showValues, showValuesSeq, showFuncons, showFunconsSeq,traceLib,
FunconLibrary, libUnions, libOverrides, libEmpty, libUnion, libOverride, Funcons.MSOS.libFromList,
evalctxt2exception, ctxt2exception, fromSeqValOp, fromNullaryValOp, fromValOp,
displayCounters, counterKeys, ppCounters,
)where
import Funcons.Types
import Funcons.RunOptions
import Funcons.Printer
import Funcons.Exceptions
import Funcons.Simulation
import qualified Funcons.Operations as VAL
import Control.Applicative
import Control.Arrow ((***))
import Control.Monad.Writer hiding ((<>))
import Control.Monad.Fail
import Data.Function (on)
import Data.Maybe (isJust, isNothing, fromJust)
import Data.List (foldl', intercalate, partition, sortBy)
import Data.Text (unpack)
import Data.Semigroup
import qualified Data.Map as M
import System.Random
import System.IO.Unsafe
trace :: p -> p -> p
trace p
p p
b = p
b
traceLib :: FunconLibrary -> FunconLibrary
traceLib :: FunconLibrary -> FunconLibrary
traceLib FunconLibrary
lib = forall a. IO a -> a
unsafePerformIO
([Char] -> IO ()
putStrLn ([[Char]] -> [Char]
unlines (forall a b. (a -> b) -> [a] -> [b]
map Name -> [Char]
unpack (forall k a. Map k a -> [k]
M.keys FunconLibrary
lib))) forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> forall (m :: * -> *) a. Monad m => a -> m a
return FunconLibrary
lib)
type FunconLibrary = M.Map Name EvalFunction
fromValOp :: ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromValOp = Bool
-> ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons)
-> EvalFunction
fromAbsValOp Bool
False
fromSeqValOp :: ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromSeqValOp = Bool
-> ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons)
-> EvalFunction
fromAbsValOp Bool
True
fromAbsValOp :: Bool -> ([Funcons] -> Funcons) -> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromAbsValOp :: Bool
-> ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons)
-> EvalFunction
fromAbsValOp Bool
seqRes [Funcons] -> Funcons
cons [OpExpr Funcons] -> OpExpr Funcons
mkExpr = ValueOp -> EvalFunction
ValueOp ValueOp
op
where op :: ValueOp
op [Values]
vs = Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report Funcons
f Bool
seqRes (forall t. HasValues t => OpExpr t -> EvalResult t
VAL.eval ([OpExpr Funcons] -> OpExpr Funcons
mkExpr (forall a b. (a -> b) -> [a] -> [b]
map forall t. Values t -> OpExpr t
ValExpr [Values]
vs)))
where f :: Funcons
f = [Funcons] -> Funcons
cons (forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs)
fromNullaryValOp :: ([Funcons] -> Funcons) -> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromNullaryValOp :: ([Funcons] -> Funcons)
-> ([OpExpr Funcons] -> OpExpr Funcons) -> EvalFunction
fromNullaryValOp [Funcons] -> Funcons
cons [OpExpr Funcons] -> OpExpr Funcons
mkExpr = Rewrite Rewritten -> EvalFunction
NullaryFuncon Rewrite Rewritten
op
where op :: Rewrite Rewritten
op = Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report ([Funcons] -> Funcons
cons []) Bool
False (forall t. HasValues t => OpExpr t -> EvalResult t
VAL.eval ([OpExpr Funcons] -> OpExpr Funcons
mkExpr []))
report :: Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report :: Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report Funcons
f Bool
seqRes EvalResult Funcons
res = case EvalResult Funcons
res of
Error OpExpr Funcons
_ Result Funcons
dres -> Result Funcons -> Rewrite Rewritten
reportResult Result Funcons
dres
Success (FValue (ADTVal Name
"null" [Funcons]
_)) -> ValueOp
rewrittens []
Success (FValue Values
v) -> Values -> Rewrite Rewritten
rewritten' Values
v
Success Funcons
t -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
t
EvalResults [EvalResult Funcons]
ress -> forall {b}. SourceOfND -> [b] -> Rewrite b
maybe_randomSelect SourceOfND
NDValueOperations [EvalResult Funcons]
ress forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
Funcons -> Bool -> EvalResult Funcons -> Rewrite Rewritten
report Funcons
f Bool
seqRes
where rewritten' :: Values -> Rewrite Rewritten
rewritten' Values
v | Bool
seqRes, ValSeq [Funcons]
fs <- Values
v,
let mvs :: [Maybe Values]
mvs = forall a b. (a -> b) -> [a] -> [b]
map forall t. HasValues t => t -> Maybe (Values t)
project [Funcons]
fs, forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
all forall a. Maybe a -> Bool
isJust [Maybe Values]
mvs
= ValueOp
rewrittens (forall a b. (a -> b) -> [a] -> [b]
map forall a. HasCallStack => Maybe a -> a
fromJust [Maybe Values]
mvs)
| Bool
otherwise = Values -> Rewrite Rewritten
rewritten Values
v
reportResult :: Result Funcons -> Rewrite Rewritten
reportResult Result Funcons
dres = case Result Funcons
dres of
(VAL.SortErr [Char]
str) -> forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
str
(DomErr [Char]
str) -> ValueOp
rewrittens []
(ArityErr [Char]
str) -> forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
str
(ProjErr [Char]
str) -> forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
str
(Normal (FValue Values
v)) -> Values -> Rewrite Rewritten
rewritten' Values
v
(Normal Funcons
t) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
t
(Nondeterministic [Result Funcons]
ress) -> case [Result Funcons]
ress of
[] -> forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
"nondeterminism: empty"
[Result Funcons]
_ -> forall {b}. [b] -> Rewrite b
randomSelect [Result Funcons]
ress forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Result Funcons -> Rewrite Rewritten
reportResult
data EvalFunction =
NonStrictFuncon NonStrictFuncon
| StrictFuncon StrictFuncon
| PartiallyStrictFuncon [Strictness] Strictness NonStrictFuncon
| ValueOp ValueOp
| NullaryFuncon NullaryFuncon
type StrictFuncon = [Values] -> Rewrite Rewritten
type NonStrictFuncon = [Funcons] -> Rewrite Rewritten
type PartiallyStrictFuncon = NonStrictFuncon
type ValueOp = StrictFuncon
type NullaryFuncon = Rewrite Rewritten
data Strictness = Strict | NonStrict
data Rewritten =
ValTerm [Values]
| CompTerm Funcons (MSOS StepRes)
type StepRes = Either Funcons [Values]
instance Show Rewritten where
show :: Rewritten -> [Char]
show (ValTerm [Values]
vs) = [Values] -> [Char]
showValuesSeq [Values]
vs
show (CompTerm Funcons
_ MSOS StepRes
_) = [Char]
"<step>"
libEmpty :: FunconLibrary
libEmpty :: FunconLibrary
libEmpty = forall k a. Map k a
M.empty
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion :: FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion = forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWithKey forall {p} {p} {a}. Name -> p -> p -> a
op
where op :: Name -> p -> p -> a
op Name
k p
x p
_ = forall a. HasCallStack => [Char] -> a
error ([Char]
"duplicate funcon name: " forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
k)
libOverride :: FunconLibrary -> FunconLibrary -> FunconLibrary
libOverride :: FunconLibrary -> FunconLibrary -> FunconLibrary
libOverride = forall a b c. (a -> b -> c) -> b -> a -> c
flip forall k a. Ord k => Map k a -> Map k a -> Map k a
M.union
libUnions :: [FunconLibrary] -> FunconLibrary
libUnions :: [FunconLibrary] -> FunconLibrary
libUnions = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl' FunconLibrary -> FunconLibrary -> FunconLibrary
libUnion FunconLibrary
libEmpty
where op :: p -> p -> a
op p
_ p
_ = forall a. HasCallStack => [Char] -> a
error ([Char]
"duplicate funcon name")
libOverrides :: [FunconLibrary] -> FunconLibrary
libOverrides :: [FunconLibrary] -> FunconLibrary
libOverrides = forall (f :: * -> *) k a.
(Foldable f, Ord k) =>
f (Map k a) -> Map k a
M.unions forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [a] -> [a]
reverse
libFromList :: [(Name, EvalFunction)] -> FunconLibrary
libFromList :: [(Name, EvalFunction)] -> FunconLibrary
libFromList = forall k a. Ord k => [(k, a)] -> Map k a
M.fromList
lookupFuncon :: Name -> Rewrite EvalFunction
lookupFuncon :: Name -> Rewrite EvalFunction
lookupFuncon Name
key = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->
(case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
key (RewriteReader -> FunconLibrary
funconlib RewriteReader
ctxt) of
Just EvalFunction
f -> forall a b. b -> Either a b
Right EvalFunction
f
Maybe EvalFunction
_ -> case forall k a. Ord k => k -> Map k a -> Maybe a
M.lookup Name
key (RunOptions -> BuiltinFunconsOptions
builtin_funcons (RewriteReader -> RunOptions
run_opts RewriteReader
ctxt)) of
Just Funcons
f -> forall a b. b -> Either a b
Right (Rewrite Rewritten -> EvalFunction
NullaryFuncon (Funcons -> Rewrite Rewritten
rewriteTo Funcons
f))
Maybe Funcons
_ -> forall a b. a -> Either a b
Left (IE -> RewriteReader -> IException
evalctxt2exception ([Char] -> IE
Internal ([Char]
"unknown funcon: "forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
key)) RewriteReader
ctxt)
, RewriteState
st, forall a. Monoid a => a
mempty)
data RewriteReader = RewriteReader
{ RewriteReader -> FunconLibrary
funconlib :: FunconLibrary
, RewriteReader -> TypeRelation
ty_env :: TypeRelation, RewriteReader -> RunOptions
run_opts :: RunOptions
, RewriteReader -> Funcons
global_fct :: Funcons, RewriteReader -> Funcons
local_fct :: Funcons }
data RewriteState = RewriteState { RewriteState -> StdGen
random_gen :: StdGen }
emptyRewriteState :: RewriteState
emptyRewriteState = StdGen -> RewriteState
RewriteState (Int -> StdGen
mkStdGen Int
0)
data RewriteWriterr = RewriteWriterr { RewriteWriterr -> Counters
counters :: Counters }
newtype Rewrite a= Rewrite {forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite :: (RewriteReader -> RewriteState ->
(Either IException a, RewriteState, RewriteWriterr))}
instance Applicative Rewrite where
pure :: forall a. a -> Rewrite a
pure = forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: forall a b. Rewrite (a -> b) -> Rewrite a -> Rewrite b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Functor Rewrite where
fmap :: forall a b. (a -> b) -> Rewrite a -> Rewrite b
fmap = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance Monad Rewrite where
return :: forall a. a -> Rewrite a
return a
a = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite (\RewriteReader
_ RewriteState
st -> (forall a b. b -> Either a b
Right a
a, RewriteState
st, forall a. Monoid a => a
mempty))
(Rewrite RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f) >>= :: forall a b. Rewrite a -> (a -> Rewrite b) -> Rewrite b
>>= a -> Rewrite b
k = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite (\RewriteReader
ctxt RewriteState
st ->
let res1 :: (Either IException a, RewriteState, RewriteWriterr)
res1@(Either IException a
e_a1,RewriteState
st1,RewriteWriterr
cs1) = RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f RewriteReader
ctxt RewriteState
st
in case Either IException a
e_a1 of
Left IException
err -> (forall a b. a -> Either a b
Left IException
err, RewriteState
st1, RewriteWriterr
cs1)
Right a
a1 -> let (Rewrite RewriteReader
-> RewriteState
-> (Either IException b, RewriteState, RewriteWriterr)
h) = a -> Rewrite b
k a
a1
(Either IException b
a2,RewriteState
st2,RewriteWriterr
cs2) = RewriteReader
-> RewriteState
-> (Either IException b, RewriteState, RewriteWriterr)
h RewriteReader
ctxt RewriteState
st1
in (Either IException b
a2,RewriteState
st2,RewriteWriterr
cs1 forall a. Semigroup a => a -> a -> a
<> RewriteWriterr
cs2))
instance Semigroup RewriteWriterr where
<> :: RewriteWriterr -> RewriteWriterr -> RewriteWriterr
(<>) = forall a. Monoid a => a -> a -> a
mappend
instance Monoid RewriteWriterr where
mempty :: RewriteWriterr
mempty = Counters -> RewriteWriterr
RewriteWriterr forall a. Monoid a => a
mempty
(RewriteWriterr Counters
cs1) mappend :: RewriteWriterr -> RewriteWriterr -> RewriteWriterr
`mappend` (RewriteWriterr Counters
cs2) = Counters -> RewriteWriterr
RewriteWriterr (Counters
cs1 forall a. Monoid a => a -> a -> a
`mappend` Counters
cs2)
liftRewrite :: Rewrite a -> MSOS a
liftRewrite :: forall a. Rewrite a -> MSOS a
liftRewrite Rewrite a
ev = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
let (Either IException a
e_a, RewriteState
est, RewriteWriterr
ewr) = forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite Rewrite a
ev (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) (forall (m :: * -> *). MSOSState m -> RewriteState
estate MSOSState m
mut)
in forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException a
e_a, MSOSState m
mut {estate :: RewriteState
estate = RewriteState
est}, forall a. Monoid a => a
mempty { ewriter :: RewriteWriterr
ewriter = RewriteWriterr
ewr })
eval_catch :: Rewrite a -> Rewrite (Either IException a)
eval_catch :: forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch Rewrite a
eval = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->
let (Either IException a
eval_res, RewriteState
st', RewriteWriterr
eval_cs) = forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite Rewrite a
eval RewriteReader
ctxt RewriteState
st
in (forall a b. b -> Either a b
Right Either IException a
eval_res, RewriteState
st', RewriteWriterr
eval_cs)
eval_else :: (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else :: forall a. (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else IE -> Bool
prop [] Rewrite a
def = Rewrite a
def
eval_else IE -> Bool
prop (Rewrite a
ev:[Rewrite a]
evs) Rewrite a
def = forall a. Rewrite a -> Rewrite (Either IException a)
eval_catch Rewrite a
ev forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Right a
a -> forall (m :: * -> *) a. Monad m => a -> m a
return a
a
Left (Funcons
gf,Funcons
lf,IE
ie) | IE -> Bool
prop IE
ie -> forall a. (IE -> Bool) -> [Rewrite a] -> Rewrite a -> Rewrite a
eval_else IE -> Bool
prop [Rewrite a]
evs Rewrite a
def
| Bool
otherwise -> forall a. IException -> Rewrite a
rewrite_rethrow (Funcons
gf,Funcons
lf,IE
ie)
rewrite_rethrow :: IException -> Rewrite a
rewrite_rethrow :: forall a. IException -> Rewrite a
rewrite_rethrow IException
ie = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> (forall a b. a -> Either a b
Left IException
ie, RewriteState
st, forall a. Monoid a => a
mempty)
rewrite_throw :: IE -> Rewrite a
rewrite_throw :: forall a. IE -> Rewrite a
rewrite_throw IE
ie = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st -> (forall a b. a -> Either a b
Left (IE -> RewriteReader -> IException
evalctxt2exception IE
ie RewriteReader
ctxt), RewriteState
st, forall a. Monoid a => a
mempty)
evalctxt2exception :: IE -> RewriteReader -> IException
evalctxt2exception :: IE -> RewriteReader -> IException
evalctxt2exception IE
ie RewriteReader
ctxt = (RewriteReader -> Funcons
global_fct RewriteReader
ctxt, RewriteReader -> Funcons
local_fct RewriteReader
ctxt, IE
ie)
ctxt2exception :: IE -> MSOSReader m -> IException
ctxt2exception :: forall (m :: * -> *). IE -> MSOSReader m -> IException
ctxt2exception IE
ie MSOSReader m
ctxt =
(RewriteReader -> Funcons
global_fct (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt), RewriteReader -> Funcons
local_fct (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt), IE
ie)
rewriteRules :: [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules = [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' []
rewriteRules' :: [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' :: [IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' [IException]
errs [] = forall a. IE -> Rewrite a
rewrite_throw ([IException] -> IE
NoMoreBranches [IException]
errs)
rewriteRules' [IException]
errs (Rewrite Rewritten
t1:[Rewrite Rewritten]
ts) = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->
let (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
rw_cs) = forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite Rewrite Rewritten
t1 RewriteReader
ctxt RewriteState
st
in case Either IException Rewritten
rw_res of
Left IException
ie| IException -> Bool
failsRule IException
ie ->
forall {p} {p}. p -> p -> p
trace (IException -> [Char]
showIException IException
ie) forall a b. (a -> b) -> a -> b
$ forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite (do
Rewrite ()
count_backtrack_in
Counters -> Rewrite ()
addToRCounter (RewriteWriterr -> Counters
counters RewriteWriterr
rw_cs)
[IException] -> [Rewrite Rewritten] -> Rewrite Rewritten
rewriteRules' (IException
ieforall a. a -> [a] -> [a]
:[IException]
errs) [Rewrite Rewritten]
ts) RewriteReader
ctxt RewriteState
st
Either IException Rewritten
_ -> (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
rw_cs)
data MSOSReader m = MSOSReader{ forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader :: RewriteReader
, forall (m :: * -> *). MSOSReader m -> Inherited
inh_entities :: Inherited
, forall (m :: * -> *). MSOSReader m -> DownControl
dctrl_entities :: DownControl
, forall (m :: * -> *). MSOSReader m -> Name -> m Funcons
def_fread :: Name -> m Funcons}
data MSOSWriter = MSOSWriter { MSOSWriter -> DownControl
ctrl_entities :: Control, MSOSWriter -> Inherited
out_entities :: Output
, MSOSWriter -> RewriteWriterr
ewriter :: RewriteWriterr }
data MSOSState m = MSOSState { forall (m :: * -> *). MSOSState m -> Input m
inp_es :: Input m, forall (m :: * -> *). MSOSState m -> Inherited
mut_entities :: Mutable
, forall (m :: * -> *). MSOSState m -> RewriteState
estate :: RewriteState }
emptyMSOSState :: Int -> MSOSState m
emptyMSOSState :: forall (m :: * -> *). Int -> MSOSState m
emptyMSOSState Int
seed =
forall (m :: * -> *).
Input m -> Inherited -> RewriteState -> MSOSState m
MSOSState forall k a. Map k a
M.empty forall k a. Map k a
M.empty (RewriteState
emptyRewriteState { random_gen :: StdGen
random_gen = Int -> StdGen
mkStdGen Int
seed })
newtype MSOS a = MSOS { forall a.
MSOS a
-> forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS ::
forall m. Interactive m =>
(MSOSReader m -> MSOSState m
-> m (Either IException a, MSOSState m, MSOSWriter)) }
instance Applicative MSOS where
pure :: forall a. a -> MSOS a
pure = forall (m :: * -> *) a. Monad m => a -> m a
return
<*> :: forall a b. MSOS (a -> b) -> MSOS a -> MSOS b
(<*>) = forall (m :: * -> *) a b. Monad m => m (a -> b) -> m a -> m b
ap
instance Functor MSOS where
fmap :: forall a b. (a -> b) -> MSOS a -> MSOS b
fmap = forall (m :: * -> *) a1 r. Monad m => (a1 -> r) -> m a1 -> m r
liftM
instance Monad MSOS where
return :: forall a. a -> MSOS a
return a
a = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS (\MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right a
a,MSOSState m
mut,forall a. Monoid a => a
mempty))
(MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f) >>= :: forall a b. MSOS a -> (a -> MSOS b) -> MSOS b
>>= a -> MSOS b
k = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS (\MSOSReader m
ctxt MSOSState m
mut -> do
res1 :: (Either IException a, MSOSState m, MSOSWriter)
res1@(Either IException a
e_a1,MSOSState m
mut1,MSOSWriter
wr1) <- forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f MSOSReader m
ctxt MSOSState m
mut
case Either IException a
e_a1 of
Left IException
err -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left IException
err, MSOSState m
mut1, MSOSWriter
wr1)
Right a
a1 -> do
let (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter)
h) = a -> MSOS b
k a
a1
(Either IException b
a2,MSOSState m
mut2,MSOSWriter
wr2) <- forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException b, MSOSState m, MSOSWriter)
h MSOSReader m
ctxt MSOSState m
mut1
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException b
a2,MSOSState m
mut2,MSOSWriter
wr1 forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr2))
instance MonadFail MSOS where
fail :: forall a. [Char] -> MSOS a
fail = forall a. Rewrite a -> MSOS a
liftRewrite forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. [Char] -> Rewrite a
internal
instance Semigroup MSOSWriter where
<> :: MSOSWriter -> MSOSWriter -> MSOSWriter
(<>) = forall a. Monoid a => a -> a -> a
mappend
instance Monoid MSOSWriter where
mempty :: MSOSWriter
mempty = DownControl -> Inherited -> RewriteWriterr -> MSOSWriter
MSOSWriter forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty forall a. Monoid a => a
mempty
(MSOSWriter DownControl
x1 Inherited
x2 RewriteWriterr
x3) mappend :: MSOSWriter -> MSOSWriter -> MSOSWriter
`mappend` (MSOSWriter DownControl
y1 Inherited
y2 RewriteWriterr
y3) =
DownControl -> Inherited -> RewriteWriterr -> MSOSWriter
MSOSWriter (DownControl
x1 forall {a}. Map Name a -> Map Name a -> Map Name a
`unionCTRL` DownControl
y1) (Inherited
x2 Inherited -> Inherited -> Inherited
`unionOUT` Inherited
y2) (RewriteWriterr
x3 forall a. Monoid a => a -> a -> a
`mappend` RewriteWriterr
y3)
type Mutable = M.Map Name [Values]
stepRules :: [IException] -> [MSOS StepRes] -> MSOS StepRes
stepRules = ([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
NoMoreBranches Rewrite ()
count_backtrack_in
stepARules :: ([IException] -> IE) -> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules :: ([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
fexc Rewrite ()
_ [IException]
errs [] = forall b. IE -> MSOS b
msos_throw ([IException] -> IE
fexc [IException]
errs)
stepARules [IException] -> IE
fexc Rewrite ()
counter [IException]
errs [MSOS StepRes]
ts =
forall a. Rewrite a -> MSOS a
liftRewrite (forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
NDRuleSelection [MSOS StepRes]
ts) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>=
\(MSOS StepRes
t1,[MSOS StepRes]
ts) -> forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> do
(Either IException StepRes
e_ie_a, MSOSState m
mut', MSOSWriter
wr) <- forall a.
MSOS a
-> forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS MSOS StepRes
t1 MSOSReader m
ctxt MSOSState m
mut
case Either IException StepRes
e_ie_a of
Left IException
ie | IException -> Bool
failsRule IException
ie ->
forall {p} {p}. p -> p -> p
trace (IException -> [Char]
showIException IException
ie) forall a b. (a -> b) -> a -> b
$ forall a.
MSOS a
-> forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
runMSOS (do
forall a. Rewrite a -> MSOS a
liftRewrite Rewrite ()
counter
Counters -> MSOS ()
addToCounter (RewriteWriterr -> Counters
counters (MSOSWriter -> RewriteWriterr
ewriter MSOSWriter
wr))
([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
fexc Rewrite ()
counter ([IException]
errsforall a. [a] -> [a] -> [a]
++[IException
ie]) [MSOS StepRes]
ts) MSOSReader m
ctxt MSOSState m
mut
Either IException StepRes
_ -> forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_ie_a, MSOSState m
mut', MSOSWriter
wr)
evalRules :: [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules = [IException]
-> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules' []
evalRules' :: [IException] -> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules' :: [IException]
-> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules' [IException]
errs [] [MSOS StepRes]
msoss = MSOS StepRes -> Rewrite Rewritten
buildStep (([IException] -> IE)
-> Rewrite () -> [IException] -> [MSOS StepRes] -> MSOS StepRes
stepARules [IException] -> IE
NoRule Rewrite ()
count_backtrack_out [IException]
errs [MSOS StepRes]
msoss)
evalRules' [IException]
errs [Rewrite Rewritten]
rules [MSOS StepRes]
msoss =
forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
NDRuleSelection [Rewrite Rewritten]
rules forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \((Rewrite RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
rw_rules),[Rewrite Rewritten]
rest) ->
forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->
let (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
wo) = RewriteReader
-> RewriteState
-> (Either IException Rewritten, RewriteState, RewriteWriterr)
rw_rules RewriteReader
ctxt RewriteState
st
in case Either IException Rewritten
rw_res of
Left IException
ie | IException -> Bool
failsRule IException
ie ->
forall {p} {p}. p -> p -> p
trace (IException -> [Char]
showIException IException
ie) forall a b. (a -> b) -> a -> b
$ forall a.
Rewrite a
-> RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
runRewrite (do
Rewrite ()
count_backtrack_out
Counters -> Rewrite ()
addToRCounter (RewriteWriterr -> Counters
counters RewriteWriterr
wo)
[IException]
-> [Rewrite Rewritten] -> [MSOS StepRes] -> Rewrite Rewritten
evalRules' (IException
ieforall a. a -> [a] -> [a]
:[IException]
errs) [Rewrite Rewritten]
rest [MSOS StepRes]
msoss) RewriteReader
ctxt RewriteState
st
Either IException Rewritten
_ -> (Either IException Rewritten
rw_res, RewriteState
st', RewriteWriterr
wo)
msos_throw :: IE -> MSOS b
msos_throw :: forall b. IE -> MSOS b
msos_throw = forall a. Rewrite a -> MSOS a
liftRewrite forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. IE -> Rewrite a
rewrite_throw
giveOpts :: Rewrite RunOptions
giveOpts :: Rewrite RunOptions
giveOpts = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
mut -> (forall a b. b -> Either a b
Right (RewriteReader -> RunOptions
run_opts RewriteReader
ctxt), RewriteState
mut, forall a. Monoid a => a
mempty)
giveINH :: MSOS Inherited
giveINH :: MSOS Inherited
giveINH = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (forall (m :: * -> *). MSOSReader m -> Inherited
inh_entities MSOSReader m
ctxt), MSOSState m
mut, forall a. Monoid a => a
mempty)
giveCTRL :: MSOS DownControl
giveCTRL :: MSOS DownControl
giveCTRL = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (forall (m :: * -> *). MSOSReader m -> DownControl
dctrl_entities MSOSReader m
ctxt), MSOSState m
mut, forall a. Monoid a => a
mempty)
doRefocus :: MSOS Bool
doRefocus :: MSOS Bool
doRefocus = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right forall a b. (a -> b) -> a -> b
$ RunOptions -> Bool
do_refocus (RewriteReader -> RunOptions
run_opts (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt)), MSOSState m
mut, forall a. Monoid a => a
mempty)
modifyRewriteCTXT :: (RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT :: forall a.
(RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT RewriteReader -> RewriteReader
mod (Rewrite RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f) = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite (RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. RewriteReader -> RewriteReader
mod)
modifyRewriteReader :: (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader :: forall a. (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader RewriteReader -> RewriteReader
mod (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f) = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS (forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall {m :: * -> *}. MSOSReader m -> MSOSReader m
mod')
where mod' :: MSOSReader m -> MSOSReader m
mod' MSOSReader m
ctxt = MSOSReader m
ctxt { ereader :: RewriteReader
ereader = RewriteReader -> RewriteReader
mod (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) }
maybe_randomRemove :: SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove :: forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
_ [] = forall a. [a] -> Rewrite (a, [a])
randomRemove []
maybe_randomRemove SourceOfND
src xs :: [a]
xs@(a
x:[a]
xs') = do
RunOptions
opts <- Rewrite RunOptions
giveOpts
if SourceOfND
src forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
`elem` RunOptions -> [SourceOfND]
get_nd_sources RunOptions
opts then forall a. [a] -> Rewrite (a, [a])
randomRemove [a]
xs
else forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, [a]
xs')
randomRemove :: [a] -> Rewrite (a, [a])
randomRemove :: forall a. [a] -> Rewrite (a, [a])
randomRemove [] = forall a. [Char] -> Rewrite a
internal [Char]
"randomRemove: empty list"
randomRemove [a
x]= forall (m :: * -> *) a. Monad m => a -> m a
return (a
x, [])
randomRemove [a]
xs = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
mut ->
let gen :: StdGen
gen = RewriteState -> StdGen
random_gen RewriteState
mut
(Int
i, StdGen
gen') = forall g. RandomGen g => g -> (Int, g)
next StdGen
gen
index :: Int
index = Int
i forall a. Integral a => a -> a -> a
`mod` (forall (t :: * -> *) a. Foldable t => t a -> Int
length [a]
xs)
elem :: a
elem = [a]
xs forall a. [a] -> Int -> a
!! Int
index
rest :: [a]
rest = forall a. Int -> [a] -> [a]
take Int
index [a]
xs forall a. [a] -> [a] -> [a]
++ forall a. Int -> [a] -> [a]
drop (Int
index forall a. Num a => a -> a -> a
+ Int
1) [a]
xs
in (forall a b. b -> Either a b
Right (a
elem, [a]
rest), RewriteState
mut {random_gen :: StdGen
random_gen = StdGen
gen'}, forall a. Monoid a => a
mempty )
maybe_randomSelect :: SourceOfND -> [b] -> Rewrite b
maybe_randomSelect SourceOfND
src [b]
xs = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
src [b]
xs
randomSelect :: [b] -> Rewrite b
randomSelect [b]
xs = forall a b. (a, b) -> a
fst forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. [a] -> Rewrite (a, [a])
randomRemove [b]
xs
type Inherited = M.Map Name [Values]
emptyINH :: Inherited
emptyINH :: Inherited
emptyINH = forall k a. Map k a
M.empty
type Control = M.Map Name (Maybe Values)
type DownControl = M.Map Name (Maybe Values)
emptyDCTRL :: DownControl
emptyDCTRL :: DownControl
emptyDCTRL = forall k a. Map k a
M.empty
emptyCTRL :: Control
emptyCTRL :: DownControl
emptyCTRL = forall k a. Map k a
M.empty
singleCTRL :: Name -> Values -> Control
singleCTRL :: Name -> Values -> DownControl
singleCTRL Name
k = forall k a. k -> a -> Map k a
M.singleton Name
k forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a. a -> Maybe a
Just
unionCTRL :: Map Name a -> Map Name a -> Map Name a
unionCTRL = forall k a.
Ord k =>
(k -> a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWithKey (forall a. HasCallStack => [Char] -> a
error forall b c a. (b -> c) -> (a -> b) -> a -> c
. Name -> [Char]
err)
where err :: Name -> [Char]
err Name
key = [Char]
"Two " forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
key forall a. [a] -> [a] -> [a]
++ [Char]
" signals converging!"
type Output = M.Map Name [Values]
unionOUT :: Output -> Output -> Output
unionOUT :: Inherited -> Inherited -> Inherited
unionOUT = forall k a. Ord k => (a -> a -> a) -> Map k a -> Map k a -> Map k a
M.unionWith forall a. [a] -> [a] -> [a]
(++)
emptyOUT :: Output
emptyOUT :: Inherited
emptyOUT = forall k a. Map k a
M.empty
readOuts :: MSOS a -> MSOS (a, Output)
readOuts :: forall a. MSOS a -> MSOS (a, Inherited)
readOuts (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f) = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ (\MSOSReader m
ctxt MSOSState m
mut -> do
(Either IException a
e_a, MSOSState m
mut1, MSOSWriter
wr1) <- forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter)
f MSOSReader m
ctxt MSOSState m
mut
case Either IException a
e_a of
Left IException
err -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left IException
err, MSOSState m
mut1, MSOSWriter
wr1)
Right a
a -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (a
a,(MSOSWriter -> Inherited
out_entities MSOSWriter
wr1))
, MSOSState m
mut1, MSOSWriter
wr1 { out_entities :: Inherited
out_entities = forall a. Monoid a => a
mempty}))
type Input m = M.Map Name ([[Values]], Maybe (m Funcons))
data Counters = Counters !Int !Int !Int !Int !Int !Int !Int !Int
instance Semigroup Counters where
<> :: Counters -> Counters -> Counters
(<>) = forall a. Monoid a => a -> a -> a
mappend
instance Monoid Counters where
mempty :: Counters
mempty = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0
(Counters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8) mappend :: Counters -> Counters -> Counters
`mappend` (Counters Int
y1 Int
y2 Int
y3 Int
y4 Int
y5 Int
y6 Int
y7 Int
y8) =
Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters (Int
x1forall a. Num a => a -> a -> a
+Int
y1) (Int
x2forall a. Num a => a -> a -> a
+Int
y2) (Int
x3forall a. Num a => a -> a -> a
+Int
y3) (Int
x4forall a. Num a => a -> a -> a
+Int
y4) (Int
x5forall a. Num a => a -> a -> a
+Int
y5) (Int
x6forall a. Num a => a -> a -> a
+Int
y6) (Int
x7forall a. Num a => a -> a -> a
+Int
y7) (Int
x8forall a. Num a => a -> a -> a
+Int
y8)
emptyCounters :: Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8 =
forall a. Monoid a => a
mempty { ewriter :: RewriteWriterr
ewriter = forall a. Monoid a => a
mempty {counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
x1 Int
x2 Int
x3 Int
x4 Int
x5 Int
x6 Int
x7 Int
x8}}
addToCounter :: Counters -> MSOS ()
addToCounter :: Counters -> MSOS ()
addToCounter Counters
cs = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right(), MSOSState m
mut, forall a. Monoid a => a
mempty { ewriter :: RewriteWriterr
ewriter = forall a. Monoid a => a
mempty { counters :: Counters
counters = Counters
cs } })
addToRCounter :: Counters -> Rewrite ()
addToRCounter :: Counters -> Rewrite ()
addToRCounter Counters
cs = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
mut -> (forall a b. b -> Either a b
Right(), RewriteState
mut, forall a. Monoid a => a
mempty { counters :: Counters
counters = Counters
cs })
count_step :: MSOS ()
count_step :: MSOS ()
count_step = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
1 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0)
count_delegation :: MSOS ()
count_delegation :: MSOS ()
count_delegation = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
0 Int
0 Int
0 Int
0 Int
0 Int
1 Int
0 Int
0)
count_refocus :: MSOS ()
count_refocus = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
0 Int
0 Int
0 Int
0 Int
1 Int
0 Int
0 Int
0)
count_restart :: MSOS ()
count_restart :: MSOS ()
count_restart = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
_ MSOSState m
mut -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right (), MSOSState m
mut, Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> MSOSWriter
emptyCounters Int
0 Int
0 Int
0 Int
1 Int
0 Int
0 Int
0 Int
0)
count_rewrite :: Rewrite ()
count_rewrite :: Rewrite ()
count_rewrite = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (forall a b. b -> Either a b
Right (), RewriteState
st, forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
1 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0})
count_rewrite_attempt :: Rewrite ()
count_rewrite_attempt :: Rewrite ()
count_rewrite_attempt = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (forall a b. b -> Either a b
Right (), RewriteState
st, forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
1 Int
0 Int
0 Int
0 Int
0 Int
0})
count_backtrack_out :: Rewrite ()
count_backtrack_out :: Rewrite ()
count_backtrack_out = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (forall a b. b -> Either a b
Right (), RewriteState
st, forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
1 Int
0 })
count_backtrack_in :: Rewrite ()
count_backtrack_in :: Rewrite ()
count_backtrack_in = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
_ RewriteState
st -> (forall a b. b -> Either a b
Right (), RewriteState
st, forall a. Monoid a => a
mempty { counters :: Counters
counters = Int -> Int -> Int -> Int -> Int -> Int -> Int -> Int -> Counters
Counters Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
0 Int
1 })
ppCounters :: Counters -> [Char]
ppCounters Counters
cs =
[Char]
"number of (" forall a. [a] -> [a] -> [a]
++ [Char]
counterKeys forall a. [a] -> [a] -> [a]
++ [Char]
"): (" forall a. [a] -> [a] -> [a]
++ Counters -> [Char]
displayCounters Counters
cs forall a. [a] -> [a] -> [a]
++ [Char]
")"
counterKeys :: [Char]
counterKeys = [Char]
"restarts,rewrites,(attempts),steps,refocus,premises,backtracking(outer),backtracking(inner)"
displayCounters :: Counters -> [Char]
displayCounters (Counters Int
steps Int
rewrites Int
rattempts Int
restarts Int
refocus Int
delegations Int
bout Int
bin) =
forall a. [a] -> [[a]] -> [a]
intercalate [Char]
"," forall a b. (a -> b) -> a -> b
$
forall a b. (a -> b) -> [a] -> [b]
map forall a. Show a => a -> [Char]
show [Int
restarts, Int
rewrites, Int
rattempts, Int
steps, Int
refocus, Int
delegations, Int
bout, Int
bin]
norule :: Funcons -> Rewrite a
norule :: forall a. Funcons -> Rewrite a
norule Funcons
f = forall a. IE -> Rewrite a
rewrite_throw ([IException] -> IE
NoRule [])
sortErr :: Funcons -> String -> Rewrite a
sortErr :: forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
str = forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
SortErr [Char]
str)
partialOp :: Funcons -> String -> Rewrite a
partialOp :: forall a. Funcons -> [Char] -> Rewrite a
partialOp Funcons
f [Char]
str = forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
PartialOp [Char]
str)
exception :: Funcons -> String -> Rewrite a
exception :: forall a. Funcons -> [Char] -> Rewrite a
exception Funcons
f [Char]
str = forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
Err [Char]
str)
internal :: String -> Rewrite a
internal :: forall a. [Char] -> Rewrite a
internal [Char]
str = forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
Internal [Char]
str)
sidecond :: String -> Rewrite a
sidecond :: forall a. [Char] -> Rewrite a
sidecond [Char]
str = forall a. IE -> Rewrite a
rewrite_throw ([Char] -> IE
SideCondFail [Char]
str)
buildStep :: MSOS StepRes -> Rewrite Rewritten
buildStep :: MSOS StepRes -> Rewrite Rewritten
buildStep = MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter (forall (m :: * -> *) a. Monad m => a -> m a
return ())
buildStepCount :: MSOS StepRes -> Rewrite Rewritten
buildStepCount :: MSOS StepRes -> Rewrite Rewritten
buildStepCount = MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter MSOS ()
count_delegation
buildStepCounter :: MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter :: MSOS () -> MSOS StepRes -> Rewrite Rewritten
buildStepCounter MSOS ()
counter MSOS StepRes
mf = MSOS StepRes -> Rewrite Rewritten
compstep (MSOS ()
counter forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes
mf)
optRefocus :: MSOS StepRes -> MSOS StepRes
optRefocus :: MSOS StepRes -> MSOS StepRes
optRefocus MSOS StepRes
stepper = MSOS Bool
doRefocus forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> MSOS StepRes -> MSOS StepRes
refocus MSOS StepRes
stepper
Bool
False -> MSOS StepRes
stepper
refocus :: MSOS StepRes -> MSOS StepRes
refocus :: MSOS StepRes -> MSOS StepRes
refocus MSOS StepRes
stepper
= MSOS ()
count_refocus forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_violates_refocus MSOS StepRes
stepper forall (m :: * -> *) a. Monad m => a -> m a
return StepRes -> MSOS StepRes
continue
where continue :: StepRes -> MSOS StepRes
continue = \case
Right [Values]
vs -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [Values]
vs)
Left Funcons
f ->
forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [Values
v])
ValTerm [Values]
vs -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. a -> Either a b
Left Funcons
f)
Rewritten
res -> MSOS StepRes -> MSOS StepRes
refocus forall a b. (a -> b) -> a -> b
$ Rewritten -> MSOS StepRes
stepRewritten Rewritten
res
stepRewritten :: Rewritten -> MSOS StepRes
stepRewritten :: Rewritten -> MSOS StepRes
stepRewritten (ValTerm [Values]
vs) = forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. b -> Either a b
Right [Values]
vs)
stepRewritten (CompTerm Funcons
f MSOS StepRes
step) = forall a. (RewriteReader -> RewriteReader) -> MSOS a -> MSOS a
modifyRewriteReader RewriteReader -> RewriteReader
mod (MSOS ()
count_step forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes
step)
where mod :: RewriteReader -> RewriteReader
mod RewriteReader
ctxt = RewriteReader
ctxt {local_fct :: Funcons
local_fct = Funcons
f}
rewritten :: Values -> Rewrite Rewritten
rewritten :: Values -> Rewrite Rewritten
rewritten = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Rewritten
ValTerm forall b c a. (b -> c) -> (a -> b) -> a -> c
. (forall a. a -> [a] -> [a]
:[])
rewrittens :: [Values] -> Rewrite Rewritten
rewrittens :: ValueOp
rewrittens = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Rewritten
ValTerm
rewriteTo :: Funcons -> Rewrite Rewritten
rewriteTo :: Funcons -> Rewrite Rewritten
rewriteTo Funcons
f = Rewrite ()
count_rewrite forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f
rewriteSeqTo :: [Funcons] -> Rewrite Rewritten
rewriteSeqTo :: [Funcons] -> Rewrite Rewritten
rewriteSeqTo [Funcons]
fs = Rewrite ()
count_rewrite forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> ([Values] -> Rewritten
ValTerm forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> [Funcons] -> Rewrite [Values]
rewriteStrictSequence [Funcons]
fs)
stepTo :: Funcons -> MSOS StepRes
stepTo :: Funcons -> MSOS StepRes
stepTo = forall (m :: * -> *) a. Monad m => a -> m a
return forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. a -> Either a b
Left
stepSeqTo :: [Funcons] -> MSOS StepRes
stepSeqTo :: [Funcons] -> MSOS StepRes
stepSeqTo [Funcons]
fs = forall a b. b -> Either a b
Right forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> forall a. Rewrite a -> MSOS a
liftRewrite ([Funcons] -> Rewrite [Values]
rewriteStrictSequence [Funcons]
fs)
if_abruptly_terminates :: Bool -> MSOS StepRes -> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes) -> MSOS StepRes
if_abruptly_terminates :: Bool
-> MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_abruptly_terminates Bool
care (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep) StepRes -> MSOS StepRes
abr StepRes -> MSOS StepRes
no_abr = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
(Right StepRes
f', MSOSState m
mut', MSOSWriter
wr') ->
let failed :: Bool
failed = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Maybe a -> Bool
isJust (MSOSWriter -> DownControl
ctrl_entities MSOSWriter
wr')
MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep | Bool
failed Bool -> Bool -> Bool
&& Bool
care = StepRes -> MSOS StepRes
abr StepRes
f'
| Bool
otherwise = StepRes -> MSOS StepRes
no_abr StepRes
f'
in do (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr'') <- forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut'
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr' forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr'')
(Either IException StepRes, MSOSState m, MSOSWriter)
norule_res -> forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res
if_violates_refocus :: MSOS StepRes -> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes) -> MSOS StepRes
if_violates_refocus :: MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_violates_refocus (MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep) StepRes -> MSOS StepRes
viol StepRes -> MSOS StepRes
no_viol = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
(Right StepRes
f', MSOSState m
mut', MSOSWriter
wr') ->
let violates :: Bool
violates = forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any forall a. Maybe a -> Bool
isJust (MSOSWriter -> DownControl
ctrl_entities MSOSWriter
wr')
Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall (t :: * -> *) a. Foldable t => t a -> Bool
null) (MSOSWriter -> Inherited
out_entities MSOSWriter
wr')
Bool -> Bool -> Bool
|| forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (forall a. Maybe a -> Bool
isNothing forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall (m :: * -> *). MSOSState m -> Input m
inp_es MSOSState m
mut')
MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep | Bool
violates = StepRes -> MSOS StepRes
viol StepRes
f'
| Bool
otherwise = StepRes -> MSOS StepRes
no_viol StepRes
f'
in do (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr'') <- forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
fstep MSOSReader m
ctxt MSOSState m
mut'
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
e_f'', MSOSState m
mut'', MSOSWriter
wr' forall a. Semigroup a => a -> a -> a
<> MSOSWriter
wr'')
(Either IException StepRes, MSOSState m, MSOSWriter)
norule_res -> forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes, MSOSState m, MSOSWriter)
norule_res
premiseEval :: ([Values] -> Rewrite Rewritten) -> (MSOS StepRes -> MSOS StepRes) ->
Funcons -> Rewrite Rewritten
premiseEval :: ValueOp
-> (MSOS StepRes -> MSOS StepRes) -> Funcons -> Rewrite Rewritten
premiseEval ValueOp
vapp MSOS StepRes -> MSOS StepRes
fapp Funcons
f = Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values]
vs -> ValueOp
vapp [Values]
vs
CompTerm Funcons
_ MSOS StepRes
step -> MSOS StepRes -> Rewrite Rewritten
buildStepCount (MSOS StepRes -> MSOS StepRes
optRefocus (MSOS StepRes -> MSOS StepRes
fapp MSOS StepRes
step))
premiseStepApp :: (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp :: (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp StepRes -> StepRes
app Funcons
f = forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values]
vs -> forall b. IE -> MSOS b
msos_throw ([Values] -> IE
StepOnValue [Values]
vs)
CompTerm Funcons
_ MSOS StepRes
step -> StepRes -> StepRes
app forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
<$> (MSOS ()
count_delegation forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> MSOS StepRes -> MSOS StepRes
optRefocus MSOS StepRes
step)
premiseStep :: Funcons -> MSOS StepRes
premiseStep :: Funcons -> MSOS StepRes
premiseStep = (StepRes -> StepRes) -> Funcons -> MSOS StepRes
premiseStepApp forall a. a -> a
id
evalFuncons :: Funcons -> MSOS StepRes
evalFuncons :: Funcons -> MSOS StepRes
evalFuncons Funcons
f = forall a. Rewrite a -> MSOS a
liftRewrite (Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f) forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= Rewritten -> MSOS StepRes
stepRewritten
rewritesToType :: Funcons -> Rewrite Types
rewritesToType :: Funcons -> Rewrite Types
rewritesToType Funcons
f = do
Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [v :: Values
v@(ComputationType ComputationTypes Funcons
_)] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall t. Values t -> Types t
downcastValueType Values
v)
Rewritten
_ -> forall {a}. Rewrite a
rewriteToValErr
rewritesToValue :: Funcons -> Rewrite Values
rewritesToValue :: Funcons -> Rewrite Values
rewritesToValue Funcons
f = do
Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v] -> forall (m :: * -> *) a. Monad m => a -> m a
return Values
v
Rewritten
_ -> forall {a}. Rewrite a
rewriteToValErr
rewritesToValues :: Funcons -> Rewrite [Values]
rewritesToValues :: Funcons -> Rewrite [Values]
rewritesToValues Funcons
f = do
Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values]
vs -> forall (m :: * -> *) a. Monad m => a -> m a
return [Values]
vs
Rewritten
_ -> forall {a}. Rewrite a
rewriteToValErr
rewriteToValErr :: Rewrite a
rewriteToValErr = forall a. IE -> Rewrite a
rewrite_throw forall a b. (a -> b) -> a -> b
$
[Char] -> IE
SideCondFail [Char]
"side-condition/entity-value/annotation evaluation requires step"
rewriteFunconsWcount :: Funcons -> Rewrite Rewritten
rewriteFunconsWcount :: Funcons -> Rewrite Rewritten
rewriteFunconsWcount Funcons
f = Rewrite ()
count_rewrite_attempt forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f
rewriteFuncons :: Funcons -> Rewrite Rewritten
rewriteFuncons :: Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f = forall a.
(RewriteReader -> RewriteReader) -> Rewrite a -> Rewrite a
modifyRewriteCTXT (\RewriteReader
ctxt -> RewriteReader
ctxt{local_fct :: Funcons
local_fct = Funcons
f}) (Funcons -> Rewrite Rewritten
rewriteFuncons' Funcons
f)
where
rewriteFuncons' :: Funcons -> Rewrite Rewritten
rewriteFuncons' (FValue Values
v) = forall (m :: * -> *) a. Monad m => a -> m a
return ([Values] -> Rewritten
ValTerm [Values
v])
rewriteFuncons' (FSet [Funcons]
fs) = [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
fs (Values -> Rewrite Rewritten
rewritten forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Values
setval_) [Funcons] -> Funcons
FSet
rewriteFuncons' (FMap [Funcons]
fs) = [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
fs (Values -> Rewrite Rewritten
rewritten forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Values] -> Values
mapval_) [Funcons] -> Funcons
FMap
rewriteFuncons' f :: Funcons
f@(FBinding Funcons
fk [Funcons]
fv) = [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence (Funcons
fkforall a. a -> [a] -> [a]
:[Funcons]
fv) (Values -> Rewrite Rewritten
rewritten forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall t. HasValues t => [Values t] -> Values t
tuple) [Funcons] -> Funcons
mkBinding
where mkBinding :: [Funcons] -> Funcons
mkBinding (Funcons
k:[Funcons]
fvs) = Funcons -> [Funcons] -> Funcons
FBinding Funcons
k [Funcons]
fvs
mkBinding [Funcons]
_ = forall a. HasCallStack => [Char] -> a
error [Char]
"invalid binding-notation"
rewriteFuncons' f :: Funcons
f@(FSortPower Funcons
s1 Funcons
fn) = case (Funcons
s1,Funcons
fn) of
(FValue mty :: Values
mty@(ComputationType ComputationTypes Funcons
_), FValue Values
v)
| Nat Integer
n <- forall t. Values t -> Values t
upcastNaturals Values
v ->
ValueOp
rewrittens (forall a. Int -> a -> [a]
replicate (forall a. Num a => Integer -> a
fromInteger Integer
n) (forall t. ComputationTypes t -> Values t
ComputationType (forall t. Types t -> ComputationTypes t
Type (forall t. Values t -> Types t
downcastValueType Values
mty))))
(FValue Values
mty, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
fn forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortPower Funcons
s1 (Values -> Funcons
FValue Values
v)
ValTerm [Values]
_ -> forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
"second operand of ^ cannot compute a sequence"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortPower Funcons
s1) MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"^_ multiadic argument"
(Funcons, Funcons)
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortPower (Values -> Funcons
FValue Values
v) Funcons
fn
ValTerm [Values]
_ -> forall a. Funcons -> [Char] -> Rewrite a
sortErr Funcons
f [Char]
"first operand of ^ cannot compute a sequence"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortPower Funcons
fn) MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"_^ multiadic argument"
rewriteFuncons' f :: Funcons
f@(FSortSeq Funcons
s1 SeqSortOp
op) = case Funcons
s1 of
(FValue (ComputationType (Type Types
ty))) -> Values -> Rewrite Rewritten
rewritten forall a b. (a -> b) -> a -> b
$ forall t. ComputationTypes t -> Values t
ComputationType forall a b. (a -> b) -> a -> b
$ forall t. Types t -> ComputationTypes t
Type forall a b. (a -> b) -> a -> b
$ forall t. Types t -> SeqSortOp -> Types t
AnnotatedType Types
ty SeqSortOp
op
(FValue Values
_) -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> SeqSortOp -> Funcons
FSortSeq Funcons
s1 SeqSortOp
op) [Char]
"sort-sequence operator not on type"
Funcons
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> SeqSortOp -> Funcons
FSortSeq (Values -> Funcons
FValue Values
v1) SeqSortOp
op
ValTerm [Values]
vs -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> SeqSortOp -> Funcons
FSortSeq Funcons
s1 SeqSortOp
op) [Char]
"operand of sort-sequence operator cannot compute a sequence"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> SeqSortOp -> Funcons
FSortSeq SeqSortOp
op) MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"sort-sequence operator, multiadic argument"
rewriteFuncons' (FSortComputes Funcons
f1) = case Funcons
f1 of
(FValue (ComputationType (Type Types
ty))) -> Values -> Rewrite Rewritten
rewritten forall a b. (a -> b) -> a -> b
$ forall t. ComputationTypes t -> Values t
ComputationType forall a b. (a -> b) -> a -> b
$ forall t. Types t -> ComputationTypes t
ComputesType Types
ty
(FValue Values
_) -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons
FSortComputes Funcons
f1) [Char]
"=> not applied to a type"
Funcons
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
FSortComputes (Values -> Funcons
FValue Values
v1)
ValTerm [Values]
vs -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons
FSortComputes Funcons
f1) [Char]
"operand of => cannot compute a sequence"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie Funcons -> Funcons
FSortComputes MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"=>_ multiadic argument"
rewriteFuncons' (FSortComputesFrom Funcons
f1 Funcons
f2) = case (Funcons
f1,Funcons
f2) of
(FValue (ComputationType (Type Types
ty1)),FValue (ComputationType (Type Types
ty2)))
-> Values -> Rewrite Rewritten
rewritten forall a b. (a -> b) -> a -> b
$ forall t. ComputationTypes t -> Values t
ComputationType (forall t. Types t -> Types t -> ComputationTypes t
ComputesFromType Types
ty1 Types
ty2)
(FValue Values
_, FValue Values
_) -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) [Char]
"=> not applied to types"
(FValue (ComputationType (Type Types
ty1)),Funcons
_)
-> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f2 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 (Values -> Funcons
FValue Values
v2)
ValTerm [Values]
_ -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) [Char]
"second operand of => cannot compute a sequence"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1) MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"_=>_ multiadic operand (2)"
(Funcons
_,Funcons
_)
-> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
f1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortComputesFrom (Values -> Funcons
FValue Values
v1) Funcons
f2
ValTerm [Values]
_ -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f1 Funcons
f2) [Char]
"_=>_ multiadic operand (1)"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortComputesFrom Funcons
f2) MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"_=>_ multiadic operand (1)"
rewriteFuncons' (FSortUnion Funcons
s1 Funcons
s2) = case (Funcons
s1, Funcons
s2) of
(FValue (ComputationType (Type Types
t1))
, FValue (ComputationType (Type Types
t2))) -> Values -> Rewrite Rewritten
rewritten forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal forall a b. (a -> b) -> a -> b
$ forall t. Types t -> Types t -> Types t
Union Types
t1 Types
t2
(FValue Values
_, FValue Values
_) -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) [Char]
"sort-union not applied to two sorts"
(FValue Values
v1, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s2 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 (Values -> Funcons
FValue Values
v2)
ValTerm [Values]
_ -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) [Char]
"sort-union multiadic argument (2)"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1) MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"sort-union multiadic argument (2)"
(Funcons, Funcons)
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortUnion (Values -> Funcons
FValue Values
v) Funcons
s2
ValTerm [Values]
_ -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortUnion Funcons
s1 Funcons
s2) [Char]
"sort-union multiadic argument (1)"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortUnion Funcons
s2) MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"sort-union multiadic argument (1)"
rewriteFuncons' (FSortInter Funcons
s1 Funcons
s2) = case (Funcons
s1, Funcons
s2) of
(FValue (ComputationType (Type Types
t1))
, FValue (ComputationType (Type Types
t2))) -> Values -> Rewrite Rewritten
rewritten forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal forall a b. (a -> b) -> a -> b
$ forall t. Types t -> Types t -> Types t
Intersection Types
t1 Types
t2
(FValue Values
_, FValue Values
_) -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) [Char]
"sort-intersection not applied to two sorts"
(FValue Values
v1, Funcons
_) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s2 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v2] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 (Values -> Funcons
FValue Values
v2)
ValTerm [Values]
_ -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) [Char]
"sort-intersection multiadic argument (2)"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1) MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"sort-intersection multiadic argument (2)"
(Funcons, Funcons)
_ -> do Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v1] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons -> Funcons
FSortInter (Values -> Funcons
FValue Values
v1) Funcons
s2
ValTerm [Values]
_ -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons -> Funcons
FSortInter Funcons
s1 Funcons
s2) [Char]
"sort-intersection multiadic argument (1)"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie (forall a b c. (a -> b -> c) -> b -> a -> c
flip Funcons -> Funcons -> Funcons
FSortInter Funcons
s2) MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"sort-intersection multiadic argument (1)"
rewriteFuncons' (FSortComplement Funcons
s1) = case Funcons
s1 of
FValue (ComputationType (Type Types
t1)) -> Values -> Rewrite Rewritten
rewritten forall a b. (a -> b) -> a -> b
$ Types -> Values
typeVal forall a b. (a -> b) -> a -> b
$ forall t. Types t -> Types t
Complement Types
t1
FValue Values
_ -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons
FSortComplement Funcons
s1) [Char]
"sort-complement not applied to a sort"
Funcons
_ -> do Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
s1 forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values
v] -> Funcons -> Rewrite Rewritten
rewriteFuncons forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
FSortComplement (Values -> Funcons
FValue Values
v)
ValTerm [Values]
vs -> forall a. Funcons -> [Char] -> Rewrite a
sortErr (Funcons -> Funcons
FSortComplement Funcons
s1) [Char]
"sort-complement multiadic argument"
CompTerm Funcons
_ MSOS StepRes
mf -> IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie Funcons -> Funcons
FSortComplement MSOS StepRes
mf
where ie :: IE
ie = [Char] -> IE
SortErr [Char]
"sort-complement multiadic argument"
rewriteFuncons' (FName Name
nm) =
do EvalFunction
mystepf <- Name -> Rewrite EvalFunction
lookupFuncon Name
nm
case EvalFunction
mystepf of
NullaryFuncon Rewrite Rewritten
mystep -> Rewrite Rewritten
mystep
StrictFuncon ValueOp
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons' (Name -> [Funcons] -> Funcons
FApp Name
nm [])
ValueOp ValueOp
_ -> Funcons -> Rewrite Rewritten
rewriteFuncons' (Name -> [Funcons] -> Funcons
FApp Name
nm [])
EvalFunction
_ -> forall a. HasCallStack => [Char] -> a
error ([Char]
"funcon " forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
nm forall a. [a] -> [a] -> [a]
++ [Char]
" not applied to any arguments")
rewriteFuncons' (FApp Name
nm [Funcons]
arg) =
do EvalFunction
mystepf <- Name -> Rewrite EvalFunction
lookupFuncon Name
nm
case EvalFunction
mystepf of
NullaryFuncon Rewrite Rewritten
_ -> forall a. Funcons -> [Char] -> Rewrite a
exception (Name -> [Funcons] -> Funcons
FApp Name
nm [Funcons]
arg) ([Char]
"nullary funcon " forall a. [a] -> [a] -> [a]
++ Name -> [Char]
unpack Name
nm forall a. [a] -> [a] -> [a]
++ [Char]
" applied to arguments: " forall a. [a] -> [a] -> [a]
++ ([Funcons] -> [Char]
showFunconsSeq [Funcons]
arg))
ValueOp ValueOp
mystep -> [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
arg ValueOp
mystep (Name -> [Funcons] -> Funcons
applyFuncon Name
nm)
StrictFuncon ValueOp
mystep -> [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
arg ValueOp
mystep (Name -> [Funcons] -> Funcons
applyFuncon Name
nm)
NonStrictFuncon [Funcons] -> Rewrite Rewritten
mystep -> [Funcons] -> Rewrite Rewritten
mystep [Funcons]
arg
PartiallyStrictFuncon [Strictness]
strns Strictness
strn [Funcons] -> Rewrite Rewritten
mystep ->
[Strictness]
-> [Funcons]
-> ([Funcons] -> Rewrite Rewritten)
-> ([Funcons] -> Funcons)
-> Rewrite Rewritten
evalSequence ([Strictness]
strns forall a. [a] -> [a] -> [a]
++ forall a. a -> [a]
repeat Strictness
strn) [Funcons]
arg [Funcons] -> Rewrite Rewritten
mystep (Name -> [Funcons] -> Funcons
applyFuncon Name
nm)
rewriteStrictSequence :: [Funcons] -> Rewrite [Values]
rewriteStrictSequence :: [Funcons] -> Rewrite [Values]
rewriteStrictSequence [Funcons]
fs = case [Funcons]
rest of
[] -> forall (m :: * -> *) a. Monad m => a -> m a
return (forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values
downcastValue [Funcons]
vs)
(Funcons
x:[Funcons]
xs) -> Funcons -> Rewrite Rewritten
rewriteFuncons Funcons
x forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
ValTerm [Values]
vs' -> [Funcons] -> Rewrite [Values]
rewriteStrictSequence ([Funcons]
vsforall a. [a] -> [a] -> [a]
++forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs'forall a. [a] -> [a] -> [a]
++[Funcons]
xs)
CompTerm Funcons
f0 MSOS StepRes
mf -> forall a. [Char] -> Rewrite a
internal ([Char]
"step on sequence of computations: " forall a. [a] -> [a] -> [a]
++ forall a. Show a => a -> [Char]
show [Funcons]
fs)
where ([Funcons]
vs, [Funcons]
rest) = forall a. (a -> Bool) -> [a] -> ([a], [a])
span (Bool -> Bool
not forall b c a. (b -> c) -> (a -> b) -> a -> c
. Funcons -> Bool
hasStep) [Funcons]
fs
evalStrictSequence :: [Funcons] -> ([Values] -> Rewrite Rewritten) -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence :: [Funcons] -> ValueOp -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalStrictSequence [Funcons]
args ValueOp
cont [Funcons] -> Funcons
cons =
[Strictness]
-> [Funcons]
-> ([Funcons] -> Rewrite Rewritten)
-> ([Funcons] -> Funcons)
-> Rewrite Rewritten
evalSequence (forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Funcons]
args) Strictness
Strict) [Funcons]
args
(ValueOp
cont forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a -> b) -> [a] -> [b]
map Funcons -> Values
downcastValue) [Funcons] -> Funcons
cons
evalSequence :: [Strictness] -> [Funcons] ->
([Funcons] -> Rewrite Rewritten) -> ([Funcons] -> Funcons) -> Rewrite Rewritten
evalSequence :: [Strictness]
-> [Funcons]
-> ([Funcons] -> Rewrite Rewritten)
-> ([Funcons] -> Funcons)
-> Rewrite Rewritten
evalSequence [Strictness]
strns [Funcons]
args [Funcons] -> Rewrite Rewritten
cont [Funcons] -> Funcons
cons = do
let args_map :: [(Int, (Strictness, Funcons))]
args_map = forall a b. [a] -> [b] -> [(a, b)]
zip [Int
1..] (forall a b. [a] -> [b] -> [(a, b)]
zip [Strictness]
strns [Funcons]
args)
let evalSeqAux :: [(Int, (Strictness, Funcons))]
-> [(Int, (Strictness, Funcons))] -> Rewrite Rewritten
evalSeqAux [(Int, (Strictness, Funcons))]
args_done [(Int, (Strictness, Funcons))]
args_undone
| forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Int, (Strictness, Funcons))]
args_undone = [Funcons] -> Rewrite Rewritten
cont (forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall {b}. [(Int, b)] -> [(Int, b)]
sorter [(Int, (Strictness, Funcons))]
args_done))
| Bool
otherwise = do
((Int
i,(Strictness
_,Funcons
f)), [(Int, (Strictness, Funcons))]
args_undone') <-
forall a. SourceOfND -> [a] -> Rewrite (a, [a])
maybe_randomRemove SourceOfND
NDInterleaving [(Int, (Strictness, Funcons))]
args_undone
let valueCont :: ValueOp
valueCont [Values]
vs = do
Rewrite ()
count_rewrite
[(Int, (Strictness, Funcons))]
-> [(Int, (Strictness, Funcons))] -> Rewrite Rewritten
evalSeqAux [(Int, (Strictness, Funcons))]
args_done' (forall a b. (a -> b) -> [a] -> [b]
map forall {b}. (Int, b) -> (Int, b)
bump [(Int, (Strictness, Funcons))]
args_undone')
where args_done' :: [(Int, (Strictness, Funcons))]
args_done' = forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
<Int
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Int, (Strictness, Funcons))]
args_done forall a. [a] -> [a] -> [a]
++
forall a b. [a] -> [b] -> [(a, b)]
zip [Int
i..] ((forall a b. [a] -> [b] -> [(a, b)]
zip (forall a. Int -> a -> [a]
replicate (forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values]
vs) Strictness
Strict)
(forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs))) forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map forall {b}. (Int, b) -> (Int, b)
bump (forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
>Int
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) [(Int, (Strictness, Funcons))]
args_done)
bump :: (Int, b) -> (Int, b)
bump (Int
k,b
v) | Int
k forall a. Ord a => a -> a -> Bool
> Int
i = (Int
k forall a. Num a => a -> a -> a
+ forall (t :: * -> *) a. Foldable t => t a -> Int
length [Values]
vs forall a. Num a => a -> a -> a
- Int
1, b
v)
| Bool
otherwise = (Int
k,b
v)
let funconCont :: MSOS StepRes -> MSOS StepRes
funconCont MSOS StepRes
stepf = MSOS StepRes
stepf forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left Funcons
f' -> Funcons -> MSOS StepRes
stepTo ([Funcons] -> Funcons
cons (forall {a} {a}. [(Int, (a, a))] -> [a] -> [(Int, (a, a))] -> [a]
remakeArgs [(Int, (Strictness, Funcons))]
args_done [Funcons
f'] [(Int, (Strictness, Funcons))]
args_undone'))
Right [Values]
vs' -> Funcons -> MSOS StepRes
stepTo ([Funcons] -> Funcons
cons (forall {a} {a}. [(Int, (a, a))] -> [a] -> [(Int, (a, a))] -> [a]
remakeArgs [(Int, (Strictness, Funcons))]
args_done (forall a b. (a -> b) -> [a] -> [b]
map Values -> Funcons
FValue [Values]
vs') [(Int, (Strictness, Funcons))]
args_undone'))
where remakeArgs :: [(Int, (a, a))] -> [a] -> [(Int, (a, a))] -> [a]
remakeArgs [(Int, (a, a))]
m1 [a]
l1 [(Int, (a, a))]
m2 =
forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall {b}. [(Int, b)] -> [(Int, b)]
sorter (forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
<Int
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) ([(Int, (a, a))]
m1forall a. [a] -> [a] -> [a]
++[(Int, (a, a))]
m2))) forall a. [a] -> [a] -> [a]
++ [a]
l1 forall a. [a] -> [a] -> [a]
++
forall a b. (a -> b) -> [a] -> [b]
map (forall a b. (a, b) -> b
snd forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) (forall {b}. [(Int, b)] -> [(Int, b)]
sorter (forall a. (a -> Bool) -> [a] -> [a]
filter ((forall a. Ord a => a -> a -> Bool
>Int
i) forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> a
fst) ([(Int, (a, a))]
m1forall a. [a] -> [a] -> [a]
++[(Int, (a, a))]
m2)))
ValueOp
-> (MSOS StepRes -> MSOS StepRes) -> Funcons -> Rewrite Rewritten
premiseEval ValueOp
valueCont MSOS StepRes -> MSOS StepRes
funconCont Funcons
f
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry [(Int, (Strictness, Funcons))]
-> [(Int, (Strictness, Funcons))] -> Rewrite Rewritten
evalSeqAux (forall a. (a -> Bool) -> [a] -> ([a], [a])
partition ((Strictness, Funcons) -> Bool
isDone forall b c a. (b -> c) -> (a -> b) -> a -> c
. forall a b. (a, b) -> b
snd) [(Int, (Strictness, Funcons))]
args_map)
where isDone :: (Strictness, Funcons) -> Bool
isDone (Strictness
NonStrict, Funcons
_) = Bool
True
isDone (Strictness
Strict, FValue Values
_) = Bool
True
isDone (Strictness
Strict,Funcons
_) = Bool
False
sorter :: [(Int, b)] -> [(Int, b)]
sorter = forall a. (a -> a -> Ordering) -> [a] -> [a]
sortBy (forall a. Ord a => a -> a -> Ordering
compare forall b c a. (b -> b -> c) -> (a -> b) -> a -> a -> c
`on` forall a b. (a, b) -> a
fst)
compstep :: MSOS StepRes -> Rewrite Rewritten
compstep :: MSOS StepRes -> Rewrite Rewritten
compstep MSOS StepRes
mf = forall a.
(RewriteReader
-> RewriteState
-> (Either IException a, RewriteState, RewriteWriterr))
-> Rewrite a
Rewrite forall a b. (a -> b) -> a -> b
$ \RewriteReader
ctxt RewriteState
st ->
let f0 :: Funcons
f0 = RewriteReader -> Funcons
local_fct RewriteReader
ctxt
in (forall a b. b -> Either a b
Right (Funcons -> MSOS StepRes -> Rewritten
CompTerm Funcons
f0 MSOS StepRes
mf), RewriteState
st, forall a. Monoid a => a
mempty)
stepTrans :: RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans :: RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans RunOptions
opts Int
i StepRes
res = case StepRes
res of
Right [Values]
vs -> forall (m :: * -> *) a. Monad m => a -> m a
return StepRes
res
Left Funcons
f | forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False ((forall a. Ord a => a -> a -> Bool
<= Int
i)) (RunOptions -> Maybe Int
max_restarts RunOptions
opts) -> forall (m :: * -> *) a. Monad m => a -> m a
return StepRes
res
| Bool
otherwise -> Bool
-> MSOS StepRes
-> (StepRes -> MSOS StepRes)
-> (StepRes -> MSOS StepRes)
-> MSOS StepRes
if_abruptly_terminates (RunOptions -> Bool
do_abrupt_terminate RunOptions
opts)
(Funcons -> MSOS StepRes
stepAndOutput Funcons
f) forall (m :: * -> *) a. Monad m => a -> m a
return StepRes -> MSOS StepRes
continue
where continue :: StepRes -> MSOS StepRes
continue StepRes
res = MSOS ()
count_restart forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> RunOptions -> Int -> StepRes -> MSOS StepRes
stepTrans RunOptions
opts (Int
iforall a. Num a => a -> a -> a
+Int
1) StepRes
res
stepAndOutput :: Funcons -> MSOS StepRes
stepAndOutput :: Funcons -> MSOS StepRes
stepAndOutput Funcons
f = forall a.
(forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m -> m (Either IException a, MSOSState m, MSOSWriter))
-> MSOS a
MSOS forall a b. (a -> b) -> a -> b
$ \MSOSReader m
ctxt MSOSState m
mut ->
let MSOS forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper' = Funcons -> MSOS StepRes
evalFuncons Funcons
f
stepper :: MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper MSOSReader m
ctxt MSOSState m
mut = forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper' (forall {m :: * -> *}. MSOSReader m -> MSOSReader m
setGlobal MSOSReader m
ctxt) MSOSState m
mut
setGlobal :: MSOSReader m -> MSOSReader m
setGlobal MSOSReader m
ctxt = MSOSReader m
ctxt
{ ereader :: RewriteReader
ereader = (forall (m :: * -> *). MSOSReader m -> RewriteReader
ereader MSOSReader m
ctxt) {global_fct :: Funcons
global_fct = Funcons
f }}
in do (Either IException StepRes
eres,MSOSState m
mut',MSOSWriter
wr') <- forall (m :: * -> *).
Interactive m =>
MSOSReader m
-> MSOSState m
-> m (Either IException StepRes, MSOSState m, MSOSWriter)
stepper MSOSReader m
ctxt MSOSState m
mut
forall (t :: * -> *) (m :: * -> *) a b.
(Foldable t, Monad m) =>
(a -> m b) -> t a -> m ()
mapM_ (forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry forall (m :: * -> *). Interactive m => Name -> Values -> m ()
fprint)
[ (Name
entity,Values
val)
| (Name
entity, [Values]
vals) <- forall k a. Map k a -> [(k, a)]
M.assocs (MSOSWriter -> Inherited
out_entities MSOSWriter
wr')
, Values
val <- [Values]
vals ]
forall (m :: * -> *) a. Monad m => a -> m a
return (Either IException StepRes
eres, MSOSState m
mut', MSOSWriter
wr')
toStepRes :: Funcons -> StepRes
toStepRes :: Funcons -> StepRes
toStepRes (FValue Values
v) = forall a b. b -> Either a b
Right [Values
v]
toStepRes Funcons
f = forall a b. a -> Either a b
Left Funcons
f
flattenApplyWithExc :: IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc :: IE -> (Funcons -> Funcons) -> MSOS StepRes -> Rewrite Rewritten
flattenApplyWithExc IE
ie Funcons -> Funcons
app MSOS StepRes
m = MSOS StepRes -> Rewrite Rewritten
compstep forall a b. (a -> b) -> a -> b
$ MSOS StepRes
m forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Left Funcons
f -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
app Funcons
f
Right [Values
v] -> forall (m :: * -> *) a. Monad m => a -> m a
return forall a b. (a -> b) -> a -> b
$ forall a b. a -> Either a b
Left forall a b. (a -> b) -> a -> b
$ Funcons -> Funcons
app (Values -> Funcons
FValue Values
v)
Right [Values]
vs -> forall b. IE -> MSOS b
msos_throw IE
ie