content: {-# LANGUAGE MultiParamTypeClasses, TypeSynonymInstances #-}
  {- |
  Module      :  ./THF/StaticAnalysisTHF.hs
  Description :  Static analysis for THF
  Copyright   :  (c) A. Tsogias, DFKI Bremen 2011
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  Alexis.Tsogias@dfki.de
  Stability   :  provisional
  Portability :  portable
  
  Static analysis for THF.
  NOTE: This implementation covers only THF0!
  -}
  
  module THF.StaticAnalysisTHF (basicAnalysis) where
  
  import THF.As as As
  import THF.Cons
  import THF.Print ()
  import THF.Sign
  import THF.Poly (type_check)
  import THF.Utils (thfTopLevelTypeToType)
  
  import Common.AS_Annotation
  import Common.GlobalAnnotations
  import Common.Result
  import Common.ExtSign
  import Common.Lib.State
  import Common.DocUtils
  
  import Control.Monad
  
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  
  {- -----------------------------------------------------------------------------
  Questions:
  how to handle SysType in isTypeConsistent?
  Todo:
  find out what fi_domain, fi_predicates and fi_functors are and try
  to somehow support them
  ----------------------------------------------------------------------------- -}
  
  -- The main method for the static analysis
  basicAnalysis :: (BasicSpecTHF, SignTHF, GlobalAnnos) ->
          Result (BasicSpecTHF, ExtSign SignTHF SymbolTHF, [Named THFFormula])
  basicAnalysis (bs@(BasicSpecTHF bs1), sig1, _) =
      let (diag1, bs2) = filterBS [] bs1
          (diag2, sig2, syms) = execState (fillSig bs2) (diag1, sig1, Set.empty)
          (diag3, ns) = getSentences bs2 (diag2, [])
      in do
       type_check (types sig2) (consts sig2) ns
       Result (reverse diag3) $ Just (bs, ExtSign sig2 syms, ns)
  
  {- This functions delets all Comments and Includes because they are not needed
  for the static analysis
  The diagnosis list has a reverted order! -}
  filterBS :: [Diagnosis] -> [TPTP_THF] -> ([Diagnosis], [TPTP_THF])
  filterBS d [] = (d, [])
  filterBS d (t : rt) = case t of
      TPTP_Include i -> let ds = mkDiag Warning "Include will be ignored." i
                        in filterBS (ds : d) rt
      TPTP_Comment _ -> filterBS d rt
      TPTP_Defined_Comment _ -> filterBS d rt
      TPTP_System_Comment _ -> filterBS d rt
      TPTP_Header _ -> filterBS d rt
      _ -> let (diag, thf) = filterBS d rt
                                 in (diag, t : thf)
  
  -- Append the Signature by the Types and Constants given inside the basic spec
  fillSig :: [TPTP_THF] -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()
  fillSig [] = return ()
  fillSig bs = mapM_ fillSingleType bs >> mapM_ fillSingleConst bs
      where
          fillSingleType t = case t of
              TPTP_THF_Annotated_Formula n fr tf a -> case fr of
                  Type ->
                      when (isKind tf) $ case makeKind tf of
                          Right d -> appandDiag d
                          Left (k, c) -> insertType c n k a
                  _ -> return ()
              _ -> return ()
          fillSingleConst t = case t of
              TPTP_THF_Annotated_Formula n fr tf a -> case fr of
                  Type ->
                      unless (isKind tf) $ case makeType tf of
                          Right d -> appandDiag d
                          Left (ty, c) -> insertConst c n ty a
                  _ -> return ()
              _ -> return ()
  
  {- Append the Diagnosis-List by the given Diagnosis
  The new diag will be put on top of the existing list. -}
  appandDiag :: Diagnosis -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()
  appandDiag d = modify (\ (diag, s, syms) -> (d : diag, s, syms))
  
  -- insert the given type into the Signature
  insertType :: Constant -> As.Name -> Kind -> Annotations
                      -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()
  insertType c n k a = do
      (diag, sig, syms) <- get
      if sigHasConstSymbol c sig then appandDiag $ mkDiag Error
          "Duplicate definition of a symbol as a type constant. Symbol: " c
       else
          if sigHasTypeSymbol c sig then
              unless (sigHasSameKind c k sig) $ appandDiag $
                  mkDiag Error ("A type with the same identifier"
                      ++ "but another Kind is already inside the signature") c
           else do -- everythign is fine
              let ti = TypeInfo { typeId = c, typeName = n, typeKind = k
                                , typeAnno = a }
                  sym = Symbol { symId = c, symName = n, symType = ST_Type k }
              put (diag, sig { types = Map.insert c ti (types sig)
                             , symbols = Map.insert c sym (symbols sig) }
                  , Set.insert sym syms)
  
  -- insert the given constant into the Signature
  insertConst :: Constant -> As.Name -> Type -> Annotations
                      -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()
  insertConst c n t a = do
      (_, sig, _) <- get
      if sigHasTypeSymbol c sig then (appandDiag $ mkDiag Error
          "Duplicate definition of a symbol as a type constant. Symbol: " c)
      else do
            isTypeConsistent t
            if sigHasConstSymbol c sig then
                 unless (sigHasSameType c t sig) $ appandDiag $ mkDiag Error
                   ("A constant with the same identifier but another " ++
                    "type is already inside the signature") c
             else -- everything is fine
                   let ci = ConstInfo { constId = c, constName = n, constType = t
                                      , constAnno = a }
                       sym = Symbol { symId = c, symName = n
                                    , symType = ST_Const t }
                   in do
                       (diag', sig', syms') <- get
                       put (diag', sig' { consts = Map.insert c ci (consts sig')
                                        , symbols = Map.insert c sym (symbols sig') }
                                        , Set.insert sym syms')
  
  -- Check if a type symbol is already inside the sig
  sigHasTypeSymbol :: Constant -> SignTHF -> Bool
  sigHasTypeSymbol c sig = Map.member c (types sig)
  
  {- This Method is ment to be used after sigHasTypeSymbol
  Check if a type symbol with the same kind is inside the Sig
  If this is not the case me have a problem! -}
  sigHasSameKind :: Constant -> Kind -> SignTHF -> Bool
  sigHasSameKind c k sig = typeKind (types sig Map.! c) == k
  
  -- Check if a const symbol is already inside the sig
  sigHasConstSymbol :: Constant -> SignTHF -> Bool
  sigHasConstSymbol c sig = Map.member c (consts sig)
  
  {- This Method is ment to be used after sigHasConstSymbol
  Check if a const symbol with the same type is inside the Sig
  If this is not the case me have a problem! -}
  sigHasSameType :: Constant -> Type -> SignTHF -> Bool
  sigHasSameType c t sig = constType (consts sig Map.! c) == t
  
  {- check if all cTypes inside the given Type are elements of the signaure.
  Nothing means that everything is fine, otherwise Just diag will be returned. -}
  isTypeConsistent :: Type -> State ([Diagnosis], SignTHF, Set.Set SymbolTHF) ()
  isTypeConsistent t = do
   (_, sig, _) <- get
   case t of
      MapType t1 t2 -> do
       isTypeConsistent t1
       isTypeConsistent t2
      ParType t1 -> isTypeConsistent t1
      CType c -> when (not (sigHasTypeSymbol c sig))
                 (do
                   insertType c (N_Atomic_Word c) Kind Null
                   appandDiag $ mkDiag Warning "Unknown type: " c)
      ProdType ts -> mapM_ isTypeConsistent ts
      _ -> return ()
      -- SType _ -> ... -- how to handle these?
  
  {- -----------------------------------------------------------------------------
  Extract the sentences from the basic spec
  ----------------------------------------------------------------------------- -}
  
  {- Get all sentences from the content of the BasicSpecTH
  The diag list has a reverted order. -}
  getSentences :: [TPTP_THF] -> ([Diagnosis], [Named THFFormula])
                             -> ([Diagnosis], [Named THFFormula])
  getSentences [] dn = dn
  getSentences (t : rt) dn@(d, ns) = case t of
      TPTP_THF_Annotated_Formula _ fr _ _ -> case fr of
          Type -> getSentences rt dn
          Unknown ->
              let diag = mkDiag Warning
                      "THFFormula with role \'unknown\' will be ignored." t
              in getSentences rt (diag : d, ns)
          Plain ->
              let diag = mkDiag Warning
                      "THFFormula with role \'plain\' will be ignored." t
              in getSentences rt (diag : d, ns)
          Fi_Domain ->
              let diag = mkDiag Warning
                      "THFFormula with role \'fi_domain\' will be ignored." t
              in getSentences rt (diag : d, ns)
          Fi_Functors ->
              let diag = mkDiag Warning
                      "THFFormula with role \'fi_functors\' will be ignored." t
              in getSentences rt (diag : d, ns)
          Fi_Predicates ->
              let diag = mkDiag Warning
                      "THFFormula with role \'fi_predicates\' will be ignored." t
              in getSentences rt (diag : d, ns)
          Assumption ->
              let diag = mkDiag Warning
                      "THFFormula with role \'assumption\' will be ignored." t
              in getSentences rt (diag : d, ns)
          _ ->
              let (d1, ns1) = getSentences rt dn
              in (d1, tptpthfToNS t : ns1)
      _ -> getSentences rt dn
  
  {- Precondition: The formulaRole must not be Type, Unknown, Plain, Fi_Domain
  Fi_Functors, Fi_Predicates or Assumption
  (They are filtered out in getSentences) -}
  tptpthfToNS :: TPTP_THF -> Named THFFormula
  tptpthfToNS f =
    let s = makeNamed (show $ pretty $ nameAF f) (thfFormulaAF f)
        t = s { isAxiom = False }
        w = s { wasTheorem = True }
    in case formulaRoleAF f of
      Definition -> s { isDef = True }
      Conjecture -> t
      Negated_Conjecture -> t
      Theorem -> w
      Lemma -> w
      Hypothesis -> t
      _ -> s -- { isAxiom = True, isDef = False, wasTheorem = False }
  
  
  {- -----------------------------------------------------------------------------
  Get the Kind of a type
  ----------------------------------------------------------------------------- -}
  
  makeKind :: THFFormula -> Either (Kind, Constant) Diagnosis
  makeKind t = maybe (Right $ mkDiag Error "Error while parsing the kind of:" t)
                  Left (thfFormulaToKind t)
  
  thfFormulaToKind :: THFFormula -> Maybe (Kind, Constant)
  thfFormulaToKind (T0F_THF_Typed_Const tc) = thfTypedConstToKind tc
  thfFormulaToKind _ = Nothing
  
  thfTypedConstToKind :: THFTypedConst -> Maybe (Kind, Constant)
  thfTypedConstToKind (T0TC_THF_TypedConst_Par tcp) = thfTypedConstToKind tcp
  thfTypedConstToKind (T0TC_Typed_Const c tlt) =
              maybe Nothing (\ k -> Just (k, c))
                  (thfTopLevelTypeToKind tlt)
  
  thfTopLevelTypeToKind :: THFTopLevelType -> Maybe Kind
  thfTopLevelTypeToKind tlt = case tlt of
      T0TLT_THF_Binary_Type bt -> thfBinaryTypeToKind bt
      T0TLT_Defined_Type _ -> Just Kind
      _ -> Nothing
  
  thfBinaryTypeToKind :: THFBinaryType -> Maybe Kind
  thfBinaryTypeToKind bt = case bt of
      T0BT_THF_Binary_Type_Par btp -> thfBinaryTypeToKind btp
      _ -> Nothing
  
  {- -----------------------------------------------------------------------------
  Get the Type of a constant
  ----------------------------------------------------------------------------- -}
  
  makeType :: THFFormula -> Either (Type, Constant) Diagnosis
  makeType t = maybe (Right $ mkDiag Error "Error while parsing the type of:" t)
                  Left (thfFormulaToType t)
  
  thfFormulaToType :: THFFormula -> Maybe (Type, Constant)
  thfFormulaToType (T0F_THF_Typed_Const tc) = thfTypedConstToType tc
  thfFormulaToType _ = Nothing
  
  thfTypedConstToType :: THFTypedConst -> Maybe (Type, Constant)
  thfTypedConstToType (T0TC_THF_TypedConst_Par tcp) = thfTypedConstToType tcp
  thfTypedConstToType (T0TC_Typed_Const c tlt) =
              maybe Nothing (\ t -> Just (t, c))
                  (thfTopLevelTypeToType tlt)
  
  {- -----------------------------------------------------------------------------
  Check if a THFFormula is a Type definition
  ----------------------------------------------------------------------------- -}
  
  isKind :: THFFormula -> Bool
  isKind tf = case tf of
      T0F_THF_Typed_Const tc -> thfTypedConstIsKind tc
      _ -> False
  
  thfTypedConstIsKind :: THFTypedConst -> Bool
  thfTypedConstIsKind tc = case tc of
      T0TC_THF_TypedConst_Par tcp -> thfTypedConstIsKind tcp
      T0TC_Typed_Const _ tlt -> thfTopLevelTypeIsKind tlt
  
  thfTopLevelTypeIsKind :: THFTopLevelType -> Bool
  thfTopLevelTypeIsKind tlt = case tlt of
      T0TLT_THF_Binary_Type bt -> thfBinaryTypeIsKind bt
      T0TLT_Defined_Type dt -> thfDefinedTypeIsKind dt
      _ -> False
  
  thfDefinedTypeIsKind :: DefinedType -> Bool
  thfDefinedTypeIsKind dt = case dt of
      DT_tType -> True
      _ -> False
  
  thfBinaryTypeIsKind :: THFBinaryType -> Bool
  thfBinaryTypeIsKind bt = case bt of
      T0BT_THF_Binary_Type_Par btp -> thfBinaryTypeIsKind btp
      _ -> False
  