content: {- |
  Module      :  ./CASL/CCC/FreeTypes.hs
  Description :  consistency checking of free types
  Copyright   :  (c) Mingyi Liu and Till Mossakowski and Uni Bremen 2004-2005
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Christian.Maeder@dfki.de
  Stability   :  provisional
  Portability :  non-portable (imports Logic.Logic)
  
  Consistency checking of free types
  -}
  
  module CASL.CCC.FreeTypes (checkFreeType) where
  
  import CASL.AlphaConvert
  import CASL.AS_Basic_CASL
  import CASL.MapSentence
  import CASL.Morphism
  import CASL.Sign
  import CASL.Simplify
  import CASL.SimplifySen
  import CASL.CCC.TermFormula
  import CASL.CCC.TerminationProof (terminationProof)
  import CASL.Overload (leqP)
  import CASL.Quantification
  import CASL.ToDoc
  import CASL.Utils
  
  import Common.AS_Annotation
  import Common.Consistency (Conservativity (..))
  import Common.DocUtils
  import Common.Id
  import Common.Result
  import Common.Utils (number)
  import qualified Common.Lib.MapSet as MapSet
  import qualified Common.Lib.Rel as Rel
  
  import Control.Monad
  import qualified Control.Monad.Fail as Fail
  
  import Data.Either
  import Data.Function
  import Data.List
  import Data.Maybe
  
  import qualified Data.Set as Set
  
  -- | check values of constructors (free types have only total ones)
  inhabited :: Set.Set SORT -> [OP_SYMB] -> Set.Set SORT
  inhabited sorts cons = iterateInhabited sorts where
    argsRes = foldr (\ os -> case os of
      Qual_op_name _ (Op_type Total args res _) _ -> ((args, res) :)
      _ -> id) [] cons
    iterateInhabited l =
      if changed then iterateInhabited newL else newL where
        (newL, changed) = foldr (\ (ags, rs) p@(l', _) ->
          if all (`Set.member` l') ags && not (Set.member rs l')
          then (Set.insert rs l', True) else p) (l, False) argsRes
  
  -- | just filter out the axioms generated for free types
  isGenAx :: Named (FORMULA f) -> Bool
  isGenAx ax = case stripPrefix "ga_" $ senAttr ax of
    Nothing -> True
    Just rname -> all (not . (`isPrefixOf` rname))
      ["disjoint_", "injective_", "selector_"]
  
  getFs :: [Named (FORMULA f)] -> [FORMULA f]
  getFs = map sentence . filter isGenAx
  
  -- | get the constraints from sort generation axioms
  constraintOfAxiom :: [FORMULA f] -> [[Constraint]]
  constraintOfAxiom = foldr (\ f -> case f of
    Sort_gen_ax constrs _ -> (constrs :)
    _ -> id) []
  
  recoverSortsAndConstructors :: [FORMULA f] -> (Set.Set SORT, Set.Set OP_SYMB)
  recoverSortsAndConstructors fs = let
    (srts, cons, _) = unzip3 . map recover_Sort_gen_ax
      $ constraintOfAxiom fs
    in (Set.unions $ map Set.fromList srts, Set.unions $ map Set.fromList cons)
  
  -- check that patterns do not overlap, if not, return proof obligation.
  getOverlapQuery :: (FormExtension f, TermExtension f, Ord f) => Sign f e
    -> [[FORMULA f]] -> [FORMULA f]
  getOverlapQuery sig = filter (not . is_True_atom)
    . mapMaybe (retrySubstForm sig) . concatMap pairs
  
  convert2Forms :: (TermExtension f, FormExtension f, Ord f) => Sign f e
    -> FORMULA f -> FORMULA f
    -> Result ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
    -> (FORMULA f, FORMULA f, ((Subst f, [FORMULA f]), (Subst f, [FORMULA f])))
  convert2Forms sig f1 f2 (Result ds m) =
    if null ds then let Just r = m in (f1, f2, r) else let
    (f3, c) = alphaConvert 1 id f1
    f4 = convertFormula c id f2
    Result _ (Just p) = getSubstForm sig f3 f4
    in (f3, f4, p)
  
  retrySubstForm :: (FormExtension f, TermExtension f, Ord f) => Sign f e
    -> (FORMULA f, FORMULA f) -> Maybe (FORMULA f)
  retrySubstForm sig (f1, f2) =
    let r@(Result ds m) = getSubstForm sig f1 f2
    in case m of
         Nothing -> Nothing
         Just s -> if null ds then Just $ mkOverlapEq sig s f1 f2
           else let (f3, f4, s2) = convert2Forms sig f1 f2 r
                in Just . stripQuant sig . convertFormula 1 id
                       $ mkOverlapEq sig s2 f3 f4
  
  quant :: TermExtension f => Sign f e -> FORMULA f -> FORMULA f
  quant sig f = quantFreeVars sig f nullRange
  
  mkOverlapEq :: (TermExtension f, GetRange f, Ord f) => Sign f e
    -> ((Subst f, [FORMULA f]), (Subst f, [FORMULA f]))
    -> FORMULA f -> FORMULA f -> FORMULA f
  mkOverlapEq sig ((s1, fs1), (s2, fs2)) f1 f2 = quant sig . simplifyFormula id
       . mkImpl (conjunct $ map (replaceVarsF s1 id) fs2
                 ++ map (replaceVarsF s2 id) fs1)
       . overlapQuery (replaceVarsF s1 id $ stripAllQuant f1)
       . replaceVarsF s2 id $ stripAllQuant f2
  
  {-
    check if leading symbols are new (not in the image of morphism),
          if not, return it as proof obligation
  -}
  getDefsForOld :: GetRange f => Sign f e -> [FORMULA f]
    -> [FORMULA f]
  getDefsForOld sig axioms = let
          oldOpMap = opMap sig
          oldPredMap = predMap sig
      in filter (\ f -> case leadingSym f of
           Just (Left (Qual_op_name ident ot _))
             | MapSet.member ident (toOpType ot) oldOpMap -> True
           Just (Right (Qual_pred_name ident pt _))
             | MapSet.member ident (toPredType pt) oldPredMap -> True
           _ -> False) axioms
  
  isFreeSortGen :: FORMULA f -> Bool
  isFreeSortGen f = case f of
    Sort_gen_ax _ True -> True
    _ -> False
  
  -- | non-inhabited non-empty sorts
  getNefsorts :: Set.Set SORT -> Set.Set SORT -> Set.Set SORT
    -> (Set.Set SORT, [OP_SYMB]) -> Set.Set SORT
  getNefsorts oldSorts nSorts esorts (srts, cons) =
    Set.difference fsorts $ inhabited oldSorts cons where
      fsorts = Set.difference (Set.intersection nSorts srts) esorts
  
  getDataStatus :: Set.Set SORT -> Set.Set SORT -> Set.Set SORT -> Conservativity
  getDataStatus nSorts defSubs genSorts
    | Set.null nSorts = Def
    | Set.null $ Set.difference nSorts $ Set.union genSorts defSubs = Mono
    | otherwise = Cons
  
  getConStatus :: Conservativity -> [FORMULA f] -> Conservativity
  getConStatus dataStatus fs = min dataStatus $ if null fs then Def else Cons
  
  -- | check whether it is the domain of a partial function
  isDomain :: FORMULA f -> Bool
  isDomain = isJust . domainDef
  
  -- | check whether it contains a definedness formula in correct form
  correctDef :: FORMULA f -> Bool
  correctDef f = case stripAllQuant f of
    Relation (Definedness _ _) c _ _ | c /= Equivalence -> True
    Negation (Definedness _ _) _ -> True
    Definedness _ _ -> True
    _ -> False
  
  showForm :: (TermExtension f, FormExtension f) => Sign f e -> FORMULA f
    -> String
  showForm s = flip showDoc "" . simplifyCASLSen s
  
  -- check the definitional form of the partial axioms
  checkDefinitional :: (FormExtension f, TermExtension f)
    => Sign f e -> [FORMULA f] -> Maybe (Result (Conservativity, [FORMULA f]))
  checkDefinitional tsig fs = let
         formatAxiom = showForm tsig
         (noLSyms, withLSyms) = partition (isNothing . fst . snd)
           $ map (\ a -> (a, leadingSymPos a)) fs
         partialLSyms = foldr (\ (a, (ma, _)) -> case ma of
           Just (Left (Application t@(Qual_op_name _ (Op_type k _ _ _) _) _ _))
             | k == Partial -> ((a, t) :)
           _ -> id) [] withLSyms
         (domainDefs, otherPartials) = partition (isDomain . fst) partialLSyms
         (withDefs, withOutDefs) = partition (containDef . fst) otherPartials
         (correctDefs, wrongDefs) = partition (correctDef . fst) withDefs
         grDomainDefs = Rel.partList (on (sameOpSymbs tsig) snd) domainDefs
         (multDomainDefs, oneDomainDefs) = partition (\ l -> case l of
            [_] -> False
            _ -> True) grDomainDefs
         singleDomainDefs = map head oneDomainDefs
         nonCompleteDomainDefs = filter (\ (da, _) -> case domainDef da of
           Just (ta, _) | all isVar $ arguOfTerm ta -> False
           _ -> True) singleDomainDefs
         domainObls = concatMap (\ (da, dt) -> map (\ (de, _) -> (da, de))
             $ filter (sameOpSymbs tsig dt . snd) correctDefs) singleDomainDefs
         nonEqDoms = filter (\ (da, de) ->
           case (domainDef da, stripAllQuant de) of
             (Just (ta, _), Relation (Definedness te _) c _ _)
               | c /= Equivalence && sameOpsApp tsig ta te ->
               case leadingTermPredication de of
                 Just (Left t) | eqPattern tsig te t -> False
                 _ -> True
             _ -> True) domainObls
         defOpSymbs = Set.fromList $ map (snd . head) grDomainDefs
           ++ map snd correctDefs
         wrongWithoutDefs = filter ((`Set.notMember` defOpSymbs) . snd)
           withOutDefs
         ds = map (\ (a, (_, pos)) -> Diag
           Warning ("missing leading symbol in:\n  " ++ formatAxiom a) pos)
             noLSyms
           ++ map (\ (a, t) -> Diag
           Warning ("definedness is not definitional:\n  " ++ formatAxiom a)
                  $ getRange t) wrongDefs
           ++ map (\ l@((_, t) : _) -> Diag Warning (unlines $
               ("multiple domain axioms for: " ++ showDoc t "")
               : map (("  " ++) . formatAxiom . fst) l) $ getRange t)
             multDomainDefs
           ++ map (\ (a, t) -> Diag
           Warning ("missing definedness condition for partial '"
                        ++ showDoc t "' in:\n  " ++ formatAxiom a)
               $ getRange t) wrongWithoutDefs
           ++ map (\ (da, _) -> Diag
           Warning ("non-complete domain axiom:\n  " ++ formatAxiom da)
               $ getRange da) nonCompleteDomainDefs
           ++ map (\ (da, de) -> Diag
           Warning ("unexpected definedness condition:\n  "
                    ++ formatAxiom de
                    ++ "\nin the presence of domain axiom:\n  "
                    ++ formatAxiom da) $ getRange de) nonEqDoms
         in if null ds then Nothing else Just $ Result ds Nothing
  
  {-
    call the symbols in the image of the signature morphism "new"
  
  - each new sort must be a free type,
    i.e. it must occur in a sort generation constraint that is marked as free
      (Sort_gen_ax constrs True)
      such that the sort is in srts,
          where (srts,ops,_)=recover_Sort_gen_ax constrs
      if not, output "don't know"
    and there must be one term of that sort (inhabited)
      if not, output "no"
  - group the axioms according to their leading operation/predicate symbol,
    i.e. the f resp. the p in
    forall x_1:s_n .... x_n:s_n .                  f(t_1,...,t_m)=t
    forall x_1:s_n .... x_n:s_n .       phi =>      f(t_1,...,t_m)=t
                                    Implication  Application  Strong_equation
    forall x_1:s_n .... x_n:s_n .                  p(t_1,...,t_m)<=>phi
    forall x_1:s_n .... x_n:s_n .    phi1  =>      p(t_1,...,t_m)<=>phi
                                   Implication   Predication    Equivalence
    if there are axioms not being of this form, output "don't know"
  -}
  checkSort :: Bool -> Set.Set SORT -> Set.Set SORT -> Set.Set SORT
    -> Set.Set SORT -> Set.Set SORT -> Sign f e -> Sign f e
    -> Maybe (Result (Conservativity, [FORMULA f]))
  checkSort noSentence nSorts defSubsorts gSorts fSorts nefsorts sSig tSig
      | noSentence && Set.null nSorts =
          let cond = MapSet.null (diffOpMapSet (opMap tSig) $ opMap sSig)
                && MapSet.null (diffMapSet (predMap tSig) $ predMap sSig)
          in Just $ justHint (if cond then Def else Cons, [])
          $ (if cond then "neither symbols"
            else "neither sorts") ++ " nor sentences have been added"
      | not $ Set.null notFreeSorts =
          mkUnknown "some types are not freely generated" notFreeSorts
      | not $ Set.null nefsorts = mkWarn "some sorts are not inhabited"
          nefsorts $ Just (Inconsistent, [])
      | not $ Set.null genNotNew = mkUnknown "some defined sorts are not new"
          genNotNew
      | otherwise = Nothing
      where
          notFreeSorts = Set.intersection nSorts
            $ Set.difference gSorts fSorts
          genNotNew = Set.difference
            (Set.unions [defSubsorts, gSorts, fSorts]) nSorts
          mkWarn s i r = Just $ Result [mkDiag Warning s i] r
          mkUnknown s i = mkWarn s i Nothing
  
  checkLeadingTerms :: (FormExtension f, TermExtension f, Ord f)
    => Sign f e -> [FORMULA f] -> [OP_SYMB]
    -> Maybe (Result (Conservativity, [FORMULA f]))
  checkLeadingTerms tsig fsn constructors = let
      ltp = mapMaybe leadingTermPredication fsn
      formatTerm = flip showDoc "" . simplifyCASLTerm tsig
      args = foldr (\ ei -> case ei of
        Left (Application os ts qs) ->
           ((qs, "term for " ++ show (opSymbName os), ts) :)
        Right (Predication ps ts qs) ->
           ((qs, "predicate " ++ show (predSymbName ps), ts) :)
        _ -> id) [] ltp
      ds = foldr (\ (qs, d, ts) l ->
             let vs = concatMap varOfTerm ts
                 dupVs = vs \\ Set.toList (Set.fromList vs)
                 nonCs = checkTerms tsig constructors ts
                 td = " in leading " ++ d ++ ": "
             in map (\ v -> Diag Warning
                      ("duplicate variable" ++ td ++ formatTerm v) qs) dupVs
                ++ map (\ t -> Diag Warning
                       ("non-constructor" ++ td ++ formatTerm t)
                       qs) nonCs
                ++ l) [] args
      in if null ds then Nothing else Just $ Result ds Nothing
  
  -- check the sufficient completeness
  checkIncomplete :: (FormExtension f, TermExtension f, Ord f)
    => Sign f e -> [FORMULA f] -> [OP_SYMB] -> [[FORMULA f]] -> [OP_SYMB]
    -> Maybe (Result (Conservativity, [FORMULA f]))
  checkIncomplete sig obligations doms fsn cons =
    case getNotComplete sig doms fsn cons of
    [] -> Nothing
    incomplete -> let
      formatAxiom = showForm sig
      in Just $ Result
        (map (\ (Result ds mfs, fs@(hd : _)) -> let
          (lSym, pos) = leadingSymPos hd
          sname = case fmap extractLeadingSymb lSym of
                        Just (Left opS) -> opSymbName opS
                        Just (Right pS) -> predSymbName pS
                        _ -> error "CASL.CCC.FreeTypes.<Symb_Name>"
          in Diag Warning (intercalate "\n" $
               ("the definition of " ++ show sname
                ++ (if null ds then " may not be" else " is not") ++ " complete")
               : "the defining formula group is:"
               : map (\ (f, n) -> "  " ++ shows n ". "
                      ++ formatAxiom f) (number fs)
               ++ map diagString ds
               ++ maybe []
                   (map (\ (p, f) -> "possibly incomplete pattern for: " ++ p
                     ++ "\n  with completeness condition: "
                     ++ formatAxiom f)) mfs
               ) pos)
         incomplete) $ Just (Cons, obligations)
  
  renameVars :: Int -> [FORMULA f] -> (Int, [FORMULA f])
  renameVars c = foldr (\ f (c1, l) ->
     let (f2, c2) = alphaConvert c1 id f in
     (c2, f2 : l)) (c, [])
  
  checkTerminal :: (FormExtension f, TermExtension f, Ord f)
    => Sign f e -> Conservativity -> [FORMULA f] -> [FORMULA f] -> [FORMULA f]
    -> IO (Result (Conservativity, [FORMULA f]))
  checkTerminal sig conStatus obligations doms fsn =
      if null fsn then return $ justHint (conStatus, obligations)
        "no defining sentences"
      else do
      let (c, domains) = renameVars 1 doms
          fs_terminalProof = snd $ renameVars c fsn
      (proof, str) <- terminationProof sig fs_terminalProof domains
      return $ case proof of
          Just True -> justHint (conStatus, obligations) "termination succeeded"
          _ -> warning (Cons, obligations)
               (if isJust proof then "not terminating"
                else "cannot prove termination: " ++ str) nullRange
  
  checkPos :: FORMULA f -> Bool
  checkPos f = case f of
        Quantification _ _ f' _ -> checkPos f'
        Junction _ cs _ -> all checkPos cs
        Relation i1 c i2 _ -> let
          c1 = checkPos i1
          c2 = checkPos i2
          in if c == Equivalence then c1 == c2 else c1 <= c2
        Negation n _ -> not $ checkPos n
        Atom b _ -> b
        Predication {} -> True
        Membership {} -> True
        Definedness {} -> True
        Equation {} -> True
        Sort_gen_ax cs _ -> case cs of
          [c] -> case opSymbs c of
            [_] -> True
              {- just a single constructor creates a unique value
              even for multiple one-point components -}
            _ -> False
          _ -> False
        _ -> False
  
  partitionMaybe :: (a -> Maybe b) -> [a] -> ([b], [a])
  partitionMaybe f = foldr (\ a (bs, as) ->
    maybe (bs, a : as) (\ b -> (b : bs, as)) $ f a) ([], [])
  
  
  {- -----------------------------------------------------------------------
     function checkFreeType:
     - check if leading symbols are new (not in the image of morphism),
             if not, return them as obligations
     - generated datatype is free
     - if new sort is not etype or esort, it can not be empty.
     - the leading terms consist of variables and constructors only,
             if not, return Nothing
       - split function leading_Symb into
         leadingTermPredication
         and
         extractLeadingSymb
       - collect all operation symbols from recover_Sort_gen_ax fconstrs
                                                         (= constructors)
     - no variable occurs twice in a leading term, if not, return Nothing
     - check that patterns do not overlap, if not, return obligations
       This means:
         in each group of the grouped axioms:
         all patterns of leading terms/formulas are disjoint
         this means: either leading symbol is a variable,
                             and there is just one axiom
                     otherwise, group axioms according to leading symbol
                                no symbol may be a variable
                                check recursively the arguments of
                                constructor in each group
    - sufficient completeness
    - termination proof
  ------------------------------------------------------------------------
  free datatypes and recursive equations are consistent -}
  checkFreeType :: (FormExtension f, TermExtension f, Ord f)
    => (Sign f e, [Named (FORMULA f)]) -> Morphism f e m
    -> [Named (FORMULA f)] -> IO (Result (Conservativity, [FORMULA f]))
  checkFreeType (_, osens) m axs = do
    let sig = mtarget m
        sSig = imageOfMorphism m
        fs = getFs axs -- strip labels and generated sentences
        (exQuants, fs2) = partition isExQuanti fs
        (memShips, fs3) = partition isMembership fs2
        (sortGens1, axioms) = partition isSortGen fs3
        (freeSortGens, sortGens) = partition isFreeSortGen sortGens1
        (domains, axLessDoms) = partition isDomain axioms
        (genSorts1, cons1) =
          recoverSortsAndConstructors $ getFs osens
        (freeSorts, cons2) =
          recoverSortsAndConstructors freeSortGens
        (genSorts2, cons3) =
          recoverSortsAndConstructors sortGens
        sortCons@(genSorts, cons) =
          (Set.unions
           [freeSorts, genSorts2, Set.map (mapSort $ sort_map m) genSorts1]
          , Set.toList $ Set.unions [cons2, cons3, Set.map (mapOpSymb m) cons1])
        oldSorts = sortSet sSig
        newSorts = Set.difference (sortSet sig) oldSorts
        emptySorts = emptySortSet sig
        nonInhabitedSorts = getNefsorts oldSorts newSorts emptySorts sortCons
        (subsortDefns, memShips2) = partitionMaybe isSubsortDef memShips
        defSubsorts = Set.fromList $ map (\ (s, _, _) -> s) subsortDefns
        dataStatus = getDataStatus newSorts defSubsorts genSorts
        defsForOld = getDefsForOld sSig axioms
        opsPredsAndExAxioms = defsForOld ++ exQuants ++ memShips2
        conStatus = getConStatus dataStatus opsPredsAndExAxioms
        memObl = infoSubsorts emptySorts subsortDefns
        axGroup = groupAxioms sig axLessDoms
        overLaps = getOverlapQuery sig axGroup
        obligations = opsPredsAndExAxioms ++ memObl ++ overLaps
        domSyms = lefts $ mapMaybe leadingSym domains
        ms =
          [ checkDefinitional sig axioms
          , checkSort (null axs) newSorts defSubsorts genSorts2 freeSorts
              nonInhabitedSorts sSig sig
          , checkLeadingTerms sig axioms cons
          , checkIncomplete sig obligations domSyms axGroup cons ]
    r <- case catMaybes ms of
      [] -> checkTerminal sig conStatus obligations domains axLessDoms
      a : _ -> return a
    return $ case r of
      Result ds Nothing ->
        case filter (not . checkPos . sentence) $ axs ++ osens of
          [] -> justHint (Cons, []) "theory is positive!"
          l -> let
            ps = map (\ f -> Diag Hint ("formula is not positive:\n  "
              ++ show (printTheoryFormula $ mapNamed (simplifyCASLSen sig) f))
              $ getRange f) $ take 2 l
            in Result (ps ++ ds) Nothing
      _ -> r
  
  {- | group the axioms according to their leading symbol,
  output Nothing if there is some axiom in incorrect form -}
  groupAxioms :: GetRange f => Sign f e -> [FORMULA f] -> [[FORMULA f]]
  groupAxioms sig phis = map (map snd)
     $ Rel.partList (\ (e1, _) (e2, _) -> case (e1, e2) of
         (Left o1, Left o2) -> sameOpSymbs sig o1 o2
         (Right (Qual_pred_name p1 t1 _), Right (Qual_pred_name p2 t2 _)) ->
             p1 == p2 && on (leqP sig) toPredType t1 t2
         _ -> False)
     $ foldr (\ f -> case leadingSym f of
      Just ei -> ((ei, f) :)
      Nothing -> id) [] phis
  
  -- | return the non-constructor terms of arguments of a leading term
  checkTerms :: Sign f e -> [OP_SYMB] -> [TERM f] -> [TERM f]
  checkTerms sig cons = concatMap checkT
    where checkT t = case unsortedTerm t of
            Qual_var {} -> []
            Application subop subts _ ->
              if isCons sig cons subop then concatMap checkT subts else [t]
            _ -> [t]
  
  {- | check whether the operation symbol is a constructor
  (or a related overloaded variant). -}
  isCons :: Sign f e -> [OP_SYMB] -> OP_SYMB -> Bool
  isCons sig cons os = any (sameOpSymbs sig os) cons
  
  -- | create all possible pairs from a list
  pairs :: [a] -> [(a, a)]
  pairs ps = case ps of
    hd : tl@(_ : _) -> map (\ x -> (hd, x)) tl ++ pairs tl
    _ -> []
  
  -- | create the proof obligation for a pair of overlapped formulas
  overlapQuery :: GetRange f => FORMULA f -> FORMULA f -> FORMULA f
  overlapQuery a1 a2 =
          case leadingSym a1 of
            Just (Left _)
              | containNeg a1 && not (containNeg a2) ->
                  mkImpl (conjunct [con1, con2])
                              (mkNeg (Definedness resT2 nullRange))
              | containNeg a2 && not (containNeg a1) ->
                  mkImpl (conjunct [con1, con2])
                              (mkNeg (Definedness resT1 nullRange))
              | containNeg a1 && containNeg a2 -> trueForm
              | otherwise ->
                  mkImpl (conjunct [con1, con2])
                              (mkStEq resT1 resT2)
            Just (Right _)
              | containNeg a1 && not (containNeg a2) ->
                  mkImpl (conjunct [con1, con2])
                              (mkNeg resA2)
              | containNeg a2 && not (containNeg a1) ->
                  mkImpl (conjunct [con1, con2])
                              (mkNeg resA1)
              | containNeg a1 && containNeg a2 -> trueForm
              | otherwise ->
                  mkImpl (conjunct [con1, con2])
                              (conjunct [resA1, resA2])
            _ -> error "CASL.CCC.FreeTypes.<overlapQuery>"
        where [con1, con2] = map conditionAxiom [a1, a2]
              [resT1, resT2] = map resultTerm [a1, a2]
              [resA1, resA2] = map resultAxiom [a1, a2]
  
  getNotComplete :: (Ord f, FormExtension f, TermExtension f)
    => Sign f e -> [OP_SYMB] -> [[FORMULA f]] -> [OP_SYMB]
    -> [(Result [(String, FORMULA f)], [FORMULA f])]
  getNotComplete sig doms fsn constructors =
    let consMap = foldr (\ (Qual_op_name o ot _) ->
          MapSet.insert (res_OP_TYPE ot) (o, ot)) MapSet.empty constructors
        consMap2 = foldr (\ (Qual_op_name o ot _) ->
          MapSet.insert o ot) MapSet.empty constructors
    in
    filter (\ (Result ds mfs, _) -> not (null ds)
        || maybe False (not . null) mfs)
    $ map (\ g ->
           (let l = map topIdOfAxiom g in
                    case Set.toList . Set.fromList $ map fst l of
                      [(p, i)] -> completePatterns sig doms consMap consMap2
                        ([(showId p "", i)]
                        , zip g $ map snd l)
                      l2 -> Fail.fail $ "wrongly grouped leading terms "
                        ++ show l2
           , g)) fsn
  
  type LeadArgs = [(String, Int)]
  
  getNextArg :: Bool -> String -> LeadArgs -> (Bool, String, LeadArgs)
  getNextArg b p l = case l of
    [] -> (False, if b then p else "_", [])
    h : r -> case h of
      (i, c) -> if c == 0 then (b, i, r) else
        let (b1, sl, r2) = getNextN c b p r
        in (b1, i ++ "(" ++ intercalate ", " sl ++ ")", r2)
  
  getNextN :: Int -> Bool -> String -> LeadArgs -> (Bool, [String], LeadArgs)
  getNextN c b p l = if c <= 0 then (b, [], l) else
    let (b1, s, r) = getNextArg b p l
        (b2, sl, r2) = getNextN (c - 1) b1 p r
    in (b2, s : sl, r2)
  
  showLeadingArgs :: String -> LeadArgs -> String
  showLeadingArgs p l = let (_, r, _) = getNextArg True p $ reverse l in r
  
  -- | check whether the patterns of a function or predicate are complete
  completePatterns :: (Ord f, FormExtension f, TermExtension f) => Sign f e
    -> [OP_SYMB] -> MapSet.MapSet SORT (OP_NAME, OP_TYPE)
    -> MapSet.MapSet OP_NAME OP_TYPE
    -> (LeadArgs, [(FORMULA f, [TERM f])])
    -> Result [(String, FORMULA f)]
  completePatterns tsig doms consMap consMap2 (leadingArgs, pas)
      | all (null . snd) pas =
         let fs = checkExhaustive tsig doms $ map fst pas
         in return $ map (\ f -> (showLeadingArgs "" leadingArgs, f)) fs
      | any (null . snd) pas = Fail.fail "wrongly grouped leading terms"
      | otherwise = let hds = map (\ (f, hd : _) -> (f, hd)) pas in
              if all (isVar . snd) hds
              then let
                tls = map (\ (f, _ : tl) -> (f, tl)) pas
                in completePatterns tsig doms consMap consMap2
                        (("_", 0) : leadingArgs, tls)
              else let
                consAppls@(_ : _) = mapMaybe (\ (f, t) -> case unsortedTerm t of
                  Application (Qual_op_name o ot _) _ _ ->
                    Just (f, o, Set.filter (sameOpTypes tsig ot)
                      $ MapSet.lookup o consMap2)
                  _ -> Nothing) hds
                consSrt = foldr1 Set.intersection
                  $ map (\ (_, _, os) -> Set.map res_OP_TYPE os) consAppls
                in case filter (not . Set.null . (`MapSet.lookup` consMap))
                       $ Set.toList consSrt of
                    [] -> Fail.fail $
                      "no common result type for constructors found: "
                         ++ showDoc (map snd hds) ""
                    cSrt : _ -> do
                      let allCons = MapSet.lookup cSrt consMap
                      when (Set.null allCons) . Fail.fail
                        $ "no constructors for result type found: " ++ show cSrt
                      let cons_group = map (\ (c, ct) -> (c, ct,
                            filter (\ (_, h : _) -> case unsortedTerm h of
                              Application (Qual_op_name o ot _) _ _ ->
                                c == o && sameOpTypes tsig ct ot
                              _ -> False) pas)) $ Set.toList allCons
                          vars = filter (\ (_, h : _) -> isVar h) pas
                      ffs <- mapM (\ f -> checkConstructor leadingArgs vars f
                          >>= completePatterns tsig doms consMap consMap2)
                        cons_group
                      return $ concat ffs
  
  mkVars :: [SORT] -> [TERM f]
  mkVars = zipWith (\ i -> mkVarTerm (mkSimpleId $ 'c' : show i)) [1 :: Int ..]
  
  checkConstructor :: (Ord f, FormExtension f, TermExtension f)
    => LeadArgs -> [(FORMULA f, [TERM f])]
    -> (Id, OP_TYPE, [(FORMULA f, [TERM f])])
    -> Result (LeadArgs, [(FORMULA f, [TERM f])])
  checkConstructor leadingArgs vars (c, ct, es) = do
    let args = args_OP_TYPE ct
        nL = (showId c "", length args) : leadingArgs
        varEqs = map (\ (f, _ : t) -> (f, mkVars args ++ t)) vars
        pat = showLeadingArgs
             (showId c "" ++ case args of
               [] -> ""
               l -> "(" ++ intercalate "," (map (const "_") l) ++ ")")
             leadingArgs
    case es of
      [] -> do
        when (null vars) $ justWarn ()
           $ "missing pattern for: " ++ pat
        return (nL, varEqs)
      _ ->
        return (nL, varEqs ++ map (\ (f, h : t) -> (f, arguOfTerm h ++ t)) es)
  
  -- | get condition axiom without matching definedness condition
  getCond :: (GetRange f, Eq f) => Sign f e -> [OP_SYMB] -> FORMULA f -> FORMULA f
  getCond sig doms f =
    let (cs, e) = splitAxiom f
    in conjunct $ filter (\ c -> case leadingTermPredication e of
         l@(Just (Left (Application os _ _)))
           | any (sameOpSymbs sig os) doms
           -> case c of  -- pattern term must be identical
                Definedness {} | leadingTermPredication c == l -> False
                _ -> True
         _ -> True) cs
  
  checkExhaustive :: (Ord f, FormExtension f, TermExtension f)
    => Sign f e -> [OP_SYMB] -> [FORMULA f] -> [FORMULA f]
  checkExhaustive sig doms es = case es of
    f1 : rs ->
      let sfs = map (\ f -> (getSubstForm sig f1 f, f)) rs
          overlap = filter (isJust . maybeResult . fst) sfs
          simpAndQuant = quant sig . simplifyFormula id
      in case overlap of
         [] -> filter (not . is_True_atom)
            (map (simpAndQuant . getCond sig doms) [f1])
            ++ checkExhaustive sig doms rs
         (r, f2) : rrs -> let
            (f3, f4, ((s3, _), (s4, _))) = convert2Forms sig f1 f2 r
            in checkExhaustive sig doms
           $ (simpAndQuant
           . mkImpl (disjunct [ replaceVarsF s3 id $ getCond sig doms f3
                              , replaceVarsF s4 id $ getCond sig doms f4 ])
             . replaceVarsF s3 id $ restAxiom f3) : map snd rrs
    [] -> []
  