{-# LANGUAGE DeriveDataTypeable #-}
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)
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)
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
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
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
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
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
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)
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
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
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}
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 }
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]
++ "."