content: {- |
  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)
  