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)
Safe Haskell	None

Logic.Morphism

Contents

Morphisms

Description

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.

Synopsis

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
- morSourceLogic :: cid -> lid1
- morSourceSublogic :: cid -> sublogics1
- morTargetLogic :: cid -> lid2
- morTargetSublogic :: cid -> sublogics2
- morMapSublogicSign :: cid -> sublogics1 -> sublogics2
- morMapSublogicSen :: cid -> sublogics2 -> sublogics1
- morMap_sign :: cid -> sign1 -> Maybe sign2
- morMap_morphism :: cid -> morphism1 -> Maybe morphism2
- morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
- morMap_sign_symbol :: cid -> sign_symbol1 -> Set sign_symbol2
data IdMorphism lid sublogics = IdMorphism lid sublogics
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
data SpanDomain cid = SpanDomain cid
data SublogicsPair a b = SublogicsPair a b
newtype S2 s = S2 {
- sentence2 :: s
}
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

Documentation

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

Methods

morSourceLogic :: cid -> lid1

morSourceSublogic :: cid -> sublogics1

morTargetLogic :: cid -> lid2

morTargetSublogic :: cid -> sublogics2

morMapSublogicSign :: cid -> sublogics1 -> sublogics2

morMapSublogicSen :: cid -> sublogics2 -> sublogics1

morMap_sign :: cid -> sign1 -> Maybe sign2

morMap_morphism :: cid -> morphism1 -> Maybe morphism2

morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1

morMap_sign_symbol :: cid -> sign_symbol1 -> Set sign_symbol2

Instances

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

data IdMorphism lid sublogics

identity morphisms

Constructors

IdMorphism lid sublogics

Instances

(Show lid, Show sublogics) => Show (IdMorphism lid sublogics)
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree => Language (IdMorphism lid sublogics)
Typeable (* -> * -> *) IdMorphism
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

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

comorphisms inducing morphisms

Methods

indMorMap_sign :: cid -> sign2 -> Maybe sign1

indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1

epsilon :: cid -> sign2 -> Maybe morphism2

data SpanDomain cid

Constructors

SpanDomain cid

Instances

Eq cid => Eq (SpanDomain cid)
Show cid => Show (SpanDomain cid)
Language cid => Language (SpanDomain cid)
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 => Syntax (SpanDomain cid) () sign_symbol1 () ()
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 => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1
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 => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1
(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) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2

data SublogicsPair a b

Constructors

SublogicsPair a b

Instances

(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) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
(Eq a, Eq b) => Eq (SublogicsPair a b)
(Ord a, Ord b) => Ord (SublogicsPair a b)
(Show a, Show b) => Show (SublogicsPair a b)
(ShATermConvertible a, ShATermConvertible b) => ShATermConvertible (SublogicsPair a b)
(SublogicName sublogics1, SublogicName sublogics2) => SublogicName (SublogicsPair sublogics1 sublogics2)
(SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2) => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2)
Typeable (* -> * -> *) SublogicsPair
(MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2) => ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1
(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha
(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha
(SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2) => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2)

newtype S2 s

Constructors

S2
Fields sentence2 :: s

Instances

Eq s => Eq (S2 s)
Data s => Data (S2 s)
Ord s => Ord (S2 s)
Show s => Show (S2 s)
ShATermConvertible s => ShATermConvertible (S2 s)
GetRange s => GetRange (S2 s)
Pretty s => Pretty (S2 s)
ToJson s => ToJson (S2 s)
ToXml s => ToXml (S2 s)
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 => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1
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 => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1
(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) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2
Typeable (* -> *) S2
(SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2) => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2)

Morphisms

data AnyMorphism

Existential type for morphisms

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

Instances

Show AnyMorphism