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 = [Set Var] -> Set Var
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
S.unions ((a -> Set Var) -> [a] -> [Set Var]
forall a b. (a -> b) -> [a] -> [b]
map (Spec -> a -> Set Var
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
_   -> Set Var
forall a. Set a
S.empty
    IntLit Int
_    -> Set Var
forall a. Set a
S.empty
    StringLit String
_ -> Set Var
forall a. Set a
S.empty
    Term
CurrentTime -> Set Var
forall a. Set a
S.empty

    Ref Var
v       -> Var -> Set Var
forall a. a -> Set a
S.singleton Var
v
    App String
d Arguments
args  -> case (TypeSpec -> Domain) -> Maybe TypeSpec -> Maybe Domain
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)  -> ([Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList [Var]
xs Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.difference` [Var] -> Set Var
forall a. Ord a => [a] -> Set a
S.fromList (((Var, Term) -> Var) -> [(Var, Term)] -> [Var]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Term) -> Var
forall a b. (a, b) -> a
fst [(Var, Term)]
replacements))
                                              Set Var -> Set Var -> Set Var
forall a. Ord a => Set a -> Set a -> Set a
`S.union` Spec -> [Term] -> Set Var
forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec (((Var, Term) -> Term) -> [(Var, Term)] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (Var, Term) -> Term
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
_                   -> Spec -> [Term] -> Set Var
forall a. HasVars a => Spec -> a -> Set Var
free Spec
spec (([Term] -> [Term]) -> ([Modifier] -> [Term]) -> Arguments -> [Term]
forall a c b. (a -> c) -> (b -> c) -> Either a b -> c
either [Term] -> [Term]
forall a. a -> a
id ((Modifier -> Term) -> [Modifier] -> [Term]
forall a b. (a -> b) -> [a] -> [b]
map (\(Rename Var
p Term
q) -> Term
q)) Arguments
args)

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

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

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