{-# LANGUAGE LambdaCase #-}
module Language.EFLINT.Saturation (rebase_and_sat) where
import Language.EFLINT.Spec
import Language.EFLINT.State
import Language.EFLINT.Eval
import Control.Monad (forM)
import Control.Applicative (empty)
import qualified Data.Map as M
import qualified Data.Set as S
rebase_and_sat :: Spec -> State -> State
rebase_and_sat Spec
spec = Spec -> State -> State
saturate Spec
spec forall b c a. (b -> c) -> (a -> b) -> a -> c
. Spec -> State -> State
rebase Spec
spec
rebase :: Spec -> State -> State
rebase :: Spec -> State -> State
rebase Spec
spec State
s = State
s { contents :: Map Tagged Info
contents = forall k a. (k -> a -> Bool) -> Map k a -> Map k a
M.filterWithKey forall {a} {b}. (a, b) -> Info -> Bool
op (State -> Map Tagged Info
contents State
s) }
where op :: (a, b) -> Info -> Bool
op (a
_,b
d) Info
i = Bool -> Bool
not (Info -> Bool
from_sat Info
i)
saturate :: Spec -> State -> State
saturate :: Spec -> State -> State
saturate Spec
spec State
state = case Spec -> State -> State
saturate' Spec
spec State
state of
State
state' | State
state forall a. Eq a => a -> a -> Bool
== State
state' -> State
state
| Bool
otherwise -> Spec -> State -> State
saturate Spec
spec State
state'
where
saturate' :: Spec -> State -> State
saturate' Spec
spec State
s = forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl State -> DomId -> State
op State
s (forall a. Set a -> [a]
S.toList (Spec -> Set DomId
derived Spec
spec))
where op :: State -> DomId -> State
op State
s DomId
d = case Spec -> DomId -> Maybe TypeSpec
find_decl Spec
spec DomId
d of
Maybe TypeSpec
Nothing -> State
s
Just TypeSpec
tdecl -> forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl State -> Derivation -> State
clause State
s (TypeSpec -> [Derivation]
derivation TypeSpec
tdecl)
where clause :: State -> Derivation -> State
clause State
s (HoldsWhen Term
t)
| Products [Var]
xs <- TypeSpec -> Domain
domain TypeSpec
tdecl = [Var] -> Term -> State -> State
derive [Var]
xs (Term -> Term -> Term
When (DomId -> Arguments -> Term
App DomId
d forall a b. (a -> b) -> a -> b
$ forall a b. b -> Either a b
Right []) Term
t) State
s
| Bool
otherwise = [Var] -> Term -> State -> State
derive [DomId -> Var
no_decoration DomId
d] (Term -> Term -> Term
When (Var -> Term
Ref forall a b. (a -> b) -> a -> b
$ DomId -> Var
no_decoration DomId
d) Term
t) State
s
clause State
s (Dv [Var]
xs Term
t) = [Var] -> Term -> State -> State
derive [Var]
xs Term
t State
s
where derive :: [Var] -> Term -> State -> State
derive [Var]
xs Term
t State
s = let dyn :: M_Subs [Tagged]
dyn = do [Tagged]
tes <- forall a. [Var] -> M_Subs a -> M_Subs [a]
foreach [Var]
xs (forall a. M_Subs Value -> (Tagged -> M_Subs a) -> M_Subs a
whenTagged (Term -> M_Subs Value
eval Term
t) forall (m :: * -> *) a. Monad m => a -> m a
return)
forall (t :: * -> *) (m :: * -> *) a b.
(Traversable t, Monad m) =>
t a -> (a -> m b) -> m (t b)
forM [Tagged]
tes forall a b. (a -> b) -> a -> b
$ \Tagged
te -> Tagged -> M_Subs Bool
sat_conditions Tagged
te forall (m :: * -> *) a b. Monad m => m a -> (a -> m b) -> m b
>>= \case
Bool
True -> forall (m :: * -> *) a. Monad m => a -> m a
return Tagged
te
Bool
False -> forall (f :: * -> *) a. Alternative f => f a
empty
ress :: [[Tagged]]
ress = case forall a.
M_Subs a
-> Spec -> State -> InputMap -> Subs -> Either RuntimeError [a]
runSubs M_Subs [Tagged]
dyn Spec
spec State
s forall k a. Map k a
M.empty forall k a. Map k a
M.empty of
Left RuntimeError
err -> []
Right [[Tagged]]
x -> [[Tagged]]
x
in [Tagged] -> State -> State
derive_all (forall (t :: * -> *) a. Foldable t => t [a] -> [a]
concat [[Tagged]]
ress) State
s