module LF.ComorphFram 
   ( mapTheory
   , mapMorphism
   , mapSen
   , mapSymb
   ) where

import LF.Morphism
import LF.Sign

import Common.Result
import Common.DocUtils
import Common.AS_Annotation

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

mapTheory :: Morphism -> (Sign, [Named EXP]) -> Result (Sign, [Named EXP])
mapTheory mor (s1, ne) = 
  let s2 = mapSign mor s1
      ne2 = map (mapNamedSent mor) ne
  in return (s2, ne2)
      
mapNamedSent :: Morphism -> Named EXP -> Named EXP
mapNamedSent mor ne = ne {sentence = mapSent mor $ sentence ne}

mapMorphism :: Morphism -> Morphism -> Result Morphism
mapMorphism mor m1 =
  let s1 = source m1
      t1 = target m1
      t2 = mapSign mor t1
      defs1 = filter (\ (Def _ _ v) -> v == Nothing) $ getDefs s1
      (defs2, m2) = makeSigMap ([], Map.empty) $ map (mapMorphH mor) (mkPairs defs1 $ symMap m1)
      s2 = Sign gen_base gen_module defs2
  in return $ Morphism gen_base gen_module gen_morph s2 t2 Unknown m2

mapMorphH :: Morphism -> (DEF, EXP) -> (DEF, Maybe EXP)
mapMorphH mor ((Def sym stp _) , e) =
  case mapSymbH mor sym stp of
       Right sym2 -> let stp2 = mapSent mor stp
                         e2 = mapSent mor e
                         sval2 = takeSymValue sym2 $ getDefs $ target mor 
                     in case sval2 of
                             Nothing -> ((Def sym2 stp2 Nothing), Just e2)
                             _ -> ((Def sym2 stp2 sval2), Nothing)
       Left err -> error $ show err

mkPairs :: [DEF] -> Map.Map Symbol EXP -> [(DEF, EXP)]
mkPairs defs m = case defs of
   [] -> []
   (Def s t v) : ds -> case Map.lookup s m of
                                  Just e -> ((Def s t v), e) : mkPairs ds m
                                  Nothing -> error $ "mkPairs : " ++
--                                                         "The symbol "
                                                        (show $ pretty s) ++
                                                        " is not in the map.\n"

makeSigMap :: ([DEF], Map.Map Symbol EXP) -> [(DEF, Maybe EXP)] 
               -> ([DEF], Map.Map Symbol EXP)
makeSigMap dms defs = case defs of
   [] -> dms
   ((Def s t v), e) : des -> let (ds, m) = dms 
                             in case e of
                                     Just e' -> makeSigMap ((Def s t v) : ds, Map.insert s e' m) des 
                                     Nothing -> makeSigMap ((Def s t v) : ds, m) des
  
  





mapSign :: Morphism -> Sign -> Sign
mapSign mor sig =
  let ds = filter (\ (Def _ _ v) -> v == Nothing) $ getDefs sig
      defs = mapDefs mor ds
  in (Sign gen_base gen_module defs)

mapDefs :: Morphism -> [DEF] -> [DEF]
mapDefs mor defs = case defs of
  [] -> []
  (Def s t _) : ds -> case mapSymbH mor s t of
                           Right s2 -> let t2 = mapSent mor t
                                           sval = takeSymValue s2 $ getDefs $ target mor
                                       in (Def s2 t2 sval) : (mapDefs mor ds)
                           Left err -> error $ show err
      
takeSymValue :: Symbol -> [DEF] -> Maybe EXP
takeSymValue sym defs = case defs of
   [] -> Nothing
   (Def sym2 _ val) : ds -> if (sym == sym2) 
                              then val
                              else takeSymValue sym ds




mapSymb :: Morphism -> Sign -> Symbol -> Set.Set Symbol
mapSymb mor sig sym = Set.singleton $ mapSymb' mor sig sym

mapSymb' :: Morphism -> Sign -> Symbol -> Symbol 
mapSymb' mor sig sym =
   let symType = getSymType sym sig
   in case symType of
           Just symT -> case mapSymbH mor sym symT of
                             Right s -> s
                             Left err -> error $ "mapSymb' : " ++ (show err)
           Nothing -> error $ "mapSymb' : The symbol " ++ 
                              (show $ pretty sym) ++
                              " is not in the signature.\n"

mapSymbH :: Morphism -> Symbol -> EXP -> Either String Symbol
mapSymbH mor sym symType' = 
   let sig2 = target mor
       symType = mapSent mor symType'
   in if ((Just symType) == (getSymType sym sig2))
         then Right sym
         else let syms = getSymsOfType symType sig2
              in case Set.toList syms of
                      [s'] -> Right s'
                      [] -> Left $ noSymError sym symType
                      _ -> let locals = getLocalSyms sig2
                               inter = Set.intersection syms locals
                           in case Set.toList inter of
                                   [s'] -> Right s'
                                   [] -> Left $ noSymError sym symType
                                   _ -> Left $ manySymError sym symType


mapSen :: Morphism -> EXP -> Result EXP
mapSen mor ex = return $ mapSent mor ex

mapSent :: Morphism -> EXP -> EXP
mapSent m e = 
  let re = translate m e
  in  case re of
           Just ex -> ex
           Nothing -> error $ "The sentence morphism" ++
                             "could not be performed.\n"

{-           
-- mapSent synM lmod_target lmod_source modM e
mapSent :: Morphism -> Morphism -> Morphism -> Morphism -> EXP -> Result EXP
mapSent synM lmodTarget lmodSource modM e = 
  let route1 = compMorph synM lmodTarget
      route2 = compMorph lmodSource modM
      em1 = translate route1 e
      em2 = translate route2 e
      if (em1 == em2)
         then let re = translate synM e
              in  case re of 
                       Nothing -> fail $ "The sentence morphism" ++
                                         "could not be performed.\n"
                       Just ex -> ex
         else fail $ 
-}  


-- ERROR MESSAGES
noSymError :: Symbol -> EXP -> String
noSymError s t = "Symbol " ++ (show $ pretty s) ++
   " cannot be mapped to anything as the target signature contains" ++
   " no symbols of type/kind " ++ (show $ pretty t) ++ "."

manySymError :: Symbol -> EXP -> String
manySymError s t = "Symbol " ++ (show $ pretty s) ++
   " cannot be mapped to anything as the target signature contains" ++
   " more than one symbol of type/kind " ++ (show $ pretty t) ++ "."
