{- |
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 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 $ "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 "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 $
                    "no common result type for constructors found: "
                       ++ showDoc (map snd hds) ""
                  cSrt : _ -> do
                    let allCons = MapSet.lookup cSrt consMap
                    when (Set.null allCons) . 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
  [] -> []
