hets/Propositional/Morphism.hs

	Morphism.hs revision 59917a4f0a6a20f5a20bcab1f2a0a0774db56807


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
{-# OPTIONS -fallow-undecidable-instances #-}
{- |
Module      :  $Header$
Description :  Instance of class Logic for propositional logic
Copyright   :  (c) Dominik Luecke, Uni Bremen 2007
License     :  similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer  :  luecke@tzi.de
Stability   :  experimental
Portability :  portable

Definition of morphisms for propositional logic
-}
{-
  Ref.

  Till Mossakowski, Joseph Goguen, Razvan Diaconescu, Andrzej Tarlecki.
  What is a Logic?.
  In Jean-Yves Beziau (Ed.), Logica Universalis, pp. 113-@133. Birkhäuser.
  2005.
-}

module Propositional.Morphism
    (
     Morphism (..)               -- datatype for Morphisms
    ,pretty                      -- pretty printing
    ,idMor                       -- identity morphism
    ,isLegalMorphism             -- check if morhpism is ok
    ,composeMor                  -- composition
    ) where

import qualified Data.Map as Map
import qualified Data.Set as Set
import Propositional.Sign as Sign
import Common.Id
import Common.Result
import Common.Doc
import Common.DocUtils
import Data.Typeable
import Common.ATerm.Conversion

-- Maps are simple maps between elements of sets
-- By the definition of maps in Common.Lib.Map
-- these maps are injective
type PropMap = Map.Map Id Id

-- | The datatype for morphisms in propositional logic as
-- | simple injective maps of sets

data Morphism = Morphism
    {
       source :: Sign
     , target :: Sign
     , propMap :: PropMap
    } deriving (Eq, Show)

instance Pretty Morphism where
    pretty = printMorphism
instance Typeable Morphism
instance ShATermConvertible Morphism

-- | Constructs an id-morphism as the diagonal

idMor :: Sign -> Morphism
idMor a = Morphism
          { source = a
          , target = a
          , propMap = makeIdMor $ items a
          }
    where
      makeIdMor :: (Ord b) => Set.Set b -> Map.Map b b
      makeIdMor b = Set.fold (\x -> Map.insert x x) Map.empty b

-- | Determines whether a morphism is valid
-- since all maps from sets to sets are ok,
-- this value is glued to true

isLegalMorphism :: Morphism -> Bool
isLegalMorphism _ = True

-- | Composition of morphisms in propositional Logic
-- possibly there are far better way to solve this,
-- but I am jsut a n00b :)

composeMor :: Morphism -> Morphism -> Result Morphism
composeMor f g
    | fTarget /= gSource = fail "Morphisms are not composable"
    | otherwise = return Morphism
                  {
                   source = fSource
                  , target = gTarget
                  , propMap = composeHelper fassoc gMap Map.empty
                  }
    where
      fSource = source f
      fTarget = target f
      gSource = source g
      gTarget = target g
      fMap    = propMap f
      gMap    = propMap g
      fassoc  = Map.assocs fMap
      composeHelper :: (Ord a, Ord k, Ord b) => [(k, a)] -> Map.Map a b
                    -> Map.Map k b -> Map.Map k b
      composeHelper [] _ newMor          = newMor
      composeHelper ((k, a):xs) h newMor =
          case Map.lookup a h of
            Nothing -> composeHelper xs h newMor
            Just v  -> composeHelper xs h (Map.insert k v newMor)

-- | Pretty printing for Morphisms
printMorphism :: Morphism -> Doc
printMorphism m = pretty (source m) <> text "-->" <> pretty (target m)
  <> vcat (map ( \ (x, y) -> lparen <> idDoc x <> text ","
  <> idDoc y <> rparen) $ Map.assocs $ propMap m)