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

data G_basic_spec = 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 => G_basic_spec lid basic_spec
data G_sign = 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 => G_sign {
- gSignLogic :: lid
- gSign :: ExtSign sign symbol
- gSignSelfIdx :: SigId
}
newtype SigId = SigId Int
startSigId :: SigId
isHomSubGsign :: G_sign -> G_sign -> Bool
isSubGsign :: LogicGraph -> G_sign -> G_sign -> Bool
logicOfGsign :: G_sign -> AnyLogic
symsOfGsign :: G_sign -> Set G_symbol
data G_symbolmap a = 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 => G_symbolmap lid (Map symbol a)
data G_mapofsymbol a = 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 => G_mapofsymbol lid (Map a symbol)
data G_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 => G_symbol lid symbol
data G_symb_items_list = 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 => G_symb_items_list lid [symb_items]
data G_symb_map_items_list = 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 => G_symb_map_items_list lid [symb_map_items]
data G_sublogics = 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 => G_sublogics lid sublogics
isSublogic :: G_sublogics -> G_sublogics -> Bool
isProperSublogic :: G_sublogics -> G_sublogics -> Bool
joinSublogics :: G_sublogics -> G_sublogics -> Maybe G_sublogics
data G_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 => G_morphism {
- gMorphismLogic :: lid
- gMorphism :: morphism
- gMorphismSelfIdx :: MorId
}
newtype MorId = MorId Int
startMorId :: MorId
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
lessSublogicComor :: G_sublogics -> AnyComorphism -> Bool
data LogicGraph = LogicGraph {
- 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
}
setCurLogic :: String -> LogicGraph -> LogicGraph
setSyntax :: Maybe IRI -> LogicGraph -> LogicGraph
setCurSublogic :: Maybe G_sublogics -> LogicGraph -> LogicGraph
emptyLogicGraph :: LogicGraph
lookupLogic :: MonadFail m => String -> String -> LogicGraph -> m AnyLogic
lookupCurrentLogic :: MonadFail m => String -> LogicGraph -> m AnyLogic
lookupCurrentSyntax :: MonadFail m => String -> LogicGraph -> m (AnyLogic, Maybe IRI)
lookupCompComorphism :: MonadFail m => [String] -> LogicGraph -> m AnyComorphism
lookupComorphism :: MonadFail m => String -> LogicGraph -> m AnyComorphism
lookupModification :: MonadFail m => String -> LogicGraph -> m AnyModification
data GMorphism = 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.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 {
- gMorphismComor :: cid
- gMorphismSign :: ExtSign sign1 symbol1
- gMorphismSignIdx :: SigId
- gMorphismMor :: morphism2
- gMorphismMorIdx :: MorId
}
isHomogeneous :: GMorphism -> Bool
data Grothendieck = Grothendieck
gEmbed :: G_morphism -> GMorphism
gEmbed2 :: G_sign -> G_morphism -> GMorphism
gEmbedComorphism :: AnyComorphism -> G_sign -> Result GMorphism
homGsigDiff :: G_sign -> G_sign -> Result G_sign
gsigUnion :: LogicGraph -> Bool -> G_sign -> G_sign -> Result G_sign
gsigManyUnion :: LogicGraph -> [G_sign] -> Result G_sign
gsigManyIntersect :: LogicGraph -> [G_sign] -> Result G_sign
homogeneousMorManyUnion :: [G_morphism] -> Result G_morphism
logicInclusion :: LogicGraph -> AnyLogic -> AnyLogic -> Result AnyComorphism
logicUnion :: LogicGraph -> AnyLogic -> AnyLogic -> Result (AnyComorphism, AnyComorphism)
updateMorIndex :: MorId -> GMorphism -> GMorphism
toG_morphism :: GMorphism -> G_morphism
gSigCoerce :: LogicGraph -> G_sign -> AnyLogic -> Result (G_sign, AnyComorphism)
ginclusion :: LogicGraph -> G_sign -> G_sign -> Result GMorphism
compInclusion :: LogicGraph -> GMorphism -> GMorphism -> Result GMorphism
findComorphismPaths :: LogicGraph -> G_sublogics -> [AnyComorphism]
logicGraph2Graph :: LogicGraph -> Graph (G_sublogics, Maybe AnyComorphism) AnyComorphism
findComorphism :: MonadFail m => G_sublogics -> [AnyComorphism] -> m AnyComorphism
isTransportable :: GMorphism -> Bool
data Square = Square {
- leftTriangle, rightTriangle :: LaxTriangle
}
data LaxTriangle = LaxTriangle {
- laxModif :: AnyModification
- laxFst, laxSnd, laxTarget :: AnyComorphism
}
mkIdSquare :: AnyLogic -> Square
mkDefSquare :: AnyComorphism -> Square
mirrorSquare :: Square -> Square
lookupSquare :: AnyComorphism -> AnyComorphism -> LogicGraph -> Result [Square]

Documentation

data G_basic_spec Source #

Grothendieck basic specifications

Constructors

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 => G_basic_spec lid basic_spec

Instances

Instances details

Eq G_basic_spec Source #
Instance details Defined in Logic.Grothendieck Methods (==) :: G_basic_spec -> G_basic_spec -> Bool (/=) :: G_basic_spec -> G_basic_spec -> Bool
Ord G_basic_spec Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> G_basic_spec -> ShowS show :: G_basic_spec -> String showList :: [G_basic_spec] -> ShowS
GetRange G_basic_spec Source #
Instance details Defined in Logic.Grothendieck Methods getRange :: G_basic_spec -> Range Source # rangeSpan :: G_basic_spec -> [Pos] Source #
Pretty G_basic_spec Source #
Instance details Defined in Logic.Grothendieck Methods pretty :: G_basic_spec -> Doc Source # pretties :: [G_basic_spec] -> Doc Source #
ShATermLG G_basic_spec Source #
Instance details Defined in ATC.Grothendieck 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

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 => G_sign
Fields gSignLogic :: lid gSign :: ExtSign sign symbol gSignSelfIdx :: SigId index to lookup this `G_sign` in sign map

Instances

Instances details

Eq G_sign Source #
Instance details Defined in Logic.Grothendieck Methods (==) :: G_sign -> G_sign -> Bool (/=) :: G_sign -> G_sign -> Bool
Ord G_sign Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> G_sign -> ShowS show :: G_sign -> String showList :: [G_sign] -> ShowS
Pretty G_sign Source #
Instance details Defined in Logic.Grothendieck Methods pretty :: G_sign -> Doc Source # pretties :: [G_sign] -> Doc Source #
ShATermLG G_sign Source #
Instance details Defined in ATC.Grothendieck Methods toShATermLG :: ATermTable -> G_sign -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, G_sign) Source #
Category G_sign GMorphism Source #
Instance details Defined in Logic.Grothendieck 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

Instances details

Enum SigId Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods (==) :: SigId -> SigId -> Bool (/=) :: SigId -> SigId -> Bool
Ord SigId Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> SigId -> ShowS show :: SigId -> String showList :: [SigId] -> ShowS
ShATermConvertible SigId Source #
Instance details Defined in Logic.Grothendieck 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

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 => G_symbolmap lid (Map symbol a)

Instances

Instances details

(Typeable a, Ord a) => Eq (G_symbolmap a) Source #
Instance details Defined in Logic.Grothendieck Methods (==) :: G_symbolmap a -> G_symbolmap a -> Bool (/=) :: G_symbolmap a -> G_symbolmap a -> Bool
(Typeable a, Ord a) => Ord (G_symbolmap a) Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in ATC.Grothendieck 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

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 => G_mapofsymbol lid (Map a symbol)

Instances

Instances details

(Typeable a, Ord a) => Eq (G_mapofsymbol a) Source #
Instance details Defined in Logic.Grothendieck Methods (==) :: G_mapofsymbol a -> G_mapofsymbol a -> Bool (/=) :: G_mapofsymbol a -> G_mapofsymbol a -> Bool
(Typeable a, Ord a) => Ord (G_mapofsymbol a) Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in ATC.Grothendieck 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

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 => G_symbol lid symbol

Instances

Instances details

Eq G_symbol Source #
Instance details Defined in Logic.Grothendieck Methods (==) :: G_symbol -> G_symbol -> Bool (/=) :: G_symbol -> G_symbol -> Bool
Ord G_symbol Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> G_symbol -> ShowS show :: G_symbol -> String showList :: [G_symbol] -> ShowS
GetRange G_symbol Source #
Instance details Defined in Logic.Grothendieck Methods getRange :: G_symbol -> Range Source # rangeSpan :: G_symbol -> [Pos] Source #
Pretty G_symbol Source #
Instance details Defined in Logic.Grothendieck Methods pretty :: G_symbol -> Doc Source # pretties :: [G_symbol] -> Doc Source #
ShATermLG G_symbol Source #
Instance details Defined in ATC.Grothendieck 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

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 => G_symb_items_list lid [symb_items]

Instances

Instances details

Eq G_symb_items_list Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods getRange :: G_symb_items_list -> Range Source # rangeSpan :: G_symb_items_list -> [Pos] Source #
Pretty G_symb_items_list Source #
Instance details Defined in Logic.Grothendieck Methods pretty :: G_symb_items_list -> Doc Source # pretties :: [G_symb_items_list] -> Doc Source #
ShATermLG G_symb_items_list Source #
Instance details Defined in ATC.Grothendieck 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

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 => G_symb_map_items_list lid [symb_map_items]

Instances

Instances details

Eq G_symb_map_items_list Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods getRange :: G_symb_map_items_list -> Range Source # rangeSpan :: G_symb_map_items_list -> [Pos] Source #
Pretty G_symb_map_items_list Source #
Instance details Defined in Logic.Grothendieck Methods pretty :: G_symb_map_items_list -> Doc Source # pretties :: [G_symb_map_items_list] -> Doc Source #
ShATermLG G_symb_map_items_list Source #
Instance details Defined in ATC.Grothendieck 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

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 => G_sublogics lid sublogics

Instances

Instances details

Eq G_sublogics Source #
Instance details Defined in Logic.Grothendieck Methods (==) :: G_sublogics -> G_sublogics -> Bool (/=) :: G_sublogics -> G_sublogics -> Bool
Ord G_sublogics Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> G_sublogics -> ShowS show :: G_sublogics -> String showList :: [G_sublogics] -> ShowS
ShATermLG G_sublogics Source #
Instance details Defined in ATC.Grothendieck 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

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 => G_morphism
Fields gMorphismLogic :: lid gMorphism :: morphism gMorphismSelfIdx :: MorId lookup index in morphism map

Instances

Instances details

Show G_morphism Source #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> G_morphism -> ShowS show :: G_morphism -> String showList :: [G_morphism] -> ShowS
Pretty G_morphism Source #
Instance details Defined in Logic.Grothendieck Methods pretty :: G_morphism -> Doc Source # pretties :: [G_morphism] -> Doc Source #
ShATermLG G_morphism Source #
Instance details Defined in ATC.Grothendieck 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

Instances details

Enum MorId Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods (==) :: MorId -> MorId -> Bool (/=) :: MorId -> MorId -> Bool
Ord MorId Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> MorId -> ShowS show :: MorId -> String showList :: [MorId] -> ShowS
ShATermConvertible MorId Source #
Instance details Defined in Logic.Grothendieck 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

Instances details

Show LogicGraph Source #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> LogicGraph -> ShowS show :: LogicGraph -> String showList :: [LogicGraph] -> ShowS
Pretty LogicGraph Source #
Instance details Defined in Logic.Grothendieck 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 :: MonadFail m => String -> String -> LogicGraph -> m AnyLogic Source #

find a logic in a logic graph

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

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

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

find a comorphism composition in a logic graph

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

find a comorphism in a logic graph

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

find a modification in a logic graph

data GMorphism Source #

Grothendieck signature morphisms with indices

Constructors

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

Instances details

Eq GMorphism Source #
Instance details Defined in Logic.Grothendieck Methods (==) :: GMorphism -> GMorphism -> Bool (/=) :: GMorphism -> GMorphism -> Bool
Ord GMorphism Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> GMorphism -> ShowS show :: GMorphism -> String showList :: [GMorphism] -> ShowS
Pretty GMorphism Source #
Instance details Defined in Logic.Grothendieck Methods pretty :: GMorphism -> Doc Source # pretties :: [GMorphism] -> Doc Source #
ShATermLG GMorphism Source #
Instance details Defined in ATC.Grothendieck Methods toShATermLG :: ATermTable -> GMorphism -> IO (ATermTable, Int) Source # fromShATermLG :: LogicGraph -> Int -> ATermTable -> (ATermTable, GMorphism) Source #
Category G_sign GMorphism Source #
Instance details Defined in Logic.Grothendieck 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

Instances details

Show Grothendieck Source #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> Grothendieck -> ShowS show :: Grothendieck -> String showList :: [Grothendieck] -> ShowS
Language Grothendieck Source #
Instance details Defined in Logic.Grothendieck 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 compositions of comorphisms starting from a give logic | use wheted graph of logics to optimize search

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

graph representation of the logic graph

findComorphism :: MonadFail 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

Instances details

Eq Square Source #
Instance details Defined in Logic.Grothendieck Methods (==) :: Square -> Square -> Bool (/=) :: Square -> Square -> Bool
Ord Square Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck Methods showsPrec :: Int -> Square -> ShowS show :: Square -> String showList :: [Square] -> ShowS

data LaxTriangle Source #

Constructors

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

Instances

Instances details

Eq LaxTriangle Source #
Instance details Defined in Logic.Grothendieck Methods (==) :: LaxTriangle -> LaxTriangle -> Bool (/=) :: LaxTriangle -> LaxTriangle -> Bool
Ord LaxTriangle Source #
Instance details Defined in Logic.Grothendieck 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 #
Instance details Defined in Logic.Grothendieck 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 #