Hets - the Heterogeneous Tool Set

Copyright(c) Till Mossakowski and Uni Bremen 2002-2006
LicenseGPLv2 or higher, see LICENSE.txt
Maintainertill@informatik.uni-bremen.de
Stabilityprovisional
Portabilitynon-portable (overlapping instances, dynamics, existentials)
Safe HaskellNone

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 

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

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

newtype SigId Source #

index for signatures

Constructors

SigId Int 

Instances

Enum SigId Source # 
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])

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

prefer a faster subsignature test if possible

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 # 
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 # 
Pretty G_symbol 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] 

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] 

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

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

Instances

Show G_morphism Source # 

Methods

showsPrec :: Int -> G_morphism -> ShowS

show :: G_morphism -> String

showList :: [G_morphism] -> ShowS

Pretty G_morphism 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 # 
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])

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

Instances

Show LogicGraph Source # 

Methods

showsPrec :: Int -> LogicGraph -> ShowS

show :: LogicGraph -> String

showList :: [LogicGraph] -> ShowS

Pretty 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

data Grothendieck Source #

Constructors

Grothendieck 

Instances

Show Grothendieck Source # 

Methods

showsPrec :: Int -> Grothendieck -> ShowS

show :: Grothendieck -> String

showList :: [Grothendieck] -> ShowS

Language Grothendieck 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

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

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 

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