{- |
Module : ./CASL/Monoton.hs
Description : monotonicities of the overload relation
Copyright : (c) C. Maeder DFKI Uni Bremen 2002-2005
License : GPLv2 or higher, see LICENSE.txt
Maintainer : Christian.Maeder@dfki.de
Stability : provisional
Portability : portable
computing the monotonicities for functions and predicates in the overload
relation
-}
module CASL.Monoton (monotonicities) where
import qualified Common.Lib.MapSet as MapSet
import Common.AS_Annotation
import Common.Id
import Common.Utils
-- CASL
import CASL.AS_Basic_CASL
import CASL.Sign
import CASL.Overload
monotonicities :: Sign f e -> [Named (FORMULA f)]
monotonicities sig =
concatMap (makeMonos sig) (MapSet.toList $ opMap sig)
++ concatMap (makePredMonos sig) (MapSet.toList $ predMap sig)
makeMonos :: Sign f e -> (Id, [OpType]) -> [Named (FORMULA f)]
makeMonos sig (o, ts) = makeEquivMonos o sig ts
makePredMonos :: Sign f e -> (Id, [PredType]) -> [Named (FORMULA f)]
makePredMonos sig (p, ts) = makeEquivPredMonos p sig ts
makeEquivMonos :: Id -> Sign f e -> [OpType] -> [Named (FORMULA f)]
makeEquivMonos o sig ts = case ts of
[] -> []
t : rs ->
concatMap (makeEquivMono o sig t) rs ++ makeEquivMonos o sig rs
makeEquivPredMonos :: Id -> Sign f e -> [PredType] -> [Named (FORMULA f)]
makeEquivPredMonos o sig ts = case ts of
[] -> []
t : rs ->
concatMap (makeEquivPredMono o sig t) rs ++ makeEquivPredMonos o sig rs
makeEquivMono :: Id -> Sign f e -> OpType -> OpType -> [Named (FORMULA f)]
makeEquivMono o sig o1 o2 =
let rs = minimalSupers sig (opRes o1) (opRes o2)
a1 = opArgs o1
a2 = opArgs o2
args = if length a1 == length a2 then
combine $ zipWith (maximalSubs sig) a1 a2
else []
in concatMap (makeEquivMonoRs o o1 o2 rs) args
makeEquivMonoRs :: Id -> OpType -> OpType -> [SORT] -> [SORT]
-> [Named (FORMULA f)]
makeEquivMonoRs o o1 o2 rs args = map (makeEquivMonoR o o1 o2 args) rs
injectVar :: VAR_DECL -> SORT -> TERM f
injectVar = injectTerm . toQualVar
injectTerm :: TERM f -> SORT -> TERM f
injectTerm t s = if maybe False (== s) $ optSortOfTerm (const Nothing) t
then t else Sorted_term t s nullRange
makeEquivMonoR :: Id -> OpType -> OpType -> [SORT] -> SORT
-> Named (FORMULA f)
makeEquivMonoR o o1 o2 args res =
let vds = map (\ (s, n) -> Var_decl [mkNumVar "x" n] s nullRange)
$ number args
a1 = zipWith injectVar vds $ opArgs o1
a2 = zipWith injectVar vds $ opArgs o2
t1 = injectTerm (Application (Qual_op_name o (toOP_TYPE o1)
nullRange) a1 nullRange) res
t2 = injectTerm (Application (Qual_op_name o (toOP_TYPE o2)
nullRange) a2 nullRange) res
in makeNamed "ga_function_monotonicity" $ mkForall vds $ mkStEq t1 t2
makeEquivPredMono :: Id -> Sign f e -> PredType -> PredType
-> [Named (FORMULA f)]
makeEquivPredMono o sig o1 o2 =
let a1 = predArgs o1
a2 = predArgs o2
args = if length a1 == length a2 then
combine $ zipWith (maximalSubs sig) a1 a2
else []
in map (makeEquivPred o o1 o2) args
makeEquivPred :: Id -> PredType -> PredType -> [SORT] -> Named (FORMULA f)
makeEquivPred o o1 o2 args =
let vds = map (\ (s, n) -> Var_decl [mkNumVar "x" n] s nullRange)
$ number args
a1 = zipWith injectVar vds $ predArgs o1
a2 = zipWith injectVar vds $ predArgs o2
t1 = Predication (Qual_pred_name o (toPRED_TYPE o1) nullRange) a1
nullRange
t2 = Predication (Qual_pred_name o (toPRED_TYPE o2) nullRange) a2
nullRange
in makeNamed "ga_predicate_monotonicity" $ mkForall vds $ mkEqv t1 t2