{-# 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 -> [] --error ("saturation error:\n" ++ show 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