{- |
Module      :  $Header$
Description :  static analysis of DL parts
Copyright   :  (c) Klaus Luettich, Uni Bremen 2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  luecke@informatik.uni-bremen.de
Stability   :  provisional
Portability :  portable

static analysis of DL parts especially cardinalities, predefined datatypes
and additional annottations
-}

module CASL_DL.StatAna ( basicCASL_DLAnalysis
                       , minDLForm
                       , checkSymbolMapDL
                       , DLSign) where

import CASL_DL.AS_CASL_DL
import CASL_DL.Print_AS ()
import CASL_DL.Sign
import CASL_DL.PredefinedCASLAxioms

import CASL.Sign
import CASL.MixfixParser
import CASL.Morphism
import CASL.StaticAna
import CASL.AS_Basic_CASL
import CASL.ShowMixfix
import CASL.Overload
import CASL.Quantification

import Common.AS_Annotation
import Common.GlobalAnnotations
import Common.ConvertGlobalAnnos
import Common.DocUtils
import Common.Id
import Common.Result
import Common.ConvertLiteral
import Common.ExtSign
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

import qualified Data.Map as Map
import qualified Data.Set as Set

instance TermExtension DL_FORMULA where
    freeVarsOfExt sign (Cardinality _ _ t1 t2 mf _) =
        Set.union (freeTermVars sign t1) $ Set.union (freeTermVars sign t2)
           $ case mf of
               Nothing -> Set.empty
               Just f -> freeVars sign f

basicCASL_DLAnalysis
    :: (BASIC_SPEC () () DL_FORMULA, Sign DL_FORMULA CASL_DLSign, GlobalAnnos)
    -> Result (BASIC_SPEC () () DL_FORMULA,
               ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
               [Named (FORMULA DL_FORMULA)])
basicCASL_DLAnalysis (bs, sig, ga) =
    do ga' <- mergeGlobalAnnos ga $ globAnnos predefSign
       let sig' = addSig addCASL_DLSign sig $ predefinedSign emptyCASL_DLSign
           bs' = transformSortDeclarations True bs
       case basicAnalysis minDLForm (const return)
             (const return) ana_Mix (bs', sig', ga') of
         r@(Result ds1 mr) ->
             maybe r (cleanStatAnaResult . postAna ds1 sig') mr

{- |
  True -> extend all sort declarations without a supersort
          with supersort Thing
  False -> remove Thing from all sort declarations with supersort Thing
-}
generateSubsorting :: Sign f e -> Sign f e
generateSubsorting sig =
    let
        inS = sortSet sig
        inR = sortRel sig
    in
      sig
      {
        sortRel = Set.fold (\ x y -> Rel.insertDiffPair x thing y) inR inS
      }

transformSortDeclarations :: Bool
                          -> BASIC_SPEC () () DL_FORMULA
                          -> BASIC_SPEC () () DL_FORMULA
transformSortDeclarations addThing (Basic_spec aBIs) =
    Basic_spec (processBIs aBIs)
    where processBIs = map (mapAn processBI)
          processBI bi = case bi of
                           Sig_items sig_i -> Sig_items (processSig_i sig_i)
                           _ -> bi
          processSig_i sig_i =
              case sig_i of
                Sort_items sk aSor_is r ->
                    Sort_items sk (concatMap processaSor_i aSor_is) r
                _ -> sig_i
          processaSor_i aSor_i =
              case processSor_i (item aSor_i) of
                [] -> []
                x : xs -> replaceAnnoted x aSor_i : map emptyAnno xs
          processSor_i sor_i =
              if addThing
              then
                    case sor_i of
                      Sort_decl sorts r ->
                          [Subsort_decl sorts thing r]
                      Subsort_decl _ supSort _
                          | supSort == thing -> [sor_i]
                          | otherwise ->
                              [ sor_i
                              , Subsort_decl [supSort] thing statAnaMarker]
                      _ -> [sor_i]
              else
                    case sor_i of
                      Subsort_decl sorts supSort r
                          | supSort == thing -> if r == statAnaMarker
                                                  then []
                                                  else [Sort_decl sorts r]
                          | otherwise -> [sor_i]
                      _ -> [sor_i]

-- | marker for sig items added to a basic spec
statAnaMarker :: Range
statAnaMarker = Range [SourcePos ">:>added for DL.StaticAna<:<" 0 0]

{- |
 * remove predefined symbols from a result of the static analysis

 * remove all explicit references of Thing from the BSIC_SPEC
-}
cleanStatAnaResult
    :: Result (BASIC_SPEC () () DL_FORMULA,
               ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
               [Named (FORMULA DL_FORMULA)])
    -> Result (BASIC_SPEC () () DL_FORMULA,
               ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
               [Named (FORMULA DL_FORMULA)])
cleanStatAnaResult r@(Result ds1 mr) = maybe r clean mr
    where clean (bs, ExtSign sig sys, sen) =
              Result ds1 (Just (transformSortDeclarations False bs
                               , ExtSign (generateSubsorting $ cleanSign sig) $
                                 Set.delete (idToSortSymbol thing) sys
                               , sen))
          cleanSign sig =
              diffSig diffCASL_DLSign sig $ predefinedSign emptyCASL_DLSign

{- |
  postAna checks the Signature for

  * all new sorts must be a proper subsort of Thing and
    must not be related to DATA

  * no new subsort relations with DATA

  * all new predicates must have a subsort of Thing as subject (1st argument)

  * all new operations must have a subsort of Thing as 1st argument

-}
postAna :: [Diagnosis]
        -> Sign DL_FORMULA CASL_DLSign
        -> (BASIC_SPEC () () DL_FORMULA,
            ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
            [Named (FORMULA DL_FORMULA)])
        -> Result (BASIC_SPEC () () DL_FORMULA,
                   ExtSign (Sign DL_FORMULA CASL_DLSign) Symbol,
                   [Named (FORMULA DL_FORMULA)])
postAna ds1 in_sig i@(_, ExtSign acc_sig _, _) =
    Result (ds1 ++ ds_sig) $ if null ds_sig then Just i else Nothing
    where ds_sig = chkSorts ++ checkPreds ++ checkOps
          diff_sig = diffSig diffCASL_DLSign acc_sig in_sig
          chkSorts = Set.fold chSort [] (sortSet diff_sig) ++
             [Diag Error
                        ("\n     new subsort relations with data " ++
                         "topsort are not allowed") nullRange
             | Set.member dataS (supersortsOf thing acc_sig) ||
                 Set.member dataS (subsortsOf thing acc_sig) ||
                 supersortsOf dataS predefSign /=
                  supersortsOf dataS acc_sig ||
                 selectDATAKernel (sortRel predefSign)
                  /= selectDATAKernel (sortRel acc_sig)]
          chSort s ds = ds ++
              [mkDiag Error
                        ("\n     new sort is not a subsort of '" ++
                         showDoc thing "':") s
              | not $ Set.member thing $ supersortsOf s acc_sig]
              ++ [mkDiag Error
                        ("\n     new sort must not be a supersort of '" ++
                         showDoc thing "':") s
                 | Set.member thing (subsortsOf s acc_sig)]
          selectDATAKernel rel =
              Rel.intransKernel $ Rel.restrict rel $
                 Set.insert dataS
                        (subsortsOf dataS predefSign)

          checkPreds = MapSet.foldWithKey chPred [] (predMap diff_sig)
          chPred p ty = (chArgs "pred" p (predArgs ty) ++)
          checkOps = MapSet.foldWithKey chOp [] (opMap diff_sig)
          chOp o ty = (chArgs "op" o (opArgs ty) ++)
          chArgs kstr sym args =
              case args of
              [] -> if kstr == "op"
                    then []
                    else [mkDiag Error
                        "\n     propositional symbols are not allowed" sym]
              (s : _) ->
                  if s == thing ||
                     Set.member thing (supersortsOf s acc_sig)
                  then []
                  else [mkDiag Error
                        ("\n     the first argument sort of this " ++ kstr ++
                        " is not a subsort of '" ++ showDoc thing "':")
                        sym]


{- sketch of Annotation analysis:

    where callAna bsRes =
              case analyseAnnos ga acc_sig bs of
              Result ds2 mESig ->
                  maybe (Result (ds1++ds2) Nothing)
                        (integrateExt (ds1++ds2) baRes) mESig
          integrateExt ds (bs',dif_sig,acc_sig,sens) eSig =
              Result ds (bs',
                         dif_sig {extendedInfo = dif eSig (extendedInfo sig)},
                         acc_sig {extendedInfo = eSig},
                         sens)
-}

ana_Mix :: Mix () () DL_FORMULA CASL_DLSign
ana_Mix = emptyMix
    { putParen = mapDL_FORMULA
    , mixResolve = resolveDL_FORMULA
    }

type DLSign = Sign DL_FORMULA CASL_DLSign

mapDL_FORMULA :: DL_FORMULA -> DL_FORMULA
mapDL_FORMULA (Cardinality ct pn varTerm natTerm qualTerm ps) =
    Cardinality ct pn (mapT varTerm) (mapT natTerm) qualTerm ps
    where mapT = mapTerm mapDL_FORMULA

resolveDL_FORMULA :: MixResolve DL_FORMULA
resolveDL_FORMULA ga ids (Cardinality ct ps varTerm natTerm qualTerm ran) =
    do vt <- resMixTerm varTerm
       nt <- resMixTerm natTerm
       mf <- case qualTerm of
         Nothing -> return Nothing
         Just f -> fmap Just $
                   resolveMixFrm mapDL_FORMULA resolveDL_FORMULA ga ids f
       return $ Cardinality ct ps vt nt mf ran
    where resMixTerm = resolveMixTrm mapDL_FORMULA
                                     resolveDL_FORMULA ga ids

minDLForm :: Min DL_FORMULA CASL_DLSign
minDLForm sign form = case form of
    Cardinality ct ps varTerm natTerm qualTerm ran ->
       let pn = predSymbName ps
           pn_RelTypes = Set.filter isBinPredType
                 $ MapSet.lookup pn (predMap sign)
       in
      if Set.null pn_RelTypes then
                Result [Diag Error ("Unknown binary predicate: \"" ++
                                    show pn ++ "\"") (posOfId pn)]
                       Nothing
      else do
                   v2 <- oneExpTerm minDLForm sign varTerm
                   let v_sort = sortOfTerm v2
                   n2 <- oneExpTerm minDLForm sign natTerm
                   let n_sort = sortOfTerm n2
                   ps' <- case sub_sort_of_subj pn v_sort pn_RelTypes of
                          Result ds mts ->
                            let ds' =
                                 if null ds
                                 then [mkDiag Error
                                       ("Variable in cardinality constraint\n"
                                        ++ "    has wrong type")
                                       varTerm]
                                 else ds
                                amigDs ts =
                                 [Diag Error
                                  ("Ambiguous types found for\n    pred '" ++
                                   showDoc pn "' in cardinalty " ++
                                   "constraint: (showing only two of them)\n" ++
                                   "    '" ++ showDoc (head ts) "', '" ++
                                   showDoc (head $ tail ts) "'") ran]
                             in maybe (Result ds' Nothing)
                              (\ ts -> case ts of
                                [] -> error "CASL_DL.StatAna: Internal error"
                                [x] -> maybe
                                         (return $
                                            Qual_pred_name pn x nullRange)
                                         (\ pt -> if x == pt
                                                  then return ps
                                                  else noPredTypeErr ps)
                                         (getType ps)
                                _ -> maybe (Result (amigDs ts) Nothing)
                                           (\ pt -> if pt `elem` ts
                                                    then return ps
                                                    else noPredTypeErr ps)
                                           (getType ps))
                              mts
                   let isNatTerm =
                           if isNumberTerm (globAnnos sign) n2 &&
                              show n_sort == "nonNegativeInteger"
                           then []
                           else [mkDiag Error
                                    ("The second argument of a\n    " ++
                                     "cardinality constrain must be a " ++
                                     "number literal\n    typeable as " ++
                                     "nonNegativeInteger")
                                    natTerm]
                       ds = isNatTerm
                   appendDiags ds
                   if null ds
                    then return (Cardinality ct ps' v2 n2 qualTerm ran)
                    else Result [] Nothing
    where
          getType ps = case ps of
                        Pred_name _ -> Nothing
                        Qual_pred_name _ pType _ -> Just pType
          isNumberTerm ga t =
              maybe False (uncurry (isNumber ga)) (splitApplM t)

          noPredTypeErr ps = Result
              [mkDiag Error "no predicate with \n    given type found" ps]
              Nothing

          sub_sort_of_subj pn v_sort typeSet =
              foldl (\ (Result ds mv) pt ->
                         case predArgs pt of
                         (s : _)
                             | leqSort sign v_sort s ->
                                 maybe (Result ds $ Just [toPRED_TYPE pt])
                                       (\ l -> Result ds $
                                                   Just $ l ++ [toPRED_TYPE pt])
                                       mv
                             | otherwise ->
                                 Result ds mv
                         _ -> Result (ds ++ [mkDiag Error
                                                  ("no propositional " ++
                                                   "symbols are allowed\n    "
                                                   ++ "within cardinality " ++
                                                   "constraints")
                                                  pn]) mv
                  ) (Result [] Nothing) $ Set.toList typeSet

-- | symbol map analysis
checkSymbolMapDL :: RawSymbolMap -> Result RawSymbolMap
{- - implement a symbol mapping that forbids mapping of predefined symbols
       from emptySign
       use from Logic.Logic.Logic and from CASL:
          matches, symOf, statSymbMapItems
-}
checkSymbolMapDL rsm =
    let checkSourceSymbol sSym _ =
              if any (`matches` sSym) symOfPredefinedSign then
                  (sSym :) else id
        syms = Map.foldWithKey checkSourceSymbol [] rsm
    in if null syms
       then return rsm
       else mkError "Predefined CASL_DL symbols cannot be mapped" syms

symOfPredefinedSign :: [Symbol]
symOfPredefinedSign = Set.toList . Set.unions $ symOf predefSign

isNumber :: GlobalAnnos -> Id -> [TERM f] -> Bool
isNumber = isGenNum splitApplM

splitApplM :: TERM f -> Maybe (Id, [TERM f])
splitApplM t = case t of
    Application _ _ _ -> Just $ splitAppl t
    _ -> Nothing

splitAppl :: TERM f -> (Id, [TERM f])
splitAppl t = case t of
              Application oi ts _ -> (op_id oi, ts)
              _ -> error "splitAppl: no Application found"

-- | extract the Id from any OP_SYMB
op_id :: OP_SYMB -> Id
op_id op = case op of
           Qual_op_name x _ _ -> x
           Op_name x -> x
