hets/Logic/Morphism.hs

	Morphism.hs revision 49744099bf207892e92973d47e43be679fe0f68d


1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
{-|

Module      :  $Header$
Copyright   :  (c) Till Mossakowski, Uni Bremen 2002-2004
Licence     :  similar to LGPL, see HetCATS/LICENCE.txt or LIZENZ.txt

Maintainer  :  hets@tzi.de
Stability   :  provisional
Portability :  non-portable (via Logic)

   Provides data structures for institution morphisms.
   These are just collections of
   functions between (some of) the types of logics.

-}

{-   References: see Logic.hs

   Todo:
   morphism modifications / representation maps
-}

module Logic.Morphism where

import Logic.Logic
import Logic.Comorphism
import Common.Lib.Set
import Data.Maybe
import Data.Dynamic
import Common.DynamicUtils
import Common.AS_Annotation (Named, mapNamedM)

class (Language cid,
       Logic lid1 sublogics1
        basic_spec1 sentence1 symb_items1 symb_map_items1
        sign1 morphism1 symbol1 raw_symbol1 proof_tree1,
       Logic 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
             | cid -> lid1, cid -> lid2

  where
    -- source and target logic and sublogic
    -- the source sublogic is the maximal one for which the comorphism works
    -- the target sublogic is the resulting one
    morSourceLogic :: cid -> lid1
    morSourceSublogic :: cid -> sublogics1
    morTargetLogic :: cid -> lid2
    morTargetSublogic :: cid -> sublogics2
    -- finer information of target sublogics corresponding to source sublogics
    morMapSublogic :: cid -> sublogics1 -> sublogics2
    -- default implementation
    morMapSublogic cid _ = targetSublogic cid
    -- the translation functions are partial
    -- because the target may be a sublanguage
    -- map_basic_spec :: cid -> basic_spec1 -> Maybe basic_spec2
    -- we do not cover theoroidal morphisms,
    --   since there are no relevant examples and they do not compose nicely
    -- no mapping of theories, since signatrures and sentences are mapped
    --   contravariantly
    morMap_sign :: cid -> sign1 -> Maybe sign2
    morMap_morphism :: cid -> morphism1 -> Maybe morphism2
    morMap_sentence :: cid -> sign1 -> sentence2 -> Maybe sentence1
          -- also covers semi-morphisms ??
          -- with no sentence translation
          -- - but these are spans!
    morMap_symbol :: cid -> symbol1 -> Set symbol2
    morConstituents :: cid -> [String]
    -- default implementation
    morConstituents cid = [language_name cid]


-- identity morphisms

data IdMorphism lid sublogics =
     IdMorphism lid sublogics deriving Show

idMorphismTc :: TyCon
idMorphismTc = mkTyCon "Logic.Morphism.IdMorphism"

instance Typeable (IdMorphism lid sub) where
  typeOf _ = mkTyConApp idMorphismTc []

instance Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree =>
         Language (IdMorphism lid sublogics) where
           language_name (IdMorphism lid sub) =
               case sublogic_names lid sub of
               [] -> error "language_name IdMorphism"
               h : _ -> "id_" ++ language_name lid ++ "." ++ h

instance Logic lid sublogics
        basic_spec sentence symb_items symb_map_items
        sign morphism symbol raw_symbol proof_tree =>
         Morphism (IdMorphism lid sublogics)
          lid sublogics
          basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree
          lid sublogics
          basic_spec sentence symb_items symb_map_items
          sign morphism symbol raw_symbol proof_tree
         where
           sourceLogic (IdMorphism lid _sub) = lid
           targetLogic (IdMorphism lid _sub) = lid
           sourceSublogic (IdMorphism _lid sub) = sub
           targetSublogic (IdMorphism _lid sub) = sub
           map_sign _ = \sigma -> Just(sigma,[])
           map_morphism _ = Just
           map_sentence _ = \_ -> Just
           map_symbol _ = single
           constituents _ = []

-- composition not needed, use lax triangles instead

-- comorphisms inducing morphisms

class 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 =>
      MorphismInducing 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
  where
    indMorMap_sign :: cid -> sign2 -> Maybe sign1
    indMorMap_morphism :: cid -> morphism2 -> Maybe morphism1
    epsilon :: cid -> sign2 -> Maybe morphism2