{-# LANGUAGE MultiParamTypeClasses #-}
{-# LANGUAGE FunctionalDependencies #-}
{-# LANGUAGE DeriveDataTypeable #-}
{-# LANGUAGE DeriveGeneric #-}
{-# LANGUAGE FlexibleInstances #-}
{-# LANGUAGE UndecidableInstances #-}
{-# LANGUAGE ExistentialQuantification #-}
{-# LANGUAGE GeneralizedNewtypeDeriving #-}
{-# LANGUAGE StandaloneDeriving #-}
{- |
Module      :  ./Logic/Morphism.hs
Description :  interface (type class) for logic projections (morphisms) in Hets
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2004
License     :  GPLv2 or higher, see LICENSE.txt
Maintainer  :  till@informatik.uni-bremen.de
Stability   :  provisional
Portability :  non-portable (via Logic)

Interface (type class) for logic projections (morphisms) in Hets

Provides data structures for institution morphisms.
   These are just collections of
   functions between (some of) the types of logics.
-}

{- References: see Logic.hs

   Todo:
   morphism modifications / representation maps
-}

module Logic.Morphism where

import Logic.Logic
import Logic.Comorphism

import Data.Data
import qualified Data.Set as Set

import ATerm.Lib

import Common.DocUtils
import Common.AS_Annotation
import Common.Id
import Common.Json
import Common.ToXml

import GHC.Generics (Generic)

class (Language cid,
       Logic lid1 sublogics1
        basic_spec1 sentence1 symb_items1 symb_map_items1
        sign1 morphism1 sign_symbol1 symbol1 proof_tree1,
       Logic lid2 sublogics2
        basic_spec2 sentence2 symb_items2 symb_map_items2
        sign2 morphism2 sign_symbol2 symbol2 proof_tree2) =>
  Morphism cid
    lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
         sign1 morphism1 sign_symbol1 symbol1 proof_tree1
    lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
         sign2 morphism2 sign_symbol2 symbol2 proof_tree2
    | cid -> lid1, cid -> lid2
    , lid1 -> sublogics1 basic_spec1 sentence1 symb_items1
        symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
    , lid2 -> sublogics2 basic_spec2 sentence2 symb_items2
        symb_map_items2 sign2 morphism2 sign_symbol2 symbol2 proof_tree2
  where
    {- source and target logic and sublogic
    the source sublogic is the maximal one for which the comorphism works
    the target sublogic is the resulting one -}
    morSourceLogic :: cid -> lid1
    morSourceSublogic :: cid -> sublogics1
    morTargetLogic :: cid -> lid2
    morTargetSublogic :: cid -> sublogics2
    -- finer information of target sublogics corresponding to source sublogics
    morMapSublogicSign :: cid -> sublogics1 -> sublogics2
    -- information about the source sublogics corresponding to target sublogics
    morMapSublogicSen :: cid -> sublogics2 -> sublogics1
    {- the translation functions are partial
    because the target may be a sublanguage
    map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
    we do not cover theoroidal morphisms,
    since there are no relevant examples and they do not compose nicely
    no mapping of theories, since signatures and sentences are mapped
    contravariantly -}
    morMap_sign :: cid -> sign1 -> Maybe sign2
    morMap_morphism :: cid -> morphism1 -> Maybe morphism2
    morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
          {- also covers semi-morphisms ??
          with no sentence translation
          - but these are spans! -}
    morMap_sign_symbol :: cid -> sign_symbol1 -> Set.Set sign_symbol2
    -- morConstituents not needed, because composition only via lax triangles

-- | identity morphisms
data IdMorphism lid sublogics =
    IdMorphism lid sublogics deriving (Typeable, Int -> IdMorphism lid sublogics -> ShowS
[IdMorphism lid sublogics] -> ShowS
IdMorphism lid sublogics -> String
(Int -> IdMorphism lid sublogics -> ShowS)
-> (IdMorphism lid sublogics -> String)
-> ([IdMorphism lid sublogics] -> ShowS)
-> Show (IdMorphism lid sublogics)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall lid sublogics.
(Show lid, Show sublogics) =>
Int -> IdMorphism lid sublogics -> ShowS
forall lid sublogics.
(Show lid, Show sublogics) =>
[IdMorphism lid sublogics] -> ShowS
forall lid sublogics.
(Show lid, Show sublogics) =>
IdMorphism lid sublogics -> String
showList :: [IdMorphism lid sublogics] -> ShowS
$cshowList :: forall lid sublogics.
(Show lid, Show sublogics) =>
[IdMorphism lid sublogics] -> ShowS
show :: IdMorphism lid sublogics -> String
$cshow :: forall lid sublogics.
(Show lid, Show sublogics) =>
IdMorphism lid sublogics -> String
showsPrec :: Int -> IdMorphism lid sublogics -> ShowS
$cshowsPrec :: forall lid sublogics.
(Show lid, Show sublogics) =>
Int -> IdMorphism lid sublogics -> ShowS
Show)

instance Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism sign_symbol symbol proof_tree =>
         Language (IdMorphism lid sublogics) where
           language_name :: IdMorphism lid sublogics -> String
language_name (IdMorphism lid :: lid
lid sub :: sublogics
sub) = "id_" String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid -> String
forall lid. Language lid => lid -> String
language_name lid
lid
               String -> ShowS
forall a. [a] -> [a] -> [a]
++ case sublogics -> String
forall l. SublogicName l => l -> String
sublogicName sublogics
sub of
                    [] -> ""
                    h :: String
h -> '.' Char -> ShowS
forall a. a -> [a] -> [a]
: String
h

instance Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism sign_symbol symbol proof_tree =>
         Morphism (IdMorphism lid sublogics)
          lid sublogics
          basic_spec sentence symb_items symb_map_items
          sign morphism sign_symbol symbol proof_tree
          lid sublogics
          basic_spec sentence symb_items symb_map_items
          sign morphism sign_symbol symbol proof_tree
         where
           morSourceLogic :: IdMorphism lid sublogics -> lid
morSourceLogic (IdMorphism lid :: lid
lid _sub :: sublogics
_sub) = lid
lid
           morTargetLogic :: IdMorphism lid sublogics -> lid
morTargetLogic (IdMorphism lid :: lid
lid _sub :: sublogics
_sub) = lid
lid
           morSourceSublogic :: IdMorphism lid sublogics -> sublogics
morSourceSublogic (IdMorphism _lid :: lid
_lid sub :: sublogics
sub) = sublogics
sub
           morTargetSublogic :: IdMorphism lid sublogics -> sublogics
morTargetSublogic (IdMorphism _lid :: lid
_lid sub :: sublogics
sub) = sublogics
sub
           -- changed to identities!
           morMapSublogicSign :: IdMorphism lid sublogics -> sublogics -> sublogics
morMapSublogicSign _ x :: sublogics
x = sublogics
x
           morMapSublogicSen :: IdMorphism lid sublogics -> sublogics -> sublogics
morMapSublogicSen _ x :: sublogics
x = sublogics
x
           morMap_sign :: IdMorphism lid sublogics -> sign -> Maybe sign
morMap_sign _ = sign -> Maybe sign
forall a. a -> Maybe a
Just
           morMap_morphism :: IdMorphism lid sublogics -> morphism -> Maybe morphism
morMap_morphism _ = morphism -> Maybe morphism
forall a. a -> Maybe a
Just
           morMap_sentence :: IdMorphism lid sublogics -> sign -> sentence -> Maybe sentence
morMap_sentence _ _ = sentence -> Maybe sentence
forall a. a -> Maybe a
Just
           morMap_sign_symbol :: IdMorphism lid sublogics -> sign_symbol -> Set sign_symbol
morMap_sign_symbol _ = sign_symbol -> Set sign_symbol
forall a. a -> Set a
Set.singleton

-- composition not needed, use lax triangles instead

-- | comorphisms inducing morphisms
class Comorphism cid
            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 sign_symbol1 symbol1 proof_tree1
            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 sign_symbol2 symbol2 proof_tree2 =>
      InducingComorphism cid
            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 sign_symbol1 symbol1 proof_tree1
            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 sign_symbol2 symbol2 proof_tree2
  where
    indMorMap_sign :: cid -> sign2 -> Maybe sign1
    indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
    epsilon :: cid -> sign2 -> Maybe morphism2

-- ------------------------------------------------------------------------

-- Morphisms as spans of comorphisms


{- if the morphism is (psi, alpha, beta) : I -> J
it is replaced with the following span
SignI    id     ->     SignI         psi ->        SignJ
SenI     alpha  <-     psi;SenJ      id  ->        psi;SenJ
ModI     beta   ->     psi^op;ModJ   id  <-        psi^op;ModJ -}

{- 1. introduce a new logic for the domain of the span
this logic will have
the name (SpanDomain cid) where cid is the name of the morphism
sublogics - pairs (s1, s2) with s1 being a sublogic of I and s2
being a sublogic of J; the lattice is the product lattice of the two
existing lattices
basic_spec will be () - the unit type, because we mix signatures
with sentences in specifications
sentence - sentences of J, wrapped
symb_items - ()
symb_map_items - ()
sign - signatures of I
morphism - morphisms of I
sign_symbol - sign_symbols of I
symbol - symbols of I
proof_tree - proof_tree of J -}

data SpanDomain cid = SpanDomain cid deriving (SpanDomain cid -> SpanDomain cid -> Bool
(SpanDomain cid -> SpanDomain cid -> Bool)
-> (SpanDomain cid -> SpanDomain cid -> Bool)
-> Eq (SpanDomain cid)
forall cid. Eq cid => SpanDomain cid -> SpanDomain cid -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: SpanDomain cid -> SpanDomain cid -> Bool
$c/= :: forall cid. Eq cid => SpanDomain cid -> SpanDomain cid -> Bool
== :: SpanDomain cid -> SpanDomain cid -> Bool
$c== :: forall cid. Eq cid => SpanDomain cid -> SpanDomain cid -> Bool
Eq, Int -> SpanDomain cid -> ShowS
[SpanDomain cid] -> ShowS
SpanDomain cid -> String
(Int -> SpanDomain cid -> ShowS)
-> (SpanDomain cid -> String)
-> ([SpanDomain cid] -> ShowS)
-> Show (SpanDomain cid)
forall cid. Show cid => Int -> SpanDomain cid -> ShowS
forall cid. Show cid => [SpanDomain cid] -> ShowS
forall cid. Show cid => SpanDomain cid -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [SpanDomain cid] -> ShowS
$cshowList :: forall cid. Show cid => [SpanDomain cid] -> ShowS
show :: SpanDomain cid -> String
$cshow :: forall cid. Show cid => SpanDomain cid -> String
showsPrec :: Int -> SpanDomain cid -> ShowS
$cshowsPrec :: forall cid. Show cid => Int -> SpanDomain cid -> ShowS
Show)

data SublogicsPair a b = SublogicsPair a b deriving (SublogicsPair a b -> SublogicsPair a b -> Bool
(SublogicsPair a b -> SublogicsPair a b -> Bool)
-> (SublogicsPair a b -> SublogicsPair a b -> Bool)
-> Eq (SublogicsPair a b)
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
forall a b.
(Eq a, Eq b) =>
SublogicsPair a b -> SublogicsPair a b -> Bool
/= :: SublogicsPair a b -> SublogicsPair a b -> Bool
$c/= :: forall a b.
(Eq a, Eq b) =>
SublogicsPair a b -> SublogicsPair a b -> Bool
== :: SublogicsPair a b -> SublogicsPair a b -> Bool
$c== :: forall a b.
(Eq a, Eq b) =>
SublogicsPair a b -> SublogicsPair a b -> Bool
Eq, Eq (SublogicsPair a b)
Eq (SublogicsPair a b) =>
(SublogicsPair a b -> SublogicsPair a b -> Ordering)
-> (SublogicsPair a b -> SublogicsPair a b -> Bool)
-> (SublogicsPair a b -> SublogicsPair a b -> Bool)
-> (SublogicsPair a b -> SublogicsPair a b -> Bool)
-> (SublogicsPair a b -> SublogicsPair a b -> Bool)
-> (SublogicsPair a b -> SublogicsPair a b -> SublogicsPair a b)
-> (SublogicsPair a b -> SublogicsPair a b -> SublogicsPair a b)
-> Ord (SublogicsPair a b)
SublogicsPair a b -> SublogicsPair a b -> Bool
SublogicsPair a b -> SublogicsPair a b -> Ordering
SublogicsPair a b -> SublogicsPair a b -> SublogicsPair a b
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
forall a b. (Ord a, Ord b) => Eq (SublogicsPair a b)
forall a b.
(Ord a, Ord b) =>
SublogicsPair a b -> SublogicsPair a b -> Bool
forall a b.
(Ord a, Ord b) =>
SublogicsPair a b -> SublogicsPair a b -> Ordering
forall a b.
(Ord a, Ord b) =>
SublogicsPair a b -> SublogicsPair a b -> SublogicsPair a b
min :: SublogicsPair a b -> SublogicsPair a b -> SublogicsPair a b
$cmin :: forall a b.
(Ord a, Ord b) =>
SublogicsPair a b -> SublogicsPair a b -> SublogicsPair a b
max :: SublogicsPair a b -> SublogicsPair a b -> SublogicsPair a b
$cmax :: forall a b.
(Ord a, Ord b) =>
SublogicsPair a b -> SublogicsPair a b -> SublogicsPair a b
>= :: SublogicsPair a b -> SublogicsPair a b -> Bool
$c>= :: forall a b.
(Ord a, Ord b) =>
SublogicsPair a b -> SublogicsPair a b -> Bool
> :: SublogicsPair a b -> SublogicsPair a b -> Bool
$c> :: forall a b.
(Ord a, Ord b) =>
SublogicsPair a b -> SublogicsPair a b -> Bool
<= :: SublogicsPair a b -> SublogicsPair a b -> Bool
$c<= :: forall a b.
(Ord a, Ord b) =>
SublogicsPair a b -> SublogicsPair a b -> Bool
< :: SublogicsPair a b -> SublogicsPair a b -> Bool
$c< :: forall a b.
(Ord a, Ord b) =>
SublogicsPair a b -> SublogicsPair a b -> Bool
compare :: SublogicsPair a b -> SublogicsPair a b -> Ordering
$ccompare :: forall a b.
(Ord a, Ord b) =>
SublogicsPair a b -> SublogicsPair a b -> Ordering
$cp1Ord :: forall a b. (Ord a, Ord b) => Eq (SublogicsPair a b)
Ord, Int -> SublogicsPair a b -> ShowS
[SublogicsPair a b] -> ShowS
SublogicsPair a b -> String
(Int -> SublogicsPair a b -> ShowS)
-> (SublogicsPair a b -> String)
-> ([SublogicsPair a b] -> ShowS)
-> Show (SublogicsPair a b)
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
forall a b. (Show a, Show b) => Int -> SublogicsPair a b -> ShowS
forall a b. (Show a, Show b) => [SublogicsPair a b] -> ShowS
forall a b. (Show a, Show b) => SublogicsPair a b -> String
showList :: [SublogicsPair a b] -> ShowS
$cshowList :: forall a b. (Show a, Show b) => [SublogicsPair a b] -> ShowS
show :: SublogicsPair a b -> String
$cshow :: forall a b. (Show a, Show b) => SublogicsPair a b -> String
showsPrec :: Int -> SublogicsPair a b -> ShowS
$cshowsPrec :: forall a b. (Show a, Show b) => Int -> SublogicsPair a b -> ShowS
Show, Typeable)

instance Language cid => Language (SpanDomain cid) where
  language_name :: SpanDomain cid -> String
language_name (SpanDomain cid :: cid
cid) = "SpanDomain" String -> ShowS
forall a. [a] -> [a] -> [a]
++ cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid

{- the category of signatures is exactly the category of signatures of
the sublogic on which the morphism is defined, but with another name -}

instance (Morphism cid
            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 sign_symbol1 symbol1 proof_tree1
            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 sign_symbol2 symbol2 proof_tree2
         , Pretty sign_symbol1)
         => Syntax (SpanDomain cid) () sign_symbol1 () ()
-- default is ok

newtype S2 s = S2 { S2 s -> s
sentence2 :: s }
  deriving (S2 s -> S2 s -> Bool
(S2 s -> S2 s -> Bool) -> (S2 s -> S2 s -> Bool) -> Eq (S2 s)
forall s. Eq s => S2 s -> S2 s -> Bool
forall a. (a -> a -> Bool) -> (a -> a -> Bool) -> Eq a
/= :: S2 s -> S2 s -> Bool
$c/= :: forall s. Eq s => S2 s -> S2 s -> Bool
== :: S2 s -> S2 s -> Bool
$c== :: forall s. Eq s => S2 s -> S2 s -> Bool
Eq, Eq (S2 s)
Eq (S2 s) =>
(S2 s -> S2 s -> Ordering)
-> (S2 s -> S2 s -> Bool)
-> (S2 s -> S2 s -> Bool)
-> (S2 s -> S2 s -> Bool)
-> (S2 s -> S2 s -> Bool)
-> (S2 s -> S2 s -> S2 s)
-> (S2 s -> S2 s -> S2 s)
-> Ord (S2 s)
S2 s -> S2 s -> Bool
S2 s -> S2 s -> Ordering
S2 s -> S2 s -> S2 s
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
forall s. Ord s => Eq (S2 s)
forall s. Ord s => S2 s -> S2 s -> Bool
forall s. Ord s => S2 s -> S2 s -> Ordering
forall s. Ord s => S2 s -> S2 s -> S2 s
min :: S2 s -> S2 s -> S2 s
$cmin :: forall s. Ord s => S2 s -> S2 s -> S2 s
max :: S2 s -> S2 s -> S2 s
$cmax :: forall s. Ord s => S2 s -> S2 s -> S2 s
>= :: S2 s -> S2 s -> Bool
$c>= :: forall s. Ord s => S2 s -> S2 s -> Bool
> :: S2 s -> S2 s -> Bool
$c> :: forall s. Ord s => S2 s -> S2 s -> Bool
<= :: S2 s -> S2 s -> Bool
$c<= :: forall s. Ord s => S2 s -> S2 s -> Bool
< :: S2 s -> S2 s -> Bool
$c< :: forall s. Ord s => S2 s -> S2 s -> Bool
compare :: S2 s -> S2 s -> Ordering
$ccompare :: forall s. Ord s => S2 s -> S2 s -> Ordering
$cp1Ord :: forall s. Ord s => Eq (S2 s)
Ord, Int -> S2 s -> ShowS
[S2 s] -> ShowS
S2 s -> String
(Int -> S2 s -> ShowS)
-> (S2 s -> String) -> ([S2 s] -> ShowS) -> Show (S2 s)
forall s. Show s => Int -> S2 s -> ShowS
forall s. Show s => [S2 s] -> ShowS
forall s. Show s => S2 s -> String
forall a.
(Int -> a -> ShowS) -> (a -> String) -> ([a] -> ShowS) -> Show a
showList :: [S2 s] -> ShowS
$cshowList :: forall s. Show s => [S2 s] -> ShowS
show :: S2 s -> String
$cshow :: forall s. Show s => S2 s -> String
showsPrec :: Int -> S2 s -> ShowS
$cshowsPrec :: forall s. Show s => Int -> S2 s -> ShowS
Show, Typeable, Typeable (S2 s)
Typeable (S2 s) =>
(ATermTable -> S2 s -> IO (ATermTable, Int))
-> (ATermTable -> [S2 s] -> IO (ATermTable, Int))
-> (Int -> ATermTable -> (ATermTable, S2 s))
-> (Int -> ATermTable -> (ATermTable, [S2 s]))
-> ShATermConvertible (S2 s)
Int -> ATermTable -> (ATermTable, [S2 s])
Int -> ATermTable -> (ATermTable, S2 s)
ATermTable -> [S2 s] -> IO (ATermTable, Int)
ATermTable -> S2 s -> IO (ATermTable, Int)
forall t.
Typeable t =>
(ATermTable -> t -> IO (ATermTable, Int))
-> (ATermTable -> [t] -> IO (ATermTable, Int))
-> (Int -> ATermTable -> (ATermTable, t))
-> (Int -> ATermTable -> (ATermTable, [t]))
-> ShATermConvertible t
forall s. ShATermConvertible s => Typeable (S2 s)
forall s.
ShATermConvertible s =>
Int -> ATermTable -> (ATermTable, [S2 s])
forall s.
ShATermConvertible s =>
Int -> ATermTable -> (ATermTable, S2 s)
forall s.
ShATermConvertible s =>
ATermTable -> [S2 s] -> IO (ATermTable, Int)
forall s.
ShATermConvertible s =>
ATermTable -> S2 s -> IO (ATermTable, Int)
fromShATermList' :: Int -> ATermTable -> (ATermTable, [S2 s])
$cfromShATermList' :: forall s.
ShATermConvertible s =>
Int -> ATermTable -> (ATermTable, [S2 s])
fromShATermAux :: Int -> ATermTable -> (ATermTable, S2 s)
$cfromShATermAux :: forall s.
ShATermConvertible s =>
Int -> ATermTable -> (ATermTable, S2 s)
toShATermList' :: ATermTable -> [S2 s] -> IO (ATermTable, Int)
$ctoShATermList' :: forall s.
ShATermConvertible s =>
ATermTable -> [S2 s] -> IO (ATermTable, Int)
toShATermAux :: ATermTable -> S2 s -> IO (ATermTable, Int)
$ctoShATermAux :: forall s.
ShATermConvertible s =>
ATermTable -> S2 s -> IO (ATermTable, Int)
$cp1ShATermConvertible :: forall s. ShATermConvertible s => Typeable (S2 s)
ShATermConvertible, Show (S2 s)
Show (S2 s) => (S2 s -> Doc) -> ([S2 s] -> Doc) -> Pretty (S2 s)
[S2 s] -> Doc
S2 s -> Doc
forall a. Show a => (a -> Doc) -> ([a] -> Doc) -> Pretty a
forall s. Pretty s => Show (S2 s)
forall s. Pretty s => [S2 s] -> Doc
forall s. Pretty s => S2 s -> Doc
pretties :: [S2 s] -> Doc
$cpretties :: forall s. Pretty s => [S2 s] -> Doc
pretty :: S2 s -> Doc
$cpretty :: forall s. Pretty s => S2 s -> Doc
$cp1Pretty :: forall s. Pretty s => Show (S2 s)
Pretty, S2 s -> [Pos]
S2 s -> Range
(S2 s -> Range) -> (S2 s -> [Pos]) -> GetRange (S2 s)
forall s. GetRange s => S2 s -> [Pos]
forall s. GetRange s => S2 s -> Range
forall a. (a -> Range) -> (a -> [Pos]) -> GetRange a
rangeSpan :: S2 s -> [Pos]
$crangeSpan :: forall s. GetRange s => S2 s -> [Pos]
getRange :: S2 s -> Range
$cgetRange :: forall s. GetRange s => S2 s -> Range
GetRange, Typeable (S2 s)
Constr
DataType
Typeable (S2 s) =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> S2 s -> c (S2 s))
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c (S2 s))
-> (S2 s -> Constr)
-> (S2 s -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c (S2 s)))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (S2 s)))
-> ((forall b. Data b => b -> b) -> S2 s -> S2 s)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r)
-> (forall u. (forall d. Data d => d -> u) -> S2 s -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> S2 s -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> S2 s -> m (S2 s))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> S2 s -> m (S2 s))
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> S2 s -> m (S2 s))
-> Data (S2 s)
S2 s -> Constr
S2 s -> DataType
(forall d. Data d => c (t d)) -> Maybe (c (S2 s))
(forall b. Data b => b -> b) -> S2 s -> S2 s
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> S2 s -> c (S2 s)
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (S2 s)
forall s. Data s => Typeable (S2 s)
forall s. Data s => S2 s -> Constr
forall s. Data s => S2 s -> DataType
forall s. Data s => (forall b. Data b => b -> b) -> S2 s -> S2 s
forall s u.
Data s =>
Int -> (forall d. Data d => d -> u) -> S2 s -> u
forall s u. Data s => (forall d. Data d => d -> u) -> S2 s -> [u]
forall s r r'.
Data s =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r
forall s r r'.
Data s =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r
forall s (m :: * -> *).
(Data s, Monad m) =>
(forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
forall s (m :: * -> *).
(Data s, MonadPlus m) =>
(forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
forall s (c :: * -> *).
Data s =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (S2 s)
forall s (c :: * -> *).
Data s =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> S2 s -> c (S2 s)
forall s (t :: * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (S2 s))
forall s (t :: * -> * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (S2 s))
forall a.
Typeable a =>
(forall (c :: * -> *).
 (forall d b. Data d => c (d -> b) -> d -> c b)
 -> (forall g. g -> c g) -> a -> c a)
-> (forall (c :: * -> *).
    (forall b r. Data b => c (b -> r) -> c r)
    -> (forall r. r -> c r) -> Constr -> c a)
-> (a -> Constr)
-> (a -> DataType)
-> (forall (t :: * -> *) (c :: * -> *).
    Typeable t =>
    (forall d. Data d => c (t d)) -> Maybe (c a))
-> (forall (t :: * -> * -> *) (c :: * -> *).
    Typeable t =>
    (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c a))
-> ((forall b. Data b => b -> b) -> a -> a)
-> (forall r r'.
    (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall r r'.
    (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> a -> r)
-> (forall u. (forall d. Data d => d -> u) -> a -> [u])
-> (forall u. Int -> (forall d. Data d => d -> u) -> a -> u)
-> (forall (m :: * -> *).
    Monad m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> (forall (m :: * -> *).
    MonadPlus m =>
    (forall d. Data d => d -> m d) -> a -> m a)
-> Data a
forall u. Int -> (forall d. Data d => d -> u) -> S2 s -> u
forall u. (forall d. Data d => d -> u) -> S2 s -> [u]
forall r r'.
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r
forall r r'.
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r
forall (m :: * -> *).
Monad m =>
(forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
forall (m :: * -> *).
MonadPlus m =>
(forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
forall (c :: * -> *).
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (S2 s)
forall (c :: * -> *).
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> S2 s -> c (S2 s)
forall (t :: * -> *) (c :: * -> *).
Typeable t =>
(forall d. Data d => c (t d)) -> Maybe (c (S2 s))
forall (t :: * -> * -> *) (c :: * -> *).
Typeable t =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (S2 s))
$cS2 :: Constr
$tS2 :: DataType
gmapMo :: (forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
$cgmapMo :: forall s (m :: * -> *).
(Data s, MonadPlus m) =>
(forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
gmapMp :: (forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
$cgmapMp :: forall s (m :: * -> *).
(Data s, MonadPlus m) =>
(forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
gmapM :: (forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
$cgmapM :: forall s (m :: * -> *).
(Data s, Monad m) =>
(forall d. Data d => d -> m d) -> S2 s -> m (S2 s)
gmapQi :: Int -> (forall d. Data d => d -> u) -> S2 s -> u
$cgmapQi :: forall s u.
Data s =>
Int -> (forall d. Data d => d -> u) -> S2 s -> u
gmapQ :: (forall d. Data d => d -> u) -> S2 s -> [u]
$cgmapQ :: forall s u. Data s => (forall d. Data d => d -> u) -> S2 s -> [u]
gmapQr :: (r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r
$cgmapQr :: forall s r r'.
Data s =>
(r' -> r -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r
gmapQl :: (r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r
$cgmapQl :: forall s r r'.
Data s =>
(r -> r' -> r) -> r -> (forall d. Data d => d -> r') -> S2 s -> r
gmapT :: (forall b. Data b => b -> b) -> S2 s -> S2 s
$cgmapT :: forall s. Data s => (forall b. Data b => b -> b) -> S2 s -> S2 s
dataCast2 :: (forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (S2 s))
$cdataCast2 :: forall s (t :: * -> * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d e. (Data d, Data e) => c (t d e)) -> Maybe (c (S2 s))
dataCast1 :: (forall d. Data d => c (t d)) -> Maybe (c (S2 s))
$cdataCast1 :: forall s (t :: * -> *) (c :: * -> *).
(Data s, Typeable t) =>
(forall d. Data d => c (t d)) -> Maybe (c (S2 s))
dataTypeOf :: S2 s -> DataType
$cdataTypeOf :: forall s. Data s => S2 s -> DataType
toConstr :: S2 s -> Constr
$ctoConstr :: forall s. Data s => S2 s -> Constr
gunfold :: (forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (S2 s)
$cgunfold :: forall s (c :: * -> *).
Data s =>
(forall b r. Data b => c (b -> r) -> c r)
-> (forall r. r -> c r) -> Constr -> c (S2 s)
gfoldl :: (forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> S2 s -> c (S2 s)
$cgfoldl :: forall s (c :: * -> *).
Data s =>
(forall d b. Data d => c (d -> b) -> d -> c b)
-> (forall g. g -> c g) -> S2 s -> c (S2 s)
$cp1Data :: forall s. Data s => Typeable (S2 s)
Data, (forall x. S2 s -> Rep (S2 s) x)
-> (forall x. Rep (S2 s) x -> S2 s) -> Generic (S2 s)
forall x. Rep (S2 s) x -> S2 s
forall x. S2 s -> Rep (S2 s) x
forall a.
(forall x. a -> Rep a x) -> (forall x. Rep a x -> a) -> Generic a
forall s x. Rep (S2 s) x -> S2 s
forall s x. S2 s -> Rep (S2 s) x
$cto :: forall s x. Rep (S2 s) x -> S2 s
$cfrom :: forall s x. S2 s -> Rep (S2 s) x
Generic)

deriving instance {-# OVERLAPPING #-} Data a => ToJson (S2 a)
deriving instance {-# OVERLAPPING #-} Data a => ToXml (S2 a)

instance (Morphism cid
            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 sign_symbol1 symbol1 proof_tree1
            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 sign_symbol2 symbol2 proof_tree2
         , Category sign1 morphism1, Ord sign_symbol1, GetRange sign_symbol1, Data sentence2)
    => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1
       sign_symbol1 where

{- one has to take care about signature and morphisms
and translate them to targetLogic
we get a Maybe sign/morphism -}

 map_sen :: SpanDomain cid
-> morphism1 -> S2 sentence2 -> Result (S2 sentence2)
map_sen (SpanDomain cid :: cid
cid) mor1 :: morphism1
mor1 (S2 sen :: sentence2
sen) =
                        case cid -> morphism1 -> Maybe morphism2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> morphism1 -> Maybe morphism2
morMap_morphism cid
cid morphism1
mor1 of
                           Just mor2 :: morphism2
mor2 -> (sentence2 -> S2 sentence2)
-> Result sentence2 -> Result (S2 sentence2)
forall (f :: * -> *) a b. Functor f => (a -> b) -> f a -> f b
fmap sentence2 -> S2 sentence2
forall s. s -> S2 s
S2 (Result sentence2 -> Result (S2 sentence2))
-> Result sentence2 -> Result (S2 sentence2)
forall a b. (a -> b) -> a -> b
$
                               lid2 -> morphism2 -> sentence2 -> Result sentence2
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> sentence -> Result sentence
map_sen (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid2
morTargetLogic cid
cid) morphism2
mor2 sentence2
sen
                           Nothing -> SpanDomain cid -> String -> Result (S2 sentence2)
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail (cid -> SpanDomain cid
forall cid. cid -> SpanDomain cid
SpanDomain cid
cid) "map_sen"
 simplify_sen :: SpanDomain cid -> sign1 -> S2 sentence2 -> S2 sentence2
simplify_sen (SpanDomain cid :: cid
cid) sigma :: sign1
sigma (S2 sen :: sentence2
sen) =
                       case cid -> sign1 -> Maybe sign2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> sign1 -> Maybe sign2
morMap_sign cid
cid sign1
sigma of
                          Just sigma2 :: sign2
sigma2 -> sentence2 -> S2 sentence2
forall s. s -> S2 s
S2 (sentence2 -> S2 sentence2) -> sentence2 -> S2 sentence2
forall a b. (a -> b) -> a -> b
$
                              lid2 -> sign2 -> sentence2 -> sentence2
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> sentence -> sentence
simplify_sen (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid2
morTargetLogic cid
cid) sign2
sigma2 sentence2
sen
                          Nothing -> String -> S2 sentence2
forall a. HasCallStack => String -> a
error "simplify_sen"
 print_named :: SpanDomain cid -> Named (S2 sentence2) -> Doc
print_named (SpanDomain cid :: cid
cid) = lid2 -> Named sentence2 -> Doc
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> Named sentence -> Doc
print_named (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid2
morTargetLogic cid
cid)
     (Named sentence2 -> Doc)
-> (Named (S2 sentence2) -> Named sentence2)
-> Named (S2 sentence2)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (S2 sentence2 -> sentence2)
-> Named (S2 sentence2) -> Named sentence2
forall s t a. (s -> t) -> SenAttr s a -> SenAttr t a
mapNamed S2 sentence2 -> sentence2
forall s. S2 s -> s
sentence2
 sym_of :: SpanDomain cid -> sign1 -> [Set sign_symbol1]
sym_of (SpanDomain cid :: cid
cid) = lid1 -> sign1 -> [Set sign_symbol1]
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> sign -> [Set symbol]
sym_of (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 symmap_of :: SpanDomain cid -> morphism1 -> EndoMap sign_symbol1
symmap_of (SpanDomain cid :: cid
cid) = lid1 -> morphism1 -> EndoMap sign_symbol1
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> morphism -> EndoMap symbol
symmap_of (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 sym_name :: SpanDomain cid -> sign_symbol1 -> Id
sym_name (SpanDomain cid :: cid
cid) = lid1 -> sign_symbol1 -> Id
forall lid sentence sign morphism symbol.
Sentences lid sentence sign morphism symbol =>
lid -> symbol -> Id
sym_name (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)

instance (Morphism cid
            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 sign_symbol1 symbol1 proof_tree1
            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 sign_symbol2 symbol2 proof_tree2
         , Ord symbol1, GetRange symbol1, Pretty symbol1, Typeable symbol1, Data sentence2)
        => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () ()
           sign1 morphism1 sign_symbol1 symbol1 where
 ensures_amalgamability :: SpanDomain cid
-> ([CASLAmalgOpt], Gr sign1 (Int, morphism1), [(Int, morphism1)],
    Gr String String)
-> Result Amalgamates
ensures_amalgamability l :: SpanDomain cid
l _ = SpanDomain cid -> String -> Result Amalgamates
forall lid (m :: * -> *) a.
(Language lid, MonadFail m) =>
lid -> String -> m a
statFail SpanDomain cid
l "ensures_amalgamability"
 symbol_to_raw :: SpanDomain cid -> sign_symbol1 -> symbol1
symbol_to_raw (SpanDomain cid :: cid
cid) = lid1 -> sign_symbol1 -> symbol1
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
symbol_to_raw (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 id_to_raw :: SpanDomain cid -> Id -> symbol1
id_to_raw (SpanDomain cid :: cid
cid) = lid1 -> Id -> symbol1
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 -> Id -> raw_symbol
id_to_raw (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 matches :: SpanDomain cid -> sign_symbol1 -> symbol1 -> Bool
matches (SpanDomain cid :: cid
cid) = lid1 -> sign_symbol1 -> symbol1 -> 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 (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 empty_signature :: SpanDomain cid -> sign1
empty_signature (SpanDomain cid :: cid
cid) = lid1 -> sign1
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 (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 signature_union :: SpanDomain cid -> sign1 -> sign1 -> Result sign1
signature_union (SpanDomain cid :: cid
cid) = lid1 -> sign1 -> sign1 -> Result sign1
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 (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 final_union :: SpanDomain cid -> sign1 -> sign1 -> Result sign1
final_union (SpanDomain cid :: cid
cid) = lid1 -> sign1 -> sign1 -> Result sign1
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 (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 morphism_union :: SpanDomain cid -> morphism1 -> morphism1 -> Result morphism1
morphism_union (SpanDomain cid :: cid
cid) = lid1 -> morphism1 -> morphism1 -> Result morphism1
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 -> morphism -> morphism -> Result morphism
morphism_union (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 is_subsig :: SpanDomain cid -> sign1 -> sign1 -> Bool
is_subsig (SpanDomain cid :: cid
cid) = lid1 -> sign1 -> sign1 -> 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 (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 subsig_inclusion :: SpanDomain cid -> sign1 -> sign1 -> Result morphism1
subsig_inclusion (SpanDomain cid :: cid
cid) = lid1 -> sign1 -> sign1 -> Result morphism1
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
subsig_inclusion (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 generated_sign :: SpanDomain cid -> Set sign_symbol1 -> sign1 -> Result morphism1
generated_sign (SpanDomain cid :: cid
cid) = lid1 -> Set sign_symbol1 -> sign1 -> Result morphism1
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 (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 cogenerated_sign :: SpanDomain cid -> Set sign_symbol1 -> sign1 -> Result morphism1
cogenerated_sign (SpanDomain cid :: cid
cid) = lid1 -> Set sign_symbol1 -> sign1 -> Result morphism1
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 (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 is_transportable :: SpanDomain cid -> morphism1 -> Bool
is_transportable (SpanDomain cid :: cid
cid) = lid1 -> morphism1 -> 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 -> morphism -> Bool
is_transportable (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
 is_injective :: SpanDomain cid -> morphism1 -> Bool
is_injective (SpanDomain cid :: cid
cid) = lid1 -> morphism1 -> 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 -> morphism -> Bool
is_injective (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)

instance (SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2)
         => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) where
            top :: SublogicsPair sublogics1 sublogics2
top = sublogics1 -> sublogics2 -> SublogicsPair sublogics1 sublogics2
forall a b. a -> b -> SublogicsPair a b
SublogicsPair sublogics1
forall l. SemiLatticeWithTop l => l
top sublogics2
forall l. SemiLatticeWithTop l => l
top
            lub :: SublogicsPair sublogics1 sublogics2
-> SublogicsPair sublogics1 sublogics2
-> SublogicsPair sublogics1 sublogics2
lub (SublogicsPair x1 :: sublogics1
x1 y1 :: sublogics2
y1) (SublogicsPair x2 :: sublogics1
x2 y2 :: sublogics2
y2) =
                sublogics1 -> sublogics2 -> SublogicsPair sublogics1 sublogics2
forall a b. a -> b -> SublogicsPair a b
SublogicsPair (sublogics1 -> sublogics1 -> sublogics1
forall l. SemiLatticeWithTop l => l -> l -> l
lub sublogics1
x1 sublogics1
x2) (sublogics2 -> sublogics2 -> sublogics2
forall l. SemiLatticeWithTop l => l -> l -> l
lub sublogics2
y1 sublogics2
y2)

instance {-# OVERLAPS #-} (SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2)
  => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) where
  minSublogic :: S2 sentence2 -> SublogicsPair sublogics1 sublogics2
minSublogic (S2 sen2 :: sentence2
sen2) = sublogics1 -> sublogics2 -> SublogicsPair sublogics1 sublogics2
forall a b. a -> b -> SublogicsPair a b
SublogicsPair sublogics1
forall l. SemiLatticeWithTop l => l
top (sentence2 -> sublogics2
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic sentence2
sen2)

{- just a dummy implementation, it should be the sublogic of sen2 in J
paired with its image through morMapSublogicSen? -}

instance {-# OVERLAPS #-} (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
         => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha where
  minSublogic :: alpha -> SublogicsPair sublogics1 sublogics2
minSublogic x :: alpha
x = sublogics1 -> sublogics2 -> SublogicsPair sublogics1 sublogics2
forall a b. a -> b -> SublogicsPair a b
SublogicsPair (alpha -> sublogics1
forall sublogic item. MinSublogic sublogic item => item -> sublogic
minSublogic alpha
x) sublogics2
forall l. SemiLatticeWithTop l => l
top

{- also should have instances of MinSublogic class for Sublogics-pair
and morphism1, sign_symbol1, sign1 this is why the wrapping is needed -}

{- instance SemiLatticeWithTop sublogics => MinSublogic sublogics () where
minSublogic _ = top -}

instance (MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2)
          => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha where
      projectSublogic :: SublogicsPair sublogics1 sublogics2 -> alpha -> alpha
projectSublogic _ x :: alpha
x = alpha
x
-- it should be used for (), morphism1, sign_symbol1, sign1

instance (MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2)
         => ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1 where
      projectSublogicM :: SublogicsPair sublogics1 sublogics2 -> sign1 -> Maybe sign1
projectSublogicM _ = sign1 -> Maybe sign1
forall a. a -> Maybe a
Just

instance (ShATermConvertible a, ShATermConvertible b)
    => ShATermConvertible (SublogicsPair a b) where
  toShATermAux :: ATermTable -> SublogicsPair a b -> IO (ATermTable, Int)
toShATermAux att0 :: ATermTable
att0 (SublogicsPair a :: a
a b :: b
b) = do
      (att1 :: ATermTable
att1, a' :: Int
a') <- ATermTable -> a -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att0 a
a
      (att2 :: ATermTable
att2, b' :: Int
b') <- ATermTable -> b -> IO (ATermTable, Int)
forall t.
ShATermConvertible t =>
ATermTable -> t -> IO (ATermTable, Int)
toShATerm' ATermTable
att1 b
b
      (ATermTable, Int) -> IO (ATermTable, Int)
forall (m :: * -> *) a. Monad m => a -> m a
return ((ATermTable, Int) -> IO (ATermTable, Int))
-> (ATermTable, Int) -> IO (ATermTable, Int)
forall a b. (a -> b) -> a -> b
$ ShATerm -> ATermTable -> (ATermTable, Int)
addATerm (String -> [Int] -> [Int] -> ShATerm
ShAAppl "SublogicsPair" [Int
a', Int
b'] []) ATermTable
att2
  fromShATermAux :: Int -> ATermTable -> (ATermTable, SublogicsPair a b)
fromShATermAux ix :: Int
ix att0 :: ATermTable
att0 = case Int -> ATermTable -> ShATerm
getShATerm Int
ix ATermTable
att0 of
    ShAAppl "SublogicsPair" [a :: Int
a, b :: Int
b] _ ->
      case Int -> ATermTable -> (ATermTable, a)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
a ATermTable
att0 of { (att1 :: ATermTable
att1, a' :: a
a') ->
      case Int -> ATermTable -> (ATermTable, b)
forall t.
ShATermConvertible t =>
Int -> ATermTable -> (ATermTable, t)
fromShATerm' Int
b ATermTable
att1 of { (att2 :: ATermTable
att2, b' :: b
b') ->
      (ATermTable
att2, a -> b -> SublogicsPair a b
forall a b. a -> b -> SublogicsPair a b
SublogicsPair a
a' b
b') }}
    u :: ShATerm
u -> String -> ShATerm -> (ATermTable, SublogicsPair a b)
forall a. String -> ShATerm -> a
fromShATermError "SublogicsPair" ShATerm
u

instance (SublogicName sublogics1, SublogicName sublogics2)
    => SublogicName (SublogicsPair sublogics1 sublogics2) where
       sublogicName :: SublogicsPair sublogics1 sublogics2 -> String
sublogicName (SublogicsPair sub1 :: sublogics1
sub1 sub2 :: sublogics2
sub2) =
           let s1 :: String
s1 = sublogics1 -> String
forall l. SublogicName l => l -> String
sublogicName sublogics1
sub1
               s2 :: String
s2 = sublogics2 -> String
forall l. SublogicName l => l -> String
sublogicName sublogics2
sub2
           in if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s1 then String
s2 else if String -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null String
s2 then String
s1 else
              String
s1 String -> ShowS
forall a. [a] -> [a] -> [a]
++ "|" String -> ShowS
forall a. [a] -> [a] -> [a]
++ String
s2

instance (MinSublogic sublogics1 ()
         , Morphism cid
            lid1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1
                sign1 morphism1 sign_symbol1 symbol1 proof_tree1
            lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
                sign2 morphism2 sign_symbol2 symbol2 proof_tree2
         , Ord proof_tree2, Show proof_tree2, Data sentence2)
         => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) ()
          (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
    where
      stability :: SpanDomain cid -> Stability
stability (SpanDomain _) = Stability
Experimental
      data_logic :: SpanDomain cid -> Maybe AnyLogic
data_logic (SpanDomain _) = Maybe AnyLogic
forall a. Maybe a
Nothing
      top_sublogic :: SpanDomain cid -> SublogicsPair sublogics1 sublogics2
top_sublogic (SpanDomain cid :: cid
cid) = sublogics1 -> sublogics2 -> SublogicsPair sublogics1 sublogics2
forall a b. a -> b -> SublogicsPair a b
SublogicsPair
        (lid1 -> sublogics1
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 -> sublogics
top_sublogic (lid1 -> sublogics1) -> lid1 -> sublogics1
forall a b. (a -> b) -> a -> b
$ cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid) (sublogics2 -> SublogicsPair sublogics1 sublogics2)
-> sublogics2 -> SublogicsPair sublogics1 sublogics2
forall a b. (a -> b) -> a -> b
$ lid2 -> sublogics2
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 -> sublogics
top_sublogic (lid2 -> sublogics2) -> lid2 -> sublogics2
forall a b. (a -> b) -> a -> b
$ cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid2
morTargetLogic cid
cid
      all_sublogics :: SpanDomain cid -> [SublogicsPair sublogics1 sublogics2]
all_sublogics (SpanDomain cid :: cid
cid) =
          [ sublogics1 -> sublogics2 -> SublogicsPair sublogics1 sublogics2
forall a b. a -> b -> SublogicsPair a b
SublogicsPair sublogics1
x sublogics2
y
          | sublogics1
x <- lid1 -> [sublogics1]
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 -> [sublogics]
all_sublogics (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
          , sublogics2
y <- lid2 -> [sublogics2]
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 -> [sublogics]
all_sublogics (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid2
morTargetLogic cid
cid) ]
      -- project_sublogic_epsilon - default implementation for now
      provers :: SpanDomain cid
-> [Prover
      sign1
      (S2 sentence2)
      morphism1
      (SublogicsPair sublogics1 sublogics2)
      proof_tree2]
provers _ = []
      cons_checkers :: SpanDomain cid
-> [ConsChecker
      sign1
      (S2 sentence2)
      (SublogicsPair sublogics1 sublogics2)
      morphism1
      proof_tree2]
cons_checkers _ = []
      conservativityCheck :: SpanDomain cid
-> [ConservativityChecker sign1 (S2 sentence2) morphism1]
conservativityCheck _ = []
      empty_proof_tree :: SpanDomain cid -> proof_tree2
empty_proof_tree (SpanDomain cid :: cid
cid) = lid2 -> proof_tree2
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 -> proof_tree
empty_proof_tree (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid2
morTargetLogic cid
cid)

-- * Morphisms

-- | Existential type for morphisms
data AnyMorphism = forall cid lid1 sublogics1
        basic_spec1 sentence1 symb_items1 symb_map_items1
        sign1 morphism1 symbol1 raw_symbol1 proof_tree1
        lid2 sublogics2
        basic_spec2 sentence2 symb_items2 symb_map_items2
        sign2 morphism2 symbol2 raw_symbol2 proof_tree2 .
      Morphism cid
                 lid1 sublogics1 basic_spec1 sentence1
                 symb_items1 symb_map_items1
                 sign1 morphism1 symbol1 raw_symbol1 proof_tree1
                 lid2 sublogics2 basic_spec2 sentence2
                 symb_items2 symb_map_items2
                 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 =>
      Morphism cid

{-
instance Eq AnyMorphism where
  Morphism cid1 == Morphism cid2 =
     constituents cid1 == constituents cid2
  -- need to be refined, using morphism translations !!!
-}

instance Show AnyMorphism where
  show :: AnyMorphism -> String
show (Morphism cid :: cid
cid) = cid -> String
forall lid. Language lid => lid -> String
language_name cid
cid
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ " : " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid1 -> String
forall lid. Language lid => lid -> String
language_name (cid -> lid1
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid1
morSourceLogic cid
cid)
    String -> ShowS
forall a. [a] -> [a] -> [a]
++ " -> " String -> ShowS
forall a. [a] -> [a] -> [a]
++ lid2 -> String
forall lid. Language lid => lid -> String
language_name (cid -> lid2
forall cid lid1 sublogics1 basic_spec1 sentence1 symb_items1
       symb_map_items1 sign1 morphism1 sign_symbol1 symbol1 proof_tree1
       lid2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2
       sign2 morphism2 sign_symbol2 symbol2 proof_tree2.
Morphism
  cid
  lid1
  sublogics1
  basic_spec1
  sentence1
  symb_items1
  symb_map_items1
  sign1
  morphism1
  sign_symbol1
  symbol1
  proof_tree1
  lid2
  sublogics2
  basic_spec2
  sentence2
  symb_items2
  symb_map_items2
  sign2
  morphism2
  sign_symbol2
  symbol2
  proof_tree2 =>
cid -> lid2
morTargetLogic cid
cid)