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

import Data.Maybe (fromMaybe, isNothing)

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) -> isNothing v) $ 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) -> isNothing v) $ 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 fromMaybe (error $ "The sentence morphism" ++

"could not be performed.\n") re

{-

-- 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) ++ "."