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