Changeset 12653

Timestamp:

16.10.2009 01:57:16 (5 months ago)

Author:

mkhl

Message:

Document and refactor Morphism.

Location:

trunk/Maude

Files:

• Logic_Maude.hs (modified) (1 diff)
• Maude2DG.hs (modified) (3 diffs)
• Morphism.hs (modified) (9 diffs)

trunk/Maude/Logic_Maude.hs

@@ -72 +72 @@
     -- sentences --
     is_of_sign Maude = flip Sign.includesSentence
-    map_sen Maude = Morphism.mapSentence
+    map_sen Maude = Morphism.translateSentence
     simplify_sen Maude = Sign.simplifySentence
     -- parse_sentence Maude = Nothing

trunk/Maude/Maude2DG.hs

@@ -338 +338 @@
          where (tok, tim', morph, _, dg') = processModExp tim Map.empty dg modExp
                (_, _, fs, _, _) = fromJust $ Map.lookup tok tim'
-               fs' = renameSorts morph fs
+               fs' = translateSorts morph fs
                morph' = qualifySorts morph (HasName.getName sort) fs'
                toks' = (HasName.getName sort, tok, fs') : toks
@@ -357 +357 @@
                            (n1, _, ss1, _, _) = fromJust $ Map.lookup tok1 tim2
                            (n2, _, ss2, _, _) = fromJust $ Map.lookup tok2 tim2
-                           ss1' = renameSorts morph1 ss1
-                           ss2' = renameSorts morph1 ss2
+                           ss1' = translateSorts morph1 ss1
+                           ss2' = translateSorts morph1 ss2
                            sg1 = target morph1
                            sg2 = target morph2
@@ -443 +443 @@
               morph'' = setTarget usg morph'
 morphismView name p ss (n, th, morph, rnms, False) morph1 =
-                         (name, morph4, vmorph', n, [(p, th, getNewSorts ss morph)])
+                         (name, morph4, vmorph', n, [(p, th, translateSorts morph ss)])
         where rnms' = qualifyRenamings2 p rnms
               morph2 = applyRenamings morph1 rnms'

trunk/Maude/Morphism.hs

@@ -13 +13 @@
 
 module Maude.Morphism (
+    -- * Types
+    -- ** The Morphism type
     Morphism(..),
+    -- ** Auxiliary type
     SortMap,
     OpMap,
-    applyRenamings,
+    -- * Construction
     fromSignRenamings,
     fromSignsRenamings,
-    symbolMap,
     empty,
     identity,
+    inclusion,
+    -- * Combination
+    inverse,
+    union,
+    compose,
+    -- * Testing
     isIdentity,
-    inclusion,
-    inverse,
-    compose,
+    isInclusion,
     isLegal,
-    isInclusion,
-    mapSentence,
-    renameSorts,
-    union,
+    -- * Conversion
+    symbolMap,
+    -- * Modification
     setTarget,
     qualifySorts,
+    applyRenamings,
     extendWithSortRenaming,
-    getNewSorts
+    -- * Application
+    translateSentence,
+    translateSorts,
 ) where
 
@@ -59 +67 @@
 import Common.DocUtils (Pretty(..))
 
+-- * Types
+
+-- ** Auxiliary types
 
 type SortMap = SymbolMap
 type OpMap = SymbolMap
 type LabelMap = SymbolMap
+
+-- ** The Morphism type
 
 data Morphism = Morphism {
@@ -72 +85 @@
     } deriving (Show, Ord, Eq)
 
+-- ** 'Morphism' instances
 
 instance Pretty Morphism where
     pretty mor = let
-            pr'pair txt left right = hsep
-                [txt, pretty left, text "to", pretty right]
-            pr'ops src tgt = pr'pair (text "op") src (getName tgt)
-            pr'map fun = vcat . map (uncurry fun) . Map.toList
-            smap = pr'map (pr'pair $ text "sort") $ sortMap mor
-            omap = pr'map pr'ops $ opMap mor
-            lmap = pr'map (pr'pair $ text "label") $ labelMap mor
+        pr'pair txt left right = hsep 
+            [txt, pretty left, text "to", pretty right]
+        pr'ops src tgt = pr'pair (text "op") src (getName tgt)
+        pr'map fun = vcat . map (uncurry fun) . Map.toList
+        smap = pr'map (pr'pair $ text "sort") $ sortMap mor
+        omap = pr'map pr'ops $ opMap mor
+        lmap = pr'map (pr'pair $ text "label") $ labelMap mor
         in vcat [ smap, omap, lmap ]
-        -- text "\n\nTarget:" <$$> pretty $ target mor
-
+
+-- * Helper functions
+
+-- ** to modify Morphisms
 
 -- mapSource :: (Sign -> Sign) -> Morphism -> Morphism
@@ -91 +107 @@
 mapTarget func mor = mor { target = func $ target mor }
 
-mapSortMap  :: (SymbolMap -> SymbolMap) -> Morphism -> Morphism
+mapSortMap  :: (SortMap -> SortMap)   -> Morphism -> Morphism
 mapSortMap  func mor = mor { sortMap  = func $ sortMap  mor }
-mapOpMap    :: (SymbolMap -> SymbolMap) -> Morphism -> Morphism
+mapOpMap    :: (OpMap -> OpMap)       -> Morphism -> Morphism
 mapOpMap    func mor = mor { opMap    = func $ opMap    mor }
-mapLabelMap :: (SymbolMap -> SymbolMap) -> Morphism -> Morphism
+mapLabelMap :: (LabelMap -> LabelMap) -> Morphism -> Morphism
 mapLabelMap func mor = mor { labelMap = func $ labelMap mor }
 
-
--- | Separate Operator and other Renamings.
-partitionRenamings :: [Renaming] -> ([Renaming], [Renaming])
-partitionRenamings = let
-        is'op renaming = case renaming of
-            OpRenaming1 _ _ -> True
-            OpRenaming2 _ _ _ _ -> True
-            _ -> False
-    in partition is'op
-
+-- ** to handle Renamings
+
+-- TODO: Handle Attrs in Op Renamings.
 renamingSymbolsMaybe :: Renaming -> Maybe (Symbol, Symbol)
 renamingSymbolsMaybe rename = case rename of
@@ -114 +123 @@
     OpRenaming1 src (To tgt _) -> Just (asSymbol src, asSymbol tgt)
     OpRenaming2 src dom cod (To tgt _) -> let
-            src' = getName src
-            tgt' = getName tgt
-            dom' = map asSymbol dom
-            cod' = asSymbol cod
-        in Just (Operator src' dom' cod', Operator tgt' dom' cod')
+        src' = Op src dom cod []
+        tgt' = Op tgt dom cod []
+        in Just (asSymbol src', asSymbol tgt')
     TermMap _ _ -> Nothing
 
+-- | Extract the 'Symbol's from a 'Renaming', if possible.
 renamingSymbols :: Renaming -> (Symbol, Symbol)
 renamingSymbols = fromJust . renamingSymbolsMaybe
 
-applyRenamings :: Morphism -> [Renaming] -> Morphism
-applyRenamings mor rens = let
-        (ops, rest) = partitionRenamings rens
-        add'ops  = flip (foldr applyOpRenaming) ops
-        add'rest = flip (foldr applyRenaming) rest
-    in add'rest . add'ops $ mor
-
--- | create a Morphism from an initial signature and a list of Renamings
-fromSignRenamings :: Sign -> [Renaming] -> Morphism
-fromSignRenamings = applyRenamings . identity
-
-
--- TODO: Handle Attrs in Op Renamings.
-applyOpRenaming :: Renaming -> Morphism -> Morphism
-applyOpRenaming rename = let
-        syms = renamingSymbols rename
-        add'op = mapOpMap $ uncurry Map.insert syms
-        use'op = mapTarget . uncurry Sign.renameOp syms
+-- | Separate Operator and other Renamings.
+partitionRenamings :: [Renaming] -> ([Renaming], [Renaming])
+partitionRenamings = let
+    is'op renaming = case renaming of
+        OpRenaming1 _ _ -> True
+        OpRenaming2 _ _ _ _ -> True
+        _ -> False
+    in partition is'op
+
+-- ** to apply Renamings to Morphisms
+
+-- | Insert an 'Operator' 'Renaming' into a 'Morphism'.
+-- Iff apply is True, apply the Renaming to the Morphism's target Signature.
+insertOpRenaming :: Bool -> Renaming -> Morphism -> Morphism
+insertOpRenaming apply rename = let
+    syms = renamingSymbols rename
+    add'op = mapOpMap $ uncurry Map.insert syms
+    use'op attrs = if apply
+        then mapTarget $ uncurry Sign.renameOp syms attrs
+        else id
     in case rename of
         OpRenaming1 _ (To _ attrs) -> use'op attrs . add'op
@@ -147 +157 @@
         _ -> id
 
-applyRenaming :: Renaming -> Morphism -> Morphism
-applyRenaming rename = let
-        syms = renamingSymbols rename
-        add'sort = mapSortMap $ uncurry Map.insert syms
-        use'sort = mapTarget $ uncurry Sign.renameSort syms
-        ren'sort = mapOpMap $ uncurry renameSortOpMap syms
-        add'labl = mapLabelMap $ uncurry Map.insert syms
-        use'labl = mapTarget $ uncurry Sign.renameLabel syms
+-- | Insert a non-Operator 'Renaming' into a 'Morphism'.
+-- ^ iff True, apply the Renaming to the target Sign
+insertRenaming :: Bool -> Renaming -> Morphism -> Morphism
+insertRenaming apply rename = let
+    syms = renamingSymbols rename
+    add'sort = mapSortMap $ uncurry Map.insert syms
+    use'sort = if apply
+        then mapTarget $ uncurry Sign.renameSort syms
+        else id
+    ren'sort = mapOpMap $ uncurry renameSortOpMap syms
+    add'labl = mapLabelMap $ uncurry Map.insert syms
+    use'labl = if apply 
+        then mapTarget $ uncurry Sign.renameLabel syms
+        else id
     in case rename of
         SortRenaming _ _ -> ren'sort . use'sort . add'sort
@@ -160 +176 @@
         _ -> id
 
-
--- | create a Morphism from the initial signatures and a list of Renamings
-fromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism
-fromSignsRenamings sign1 sign2 rens = let
-        (ops, rest) = partitionRenamings rens
-        add'ops  = flip (foldr insertOpRenaming) ops
-        add'rest = flip (foldr insertRenaming) rest
-        mor = inclusion sign1 sign2
-    in add'rest . add'ops $ mor
-
--- TODO: Handle Attrs in Op Renamings.
-insertOpRenaming :: Renaming -> Morphism -> Morphism
-insertOpRenaming rename = let
-        syms = renamingSymbols rename
-        add'op = mapOpMap $ uncurry Map.insert syms
-    in case rename of
-        OpRenaming1 _ _ -> add'op
-        OpRenaming2 _ _ _ _ -> add'op
-        _ -> id
-
-insertRenaming :: Renaming -> Morphism -> Morphism
-insertRenaming rename = let
-        syms = renamingSymbols rename
-        add'sort = mapSortMap $ uncurry Map.insert syms
-        ren'sort = mapOpMap $ uncurry renameSortOpMap syms
-        add'labl = mapLabelMap $ uncurry Map.insert syms
-    in case rename of
-        SortRenaming _ _ -> ren'sort . add'sort
-        LabelRenaming _ _ -> add'labl
-        _ -> id
-
 -- | Rename sorts in the profiles of an operator map.
 renameSortOpMap :: Symbol -> Symbol -> OpMap -> OpMap
 renameSortOpMap from to = Map.map $ mapSorts $ Map.singleton from to
 
--- | extract the SymbolMap of a Morphism
-symbolMap :: Morphism -> SymbolMap
-symbolMap mor = Map.unions [sortMap mor, opMap mor, labelMap mor]
-
--- | the empty Morphism
+-- | Insert 'Renaming's into a 'Morphism'.
+insertRenamings :: Bool -> Morphism -> [Renaming] -> Morphism
+insertRenamings apply mor rens = let
+    (ops, rest) = partitionRenamings rens
+    add'ops  = flip (foldr $ insertOpRenaming apply) ops
+    add'rest = flip (foldr $ insertRenaming apply) rest
+    in add'rest . add'ops $ mor
+
+-- * Construction
+
+-- | Create a 'Morphism' from an initial 'Sign'ature and a list of 'Renaming's.
+fromSignRenamings :: Sign -> [Renaming] -> Morphism
+fromSignRenamings = insertRenamings True . identity
+
+-- | Create a 'Morphism' from a pair of 'Sign'atures and a list of 'Renaming's.
+fromSignsRenamings :: Sign -> Sign -> [Renaming] -> Morphism
+fromSignsRenamings sign1 sign2 = insertRenamings False $ inclusion sign1 sign2
+
+-- | the empty 'Morphism'
 empty :: Morphism
 empty = identity Sign.empty
 
--- | the identity Morphism
+-- | the identity 'Morphism'
 identity :: Sign -> Morphism
 identity sign = inclusion sign sign
 
--- | the inclusion Morphism
+-- | the inclusion 'Morphism'
 inclusion :: Sign -> Sign -> Morphism
 inclusion src tgt = Morphism {
         source = src,
         target = tgt,
-        sortMap = Map.empty,
-        opMap = Map.empty,
+        sortMap  = Map.empty,
+        opMap    = Map.empty,
         labelMap = Map.empty
     }
 
-
--- | the inverse Morphism
+-- * Combination
+
+-- | the inverse 'Morphism'
 inverse :: Morphism -> Result Morphism
 inverse mor = let
-        invertMap = Map.foldWithKey (flip Map.insert) Map.empty
+    invertMap = Map.foldWithKey (flip Map.insert) Map.empty
     in return Morphism {
         source = target mor,
@@ -230 +230 @@
     }
 
-
--- | the composition of two Morphisms
-compose :: Morphism -> Morphism -> Result Morphism
-compose f g
-    | target f /= source g = fail
-        "target of the first and source of the second morphism are different"
-    | otherwise = let
-            -- Take SymbolMap |mp| of each Morphism.
-            -- Convert each SymbolMap to a function.
-            -- Compose those functions.
-            map'map :: (Morphism -> SymbolMap) -> Symbol -> Symbol
-            map'map mp = mapAsFunction (mp g) . mapAsFunction (mp f)
-            -- Map |x| via the composed SymbolMaps |mp| of both Morphisms.
-            -- Insert the renaming mapping into a SymbolMap.
-            insert :: (Morphism -> SymbolMap) -> Symbol -> SymbolMap -> SymbolMap
-            insert mp x = let y = map'map mp x
-                in if x == y then id else Map.insert x y
-            -- Map each symbol in |items| via the combined SymbolMaps |mp|.
-            compose'map :: (Morphism -> SymbolMap) -> (Sign -> SymbolSet) -> SymbolMap
-            compose'map mp items = if Map.null (mp g)
-                -- if the SymbolMap of |g| is empty, we use the one from |f|
-                then mp f
-                -- otherwise we start with the SymbolSet from |source f|
-                -- and construct a combined SymbolMap by applying both
-                -- SymbolMaps (from |f| and |g|) to each item in |insert|
-                else Set.fold (insert mp) Map.empty $ items (source f)
-            -- We want a morphism from |source f| to |target g|.
-            mor = inclusion (source f) (target g)
-        in return mor {
-                sortMap = compose'map sortMap getSorts,
-                opMap = compose'map opMap getOps,
-                labelMap = compose'map labelMap getLabels
-            }
-
--- | check that a Morphism is legal
-isLegal :: Morphism -> Bool
-isLegal mor = let
-        src = source mor
-        tgt = target mor
-        smap = sortMap mor
-        omap = opMap mor
-        lmap = labelMap mor
-        subset mp items = let mapped = Set.map $ mapAsFunction mp
-            in Set.isSubsetOf (mapped $ items src) $ items tgt
-        lg'source = Sign.isLegal src
-        lg'sortMap = subset smap getSorts
-        lg'opMap = subset omap getOps
-        lg'labelMap = subset lmap getLabels
-        lg'target = Sign.isLegal tgt
-    in all id [lg'source, lg'sortMap, lg'opMap, lg'labelMap, lg'target]
-
--- | check that a Morphism is the identity
-isIdentity :: Morphism -> Bool
-isIdentity mor = source mor == target mor
-
--- | check that a Morphism is an Inclusion
-isInclusion :: Morphism -> Bool
-isInclusion mor = let
-        null'sortMap  = Map.null (sortMap mor)
-        null'opMap    = Map.null (opMap mor)
-        null'labelMap = Map.null (labelMap mor)
-    in all id [null'sortMap, null'opMap, null'labelMap]
-
--- | translate a Sentence along a Morphism
-mapSentence :: Morphism -> Sentence -> Result Sentence
-mapSentence mor = let
-        smap = mapSorts (sortMap mor)
-        omap = mapOps (opMap mor)
-        lmap = mapLabels (labelMap mor)
-    in return . lmap . smap . omap
-
+-- | the union of two 'Morphism's
 union :: Morphism -> Morphism -> Morphism
-union m1 m2 = let apply func items = func (items m1) (items m2)
+union mor1 mor2 = let
+    apply func items = func (items mor1) (items mor2)
     in Morphism {
         source = apply Sign.union source,
@@ -311 +242 @@
     }
 
+-- Just a shorthand for types inside compose.
+type Extraction = Morphism -> SymbolMap
+
+-- | the composition of two 'Morphism's
+compose :: Morphism -> Morphism -> Result Morphism
+compose f g
+    | target f /= source g = fail
+        "target of the first and source of the second morphism are different"
+    | otherwise = let
+        -- Take SymbolMap |mp| of each Morphism.
+        -- Convert each SymbolMap to a function.
+        -- Compose those functions.
+        map'map :: Extraction -> Symbol -> Symbol
+        map'map mp = mapAsFunction (mp g) . mapAsFunction (mp f)
+        -- Map |x| via the composed SymbolMaps |mp| of both Morphisms.
+        -- Insert the renaming mapping into a SymbolMap.
+        insert :: Extraction -> Symbol -> SymbolMap -> SymbolMap
+        insert mp x = let y = map'map mp x
+            in if x == y then id else Map.insert x y
+        -- Map each symbol in |items| via the combined SymbolMaps |mp|.
+        compose'map :: Extraction -> (Sign -> SymbolSet) -> SymbolMap
+        compose'map mp items = if Map.null (mp g)
+            -- if the SymbolMap of |g| is empty, we use the one from |f|
+            then mp f
+            -- otherwise we start with the SymbolSet from |source f|
+            -- and construct a combined SymbolMap by applying both
+            -- SymbolMaps (from |f| and |g|) to each item in |insert|
+            else Set.fold (insert mp) Map.empty $ items (source f)
+        -- We want a morphism from |source f| to |target g|.
+        mor = inclusion (source f) (target g)
+        in return mor {
+            sortMap = compose'map sortMap getSorts,
+            opMap = compose'map opMap getOps,
+            labelMap = compose'map labelMap getLabels
+        }
+
+-- * Testing
+
+-- | True iff the 'Morphism' is the identity
+isIdentity :: Morphism -> Bool
+isIdentity mor = source mor == target mor
+
+-- | True iff the 'Morphism' is an inclusion
+isInclusion :: Morphism -> Bool
+isInclusion mor = let
+    null'sortMap  = Map.null (sortMap mor)
+    null'opMap    = Map.null (opMap mor)
+    null'labelMap = Map.null (labelMap mor)
+    in all id [null'sortMap, null'opMap, null'labelMap]
+
+-- | True iff the 'Morphism' is legal
+isLegal :: Morphism -> Bool
+isLegal mor = let
+    src = source mor
+    tgt = target mor
+    smap = sortMap mor
+    omap = opMap mor
+    lmap = labelMap mor
+    subset mp items = let mapped = Set.map $ mapAsFunction mp
+        in Set.isSubsetOf (mapped $ items src) $ items tgt
+    lg'source = Sign.isLegal src
+    lg'sortMap = subset smap getSorts
+    lg'opMap = subset omap getOps
+    lg'labelMap = subset lmap getLabels
+    lg'target = Sign.isLegal tgt
+    in all id [lg'source, lg'sortMap, lg'opMap, lg'labelMap, lg'target]
+
+-- * Conversion
+
+-- | extract the complete 'SymbolMap' of a 'Morphism'
+symbolMap :: Morphism -> SymbolMap
+symbolMap mor = Map.unions [sortMap mor, opMap mor, labelMap mor]
+
+-- * Modification
+
+-- | set a new target for a 'Morphism'
 setTarget :: Sign -> Morphism -> Morphism
-setTarget sign morph = morph {target = sign}
-
-renameSorts :: Morphism -> Symbols -> Symbols
-renameSorts = mapSorts . sortMap
-
+setTarget = mapTarget . const
+
+-- | qualify a list of 'Symbol's inside a 'Morphism'
 qualifySorts :: Morphism -> Qid -> Symbols -> Morphism
 qualifySorts mor qid syms = let
-        insert symb = Map.insert symb $ qualify qid symb
-        smap = foldr insert Map.empty syms
-        q'tgt  = mapTarget $ mapSorts smap
-        q'smap = mapSortMap $ mapSorts smap
-        x'smap = mapSortMap $ Map.union smap
+    insert symb = Map.insert symb $ qualify qid symb
+    smap = foldr insert Map.empty syms
+    q'tgt  = mapTarget $ mapSorts smap
+    q'smap = mapSortMap $ mapSorts smap
+    x'smap = mapSortMap $ Map.union smap
     in q'tgt . x'smap .  q'smap $ mor
 
--- FIXME: Code duplication!
+-- | apply a list of 'Renaming's to a 'Morphism'
+applyRenamings :: Morphism -> [Renaming] -> Morphism
+applyRenamings = insertRenamings True
+
+-- | apply a 'Sort' 'Renaming' to a 'Morphism'
 extendWithSortRenaming :: Symbol -> Symbol -> Morphism -> Morphism
 extendWithSortRenaming src tgt = let
-        add'sort = mapSortMap $ Map.insert src tgt
-        use'sort = mapTarget $ Sign.renameSort src tgt
-        ren'sort = mapOpMap $ renameSortOpMap src tgt
+    add'sort = mapSortMap $ Map.insert src tgt
+    use'sort = mapTarget $ Sign.renameSort src tgt
+    ren'sort = mapOpMap $ renameSortOpMap src tgt
     in ren'sort . use'sort . add'sort
 
-getNewSorts :: [Symbol] -> Morphism -> [Symbol]
-getNewSorts ss morph = mapSorts (sortMap morph) ss
+-- * Application
+
+-- | translate a 'Sentence' along a 'Morphism'
+translateSentence :: Morphism -> Sentence -> Result Sentence
+translateSentence mor = let
+    smap = mapSorts (sortMap mor)
+    omap = mapOps (opMap mor)
+    lmap = mapLabels (labelMap mor)
+    in return . lmap . smap . omap
+
+-- | translate 'Sort's along a 'Morphism'
+translateSorts :: (HasSorts a) => Morphism -> a -> a
+translateSorts = mapSorts . sortMap