{- |
Module      :  ./CASL/Quantification.hs
Description :  Free variables; getting rid of superfluous quantifications
Copyright   :  (c) Till Mossakowski and Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Free variables; getting rid of superfluous quantifications

-}
module CASL.Quantification where

import CASL.AS_Basic_CASL
import CASL.Fold
import CASL.Sign

import Common.AS_Annotation
import Common.Id
import Common.Result
import Common.Utils (nubOrdOn)

import Data.List
import qualified Data.Set as Set
import qualified Data.Map as Map

symbolsRecord :: (f -> Set.Set Symbol)
  -> Record f (Set.Set Symbol) (Set.Set Symbol)
symbolsRecord :: (f -> Set Symbol) -> Record f (Set Symbol) (Set Symbol)
symbolsRecord mf :: f -> Set Symbol
mf = ((f -> Set Symbol)
-> ([Set Symbol] -> Set Symbol)
-> Set Symbol
-> Record f (Set Symbol) (Set Symbol)
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord f -> Set Symbol
mf [Set Symbol] -> Set Symbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions Set Symbol
forall a. Set a
Set.empty)
    { foldPredication :: FORMULA f -> PRED_SYMB -> [Set Symbol] -> Range -> Set Symbol
foldPredication = \ _ p :: PRED_SYMB
p ts :: [Set Symbol]
ts _ -> Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union (case PRED_SYMB
p of
        Qual_pred_name i :: PRED_NAME
i t :: PRED_TYPE
t _ -> Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol)
-> (PredType -> Symbol) -> PredType -> Set Symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. PRED_NAME -> PredType -> Symbol
idToPredSymbol PRED_NAME
i (PredType -> Set Symbol) -> PredType -> Set Symbol
forall a b. (a -> b) -> a -> b
$ PRED_TYPE -> PredType
toPredType PRED_TYPE
t
        Pred_name _ -> Set Symbol
forall a. Set a
Set.empty) (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ [Set Symbol] -> Set Symbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Symbol]
ts
    , foldMembership :: FORMULA f -> Set Symbol -> PRED_NAME -> Range -> Set Symbol
foldMembership = \ _ f :: Set Symbol
f s :: PRED_NAME
s _ -> Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.insert (PRED_NAME -> Symbol
idToSortSymbol PRED_NAME
s) Set Symbol
f
    , foldQual_var :: TERM f -> VAR -> PRED_NAME -> Range -> Set Symbol
foldQual_var = \ _ _ s :: PRED_NAME
s _ -> Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol) -> Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ PRED_NAME -> Symbol
idToSortSymbol PRED_NAME
s
    , foldApplication :: TERM f -> OP_SYMB -> [Set Symbol] -> Range -> Set Symbol
foldApplication = \ _ o :: OP_SYMB
o ts :: [Set Symbol]
ts _ -> Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.union (case OP_SYMB
o of
        Qual_op_name i :: PRED_NAME
i t :: OP_TYPE
t _ -> [Symbol] -> Set Symbol
forall a. Ord a => [a] -> Set a
Set.fromList
          [PRED_NAME -> OpType -> Symbol
idToOpSymbol PRED_NAME
i (OpType -> Symbol) -> OpType -> Symbol
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> OpType
toOpType OP_TYPE
t, PRED_NAME -> Symbol
idToSortSymbol (PRED_NAME -> Symbol) -> PRED_NAME -> Symbol
forall a b. (a -> b) -> a -> b
$ OP_TYPE -> PRED_NAME
res_OP_TYPE OP_TYPE
t]
        Op_name _ -> Set Symbol
forall a. Set a
Set.empty) (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ [Set Symbol] -> Set Symbol
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions [Set Symbol]
ts
    , foldSorted_term :: TERM f -> Set Symbol -> PRED_NAME -> Range -> Set Symbol
foldSorted_term = \ _ t :: Set Symbol
t s :: PRED_NAME
s _ -> Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.insert (PRED_NAME -> Symbol
idToSortSymbol PRED_NAME
s) Set Symbol
t
    , foldCast :: TERM f -> Set Symbol -> PRED_NAME -> Range -> Set Symbol
foldCast = \ _ t :: Set Symbol
t s :: PRED_NAME
s _ -> Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.insert (PRED_NAME -> Symbol
idToSortSymbol PRED_NAME
s) Set Symbol
t
    }

flatVAR_DECLs :: [VAR_DECL] -> [(VAR, SORT)]
flatVAR_DECLs :: [VAR_DECL] -> [(VAR, PRED_NAME)]
flatVAR_DECLs = (VAR_DECL -> [(VAR, PRED_NAME)])
-> [VAR_DECL] -> [(VAR, PRED_NAME)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (\ (Var_decl vs :: [VAR]
vs s :: PRED_NAME
s _) -> (VAR -> (VAR, PRED_NAME)) -> [VAR] -> [(VAR, PRED_NAME)]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: VAR
v -> (VAR
v, PRED_NAME
s)) [VAR]
vs)

freeVarsRecord :: (f -> VarSet) -> Record f VarSet VarSet
freeVarsRecord :: (f -> VarSet) -> Record f VarSet VarSet
freeVarsRecord mf :: f -> VarSet
mf = ((f -> VarSet)
-> ([VarSet] -> VarSet) -> VarSet -> Record f VarSet VarSet
forall f a. (f -> a) -> ([a] -> a) -> a -> Record f a a
constRecord f -> VarSet
mf [VarSet] -> VarSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions VarSet
forall a. Set a
Set.empty)
    { foldQual_var :: TERM f -> VAR -> PRED_NAME -> Range -> VarSet
foldQual_var = \ _ v :: VAR
v s :: PRED_NAME
s _ -> (VAR, PRED_NAME) -> VarSet
forall a. a -> Set a
Set.singleton (VAR
v, PRED_NAME
s)
    , foldQuantification :: FORMULA f -> QUANTIFIER -> [VAR_DECL] -> VarSet -> Range -> VarSet
foldQuantification = \ _ _ vdecl :: [VAR_DECL]
vdecl phiVars :: VarSet
phiVars _ ->
           VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.difference VarSet
phiVars (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$
                    [(VAR, PRED_NAME)] -> VarSet
forall a. Ord a => [a] -> Set a
Set.fromList ([(VAR, PRED_NAME)] -> VarSet) -> [(VAR, PRED_NAME)] -> VarSet
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(VAR, PRED_NAME)]
flatVAR_DECLs [VAR_DECL]
vdecl
    }

freeTermVars :: TermExtension f => Sign f e -> TERM f -> VarSet
freeTermVars :: Sign f e -> TERM f -> VarSet
freeTermVars = Record f VarSet VarSet -> TERM f -> VarSet
forall f a b. Record f a b -> TERM f -> b
foldTerm (Record f VarSet VarSet -> TERM f -> VarSet)
-> (Sign f e -> Record f VarSet VarSet)
-> Sign f e
-> TERM f
-> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> VarSet) -> Record f VarSet VarSet
forall f. (f -> VarSet) -> Record f VarSet VarSet
freeVarsRecord ((f -> VarSet) -> Record f VarSet VarSet)
-> (Sign f e -> f -> VarSet) -> Sign f e -> Record f VarSet VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> f -> VarSet
forall f e. TermExtension f => Sign f e -> f -> VarSet
freeVarsOfExt

freeVars :: TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars :: Sign f e -> FORMULA f -> VarSet
freeVars = Record f VarSet VarSet -> FORMULA f -> VarSet
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f VarSet VarSet -> FORMULA f -> VarSet)
-> (Sign f e -> Record f VarSet VarSet)
-> Sign f e
-> FORMULA f
-> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (f -> VarSet) -> Record f VarSet VarSet
forall f. (f -> VarSet) -> Record f VarSet VarSet
freeVarsRecord ((f -> VarSet) -> Record f VarSet VarSet)
-> (Sign f e -> f -> VarSet) -> Sign f e -> Record f VarSet VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Sign f e -> f -> VarSet
forall f e. TermExtension f => Sign f e -> f -> VarSet
freeVarsOfExt

varSetToDecls :: VarSet -> [VAR_DECL]
varSetToDecls :: VarSet -> [VAR_DECL]
varSetToDecls = ((VAR, PRED_NAME) -> VAR_DECL) -> [(VAR, PRED_NAME)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (v :: VAR
v, s :: PRED_NAME
s) -> [VAR] -> PRED_NAME -> Range -> VAR_DECL
Var_decl [VAR
v] PRED_NAME
s (Range -> VAR_DECL) -> Range -> VAR_DECL
forall a b. (a -> b) -> a -> b
$ VAR -> Range
tokPos VAR
v) ([(VAR, PRED_NAME)] -> [VAR_DECL])
-> (VarSet -> [(VAR, PRED_NAME)]) -> VarSet -> [VAR_DECL]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VarSet -> [(VAR, PRED_NAME)]
forall a. Set a -> [a]
Set.toList

quantFreeVars :: TermExtension f => Sign f e -> FORMULA f -> Range -> FORMULA f
quantFreeVars :: Sign f e -> FORMULA f -> Range -> FORMULA f
quantFreeVars sig :: Sign f e
sig f :: FORMULA f
f =
  Sign f e -> FORMULA f -> FORMULA f
forall f e. TermExtension f => Sign f e -> FORMULA f -> FORMULA f
stripQuant Sign f e
sig (FORMULA f -> FORMULA f)
-> (Range -> FORMULA f) -> Range -> FORMULA f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
mkForallRange (VarSet -> [VAR_DECL]
varSetToDecls (VarSet -> [VAR_DECL]) -> VarSet -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ Sign f e -> FORMULA f -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign f e
sig FORMULA f
f) FORMULA f
f

-- | quantify only over free variables (and only once)
effQuantify :: TermExtension f => Sign f e -> QUANTIFIER -> [VAR_DECL]
            -> FORMULA f -> Range -> FORMULA f
effQuantify :: Sign f e
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
effQuantify sign :: Sign f e
sign q :: QUANTIFIER
q vdecls :: [VAR_DECL]
vdecls phi :: FORMULA f
phi pos :: Range
pos =
    let flatVAR_DECL :: VAR_DECL -> [VAR_DECL]
flatVAR_DECL (Var_decl vs :: [VAR]
vs s :: PRED_NAME
s ps :: Range
ps) =
            (VAR -> VAR_DECL) -> [VAR] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ v :: VAR
v -> [VAR] -> PRED_NAME -> Range -> VAR_DECL
Var_decl [VAR
v] PRED_NAME
s Range
ps) [VAR]
vs
        joinVarDecl :: [VAR_DECL] -> VAR_DECL
joinVarDecl = (VAR_DECL -> VAR_DECL -> VAR_DECL) -> [VAR_DECL] -> VAR_DECL
forall (t :: * -> *) a. Foldable t => (a -> a -> a) -> t a -> a
foldr1 ( \ (Var_decl v1 :: [VAR]
v1 s1 :: PRED_NAME
s1 ps :: Range
ps) (Var_decl v2 :: [VAR]
v2 _s2 :: PRED_NAME
_s2 _) ->
                          [VAR] -> PRED_NAME -> Range -> VAR_DECL
Var_decl ([VAR]
v1 [VAR] -> [VAR] -> [VAR]
forall a. [a] -> [a] -> [a]
++ [VAR]
v2) PRED_NAME
s1 Range
ps)
        cleanDecls :: [VAR_DECL] -> [VAR_DECL]
cleanDecls =
            ([VAR_DECL] -> VAR_DECL) -> [[VAR_DECL]] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map [VAR_DECL] -> VAR_DECL
joinVarDecl ([[VAR_DECL]] -> [VAR_DECL])
-> ([VAR_DECL] -> [[VAR_DECL]]) -> [VAR_DECL] -> [VAR_DECL]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR_DECL] -> [[VAR_DECL]]
myGroup ([VAR_DECL] -> [[VAR_DECL]])
-> ([VAR_DECL] -> [VAR_DECL]) -> [VAR_DECL] -> [[VAR_DECL]]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a]
reverse ([VAR_DECL] -> [VAR_DECL])
-> ([VAR_DECL] -> [VAR_DECL]) -> [VAR_DECL] -> [VAR_DECL]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR_DECL] -> [VAR_DECL]
myNub ([VAR_DECL] -> [VAR_DECL])
-> ([VAR_DECL] -> [VAR_DECL]) -> [VAR_DECL] -> [VAR_DECL]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a]
reverse ([VAR_DECL] -> [VAR_DECL])
-> ([VAR_DECL] -> [VAR_DECL]) -> [VAR_DECL] -> [VAR_DECL]
forall b c a. (b -> c) -> (a -> b) -> a -> c
.
                   (VAR_DECL -> [VAR_DECL]) -> [VAR_DECL] -> [VAR_DECL]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap VAR_DECL -> [VAR_DECL]
flatVAR_DECL
        myGroup :: [VAR_DECL] -> [[VAR_DECL]]
myGroup = (VAR_DECL -> VAR_DECL -> Bool) -> [VAR_DECL] -> [[VAR_DECL]]
forall a. (a -> a -> Bool) -> [a] -> [[a]]
groupBy (\ (Var_decl _ s1 :: PRED_NAME
s1 _) (Var_decl _ s2 :: PRED_NAME
s2 _) -> PRED_NAME
s1 PRED_NAME -> PRED_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PRED_NAME
s2)
        myNub :: [VAR_DECL] -> [VAR_DECL]
myNub = (VAR_DECL -> [VAR]) -> [VAR_DECL] -> [VAR_DECL]
forall b a. Ord b => (a -> b) -> [a] -> [a]
nubOrdOn (\ (Var_decl v :: [VAR]
v _ _) -> [VAR]
v)
        in case QUANTIFIER
q of
           Unique_existential -> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q ([VAR_DECL] -> [VAR_DECL]
cleanDecls [VAR_DECL]
vdecls) FORMULA f
phi Range
pos
           _ -> let fvs :: VarSet
fvs = Sign f e -> FORMULA f -> VarSet
forall f e. TermExtension f => Sign f e -> FORMULA f -> VarSet
freeVars Sign f e
sign FORMULA f
phi
                    filterVAR_DECL :: VAR_DECL -> VAR_DECL
filterVAR_DECL (Var_decl vs :: [VAR]
vs s :: PRED_NAME
s ps :: Range
ps) =
                        [VAR] -> PRED_NAME -> Range -> VAR_DECL
Var_decl ((VAR -> Bool) -> [VAR] -> [VAR]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ v :: VAR
v -> (VAR, PRED_NAME) -> VarSet -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member (VAR
v, PRED_NAME
s) VarSet
fvs
                            Bool -> Bool -> Bool
|| PRED_NAME -> Set PRED_NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member PRED_NAME
s (Sign f e -> Set PRED_NAME
forall f e. Sign f e -> Set PRED_NAME
emptySortSet Sign f e
sign)) [VAR]
vs) PRED_NAME
s Range
ps
                    newDecls :: [VAR_DECL]
newDecls = [VAR_DECL] -> [VAR_DECL]
cleanDecls ([VAR_DECL] -> [VAR_DECL]) -> [VAR_DECL] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ (VAR_DECL -> VAR_DECL) -> [VAR_DECL] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map VAR_DECL -> VAR_DECL
filterVAR_DECL [VAR_DECL]
vdecls
                in if [VAR_DECL] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [VAR_DECL]
newDecls then FORMULA f
phi else
                   QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f.
QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
Quantification QUANTIFIER
q [VAR_DECL]
newDecls FORMULA f
phi Range
pos


stripRecord :: TermExtension f => Sign f e -> (f -> f)
            -> Record f (FORMULA f) (TERM f)
stripRecord :: Sign f e -> (f -> f) -> Record f (FORMULA f) (TERM f)
stripRecord s :: Sign f e
s mf :: f -> f
mf = ((f -> f) -> Record f (FORMULA f) (TERM f)
forall f g. (f -> g) -> Record f (FORMULA g) (TERM g)
mapRecord f -> f
mf)
    { foldQuantification :: FORMULA f
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
foldQuantification = \ _ quant :: QUANTIFIER
quant vdecl :: [VAR_DECL]
vdecl newF :: FORMULA f
newF pos :: Range
pos ->
      let qF :: FORMULA f
qF = Sign f e
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f e.
TermExtension f =>
Sign f e
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
effQuantify Sign f e
s QUANTIFIER
quant [VAR_DECL]
vdecl FORMULA f
newF Range
pos in
      case FORMULA f
newF of
        Quantification quant2 :: QUANTIFIER
quant2 vd2 :: [VAR_DECL]
vd2 f2 :: FORMULA f
f2 ps :: Range
ps ->
            if QUANTIFIER
quant QUANTIFIER -> QUANTIFIER -> Bool
forall a. Eq a => a -> a -> Bool
/= QUANTIFIER
quant2 then FORMULA f
qF else
                Sign f e
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
forall f e.
TermExtension f =>
Sign f e
-> QUANTIFIER -> [VAR_DECL] -> FORMULA f -> Range -> FORMULA f
effQuantify Sign f e
s QUANTIFIER
quant ([VAR_DECL]
vdecl [VAR_DECL] -> [VAR_DECL] -> [VAR_DECL]
forall a. [a] -> [a] -> [a]
++ [VAR_DECL]
vd2) FORMULA f
f2 (Range
pos Range -> Range -> Range
`appRange` Range
ps)
        _ -> FORMULA f
qF
    }

-- | strip superfluous (or nested) quantifications
stripQuant :: TermExtension f => Sign f e -> FORMULA f -> FORMULA f
stripQuant :: Sign f e -> FORMULA f -> FORMULA f
stripQuant s :: Sign f e
s = Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall f a b. Record f a b -> FORMULA f -> a
foldFormula (Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f)
-> Record f (FORMULA f) (TERM f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ Sign f e -> (f -> f) -> Record f (FORMULA f) (TERM f)
forall f e.
TermExtension f =>
Sign f e -> (f -> f) -> Record f (FORMULA f) (TERM f)
stripRecord Sign f e
s f -> f
forall a. a -> a
id

-- | strip all universal quantifications
stripAllQuant :: FORMULA f -> FORMULA f
stripAllQuant :: FORMULA f -> FORMULA f
stripAllQuant f :: FORMULA f
f = case FORMULA f
f of
  Quantification Universal _ phi :: FORMULA f
phi _ -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f
stripAllQuant FORMULA f
phi
  _ -> FORMULA f
f

-- | get top-level variables
getQuantVars :: FORMULA f -> VarSet
getQuantVars :: FORMULA f -> VarSet
getQuantVars f :: FORMULA f
f = case FORMULA f
f of
  Quantification Universal vds :: [VAR_DECL]
vds phi :: FORMULA f
phi _ -> VarSet -> VarSet -> VarSet
forall a. Ord a => Set a -> Set a -> Set a
Set.union
     ([(VAR, PRED_NAME)] -> VarSet
forall a. Ord a => [a] -> Set a
Set.fromList ([(VAR, PRED_NAME)] -> VarSet) -> [(VAR, PRED_NAME)] -> VarSet
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> [(VAR, PRED_NAME)]
flatVAR_DECLs [VAR_DECL]
vds) (VarSet -> VarSet) -> VarSet -> VarSet
forall a b. (a -> b) -> a -> b
$ FORMULA f -> VarSet
forall f. FORMULA f -> VarSet
getQuantVars FORMULA f
phi
  _ -> VarSet
forall a. Set a
Set.empty

-- | get top-level variables for all sentences
getTopVars :: [Named (FORMULA f)] -> VarSet
getTopVars :: [Named (FORMULA f)] -> VarSet
getTopVars = [VarSet] -> VarSet
forall (f :: * -> *) a. (Foldable f, Ord a) => f (Set a) -> Set a
Set.unions ([VarSet] -> VarSet)
-> ([Named (FORMULA f)] -> [VarSet])
-> [Named (FORMULA f)]
-> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Named (FORMULA f) -> VarSet) -> [Named (FORMULA f)] -> [VarSet]
forall a b. (a -> b) -> [a] -> [b]
map (FORMULA f -> VarSet
forall f. FORMULA f -> VarSet
getQuantVars (FORMULA f -> VarSet)
-> (Named (FORMULA f) -> FORMULA f) -> Named (FORMULA f) -> VarSet
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Named (FORMULA f) -> FORMULA f
forall s a. SenAttr s a -> s
sentence)

diffVars :: Map.Map VAR SORT -> VarSet -> Map.Map VAR SORT
diffVars :: Map VAR PRED_NAME -> VarSet -> Map VAR PRED_NAME
diffVars = ((VAR, PRED_NAME) -> Map VAR PRED_NAME -> Map VAR PRED_NAME)
-> Map VAR PRED_NAME -> VarSet -> Map VAR PRED_NAME
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ (v :: VAR
v, s :: PRED_NAME
s) m :: Map VAR PRED_NAME
m -> case VAR -> Map VAR PRED_NAME -> Maybe PRED_NAME
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup VAR
v Map VAR PRED_NAME
m of
    Just t :: PRED_NAME
t | PRED_NAME
t PRED_NAME -> PRED_NAME -> Bool
forall a. Eq a => a -> a -> Bool
== PRED_NAME
s -> VAR -> Map VAR PRED_NAME -> Map VAR PRED_NAME
forall k a. Ord k => k -> Map k a -> Map k a
Map.delete VAR
v Map VAR PRED_NAME
m
    _ -> Map VAR PRED_NAME
m)

warnUnusedVars :: String -> Sign f e -> VarSet -> [Diagnosis]
warnUnusedVars :: String -> Sign f e -> VarSet -> [Diagnosis]
warnUnusedVars msg :: String
msg sig :: Sign f e
sig = (VAR -> Diagnosis) -> [VAR] -> [Diagnosis]
forall a b. (a -> b) -> [a] -> [b]
map (DiagKind -> String -> VAR -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Warning (String -> VAR -> Diagnosis) -> String -> VAR -> Diagnosis
forall a b. (a -> b) -> a -> b
$ "unused" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ "variable")
  ([VAR] -> [Diagnosis])
-> (VarSet -> [VAR]) -> VarSet -> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map VAR PRED_NAME -> [VAR]
forall k a. Map k a -> [k]
Map.keys (Map VAR PRED_NAME -> [VAR])
-> (VarSet -> Map VAR PRED_NAME) -> VarSet -> [VAR]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Map VAR PRED_NAME -> VarSet -> Map VAR PRED_NAME
diffVars (Sign f e -> Map VAR PRED_NAME
forall f e. Sign f e -> Map VAR PRED_NAME
varMap Sign f e
sig)

warnUnused :: Sign f e -> [Named (FORMULA f)] -> [Diagnosis]
warnUnused :: Sign f e -> [Named (FORMULA f)] -> [Diagnosis]
warnUnused sig :: Sign f e
sig = String -> Sign f e -> VarSet -> [Diagnosis]
forall f e. String -> Sign f e -> VarSet -> [Diagnosis]
warnUnusedVars " " Sign f e
sig (VarSet -> [Diagnosis])
-> ([Named (FORMULA f)] -> VarSet)
-> [Named (FORMULA f)]
-> [Diagnosis]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [Named (FORMULA f)] -> VarSet
forall f. [Named (FORMULA f)] -> VarSet
getTopVars