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