{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  $Header$
Description :  Morphisms in 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

Definition of morphisms for propositional logic
copied to "Temporal.Morphism"
  Ref.

  Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
  What is a Logic?.
  In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-133. Birkhaeuser.
  2005.
-}

module QBF.Morphism
  ( Morphism (..)               -- datatype for Morphisms
  , pretty                      -- pretty printing
  , idMor                       -- identity morphism
  , isLegalMorphism             -- check if morhpism is ok
  , composeMor                  -- composition
  , inclusionMap                -- inclusion map
  , mapSentence                 -- map of sentences
  , mapSentenceH                -- map of sentences, without Result type
  , applyMap                    -- application function for maps
  , applyMorphism               -- application function for morphism
  , morphismUnion
  ) where

import Data.Data
import qualified Data.Map as Map
import qualified Data.Set as Set

import Propositional.Sign as Sign

import qualified QBF.AS_BASIC_QBF as AS_BASIC

import Common.Id as Id
import Common.Result
import Common.Doc
import Common.DocUtils
import qualified Common.Result as Result

import Control.Monad (unless)

{- | The datatype for morphisms in propositional logic as
maps of sets -}
data Morphism = Morphism
  { source :: Sign
  , target :: Sign
  , propMap :: Map.Map Id Id
  } deriving (Show, Eq, Ord, Typeable, Data)

instance Pretty Morphism where
    pretty = printMorphism

-- | Constructs an id-morphism
idMor :: Sign -> Morphism
idMor a = inclusionMap a a

-- | Determines whether a morphism is valid
isLegalMorphism :: Morphism -> Result ()
isLegalMorphism pmor =
    let psource = items $ source pmor
        ptarget = items $ target pmor
        pdom = Map.keysSet $ propMap pmor
        pcodom = Set.map (applyMorphism pmor) psource
    in unless (Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource)
        $ fail "illegal QBF morphism"

-- | Application funtion for morphisms
applyMorphism :: Morphism -> Id -> Id
applyMorphism mor idt = Map.findWithDefault idt idt $ propMap mor

-- | Application function for propMaps
applyMap :: Map.Map Id Id -> Id -> Id
applyMap pmap idt = Map.findWithDefault idt idt pmap

-- | Composition of morphisms in propositional Logic
composeMor :: Morphism -> Morphism -> Result Morphism
composeMor f g =
  let fSource = source f
      gTarget = target g
      fMap = propMap f
      gMap = propMap g
  in return Morphism
  { source = fSource
  , target = gTarget
  , propMap = if Map.null gMap then fMap else
      Set.fold ( \ i -> let j = applyMap gMap (applyMap fMap i) in
                        if i == j then id else Map.insert i j)
                                  Map.empty $ items fSource }

-- | Pretty printing for Morphisms
printMorphism :: Morphism -> Doc
printMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
  <> vcat (map ( \ (x, y) -> lparen <> pretty x <> text ","
  <> pretty y <> rparen) $ Map.assocs $ propMap m)

-- | Inclusion map of a subsig into a supersig
inclusionMap :: Sign.Sign -> Sign.Sign -> Morphism
inclusionMap s1 s2 = Morphism
  { source = s1
  , target = s2
  , propMap = Map.empty }

{- | sentence translation along signature morphism
here just the renaming of formulae -}
mapSentence :: Morphism -> AS_BASIC.FORMULA -> Result.Result AS_BASIC.FORMULA
mapSentence mor = return . mapSentenceH mor

mapSentenceH :: Morphism -> AS_BASIC.FORMULA -> AS_BASIC.FORMULA
mapSentenceH mor frm = case frm of
  AS_BASIC.Negation form rn -> AS_BASIC.Negation (mapSentenceH mor form) rn
  AS_BASIC.Conjunction form rn ->
      AS_BASIC.Conjunction (map (mapSentenceH mor) form) rn
  AS_BASIC.Disjunction form rn ->
      AS_BASIC.Disjunction (map (mapSentenceH mor) form) rn
  AS_BASIC.Implication form1 form2 rn -> AS_BASIC.Implication
      (mapSentenceH mor form1) (mapSentenceH mor form2) rn
  AS_BASIC.Equivalence form1 form2 rn -> AS_BASIC.Equivalence
      (mapSentenceH mor form1) (mapSentenceH mor form2) rn
  AS_BASIC.TrueAtom rn -> AS_BASIC.TrueAtom rn
  AS_BASIC.FalseAtom rn -> AS_BASIC.FalseAtom rn
  AS_BASIC.Predication predH -> AS_BASIC.Predication
      $ id2SimpleId $ applyMorphism mor $ Id.simpleIdToId predH
  AS_BASIC.ForAll xs form rn -> AS_BASIC.ForAll (map
    (id2SimpleId . applyMorphism mor . Id.simpleIdToId) xs)
    (mapSentenceH mor form) rn
  AS_BASIC.Exists xs form rn -> AS_BASIC.Exists
    (map (id2SimpleId . applyMorphism mor . Id.simpleIdToId) xs)
    (mapSentenceH mor form) rn

morphismUnion :: Morphism -> Morphism -> Result.Result Morphism
morphismUnion mor1 mor2 =
  let pmap1 = propMap mor1
      pmap2 = propMap mor2
      p1 = source mor1
      p2 = source mor2
      up1 = Set.difference (items p1) $ Map.keysSet pmap1
      up2 = Set.difference (items p2) $ Map.keysSet pmap2
      (pds, pmap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of
          Nothing -> (ds, Map.insert i j m)
          Just k -> if j == k then (ds, m) else
              (Diag Error
               ("incompatible mapping of prop " ++ showId i " to "
                ++ showId j " and " ++ showId k "")
               nullRange : ds, m)) ([], pmap1)
          (Map.toList pmap2 ++ map (\ a -> (a, a))
                      (Set.toList $ Set.union up1 up2))
   in if null pds then return Morphism
      { source = unite p1 p2
      , target = unite (target mor1) $ target mor2
      , propMap = pmap } else Result pds Nothing
