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