content: {- |
  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
  