module Language.EFLINT.Binders where

import Language.EFLINT.Spec

import qualified Data.Set as S

class HasVars a where
  free :: Spec -> a -> S.Set Var

instance HasVars a => HasVars [a] where
  free :: Spec -> [a] -> Set Var
free Spec
spec [a]
as = forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions (forall a b. (a -> b) -> [a] -> [b]
map (forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec) [a]
as)

instance HasVars Term where
  free :: Spec -> Term -> Set Var
free Spec
spec Term
t = case Term
t of
    BoolLit Bool
_   -> forall a. Set a
S.empty
    IntLit Int
_    -> forall a. Set a
S.empty
    StringLit String
_ -> forall a. Set a
S.empty
    Term
CurrentTime -> forall a. Set a
S.empty

    Ref Var
v       -> forall a. a -> Set a
S.singleton Var
v
    App String
d Arguments
args  -> case forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap TypeSpec -> Domain
domain (Spec -> String -> Maybe TypeSpec
find_decl Spec
spec String
d) of
                    Just (Products [Var]
xs)  -> (forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> a
fst [(Var, Term)]
replacements))
                                              forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec (forall a b. (a -> b) -> [a] -> [b]
map forall a b. (a, b) -> b
snd [(Var, Term)]
replacements)
                      where replacements :: [(Var, Term)]
replacements = [Var] -> Arguments -> [(Var, Term)]
make_substitutions_of [Var]
xs Arguments
args 
                    Maybe Domain
_                   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec (forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either forall a. a -> a
id (forall a b. (a -> b) -> [a] -> [b]
map (\(Rename Var
p Term
q) -> Term
q)) Arguments
args)

    Not Term
t       -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t
    Present Term
t   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t
    Violated Term
t  -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t
    Enabled Term
t  -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t
    Project Term
t Var
x -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t
    Tag Term
t String
x     -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t
    Untag Term
t     -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t

    And Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Or  Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Leq Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Geq Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Ge  Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Le  Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Mult Term
t1 Term
t2  -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Mod Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Div  Term
t1 Term
t2  -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Sub Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Add Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Eq  Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    Neq Term
t1 Term
t2   -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2
    When Term
t1 Term
t2  -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t1 forall a. Ord a => Set a -> Set a -> Set a
`S.union` forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t2

    Exists [Var]
xs Term
t -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs
    Forall [Var]
xs Term
t -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs
    Count  [Var]
xs Term
t -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs
    Max    [Var]
xs Term
t -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs
    Min    [Var]
xs Term
t -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs
    Sum    [Var]
xs Term
t -> forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec Term
t forall a. Ord a => Set a -> Set a -> Set a
`S.difference` forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs