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 (overlapping instances, dynamics, existentials)
Safe Haskell	None

Logic.Grothendieck

Description

Grothendieck logic (flattening of logic graph to a single logic)

The Grothendieck logic is defined to be the heterogeneous logic over the logic graph. This will be the logic over which the data structures and algorithms for specification in-the-large are built.

This module heavily works with existential types, see http://haskell.org/hawiki/ExistentialTypes and chapter 7 of /Heterogeneous specification and the heterogeneous tool set/ (http://www.informatik.uni-bremen.de/~till/papers/habil.ps).

References:

R. Diaconescu: Grothendieck institutions J. applied categorical structures 10, 2002, p. 383-402.

T. Mossakowski: Comorphism-based Grothendieck institutions. In K. Diks, W. Rytter (Eds.), Mathematical foundations of computer science, LNCS 2420, pp. 593-604

T. Mossakowski: Heterogeneous specification and the heterogeneous tool set.

Synopsis

Documentation

data G_basic_spec Source #

Grothendieck basic specifications

Constructors

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_basic_spec lid basic_spec

Instances

Eq G_basic_spec Source #
Methods (==) :: G_basic_spec -> G_basic_spec -> Bool (/=) :: G_basic_spec -> G_basic_spec -> Bool
Ord G_basic_spec Source #
Methods compare :: G_basic_spec -> G_basic_spec -> Ordering (<) :: G_basic_spec -> G_basic_spec -> Bool (<=) :: G_basic_spec -> G_basic_spec -> Bool (>) :: G_basic_spec -> G_basic_spec -> Bool (>=) :: G_basic_spec -> G_basic_spec -> Bool max :: G_basic_spec -> G_basic_spec -> G_basic_spec min :: G_basic_spec -> G_basic_spec -> G_basic_spec
Show G_basic_spec Source #
Methods showsPrec :: Int -> G_basic_spec -> ShowS show :: G_basic_spec -> String showList :: [G_basic_spec] -> ShowS
GetRange G_basic_spec Source #
Methods getRange :: G_basic_spec -> Range Source # rangeSpan :: G_basic_spec -> [Pos] Source #
Pretty G_basic_spec Source #
Methods pretty :: G_basic_spec -> Doc Source # pretties :: [G_basic_spec] -> Doc Source #
ShATermLG G_basic_spec Source #
Methods toShATermLG :: ATermTable -> G_basic_spec -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_basic_spec) Source #

data G_sign Source #

Grothendieck signatures with an lookup index. Zero indices indicate unknown ones. It would be nice to have special (may be negative) indices for empty signatures (one for every logic).

Constructors

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_sign
Fields gSignLogic :: lid gSign :: ExtSign sign symbol gSignSelfIdx :: SigId index to lookup this `G_sign` in sign map

Instances

Eq G_sign Source #
Methods (==) :: G_sign -> G_sign -> Bool (/=) :: G_sign -> G_sign -> Bool
Ord G_sign Source #
Methods compare :: G_sign -> G_sign -> Ordering (<) :: G_sign -> G_sign -> Bool (<=) :: G_sign -> G_sign -> Bool (>) :: G_sign -> G_sign -> Bool (>=) :: G_sign -> G_sign -> Bool max :: G_sign -> G_sign -> G_sign min :: G_sign -> G_sign -> G_sign
Show G_sign Source #
Methods showsPrec :: Int -> G_sign -> ShowS show :: G_sign -> String showList :: [G_sign] -> ShowS
Pretty G_sign Source #
Methods pretty :: G_sign -> Doc Source # pretties :: [G_sign] -> Doc Source #
ShATermLG G_sign Source #
Methods toShATermLG :: ATermTable -> G_sign -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_sign) Source #
Category G_sign GMorphism Source #
Methods ide :: G_sign -> GMorphism Source # composeMorphisms :: GMorphism -> GMorphism -> Result GMorphism Source # dom :: GMorphism -> G_sign Source # cod :: GMorphism -> G_sign Source # inverse :: GMorphism -> Result GMorphism Source # isInclusion :: GMorphism -> Bool Source # legal_mor :: GMorphism -> Result () Source #

newtype SigId Source #

index for signatures

Constructors

SigId Int

Instances

Enum SigId Source #
Methods succ :: SigId -> SigId pred :: SigId -> SigId toEnum :: Int -> SigId fromEnum :: SigId -> Int enumFrom :: SigId -> [SigId] enumFromThen :: SigId -> SigId -> [SigId] enumFromTo :: SigId -> SigId -> [SigId] enumFromThenTo :: SigId -> SigId -> SigId -> [SigId]
Eq SigId Source #
Methods (==) :: SigId -> SigId -> Bool (/=) :: SigId -> SigId -> Bool
Ord SigId Source #
Methods compare :: SigId -> SigId -> Ordering (<) :: SigId -> SigId -> Bool (<=) :: SigId -> SigId -> Bool (>) :: SigId -> SigId -> Bool (>=) :: SigId -> SigId -> Bool max :: SigId -> SigId -> SigId min :: SigId -> SigId -> SigId
Show SigId Source #
Methods showsPrec :: Int -> SigId -> ShowS show :: SigId -> String showList :: [SigId] -> ShowS
ShATermConvertible SigId Source #
Methods toShATermAux :: ATermTable -> SigId -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [SigId] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, SigId) fromShATermList' :: Int -> ATermTable -> (ATermTable, [SigId])

startSigId :: SigId Source #

isHomSubGsign :: G_sign -> G_sign -> Bool Source #

prefer a faster subsignature test if possible

isSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool Source #

logicOfGsign :: G_sign -> AnyLogic Source #

symsOfGsign :: G_sign -> Set G_symbol Source #

data G_symbolmap a Source #

Grothendieck maps with symbol as keys

Constructors

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symbolmap lid (Map symbol a)

Instances

(Typeable * a, Ord a) => Eq (G_symbolmap a) Source #
Methods (==) :: G_symbolmap a -> G_symbolmap a -> Bool (/=) :: G_symbolmap a -> G_symbolmap a -> Bool
(Typeable * a, Ord a) => Ord (G_symbolmap a) Source #
Methods compare :: G_symbolmap a -> G_symbolmap a -> Ordering (<) :: G_symbolmap a -> G_symbolmap a -> Bool (<=) :: G_symbolmap a -> G_symbolmap a -> Bool (>) :: G_symbolmap a -> G_symbolmap a -> Bool (>=) :: G_symbolmap a -> G_symbolmap a -> Bool max :: G_symbolmap a -> G_symbolmap a -> G_symbolmap a min :: G_symbolmap a -> G_symbolmap a -> G_symbolmap a
Show a => Show (G_symbolmap a) Source #
Methods showsPrec :: Int -> G_symbolmap a -> ShowS show :: G_symbolmap a -> String showList :: [G_symbolmap a] -> ShowS
(Ord a, ShATermLG a) => ShATermLG (G_symbolmap a) Source #
Methods toShATermLG :: ATermTable -> G_symbolmap a -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_symbolmap a) Source #

data G_mapofsymbol a Source #

Grothendieck maps with symbol as values

Constructors

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_mapofsymbol lid (Map a symbol)

Instances

(Typeable * a, Ord a) => Eq (G_mapofsymbol a) Source #
Methods (==) :: G_mapofsymbol a -> G_mapofsymbol a -> Bool (/=) :: G_mapofsymbol a -> G_mapofsymbol a -> Bool
(Typeable * a, Ord a) => Ord (G_mapofsymbol a) Source #
Methods compare :: G_mapofsymbol a -> G_mapofsymbol a -> Ordering (<) :: G_mapofsymbol a -> G_mapofsymbol a -> Bool (<=) :: G_mapofsymbol a -> G_mapofsymbol a -> Bool (>) :: G_mapofsymbol a -> G_mapofsymbol a -> Bool (>=) :: G_mapofsymbol a -> G_mapofsymbol a -> Bool max :: G_mapofsymbol a -> G_mapofsymbol a -> G_mapofsymbol a min :: G_mapofsymbol a -> G_mapofsymbol a -> G_mapofsymbol a
Show a => Show (G_mapofsymbol a) Source #
Methods showsPrec :: Int -> G_mapofsymbol a -> ShowS show :: G_mapofsymbol a -> String showList :: [G_mapofsymbol a] -> ShowS
(Ord a, ShATermLG a) => ShATermLG (G_mapofsymbol a) Source #
Methods toShATermLG :: ATermTable -> G_mapofsymbol a -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_mapofsymbol a) Source #

data G_symbol Source #

Grothendieck symbols

Constructors

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symbol lid symbol

Instances

Eq G_symbol Source #
Methods (==) :: G_symbol -> G_symbol -> Bool (/=) :: G_symbol -> G_symbol -> Bool
Ord G_symbol Source #
Methods compare :: G_symbol -> G_symbol -> Ordering (<) :: G_symbol -> G_symbol -> Bool (<=) :: G_symbol -> G_symbol -> Bool (>) :: G_symbol -> G_symbol -> Bool (>=) :: G_symbol -> G_symbol -> Bool max :: G_symbol -> G_symbol -> G_symbol min :: G_symbol -> G_symbol -> G_symbol
Show G_symbol Source #
Methods showsPrec :: Int -> G_symbol -> ShowS show :: G_symbol -> String showList :: [G_symbol] -> ShowS
GetRange G_symbol Source #
Methods getRange :: G_symbol -> Range Source # rangeSpan :: G_symbol -> [Pos] Source #
Pretty G_symbol Source #
Methods pretty :: G_symbol -> Doc Source # pretties :: [G_symbol] -> Doc Source #
ShATermLG G_symbol Source #
Methods toShATermLG :: ATermTable -> G_symbol -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_symbol) Source #

data G_symb_items_list Source #

Grothendieck symbol lists

Constructors

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symb_items_list lid [symb_items]

Instances

Eq G_symb_items_list Source #
Methods (==) :: G_symb_items_list -> G_symb_items_list -> Bool (/=) :: G_symb_items_list -> G_symb_items_list -> Bool
Show G_symb_items_list Source #
Methods showsPrec :: Int -> G_symb_items_list -> ShowS show :: G_symb_items_list -> String showList :: [G_symb_items_list] -> ShowS
GetRange G_symb_items_list Source #
Methods getRange :: G_symb_items_list -> Range Source # rangeSpan :: G_symb_items_list -> [Pos] Source #
Pretty G_symb_items_list Source #
Methods pretty :: G_symb_items_list -> Doc Source # pretties :: [G_symb_items_list] -> Doc Source #
ShATermLG G_symb_items_list Source #
Methods toShATermLG :: ATermTable -> G_symb_items_list -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_symb_items_list) Source #

data G_symb_map_items_list Source #

Grothendieck symbol maps

Constructors

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_symb_map_items_list lid [symb_map_items]

Instances

Eq G_symb_map_items_list Source #
Methods (==) :: G_symb_map_items_list -> G_symb_map_items_list -> Bool (/=) :: G_symb_map_items_list -> G_symb_map_items_list -> Bool
Show G_symb_map_items_list Source #
Methods showsPrec :: Int -> G_symb_map_items_list -> ShowS show :: G_symb_map_items_list -> String showList :: [G_symb_map_items_list] -> ShowS
GetRange G_symb_map_items_list Source #
Methods getRange :: G_symb_map_items_list -> Range Source # rangeSpan :: G_symb_map_items_list -> [Pos] Source #
Pretty G_symb_map_items_list Source #
Methods pretty :: G_symb_map_items_list -> Doc Source # pretties :: [G_symb_map_items_list] -> Doc Source #
ShATermLG G_symb_map_items_list Source #
Methods toShATermLG :: ATermTable -> G_symb_map_items_list -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_symb_map_items_list) Source #

data G_sublogics Source #

Grothendieck sublogics

Constructors

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_sublogics lid sublogics

Instances

Eq G_sublogics Source #
Methods (==) :: G_sublogics -> G_sublogics -> Bool (/=) :: G_sublogics -> G_sublogics -> Bool
Ord G_sublogics Source #
Methods compare :: G_sublogics -> G_sublogics -> Ordering (<) :: G_sublogics -> G_sublogics -> Bool (<=) :: G_sublogics -> G_sublogics -> Bool (>) :: G_sublogics -> G_sublogics -> Bool (>=) :: G_sublogics -> G_sublogics -> Bool max :: G_sublogics -> G_sublogics -> G_sublogics min :: G_sublogics -> G_sublogics -> G_sublogics
Show G_sublogics Source #
Methods showsPrec :: Int -> G_sublogics -> ShowS show :: G_sublogics -> String showList :: [G_sublogics] -> ShowS
ShATermLG G_sublogics Source #
Methods toShATermLG :: ATermTable -> G_sublogics -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_sublogics) Source #

isSublogic :: G_sublogics -> G_sublogics -> Bool Source #

isProperSublogic :: G_sublogics -> G_sublogics -> Bool Source #

joinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics Source #

data G_morphism Source #

Homogeneous Grothendieck signature morphisms with indices. For the domain index it would be nice it showed also the emptiness.

Constructors

Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism symbol raw_symbol proof_tree => G_morphism
Fields gMorphismLogic :: lid gMorphism :: morphism gMorphismSelfIdx :: MorId lookup index in morphism map

Instances

Show G_morphism Source #
Methods showsPrec :: Int -> G_morphism -> ShowS show :: G_morphism -> String showList :: [G_morphism] -> ShowS
Pretty G_morphism Source #
Methods pretty :: G_morphism -> Doc Source # pretties :: [G_morphism] -> Doc Source #
ShATermLG G_morphism Source #
Methods toShATermLG :: ATermTable -> G_morphism -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_morphism) Source #

newtype MorId Source #

index for morphisms

Constructors

MorId Int

Instances

Enum MorId Source #
Methods succ :: MorId -> MorId pred :: MorId -> MorId toEnum :: Int -> MorId fromEnum :: MorId -> Int enumFrom :: MorId -> [MorId] enumFromThen :: MorId -> MorId -> [MorId] enumFromTo :: MorId -> MorId -> [MorId] enumFromThenTo :: MorId -> MorId -> MorId -> [MorId]
Eq MorId Source #
Methods (==) :: MorId -> MorId -> Bool (/=) :: MorId -> MorId -> Bool
Ord MorId Source #
Methods compare :: MorId -> MorId -> Ordering (<) :: MorId -> MorId -> Bool (<=) :: MorId -> MorId -> Bool (>) :: MorId -> MorId -> Bool (>=) :: MorId -> MorId -> Bool max :: MorId -> MorId -> MorId min :: MorId -> MorId -> MorId
Show MorId Source #
Methods showsPrec :: Int -> MorId -> ShowS show :: MorId -> String showList :: [MorId] -> ShowS
ShATermConvertible MorId Source #
Methods toShATermAux :: ATermTable -> MorId -> IO (ATermTable, Int) toShATermList' :: ATermTable -> [MorId] -> IO (ATermTable, Int) fromShATermAux :: Int -> ATermTable -> (ATermTable, MorId) fromShATermList' :: Int -> ATermTable -> (ATermTable, [MorId])

startMorId :: MorId Source #

mkG_morphism :: 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 -> morphism -> G_morphism Source #

lessSublogicComor :: G_sublogics -> AnyComorphism -> Bool Source #

check if sublogic fits for comorphism

data LogicGraph Source #

Logic graph

Constructors

LogicGraph

Fields

logics :: Map String AnyLogic
currentLogic :: String
currentSyntax :: Maybe IRI
currentSublogic :: Maybe G_sublogics
currentTargetBase :: Maybe (LibName, String)
sublogicBasedTheories :: Map AnyLogic SublogicBasedTheories
comorphisms :: Map String AnyComorphism
inclusions :: Map (String, String) AnyComorphism
unions :: Map (String, String) (AnyComorphism, AnyComorphism)
morphisms :: Map String AnyMorphism
modifications :: Map String AnyModification
squares :: Map (AnyComorphism, AnyComorphism) [Square]
qTATranslations :: Map String AnyComorphism
prefixes :: Map String IRI
dolOnly :: Bool

Instances

Show LogicGraph Source #
Methods showsPrec :: Int -> LogicGraph -> ShowS show :: LogicGraph -> String showList :: [LogicGraph] -> ShowS
Pretty LogicGraph Source #
Methods pretty :: LogicGraph -> Doc Source # pretties :: [LogicGraph] -> Doc Source #

setCurLogic :: String -> LogicGraph -> LogicGraph Source #

setSyntax :: Maybe IRI -> LogicGraph -> LogicGraph Source #

setCurSublogic :: Maybe G_sublogics -> LogicGraph -> LogicGraph Source #

emptyLogicGraph :: LogicGraph Source #

lookupLogic :: Monad m => String -> String -> LogicGraph -> m AnyLogic Source #

find a logic in a logic graph

lookupCurrentLogic :: Monad m => String -> LogicGraph -> m AnyLogic Source #

lookupCurrentSyntax :: Monad m => String -> LogicGraph -> m (AnyLogic, Maybe IRI) Source #

lookupCompComorphism :: Monad m => [String] -> LogicGraph -> m AnyComorphism Source #

find a comorphism composition in a logic graph

lookupComorphism :: Monad m => String -> LogicGraph -> m AnyComorphism Source #

find a comorphism in a logic graph

lookupModification :: Monad m => String -> LogicGraph -> m AnyModification Source #

find a modification in a logic graph

data GMorphism Source #

Grothendieck signature morphisms with indices

Constructors

Comorphism 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 => GMorphism
Fields gMorphismComor :: cid gMorphismSign :: ExtSign sign1 symbol1 gMorphismSignIdx :: SigId `G_sign` index of source signature gMorphismMor :: morphism2 gMorphismMorIdx :: MorId `G_morphism index of target morphism

Instances

Eq GMorphism Source #
Methods (==) :: GMorphism -> GMorphism -> Bool (/=) :: GMorphism -> GMorphism -> Bool
Ord GMorphism Source #
Methods compare :: GMorphism -> GMorphism -> Ordering (<) :: GMorphism -> GMorphism -> Bool (<=) :: GMorphism -> GMorphism -> Bool (>) :: GMorphism -> GMorphism -> Bool (>=) :: GMorphism -> GMorphism -> Bool max :: GMorphism -> GMorphism -> GMorphism min :: GMorphism -> GMorphism -> GMorphism
Show GMorphism Source #
Methods showsPrec :: Int -> GMorphism -> ShowS show :: GMorphism -> String showList :: [GMorphism] -> ShowS
Pretty GMorphism Source #
Methods pretty :: GMorphism -> Doc Source # pretties :: [GMorphism] -> Doc Source #
ShATermLG GMorphism Source #
Methods toShATermLG :: ATermTable -> GMorphism -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism) Source #
Category G_sign GMorphism Source #
Methods ide :: G_sign -> GMorphism Source # composeMorphisms :: GMorphism -> GMorphism -> Result GMorphism Source # dom :: GMorphism -> G_sign Source # cod :: GMorphism -> G_sign Source # inverse :: GMorphism -> Result GMorphism Source # isInclusion :: GMorphism -> Bool Source # legal_mor :: GMorphism -> Result () Source #

isHomogeneous :: GMorphism -> Bool Source #

data Grothendieck Source #

Constructors

Grothendieck

Instances

Show Grothendieck Source #
Methods showsPrec :: Int -> Grothendieck -> ShowS show :: Grothendieck -> String showList :: [Grothendieck] -> ShowS
Language Grothendieck Source #
Methods language_name :: Grothendieck -> String Source # description :: Grothendieck -> String Source #

gEmbed :: G_morphism -> GMorphism Source #

Embedding of homogeneous signature morphisms as Grothendieck sig mors

gEmbed2 :: G_sign -> G_morphism -> GMorphism Source #

Embedding of homogeneous signature morphisms as Grothendieck sig mors

gEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism Source #

Embedding of comorphisms as Grothendieck sig mors

homGsigDiff :: G_sign -> G_sign -> Result G_sign Source #

gsigUnion :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign Source #

heterogeneous union of two Grothendieck signatures

gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign Source #

union of a list of Grothendieck signatures

gsigManyIntersect :: LogicGraph -> [G_sign] -> Result G_sign Source #

intersection of a list of Grothendieck signatures

homogeneousMorManyUnion :: [G_morphism] -> Result G_morphism Source #

homogeneous Union of a list of morphisms

logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism Source #

inclusion between two logics

logicUnion :: LogicGraph -> AnyLogic -> AnyLogic -> Result (AnyComorphism, AnyComorphism) Source #

union to two logics

updateMorIndex :: MorId -> GMorphism -> GMorphism Source #

toG_morphism :: GMorphism -> G_morphism Source #

gSigCoerce :: LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism) Source #

ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism Source #

inclusion morphism between two Grothendieck signatures

compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism Source #

Composition of two Grothendieck signature morphisms with intermediate inclusion

findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism] Source #

Find all (composites of) comorphisms starting from a given logic

logicGraph2Graph :: LogicGraph -> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism Source #

graph representation of the logic graph

findComorphism :: Monad m => G_sublogics -> [AnyComorphism] -> m AnyComorphism Source #

finds first comorphism with a matching sublogic

isTransportable :: GMorphism -> Bool Source #

check transportability of Grothendieck signature morphisms (currently returns false for heterogeneous morphisms)

data Square Source #

Constructors

Square
Fields leftTriangle, rightTriangle :: LaxTriangle

Instances

Eq Square Source #
Methods (==) :: Square -> Square -> Bool (/=) :: Square -> Square -> Bool
Ord Square Source #
Methods compare :: Square -> Square -> Ordering (<) :: Square -> Square -> Bool (<=) :: Square -> Square -> Bool (>) :: Square -> Square -> Bool (>=) :: Square -> Square -> Bool max :: Square -> Square -> Square min :: Square -> Square -> Square
Show Square Source #
Methods showsPrec :: Int -> Square -> ShowS show :: Square -> String showList :: [Square] -> ShowS

data LaxTriangle Source #

Constructors

LaxTriangle
Fields laxModif :: AnyModification laxFst, laxSnd, laxTarget :: AnyComorphism

Instances

Eq LaxTriangle Source #
Methods (==) :: LaxTriangle -> LaxTriangle -> Bool (/=) :: LaxTriangle -> LaxTriangle -> Bool
Ord LaxTriangle Source #
Methods compare :: LaxTriangle -> LaxTriangle -> Ordering (<) :: LaxTriangle -> LaxTriangle -> Bool (<=) :: LaxTriangle -> LaxTriangle -> Bool (>) :: LaxTriangle -> LaxTriangle -> Bool (>=) :: LaxTriangle -> LaxTriangle -> Bool max :: LaxTriangle -> LaxTriangle -> LaxTriangle min :: LaxTriangle -> LaxTriangle -> LaxTriangle
Show LaxTriangle Source #
Methods showsPrec :: Int -> LaxTriangle -> ShowS show :: LaxTriangle -> String showList :: [LaxTriangle] -> ShowS

mkIdSquare :: AnyLogic -> Square Source #

mkDefSquare :: AnyComorphism -> Square Source #

mirrorSquare :: Square -> Square Source #

lookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square] Source #