{- |
Module      :  ./CASL/Cycle.hs
Description :  removing sort cycles
Copyright   :  (c) Christian Maeder, DFKI GmbH 2013
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

removing sort cycles
-}

module CASL.Cycle where

import CASL.Sign
import CASL.Morphism

import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel

removeSortCycles :: Sign f e -> (Sign f e, Sort_map)
removeSortCycles :: Sign f e -> (Sign f e, Sort_map)
removeSortCycles sign :: Sign f e
sign = let
   rel :: Rel SORT
rel = Sign f e -> Rel SORT
forall f e. Sign f e -> Rel SORT
sortRel Sign f e
sign
   cs :: [Set SORT]
cs = Rel SORT -> [Set SORT]
forall a. Ord a => Rel a -> [Set a]
Rel.sccOfClosure Rel SORT
rel
   mc :: Sort_map
mc = (Set SORT -> Sort_map -> Sort_map)
-> Sort_map -> [Set SORT] -> Sort_map
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr ((\ (a :: SORT
a, s :: Set SORT
s) m :: Sort_map
m -> (SORT -> Sort_map -> Sort_map) -> Sort_map -> Set SORT -> Sort_map
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (SORT -> SORT -> Sort_map -> Sort_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
`Map.insert` SORT
a) Sort_map
m Set SORT
s)
               ((SORT, Set SORT) -> Sort_map -> Sort_map)
-> (Set SORT -> (SORT, Set SORT))
-> Set SORT
-> Sort_map
-> Sort_map
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Set SORT -> (SORT, Set SORT)
forall a. Set a -> (a, Set a)
Set.deleteFindMin) Sort_map
forall k a. Map k a
Map.empty [Set SORT]
cs
   in (Sign f e
sign
       { sortRel :: Rel SORT
sortRel = Rel SORT -> Rel SORT
forall a. Ord a => Rel a -> Rel a
Rel.irreflex (Rel SORT -> Rel SORT) -> Rel SORT -> Rel SORT
forall a b. (a -> b) -> a -> b
$ [Set SORT] -> Rel SORT -> Rel SORT
forall a. Ord a => [Set a] -> Rel a -> Rel a
Rel.collaps [Set SORT]
cs Rel SORT
rel
       , emptySortSet :: Set SORT
emptySortSet = (SORT -> SORT) -> Set SORT -> Set SORT
forall b a. Ord b => (a -> b) -> Set a -> Set b
Set.map (Sort_map -> SORT -> SORT
mapSort Sort_map
mc) (Set SORT -> Set SORT) -> Set SORT -> Set SORT
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set SORT
forall f e. Sign f e -> Set SORT
emptySortSet Sign f e
sign
       , opMap :: OpMap
opMap = (OpType -> OpType) -> OpMap -> OpMap
forall b c a.
(Ord b, Ord c) =>
(b -> c) -> MapSet a b -> MapSet a c
MapSet.map (Sort_map -> OpType -> OpType
mapOpType Sort_map
mc) (OpMap -> OpMap) -> OpMap -> OpMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> OpMap
forall f e. Sign f e -> OpMap
opMap Sign f e
sign
       , predMap :: PredMap
predMap = (PredType -> PredType) -> PredMap -> PredMap
forall b c a.
(Ord b, Ord c) =>
(b -> c) -> MapSet a b -> MapSet a c
MapSet.map (Sort_map -> PredType -> PredType
mapPredType Sort_map
mc) (PredMap -> PredMap) -> PredMap -> PredMap
forall a b. (a -> b) -> a -> b
$ Sign f e -> PredMap
forall f e. Sign f e -> PredMap
predMap Sign f e
sign
       }, Sort_map
mc)