{- |
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 :: Sign f e -> [Named (FORMULA f)]
monotonicities sig :: Sign f e
sig =
    ((Id, [OpType]) -> [Named (FORMULA f)])
-> [(Id, [OpType])] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Sign f e -> (Id, [OpType]) -> [Named (FORMULA f)]
forall f e. Sign f e -> (Id, [OpType]) -> [Named (FORMULA f)]
makeMonos Sign f e
sig) (MapSet Id OpType -> [(Id, [OpType])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList (MapSet Id OpType -> [(Id, [OpType])])
-> MapSet Id OpType -> [(Id, [OpType])]
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
sig)
    [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ ((Id, [PredType]) -> [Named (FORMULA f)])
-> [(Id, [PredType])] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Sign f e -> (Id, [PredType]) -> [Named (FORMULA f)]
forall f e. Sign f e -> (Id, [PredType]) -> [Named (FORMULA f)]
makePredMonos Sign f e
sig) (MapSet Id PredType -> [(Id, [PredType])]
forall a b. MapSet a b -> [(a, [b])]
MapSet.toList (MapSet Id PredType -> [(Id, [PredType])])
-> MapSet Id PredType -> [(Id, [PredType])]
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
sig)

makeMonos :: Sign f e -> (Id, [OpType]) -> [Named (FORMULA f)]
makeMonos :: Sign f e -> (Id, [OpType]) -> [Named (FORMULA f)]
makeMonos sig :: Sign f e
sig (o :: Id
o, ts :: [OpType]
ts) = Id -> Sign f e -> [OpType] -> [Named (FORMULA f)]
forall f e. Id -> Sign f e -> [OpType] -> [Named (FORMULA f)]
makeEquivMonos Id
o Sign f e
sig [OpType]
ts

makePredMonos :: Sign f e -> (Id, [PredType]) -> [Named (FORMULA f)]
makePredMonos :: Sign f e -> (Id, [PredType]) -> [Named (FORMULA f)]
makePredMonos sig :: Sign f e
sig (p :: Id
p, ts :: [PredType]
ts) = Id -> Sign f e -> [PredType] -> [Named (FORMULA f)]
forall f e. Id -> Sign f e -> [PredType] -> [Named (FORMULA f)]
makeEquivPredMonos Id
p Sign f e
sig [PredType]
ts

makeEquivMonos :: Id -> Sign f e -> [OpType] -> [Named (FORMULA f)]
makeEquivMonos :: Id -> Sign f e -> [OpType] -> [Named (FORMULA f)]
makeEquivMonos o :: Id
o sig :: Sign f e
sig ts :: [OpType]
ts = case [OpType]
ts of
  [] -> []
  t :: OpType
t : rs :: [OpType]
rs ->
    (OpType -> [Named (FORMULA f)]) -> [OpType] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Id -> Sign f e -> OpType -> OpType -> [Named (FORMULA f)]
forall f e.
Id -> Sign f e -> OpType -> OpType -> [Named (FORMULA f)]
makeEquivMono Id
o Sign f e
sig OpType
t) [OpType]
rs [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ Id -> Sign f e -> [OpType] -> [Named (FORMULA f)]
forall f e. Id -> Sign f e -> [OpType] -> [Named (FORMULA f)]
makeEquivMonos Id
o Sign f e
sig [OpType]
rs

makeEquivPredMonos :: Id -> Sign f e -> [PredType] -> [Named (FORMULA f)]
makeEquivPredMonos :: Id -> Sign f e -> [PredType] -> [Named (FORMULA f)]
makeEquivPredMonos o :: Id
o sig :: Sign f e
sig ts :: [PredType]
ts = case [PredType]
ts of
  [] -> []
  t :: PredType
t : rs :: [PredType]
rs ->
    (PredType -> [Named (FORMULA f)])
-> [PredType] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Id -> Sign f e -> PredType -> PredType -> [Named (FORMULA f)]
forall f e.
Id -> Sign f e -> PredType -> PredType -> [Named (FORMULA f)]
makeEquivPredMono Id
o Sign f e
sig PredType
t) [PredType]
rs [Named (FORMULA f)] -> [Named (FORMULA f)] -> [Named (FORMULA f)]
forall a. [a] -> [a] -> [a]
++ Id -> Sign f e -> [PredType] -> [Named (FORMULA f)]
forall f e. Id -> Sign f e -> [PredType] -> [Named (FORMULA f)]
makeEquivPredMonos Id
o Sign f e
sig [PredType]
rs

makeEquivMono :: Id -> Sign f e -> OpType -> OpType -> [Named (FORMULA f)]
makeEquivMono :: Id -> Sign f e -> OpType -> OpType -> [Named (FORMULA f)]
makeEquivMono o :: Id
o sig :: Sign f e
sig o1 :: OpType
o1 o2 :: OpType
o2 =
      let rs :: [Id]
rs = Sign f e -> Id -> Id -> [Id]
forall f e. Sign f e -> Id -> Id -> [Id]
minimalSupers Sign f e
sig (OpType -> Id
opRes OpType
o1) (OpType -> Id
opRes OpType
o2)
          a1 :: [Id]
a1 = OpType -> [Id]
opArgs OpType
o1
          a2 :: [Id]
a2 = OpType -> [Id]
opArgs OpType
o2
          args :: [[Id]]
args = if [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
a1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
a2 then
                 [[Id]] -> [[Id]]
forall a. [[a]] -> [[a]]
combine ([[Id]] -> [[Id]]) -> [[Id]] -> [[Id]]
forall a b. (a -> b) -> a -> b
$ (Id -> Id -> [Id]) -> [Id] -> [Id] -> [[Id]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Sign f e -> Id -> Id -> [Id]
forall f e. Sign f e -> Id -> Id -> [Id]
maximalSubs Sign f e
sig) [Id]
a1 [Id]
a2
                 else []
      in ([Id] -> [Named (FORMULA f)]) -> [[Id]] -> [Named (FORMULA f)]
forall (t :: * -> *) a b. Foldable t => (a -> [b]) -> t a -> [b]
concatMap (Id -> OpType -> OpType -> [Id] -> [Id] -> [Named (FORMULA f)]
forall f.
Id -> OpType -> OpType -> [Id] -> [Id] -> [Named (FORMULA f)]
makeEquivMonoRs Id
o OpType
o1 OpType
o2 [Id]
rs) [[Id]]
args

makeEquivMonoRs :: Id -> OpType -> OpType -> [SORT] -> [SORT]
                -> [Named (FORMULA f)]
makeEquivMonoRs :: Id -> OpType -> OpType -> [Id] -> [Id] -> [Named (FORMULA f)]
makeEquivMonoRs o :: Id
o o1 :: OpType
o1 o2 :: OpType
o2 rs :: [Id]
rs args :: [Id]
args = (Id -> Named (FORMULA f)) -> [Id] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> OpType -> OpType -> [Id] -> Id -> Named (FORMULA f)
forall f. Id -> OpType -> OpType -> [Id] -> Id -> Named (FORMULA f)
makeEquivMonoR Id
o OpType
o1 OpType
o2 [Id]
args) [Id]
rs

injectVar :: VAR_DECL -> SORT -> TERM f
injectVar :: VAR_DECL -> Id -> TERM f
injectVar = TERM f -> Id -> TERM f
forall f. TERM f -> Id -> TERM f
injectTerm (TERM f -> Id -> TERM f)
-> (VAR_DECL -> TERM f) -> VAR_DECL -> Id -> TERM f
forall b c a. (b -> c) -> (a -> b) -> a -> c
. VAR_DECL -> TERM f
forall f. VAR_DECL -> TERM f
toQualVar

injectTerm :: TERM f -> SORT -> TERM f
injectTerm :: TERM f -> Id -> TERM f
injectTerm t :: TERM f
t s :: Id
s = if Bool -> (Id -> Bool) -> Maybe Id -> Bool
forall b a. b -> (a -> b) -> Maybe a -> b
maybe Bool
False (Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s) (Maybe Id -> Bool) -> Maybe Id -> Bool
forall a b. (a -> b) -> a -> b
$ (f -> Maybe Id) -> TERM f -> Maybe Id
forall f. (f -> Maybe Id) -> TERM f -> Maybe Id
optSortOfTerm (Maybe Id -> f -> Maybe Id
forall a b. a -> b -> a
const Maybe Id
forall a. Maybe a
Nothing) TERM f
t
  then TERM f
t else TERM f -> Id -> Range -> TERM f
forall f. TERM f -> Id -> Range -> TERM f
Sorted_term TERM f
t Id
s Range
nullRange

makeEquivMonoR :: Id -> OpType -> OpType -> [SORT] -> SORT
               -> Named (FORMULA f)
makeEquivMonoR :: Id -> OpType -> OpType -> [Id] -> Id -> Named (FORMULA f)
makeEquivMonoR o :: Id
o o1 :: OpType
o1 o2 :: OpType
o2 args :: [Id]
args res :: Id
res =
    let vds :: [VAR_DECL]
vds = ((Id, Int) -> VAR_DECL) -> [(Id, Int)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Id
s, n :: Int
n) -> [VAR] -> Id -> Range -> VAR_DECL
Var_decl [String -> Int -> VAR
mkNumVar "x" Int
n] Id
s Range
nullRange)
              ([(Id, Int)] -> [VAR_DECL]) -> [(Id, Int)] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
args
        a1 :: [TERM f]
a1 = (VAR_DECL -> Id -> TERM f) -> [VAR_DECL] -> [Id] -> [TERM f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VAR_DECL -> Id -> TERM f
forall f. VAR_DECL -> Id -> TERM f
injectVar [VAR_DECL]
vds ([Id] -> [TERM f]) -> [Id] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
o1
        a2 :: [TERM f]
a2 = (VAR_DECL -> Id -> TERM f) -> [VAR_DECL] -> [Id] -> [TERM f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VAR_DECL -> Id -> TERM f
forall f. VAR_DECL -> Id -> TERM f
injectVar [VAR_DECL]
vds ([Id] -> [TERM f]) -> [Id] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opArgs OpType
o2
        t1 :: TERM f
t1 = TERM f -> Id -> TERM f
forall f. TERM f -> Id -> TERM f
injectTerm (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
o (OpType -> OP_TYPE
toOP_TYPE OpType
o1)
                                            Range
nullRange) [TERM f]
forall f. [TERM f]
a1 Range
nullRange) Id
res
        t2 :: TERM f
t2 = TERM f -> Id -> TERM f
forall f. TERM f -> Id -> TERM f
injectTerm (OP_SYMB -> [TERM f] -> Range -> TERM f
forall f. OP_SYMB -> [TERM f] -> Range -> TERM f
Application (Id -> OP_TYPE -> Range -> OP_SYMB
Qual_op_name Id
o (OpType -> OP_TYPE
toOP_TYPE OpType
o2)
                                            Range
nullRange) [TERM f]
forall f. [TERM f]
a2 Range
nullRange) Id
res
    in String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed "ga_function_monotonicity" (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vds (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ TERM f -> TERM f -> FORMULA f
forall f. TERM f -> TERM f -> FORMULA f
mkStEq TERM f
forall f. TERM f
t1 TERM f
forall f. TERM f
t2

makeEquivPredMono :: Id -> Sign f e -> PredType -> PredType
                  -> [Named (FORMULA f)]
makeEquivPredMono :: Id -> Sign f e -> PredType -> PredType -> [Named (FORMULA f)]
makeEquivPredMono o :: Id
o sig :: Sign f e
sig o1 :: PredType
o1 o2 :: PredType
o2 =
      let a1 :: [Id]
a1 = PredType -> [Id]
predArgs PredType
o1
          a2 :: [Id]
a2 = PredType -> [Id]
predArgs PredType
o2
          args :: [[Id]]
args = if [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
a1 Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [Id]
a2 then
                 [[Id]] -> [[Id]]
forall a. [[a]] -> [[a]]
combine ([[Id]] -> [[Id]]) -> [[Id]] -> [[Id]]
forall a b. (a -> b) -> a -> b
$ (Id -> Id -> [Id]) -> [Id] -> [Id] -> [[Id]]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith (Sign f e -> Id -> Id -> [Id]
forall f e. Sign f e -> Id -> Id -> [Id]
maximalSubs Sign f e
sig) [Id]
a1 [Id]
a2
                 else []
      in ([Id] -> Named (FORMULA f)) -> [[Id]] -> [Named (FORMULA f)]
forall a b. (a -> b) -> [a] -> [b]
map (Id -> PredType -> PredType -> [Id] -> Named (FORMULA f)
forall f. Id -> PredType -> PredType -> [Id] -> Named (FORMULA f)
makeEquivPred Id
o PredType
o1 PredType
o2) [[Id]]
args

makeEquivPred :: Id -> PredType -> PredType -> [SORT] -> Named (FORMULA f)
makeEquivPred :: Id -> PredType -> PredType -> [Id] -> Named (FORMULA f)
makeEquivPred o :: Id
o o1 :: PredType
o1 o2 :: PredType
o2 args :: [Id]
args =
    let vds :: [VAR_DECL]
vds = ((Id, Int) -> VAR_DECL) -> [(Id, Int)] -> [VAR_DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Id
s, n :: Int
n) -> [VAR] -> Id -> Range -> VAR_DECL
Var_decl [String -> Int -> VAR
mkNumVar "x" Int
n] Id
s Range
nullRange)
              ([(Id, Int)] -> [VAR_DECL]) -> [(Id, Int)] -> [VAR_DECL]
forall a b. (a -> b) -> a -> b
$ [Id] -> [(Id, Int)]
forall a. [a] -> [(a, Int)]
number [Id]
args
        a1 :: [TERM f]
a1 = (VAR_DECL -> Id -> TERM f) -> [VAR_DECL] -> [Id] -> [TERM f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VAR_DECL -> Id -> TERM f
forall f. VAR_DECL -> Id -> TERM f
injectVar [VAR_DECL]
vds ([Id] -> [TERM f]) -> [Id] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ PredType -> [Id]
predArgs PredType
o1
        a2 :: [TERM f]
a2 = (VAR_DECL -> Id -> TERM f) -> [VAR_DECL] -> [Id] -> [TERM f]
forall a b c. (a -> b -> c) -> [a] -> [b] -> [c]
zipWith VAR_DECL -> Id -> TERM f
forall f. VAR_DECL -> Id -> TERM f
injectVar [VAR_DECL]
vds ([Id] -> [TERM f]) -> [Id] -> [TERM f]
forall a b. (a -> b) -> a -> b
$ PredType -> [Id]
predArgs PredType
o2
        t1 :: FORMULA f
t1 = PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
o (PredType -> PRED_TYPE
toPRED_TYPE PredType
o1) Range
nullRange) [TERM f]
forall f. [TERM f]
a1
             Range
nullRange
        t2 :: FORMULA f
t2 = PRED_SYMB -> [TERM f] -> Range -> FORMULA f
forall f. PRED_SYMB -> [TERM f] -> Range -> FORMULA f
Predication (Id -> PRED_TYPE -> Range -> PRED_SYMB
Qual_pred_name Id
o (PredType -> PRED_TYPE
toPRED_TYPE PredType
o2) Range
nullRange) [TERM f]
forall f. [TERM f]
a2
             Range
nullRange
    in String -> FORMULA f -> Named (FORMULA f)
forall a s. a -> s -> SenAttr s a
makeNamed "ga_predicate_monotonicity" (FORMULA f -> Named (FORMULA f)) -> FORMULA f -> Named (FORMULA f)
forall a b. (a -> b) -> a -> b
$ [VAR_DECL] -> FORMULA f -> FORMULA f
forall f. [VAR_DECL] -> FORMULA f -> FORMULA f
mkForall [VAR_DECL]
vds (FORMULA f -> FORMULA f) -> FORMULA f -> FORMULA f
forall a b. (a -> b) -> a -> b
$ FORMULA f -> FORMULA f -> FORMULA f
forall f. FORMULA f -> FORMULA f -> FORMULA f
mkEqv FORMULA f
forall f. FORMULA f
t1 FORMULA f
forall f. FORMULA f
t2