content: {- |
  Module      :  ./DFOL/Analysis_DFOL.hs
  Description :  Static analysis for first-order logic with dependent types (DFOL)
  Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  k.sojakova@jacobs-university.de
  Stability   :  experimental
  Portability :  portable
  -}
  
  module DFOL.Analysis_DFOL
    (
      basicAnalysis         -- static analysis of basic specifications
    , symbAnalysis          -- static analysis for symbols lists
    , symbMapAnalysis       -- static analysis for symbol map lists
     ) where
  
  import DFOL.Utils
  import DFOL.AS_DFOL
  import DFOL.Sign
  import DFOL.Symbol
  
  import Common.DocUtils
  import Common.ExtSign
  import Common.GlobalAnnotations
  import Common.Id
  import qualified Common.Result as Result
  import qualified Common.AS_Annotation as Anno
  
  import qualified Data.Set as Set
  import qualified Data.Map as Map
  
  -- BASIC SPEC ANALYSIS
  basicAnalysis :: (BASIC_SPEC, Sign, GlobalAnnos) ->
     Result.Result (BASIC_SPEC, ExtSign Sign Symbol, [Anno.Named FORMULA])
  basicAnalysis (bs, sig, _) =
     if errs
        then Result.Result diag Nothing
        else Result.Result [] $ Just (bs, ExtSign newSig declaredSyms, formulae)
     where Diagn diag1 newSig = makeSig bs sig
           Diagn diag2 formulae = makeFormulas bs newSig
           declaredSyms = Set.map Symbol
                           $ Set.difference (getSymbols newSig) (getSymbols sig)
           diag = diag1 ++ diag2
           errs = Result.hasErrors diag
  
  {- SIGNATURES
  make a new signature out of a basic spec and an input signature -}
  makeSig :: BASIC_SPEC -> Sign -> DIAGN Sign
  makeSig (Basic_spec items) = addItemsToSig items
  
  -- adds a list of annotated basic items to an input signature
  addItemsToSig :: [Anno.Annoted BASIC_ITEM] -> Sign -> DIAGN Sign
  addItemsToSig [] sig = Diagn [] sig
  addItemsToSig (i : is) sig =
     case i of
          (Anno.Annoted (Axiom_item _) _ _ _) -> addItemsToSig is sig
          (Anno.Annoted (Decl_item d) _ _ _) ->
               if Result.hasErrors diag
                  then Diagn diag sig
                  else addItemsToSig is newSig
               where Diagn diag newSig = addDeclToSig d sig
  
  -- adds a declaration to an existing signature
  addDeclToSig :: DECL -> Sign -> DIAGN Sign
  addDeclToSig dec sig = if valid
                            then Diagn [] $ addSymbolDecl dec sig
                            else Diagn diag sig
                         where Diagn diag valid = isValidDecl dec sig emptyContext
  
  {- FORMULAS
  make a list of formulas for the given signature out of a basic spec -}
  makeFormulas :: BASIC_SPEC -> Sign -> DIAGN [Anno.Named FORMULA]
  makeFormulas (Basic_spec items) = makeFormulasFromItems items 0
  
  -- make a list of named formulas out of a list of annotated items
  makeFormulasFromItems :: [Anno.Annoted BASIC_ITEM] -> Int
                           -> Sign -> DIAGN [Anno.Named FORMULA]
  makeFormulasFromItems [] _ _ = Diagn [] []
  makeFormulasFromItems (i : is) num sig =
      case i of
           (Anno.Annoted (Decl_item _) _ _ _) -> makeFormulasFromItems is num sig
           (Anno.Annoted (Axiom_item a) _ _ annos) ->
             case fM of
                  Just f ->
                     let Diagn diagL fs = makeFormulasFromItems is newNum sig
                         in Diagn diagL (f : fs)
                  Nothing ->
                     let Diagn diagL fs = makeFormulasFromItems is num sig
                         in Diagn (diag ++ diagL) fs
             where Result.Result diag fM = makeNamedFormula a nam annos sig
                   label = Anno.getRLabel i
                   nam = if label == "" then "Ax_" ++ show num else label
                   newNum = if label == "" then num + 1 else num
  
  -- make a named formula
  makeNamedFormula :: FORMULA -> String -> [Anno.Annotation]
                      -> Sign -> Result.Result (Anno.Named FORMULA)
  makeNamedFormula f nam annos sig =
      if valid
         then Result.Result [] $ Just namedF
         else Result.Result diag Nothing
      where Diagn diag valid = isValidFormula f sig emptyContext
            namedF = (Anno.makeNamed nam f) {Anno.isAxiom = not isTheorem}
            isImplies = any Anno.isImplies annos
            isImplied = any Anno.isImplied annos
            isTheorem = isImplies || isImplied
  
  -- determines whether a formula is valid w.r.t. a signature and a context
  isValidFormula :: FORMULA -> Sign -> CONTEXT -> DIAGN Bool
  isValidFormula T _ _ = Diagn [] True
  isValidFormula F _ _ = Diagn [] True
  isValidFormula (Pred t) sig cont = hasType t Form sig cont
  isValidFormula (Equality term1 term2) sig cont =
      case type1M of
           Nothing -> Diagn diag1 False
           Just type1 -> case type1 of
                              Univ _ -> hasType term2 type1 sig cont
                              _ -> Diagn [noDiscourseTermError term1 type1 cont]
                                         False
      where Result.Result diag1 type1M = getTermType term1 sig cont
  isValidFormula (Negation f) sig cont = isValidFormula f sig cont
  isValidFormula (Conjunction fs) sig cont =
     andD $ map (\ f -> isValidFormula f sig cont) fs
  isValidFormula (Disjunction fs) sig cont =
     andD $ map (\ f -> isValidFormula f sig cont) fs
  isValidFormula (Implication f g) sig cont =
     andD [isValidFormula f sig cont, isValidFormula g sig cont]
  isValidFormula (Equivalence f g) sig cont =
     andD [isValidFormula f sig cont, isValidFormula g sig cont]
  isValidFormula (Forall [] f) sig cont = isValidFormula f sig cont
  isValidFormula (Forall (d : ds) f) sig cont =
     andD [validDecl, validFormula]
     where validDecl = isValidVarDecl d sig cont
           validFormula = isValidFormula (Forall ds f) sig (addVarDecl d cont)
  isValidFormula (Exists [] f) sig cont = isValidFormula f sig cont
  isValidFormula (Exists (d : ds) f) sig cont =
     andD [validDecl, validFormula]
     where validDecl = isValidVarDecl d sig cont
           validFormula = isValidFormula (Exists ds f) sig (addVarDecl d cont)
  
  {- SYMBOL LIST AND MAP ANALYSIS
  creates a symbol map out of a list of symbol map items -}
  symbMapAnalysis :: [SYMB_MAP_ITEMS] -> Result.Result (Map.Map Symbol Symbol)
  symbMapAnalysis xs = Result.Result []
       $ Just $ foldl (\ m x -> Map.union m (makeSymbMap x)) Map.empty xs
  
  -- creates a symbol map out of symbol map items
  makeSymbMap :: SYMB_MAP_ITEMS -> Map.Map Symbol Symbol
  makeSymbMap (Symb_map_items xs) =
     foldl (\ m x -> case x of
                          Symb s -> Map.insert (Symbol s) (Symbol s) m
                          Symb_map s1 s2 -> Map.insert (Symbol s1) (Symbol s2) m
           )
           Map.empty
           xs
  
  -- creates a symbol list out of a list of symbol items
  symbAnalysis :: [SYMB_ITEMS] -> Result.Result [Symbol]
  symbAnalysis xs = Result.Result [] $ Just $ concatMap makeSymbols xs
  
  -- creates a symbol list out of symbol item
  makeSymbols :: SYMB_ITEMS -> [Symbol]
  makeSymbols (Symb_items symbs) = map Symbol symbs
  
  -- ERROR MESSAGES
  noDiscourseTermError :: TERM -> TYPE -> CONTEXT -> Result.Diagnosis
  noDiscourseTermError term t cont =
    Result.Diag
      { Result.diagKind = Result.Error
      , Result.diagString = "Term " ++ show (pretty term)
                            ++ " has the non-discourse type " ++ show (pretty t)
                            ++ " in the context " ++ show (pretty cont)
                            ++ " and hence cannot be used in an equality."
      , Result.diagPos = nullRange
      }
  