content: {- |
  Module      :  ./Propositional/Analysis.hs
  Description :  Basic analysis for propositional logic
  Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
  License     :  GPLv2 or higher, see LICENSE.txt
  
  Maintainer  :  luecke@informatik.uni-bremen.de
  Stability   :  experimental
  Portability :  portable
  
  Basic and static analysis for propositional logic
  
    Ref.
    <http://en.wikipedia.org/wiki/Propositional_logic>
  -}
  
  module Propositional.Analysis
      ( basicPropositionalAnalysis
      , mkStatSymbItems
      , mkStatSymbMapItem
      , inducedFromMorphism
      , inducedFromToMorphism
      , signatureColimit
      , pROPsen_analysis
      )
      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 Control.Monad.Fail as Fail
  import qualified Data.List as List
  import qualified Data.Map as Map
  import qualified Data.Set as Set
  import qualified Propositional.AS_BASIC_Propositional as AS_BASIC
  import qualified Propositional.Morphism as Morphism
  import qualified Propositional.Symbol as Symbol
  
  -- | Datatype for formulas with diagnosis data
  data DIAG_FORM = DiagForm
      {
        formula :: AS_Anno.Named AS_BASIC.FORMULA,
        diagnosis :: Result.Diagnosis
      }
  
  -- | Formula annotated with a number
  data NUM_FORM = NumForm
      {
        nfformula :: AS_Anno.Annoted AS_BASIC.FORMULA
      , nfnum :: Integer
      }
  
  data TEST_SIG = TestSig
      {
        msign :: Sign.Sign
      , occurence :: Int
      , tdiagnosis :: [Result.Diagnosis]
      }
  
  -- | Retrieves the signature out of a basic spec
  makeSig ::
      AS_BASIC.BASIC_SPEC                  -- Input SPEC
      -> Sign.Sign                         -- Input Signature
      -> TEST_SIG                          -- Output Signature
  makeSig (AS_BASIC.Basic_spec spec) sig = List.foldl retrieveBasicItem
                                           TestSig { msign = sig
                                                   , occurence = 0
                                                   , tdiagnosis = []
                                                   }
                                           spec
  
  -- Helper for makeSig
  retrieveBasicItem ::
      TEST_SIG                                      -- Input Signature
      -> AS_Anno.Annoted AS_BASIC.BASIC_ITEMS       -- Input Item
      -> TEST_SIG                                   -- Output Signature
  retrieveBasicItem tsig x =
      let
          occ = occurence tsig
          nocc = occ == 0
      in
      case AS_Anno.item x of
        AS_BASIC.Pred_decl apred -> List.foldl (\ asig ax -> TestSig
          { msign = Sign.addToSig (msign asig) $ Id.simpleIdToId ax
          , occurence = occ
          , tdiagnosis = tdiagnosis tsig ++
              [ Result.Diag
                { Result.diagKind = if nocc then Result.Hint else Result.Error
                , Result.diagString = if nocc then "All fine" else
                   "Definition of proposition " ++ show (pretty ax)
                   ++ " after first axiom"
                , Result.diagPos = AS_Anno.opt_pos x }]
          }) tsig $ (\ (AS_BASIC.Pred_item xs _) -> xs) apred
        AS_BASIC.Axiom_items _ -> 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.BASIC_SPEC
      -> Sign.Sign
      -> [DIAG_FORM]
  makeFormulas (AS_BASIC.Basic_spec bspec) sig =
      List.foldl (\ xs bs -> retrieveFormulaItem xs bs sig) [] bspec
  
  -- Helper for makeFormulas
  retrieveFormulaItem ::
      [DIAG_FORM]
      -> AS_Anno.Annoted AS_BASIC.BASIC_ITEMS
      -> Sign.Sign
      -> [DIAG_FORM]
  retrieveFormulaItem axs x sig =
      case AS_Anno.item x of
        AS_BASIC.Pred_decl _ -> axs
        AS_BASIC.Axiom_items ax ->
            List.foldl (\ xs bs -> addFormula xs bs sig) axs $ numberFormulae ax 0
  
  -- Number formulae
  numberFormulae :: [AS_Anno.Annoted AS_BASIC.FORMULA] -> Integer -> [NUM_FORM]
  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 :: [DIAG_FORM]
             -> NUM_FORM
             -> Sign.Sign
             -> [DIAG_FORM]
  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.True_atom _) = Sign.emptySig
  propsOfFormula (AS_BASIC.False_atom _) = 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
  
  -- Basic analysis for propositional logic
  basicPropositionalAnalysis
    :: (AS_BASIC.BASIC_SPEC, Sign.Sign, GlobalAnnos.GlobalAnnos)
    -> Result.Result (AS_BASIC.BASIC_SPEC,
                      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.SYMB_MAP_ITEMS]
                    -> 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.Symb_map_items sitem _ ->
                                         Map.union smap $ statSymbMapItem sitem
                             )
                             Map.empty
                             xs
      }
  
  statSymbMapItem :: [AS_BASIC.SYMB_OR_MAP]
                   -> 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.Symb_map s1 s2 _ ->
                 Map.insert (symbToSymbol s1) (symbToSymbol s2) mmap
      )
      Map.empty
  
  -- | Retrieve raw symbols
  mkStatSymbItems :: [AS_BASIC.SYMB_ITEMS] -> Result.Result [Symbol.Symbol]
  mkStatSymbItems a = Result.Result
                      {
                        Result.diags = []
                      , Result.maybeResult = Just $ statSymbItems a
                      }
  
  statSymbItems :: [AS_BASIC.SYMB_ITEMS] -> [Symbol.Symbol]
  statSymbItems = concatMap symbItemsToSymbol
  
  symbItemsToSymbol :: AS_BASIC.SYMB_ITEMS -> [Symbol.Symbol]
  symbItemsToSymbol (AS_BASIC.Symb_items syms _) = map symbToSymbol syms
  
  symbToSymbol :: AS_BASIC.SYMB -> Symbol.Symbol
  symbToSymbol (AS_BASIC.Symb_id tok) =
      Symbol.Symbol {Symbol.symName = Id.simpleIdToId tok}
  
  makePMap :: Map.Map Symbol.Symbol Symbol.Symbol -> Sign.Sign
    -> Map.Map Id.Id Id.Id
  makePMap imap sig = Set.fold ( \ x ->
    let symOf = Symbol.Symbol { Symbol.symName = x }
        y = Symbol.symName $ Symbol.applySymMap imap symOf
    in Map.insert x y ) Map.empty $ Sign.items sig
  
  -- | 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 = let pMap = makePMap imap sig in
                return
                Morphism.Morphism
                            { Morphism.source = sig
                            , Morphism.propMap = pMap
                            , Morphism.target = Sign.Sign
                              { Sign.items = Set.map (Morphism.applyMap pMap)
                                $ 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
                    pMap :: Map.Map Id.Id Id.Id
                    pMap = Set.fold ( \ x ->
                      let symOf = Symbol.Symbol { Symbol.symName = x }
                          y = Symbol.symName $ Symbol.applySymMap imap symOf
                      in Map.insert x y ) Map.empty sigItems
                    targetSig = Sign.Sign
                      { Sign.items = Set.map (Morphism.applyMap pMap)
                        $ Sign.items sig }
                    isSub = Sign.items targetSig `Set.isSubsetOf` Sign.items tSig
                in if isSub then return Morphism.Morphism
                       { Morphism.source = sig
                       , Morphism.propMap = makePMap imap sig
                       , Morphism.target = tSig
                       }
                       else Fail.fail "Incompatible mapping"
  
  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 (\ (x, y) -> (x, Morphism.propMap y)) 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)
  
  
  pROPsen_analysis :: (AS_BASIC.BASIC_SPEC, Sign.Sign, AS_BASIC.FORMULA)
    -> Result.Result AS_BASIC.FORMULA
  pROPsen_analysis (_, s, f) =
          let x = addFormula [] (NumForm annoF 0) s
              h = return . diagnosis . head
              g = Just . AS_Anno.sentence . formula . head
              annoF = AS_Anno.Annoted f Id.nullRange [] []
          in Result.Result (h x) (g x)
  