{- |
Module      :  ./QBF/Analysis.hs
Description :  Basic analysis for propositional logic extended with QBFs
Copyright   :  (c) Jonathan von Schroeder, DFKI GmbH 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  jonathan.von_schroeder@dfki.de
Stability   :  experimental
Portability :  portable

Basic and static analysis for propositional logic

  Ref.
  <http://en.wikipedia.org/wiki/Propositional_logic>
  <http://www.voronkov.com/lics.cgi>
-}

module QBF.Analysis
    (
     basicPropositionalAnalysis
    , mkStatSymbItems
    , mkStatSymbMapItem
    , inducedFromMorphism
    , inducedFromToMorphism
    , signatureColimit
    )
    where

import Common.ExtSign
import Common.Lib.Graph
import Common.SetColimit
import Data.Graph.Inductive.Graph
import Propositional.Sign as Sign
import qualified Common.AS_Annotation as AS_Anno
import qualified Common.GlobalAnnotations as GlobalAnnos
import qualified Common.Id as Id
import qualified Common.Result as Result
import qualified Data.List as List
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified QBF.AS_BASIC_QBF as AS_BASIC
import qualified QBF.Morphism as Morphism
import qualified QBF.Symbol as Symbol
import Control.Arrow

-- | Datatype for formulas with diagnosis data
data DIAGFORM = DiagForm
    {
      formula :: AS_Anno.Named AS_BASIC.FORMULA,
      diagnosis :: Result.Diagnosis
    }

-- | Formula annotated with a number
data NUMFORM = NumForm
    {
      nfformula :: AS_Anno.Annoted AS_BASIC.FORMULA
    , nfnum :: Integer
    }

data TESTSIG = TestSig
    {
      msign :: Sign.Sign
    , occurence :: Int
    , tdiagnosis :: [Result.Diagnosis]
    }

-- | Retrieves the signature out of a basic spec
makeSig ::
    AS_BASIC.BASICSPEC                   -- Input SPEC
    -> Sign.Sign                         -- Input Signature
    -> TESTSIG                           -- Output Signature
makeSig (AS_BASIC.BasicSpec spec) sig = List.foldl retrieveBasicItem
                                         TestSig { msign = sig
                                                 , occurence = 0
                                                 , tdiagnosis = []
                                                 }
                                         spec

-- Helper for makeSig
retrieveBasicItem ::
    TESTSIG                                      -- Input Signature
    -> AS_Anno.Annoted AS_BASIC.BASICITEMS      -- Input Item
    -> TESTSIG                                   -- Output Signature
retrieveBasicItem tsig x =
    let
        occ = occurence tsig
    in
    case AS_Anno.item x of
      (AS_BASIC.PredDecl apred) ->
          if occ == 0
          then
              List.foldl
                      (\ asig ax -> TestSig {
                                   msign = Sign.addToSig (msign asig)
                                            $ Id.simpleIdToId ax
                                 , occurence = occ
                                 , tdiagnosis = tdiagnosis tsig ++
                                   [Result.Diag
                                    {
                                      Result.diagKind = Result.Hint
                                    , Result.diagString = "All fine"
                                    , Result.diagPos = AS_Anno.opt_pos x
                                    }]
                                 })
                      tsig $ (\ (AS_BASIC.PredItem xs _) -> xs) apred
          else
              List.foldl
                      (\ asig ax -> TestSig {
                                   msign = Sign.addToSig (msign asig)
                                            $ Id.simpleIdToId ax
                                 , occurence = occ
                                 , tdiagnosis = tdiagnosis tsig ++
                                   [Result.Diag
                                    {
                                      Result.diagKind = Result.Error
                                    , Result.diagString =
                                              "Definition of proposition " ++
                                              show (pretty ax) ++
                                              " after first axiom"
                                    , Result.diagPos = AS_Anno.opt_pos x
                                    }]
                                 })
                          tsig $ (\ (AS_BASIC.PredItem xs _) -> xs) apred
      (AS_BASIC.AxiomItems _) -> TestSig { msign = msign tsig
                                          , occurence = occ + 1
                                          , tdiagnosis = tdiagnosis tsig ++
                                              [Result.Diag
                                               {
                                                 Result.diagKind = Result.Hint
                                               , Result.diagString =
                                                         "First axiom"
                                               , Result.diagPos =
                                                         AS_Anno.opt_pos x
                                               }]
                                            }

-- | Retrieve the formulas out of a basic spec
makeFormulas ::
    AS_BASIC.BASICSPEC
    -> Sign.Sign
    -> [DIAGFORM]
makeFormulas (AS_BASIC.BasicSpec bspec) sig =
    List.foldl (\ xs bs -> retrieveFormulaItem xs bs sig) [] bspec

-- Helper for makeFormulas
retrieveFormulaItem ::
    [DIAGFORM]
    -> AS_Anno.Annoted AS_BASIC.BASICITEMS
    -> Sign.Sign
    -> [DIAGFORM]
retrieveFormulaItem axs x sig =
    case AS_Anno.item x of
      (AS_BASIC.PredDecl _) -> axs
      (AS_BASIC.AxiomItems ax) ->
          List.foldl (\ xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0

-- Number formulae
numberFormulae :: [AS_Anno.Annoted AS_BASIC.FORMULA] -> Integer -> [NUMFORM]
numberFormulae [] _ = []
numberFormulae (x : xs) i
    | label == "" =
       NumForm {nfformula = x, nfnum = i} : numberFormulae xs (i + 1)
    | otherwise =
       NumForm {nfformula = x, nfnum = 0} : numberFormulae xs i
    where
      label = AS_Anno.getRLabel x

-- Add a formula to a named list of formulas
addFormula :: [DIAGFORM]
           -> NUMFORM
           -> Sign.Sign
           -> [DIAGFORM]
addFormula formulae nf sign
    | isLegal = formulae ++
                        [DiagForm
                         {
                           formula = makeNamed f i
                         , diagnosis = Result.Diag
                           {
                             Result.diagKind = Result.Hint
                           , Result.diagString = "All fine"
                           , Result.diagPos = lnum
                           }
                         }]
    | otherwise = formulae ++
                        [DiagForm
                         {
                           formula = makeNamed f i
                         , diagnosis = Result.Diag
                                       {
                                         Result.diagKind = Result.Error
                                       , Result.diagString =
                                                 "Unknown propositions "
                                         ++ show (pretty difference)
                                         ++ " in formula "
                                         ++ show (pretty nakedFormula)
                                       , Result.diagPos = lnum
                                       }
                         }]
    where
      f = nfformula nf
      i = nfnum nf
      nakedFormula = AS_Anno.item f
      varsOfFormula = propsOfFormula nakedFormula
      isLegal = Sign.isSubSigOf varsOfFormula sign
      difference = Sign.sigDiff varsOfFormula sign
      lnum = AS_Anno.opt_pos f

-- generates a named formula
makeNamed :: AS_Anno.Annoted AS_BASIC.FORMULA -> Integer
              -> AS_Anno.Named AS_BASIC.FORMULA
makeNamed f i = (AS_Anno.makeNamed (if label == "" then "Ax_" ++ show i
                                       else label) $ AS_Anno.item f)
                    { AS_Anno.isAxiom = not isTheorem }
    where
      label = AS_Anno.getRLabel f
      annos = AS_Anno.r_annos f
      isImplies = foldl (\ y x -> AS_Anno.isImplies x || y) False annos
      isImplied = foldl (\ y x -> AS_Anno.isImplied x || y) False annos
      isTheorem = isImplies || isImplied

-- Retrives the signature of a formula
propsOfFormula :: AS_BASIC.FORMULA -> Sign.Sign
propsOfFormula (AS_BASIC.Negation form _) = propsOfFormula form
propsOfFormula (AS_BASIC.Implication form1 form2 _) = Sign.unite
                                           (propsOfFormula form1)
                                           (propsOfFormula form2)
propsOfFormula (AS_BASIC.Equivalence form1 form2 _) = Sign.unite
                                           (propsOfFormula form1)
                                           (propsOfFormula form2)
propsOfFormula (AS_BASIC.TrueAtom _) = Sign.emptySig
propsOfFormula (AS_BASIC.FalseAtom _) = Sign.emptySig
propsOfFormula (AS_BASIC.Predication x) = Sign.Sign
                         {Sign.items = Set.singleton $
                                       Id.simpleIdToId x }
propsOfFormula (AS_BASIC.Conjunction xs _) = List.foldl
 (\ sig frm -> Sign.unite sig $ propsOfFormula frm)
 Sign.emptySig xs
propsOfFormula (AS_BASIC.Disjunction xs _) = List.foldl
 (\ sig frm -> Sign.unite sig $ propsOfFormula frm)
 Sign.emptySig xs
propsOfFormula (AS_BASIC.ForAll xs f _) = sigDiff
                         (propsOfFormula f)
                         (Sign.Sign (Set.fromList (map Id.simpleIdToId xs)))
propsOfFormula (AS_BASIC.Exists xs f _) = sigDiff
                         (propsOfFormula f)
                         (Sign.Sign (Set.fromList (map Id.simpleIdToId xs)))

-- Basic analysis for propositional logic
basicPropositionalAnalysis
  :: (AS_BASIC.BASICSPEC, Sign.Sign, GlobalAnnos.GlobalAnnos)
  -> Result.Result (AS_BASIC.BASICSPEC,
                    ExtSign Sign.Sign Symbol.Symbol,
                    [AS_Anno.Named AS_BASIC.FORMULA])
basicPropositionalAnalysis (bs, sig, _) =
   Result.Result diags $ if exErrs then Nothing else
     Just (bs, ExtSign sigItems declaredSyms, formulae)
    where
      bsSig = makeSig bs sig
      sigItems = msign bsSig
      declaredSyms = Set.map Symbol.Symbol
        $ Set.difference (items sigItems) $ items sig
      bsForm = makeFormulas bs sigItems
      formulae = map formula bsForm
      diags = map diagnosis bsForm ++ tdiagnosis bsSig
      exErrs = Result.hasErrors diags

-- | Static analysis for symbol maps
mkStatSymbMapItem :: [AS_BASIC.SYMBMAPITEMS]
                  -> Result.Result (Map.Map Symbol.Symbol Symbol.Symbol)
mkStatSymbMapItem xs =
    Result.Result
    {
      Result.diags = []
    , Result.maybeResult = Just $
                           foldl
                           (
                            \ smap x ->
                                case x of
                                  AS_BASIC.SymbMapItems sitem _ ->
                                       Map.union smap $ statSymbMapItem sitem
                           )
                           Map.empty
                           xs
    }

statSymbMapItem :: [AS_BASIC.SYMBORMAP]
                 -> Map.Map Symbol.Symbol Symbol.Symbol
statSymbMapItem =
    foldl
    (
     \ mmap x ->
         case x of
           AS_BASIC.Symb sym -> Map.insert
                                     (symbToSymbol sym)
                                     (symbToSymbol sym) mmap
           AS_BASIC.SymbMap s1 s2 _
             -> Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
    )
    Map.empty

-- | Retrieve raw symbols
mkStatSymbItems :: [AS_BASIC.SYMBITEMS] -> Result.Result [Symbol.Symbol]
mkStatSymbItems a = Result.Result
                    {
                      Result.diags = []
                    , Result.maybeResult = Just $ statSymbItems a
                    }

statSymbItems :: [AS_BASIC.SYMBITEMS] -> [Symbol.Symbol]
statSymbItems = concatMap symbItemsToSymbol

symbItemsToSymbol :: AS_BASIC.SYMBITEMS -> [Symbol.Symbol]
symbItemsToSymbol (AS_BASIC.SymbItems syms _) = map symbToSymbol syms

symbToSymbol :: AS_BASIC.SYMB -> Symbol.Symbol
symbToSymbol (AS_BASIC.SymbId tok) =
    Symbol.Symbol {Symbol.symName = Id.simpleIdToId tok}

pMap :: Map.Map Symbol.Symbol Symbol.Symbol -> Set.Set Id.Id
         -> Map.Map Id.Id Id.Id
pMap imap =
 Set.fold (
  \ x ->
    let
        symOf = Symbol.Symbol
                 { Symbol.symName = x }
        y = Symbol.symName
             $ Symbol.applySymMap imap symOf
    in Map.insert x y
 ) Map.empty

-- | Induce a signature morphism from a source signature and a raw symbol map
inducedFromMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
                    -> Sign.Sign
                    -> Result.Result Morphism.Morphism
inducedFromMorphism imap sig =
    Result.Result
          {
            Result.diags = []
          , Result.maybeResult =
              let
                  sigItems = Sign.items sig
              in
              Just
              Morphism.Morphism
                          {
                            Morphism.source = sig
                          , Morphism.propMap = pMap imap sigItems
                          , Morphism.target = Sign.Sign
                                      {Sign.items =
                                             Set.map (Morphism.applyMap
                                              (pMap imap sigItems))
                                                  $ Sign.items sig
                                      }
                          }
          }

-- | Induce a signature morphism from a source signature and a raw symbol map
inducedFromToMorphism :: Map.Map Symbol.Symbol Symbol.Symbol
                    -> ExtSign Sign.Sign Symbol.Symbol
                    -> ExtSign Sign.Sign Symbol.Symbol
                    -> Result.Result Morphism.Morphism
inducedFromToMorphism imap (ExtSign sig _) (ExtSign tSig _) =
              let
                  sigItems = Sign.items sig
                  targetSig = Sign.Sign
                                               {Sign.items =
                                                    Set.map
                                                       (Morphism.applyMap
                                                        (pMap imap sigItems))
                                                       $ Sign.items sig
                                               }
                  isSub = Sign.items targetSig
                           `Set.isSubsetOf`
                          Sign.items tSig
              in
                if isSub then
                     Result.Result {
                         Result.diags = []
                         , Result.maybeResult =
                             Just Morphism.Morphism
                                 {
                                     Morphism.source = sig
                                     , Morphism.propMap = pMap imap sigItems
                                     , Morphism.target = tSig
                                 }
                     }
                else
                    Result.Result {
                        Result.diags =
                            [
                                Result.Diag
                                    {
                                        Result.diagKind = Result.Error
                                        , Result.diagString =
                                                 "Incompatible mapping"
                                        , Result.diagPos = Id.nullRange
                                    }
                            ]
                        , Result.maybeResult = Nothing
                    }

signatureColimit :: Gr Sign.Sign (Int, Morphism.Morphism)
                 -> Result.Result (Sign.Sign, Map.Map Int Morphism.Morphism)
signatureColimit graph = do
 let graph1 = nmap Sign.items $ emap (Control.Arrow.second Morphism.propMap)
                                     graph
     (set, maps) = addIntToSymbols $ computeColimitSet graph1
     cSig = Sign.Sign {Sign.items = set}
 return (cSig,
         Map.fromList $ map (\ (i, n) ->
                              (i, Morphism.Morphism {
                                    Morphism.source = n,
                                    Morphism.target = cSig,
                                    Morphism.propMap = maps Map.! i
                                  })) $ labNodes graph)