{-# LANGUAGE DeriveDataTypeable #-}
{- |
Module      :  ./DFOL/Morphism.hs
Description :  Definition of signature morphisms for
               first-order logic with dependent types (DFOL)
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 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

-- morphisms for DFOL - maps of symbol names
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)

-- constructs an identity morphism
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

-- composes two morphisms
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

-- determines whether a morphism is valid
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

{- converts the morphism into its canonical form where the symbol map contains
   no key/value pairs of the form (k,k) -}
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

-- constructs the inclusion morphism between signatures
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

{- generated and cogenerated signatures
Algorithm description:

FOR GENERATED SIGNATURES

Input : a signature "sig" and a set of symbols "syms"
Output : an inclusion morphism

1 : Check if all symbols in syms occur in sig; if not, output Nothing

2 : Initialize the set of symbols "incl" which necessarily must be included
    in the generated signature to syms
    Initialize the set "done" of analyzed symbols to empty
    Initialize the set "todo" of symbols to be analyzed to syms

3 : Check if todo is empty
    3.1 : If yes, go to 5
    3.2 : If not, go to 4

4 : Pick a symbol "s" from todo
    4.1 : Get the type "t" of s in sig
    4.2 : Get the set "vars" of free variables in t, i.e. the symbols of sig
          that t depends on
    4.3 : For each "v" in vars :
          4.3.1 : Add v to incl
          4.3.2 : If v does not occur in done, add it to todo
    4.4 : Remove v from todo and add it to done
    4.5 : Go to 3

5 : Let "sig1" be the subsignature of sig containing only the symbols in incl
    and output the inclusion morphism m : sig1 -> sig

FOR COGENERATED SIGNATURES

Input : a signature "sig" and a set of symbols "syms"
Output : an inclusion morphism

1 : Check if all symbols in syms occur in sig; if not, output Nothing

2 : Initialize the set of symbols "excl" which necessarily must be excluded
    from the cogenerated signature to syms

3 : For each symbol "s" in sig (keeping the order in which they are defined) :
    3.1 : If s does not occur in excl :
          4.1 : Get the type "t" of s in sig
          4.2 : Get the set "vars" of free variables in t, i.e. the symbols
                of sig that t depends on
          4.3 : If any of the symbols in vars occurs in excl, add s to excl

4 : Let "sig1" be the subsignature of sig containing all the symbols not
    occurring in excl and output the inclusion morphism m : sig1 -> sig
-}
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

-- morphism union
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

-- applies a morphism to a symbol
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

-- translates a term, type or formula along the given morphism
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

-- 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 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)

-- pretty printing
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

-- induces a signature morphism from the source signature and a symbol map
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

-- induces a signature morphism from the source and target sigs and a symbol map
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

-- ERROR MESSAGES
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
    }