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
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.
- 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
- 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
- data SpanDomain cid = SpanDomain cid
- data SublogicsPair a b = SublogicsPair a b
- newtype S2 s = S2 {
- sentence2 :: s
- data AnyMorphism = 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 Source #
Minimal complete definition
morSourceLogic, morSourceSublogic, morTargetLogic, morTargetSublogic, morMapSublogicSign, morMapSublogicSen, morMap_sign, morMap_morphism, morMap_sentence, morMap_sign_symbol
Methods
morSourceLogic :: cid -> lid1 Source #
morSourceSublogic :: cid -> sublogics1 Source #
morTargetLogic :: cid -> lid2 Source #
morTargetSublogic :: cid -> sublogics2 Source #
morMapSublogicSign :: cid -> sublogics1 -> sublogics2 Source #
morMapSublogicSen :: cid -> sublogics2 -> sublogics1 Source #
morMap_sign :: cid -> sign1 -> Maybe sign2 Source #
morMap_morphism :: cid -> morphism1 -> Maybe morphism2 Source #
morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1 Source #
morMap_sign_symbol :: cid -> sign_symbol1 -> Set sign_symbol2 Source #
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 Source # | |
data IdMorphism lid sublogics Source #
identity morphisms
Constructors
IdMorphism lid sublogics |
Instances
(Show sublogics, Show lid) => Show (IdMorphism lid sublogics) Source # | |
Logic lid sublogics basic_spec sentence symb_items symb_map_items sign morphism sign_symbol symbol proof_tree => Language (IdMorphism lid sublogics) Source # | |
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 Source # | |
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 Source #
comorphisms inducing morphisms
Minimal complete definition
Methods
indMorMap_sign :: cid -> sign2 -> Maybe sign1 Source #
indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1 Source #
data SpanDomain cid Source #
Constructors
SpanDomain cid |
Instances
Eq cid => Eq (SpanDomain cid) Source # | |
Show cid => Show (SpanDomain cid) Source # | |
Language cid => Language (SpanDomain cid) Source # | |
(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 () () Source # | |
(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) => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 Source # | |
(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) => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1 Source # | |
(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) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 Source # | |
data SublogicsPair a b Source #
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, Ord proof_tree2, Show proof_tree2) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 Source # | |
(Eq b, Eq a) => Eq (SublogicsPair a b) Source # | |
(Ord b, Ord a) => Ord (SublogicsPair a b) Source # | |
(Show b, Show a) => Show (SublogicsPair a b) Source # | |
(ShATermConvertible a, ShATermConvertible b) => ShATermConvertible (SublogicsPair a b) Source # | |
(SublogicName sublogics1, SublogicName sublogics2) => SublogicName (SublogicsPair sublogics1 sublogics2) Source # | |
(SemiLatticeWithTop sublogics1, SemiLatticeWithTop sublogics2) => SemiLatticeWithTop (SublogicsPair sublogics1 sublogics2) Source # | |
(MinSublogic sublogics1 sign1, SemiLatticeWithTop sublogics2) => ProjectSublogicM (SublogicsPair sublogics1 sublogics2) sign1 Source # | |
(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => ProjectSublogic (SublogicsPair sublogics1 sublogics2) alpha Source # | |
(MinSublogic sublogics1 alpha, SemiLatticeWithTop sublogics2) => MinSublogic (SublogicsPair sublogics1 sublogics2) alpha Source # | |
(SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2) => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) Source # | |
Instances
Eq s => Eq (S2 s) Source # | |
Data s => Data (S2 s) Source # | |
Ord s => Ord (S2 s) Source # | |
Show s => Show (S2 s) Source # | |
ShATermConvertible s => ShATermConvertible (S2 s) Source # | |
GetRange s => GetRange (S2 s) Source # | |
Pretty s => Pretty (S2 s) Source # | |
ToJson s => ToJson (S2 s) Source # | |
ToXml s => ToXml (S2 s) Source # | |
(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) => StaticAnalysis (SpanDomain cid) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 Source # | |
(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) => Sentences (SpanDomain cid) (S2 sentence2) sign1 morphism1 sign_symbol1 Source # | |
(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) => Logic (SpanDomain cid) (SublogicsPair sublogics1 sublogics2) () (S2 sentence2) () () sign1 morphism1 sign_symbol1 symbol1 proof_tree2 Source # | |
(SemiLatticeWithTop sublogics1, MinSublogic sublogics2 sentence2) => MinSublogic (SublogicsPair sublogics1 sublogics2) (S2 sentence2) Source # | |
Morphisms
data AnyMorphism Source #
Existential type for morphisms
Constructors
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 Source # | |