| Copyright | (c) Mihai Codescu, Uni Bremen 2002-2004 |
|---|---|
| License | GPLv2 or higher, see LICENSE.txt |
| Maintainer | mcodescu@informatik.uni-bremen.de |
| Stability | provisional |
| Portability | non-portable (via Logic) |
| Safe Haskell | None |
Logic.Modification
Description
Interface (type class) for comorphism modifications in Hets
- class (Language lid, Comorphism cid1 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, Comorphism cid2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4) => Modification lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4 | lid -> cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4 where
- tauSigma :: lid -> sign1 -> Result morphism2
- sourceComorphism :: lid -> cid1
- targetComorphism :: lid -> cid2
- data IdModif lid = IdModif lid
- data VerCompModif lid1 lid2 = VerCompModif lid1 lid2
- data HorCompModif lid1 lid2 = HorCompModif lid1 lid2
- data AnyModification = forall lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4 . Modification lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4 => Modification lid
- idModification :: AnyComorphism -> AnyModification
- vertCompModification :: Monad m => AnyModification -> AnyModification -> m AnyModification
- horCompModification :: Monad m => AnyModification -> AnyModification -> m AnyModification
Documentation
class (Language lid, Comorphism cid1 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2, Comorphism cid2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4) => Modification lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4 | lid -> cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4 where
comorphism modifications
Methods
tauSigma :: lid -> sign1 -> Result morphism2
sourceComorphism :: lid -> cid1
targetComorphism :: lid -> cid2
Instances
| Modification MODAL_EMBEDDING (InclComorphism CASL CASL_Sublogics) (CompComorphism CASL2Modal Modal2CASL) CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree CASL CASL_Sublogics CASLBasicSpec CASLFORMULA SYMB_ITEMS SYMB_MAP_ITEMS CASLSign CASLMor Symbol RawSymbol ProofTree | |
| Comorphism cid log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => Modification (IdModif cid) cid cid log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 | |
| (Modification lid1 cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4, Modification lid2 cid3 cid4 log5 sublogics5 basic_spec5 sentence5 symb_items5 symb_map_items5 sign5 morphism5 symbol5 raw_symbol5 proof_tree5 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6 log7 sublogics7 basic_spec7 sentence7 symb_item7 symb_map_items7 sign7 morphism7 symbol7 raw_symbol7 proof_tree7 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8) => Modification (VerCompModif lid1 lid2) cid1 cid4 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log7 sublogics7 basic_spec7 sentence7 symb_item7 symb_map_items7 sign7 morphism7 symbol7 raw_symbol7 proof_tree7 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8 | |
| (Modification lid1 cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4, Modification lid2 cid3 cid4 log5 sublogics5 basic_spec5 sentence5 symb_items5 symb_map_items5 sign5 morphism5 symbol5 raw_symbol5 proof_tree5 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6 log7 sublogics7 basic_spec7 sentence7 symb_items7 symb_map_items7 sign7 morphism7 symbol7 raw_symbol7 proof_tree7 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8, Comorphism (CompComorphism cid1 cid3) log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6, Comorphism (CompComorphism cid2 cid4) log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8) => Modification (HorCompModif lid1 lid2) (CompComorphism cid1 cid3) (CompComorphism cid2 cid4) log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8 |
data IdModif lid
Constructors
| IdModif lid |
Instances
| Show lid => Show (IdModif lid) | |
| Language lid => Language (IdModif lid) | |
| Comorphism cid log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 => Modification (IdModif cid) cid cid log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 |
data VerCompModif lid1 lid2
vertical composition of modifications
Constructors
| VerCompModif lid1 lid2 |
Instances
| (Show lid1, Show lid2) => Show (VerCompModif lid1 lid2) | |
| (Language lid1, Language lid2) => Language (VerCompModif lid1 lid2) | |
| (Modification lid1 cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4, Modification lid2 cid3 cid4 log5 sublogics5 basic_spec5 sentence5 symb_items5 symb_map_items5 sign5 morphism5 symbol5 raw_symbol5 proof_tree5 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6 log7 sublogics7 basic_spec7 sentence7 symb_item7 symb_map_items7 sign7 morphism7 symbol7 raw_symbol7 proof_tree7 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8) => Modification (VerCompModif lid1 lid2) cid1 cid4 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log7 sublogics7 basic_spec7 sentence7 symb_item7 symb_map_items7 sign7 morphism7 symbol7 raw_symbol7 proof_tree7 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8 |
data HorCompModif lid1 lid2
horizontal composition of modifications
Constructors
| HorCompModif lid1 lid2 |
Instances
| (Show lid1, Show lid2) => Show (HorCompModif lid1 lid2) | |
| (Language lid1, Language lid2) => Language (HorCompModif lid1 lid2) | |
| (Modification lid1 cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4, Modification lid2 cid3 cid4 log5 sublogics5 basic_spec5 sentence5 symb_items5 symb_map_items5 sign5 morphism5 symbol5 raw_symbol5 proof_tree5 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6 log7 sublogics7 basic_spec7 sentence7 symb_items7 symb_map_items7 sign7 morphism7 symbol7 raw_symbol7 proof_tree7 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8, Comorphism (CompComorphism cid1 cid3) log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6, Comorphism (CompComorphism cid2 cid4) log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8) => Modification (HorCompModif lid1 lid2) (CompComorphism cid1 cid3) (CompComorphism cid2 cid4) log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log6 sublogics6 basic_spec6 sentence6 symb_items6 symb_map_items6 sign6 morphism6 symbol6 raw_symbol6 proof_tree6 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log8 sublogics8 basic_spec8 sentence8 symb_items8 symb_map_items8 sign8 morphism8 symbol8 raw_symbol8 proof_tree8 |
data AnyModification
Modifications
Constructors
| forall lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4 . Modification lid cid1 cid2 log1 sublogics1 basic_spec1 sentence1 symb_items1 symb_map_items1 sign1 morphism1 symbol1 raw_symbol1 proof_tree1 log2 sublogics2 basic_spec2 sentence2 symb_items2 symb_map_items2 sign2 morphism2 symbol2 raw_symbol2 proof_tree2 log3 sublogics3 basic_spec3 sentence3 symb_items3 symb_map_items3 sign3 morphism3 symbol3 raw_symbol3 proof_tree3 log4 sublogics4 basic_spec4 sentence4 symb_items4 symb_map_items4 sign4 morphism4 symbol4 raw_symbol4 proof_tree4 => Modification lid |
Instances
vertCompModification :: Monad m => AnyModification -> AnyModification -> m AnyModification
vertical compositions of modifications
horCompModification :: Monad m => AnyModification -> AnyModification -> m AnyModification
horizontal composition of modifications