content: {- |
  Module      :  ./CASL/CCC/TermFormula.hs
  Description :  auxiliary functions on terms and formulas
  Copyright   :  (c) Mingyi Liu, Till Mossakowski, Uni Bremen 2004-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  Auxiliary functions on terms and formulas
  -}
  
  module CASL.CCC.TermFormula where
  
  import CASL.AS_Basic_CASL
  import CASL.Fold
  import CASL.Overload
  import CASL.Quantification
  import CASL.Sign
  import CASL.ToDoc
  import CASL.Utils
  
  import Common.Id
  import Common.Result
  
  import Control.Monad
  
  import Data.Function
  import Data.List
  import Data.Maybe
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  -- | the sorted term is always ignored
  unsortedTerm :: TERM f -> TERM f
  unsortedTerm t = case t of
    Sorted_term t' _ _ -> unsortedTerm t'
    Cast t' _ _ -> unsortedTerm t'
    _ -> t
  
  -- | check whether it exist a (unique)existent quantification
  isExQuanti :: FORMULA f -> Bool
  isExQuanti f = case f of
    Quantification Universal _ f' _ -> isExQuanti f'
    Quantification {} -> True
    Relation f1 _ f2 _ -> isExQuanti f1 || isExQuanti f2
    Negation f' _ -> isExQuanti f'
    _ -> False
  
  -- | check whether it contains a membership formula
  isMembership :: FORMULA f -> Bool
  isMembership f = case f of
    Quantification _ _ f' _ -> isMembership f'
    Junction _ fs _ -> any isMembership fs
    Negation f' _ -> isMembership f'
    Relation f1 _ f2 _ -> isMembership f1 || isMembership f2
    Membership {} -> True
    _ -> False
  
  -- | check whether it contains a definedness formula
  containDef :: FORMULA f -> Bool
  containDef f = case f of
    Quantification _ _ f' _ -> containDef f'
    Junction _ fs _ -> any containDef fs
    Relation f1 _ f2 _ -> containDef f1 || containDef f2
    Negation f' _ -> containDef f'
    Definedness _ _ -> True
    _ -> False
  
  -- | check whether it contains a negation
  containNeg :: FORMULA f -> Bool
  containNeg f = case f of
    Quantification _ _ f' _ -> containNeg f'
    Relation _ c f' _ | c /= Equivalence -> containNeg f'
    Relation f' Equivalence _ _ -> containNeg f'
    Negation _ _ -> True
    _ -> False
  
  domainDef :: FORMULA f -> Maybe (TERM f, FORMULA f)
  domainDef f = case stripAllQuant f of
    Relation (Definedness t _) Equivalence f' _
      | not (containDef f') -> Just (t, f')
    _ -> Nothing
  
  -- | check whether it is a Variable
  isVar :: TERM t -> Bool
  isVar t = case unsortedTerm t of
    Qual_var {} -> True
    _ -> False
  
  -- | extract all variables of a term
  varOfTerm :: Ord f => TERM f -> [TERM f]
  varOfTerm t = case unsortedTerm t of
    Qual_var {} -> [t]
    Application _ ts _ -> concatMap varOfTerm ts
    _ -> []
  
  -- | extract all arguments of a term
  arguOfTerm :: TERM f -> [TERM f]
  arguOfTerm = snd . topIdOfTerm
  
  nullId :: ((Id, Int), [TERM f])
  nullId = ((stringToId "", 0), [])
  
  topIdOfTerm :: TERM f -> ((Id, Int), [TERM f])
  topIdOfTerm t = case unsortedTerm t of
    Application o ts _ -> ((opSymbName o, length ts), ts)
    _ -> nullId
  
  -- | get the patterns of a axiom
  patternsOfAxiom :: FORMULA f -> [TERM f]
  patternsOfAxiom = snd . topIdOfAxiom
  
  topIdOfAxiom :: FORMULA f -> ((Id, Int), [TERM f])
  topIdOfAxiom f = case stripAllQuant f of
      Negation f' _ -> topIdOfAxiom f'
      Relation _ c f' _ | c /= Equivalence -> topIdOfAxiom f'
      Relation f' Equivalence _ _ -> topIdOfAxiom f'
      Predication p ts _ -> ((predSymbName p, length ts), ts)
      Equation t _ _ _ -> topIdOfTerm t
      Definedness t _ -> topIdOfTerm t
      _ -> nullId
  
  -- | split the axiom into condition and rest axiom
  splitAxiom :: FORMULA f -> ([FORMULA f], FORMULA f)
  splitAxiom f = case stripAllQuant f of
                       Relation f1 c f2 _ | c /= Equivalence ->
                         let (f3, f4) = splitAxiom f2 in (f1 : f3, f4)
                       f' -> ([], f')
  
  -- | get the premise of a formula, without implication return true
  conditionAxiom :: FORMULA f -> FORMULA f
  conditionAxiom = conjunct . fst . splitAxiom
  
  -- | get the conclusion of a formula, without implication return the formula
  restAxiom :: FORMULA f -> FORMULA f
  restAxiom = snd . splitAxiom
  
  -- | get right hand side of an equivalence, without equivalence return true
  resultAxiom :: FORMULA f -> FORMULA f
  resultAxiom f = case restAxiom f of
                    Relation _ Equivalence f' _ -> f'
                    _ -> trueForm
  
  -- | get right hand side of an equation, without equation return dummy term
  resultTerm :: FORMULA f -> TERM f
  resultTerm f = case restAxiom f of
                   Negation (Definedness _ _) _ ->
                     varOrConst (mkSimpleId "undefined")
                   Equation _ _ t _ -> t
                   _ -> varOrConst (mkSimpleId "unknown")
  
  getSubstForm :: (FormExtension f, TermExtension f, Ord f) => Sign f e
    -> FORMULA f -> FORMULA f
    -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
  getSubstForm sig f1 f2 = do
    let p1 = patternsOfAxiom f1
        p2 = patternsOfAxiom f2
        getVars = Set.map fst . freeVars sig . stripAllQuant
    getSubst sig (p1, getVars f1) (p2, getVars f2)
  
  mkCast :: SORT -> TERM f -> SORT -> (TERM f, [FORMULA f])
  mkCast s2 t s1 = if s1 == s2 then (t, []) else
    case unsortedTerm t of
      Qual_var v _ r -> (Qual_var v s1 r, [])
      _ -> (Cast t s1 nullRange, [Membership t s1 nullRange])
  
  mkSortedTerm :: SORT -> TERM f -> SORT -> TERM f
  mkSortedTerm s1 t s2 = if s1 == s2 then t else
    case unsortedTerm t of
      Qual_var v _ r -> Qual_var v s2 r
      _ -> Sorted_term t s2 nullRange
  
  minSortTerm :: TermExtension f => TERM f -> TERM f
  minSortTerm t = case t of
    Sorted_term st _ _ -> case optTermSort st of
      Nothing -> t
      Just _ -> minSortTerm st
    _ -> t
  
  mkSTerm :: TermExtension f => Sign f e -> SORT -> TERM f
    -> (TERM f, [FORMULA f])
  mkSTerm sig s t =
    let s2 = fromMaybe s $ optTermSort t
        t0 = minSortTerm t
        s0 = fromMaybe s $ optTermSort t0
    in case maximalSubs sig s s2 of
      l@(s1 : _) -> let
        s3 = if s0 == s2 then s1 else
             fromMaybe s1 $ find (leqSort sig s0) l
        (s4, fs) = mkCast s2 t s3
        in (mkSortedTerm s3 s4 s, fs)
      _ -> error $ "CCC.mkSTerm " ++ show (s0, s, s2)
  
  getSubst :: (FormExtension f, TermExtension f, Ord f) => Sign f e
    -> ([TERM f], Set.Set VAR) -> ([TERM f], Set.Set VAR)
    -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
  getSubst sig (p1, vs1) (p2, vs2) =
    let getVars = Set.map fst . freeTermVars sig
    in case (p1, p2) of
      ([], []) -> do
        let i = Set.intersection vs1 vs2
        unless (Set.null i)
          $ appendDiags [mkDiag Warning "possibly conflicting variables" i]
        return ((Map.empty, []), (Map.empty, []))
      (hd1 : tl1, hd2 : tl2) ->
        let r = getSubst sig (tl1, vs1) (tl2, vs2)
            mkS1 v1 s1 = do
                let (hd3, fs) = mkSTerm sig s1 hd2
                ((m1, fs1), m2) <- getSubst sig
                  (tl1, Set.delete v1 vs1) (tl2, vs2)
                return ((Map.insert v1 hd3 m1, fs ++ fs1), m2)
            mkS2 v2 s2 = do
                let (hd3, fs) = mkSTerm sig s2 hd1
                (m1, (m2, fs2)) <- getSubst sig (tl1, vs1)
                  (tl2, Set.delete v2 vs2)
                return (m1, (Map.insert v2 hd3 m2, fs ++ fs2))
            cond v vs hd = Set.member v vs && Set.notMember v (getVars hd)
            diag v = appendDiags [mkDiag Warning
                              "unsupported occurrence of variable" v] >> r
        in case (unsortedTerm hd1, unsortedTerm hd2) of
          (Qual_var v1 s1 _, Qual_var v2 s2 _)
            | v1 == v2 && s1 == s2 -> getSubst sig (tl1, Set.delete v1 vs1)
                 (tl2, Set.delete v2 vs2)
            | Set.member v1 vs2 ->
              if Set.member v2 vs1
              then appendDiags [mkDiag Warning
                              ("unsupported mix of variables '"
                               ++ show v1 ++ "' and") v2] >> r
              else mkS1 v1 s1
            | otherwise -> mkS2 v2 s2
          (Qual_var v1 s1 _, _) ->
              if cond v1 vs2 hd2 then diag v1
              else mkS1 v1 s1
          (_, Qual_var v2 s2 _) ->
              if cond v2 vs1 hd1 then diag v2
              else mkS2 v2 s2
          (_, _) | sameOpsApp sig hd1 hd2 ->
               getSubst sig (arguOfTerm hd1 ++ tl1, vs1)
                            (arguOfTerm hd2 ++ tl2, vs2)
          _ -> mkError "no overlap at" hd1
      _ -> error "non-matching leading terms"
  
  -- | extract defined subsorts
  isSubsortDef :: FORMULA f -> Maybe (SORT, VAR_DECL, FORMULA f)
  isSubsortDef f = case f of
    Quantification Universal [vd@(Var_decl [v] super _)]
      (Relation (Membership (Qual_var v2 super2 _) sub _) Equivalence f1 _) _
       | (v, super) == (v2, super2) -> Just (sub, vd, f1)
    _ -> Nothing
  
  -- | create the obligations for subsorts
  infoSubsorts :: Set.Set SORT -> [(SORT, VAR_DECL, FORMULA f)] -> [FORMULA f]
  infoSubsorts emptySorts = map (\ (_, v, f) -> mkExist [v] f)
    . filter (\ (s, _, _) -> not $ Set.member s emptySorts)
  
  -- | extract the leading symbol from a formula
  leadingSym :: GetRange f => FORMULA f -> Maybe (Either OP_SYMB PRED_SYMB)
  leadingSym = fmap extractLeadingSymb . leadingTermPredication
  
  -- | extract the leading symbol with the range from a formula
  leadingSymPos :: GetRange f => FORMULA f
    -> (Maybe (Either (TERM f) (FORMULA f)), Range)
  leadingSymPos f = leading (f, False, False, False) where
    -- three booleans to indicate inside implication, equivalence or negation
    leadTerm t q = case unsortedTerm t of
      a@(Application _ _ p) -> (Just (Left a), p)
      _ -> (Nothing, q)
    leading (f1, b1, b2, b3) = case (stripAllQuant f1, b1, b2, b3) of
      (Negation f' _, _, _, False) ->
          leading (f', b1, b2, True)
      (Relation _ c f' _, _, False, False)
          | c /= Equivalence ->
          leading (f', True, False, False)
      (Relation f' Equivalence _ _, _, False, False) ->
          leading (f', b1, True, False)
      (Definedness t q, _, _, _) -> leadTerm t q
      (pr@(Predication _ _ p), _, _, _) ->
          (Just (Right pr), p)
      (Equation t _ _ q, _, False, False) -> leadTerm t q
      _ -> (Nothing, getRange f1)
  
  -- | extract the leading term or predication from a formula
  leadingTermPredication :: GetRange f => FORMULA f
    -> Maybe (Either (TERM f) (FORMULA f))
  leadingTermPredication = fst . leadingSymPos
  
  -- | extract the leading symbol from a term or a formula
  extractLeadingSymb :: Either (TERM f) (FORMULA f) -> Either OP_SYMB PRED_SYMB
  extractLeadingSymb lead = case lead of
    Left (Application os _ _) -> Left os
    Right (Predication p _ _) -> Right p
    _ -> error "CASL.CCC.TermFormula<extractLeadingSymb>"
  
  -- | replaces variables by terms in a term or formula
  substRec :: Eq f => [(TERM f, TERM f)] -> Record f (FORMULA f) (TERM f)
  substRec subs = (mapRecord id)
     { foldQual_var = \ t _ _ _ -> subst subs t } where
    subst l tt = case l of
      [] -> tt
      (n, v) : r -> if tt == v then n else subst r tt
  
  substitute :: Eq f => [(TERM f, TERM f)] -> TERM f -> TERM f
  substitute = foldTerm . substRec
  
  substiF :: Eq f => [(TERM f, TERM f)] -> FORMULA f -> FORMULA f
  substiF = foldFormula . substRec
  
  sameOpTypes :: Sign f e -> OP_TYPE -> OP_TYPE -> Bool
  sameOpTypes sig = on (leqF sig) toOpType
  
  sameOpSymbs :: Sign f e -> OP_SYMB -> OP_SYMB -> Bool
  sameOpSymbs sig o1 o2 = on (==) opSymbName o1 o2 && case (o1, o2) of
    (Qual_op_name _ t1 _, Qual_op_name _ t2 _) -> sameOpTypes sig t1 t2
    _ -> False
  
  -- | check whether two terms are the terms of same application symbol
  sameOpsApp :: Sign f e -> TERM f -> TERM f -> Bool
  sameOpsApp sig app1 app2 = case (unsortedTerm app1, unsortedTerm app2) of
    (Application o1 _ _, Application o2 _ _) -> sameOpSymbs sig o1 o2
    _ -> False
  
  eqPattern :: Sign f e -> TERM f -> TERM f -> Bool
  eqPattern sig t1 t2 = case (unsortedTerm t1, unsortedTerm t2) of
    (Qual_var v1 _ _, Qual_var v2 _ _) -> v1 == v2
    _ | sameOpsApp sig t1 t2 ->
      and $ on (zipWith $ eqPattern sig) arguOfTerm t1 t2
    _ -> False
  