{- |
Module      :  $Header$
Description :  Morphism of Common Logic
Copyright   :  (c) Uni Bremen DFKI 2010
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  eugenk@informatik.uni-bremen.de
Stability   :  experimental
Portability :  non-portable (via Logic.Logic)

Morphism of Common Logic

-}

module CommonLogic.Morphism
  ( Morphism (..)
  , pretty                      -- pretty printing
  , idMor                       -- identity morphism
  , isLegalMorphism             -- check if morhpism is ok
  , composeMor                  -- composition
  , inclusionMap                -- inclusion map
  , mkMorphism                  -- create Morphism
  , mapSentence                 -- map of sentences
  , applyMap                    -- application function for maps
  , applyMorphism               -- application function for morphism
  , morphismUnion
  ) where

import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Result as Result
import Common.Id as Id
import Common.Result
import Common.Doc
import Common.DocUtils

import CommonLogic.AS_CommonLogic as AS
import CommonLogic.Sign as Sign

-- maps of sets
data Morphism = Morphism
  { source :: Sign
  , target :: Sign
  , propMap :: Map.Map Id Id
  } deriving (Eq, Ord, Show)

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 = allItems $ source pmor
        ptarget = allItems $ target pmor
        pdom = Map.keysSet $ propMap pmor
        pcodom = Set.map (applyMorphism pmor) psource
    in if Set.isSubsetOf pcodom ptarget && Set.isSubsetOf pdom psource
    then return () else fail "illegal CommonLogic 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 $ allItems 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 }

-- | creates a Morphism
mkMorphism :: Sign.Sign -> Sign.Sign -> Map.Map Id Id -> Morphism
mkMorphism s t p =
  Morphism { source = s
           , target = t
           , propMap = p }

-- | sentence (text) translation along signature morphism
-- here just the renaming of formulae
mapSentence :: Morphism -> AS.TEXT_META -> Result.Result AS.TEXT_META
mapSentence mor tm =
  return $ tm { getText = mapSen_txt mor $ getText tm }

-- propagates the translation to sentences
mapSen_txt :: Morphism -> AS.TEXT -> AS.TEXT
mapSen_txt mor txt = case txt of
  AS.Text phrs r -> AS.Text (map (mapSen_phr mor) phrs) r
  AS.Named_text n t r -> AS.Named_text n (mapSen_txt mor t) r

-- propagates the translation to sentences
mapSen_phr :: Morphism -> AS.PHRASE -> AS.PHRASE
mapSen_phr mor phr = case phr of
  AS.Module m -> AS.Module $ mapSen_mod mor m
  AS.Sentence s -> AS.Sentence $ mapSen_sen mor s
  AS.Comment_text c t r -> AS.Comment_text c (mapSen_txt mor t) r
  x -> x

-- propagates the translation to sentences
mapSen_mod :: Morphism -> AS.MODULE -> AS.MODULE
mapSen_mod mor m = case m of
  AS.Mod n t rn -> AS.Mod n (mapSen_txt mor t) rn
  AS.Mod_ex n exs t rn -> AS.Mod_ex n exs (mapSen_txt mor t) rn

mapSen_sen :: Morphism -> AS.SENTENCE -> AS.SENTENCE
mapSen_sen mor frm = case frm of
  AS.Quant_sent qs rn -> AS.Quant_sent (case qs of
      AS.Universal xs sen ->
          AS.Universal (map (mapSen_nos mor) xs) (mapSen_sen mor sen)
      AS.Existential xs sen ->
          AS.Existential (map (mapSen_nos mor) xs) (mapSen_sen mor sen)
      ) rn
  AS.Bool_sent bs rn -> AS.Bool_sent (case bs of
      AS.Conjunction sens ->  AS.Conjunction (map (mapSen_sen mor) sens)
      AS.Disjunction sens -> AS.Disjunction (map (mapSen_sen mor) sens)
      AS.Negation sen -> AS.Negation (mapSen_sen mor sen)
      AS.Implication s1 s2 ->
          AS.Implication (mapSen_sen mor s1) (mapSen_sen mor s2)
      AS.Biconditional s1 s2 ->
          AS.Biconditional (mapSen_sen mor s1) (mapSen_sen mor s2)
    ) rn
  AS.Atom_sent atom rn -> AS.Atom_sent (case atom of
      AS.Equation t1 t2 -> AS.Equation (mapSen_trm mor t1) (mapSen_trm mor t2)
      AS.Atom t tss -> AS.Atom (mapSen_trm mor t) (map (mapSen_trmSeq mor) tss)
    ) rn
  AS.Comment_sent cm sen rn -> AS.Comment_sent cm (mapSen_sen mor sen) rn
  AS.Irregular_sent sen rn -> AS.Irregular_sent (mapSen_sen mor sen) rn

mapSen_trm :: Morphism -> AS.TERM -> AS.TERM
mapSen_trm mor trm = case trm of
  AS.Name_term n -> AS.Name_term (mapSen_tok mor n)
  AS.Funct_term t ts rn ->
      AS.Funct_term (mapSen_trm mor t) (map (mapSen_trmSeq mor) ts) rn
  AS.Comment_term t c rn -> AS.Comment_term (mapSen_trm mor t) c rn

mapSen_nos :: Morphism -> AS.NAME_OR_SEQMARK -> AS.NAME_OR_SEQMARK
mapSen_nos mor nos = case nos of
  AS.Name n -> AS.Name (mapSen_tok mor n)
  AS.SeqMark s -> AS.SeqMark (mapSen_tok mor s)

mapSen_trmSeq :: Morphism -> AS.TERM_SEQ -> AS.TERM_SEQ
mapSen_trmSeq mor ts = case ts of
  AS.Term_seq t -> AS.Term_seq (mapSen_trm mor t)
  AS.Seq_marks s -> AS.Seq_marks (mapSen_tok mor s)

mapSen_tok :: Morphism -> Id.Token -> Id.Token
mapSen_tok mor tok = Id.idToSimpleId $ applyMorphism mor $ Id.simpleIdToId tok

-- | Union of two morphisms.
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 (allItems p1) $ Map.keysSet pmap1
      up2 = Set.difference (allItems 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
