{- |
Module      :  $Header$
Description :  Definition of signature morphisms for
               first-order logic with dependent types (DFOL)
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable
-}

module DFOL.Morphism
   ( Morphism (..)
   , idMorph
   , compMorph
   , isValidMorph
   , canForm
   , applyMorph
   , mapSymbol
   , inclusionMorph
   , morphUnion
   , inducedFromMorphism
   , inducedFromToMorphism
   , coGenSig
   , toTermMap
   ) where

import DFOL.AS_DFOL
import DFOL.Sign
import DFOL.Symbol
import Common.Result
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.ExtSign
import qualified Common.Result as Result
import qualified Data.Map as Map
import qualified Data.Set as Set

-- morphisms for DFOL - maps of symbol names
data Morphism = Morphism
  { source :: Sign
  , target :: Sign
  , symMap :: Map.Map NAME NAME
  } deriving (Ord, Show)

-- constructs an identity morphism
idMorph :: Sign -> Morphism
idMorph sig = Morphism sig sig Map.empty

-- composes two morphisms
compMorph :: Morphism -> Morphism -> Result Morphism
compMorph m1 m2 =
  if target m1 /= source m2
     then Result.Result [incompatibleMorphsError m1 m2] Nothing
     else return $ Morphism (source m1) (target m2) $
                 Set.fold (\ sym1 -> let sym2 = mapSymbol m2
                                                  $ mapSymbol m1 sym1
                                         in Map.insert sym1 sym2)
                          Map.empty $
                          getSymbols $ source m1

-- determines whether a morphism is valid
isValidMorph :: Morphism -> Bool
isValidMorph m@(Morphism sig1 sig2 map1) =
  let sym1 = getSymbols sig1
      sym2 = getSymbols sig2
      checkDom = Set.isSubsetOf (Map.keysSet map1) sym1
      checkCod = Set.isSubsetOf (Set.map (mapSymbol m) sym1) sym2
      checkTypes = map (checkTypePres m) $ Set.toList sym1
      in and $ [checkDom, checkCod] ++ checkTypes

checkTypePres :: Morphism -> NAME -> Bool
checkTypePres m n =
  let Just type1 = getSymbolType n $ source m
      Just type2 = getSymbolType (mapSymbol m n) $ target m
      in applyMorph m type1 == type2

{- converts the morphism into its canonical form where the symbol map contains
   no key/value pairs of the form (k,k) -}
canForm :: Morphism -> Morphism
canForm (Morphism sig1 sig2 map1) =
  let map2 = Map.fromList $ filter (uncurry (/=)) $ Map.toList map1
      in Morphism sig1 sig2 map2

-- constructs the inclusion morphism between signatures
inclusionMorph :: Sign -> Sign -> Result.Result Morphism
inclusionMorph sig1 sig2 =
  let m = Morphism sig1 sig2 Map.empty
      in if isValidMorph m
            then Result.Result [] $ Just m
            else Result.Result [noSubsigError sig1 sig2] Nothing

{- generated and cogenerated signatures
Algorithm description:

FOR GENERATED SIGNATURES

Input : a signature "sig" and a set of symbols "syms"
Output : an inclusion morphism

1 : Check if all symbols in syms occur in sig; if not, output Nothing

2 : Initialize the set of symbols "incl" which necessarily must be included
    in the generated signature to syms
    Initialize the set "done" of analyzed symbols to empty
    Initialize the set "todo" of symbols to be analyzed to syms

3 : Check if todo is empty
    3.1 : If yes, go to 5
    3.2 : If not, go to 4

4 : Pick a symbol "s" from todo
    4.1 : Get the type "t" of s in sig
    4.2 : Get the set "vars" of free variables in t, i.e. the symbols of sig
          that t depends on
    4.3 : For each "v" in vars :
          4.3.1 : Add v to incl
          4.3.2 : If v does not occur in done, add it to todo
    4.4 : Remove v from todo and add it to done
    4.5 : Go to 3

5 : Let "sig1" be the subsignature of sig containing only the symbols in incl
    and output the inclusion morphism m : sig1 -> sig

FOR COGENERATED SIGNATURES

Input : a signature "sig" and a set of symbols "syms"
Output : an inclusion morphism

1 : Check if all symbols in syms occur in sig; if not, output Nothing

2 : Initialize the set of symbols "excl" which necessarily must be excluded
    from the cogenerated signature to syms

3 : For each symbol "s" in sig (keeping the order in which they are defined) :
    3.1 : If s does not occur in excl :
          4.1 : Get the type "t" of s in sig
          4.2 : Get the set "vars" of free variables in t, i.e. the symbols
                of sig that t depends on
          4.3 : If any of the symbols in vars occurs in excl, add s to excl

4 : Let "sig1" be the subsignature of sig containing all the symbols not
    occurring in excl and output the inclusion morphism m : sig1 -> sig
-}
coGenSig :: Bool -> Set.Set Symbol -> Sign -> Result Morphism
coGenSig flag syms sig@(Sign ds) =
  let names = Set.map name syms
      ds1 = expandDecls ds
      in if Set.isSubsetOf names (getSymbols sig)
            then let incl = if flag
                               then cogSig names ds1 sig
                               else genSig names Set.empty names sig
                     ds2 = map (\ (n, t) -> ([n], t))
                           $ filter (\ (n, _) -> Set.member n incl) ds1
                     in inclusionMorph (Sign ds2) sig
            else Result.Result [symsNotInSigError names sig] Nothing

genSig :: Set.Set NAME -> Set.Set NAME -> Set.Set NAME -> Sign -> Set.Set NAME
genSig incl done todo sig =
  if Set.null todo
     then incl
     else let n = Set.findMin todo
              Just t = getSymbolType n sig
              ns = getFreeVars t
              incl1 = Set.union incl ns
              ns1 = Set.filter (`Set.member` done) ns
              done1 = Set.insert n done
              todo1 = Set.union ns1 $ Set.delete n todo
              in genSig incl1 done1 todo1 sig

cogSig :: Set.Set NAME -> [SDECL] -> Sign -> Set.Set NAME
cogSig excl [] sig = Set.difference (getSymbols sig) excl
cogSig excl ((n, t) : ds) sig =
  if Set.member n excl
     then cogSig excl ds sig
     else let ns = Set.toList $ getFreeVars t
              depen = any (`Set.member` excl) ns
              in if depen
                    then let excl1 = Set.insert n excl
                             in cogSig excl1 ds sig
                    else cogSig excl ds sig

-- morphism union
morphUnion :: Morphism -> Morphism -> Result.Result Morphism
morphUnion m1@(Morphism sig1D sig1C map1) m2@(Morphism sig2D sig2C map2) =
  let Result.Result diag1 sigDM = sigUnion sig1D sig2D
      Result.Result diag2 sigCM = sigUnion sig1C sig2C
      Result.Result diag3 map3M = combineMaps map1 map2
      in case sigDM of
              Nothing -> Result.Result diag1 Nothing
              Just sigD ->
                case sigCM of
                     Nothing -> Result.Result diag2 Nothing
                     Just sigC ->
                       case map3M of
                            Nothing -> Result.Result diag3 Nothing
                            Just map3 ->
                              let m = Morphism sigD sigC map3
                                  in if isValidMorph m
                                     then Result.Result [] $ Just m
                                     else Result.Result
                                            [invalidMorphError m1 m2] Nothing

combineMaps :: Map.Map NAME NAME -> Map.Map NAME NAME ->
               Result.Result (Map.Map NAME NAME)
combineMaps map1 map2 = combineMapsH map1 $ Map.toList map2

combineMapsH :: Map.Map NAME NAME -> [(NAME, NAME)] ->
                Result.Result (Map.Map NAME NAME)
combineMapsH map1 [] = Result.Result [] $ Just map1
combineMapsH map1 ((k, v) : ds) =
  if Map.member k map1
     then let Just v1 = Map.lookup k map1
              in if v == v1
                 then combineMapsH map1 ds
                 else Result.Result [incompatibleMapError k v v1] Nothing
     else let map2 = Map.insert k v map1
          in combineMapsH map2 ds

-- applies a morphism to a symbol
mapSymbol :: Morphism -> NAME -> NAME
mapSymbol m sym = Map.findWithDefault sym sym $ symMap m

-- translates a term, type or formula along the given morphism
applyMorph :: Translatable a => Morphism -> a -> a
applyMorph m t =
  let syms = getSymbols (target m)
      map1 = toTermMap $ symMap m
      in translate map1 syms t

toTermMap :: Map.Map NAME NAME -> Map.Map NAME TERM
toTermMap m = Map.fromList $ map (\ (k, a) -> (k, Identifier a))
               $ Map.toList m

-- equality
instance Eq Morphism where
    m1 == m2 = eqMorph (canForm m1) (canForm m2)

eqMorph :: Morphism -> Morphism -> Bool
eqMorph (Morphism s1 t1 map1) (Morphism s2 t2 map2) =
  (s1, t1, map1) == (s2, t2, map2)

-- pretty printing
instance Pretty Morphism where
  pretty = printMorph

printMorph :: Morphism -> Doc
printMorph m =
  vcat $ if m == idMorph (source m)
     then [text "Identity morphism on:", pretty $ source m]
     else [text "Source signature:", pretty $ source m,
           text "Target signature:", pretty $ target m,
           text "Mapping:", printSymMap $ symMap m]

printSymMap :: Map.Map NAME NAME -> Doc
printSymMap m = vcat $ map (\ (k, a) -> pretty k <+> text "|->" <+> pretty a)
                     $ Map.toList m

-- induces a signature morphism from the source signature and a symbol map
inducedFromMorphism :: Map.Map Symbol Symbol -> Sign -> Result.Result Morphism
inducedFromMorphism map1 sig1 =
  let map2 = toNameMap map1
      Result.Result dgs sig2M = buildSig sig1 map2
      in case sig2M of
              Nothing -> Result.Result dgs Nothing
              Just sig2 -> Result.Result [] $ Just $ Morphism sig1 sig2 map2

buildSig :: Sign -> Map.Map NAME NAME -> Result.Result Sign
buildSig (Sign ds) = buildSigH (expandDecls ds) emptySig

buildSigH :: [SDECL] -> Sign -> Map.Map NAME NAME -> Result.Result Sign
buildSigH [] sig _ = Result.Result [] $ Just sig
buildSigH ((n1, t1) : ds) sig map1 =
  let n2 = Map.findWithDefault n1 n1 map1
      map2 = toTermMap map1
      syms = Set.map (\ n -> Map.findWithDefault n n map1)
                 $ getSymbols sig
      t2 = translate map2 syms t1
      in if isConstant n2 sig
            then let Just t3 = getSymbolType n2 sig
                 in if t2 == t3
                       then buildSigH ds sig map1
                       else Result.Result [incompatibleViewError1 n2 t2 t3]
                                          Nothing
            else buildSigH ds (addSymbolDecl ([n2], t2) sig) map1

-- induces a signature morphism from the source and target sigs and a symbol map
inducedFromToMorphism :: Map.Map Symbol Symbol -> ExtSign Sign Symbol ->
                         ExtSign Sign Symbol -> Result.Result Morphism
inducedFromToMorphism map1 (ExtSign sig1 _) (ExtSign sig2 _) =
  let map2 = toNameMap map1
      m = Morphism sig1 sig2 map2
      Sign ds = sig1
      in buildMorph (expandDecls ds) m

buildMorph :: [SDECL] -> Morphism -> Result.Result Morphism
buildMorph [] m = Result.Result [] $ Just m
buildMorph ((n1, t1) : ds) m@(Morphism _ sig2 map1) = do
  let t2 = applyMorph m t1
  if Map.member n1 map1
     then do
        let n2 = mapSymbol m n1
        let Just t3 = getSymbolType n2 sig2
        if t2 == t3 then buildMorph ds m else
           Result.Result [incompatibleViewError2 n2 t2 t3] Nothing
     else do
        let t3 = getSymbolType n1 sig2
        if Just t2 == t3 then buildMorph ds m else do
           let ss = getSymsOfType sig2 t2
           case ss of
                [s] -> buildMorph ds $
                          m {symMap = Map.insert n1 s $ symMap m}
                [] -> Result.Result [noSymToMapError n1 t2] Nothing
                _ -> Result.Result [manySymToMapError n1 t2 ss] Nothing

-- ERROR MESSAGES
incompatibleMorphsError :: Morphism -> Morphism -> Result.Diagnosis
incompatibleMorphsError m1 m2 =
  Result.Diag
    { Result.diagKind = Result.Error
    , Result.diagString = "Codomain of the morphism\n" ++ show (pretty m1)
                          ++ "\nis different from the domain of the morphism\n"
                          ++ show (pretty m2)
                          ++ "\nhence their composition cannot be constructed."
    , Result.diagPos = nullRange
    }

incompatibleViewError1 :: NAME -> TYPE -> TYPE -> Result.Diagnosis
incompatibleViewError1 n t1 t2 =
  Result.Diag
    { Result.diagKind = Result.Error
    , Result.diagString = "Symbol\n" ++ show (pretty n)
                          ++ "\nmust have both type\n" ++ show (pretty t1)
                          ++ "\nand type\n" ++ show (pretty t2)
                          ++ "\nin the target signature and hence "
                          ++ "the view is ill-formed."
    , Result.diagPos = nullRange
    }

incompatibleViewError2 :: NAME -> TYPE -> TYPE -> Result.Diagnosis
incompatibleViewError2 n t1 t2 =
  Result.Diag
    { Result.diagKind = Result.Error
    , Result.diagString = "Symbol\n" ++ show (pretty n)
                          ++ "\nmust have type\n" ++ show (pretty t1)
                          ++ "\nbut instead has type\n" ++ show (pretty t2)
                          ++ "\nin the target signature and hence "
                          ++ "the view is ill-formed."
    , Result.diagPos = nullRange
    }

noSymToMapError :: NAME -> TYPE -> Result.Diagnosis
noSymToMapError n t =
  Result.Diag
    { Result.diagKind = Result.Error
    , Result.diagString = "Symbol\n" ++ show (pretty n)
                          ++ "\ncannot be mapped to anything as the target "
                          ++ "signature contains no symbols of type\n"
                          ++ show (pretty t)
    , Result.diagPos = nullRange
    }

manySymToMapError :: NAME -> TYPE -> [NAME] -> Result.Diagnosis
manySymToMapError n t ss =
  Result.Diag
    { Result.diagKind = Result.Error
    , Result.diagString = "Symbol\n" ++ show (pretty n)
                          ++ "\ncannot be uniquely mapped as the target "
                          ++ "signature contains multiple symbols of type\n"
                          ++ show (pretty t) ++ "\n namely\n"
                          ++ show (printNames ss)
    , Result.diagPos = nullRange
    }

noSubsigError :: Sign -> Sign -> Result.Diagnosis
noSubsigError sig1 sig2 =
  Result.Diag
    { Result.diagKind = Result.Error
    , Result.diagString = "Signature\n" ++ show (pretty sig1)
                          ++ "\nis not a subsignature of\n"
                          ++ show (pretty sig2)
                          ++ "\nand hence the inclusion morphism "
                          ++ "cannot be constructed."
    , Result.diagPos = nullRange
    }

incompatibleMapError :: NAME -> NAME -> NAME -> Result.Diagnosis
incompatibleMapError n n1 n2 =
  Result.Diag
    { Result.diagKind = Result.Error
    , Result.diagString = "Symbol\n" ++ show (pretty n)
                          ++ "\nis mapped both to\n" ++ show (pretty n1)
                          ++ "\nand\n" ++ show (pretty n2)
                          ++ "\nin the target signature and hence "
                          ++ "the morphism union cannot be constructed."
    , Result.diagPos = nullRange
    }

invalidMorphError :: Morphism -> Morphism -> Result.Diagnosis
invalidMorphError m1 m2 =
  Result.Diag
    { Result.diagKind = Result.Error
    , Result.diagString = "The combination of morphisms\n" ++ show (pretty m1)
                          ++ "\nand\n" ++ show (pretty m2)
                          ++ "\nis not a valid morphism and hence "
                          ++ "their union cannot be constructed."
    , Result.diagPos = nullRange
    }

symsNotInSigError :: Set.Set NAME -> Sign -> Result.Diagnosis
symsNotInSigError syms sig =
  Result.Diag
    { Result.diagKind = Result.Error
    , Result.diagString = "The symbols\n"
                          ++ show (printNames $ Set.toList syms)
                          ++ "\nare not in the signature\n"
                          ++ show (pretty sig)
                          ++ "\nand hence the (co)generated signature "
                          ++ "cannot be constructed."
    , Result.diagPos = nullRange
    }
