{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./LF/Morphism.hs
Description :  Definition of signature morphisms for the Edinburgh
               Logical Framework
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 LF.Morphism
   ( MorphType (..)
   , Morphism (..)
   , idMorph
   , compMorph
   , mapSymbol
   , translate
   , canForm
   , inclusionMorph
   , inducedFromToMorphism
   , inducedFromMorphism
   , gen_morph
   ) where

import LF.Sign

import Common.Result
import Common.Doc hiding (space)
import Common.DocUtils
import qualified Control.Monad.Fail as Fail

import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Data
import Data.Maybe (isNothing, fromMaybe)

gen_morph :: String
gen_morph :: String
gen_morph = "GEN_MORPH"

data MorphType = Definitional | Postulated | Unknown
  deriving (Eq MorphType
Eq MorphType =>
(MorphType -> MorphType -> Ordering)
-> (MorphType -> MorphType -> Bool)
-> (MorphType -> MorphType -> Bool)
-> (MorphType -> MorphType -> Bool)
-> (MorphType -> MorphType -> Bool)
-> (MorphType -> MorphType -> MorphType)
-> (MorphType -> MorphType -> MorphType)
-> Ord MorphType
MorphType -> MorphType -> Bool
MorphType -> MorphType -> Ordering
MorphType -> MorphType -> MorphType
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: MorphType -> MorphType -> MorphType
$cmin :: MorphType -> MorphType -> MorphType
max :: MorphType -> MorphType -> MorphType
$cmax :: MorphType -> MorphType -> MorphType
>= :: MorphType -> MorphType -> Bool
$c>= :: MorphType -> MorphType -> Bool
> :: MorphType -> MorphType -> Bool
$c> :: MorphType -> MorphType -> Bool
<= :: MorphType -> MorphType -> Bool
$c<= :: MorphType -> MorphType -> Bool
< :: MorphType -> MorphType -> Bool
$c< :: MorphType -> MorphType -> Bool
compare :: MorphType -> MorphType -> Ordering
$ccompare :: MorphType -> MorphType -> Ordering
$cp1Ord :: Eq MorphType
Ord, MorphType -> MorphType -> Bool
(MorphType -> MorphType -> Bool)
-> (MorphType -> MorphType -> Bool) -> Eq MorphType
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: MorphType -> MorphType -> Bool
$c/= :: MorphType -> MorphType -> Bool
== :: MorphType -> MorphType -> Bool
$c== :: MorphType -> MorphType -> Bool
Eq, Int -> MorphType -> ShowS
[MorphType] -> ShowS
MorphType -> String
(Int -> MorphType -> ShowS)
-> (MorphType -> String)
-> ([MorphType] -> ShowS)
-> Show MorphType
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [MorphType] -> ShowS
$cshowList :: [MorphType] -> ShowS
show :: MorphType -> String
$cshow :: MorphType -> String
showsPrec :: Int -> MorphType -> ShowS
$cshowsPrec :: Int -> MorphType -> ShowS
Show, Typeable)

-- LF morphism cannot map defined symbols, only declared ones
data Morphism = Morphism
  { Morphism -> String
morphBase :: BASE
  , Morphism -> String
morphModule :: MODULE
  , Morphism -> String
morphName :: NAME
  , Morphism -> Sign
source :: Sign
  , Morphism -> Sign
target :: Sign
  , Morphism -> MorphType
morphType :: MorphType
  , Morphism -> Map Symbol EXP
symMap :: Map.Map Symbol EXP
  } deriving (Eq Morphism
Eq Morphism =>
(Morphism -> Morphism -> Ordering)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Bool)
-> (Morphism -> Morphism -> Morphism)
-> (Morphism -> Morphism -> Morphism)
-> Ord Morphism
Morphism -> Morphism -> Bool
Morphism -> Morphism -> Ordering
Morphism -> Morphism -> Morphism
forall a.
Eq a =>
(a -> a -> Ordering)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> Bool)
-> (a -> a -> a)
-> (a -> a -> a)
-> Ord a
min :: Morphism -> Morphism -> Morphism
$cmin :: Morphism -> Morphism -> Morphism
max :: Morphism -> Morphism -> Morphism
$cmax :: Morphism -> Morphism -> Morphism
>= :: Morphism -> Morphism -> Bool
$c>= :: Morphism -> Morphism -> Bool
> :: Morphism -> Morphism -> Bool
$c> :: Morphism -> Morphism -> Bool
<= :: Morphism -> Morphism -> Bool
$c<= :: Morphism -> Morphism -> Bool
< :: Morphism -> Morphism -> Bool
$c< :: Morphism -> Morphism -> Bool
compare :: Morphism -> Morphism -> Ordering
$ccompare :: Morphism -> Morphism -> Ordering
$cp1Ord :: Eq Morphism
Ord, Int -> Morphism -> ShowS
[Morphism] -> ShowS
Morphism -> String
(Int -> Morphism -> ShowS)
-> (Morphism -> String) -> ([Morphism] -> ShowS) -> Show Morphism
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [Morphism] -> ShowS
$cshowList :: [Morphism] -> ShowS
show :: Morphism -> String
$cshow :: Morphism -> String
showsPrec :: Int -> Morphism -> ShowS
$cshowsPrec :: Int -> Morphism -> ShowS
Show, Typeable)

-- constructs an identity morphism
idMorph :: Sign -> Morphism
idMorph :: Sign -> Morphism
idMorph sig :: Sign
sig = String
-> String
-> String
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism String
gen_base String
gen_module "" Sign
sig Sign
sig MorphType
Unknown Map Symbol EXP
forall k a. Map k a
Map.empty

-- composes two morphisms
compMorph :: Morphism -> Morphism -> Result Morphism
compMorph :: Morphism -> Morphism -> Result Morphism
compMorph m1 :: Morphism
m1 m2 :: Morphism
m2 = do
  let newmap :: Map Symbol EXP
newmap =
        (Symbol -> Map Symbol EXP -> Map Symbol EXP)
-> Map Symbol EXP -> Set Symbol -> Map Symbol EXP
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ s :: Symbol
s ->
                    let Just e1 :: EXP
e1 = Symbol -> Morphism -> Maybe EXP
mapSymbol Symbol
s Morphism
m1
                        Just e2 :: EXP
e2 = Morphism -> EXP -> Maybe EXP
translate Morphism
m2 EXP
e1
                        in 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
e2
                 )
                 Map Symbol EXP
forall k a. Map k a
Map.empty (Set Symbol -> Map Symbol EXP) -> Set Symbol -> Map Symbol EXP
forall a b. (a -> b) -> a -> b
$
                 Sign -> Set Symbol
getDeclaredSyms (Sign -> Set Symbol) -> Sign -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
m1
  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
$ String
-> String
-> String
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism String
gen_base String
gen_module "" (Morphism -> Sign
source Morphism
m1) (Morphism -> Sign
target Morphism
m2) MorphType
Unknown Map Symbol EXP
newmap

-- applies a morphism to a symbol in the source signature
mapSymbol :: Symbol -> Morphism -> Maybe EXP
mapSymbol :: Symbol -> Morphism -> Maybe EXP
mapSymbol s :: Symbol
s m :: Morphism
m =
  let sig :: Sign
sig = Morphism -> Sign
source Morphism
m
      in if Symbol -> Sign -> Bool
isDeclaredSym Symbol
s Sign
sig
            then EXP -> Maybe EXP
forall a. a -> Maybe a
Just (EXP -> Maybe EXP) -> EXP -> Maybe EXP
forall a b. (a -> b) -> a -> b
$ EXP -> Symbol -> Map Symbol EXP -> EXP
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault (Symbol -> EXP
Const Symbol
s) Symbol
s (Map Symbol EXP -> EXP) -> Map Symbol EXP -> EXP
forall a b. (a -> b) -> a -> b
$ Morphism -> Map Symbol EXP
symMap Morphism
m
            else if Symbol -> Sign -> Bool
isDefinedSym Symbol
s Sign
sig
                    then do EXP
val <- Symbol -> Sign -> Maybe EXP
getSymValue Symbol
s Sign
sig
                            Morphism -> EXP -> Maybe EXP
translate Morphism
m EXP
val
                    else Maybe EXP
forall a. Maybe a
Nothing

-- translates a well-formed expression along the given morphism
translate :: Morphism -> EXP -> Maybe EXP
translate :: Morphism -> EXP -> Maybe EXP
translate m :: Morphism
m e :: EXP
e = Morphism -> EXP -> Maybe EXP
translateH Morphism
m (EXP -> EXP
recForm EXP
e)

translateH :: Morphism -> EXP -> Maybe EXP
translateH :: Morphism -> EXP -> Maybe EXP
translateH _ Type = EXP -> Maybe EXP
forall a. a -> Maybe a
Just EXP
Type
translateH _ (Var n :: String
n) = EXP -> Maybe EXP
forall a. a -> Maybe a
Just (EXP -> Maybe EXP) -> EXP -> Maybe EXP
forall a b. (a -> b) -> a -> b
$ String -> EXP
Var String
n
translateH m :: Morphism
m (Const s :: Symbol
s) = Symbol -> Morphism -> Maybe EXP
mapSymbol Symbol
s Morphism
m
translateH m :: Morphism
m (Appl f :: EXP
f [a :: EXP
a]) =
  do EXP
f1 <- Morphism -> EXP -> Maybe EXP
translateH Morphism
m EXP
f
     EXP
a1 <- Morphism -> EXP -> Maybe EXP
translateH Morphism
m EXP
a
     EXP -> Maybe EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> Maybe EXP) -> EXP -> Maybe EXP
forall a b. (a -> b) -> a -> b
$ EXP -> [EXP] -> EXP
Appl EXP
f1 [EXP
a1]
translateH m :: Morphism
m (Func [t :: EXP
t] s :: EXP
s) =
  do EXP
t1 <- Morphism -> EXP -> Maybe EXP
translateH Morphism
m EXP
t
     EXP
s1 <- Morphism -> EXP -> Maybe EXP
translateH Morphism
m EXP
s
     EXP -> Maybe EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> Maybe EXP) -> EXP -> Maybe EXP
forall a b. (a -> b) -> a -> b
$ [EXP] -> EXP -> EXP
Func [EXP
t1] EXP
s1
translateH m :: Morphism
m (Pi [(x :: String
x, t :: EXP
t)] a :: EXP
a) =
  do EXP
t1 <- Morphism -> EXP -> Maybe EXP
translateH Morphism
m EXP
t
     EXP
a1 <- Morphism -> EXP -> Maybe EXP
translateH Morphism
m EXP
a
     EXP -> Maybe EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> Maybe EXP) -> EXP -> Maybe EXP
forall a b. (a -> b) -> a -> b
$ CONTEXT -> EXP -> EXP
Pi [(String
x, EXP
t1)] EXP
a1
translateH m :: Morphism
m (Lamb [(x :: String
x, t :: EXP
t)] a :: EXP
a) =
  do EXP
t1 <- Morphism -> EXP -> Maybe EXP
translateH Morphism
m EXP
t
     EXP
a1 <- Morphism -> EXP -> Maybe EXP
translateH Morphism
m EXP
a
     EXP -> Maybe EXP
forall (m :: * -> *) a. Monad m => a -> m a
return (EXP -> Maybe EXP) -> EXP -> Maybe EXP
forall a b. (a -> b) -> a -> b
$ CONTEXT -> EXP -> EXP
Lamb [(String
x, EXP
t1)] EXP
a1
translateH _ _ = Maybe EXP
forall a. Maybe a
Nothing

{- converts the morphism into its canonical form where the symbol map contains
   no key/value pairs of the form (s, Const s) -}
canForm :: Morphism -> Morphism
canForm :: Morphism -> Morphism
canForm (Morphism b :: String
b m :: String
m n :: String
n sig1 :: Sign
sig1 sig2 :: Sign
sig2 k :: MorphType
k map1 :: Map Symbol EXP
map1) =
  let map2 :: Map Symbol EXP
map2 = [(Symbol, EXP)] -> Map Symbol EXP
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Symbol, EXP)] -> Map Symbol EXP)
-> [(Symbol, EXP)] -> Map Symbol EXP
forall a b. (a -> b) -> a -> b
$ ((Symbol, EXP) -> Bool) -> [(Symbol, EXP)] -> [(Symbol, EXP)]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (s :: Symbol
s, e :: EXP
e) -> Symbol -> EXP
Const Symbol
s EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
/= EXP
e) ([(Symbol, EXP)] -> [(Symbol, EXP)])
-> [(Symbol, EXP)] -> [(Symbol, EXP)]
forall a b. (a -> b) -> a -> b
$ Map Symbol EXP -> [(Symbol, EXP)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Symbol EXP
map1
      in String
-> String
-> String
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism String
b String
m String
n Sign
sig1 Sign
sig2 MorphType
k Map Symbol EXP
map2

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

eqMorph :: Morphism -> Morphism -> Bool
eqMorph :: Morphism -> Morphism -> Bool
eqMorph (Morphism b1 :: String
b1 m1 :: String
m1 n1 :: String
n1 s1 :: Sign
s1 t1 :: Sign
t1 k1 :: MorphType
k1 map1 :: Map Symbol EXP
map1) (Morphism b2 :: String
b2 m2 :: String
m2 n2 :: String
n2 s2 :: Sign
s2 t2 :: Sign
t2 k2 :: MorphType
k2 map2 :: Map Symbol EXP
map2) =
  (String
b1, String
m1, String
n1, Sign
s1, Sign
t1, MorphType
k1, Map Symbol EXP
map1) (String, String, String, Sign, Sign, MorphType, Map Symbol EXP)
-> (String, String, String, Sign, Sign, MorphType, Map Symbol EXP)
-> Bool
forall a. Eq a => a -> a -> Bool
== (String
b2, String
m2, String
n2, Sign
s2, Sign
t2, MorphType
k2, Map Symbol EXP
map2)

-- pretty printing
instance Pretty Morphism where
  pretty :: Morphism -> Doc
pretty m :: Morphism
m = Map Symbol EXP -> Doc
printSymMap (Map Symbol EXP -> Doc) -> Map Symbol EXP -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> Map Symbol EXP
symMap (Morphism -> Map Symbol EXP) -> Morphism -> Map Symbol EXP
forall a b. (a -> b) -> a -> b
$ Morphism -> Morphism
canForm Morphism
m

printSymMap :: Map.Map Symbol EXP -> Doc
printSymMap :: Map Symbol EXP -> Doc
printSymMap m :: Map Symbol EXP
m =
  [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((Symbol, EXP) -> Doc) -> [(Symbol, EXP)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (s :: Symbol
s, e :: EXP
e) -> Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s Doc -> Doc -> Doc
<+> Doc
mapsto Doc -> Doc -> Doc
<+> EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
e) ([(Symbol, EXP)] -> [Doc]) -> [(Symbol, EXP)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Map Symbol EXP -> [(Symbol, EXP)]
forall k a. Map k a -> [(k, a)]
Map.toList Map Symbol EXP
m

-- constructs the inclusion morphism between signatures
inclusionMorph :: Sign -> Sign -> Result Morphism
inclusionMorph :: Sign -> Sign -> Result Morphism
inclusionMorph sig1 :: Sign
sig1 sig2 :: Sign
sig2 =
  let m :: Morphism
m = String
-> String
-> String
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism String
gen_base String
gen_module "" Sign
sig1 Sign
sig2 MorphType
Unknown Map Symbol EXP
forall k a. Map k a
Map.empty
      in [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe Morphism -> Result Morphism)
-> Maybe Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Morphism -> Maybe Morphism
forall a. a -> Maybe a
Just Morphism
m

-- induces a morphism from the source and target sigs and a symbol map
inducedFromToMorphism :: Map.Map Symbol (EXP, EXP) -> Sign ->
                         Sign -> Result Morphism
inducedFromToMorphism :: Map Symbol (EXP, EXP) -> Sign -> Sign -> Result Morphism
inducedFromToMorphism m :: Map Symbol (EXP, EXP)
m sig1 :: Sign
sig1 sig2 :: Sign
sig2 =
  let mor :: Morphism
mor = String
-> String
-> String
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism String
gen_base String
gen_module "" Sign
sig1 Sign
sig2 MorphType
Unknown Map Symbol EXP
forall k a. Map k a
Map.empty
      defs :: [DEF]
defs = (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]
getLocalDefs Sign
sig1
      in [DEF] -> Map Symbol (EXP, EXP) -> Morphism -> Result Morphism
buildFromToMorph [DEF]
defs Map Symbol (EXP, EXP)
m Morphism
mor

buildFromToMorph :: [DEF] -> Map.Map Symbol (EXP, EXP) -> Morphism ->
                    Result Morphism
buildFromToMorph :: [DEF] -> Map Symbol (EXP, EXP) -> Morphism -> Result Morphism
buildFromToMorph [] _ mor :: Morphism
mor = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism
mor
buildFromToMorph (Def s :: Symbol
s t :: EXP
t _ : ds :: [DEF]
ds) m :: Map Symbol (EXP, EXP)
m mor :: Morphism
mor = do
  let m1 :: Map Symbol EXP
m1 = Morphism -> Map Symbol EXP
symMap Morphism
mor
  let t1 :: EXP
t1 = EXP -> Maybe EXP -> EXP
forall a. a -> Maybe a -> a
fromMaybe (String -> EXP
forall a. HasCallStack => String -> a
error (String -> EXP) -> String -> EXP
forall a b. (a -> b) -> a -> b
$ EXP -> String
badTypeError EXP
t) (Maybe EXP -> EXP) -> Maybe EXP -> EXP
forall a b. (a -> b) -> a -> b
$ Morphism -> EXP -> Maybe EXP
translate Morphism
mor EXP
t
  let sig2 :: Sign
sig2 = Morphism -> Sign
target Morphism
mor
  if Symbol -> Map Symbol (EXP, EXP) -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member Symbol
s Map Symbol (EXP, EXP)
m
     then do
        let Just (v :: EXP
v, t2 :: EXP
t2) = Symbol -> Map Symbol (EXP, EXP) -> Maybe (EXP, EXP)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup Symbol
s Map Symbol (EXP, EXP)
m
        if EXP
t1 EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
t2
           then [DEF] -> Map Symbol (EXP, EXP) -> Morphism -> Result Morphism
buildFromToMorph [DEF]
ds Map Symbol (EXP, EXP)
m (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Morphism
mor {symMap :: Map Symbol EXP
symMap = 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
v Map Symbol EXP
m1 }
           else String -> Result Morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result Morphism) -> String -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Symbol -> EXP -> String
badViewError Symbol
s EXP
t1
     else do
        let s1 :: Symbol
s1 = if EXP -> Maybe EXP
forall a. a -> Maybe a
Just EXP
t1 Maybe EXP -> Maybe EXP -> Bool
forall a. Eq a => a -> a -> Bool
== Symbol -> Sign -> Maybe EXP
getSymType Symbol
s Sign
sig2 then Symbol
s else do
                    let syms :: Set Symbol
syms = EXP -> Sign -> Set Symbol
getSymsOfType EXP
t1 Sign
sig2
                    let local :: Set Symbol
local = Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection Set Symbol
syms (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ Sign -> Set Symbol
getLocalSyms Sign
sig2
                    case Set Symbol -> [Symbol]
forall a. Set a -> [a]
Set.toList Set Symbol
syms of
                         [s' :: Symbol
s'] -> Symbol
s'
                         [] -> String -> Symbol
forall a. HasCallStack => String -> a
error (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> EXP -> String
noSymError Symbol
s EXP
t1
                         _ -> case Set Symbol -> [Symbol]
forall a. Set a -> [a]
Set.toList Set Symbol
local of
                                   [s' :: Symbol
s'] -> Symbol
s'
                                   [] -> String -> Symbol
forall a. HasCallStack => String -> a
error (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> EXP -> String
noSymError Symbol
s EXP
t1
                                   _ -> String -> Symbol
forall a. HasCallStack => String -> a
error (String -> Symbol) -> String -> Symbol
forall a b. (a -> b) -> a -> b
$ Symbol -> EXP -> String
manySymError Symbol
s EXP
t1
        [DEF] -> Map Symbol (EXP, EXP) -> Morphism -> Result Morphism
buildFromToMorph [DEF]
ds Map Symbol (EXP, EXP)
m (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Morphism
mor {symMap :: Map Symbol EXP
symMap = 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 (Symbol -> EXP
Const Symbol
s1) Map Symbol EXP
m1}

-- induces a morphism from the source signature and a symbol map
inducedFromMorphism :: Map.Map Symbol Symbol -> Sign -> Result Morphism
inducedFromMorphism :: Map Symbol Symbol -> Sign -> Result Morphism
inducedFromMorphism m :: Map Symbol Symbol
m sig1 :: Sign
sig1 = do
  let mor :: Morphism
mor = String
-> String
-> String
-> Sign
-> Sign
-> MorphType
-> Map Symbol EXP
-> Morphism
Morphism String
gen_base String
gen_module "" Sign
sig1 Sign
emptySig MorphType
Unknown (Map Symbol EXP -> Morphism) -> Map Symbol EXP -> Morphism
forall a b. (a -> b) -> a -> b
$
              (Symbol -> EXP) -> Map Symbol Symbol -> Map Symbol EXP
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map Symbol -> EXP
Const Map Symbol Symbol
m
  let defs :: [DEF]
defs = (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
sig1
  [DEF] -> Morphism -> Result Morphism
buildFromMorph [DEF]
defs Morphism
mor

buildFromMorph :: [DEF] -> Morphism -> Result Morphism
buildFromMorph :: [DEF] -> Morphism -> Result Morphism
buildFromMorph [] mor :: Morphism
mor = Morphism -> Result Morphism
forall (m :: * -> *) a. Monad m => a -> m a
return Morphism
mor
buildFromMorph (Def s :: Symbol
s t :: EXP
t _ : ds :: [DEF]
ds) mor :: Morphism
mor = do
  let sig2 :: Sign
sig2 = Morphism -> Sign
target Morphism
mor
  let t1 :: EXP
t1 = EXP -> Maybe EXP -> EXP
forall a. a -> Maybe a -> a
fromMaybe (String -> EXP
forall a. HasCallStack => String -> a
error (String -> EXP) -> String -> EXP
forall a b. (a -> b) -> a -> b
$ EXP -> String
badTypeError EXP
t) (Maybe EXP -> EXP) -> Maybe EXP -> EXP
forall a b. (a -> b) -> a -> b
$ Morphism -> EXP -> Maybe EXP
translate Morphism
mor EXP
t
  let Just (Const s1 :: Symbol
s1) = Symbol -> Morphism -> Maybe EXP
mapSymbol Symbol
s Morphism
mor
  case Symbol -> Sign -> Maybe EXP
getSymType Symbol
s1 Sign
sig2 of
       Just t2 :: EXP
t2 ->
          if EXP
t1 EXP -> EXP -> Bool
forall a. Eq a => a -> a -> Bool
== EXP
t2
             then [DEF] -> Morphism -> Result Morphism
buildFromMorph [DEF]
ds Morphism
mor
             else String -> Result Morphism
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result Morphism) -> String -> Result Morphism
forall a b. (a -> b) -> a -> b
$ Symbol -> EXP -> String
badViewError Symbol
s1 EXP
t1
       Nothing -> [DEF] -> Morphism -> Result Morphism
buildFromMorph [DEF]
ds (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$
                    Morphism
mor { target :: Sign
target = DEF -> Sign -> Sign
addDef (Symbol -> EXP -> Maybe EXP -> DEF
Def Symbol
s1 EXP
t1 Maybe EXP
forall a. Maybe a
Nothing) Sign
sig2 }

{- -------------------------------------------------------------------------
------------------------------------------------------------------------- -}

-- ERROR MESSAGES
badTypeError :: EXP -> String
badTypeError :: EXP -> String
badTypeError t :: EXP
t = "Type/kind " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ " cannot be translated."

badViewError :: Symbol -> EXP -> String
badViewError :: Symbol -> EXP -> String
badViewError s :: Symbol
s t :: EXP
t = "Symbol " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s) String -> ShowS
forall a. [a] -> [a] -> [a]
++
   " must be mapped to an expression of type/kind " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "."

noSymError :: Symbol -> EXP -> String
noSymError :: Symbol -> EXP -> String
noSymError s :: Symbol
s t :: EXP
t = "Symbol " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Symbol -> Doc
forall a. Pretty a => a -> Doc
pretty Symbol
s) String -> ShowS
forall a. [a] -> [a] -> [a]
++
   " cannot be mapped to anything as the target signature contains" String -> ShowS
forall a. [a] -> [a] -> [a]
++
   " no symbols of type/kind " String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (EXP -> Doc
forall a. Pretty a => a -> Doc
pretty EXP
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "."

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