{-# LANGUAGE DeriveDataTypeable #-}
module DFOL.Morphism
( Morphism (..)
, idMorph
, compMorph
, isValidMorph
, canForm
, applyMorph
, mapSymbol
, inclusionMorph
, morphUnion
, inducedFromMorphism
, inducedFromToMorphism
, coGenSig
, toTermMap
) where
import DFOL.AS_DFOL
import DFOL.Sign
import DFOL.Symbol
import Common.Result
import Common.Doc
import Common.DocUtils
import Common.Id
import Common.ExtSign
import qualified Common.Result as Result
import qualified Data.Map as Map
import qualified Data.Set as Set
import Data.Data
data Morphism = Morphism
{ Morphism -> Sign
source :: Sign
, Morphism -> Sign
target :: Sign
, Morphism -> Map NAME NAME
symMap :: Map.Map NAME NAME
} 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 = Sign -> Sign -> Map NAME NAME -> Morphism
Morphism Sign
sig Sign
sig Map NAME NAME
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 =
if Morphism -> Sign
target Morphism
m1 Sign -> Sign -> Bool
forall a. Eq a => a -> a -> Bool
/= Morphism -> Sign
source Morphism
m2
then [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Morphism -> Morphism -> Diagnosis
incompatibleMorphsError Morphism
m1 Morphism
m2] Maybe Morphism
forall a. Maybe a
Nothing
else 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
$ Sign -> Sign -> Map NAME NAME -> Morphism
Morphism (Morphism -> Sign
source Morphism
m1) (Morphism -> Sign
target Morphism
m2) (Map NAME NAME -> Morphism) -> Map NAME NAME -> Morphism
forall a b. (a -> b) -> a -> b
$
(NAME -> Map NAME NAME -> Map NAME NAME)
-> Map NAME NAME -> Set NAME -> Map NAME NAME
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ sym1 :: NAME
sym1 -> let sym2 :: NAME
sym2 = Morphism -> NAME -> NAME
mapSymbol Morphism
m2
(NAME -> NAME) -> NAME -> NAME
forall a b. (a -> b) -> a -> b
$ Morphism -> NAME -> NAME
mapSymbol Morphism
m1 NAME
sym1
in NAME -> NAME -> Map NAME NAME -> Map NAME NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NAME
sym1 NAME
sym2)
Map NAME NAME
forall k a. Map k a
Map.empty (Set NAME -> Map NAME NAME) -> Set NAME -> Map NAME NAME
forall a b. (a -> b) -> a -> b
$
Sign -> Set NAME
getSymbols (Sign -> Set NAME) -> Sign -> Set NAME
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
m1
isValidMorph :: Morphism -> Bool
isValidMorph :: Morphism -> Bool
isValidMorph m :: Morphism
m@(Morphism sig1 :: Sign
sig1 sig2 :: Sign
sig2 map1 :: Map NAME NAME
map1) =
let sym1 :: Set NAME
sym1 = Sign -> Set NAME
getSymbols Sign
sig1
sym2 :: Set NAME
sym2 = Sign -> Set NAME
getSymbols Sign
sig2
checkDom :: Bool
checkDom = Set NAME -> Set NAME -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf (Map NAME NAME -> Set NAME
forall k a. Map k a -> Set k
Map.keysSet Map NAME NAME
map1) Set NAME
sym1
checkCod :: Bool
checkCod = Set NAME -> Set NAME -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf ((NAME -> NAME) -> Set NAME -> Set NAME
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Morphism -> NAME -> NAME
mapSymbol Morphism
m) Set NAME
sym1) Set NAME
sym2
checkTypes :: [Bool]
checkTypes = (NAME -> Bool) -> [NAME] -> [Bool]
forall a b. (a -> b) -> [a] -> [b]
map (Morphism -> NAME -> Bool
checkTypePres Morphism
m) ([NAME] -> [Bool]) -> [NAME] -> [Bool]
forall a b. (a -> b) -> a -> b
$ Set NAME -> [NAME]
forall a. Set a -> [a]
Set.toList Set NAME
sym1
in [Bool] -> Bool
forall (t :: * -> *). Foldable t => t Bool -> Bool
and ([Bool] -> Bool) -> [Bool] -> Bool
forall a b. (a -> b) -> a -> b
$ [Bool
checkDom, Bool
checkCod] [Bool] -> [Bool] -> [Bool]
forall a. [a] -> [a] -> [a]
++ [Bool]
checkTypes
checkTypePres :: Morphism -> NAME -> Bool
checkTypePres :: Morphism -> NAME -> Bool
checkTypePres m :: Morphism
m n :: NAME
n =
let Just type1 :: TYPE
type1 = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n (Sign -> Maybe TYPE) -> Sign -> Maybe TYPE
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
m
Just type2 :: TYPE
type2 = NAME -> Sign -> Maybe TYPE
getSymbolType (Morphism -> NAME -> NAME
mapSymbol Morphism
m NAME
n) (Sign -> Maybe TYPE) -> Sign -> Maybe TYPE
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
m
in Morphism -> TYPE -> TYPE
forall a. Translatable a => Morphism -> a -> a
applyMorph Morphism
m TYPE
type1 TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
type2
canForm :: Morphism -> Morphism
canForm :: Morphism -> Morphism
canForm (Morphism sig1 :: Sign
sig1 sig2 :: Sign
sig2 map1 :: Map NAME NAME
map1) =
let map2 :: Map NAME NAME
map2 = [(NAME, NAME)] -> Map NAME NAME
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(NAME, NAME)] -> Map NAME NAME)
-> [(NAME, NAME)] -> Map NAME NAME
forall a b. (a -> b) -> a -> b
$ ((NAME, NAME) -> Bool) -> [(NAME, NAME)] -> [(NAME, NAME)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((NAME -> NAME -> Bool) -> (NAME, NAME) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry NAME -> NAME -> Bool
forall a. Eq a => a -> a -> Bool
(/=)) ([(NAME, NAME)] -> [(NAME, NAME)])
-> [(NAME, NAME)] -> [(NAME, NAME)]
forall a b. (a -> b) -> a -> b
$ Map NAME NAME -> [(NAME, NAME)]
forall k a. Map k a -> [(k, a)]
Map.toList Map NAME NAME
map1
in Sign -> Sign -> Map NAME NAME -> Morphism
Morphism Sign
sig1 Sign
sig2 Map NAME NAME
map2
inclusionMorph :: Sign -> Sign -> Result.Result Morphism
inclusionMorph :: Sign -> Sign -> Result Morphism
inclusionMorph sig1 :: Sign
sig1 sig2 :: Sign
sig2 =
let m :: Morphism
m = Sign -> Sign -> Map NAME NAME -> Morphism
Morphism Sign
sig1 Sign
sig2 Map NAME NAME
forall k a. Map k a
Map.empty
in if Morphism -> Bool
isValidMorph Morphism
m
then [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.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
else [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Sign -> Sign -> Diagnosis
noSubsigError Sign
sig1 Sign
sig2] Maybe Morphism
forall a. Maybe a
Nothing
coGenSig :: Bool -> Set.Set Symbol -> Sign -> Result Morphism
coGenSig :: Bool -> Set Symbol -> Sign -> Result Morphism
coGenSig flag :: Bool
flag syms :: Set Symbol
syms sig :: Sign
sig@(Sign ds :: [DECL]
ds) =
let names :: Set NAME
names = (Symbol -> NAME) -> Set Symbol -> Set NAME
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map Symbol -> NAME
name Set Symbol
syms
ds1 :: [SDECL]
ds1 = [DECL] -> [SDECL]
expandDecls [DECL]
ds
in if Set NAME -> Set NAME -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set NAME
names (Sign -> Set NAME
getSymbols Sign
sig)
then let incl :: Set NAME
incl = if Bool
flag
then Set NAME -> [SDECL] -> Sign -> Set NAME
cogSig Set NAME
names [SDECL]
ds1 Sign
sig
else Set NAME -> Set NAME -> Set NAME -> Sign -> Set NAME
genSig Set NAME
names Set NAME
forall a. Set a
Set.empty Set NAME
names Sign
sig
ds2 :: [DECL]
ds2 = (SDECL -> DECL) -> [SDECL] -> [DECL]
forall a b. (a -> b) -> [a] -> [b]
map (\ (n :: NAME
n, t :: TYPE
t) -> ([NAME
n], TYPE
t))
([SDECL] -> [DECL]) -> [SDECL] -> [DECL]
forall a b. (a -> b) -> a -> b
$ (SDECL -> Bool) -> [SDECL] -> [SDECL]
forall a. (a -> Bool) -> [a] -> [a]
filter (\ (n :: NAME
n, _) -> NAME -> Set NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member NAME
n Set NAME
incl) [SDECL]
ds1
in Sign -> Sign -> Result Morphism
inclusionMorph ([DECL] -> Sign
Sign [DECL]
ds2) Sign
sig
else [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Set NAME -> Sign -> Diagnosis
symsNotInSigError Set NAME
names Sign
sig] Maybe Morphism
forall a. Maybe a
Nothing
genSig :: Set.Set NAME -> Set.Set NAME -> Set.Set NAME -> Sign -> Set.Set NAME
genSig :: Set NAME -> Set NAME -> Set NAME -> Sign -> Set NAME
genSig incl :: Set NAME
incl done :: Set NAME
done todo :: Set NAME
todo sig :: Sign
sig =
if Set NAME -> Bool
forall a. Set a -> Bool
Set.null Set NAME
todo
then Set NAME
incl
else let n :: NAME
n = Set NAME -> NAME
forall a. Set a -> a
Set.findMin Set NAME
todo
Just t :: TYPE
t = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n Sign
sig
ns :: Set NAME
ns = TYPE -> Set NAME
getFreeVars TYPE
t
incl1 :: Set NAME
incl1 = Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set NAME
incl Set NAME
ns
ns1 :: Set NAME
ns1 = (NAME -> Bool) -> Set NAME -> Set NAME
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (NAME -> Set NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set NAME
done) Set NAME
ns
done1 :: Set NAME
done1 = NAME -> Set NAME -> Set NAME
forall a. Ord a => a -> Set a -> Set a
Set.insert NAME
n Set NAME
done
todo1 :: Set NAME
todo1 = Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.union Set NAME
ns1 (Set NAME -> Set NAME) -> Set NAME -> Set NAME
forall a b. (a -> b) -> a -> b
$ NAME -> Set NAME -> Set NAME
forall a. Ord a => a -> Set a -> Set a
Set.delete NAME
n Set NAME
todo
in Set NAME -> Set NAME -> Set NAME -> Sign -> Set NAME
genSig Set NAME
incl1 Set NAME
done1 Set NAME
todo1 Sign
sig
cogSig :: Set.Set NAME -> [SDECL] -> Sign -> Set.Set NAME
cogSig :: Set NAME -> [SDECL] -> Sign -> Set NAME
cogSig excl :: Set NAME
excl [] sig :: Sign
sig = Set NAME -> Set NAME -> Set NAME
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (Sign -> Set NAME
getSymbols Sign
sig) Set NAME
excl
cogSig excl :: Set NAME
excl ((n :: NAME
n, t :: TYPE
t) : ds :: [SDECL]
ds) sig :: Sign
sig =
if NAME -> Set NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.member NAME
n Set NAME
excl
then Set NAME -> [SDECL] -> Sign -> Set NAME
cogSig Set NAME
excl [SDECL]
ds Sign
sig
else let ns :: [NAME]
ns = Set NAME -> [NAME]
forall a. Set a -> [a]
Set.toList (Set NAME -> [NAME]) -> Set NAME -> [NAME]
forall a b. (a -> b) -> a -> b
$ TYPE -> Set NAME
getFreeVars TYPE
t
depen :: Bool
depen = (NAME -> Bool) -> [NAME] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (NAME -> Set NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
`Set.member` Set NAME
excl) [NAME]
ns
in if Bool
depen
then let excl1 :: Set NAME
excl1 = NAME -> Set NAME -> Set NAME
forall a. Ord a => a -> Set a -> Set a
Set.insert NAME
n Set NAME
excl
in Set NAME -> [SDECL] -> Sign -> Set NAME
cogSig Set NAME
excl1 [SDECL]
ds Sign
sig
else Set NAME -> [SDECL] -> Sign -> Set NAME
cogSig Set NAME
excl [SDECL]
ds Sign
sig
morphUnion :: Morphism -> Morphism -> Result.Result Morphism
morphUnion :: Morphism -> Morphism -> Result Morphism
morphUnion m1 :: Morphism
m1@(Morphism sig1D :: Sign
sig1D sig1C :: Sign
sig1C map1 :: Map NAME NAME
map1) m2 :: Morphism
m2@(Morphism sig2D :: Sign
sig2D sig2C :: Sign
sig2C map2 :: Map NAME NAME
map2) =
let Result.Result diag1 :: [Diagnosis]
diag1 sigDM :: Maybe Sign
sigDM = Sign -> Sign -> Result Sign
sigUnion Sign
sig1D Sign
sig2D
Result.Result diag2 :: [Diagnosis]
diag2 sigCM :: Maybe Sign
sigCM = Sign -> Sign -> Result Sign
sigUnion Sign
sig1C Sign
sig2C
Result.Result diag3 :: [Diagnosis]
diag3 map3M :: Maybe (Map NAME NAME)
map3M = Map NAME NAME -> Map NAME NAME -> Result (Map NAME NAME)
combineMaps Map NAME NAME
map1 Map NAME NAME
map2
in case Maybe Sign
sigDM of
Nothing -> [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Diagnosis]
diag1 Maybe Morphism
forall a. Maybe a
Nothing
Just sigD :: Sign
sigD ->
case Maybe Sign
sigCM of
Nothing -> [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Diagnosis]
diag2 Maybe Morphism
forall a. Maybe a
Nothing
Just sigC :: Sign
sigC ->
case Maybe (Map NAME NAME)
map3M of
Nothing -> [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Diagnosis]
diag3 Maybe Morphism
forall a. Maybe a
Nothing
Just map3 :: Map NAME NAME
map3 ->
let m :: Morphism
m = Sign -> Sign -> Map NAME NAME -> Morphism
Morphism Sign
sigD Sign
sigC Map NAME NAME
map3
in if Morphism -> Bool
isValidMorph Morphism
m
then [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.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
else [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result
[Morphism -> Morphism -> Diagnosis
invalidMorphError Morphism
m1 Morphism
m2] Maybe Morphism
forall a. Maybe a
Nothing
combineMaps :: Map.Map NAME NAME -> Map.Map NAME NAME ->
Result.Result (Map.Map NAME NAME)
combineMaps :: Map NAME NAME -> Map NAME NAME -> Result (Map NAME NAME)
combineMaps map1 :: Map NAME NAME
map1 map2 :: Map NAME NAME
map2 = Map NAME NAME -> [(NAME, NAME)] -> Result (Map NAME NAME)
combineMapsH Map NAME NAME
map1 ([(NAME, NAME)] -> Result (Map NAME NAME))
-> [(NAME, NAME)] -> Result (Map NAME NAME)
forall a b. (a -> b) -> a -> b
$ Map NAME NAME -> [(NAME, NAME)]
forall k a. Map k a -> [(k, a)]
Map.toList Map NAME NAME
map2
combineMapsH :: Map.Map NAME NAME -> [(NAME, NAME)] ->
Result.Result (Map.Map NAME NAME)
combineMapsH :: Map NAME NAME -> [(NAME, NAME)] -> Result (Map NAME NAME)
combineMapsH map1 :: Map NAME NAME
map1 [] = [Diagnosis] -> Maybe (Map NAME NAME) -> Result (Map NAME NAME)
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe (Map NAME NAME) -> Result (Map NAME NAME))
-> Maybe (Map NAME NAME) -> Result (Map NAME NAME)
forall a b. (a -> b) -> a -> b
$ Map NAME NAME -> Maybe (Map NAME NAME)
forall a. a -> Maybe a
Just Map NAME NAME
map1
combineMapsH map1 :: Map NAME NAME
map1 ((k :: NAME
k, v :: NAME
v) : ds :: [(NAME, NAME)]
ds) =
if NAME -> Map NAME NAME -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member NAME
k Map NAME NAME
map1
then let Just v1 :: NAME
v1 = NAME -> Map NAME NAME -> Maybe NAME
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup NAME
k Map NAME NAME
map1
in if NAME
v NAME -> NAME -> Bool
forall a. Eq a => a -> a -> Bool
== NAME
v1
then Map NAME NAME -> [(NAME, NAME)] -> Result (Map NAME NAME)
combineMapsH Map NAME NAME
map1 [(NAME, NAME)]
ds
else [Diagnosis] -> Maybe (Map NAME NAME) -> Result (Map NAME NAME)
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [NAME -> NAME -> NAME -> Diagnosis
incompatibleMapError NAME
k NAME
v NAME
v1] Maybe (Map NAME NAME)
forall a. Maybe a
Nothing
else let map2 :: Map NAME NAME
map2 = NAME -> NAME -> Map NAME NAME -> Map NAME NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NAME
k NAME
v Map NAME NAME
map1
in Map NAME NAME -> [(NAME, NAME)] -> Result (Map NAME NAME)
combineMapsH Map NAME NAME
map2 [(NAME, NAME)]
ds
mapSymbol :: Morphism -> NAME -> NAME
mapSymbol :: Morphism -> NAME -> NAME
mapSymbol m :: Morphism
m sym :: NAME
sym = NAME -> NAME -> Map NAME NAME -> NAME
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault NAME
sym NAME
sym (Map NAME NAME -> NAME) -> Map NAME NAME -> NAME
forall a b. (a -> b) -> a -> b
$ Morphism -> Map NAME NAME
symMap Morphism
m
applyMorph :: Translatable a => Morphism -> a -> a
applyMorph :: Morphism -> a -> a
applyMorph m :: Morphism
m t :: a
t =
let syms :: Set NAME
syms = Sign -> Set NAME
getSymbols (Morphism -> Sign
target Morphism
m)
map1 :: Map NAME TERM
map1 = Map NAME NAME -> Map NAME TERM
toTermMap (Map NAME NAME -> Map NAME TERM) -> Map NAME NAME -> Map NAME TERM
forall a b. (a -> b) -> a -> b
$ Morphism -> Map NAME NAME
symMap Morphism
m
in Map NAME TERM -> Set NAME -> a -> a
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
map1 Set NAME
syms a
t
toTermMap :: Map.Map NAME NAME -> Map.Map NAME TERM
toTermMap :: Map NAME NAME -> Map NAME TERM
toTermMap m :: Map NAME NAME
m = [(NAME, TERM)] -> Map NAME TERM
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(NAME, TERM)] -> Map NAME TERM)
-> [(NAME, TERM)] -> Map NAME TERM
forall a b. (a -> b) -> a -> b
$ ((NAME, NAME) -> (NAME, TERM)) -> [(NAME, NAME)] -> [(NAME, TERM)]
forall a b. (a -> b) -> [a] -> [b]
map (\ (k :: NAME
k, a :: NAME
a) -> (NAME
k, NAME -> TERM
Identifier NAME
a))
([(NAME, NAME)] -> [(NAME, TERM)])
-> [(NAME, NAME)] -> [(NAME, TERM)]
forall a b. (a -> b) -> a -> b
$ Map NAME NAME -> [(NAME, NAME)]
forall k a. Map k a -> [(k, a)]
Map.toList Map NAME NAME
m
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 s1 :: Sign
s1 t1 :: Sign
t1 map1 :: Map NAME NAME
map1) (Morphism s2 :: Sign
s2 t2 :: Sign
t2 map2 :: Map NAME NAME
map2) =
(Sign
s1, Sign
t1, Map NAME NAME
map1) (Sign, Sign, Map NAME NAME) -> (Sign, Sign, Map NAME NAME) -> Bool
forall a. Eq a => a -> a -> Bool
== (Sign
s2, Sign
t2, Map NAME NAME
map2)
instance Pretty Morphism where
pretty :: Morphism -> Doc
pretty = Morphism -> Doc
printMorph
printMorph :: Morphism -> Doc
printMorph :: Morphism -> Doc
printMorph m :: Morphism
m =
[Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ if Morphism
m Morphism -> Morphism -> Bool
forall a. Eq a => a -> a -> Bool
== Sign -> Morphism
idMorph (Morphism -> Sign
source Morphism
m)
then [String -> Doc
text "Identity morphism on:", Sign -> Doc
forall a. Pretty a => a -> Doc
pretty (Sign -> Doc) -> Sign -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
m]
else [String -> Doc
text "Source signature:", Sign -> Doc
forall a. Pretty a => a -> Doc
pretty (Sign -> Doc) -> Sign -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
m,
String -> Doc
text "Target signature:", Sign -> Doc
forall a. Pretty a => a -> Doc
pretty (Sign -> Doc) -> Sign -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
target Morphism
m,
String -> Doc
text "Mapping:", Map NAME NAME -> Doc
printSymMap (Map NAME NAME -> Doc) -> Map NAME NAME -> Doc
forall a b. (a -> b) -> a -> b
$ Morphism -> Map NAME NAME
symMap Morphism
m]
printSymMap :: Map.Map NAME NAME -> Doc
printSymMap :: Map NAME NAME -> Doc
printSymMap m :: Map NAME NAME
m = [Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((NAME, NAME) -> Doc) -> [(NAME, NAME)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (\ (k :: NAME
k, a :: NAME
a) -> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
k Doc -> Doc -> Doc
<+> String -> Doc
text "|->" Doc -> Doc -> Doc
<+> NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
a)
([(NAME, NAME)] -> [Doc]) -> [(NAME, NAME)] -> [Doc]
forall a b. (a -> b) -> a -> b
$ Map NAME NAME -> [(NAME, NAME)]
forall k a. Map k a -> [(k, a)]
Map.toList Map NAME NAME
m
inducedFromMorphism :: Map.Map Symbol Symbol -> Sign -> Result.Result Morphism
inducedFromMorphism :: Map Symbol Symbol -> Sign -> Result Morphism
inducedFromMorphism map1 :: Map Symbol Symbol
map1 sig1 :: Sign
sig1 =
let map2 :: Map NAME NAME
map2 = Map Symbol Symbol -> Map NAME NAME
toNameMap Map Symbol Symbol
map1
Result.Result dgs :: [Diagnosis]
dgs sig2M :: Maybe Sign
sig2M = Sign -> Map NAME NAME -> Result Sign
buildSig Sign
sig1 Map NAME NAME
map2
in case Maybe Sign
sig2M of
Nothing -> [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [Diagnosis]
dgs Maybe Morphism
forall a. Maybe a
Nothing
Just sig2 :: Sign
sig2 -> [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.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 -> Maybe Morphism) -> Morphism -> Maybe Morphism
forall a b. (a -> b) -> a -> b
$ Sign -> Sign -> Map NAME NAME -> Morphism
Morphism Sign
sig1 Sign
sig2 Map NAME NAME
map2
buildSig :: Sign -> Map.Map NAME NAME -> Result.Result Sign
buildSig :: Sign -> Map NAME NAME -> Result Sign
buildSig (Sign ds :: [DECL]
ds) = [SDECL] -> Sign -> Map NAME NAME -> Result Sign
buildSigH ([DECL] -> [SDECL]
expandDecls [DECL]
ds) Sign
emptySig
buildSigH :: [SDECL] -> Sign -> Map.Map NAME NAME -> Result.Result Sign
buildSigH :: [SDECL] -> Sign -> Map NAME NAME -> Result Sign
buildSigH [] sig :: Sign
sig _ = [Diagnosis] -> Maybe Sign -> Result Sign
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [] (Maybe Sign -> Result Sign) -> Maybe Sign -> Result Sign
forall a b. (a -> b) -> a -> b
$ Sign -> Maybe Sign
forall a. a -> Maybe a
Just Sign
sig
buildSigH ((n1 :: NAME
n1, t1 :: TYPE
t1) : ds :: [SDECL]
ds) sig :: Sign
sig map1 :: Map NAME NAME
map1 =
let n2 :: NAME
n2 = NAME -> NAME -> Map NAME NAME -> NAME
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault NAME
n1 NAME
n1 Map NAME NAME
map1
map2 :: Map NAME TERM
map2 = Map NAME NAME -> Map NAME TERM
toTermMap Map NAME NAME
map1
syms :: Set NAME
syms = (NAME -> NAME) -> Set NAME -> Set NAME
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (\ n :: NAME
n -> NAME -> NAME -> Map NAME NAME -> NAME
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault NAME
n NAME
n Map NAME NAME
map1)
(Set NAME -> Set NAME) -> Set NAME -> Set NAME
forall a b. (a -> b) -> a -> b
$ Sign -> Set NAME
getSymbols Sign
sig
t2 :: TYPE
t2 = Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
map2 Set NAME
syms TYPE
t1
in if NAME -> Sign -> Bool
isConstant NAME
n2 Sign
sig
then let Just t3 :: TYPE
t3 = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n2 Sign
sig
in if TYPE
t2 TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
t3
then [SDECL] -> Sign -> Map NAME NAME -> Result Sign
buildSigH [SDECL]
ds Sign
sig Map NAME NAME
map1
else [Diagnosis] -> Maybe Sign -> Result Sign
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [NAME -> TYPE -> TYPE -> Diagnosis
incompatibleViewError1 NAME
n2 TYPE
t2 TYPE
t3]
Maybe Sign
forall a. Maybe a
Nothing
else [SDECL] -> Sign -> Map NAME NAME -> Result Sign
buildSigH [SDECL]
ds (DECL -> Sign -> Sign
addSymbolDecl ([NAME
n2], TYPE
t2) Sign
sig) Map NAME NAME
map1
inducedFromToMorphism :: Map.Map Symbol Symbol -> ExtSign Sign Symbol ->
ExtSign Sign Symbol -> Result.Result Morphism
inducedFromToMorphism :: Map Symbol Symbol
-> ExtSign Sign Symbol -> ExtSign Sign Symbol -> Result Morphism
inducedFromToMorphism map1 :: Map Symbol Symbol
map1 (ExtSign sig1 :: Sign
sig1 _) (ExtSign sig2 :: Sign
sig2 _) =
let map2 :: Map NAME NAME
map2 = Map Symbol Symbol -> Map NAME NAME
toNameMap Map Symbol Symbol
map1
m :: Morphism
m = Sign -> Sign -> Map NAME NAME -> Morphism
Morphism Sign
sig1 Sign
sig2 Map NAME NAME
map2
Sign ds :: [DECL]
ds = Sign
sig1
in [SDECL] -> Morphism -> Result Morphism
buildMorph ([DECL] -> [SDECL]
expandDecls [DECL]
ds) Morphism
m
buildMorph :: [SDECL] -> Morphism -> Result.Result Morphism
buildMorph :: [SDECL] -> Morphism -> Result Morphism
buildMorph [] m :: Morphism
m = [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.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
buildMorph ((n1 :: NAME
n1, t1 :: TYPE
t1) : ds :: [SDECL]
ds) m :: Morphism
m@(Morphism _ sig2 :: Sign
sig2 map1 :: Map NAME NAME
map1) = do
let t2 :: TYPE
t2 = Morphism -> TYPE -> TYPE
forall a. Translatable a => Morphism -> a -> a
applyMorph Morphism
m TYPE
t1
if NAME -> Map NAME NAME -> Bool
forall k a. Ord k => k -> Map k a -> Bool
Map.member NAME
n1 Map NAME NAME
map1
then do
let n2 :: NAME
n2 = Morphism -> NAME -> NAME
mapSymbol Morphism
m NAME
n1
let Just t3 :: TYPE
t3 = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n2 Sign
sig2
if TYPE
t2 TYPE -> TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== TYPE
t3 then [SDECL] -> Morphism -> Result Morphism
buildMorph [SDECL]
ds Morphism
m else
[Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [NAME -> TYPE -> TYPE -> Diagnosis
incompatibleViewError2 NAME
n2 TYPE
t2 TYPE
t3] Maybe Morphism
forall a. Maybe a
Nothing
else do
let t3 :: Maybe TYPE
t3 = NAME -> Sign -> Maybe TYPE
getSymbolType NAME
n1 Sign
sig2
if TYPE -> Maybe TYPE
forall a. a -> Maybe a
Just TYPE
t2 Maybe TYPE -> Maybe TYPE -> Bool
forall a. Eq a => a -> a -> Bool
== Maybe TYPE
t3 then [SDECL] -> Morphism -> Result Morphism
buildMorph [SDECL]
ds Morphism
m else do
let ss :: [NAME]
ss = Sign -> TYPE -> [NAME]
getSymsOfType Sign
sig2 TYPE
t2
case [NAME]
ss of
[s :: NAME
s] -> [SDECL] -> Morphism -> Result Morphism
buildMorph [SDECL]
ds (Morphism -> Result Morphism) -> Morphism -> Result Morphism
forall a b. (a -> b) -> a -> b
$
Morphism
m {symMap :: Map NAME NAME
symMap = NAME -> NAME -> Map NAME NAME -> Map NAME NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NAME
n1 NAME
s (Map NAME NAME -> Map NAME NAME) -> Map NAME NAME -> Map NAME NAME
forall a b. (a -> b) -> a -> b
$ Morphism -> Map NAME NAME
symMap Morphism
m}
[] -> [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [NAME -> TYPE -> Diagnosis
noSymToMapError NAME
n1 TYPE
t2] Maybe Morphism
forall a. Maybe a
Nothing
_ -> [Diagnosis] -> Maybe Morphism -> Result Morphism
forall a. [Diagnosis] -> Maybe a -> Result a
Result.Result [NAME -> TYPE -> [NAME] -> Diagnosis
manySymToMapError NAME
n1 TYPE
t2 [NAME]
ss] Maybe Morphism
forall a. Maybe a
Nothing
incompatibleMorphsError :: Morphism -> Morphism -> Result.Diagnosis
incompatibleMorphsError :: Morphism -> Morphism -> Diagnosis
incompatibleMorphsError m1 :: Morphism
m1 m2 :: Morphism
m2 =
Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
{ diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
, diagString :: String
Result.diagString = "Codomain of the morphism\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Morphism -> Doc
forall a. Pretty a => a -> Doc
pretty Morphism
m1)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nis different from the domain of the morphism\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Morphism -> Doc
forall a. Pretty a => a -> Doc
pretty Morphism
m2)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nhence their composition cannot be constructed."
, diagPos :: Range
Result.diagPos = Range
nullRange
}
incompatibleViewError1 :: NAME -> TYPE -> TYPE -> Result.Diagnosis
incompatibleViewError1 :: NAME -> TYPE -> TYPE -> Diagnosis
incompatibleViewError1 n :: NAME
n t1 :: TYPE
t1 t2 :: TYPE
t2 =
Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
{ diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
, diagString :: String
Result.diagString = "Symbol\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
n)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nmust have both type\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t1)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nand type\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t2)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nin the target signature and hence "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "the view is ill-formed."
, diagPos :: Range
Result.diagPos = Range
nullRange
}
incompatibleViewError2 :: NAME -> TYPE -> TYPE -> Result.Diagnosis
incompatibleViewError2 :: NAME -> TYPE -> TYPE -> Diagnosis
incompatibleViewError2 n :: NAME
n t1 :: TYPE
t1 t2 :: TYPE
t2 =
Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
{ diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
, diagString :: String
Result.diagString = "Symbol\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
n)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nmust have type\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t1)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nbut instead has type\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t2)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nin the target signature and hence "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "the view is ill-formed."
, diagPos :: Range
Result.diagPos = Range
nullRange
}
noSymToMapError :: NAME -> TYPE -> Result.Diagnosis
noSymToMapError :: NAME -> TYPE -> Diagnosis
noSymToMapError n :: NAME
n t :: TYPE
t =
Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
{ diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
, diagString :: String
Result.diagString = "Symbol\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
n)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\ncannot be mapped to anything as the target "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "signature contains no symbols of type\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t)
, diagPos :: Range
Result.diagPos = Range
nullRange
}
manySymToMapError :: NAME -> TYPE -> [NAME] -> Result.Diagnosis
manySymToMapError :: NAME -> TYPE -> [NAME] -> Diagnosis
manySymToMapError n :: NAME
n t :: TYPE
t ss :: [NAME]
ss =
Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
{ diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
, diagString :: String
Result.diagString = "Symbol\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
n)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\ncannot be uniquely mapped as the target "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "signature contains multiple symbols of type\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (TYPE -> Doc
forall a. Pretty a => a -> Doc
pretty TYPE
t) String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\n namely\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show ([NAME] -> Doc
printNames [NAME]
ss)
, diagPos :: Range
Result.diagPos = Range
nullRange
}
noSubsigError :: Sign -> Sign -> Result.Diagnosis
noSubsigError :: Sign -> Sign -> Diagnosis
noSubsigError sig1 :: Sign
sig1 sig2 :: Sign
sig2 =
Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
{ diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
, diagString :: String
Result.diagString = "Signature\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Sign -> Doc
forall a. Pretty a => a -> Doc
pretty Sign
sig1)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nis not a subsignature of\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Sign -> Doc
forall a. Pretty a => a -> Doc
pretty Sign
sig2)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nand hence the inclusion morphism "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "cannot be constructed."
, diagPos :: Range
Result.diagPos = Range
nullRange
}
incompatibleMapError :: NAME -> NAME -> NAME -> Result.Diagnosis
incompatibleMapError :: NAME -> NAME -> NAME -> Diagnosis
incompatibleMapError n :: NAME
n n1 :: NAME
n1 n2 :: NAME
n2 =
Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
{ diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
, diagString :: String
Result.diagString = "Symbol\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
n)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nis mapped both to\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
n1)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nand\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (NAME -> Doc
forall a. Pretty a => a -> Doc
pretty NAME
n2)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nin the target signature and hence "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "the morphism union cannot be constructed."
, diagPos :: Range
Result.diagPos = Range
nullRange
}
invalidMorphError :: Morphism -> Morphism -> Result.Diagnosis
invalidMorphError :: Morphism -> Morphism -> Diagnosis
invalidMorphError m1 :: Morphism
m1 m2 :: Morphism
m2 =
Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
{ diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
, diagString :: String
Result.diagString = "The combination of morphisms\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Morphism -> Doc
forall a. Pretty a => a -> Doc
pretty Morphism
m1)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nand\n" String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Morphism -> Doc
forall a. Pretty a => a -> Doc
pretty Morphism
m2)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nis not a valid morphism and hence "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "their union cannot be constructed."
, diagPos :: Range
Result.diagPos = Range
nullRange
}
symsNotInSigError :: Set.Set NAME -> Sign -> Result.Diagnosis
symsNotInSigError :: Set NAME -> Sign -> Diagnosis
symsNotInSigError syms :: Set NAME
syms sig :: Sign
sig =
Diag :: DiagKind -> String -> Range -> Diagnosis
Result.Diag
{ diagKind :: DiagKind
Result.diagKind = DiagKind
Result.Error
, diagString :: String
Result.diagString = "The symbols\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show ([NAME] -> Doc
printNames ([NAME] -> Doc) -> [NAME] -> Doc
forall a b. (a -> b) -> a -> b
$ Set NAME -> [NAME]
forall a. Set a -> [a]
Set.toList Set NAME
syms)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nare not in the signature\n"
String -> ShowS
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (Sign -> Doc
forall a. Pretty a => a -> Doc
pretty Sign
sig)
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "\nand hence the (co)generated signature "
String -> ShowS
forall a. [a] -> [a] -> [a]
++ "cannot be constructed."
, diagPos :: Range
Result.diagPos = Range
nullRange
}