{- |
Module      :  ./Logic/ExtSign.hs
Description :  derived functions for signatures with symbol sets
Copyright   :  (c) Till Mossakowski, and Uni Bremen 2002-2006
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (imports Logic.Logic)

Functions from the class Logic that operate over signatures are
extended to work over signatures with symbol sets.
-}

module Logic.ExtSign where

import qualified Data.Set as Set
import qualified Data.Map as Map
import Control.Monad
import qualified Control.Monad.Fail as Fail
import Common.Result
import Common.DocUtils
import Common.ExtSign
import Logic.Logic


ext_sym_of :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> ExtSign sign symbol -> Set.Set symbol
ext_sym_of :: lid -> ExtSign sign symbol -> Set symbol
ext_sym_of l :: lid
l = lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
l (sign -> Set symbol)
-> (ExtSign sign symbol -> sign)
-> ExtSign sign symbol
-> Set symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign

-- | simply put all symbols into the symbol set
makeExtSign :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> sign -> ExtSign sign symbol
makeExtSign :: lid -> sign -> ExtSign sign symbol
makeExtSign l :: lid
l s :: sign
s = sign -> Set symbol -> ExtSign sign symbol
forall sign symbol. sign -> Set symbol -> ExtSign sign symbol
ExtSign sign
s (Set symbol -> ExtSign sign symbol)
-> Set symbol -> ExtSign sign symbol
forall a b. (a -> b) -> a -> b
$ lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
l sign
s

ext_ide :: (Ord symbol, Category sign morphism)
           => ExtSign sign symbol -> morphism
ext_ide :: ExtSign sign symbol -> morphism
ext_ide = sign -> morphism
forall object morphism.
Category object morphism =>
object -> morphism
ide (sign -> morphism)
-> (ExtSign sign symbol -> sign) -> ExtSign sign symbol -> morphism
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ExtSign sign symbol -> sign
forall sign symbol. ExtSign sign symbol -> sign
plainSign

ext_empty_signature :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> ExtSign sign symbol
ext_empty_signature :: lid -> ExtSign sign symbol
ext_empty_signature = sign -> ExtSign sign symbol
forall sign symbol. sign -> ExtSign sign symbol
mkExtSign (sign -> ExtSign sign symbol)
-> (lid -> sign) -> lid -> ExtSign sign symbol
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid -> sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign
empty_signature

checkExtSign :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> String -> ExtSign sign symbol -> Result ()
checkExtSign :: lid -> String -> ExtSign sign symbol -> Result ()
checkExtSign l :: lid
l msg :: String
msg e :: ExtSign sign symbol
e@(ExtSign s :: sign
s sy :: Set symbol
sy) = let sys :: Set symbol
sys = lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
l sign
s in
    Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless (Set symbol -> Set symbol -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set symbol
sy Set symbol
sys) (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$
        String -> Result ()
forall a. HasCallStack => String -> a
error (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "inconsistent symbol set in extended signature: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
msg String -> String -> String
forall a. [a] -> [a] -> [a]
++ "\n"
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ ExtSign sign symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ExtSign sign symbol
e "\rwith unknown symbols\n"
             String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc (Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.difference Set symbol
sy Set symbol
sys) ""

ext_signature_union :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> ExtSign sign symbol -> ExtSign sign symbol
               -> Result (ExtSign sign symbol)
ext_signature_union :: lid
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
ext_signature_union l :: lid
l e1 :: ExtSign sign symbol
e1@(ExtSign s1 :: sign
s1 _) e2 :: ExtSign sign symbol
e2@(ExtSign s2 :: sign
s2 _) = do
    lid -> String -> ExtSign sign symbol -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> String -> ExtSign sign symbol -> Result ()
checkExtSign lid
l "ext_signature_union_1" ExtSign sign symbol
e1
    lid -> String -> ExtSign sign symbol -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> String -> ExtSign sign symbol -> Result ()
checkExtSign lid
l "ext_signature_union_2" ExtSign sign symbol
e2
    sign
s <- lid -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
signature_union lid
l sign
s1 sign
s2
    ExtSign sign symbol -> Result (ExtSign sign symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtSign sign symbol -> Result (ExtSign sign symbol))
-> ExtSign sign symbol -> Result (ExtSign sign symbol)
forall a b. (a -> b) -> a -> b
$ lid -> sign -> ExtSign sign symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign lid
l sign
s

ext_signature_intersect :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> ExtSign sign symbol -> ExtSign sign symbol
               -> Result (ExtSign sign symbol)
ext_signature_intersect :: lid
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
ext_signature_intersect l :: lid
l e1 :: ExtSign sign symbol
e1@(ExtSign s1 :: sign
s1 _) e2 :: ExtSign sign symbol
e2@(ExtSign s2 :: sign
s2 _) = do
    lid -> String -> ExtSign sign symbol -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> String -> ExtSign sign symbol -> Result ()
checkExtSign lid
l "ext_signature_intersect_1" ExtSign sign symbol
e1
    lid -> String -> ExtSign sign symbol -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> String -> ExtSign sign symbol -> Result ()
checkExtSign lid
l "ext_signature_intersect_2" ExtSign sign symbol
e2
    sign
s <- lid -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
intersection lid
l sign
s1 sign
s2
    ExtSign sign symbol -> Result (ExtSign sign symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtSign sign symbol -> Result (ExtSign sign symbol))
-> ExtSign sign symbol -> Result (ExtSign sign symbol)
forall a b. (a -> b) -> a -> b
$ lid -> sign -> ExtSign sign symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign lid
l sign
s

ext_is_subsig :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> ExtSign sign symbol -> ExtSign sign symbol -> Bool
ext_is_subsig :: lid -> ExtSign sign symbol -> ExtSign sign symbol -> Bool
ext_is_subsig l :: lid
l (ExtSign sig1 :: sign
sig1 _) (ExtSign sig2 :: sign
sig2 _) =
    lid -> sign -> sign -> Bool
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Bool
is_subsig lid
l sign
sig1 sign
sig2

ext_final_union :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> ExtSign sign symbol -> ExtSign sign symbol
               -> Result (ExtSign sign symbol)
ext_final_union :: lid
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result (ExtSign sign symbol)
ext_final_union l :: lid
l e1 :: ExtSign sign symbol
e1@(ExtSign s1 :: sign
s1 _) e2 :: ExtSign sign symbol
e2@(ExtSign s2 :: sign
s2 _) = do
    lid -> String -> ExtSign sign symbol -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> String -> ExtSign sign symbol -> Result ()
checkExtSign lid
l "f1" ExtSign sign symbol
e1
    lid -> String -> ExtSign sign symbol -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> String -> ExtSign sign symbol -> Result ()
checkExtSign lid
l "f2" ExtSign sign symbol
e2
    sign
s <- lid -> sign -> sign -> Result sign
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result sign
final_union lid
l sign
s1 sign
s2
    ExtSign sign symbol -> Result (ExtSign sign symbol)
forall (m :: * -> *) a. Monad m => a -> m a
return (ExtSign sign symbol -> Result (ExtSign sign symbol))
-> ExtSign sign symbol -> Result (ExtSign sign symbol)
forall a b. (a -> b) -> a -> b
$ lid -> sign -> ExtSign sign symbol
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> sign -> ExtSign sign symbol
makeExtSign lid
l sign
s

ext_inclusion :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> ExtSign sign symbol -> ExtSign sign symbol -> Result morphism
ext_inclusion :: lid
-> ExtSign sign symbol -> ExtSign sign symbol -> Result morphism
ext_inclusion l :: lid
l (ExtSign s1 :: sign
s1 _) (ExtSign s2 :: sign
s2 _) =
    lid -> sign -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> sign -> sign -> Result morphism
inclusion lid
l sign
s1 sign
s2

ext_generated_sign :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> Set.Set symbol -> ExtSign sign symbol -> Result morphism
ext_generated_sign :: lid -> Set symbol -> ExtSign sign symbol -> Result morphism
ext_generated_sign l :: lid
l s :: Set symbol
s (ExtSign sig :: sign
sig _) =
    lid -> Set symbol -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Set symbol -> sign -> Result morphism
generated_sign lid
l Set symbol
s sign
sig

ext_cogenerated_sign :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> Set.Set symbol -> ExtSign sign symbol -> Result morphism
ext_cogenerated_sign :: lid -> Set symbol -> ExtSign sign symbol -> Result morphism
ext_cogenerated_sign l :: lid
l s :: Set symbol
s (ExtSign sig :: sign
sig _) =
    lid -> Set symbol -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> Set symbol -> sign -> Result morphism
cogenerated_sign lid
l Set symbol
s sign
sig

ext_induced_from_morphism :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> EndoMap raw_symbol -> ExtSign sign symbol
               -> Result morphism
ext_induced_from_morphism :: lid -> EndoMap raw_symbol -> ExtSign sign symbol -> Result morphism
ext_induced_from_morphism l :: lid
l rmap :: EndoMap raw_symbol
rmap (ExtSign sigma :: sign
sigma _) = do
  -- first check: do all source raw symbols match with source signature?
  lid -> EndoMap raw_symbol -> sign -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> EndoMap raw_symbol -> sign -> Result ()
checkRawMap lid
l EndoMap raw_symbol
rmap sign
sigma
  morphism
mor <- lid -> EndoMap raw_symbol -> sign -> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> EndoMap raw_symbol -> sign -> Result morphism
induced_from_morphism lid
l EndoMap raw_symbol
rmap sign
sigma
  morphism -> Result ()
forall object morphism.
Category object morphism =>
morphism -> Result ()
legal_mor morphism
mor
  morphism -> Result morphism
forall (m :: * -> *) a. Monad m => a -> m a
return morphism
mor

checkRawMap :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> EndoMap raw_symbol -> sign -> Result ()
checkRawMap :: lid -> EndoMap raw_symbol -> sign -> Result ()
checkRawMap l :: lid
l rmap :: EndoMap raw_symbol
rmap = lid -> [raw_symbol] -> Set symbol -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [raw_symbol] -> Set symbol -> Result ()
checkRawSyms lid
l (EndoMap raw_symbol -> [raw_symbol]
forall k a. Map k a -> [k]
Map.keys EndoMap raw_symbol
rmap) (Set symbol -> Result ())
-> (sign -> Set symbol) -> sign -> Result ()
forall b c a. (b -> c) -> (a -> b) -> a -> c
. lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
l

checkRawSyms :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> [raw_symbol] -> Set.Set symbol -> Result ()
checkRawSyms :: lid -> [raw_symbol] -> Set symbol -> Result ()
checkRawSyms l :: lid
l rsyms :: [raw_symbol]
rsyms syms :: Set symbol
syms = do
  let unknownSyms :: [raw_symbol]
unknownSyms = (raw_symbol -> Bool) -> [raw_symbol] -> [raw_symbol]
forall a. (a -> Bool) -> [a] -> [a]
filter
          ( \ rsy :: raw_symbol
rsy -> Set symbol -> Bool
forall a. Set a -> Bool
Set.null (Set symbol -> Bool) -> Set symbol -> Bool
forall a b. (a -> b) -> a -> b
$ (symbol -> Bool) -> Set symbol -> Set symbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter ((symbol -> raw_symbol -> Bool) -> raw_symbol -> symbol -> Bool
forall a b c. (a -> b -> c) -> b -> a -> c
flip (lid -> symbol -> raw_symbol -> Bool
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid -> symbol -> raw_symbol -> Bool
matches lid
l) raw_symbol
rsy) Set symbol
syms)
          [raw_symbol]
rsyms
  Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([raw_symbol] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [raw_symbol]
unknownSyms)
    (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ [Diagnosis] -> Maybe () -> Result ()
forall a. [Diagnosis] -> Maybe a -> Result a
Result [DiagKind -> String -> [raw_symbol] -> Diagnosis
forall a.
(GetRange a, Pretty a) =>
DiagKind -> String -> a -> Diagnosis
mkDiag DiagKind
Error "unknown symbols" [raw_symbol]
unknownSyms] (Maybe () -> Result ()) -> Maybe () -> Result ()
forall a b. (a -> b) -> a -> b
$ () -> Maybe ()
forall a. a -> Maybe a
Just ()

ext_induced_from_to_morphism :: Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree
        => lid -> EndoMap raw_symbol -> ExtSign sign symbol
               -> ExtSign sign symbol -> Result morphism
ext_induced_from_to_morphism :: lid
-> EndoMap raw_symbol
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result morphism
ext_induced_from_to_morphism l :: lid
l r :: EndoMap raw_symbol
r s :: ExtSign sign symbol
s@(ExtSign p :: sign
p sy :: Set symbol
sy) t :: ExtSign sign symbol
t = do
    lid -> String -> ExtSign sign symbol -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> String -> ExtSign sign symbol -> Result ()
checkExtSign lid
l "from" ExtSign sign symbol
s
    lid -> String -> ExtSign sign symbol -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> String -> ExtSign sign symbol -> Result ()
checkExtSign lid
l "to" ExtSign sign symbol
t
    lid -> EndoMap raw_symbol -> sign -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> EndoMap raw_symbol -> sign -> Result ()
checkRawMap lid
l EndoMap raw_symbol
r sign
p
    lid -> [raw_symbol] -> Set symbol -> Result ()
forall lid sublogics basic_spec sentence symb_items symb_map_items
       sign morphism symbol raw_symbol proof_tree.
Logic
  lid
  sublogics
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol
  proof_tree =>
lid -> [raw_symbol] -> Set symbol -> Result ()
checkRawSyms lid
l (EndoMap raw_symbol -> [raw_symbol]
forall k a. Map k a -> [a]
Map.elems EndoMap raw_symbol
r) (Set symbol -> Result ()) -> Set symbol -> Result ()
forall a b. (a -> b) -> a -> b
$ ExtSign sign symbol -> Set symbol
forall sign symbol. ExtSign sign symbol -> Set symbol
nonImportedSymbols ExtSign sign symbol
t
    morphism
mor <- lid
-> EndoMap raw_symbol
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result morphism
forall lid basic_spec sentence symb_items symb_map_items sign
       morphism symbol raw_symbol.
StaticAnalysis
  lid
  basic_spec
  sentence
  symb_items
  symb_map_items
  sign
  morphism
  symbol
  raw_symbol =>
lid
-> EndoMap raw_symbol
-> ExtSign sign symbol
-> ExtSign sign symbol
-> Result morphism
induced_from_to_morphism lid
l EndoMap raw_symbol
r ExtSign sign symbol
s ExtSign sign symbol
t
    let sysI :: [symbol]
sysI = Set symbol -> [symbol]
forall a. Set a -> [a]
Set.toList (Set symbol -> [symbol]) -> Set symbol -> [symbol]
forall a b. (a -> b) -> a -> b
$ Set symbol -> Set symbol -> Set symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.difference (lid -> sign -> Set symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> Set symbol
symset_of lid
l sign
p) Set symbol
sy
        morM :: EndoMap symbol
morM = lid -> morphism -> EndoMap symbol
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> EndoMap symbol
symmap_of lid
l morphism
mor
        msysI :: [symbol]
msysI = (symbol -> symbol) -> [symbol] -> [symbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ sym :: symbol
sym -> symbol -> symbol -> EndoMap symbol -> symbol
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault symbol
sym symbol
sym EndoMap symbol
morM) [symbol]
sysI
    Bool -> Result () -> Result ()
forall (f :: * -> *). Applicative f => Bool -> f () -> f ()
unless ([symbol]
sysI [symbol] -> [symbol] -> Bool
forall a. Eq a => a -> a -> Bool
== [symbol]
msysI)
      (Result () -> Result ()) -> Result () -> Result ()
forall a b. (a -> b) -> a -> b
$ String -> Result ()
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result ()) -> String -> Result ()
forall a b. (a -> b) -> a -> b
$ "imported symbols are mapped differently.\n"
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ [(symbol, symbol)] -> String -> String
forall a. Pretty a => a -> String -> String
showDoc (((symbol, symbol) -> Bool)
-> [(symbol, symbol)] -> [(symbol, symbol)]
forall a. (a -> Bool) -> [a] -> [a]
filter ((symbol -> symbol -> Bool) -> (symbol, symbol) -> Bool
forall a b c. (a -> b -> c) -> (a, b) -> c
uncurry symbol -> symbol -> Bool
forall a. Eq a => a -> a -> Bool
(/=)) ([(symbol, symbol)] -> [(symbol, symbol)])
-> [(symbol, symbol)] -> [(symbol, symbol)]
forall a b. (a -> b) -> a -> b
$ [symbol] -> [symbol] -> [(symbol, symbol)]
forall a b. [a] -> [b] -> [(a, b)]
zip [symbol]
sysI [symbol]
msysI) ""
    morphism -> Result ()
forall object morphism.
Category object morphism =>
morphism -> Result ()
legal_mor morphism
mor
    morphism -> Result morphism
forall (m :: * -> *) a. Monad m => a -> m a
return morphism
mor