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 :: Morphism -> (Sign, [Named EXP]) -> Result (Sign, [Named EXP])
mapTheory mor :: Morphism
mor (s1 :: Sign
s1, ne :: [Named EXP]
ne) =
  let s2 :: Sign
s2 = Morphism -> Sign -> Sign
mapSign Morphism
mor Sign
s1
      ne2 :: [Named EXP]
ne2 = (Named EXP -> Named EXP) -> [Named EXP] -> [Named EXP]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism -> Named EXP -> Named EXP
mapNamedSent Morphism
mor) [Named EXP]
ne
  in (Sign, [Named EXP]) -> Result (Sign, [Named EXP])
forall (m :: * -> *) a. Monad m => a -> m a
return (Sign
s2, [Named EXP]
ne2)

mapNamedSent :: Morphism -> Named EXP -> Named EXP
mapNamedSent :: Morphism -> Named EXP -> Named EXP
mapNamedSent mor :: Morphism
mor ne :: Named EXP
ne = Named EXP
ne {sentence :: EXP
sentence = Morphism -> EXP -> EXP
mapSent Morphism
mor (EXP -> EXP) -> EXP -> EXP
forall a b. (a -> b) -> a -> b
$ Named EXP -> EXP
forall s a. SenAttr s a -> s
sentence Named EXP
ne}

mapMorphism :: Morphism -> Morphism -> Result Morphism
mapMorphism :: Morphism -> Morphism -> Result Morphism
mapMorphism mor :: Morphism
mor m1 :: Morphism
m1 =
  let s1 :: Sign
s1 = Morphism -> Sign
source Morphism
m1
      t1 :: Sign
t1 = Morphism -> Sign
target Morphism
m1
      t2 :: Sign
t2 = Morphism -> Sign -> Sign
mapSign Morphism
mor Sign
t1
      defs1 :: [DEF]
defs1 = (DEF -> Bool) -> [DEF] -> [DEF]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Def _ _ v :: Maybe EXP
v) -> Maybe EXP -> Bool
forall a. Maybe a -> Bool
isNothing Maybe EXP
v) ([DEF] -> [DEF]) -> [DEF] -> [DEF]
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
s1
      (defs2 :: [DEF]
defs2, m2 :: Map Symbol EXP
m2) = ([DEF], Map Symbol EXP)
-> [(DEF, Maybe EXP)] -> ([DEF], Map Symbol EXP)
makeSigMap ([], Map Symbol EXP
forall k a. Map k a
Map.empty) ([(DEF, Maybe EXP)] -> ([DEF], Map Symbol EXP))
-> [(DEF, Maybe EXP)] -> ([DEF], Map Symbol EXP)
forall a b. (a -> b) -> a -> b
$ ((DEF, EXP) -> (DEF, Maybe EXP))
-> [(DEF, EXP)] -> [(DEF, Maybe EXP)]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism -> (DEF, EXP) -> (DEF, Maybe EXP)
mapMorphH Morphism
mor)
                      ([DEF] -> Map Symbol EXP -> [(DEF, EXP)]
mkPairs [DEF]
defs1 (Map Symbol EXP -> [(DEF, EXP)]) -> Map Symbol EXP -> [(DEF, EXP)]
forall a b. (a -> b) -> a -> b
$ Morphism -> Map Symbol EXP
symMap Morphism
m1)
      s2 :: Sign
s2 = BASE -> BASE -> [DEF] -> Sign
Sign BASE
gen_base BASE
gen_module [DEF]
defs2
  in Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ BASE
-> BASE
-> BASE
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism BASE
gen_base BASE
gen_module BASE
gen_morph Sign
s2 Sign
t2 MorphType
Unknown Map Symbol EXP
m2

mapMorphH :: Morphism -> (DEF, EXP) -> (DEF, Maybe EXP)
mapMorphH :: Morphism -> (DEF, EXP) -> (DEF, Maybe EXP)
mapMorphH mor :: Morphism
mor (Def sym :: Symbol
sym stp :: EXP
stp _ , e :: EXP
e) =
  case Morphism -> Symbol -> EXP -> Either BASE Symbol
mapSymbH Morphism
mor Symbol
sym EXP
stp of
       Right sym2 :: Symbol
sym2 -> let stp2 :: EXP
stp2 = Morphism -> EXP -> EXP
mapSent Morphism
mor EXP
stp
                         e2 :: EXP
e2 = Morphism -> EXP -> EXP
mapSent Morphism
mor EXP
e
                         sval2 :: Maybe EXP
sval2 = Symbol -> [DEF] -> Maybe EXP
takeSymValue Symbol
sym2 ([DEF] -> Maybe EXP) -> [DEF] -> Maybe EXP
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs (Sign -> [DEF]) -> Sign -> [DEF]
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
mor
                     in case Maybe EXP
sval2 of
                             Nothing -> (Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
sym2 EXP
stp2 Maybe EXP
forall a. Maybe a
Nothing, EXP -> Maybe EXP
forall a. a -> Maybe a
Just EXP
e2)
                             _ -> (Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
sym2 EXP
stp2 Maybe EXP
sval2, Maybe EXP
forall a. Maybe a
Nothing)
       Left err :: BASE
err -> BASE -> (DEF, Maybe EXP)
forall a. HasCallStack => BASE -> a
error (BASE -> (DEF, Maybe EXP)) -> BASE -> (DEF, Maybe EXP)
forall a b. (a -> b) -> a -> b
$ BASE -> BASE
forall a. Show a => a -> BASE
show BASE
err

mkPairs :: [DEF] -> Map.Map Symbol EXP -> [(DEF, EXP)]
mkPairs :: [DEF] -> Map Symbol EXP -> [(DEF, EXP)]
mkPairs defs :: [DEF]
defs m :: Map Symbol EXP
m = case [DEF]
defs of
   [] -> []
   Def s :: Symbol
s t :: EXP
t v :: Maybe EXP
v : ds :: [DEF]
ds -> case Symbol -> Map Symbol EXP -> Maybe EXP
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
s Map Symbol EXP
m of
                                  Just e :: EXP
e -> (Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
s EXP
t Maybe EXP
v, EXP
e) (DEF, EXP) -> [(DEF, EXP)] -> [(DEF, EXP)]
forall a. a -> [a] -> [a]
: [DEF] -> Map Symbol EXP -> [(DEF, EXP)]
mkPairs [DEF]
ds Map Symbol EXP
m
                                  Nothing -> BASE -> [(DEF, EXP)]
forall a. HasCallStack => BASE -> a
error (BASE -> [(DEF, EXP)]) -> BASE -> [(DEF, EXP)]
forall a b. (a -> b) -> a -> b
$ "mkPairs : " BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++
-- "The symbol "
                                                        Doc -> BASE
forall a. Show a => a -> BASE
show (Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s) BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++
                                                        " is not in the map.\n"

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


mapSign :: Morphism -> Sign -> Sign
mapSign :: Morphism -> Sign -> Sign
mapSign mor :: Morphism
mor sig :: Sign
sig =
  let ds :: [DEF]
ds = (DEF -> Bool) -> [DEF] -> [DEF]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (Def _ _ v :: Maybe EXP
v) -> Maybe EXP -> Bool
forall a. Maybe a -> Bool
isNothing Maybe EXP
v) ([DEF] -> [DEF]) -> [DEF] -> [DEF]
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs Sign
sig
      defs :: [DEF]
defs = Morphism -> [DEF] -> [DEF]
mapDefs Morphism
mor [DEF]
ds
  in BASE -> BASE -> [DEF] -> Sign
Sign BASE
gen_base BASE
gen_module [DEF]
defs

mapDefs :: Morphism -> [DEF] -> [DEF]
mapDefs :: Morphism -> [DEF] -> [DEF]
mapDefs mor :: Morphism
mor defs :: [DEF]
defs = case [DEF]
defs of
  [] -> []
  Def s :: Symbol
s t :: EXP
t _ : ds :: [DEF]
ds -> case Morphism -> Symbol -> EXP -> Either BASE Symbol
mapSymbH Morphism
mor Symbol
s EXP
t of
                  Right s2 :: Symbol
s2 -> let t2 :: EXP
t2 = Morphism -> EXP -> EXP
mapSent Morphism
mor EXP
t
                                  sval :: Maybe EXP
sval = Symbol -> [DEF] -> Maybe EXP
takeSymValue Symbol
s2 ([DEF] -> Maybe EXP) -> [DEF] -> Maybe EXP
forall a b. (a -> b) -> a -> b
$ Sign -> [DEF]
getDefs (Sign -> [DEF]) -> Sign -> [DEF]
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
mor
                              in Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
s2 EXP
t2 Maybe EXP
sval DEF -> [DEF] -> [DEF]
forall a. a -> [a] -> [a]
: Morphism -> [DEF] -> [DEF]
mapDefs Morphism
mor [DEF]
ds
                  Left err :: BASE
err -> BASE -> [DEF]
forall a. HasCallStack => BASE -> a
error (BASE -> [DEF]) -> BASE -> [DEF]
forall a b. (a -> b) -> a -> b
$ BASE -> BASE
forall a. Show a => a -> BASE
show BASE
err

takeSymValue :: Symbol -> [DEF] -> Maybe EXP
takeSymValue :: Symbol -> [DEF] -> Maybe EXP
takeSymValue sym :: Symbol
sym defs :: [DEF]
defs = case [DEF]
defs of
   [] -> Maybe EXP
forall a. Maybe a
Nothing
   Def sym2 :: Symbol
sym2 _ val :: Maybe EXP
val : ds :: [DEF]
ds -> if Symbol
sym Symbol -> Symbol -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol
sym2
                              then Maybe EXP
val
                              else Symbol -> [DEF] -> Maybe EXP
takeSymValue Symbol
sym [DEF]
ds


mapSymb :: Morphism -> Sign -> Symbol -> Set.Set Symbol
mapSymb :: Morphism -> Sign -> Symbol -> Set Symbol
mapSymb mor :: Morphism
mor sig :: Sign
sig sym :: Symbol
sym = Symbol -> Set Symbol
forall a. a -> Set a
Set.singleton (Symbol -> Set Symbol) -> Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign -> Symbol -> Symbol
mapSymb' Morphism
mor Sign
sig Symbol
sym

mapSymb' :: Morphism -> Sign -> Symbol -> Symbol
mapSymb' :: Morphism -> Sign -> Symbol -> Symbol
mapSymb' mor :: Morphism
mor sig :: Sign
sig sym :: Symbol
sym =
   let symType :: Maybe EXP
symType = Symbol -> Sign -> Maybe EXP
getSymType Symbol
sym Sign
sig
   in case Maybe EXP
symType of
           Just symT :: EXP
symT -> case Morphism -> Symbol -> EXP -> Either BASE Symbol
mapSymbH Morphism
mor Symbol
sym EXP
symT of
                             Right s :: Symbol
s -> Symbol
s
                             Left err :: BASE
err -> BASE -> Symbol
forall a. HasCallStack => BASE -> a
error (BASE -> Symbol) -> BASE -> Symbol
forall a b. (a -> b) -> a -> b
$ "mapSymb' : " BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ BASE -> BASE
forall a. Show a => a -> BASE
show BASE
err
           Nothing -> BASE -> Symbol
forall a. HasCallStack => BASE -> a
error (BASE -> Symbol) -> BASE -> Symbol
forall a b. (a -> b) -> a -> b
$ "mapSymb' : The symbol " BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++
                              Doc -> BASE
forall a. Show a => a -> BASE
show (Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
sym) BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++
                              " is not in the signature.\n"

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


mapSen :: Morphism -> EXP -> Result EXP
mapSen :: Morphism -> EXP -> Result EXP
mapSen mor :: Morphism
mor ex :: EXP
ex = EXP -> Result EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> Result EXP) -> EXP -> Result EXP
forall a b. (a -> b) -> a -> b
$ Morphism -> EXP -> EXP
mapSent Morphism
mor EXP
ex

mapSent :: Morphism -> EXP -> EXP
mapSent :: Morphism -> EXP -> EXP
mapSent m :: Morphism
m e :: EXP
e =
  let re :: Maybe EXP
re = Morphism -> EXP -> Maybe EXP
translate Morphism
m EXP
e
  in EXP -> Maybe EXP -> EXP
forall a. a -> Maybe a -> a
fromMaybe (BASE -> EXP
forall a. HasCallStack => BASE -> a
error (BASE -> EXP) -> BASE -> EXP
forall a b. (a -> b) -> a -> b
$ "The sentence morphism" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++
                        "could not be performed.\n") Maybe EXP
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 :: Symbol -> EXP -> BASE
noSymError s :: Symbol
s t :: EXP
t = "Symbol " BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ Doc -> BASE
forall a. Show a => a -> BASE
show (Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s) BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++
   " cannot be mapped to anything as the target signature contains" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++
   " no symbols of type/kind " BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ Doc -> BASE
forall a. Show a => a -> BASE
show (EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
t) BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "."

manySymError :: Symbol -> EXP -> String
manySymError :: Symbol -> EXP -> BASE
manySymError s :: Symbol
s t :: EXP
t = "Symbol " BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ Doc -> BASE
forall a. Show a => a -> BASE
show (Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s) BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++
   " cannot be mapped to anything as the target signature contains" BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++
   " more than one symbol of type/kind " BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ Doc -> BASE
forall a. Show a => a -> BASE
show (EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
t) BASE -> BASE -> BASE
forall a. [a] -> [a] -> [a]
++ "."