{-# LANGUAGE DeriveDataTypeable #-} {- | Module : ./LF/Morphism.hs Description : Definition of signature morphisms for the Edinburgh Logical Framework Copyright : (c) Kristina Sojakova, DFKI Bremen 2009 License : GPLv2 or higher, see LICENSE.txt Maintainer : k.sojakova@jacobs-university.de Stability : experimental Portability : portable -} module LF.Morphism ( MorphType (..) , Morphism (..) , idMorph , compMorph , mapSymbol , translate , canForm , inclusionMorph , inducedFromToMorphism , inducedFromMorphism , gen_morph ) where import LF.Sign import Common.Result import Common.Doc hiding (space) import Common.DocUtils import qualified Control.Monad.Fail as Fail import qualified Data.Map as Map import qualified Data.Set as Set import Data.Data import Data.Maybe (isNothing, fromMaybe) gen_morph :: String gen_morph :: String gen_morph = "GEN_MORPH" data MorphType = Definitional | Postulated | Unknown deriving (Eq MorphType Eq MorphType => (MorphType -> MorphType -> Ordering) -> (MorphType -> MorphType -> Bool) -> (MorphType -> MorphType -> Bool) -> (MorphType -> MorphType -> Bool) -> (MorphType -> MorphType -> Bool) -> (MorphType -> MorphType -> MorphType) -> (MorphType -> MorphType -> MorphType) -> Ord MorphType MorphType -> MorphType -> Bool MorphType -> MorphType -> Ordering MorphType -> MorphType -> MorphType forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: MorphType -> MorphType -> MorphType $cmin :: MorphType -> MorphType -> MorphType max :: MorphType -> MorphType -> MorphType $cmax :: MorphType -> MorphType -> MorphType >= :: MorphType -> MorphType -> Bool $c>= :: MorphType -> MorphType -> Bool > :: MorphType -> MorphType -> Bool $c> :: MorphType -> MorphType -> Bool <= :: MorphType -> MorphType -> Bool $c<= :: MorphType -> MorphType -> Bool < :: MorphType -> MorphType -> Bool $c< :: MorphType -> MorphType -> Bool compare :: MorphType -> MorphType -> Ordering $ccompare :: MorphType -> MorphType -> Ordering $cp1Ord :: Eq MorphType Ord, MorphType -> MorphType -> Bool (MorphType -> MorphType -> Bool) -> (MorphType -> MorphType -> Bool) -> Eq MorphType forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a /= :: MorphType -> MorphType -> Bool $c/= :: MorphType -> MorphType -> Bool == :: MorphType -> MorphType -> Bool $c== :: MorphType -> MorphType -> Bool Eq, Int -> MorphType -> ShowS [MorphType] -> ShowS MorphType -> String (Int -> MorphType -> ShowS) -> (MorphType -> String) -> ([MorphType] -> ShowS) -> Show MorphType forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [MorphType] -> ShowS $cshowList :: [MorphType] -> ShowS show :: MorphType -> String $cshow :: MorphType -> String showsPrec :: Int -> MorphType -> ShowS $cshowsPrec :: Int -> MorphType -> ShowS Show, Typeable) -- LF morphism cannot map defined symbols, only declared ones data Morphism = Morphism { Morphism -> String morphBase :: BASE , Morphism -> String morphModule :: MODULE , Morphism -> String morphName :: NAME , Morphism -> Sign source :: Sign , Morphism -> Sign target :: Sign , Morphism -> MorphType morphType :: MorphType , Morphism -> Map Symbol EXP symMap :: Map.Map Symbol EXP } deriving (Eq Morphism Eq Morphism => (Morphism -> Morphism -> Ordering) -> (Morphism -> Morphism -> Bool) -> (Morphism -> Morphism -> Bool) -> (Morphism -> Morphism -> Bool) -> (Morphism -> Morphism -> Bool) -> (Morphism -> Morphism -> Morphism) -> (Morphism -> Morphism -> Morphism) -> Ord Morphism Morphism -> Morphism -> Bool Morphism -> Morphism -> Ordering Morphism -> Morphism -> Morphism forall a. Eq a => (a -> a -> Ordering) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> Bool) -> (a -> a -> a) -> (a -> a -> a) -> Ord a min :: Morphism -> Morphism -> Morphism $cmin :: Morphism -> Morphism -> Morphism max :: Morphism -> Morphism -> Morphism $cmax :: Morphism -> Morphism -> Morphism >= :: Morphism -> Morphism -> Bool $c>= :: Morphism -> Morphism -> Bool > :: Morphism -> Morphism -> Bool $c> :: Morphism -> Morphism -> Bool <= :: Morphism -> Morphism -> Bool $c<= :: Morphism -> Morphism -> Bool < :: Morphism -> Morphism -> Bool $c< :: Morphism -> Morphism -> Bool compare :: Morphism -> Morphism -> Ordering $ccompare :: Morphism -> Morphism -> Ordering $cp1Ord :: Eq Morphism Ord, Int -> Morphism -> ShowS [Morphism] -> ShowS Morphism -> String (Int -> Morphism -> ShowS) -> (Morphism -> String) -> ([Morphism] -> ShowS) -> Show Morphism forall a. (Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a showList :: [Morphism] -> ShowS $cshowList :: [Morphism] -> ShowS show :: Morphism -> String $cshow :: Morphism -> String showsPrec :: Int -> Morphism -> ShowS $cshowsPrec :: Int -> Morphism -> ShowS Show, Typeable) -- constructs an identity morphism idMorph :: Sign -> Morphism idMorph :: Sign -> Morphism idMorph sig :: Sign sig = String -> String -> String -> Sign -> Sign -> MorphType -> Map Symbol EXP -> Morphism Morphism String gen_base String gen_module "" Sign sig Sign sig MorphType Unknown Map Symbol EXP forall k a. Map k a Map.empty -- composes two morphisms compMorph :: Morphism -> Morphism -> Result Morphism compMorph :: Morphism -> Morphism -> Result Morphism compMorph m1 :: Morphism m1 m2 :: Morphism m2 = do let newmap :: Map Symbol EXP newmap = (Symbol -> Map Symbol EXP -> Map Symbol EXP) -> Map Symbol EXP -> Set Symbol -> Map Symbol EXP forall a b. (a -> b -> b) -> b -> Set a -> b Set.fold (\ s :: Symbol s -> let Just e1 :: EXP e1 = Symbol -> Morphism -> Maybe EXP mapSymbol Symbol s Morphism m1 Just e2 :: EXP e2 = Morphism -> EXP -> Maybe EXP translate Morphism m2 EXP e1 in Symbol -> EXP -> Map Symbol EXP -> Map Symbol EXP forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert Symbol s EXP e2 ) Map Symbol EXP forall k a. Map k a Map.empty (Set Symbol -> Map Symbol EXP) -> Set Symbol -> Map Symbol EXP forall a b. (a -> b) -> a -> b $ Sign -> Set Symbol getDeclaredSyms (Sign -> Set Symbol) -> Sign -> Set Symbol forall a b. (a -> b) -> a -> b $ Morphism -> Sign source Morphism m1 Morphism -> Result Morphism forall (m :: * -> *) a. Monad m => a -> m a return (Morphism -> Result Morphism) -> Morphism -> Result Morphism forall a b. (a -> b) -> a -> b $ String -> String -> String -> Sign -> Sign -> MorphType -> Map Symbol EXP -> Morphism Morphism String gen_base String gen_module "" (Morphism -> Sign source Morphism m1) (Morphism -> Sign target Morphism m2) MorphType Unknown Map Symbol EXP newmap -- applies a morphism to a symbol in the source signature mapSymbol :: Symbol -> Morphism -> Maybe EXP mapSymbol :: Symbol -> Morphism -> Maybe EXP mapSymbol s :: Symbol s m :: Morphism m = let sig :: Sign sig = Morphism -> Sign source Morphism m in if Symbol -> Sign -> Bool isDeclaredSym Symbol s Sign sig then EXP -> Maybe EXP forall a. a -> Maybe a Just (EXP -> Maybe EXP) -> EXP -> Maybe EXP forall a b. (a -> b) -> a -> b $ EXP -> Symbol -> Map Symbol EXP -> EXP forall k a. Ord k => a -> k -> Map k a -> a Map.findWithDefault (Symbol -> EXP Const Symbol s) Symbol s (Map Symbol EXP -> EXP) -> Map Symbol EXP -> EXP forall a b. (a -> b) -> a -> b $ Morphism -> Map Symbol EXP symMap Morphism m else if Symbol -> Sign -> Bool isDefinedSym Symbol s Sign sig then do EXP val <- Symbol -> Sign -> Maybe EXP getSymValue Symbol s Sign sig Morphism -> EXP -> Maybe EXP translate Morphism m EXP val else Maybe EXP forall a. Maybe a Nothing -- translates a well-formed expression along the given morphism translate :: Morphism -> EXP -> Maybe EXP translate :: Morphism -> EXP -> Maybe EXP translate m :: Morphism m e :: EXP e = Morphism -> EXP -> Maybe EXP translateH Morphism m (EXP -> EXP recForm EXP e) translateH :: Morphism -> EXP -> Maybe EXP translateH :: Morphism -> EXP -> Maybe EXP translateH _ Type = EXP -> Maybe EXP forall a. a -> Maybe a Just EXP Type translateH _ (Var n :: String n) = EXP -> Maybe EXP forall a. a -> Maybe a Just (EXP -> Maybe EXP) -> EXP -> Maybe EXP forall a b. (a -> b) -> a -> b $ String -> EXP Var String n translateH m :: Morphism m (Const s :: Symbol s) = Symbol -> Morphism -> Maybe EXP mapSymbol Symbol s Morphism m translateH m :: Morphism m (Appl f :: EXP f [a :: EXP a]) = do EXP f1 <- Morphism -> EXP -> Maybe EXP translateH Morphism m EXP f EXP a1 <- Morphism -> EXP -> Maybe EXP translateH Morphism m EXP a EXP -> Maybe EXP forall (m :: * -> *) a. Monad m => a -> m a return (EXP -> Maybe EXP) -> EXP -> Maybe EXP forall a b. (a -> b) -> a -> b $ EXP -> [EXP] -> EXP Appl EXP f1 [EXP a1] translateH m :: Morphism m (Func [t :: EXP t] s :: EXP s) = do EXP t1 <- Morphism -> EXP -> Maybe EXP translateH Morphism m EXP t EXP s1 <- Morphism -> EXP -> Maybe EXP translateH Morphism m EXP s EXP -> Maybe EXP forall (m :: * -> *) a. Monad m => a -> m a return (EXP -> Maybe EXP) -> EXP -> Maybe EXP forall a b. (a -> b) -> a -> b $ [EXP] -> EXP -> EXP Func [EXP t1] EXP s1 translateH m :: Morphism m (Pi [(x :: String x, t :: EXP t)] a :: EXP a) = do EXP t1 <- Morphism -> EXP -> Maybe EXP translateH Morphism m EXP t EXP a1 <- Morphism -> EXP -> Maybe EXP translateH Morphism m EXP a EXP -> Maybe EXP forall (m :: * -> *) a. Monad m => a -> m a return (EXP -> Maybe EXP) -> EXP -> Maybe EXP forall a b. (a -> b) -> a -> b $ CONTEXT -> EXP -> EXP Pi [(String x, EXP t1)] EXP a1 translateH m :: Morphism m (Lamb [(x :: String x, t :: EXP t)] a :: EXP a) = do EXP t1 <- Morphism -> EXP -> Maybe EXP translateH Morphism m EXP t EXP a1 <- Morphism -> EXP -> Maybe EXP translateH Morphism m EXP a EXP -> Maybe EXP forall (m :: * -> *) a. Monad m => a -> m a return (EXP -> Maybe EXP) -> EXP -> Maybe EXP forall a b. (a -> b) -> a -> b $ CONTEXT -> EXP -> EXP Lamb [(String x, EXP t1)] EXP a1 translateH _ _ = Maybe EXP forall a. Maybe a Nothing {- converts the morphism into its canonical form where the symbol map contains no key/value pairs of the form (s, Const s) -} canForm :: Morphism -> Morphism canForm :: Morphism -> Morphism canForm (Morphism b :: String b m :: String m n :: String n sig1 :: Sign sig1 sig2 :: Sign sig2 k :: MorphType k map1 :: Map Symbol EXP map1) = let map2 :: Map Symbol EXP map2 = [(Symbol, EXP)] -> Map Symbol EXP forall k a. Ord k => [(k, a)] -> Map k a Map.fromList ([(Symbol, EXP)] -> Map Symbol EXP) -> [(Symbol, EXP)] -> Map Symbol EXP forall a b. (a -> b) -> a -> b $ ((Symbol, EXP) -> Bool) -> [(Symbol, EXP)] -> [(Symbol, EXP)] forall a. (a -> Bool) -> [a] -> [a] filter (\ (s :: Symbol s, e :: EXP e) -> Symbol -> EXP Const Symbol s EXP -> EXP -> Bool forall a. Eq a => a -> a -> Bool /= EXP e) ([(Symbol, EXP)] -> [(Symbol, EXP)]) -> [(Symbol, EXP)] -> [(Symbol, EXP)] forall a b. (a -> b) -> a -> b $ Map Symbol EXP -> [(Symbol, EXP)] forall k a. Map k a -> [(k, a)] Map.toList Map Symbol EXP map1 in String -> String -> String -> Sign -> Sign -> MorphType -> Map Symbol EXP -> Morphism Morphism String b String m String n Sign sig1 Sign sig2 MorphType k Map Symbol EXP map2 -- equality instance Eq Morphism where m1 :: Morphism m1 == :: Morphism -> Morphism -> Bool == m2 :: Morphism m2 = Morphism -> Morphism -> Bool eqMorph (Morphism -> Morphism canForm Morphism m1) (Morphism -> Morphism canForm Morphism m2) eqMorph :: Morphism -> Morphism -> Bool eqMorph :: Morphism -> Morphism -> Bool eqMorph (Morphism b1 :: String b1 m1 :: String m1 n1 :: String n1 s1 :: Sign s1 t1 :: Sign t1 k1 :: MorphType k1 map1 :: Map Symbol EXP map1) (Morphism b2 :: String b2 m2 :: String m2 n2 :: String n2 s2 :: Sign s2 t2 :: Sign t2 k2 :: MorphType k2 map2 :: Map Symbol EXP map2) = (String b1, String m1, String n1, Sign s1, Sign t1, MorphType k1, Map Symbol EXP map1) (String, String, String, Sign, Sign, MorphType, Map Symbol EXP) -> (String, String, String, Sign, Sign, MorphType, Map Symbol EXP) -> Bool forall a. Eq a => a -> a -> Bool == (String b2, String m2, String n2, Sign s2, Sign t2, MorphType k2, Map Symbol EXP map2) -- pretty printing instance Pretty Morphism where pretty :: Morphism -> Doc pretty m :: Morphism m = Map Symbol EXP -> Doc printSymMap (Map Symbol EXP -> Doc) -> Map Symbol EXP -> Doc forall a b. (a -> b) -> a -> b $ Morphism -> Map Symbol EXP symMap (Morphism -> Map Symbol EXP) -> Morphism -> Map Symbol EXP forall a b. (a -> b) -> a -> b $ Morphism -> Morphism canForm Morphism m printSymMap :: Map.Map Symbol EXP -> Doc printSymMap :: Map Symbol EXP -> Doc printSymMap m :: Map Symbol EXP m = [Doc] -> Doc vcat ([Doc] -> Doc) -> [Doc] -> Doc forall a b. (a -> b) -> a -> b $ ((Symbol, EXP) -> Doc) -> [(Symbol, EXP)] -> [Doc] forall a b. (a -> b) -> [a] -> [b] map (\ (s :: Symbol s, e :: EXP e) -> Symbol -> Doc forall a. Pretty a => a -> Doc pretty Symbol s Doc -> Doc -> Doc <+> Doc mapsto Doc -> Doc -> Doc <+> EXP -> Doc forall a. Pretty a => a -> Doc pretty EXP e) ([(Symbol, EXP)] -> [Doc]) -> [(Symbol, EXP)] -> [Doc] forall a b. (a -> b) -> a -> b $ Map Symbol EXP -> [(Symbol, EXP)] forall k a. Map k a -> [(k, a)] Map.toList Map Symbol EXP m -- constructs the inclusion morphism between signatures inclusionMorph :: Sign -> Sign -> Result Morphism inclusionMorph :: Sign -> Sign -> Result Morphism inclusionMorph sig1 :: Sign sig1 sig2 :: Sign sig2 = let m :: Morphism m = String -> String -> String -> Sign -> Sign -> MorphType -> Map Symbol EXP -> Morphism Morphism String gen_base String gen_module "" Sign sig1 Sign sig2 MorphType Unknown Map Symbol EXP forall k a. Map k a Map.empty in [Diagnosis] -> Maybe Morphism -> Result Morphism forall a. [Diagnosis] -> Maybe a -> Result a Result [] (Maybe Morphism -> Result Morphism) -> Maybe Morphism -> Result Morphism forall a b. (a -> b) -> a -> b $ Morphism -> Maybe Morphism forall a. a -> Maybe a Just Morphism m -- induces a morphism from the source and target sigs and a symbol map inducedFromToMorphism :: Map.Map Symbol (EXP, EXP) -> Sign -> Sign -> Result Morphism inducedFromToMorphism :: Map Symbol (EXP, EXP) -> Sign -> Sign -> Result Morphism inducedFromToMorphism m :: Map Symbol (EXP, EXP) m sig1 :: Sign sig1 sig2 :: Sign sig2 = let mor :: Morphism mor = String -> String -> String -> Sign -> Sign -> MorphType -> Map Symbol EXP -> Morphism Morphism String gen_base String gen_module "" Sign sig1 Sign sig2 MorphType Unknown Map Symbol EXP forall k a. Map k a Map.empty defs :: [DEF] defs = (DEF -> Bool) -> [DEF] -> [DEF] forall a. (a -> Bool) -> [a] -> [a] filter (\ (Def _ _ v :: Maybe EXP v) -> Maybe EXP -> Bool forall a. Maybe a -> Bool isNothing Maybe EXP v) ([DEF] -> [DEF]) -> [DEF] -> [DEF] forall a b. (a -> b) -> a -> b $ Sign -> [DEF] getLocalDefs Sign sig1 in [DEF] -> Map Symbol (EXP, EXP) -> Morphism -> Result Morphism buildFromToMorph [DEF] defs Map Symbol (EXP, EXP) m Morphism mor buildFromToMorph :: [DEF] -> Map.Map Symbol (EXP, EXP) -> Morphism -> Result Morphism buildFromToMorph :: [DEF] -> Map Symbol (EXP, EXP) -> Morphism -> Result Morphism buildFromToMorph [] _ mor :: Morphism mor = Morphism -> Result Morphism forall (m :: * -> *) a. Monad m => a -> m a return Morphism mor buildFromToMorph (Def s :: Symbol s t :: EXP t _ : ds :: [DEF] ds) m :: Map Symbol (EXP, EXP) m mor :: Morphism mor = do let m1 :: Map Symbol EXP m1 = Morphism -> Map Symbol EXP symMap Morphism mor let t1 :: EXP t1 = EXP -> Maybe EXP -> EXP forall a. a -> Maybe a -> a fromMaybe (String -> EXP forall a. HasCallStack => String -> a error (String -> EXP) -> String -> EXP forall a b. (a -> b) -> a -> b $ EXP -> String badTypeError EXP t) (Maybe EXP -> EXP) -> Maybe EXP -> EXP forall a b. (a -> b) -> a -> b $ Morphism -> EXP -> Maybe EXP translate Morphism mor EXP t let sig2 :: Sign sig2 = Morphism -> Sign target Morphism mor if Symbol -> Map Symbol (EXP, EXP) -> Bool forall k a. Ord k => k -> Map k a -> Bool Map.member Symbol s Map Symbol (EXP, EXP) m then do let Just (v :: EXP v, t2 :: EXP t2) = Symbol -> Map Symbol (EXP, EXP) -> Maybe (EXP, EXP) forall k a. Ord k => k -> Map k a -> Maybe a Map.lookup Symbol s Map Symbol (EXP, EXP) m if EXP t1 EXP -> EXP -> Bool forall a. Eq a => a -> a -> Bool == EXP t2 then [DEF] -> Map Symbol (EXP, EXP) -> Morphism -> Result Morphism buildFromToMorph [DEF] ds Map Symbol (EXP, EXP) m (Morphism -> Result Morphism) -> Morphism -> Result Morphism forall a b. (a -> b) -> a -> b $ Morphism mor {symMap :: Map Symbol EXP symMap = Symbol -> EXP -> Map Symbol EXP -> Map Symbol EXP forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert Symbol s EXP v Map Symbol EXP m1 } else String -> Result Morphism forall (m :: * -> *) a. MonadFail m => String -> m a Fail.fail (String -> Result Morphism) -> String -> Result Morphism forall a b. (a -> b) -> a -> b $ Symbol -> EXP -> String badViewError Symbol s EXP t1 else do let s1 :: Symbol s1 = if EXP -> Maybe EXP forall a. a -> Maybe a Just EXP t1 Maybe EXP -> Maybe EXP -> Bool forall a. Eq a => a -> a -> Bool == Symbol -> Sign -> Maybe EXP getSymType Symbol s Sign sig2 then Symbol s else do let syms :: Set Symbol syms = EXP -> Sign -> Set Symbol getSymsOfType EXP t1 Sign sig2 let local :: Set Symbol local = Set Symbol -> Set Symbol -> Set Symbol forall a. Ord a => Set a -> Set a -> Set a Set.intersection Set Symbol syms (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol forall a b. (a -> b) -> a -> b $ Sign -> Set Symbol getLocalSyms Sign sig2 case Set Symbol -> [Symbol] forall a. Set a -> [a] Set.toList Set Symbol syms of [s' :: Symbol s'] -> Symbol s' [] -> String -> Symbol forall a. HasCallStack => String -> a error (String -> Symbol) -> String -> Symbol forall a b. (a -> b) -> a -> b $ Symbol -> EXP -> String noSymError Symbol s EXP t1 _ -> case Set Symbol -> [Symbol] forall a. Set a -> [a] Set.toList Set Symbol local of [s' :: Symbol s'] -> Symbol s' [] -> String -> Symbol forall a. HasCallStack => String -> a error (String -> Symbol) -> String -> Symbol forall a b. (a -> b) -> a -> b $ Symbol -> EXP -> String noSymError Symbol s EXP t1 _ -> String -> Symbol forall a. HasCallStack => String -> a error (String -> Symbol) -> String -> Symbol forall a b. (a -> b) -> a -> b $ Symbol -> EXP -> String manySymError Symbol s EXP t1 [DEF] -> Map Symbol (EXP, EXP) -> Morphism -> Result Morphism buildFromToMorph [DEF] ds Map Symbol (EXP, EXP) m (Morphism -> Result Morphism) -> Morphism -> Result Morphism forall a b. (a -> b) -> a -> b $ Morphism mor {symMap :: Map Symbol EXP symMap = Symbol -> EXP -> Map Symbol EXP -> Map Symbol EXP forall k a. Ord k => k -> a -> Map k a -> Map k a Map.insert Symbol s (Symbol -> EXP Const Symbol s1) Map Symbol EXP m1} -- induces a morphism from the source signature and a symbol map inducedFromMorphism :: Map.Map Symbol Symbol -> Sign -> Result Morphism inducedFromMorphism :: Map Symbol Symbol -> Sign -> Result Morphism inducedFromMorphism m :: Map Symbol Symbol m sig1 :: Sign sig1 = do let mor :: Morphism mor = String -> String -> String -> Sign -> Sign -> MorphType -> Map Symbol EXP -> Morphism Morphism String gen_base String gen_module "" Sign sig1 Sign emptySig MorphType Unknown (Map Symbol EXP -> Morphism) -> Map Symbol EXP -> Morphism forall a b. (a -> b) -> a -> b $ (Symbol -> EXP) -> Map Symbol Symbol -> Map Symbol EXP forall a b k. (a -> b) -> Map k a -> Map k b Map.map Symbol -> EXP Const Map Symbol Symbol m let defs :: [DEF] defs = (DEF -> Bool) -> [DEF] -> [DEF] forall a. (a -> Bool) -> [a] -> [a] filter (\ (Def _ _ v :: Maybe EXP v) -> Maybe EXP -> Bool forall a. Maybe a -> Bool isNothing Maybe EXP v) ([DEF] -> [DEF]) -> [DEF] -> [DEF] forall a b. (a -> b) -> a -> b $ Sign -> [DEF] getDefs Sign sig1 [DEF] -> Morphism -> Result Morphism buildFromMorph [DEF] defs Morphism mor buildFromMorph :: [DEF] -> Morphism -> Result Morphism buildFromMorph :: [DEF] -> Morphism -> Result Morphism buildFromMorph [] mor :: Morphism mor = Morphism -> Result Morphism forall (m :: * -> *) a. Monad m => a -> m a return Morphism mor buildFromMorph (Def s :: Symbol s t :: EXP t _ : ds :: [DEF] ds) mor :: Morphism mor = do let sig2 :: Sign sig2 = Morphism -> Sign target Morphism mor let t1 :: EXP t1 = EXP -> Maybe EXP -> EXP forall a. a -> Maybe a -> a fromMaybe (String -> EXP forall a. HasCallStack => String -> a error (String -> EXP) -> String -> EXP forall a b. (a -> b) -> a -> b $ EXP -> String badTypeError EXP t) (Maybe EXP -> EXP) -> Maybe EXP -> EXP forall a b. (a -> b) -> a -> b $ Morphism -> EXP -> Maybe EXP translate Morphism mor EXP t let Just (Const s1 :: Symbol s1) = Symbol -> Morphism -> Maybe EXP mapSymbol Symbol s Morphism mor case Symbol -> Sign -> Maybe EXP getSymType Symbol s1 Sign sig2 of Just t2 :: EXP t2 -> if EXP t1 EXP -> EXP -> Bool forall a. Eq a => a -> a -> Bool == EXP t2 then [DEF] -> Morphism -> Result Morphism buildFromMorph [DEF] ds Morphism mor else String -> Result Morphism forall (m :: * -> *) a. MonadFail m => String -> m a Fail.fail (String -> Result Morphism) -> String -> Result Morphism forall a b. (a -> b) -> a -> b $ Symbol -> EXP -> String badViewError Symbol s1 EXP t1 Nothing -> [DEF] -> Morphism -> Result Morphism buildFromMorph [DEF] ds (Morphism -> Result Morphism) -> Morphism -> Result Morphism forall a b. (a -> b) -> a -> b $ Morphism mor { target :: Sign target = DEF -> Sign -> Sign addDef (Symbol -> EXP -> Maybe EXP -> DEF Def Symbol s1 EXP t1 Maybe EXP forall a. Maybe a Nothing) Sign sig2 } {- ------------------------------------------------------------------------- ------------------------------------------------------------------------- -} -- ERROR MESSAGES badTypeError :: EXP -> String badTypeError :: EXP -> String badTypeError t :: EXP t = "Type/kind " String -> ShowS forall a. [a] -> [a] -> [a] ++ Doc -> String forall a. Show a => a -> String show (EXP -> Doc forall a. Pretty a => a -> Doc pretty EXP t) String -> ShowS forall a. [a] -> [a] -> [a] ++ " cannot be translated." badViewError :: Symbol -> EXP -> String badViewError :: Symbol -> EXP -> String badViewError s :: Symbol s t :: EXP t = "Symbol " String -> ShowS forall a. [a] -> [a] -> [a] ++ Doc -> String forall a. Show a => a -> String show (Symbol -> Doc forall a. Pretty a => a -> Doc pretty Symbol s) String -> ShowS forall a. [a] -> [a] -> [a] ++ " must be mapped to an expression of type/kind " String -> ShowS forall a. [a] -> [a] -> [a] ++ Doc -> String forall a. Show a => a -> String show (EXP -> Doc forall a. Pretty a => a -> Doc pretty EXP t) String -> ShowS forall a. [a] -> [a] -> [a] ++ "." noSymError :: Symbol -> EXP -> String noSymError :: Symbol -> EXP -> String noSymError s :: Symbol s t :: EXP t = "Symbol " String -> ShowS forall a. [a] -> [a] -> [a] ++ Doc -> String forall a. Show a => a -> String show (Symbol -> Doc forall a. Pretty a => a -> Doc pretty Symbol s) String -> ShowS forall a. [a] -> [a] -> [a] ++ " cannot be mapped to anything as the target signature contains" String -> ShowS forall a. [a] -> [a] -> [a] ++ " no symbols of type/kind " String -> ShowS forall a. [a] -> [a] -> [a] ++ Doc -> String forall a. Show a => a -> String show (EXP -> Doc forall a. Pretty a => a -> Doc pretty EXP t) String -> ShowS forall a. [a] -> [a] -> [a] ++ "." manySymError :: Symbol -> EXP -> String manySymError :: Symbol -> EXP -> String manySymError s :: Symbol s t :: EXP t = "Symbol " String -> ShowS forall a. [a] -> [a] -> [a] ++ Doc -> String forall a. Show a => a -> String show (Symbol -> Doc forall a. Pretty a => a -> Doc pretty Symbol s) String -> ShowS forall a. [a] -> [a] -> [a] ++ " cannot be mapped to anything as the target signature contains" String -> ShowS forall a. [a] -> [a] -> [a] ++ " more than one symbol of type/kind " String -> ShowS forall a. [a] -> [a] -> [a] ++ Doc -> String forall a. Show a => a -> String show (EXP -> Doc forall a. Pretty a => a -> Doc pretty EXP t) String -> ShowS forall a. [a] -> [a] -> [a] ++ "."