{- |
Module      :  ./DFOL/Colimit.hs
Description :  Signature colimits for first-order logic with dependent
               types (DFOL)
Copyright   :  (c) Kristina Sojakova, DFKI Bremen 2009
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  k.sojakova@jacobs-university.de
Stability   :  experimental
Portability :  portable

Algorithm description:

Input : graph where nodes are signatures and edges are morphisms
Output : a signature "sig" and for each input signature "sig1" a morphism
         m : sig1 -> sig

1 : Compute the transitive and symmetric closure of the relation R induced
    by the morphisms in the graph

2 : Initialize the output signature "sig" and collection of morphisms "M" to
    empty
    Initialize the set of analyzed symbols to empty

3 : For each input signature sig1 :
    3.1 : Initialize the output map "m" to empty
    3.2 : For each symbol "s" in sig1 (keeping the order in which they are
              defined) :
          3.1.1 Check if s R s' for any already analyzed symbol "s'"
          3.1.2 If yes:
                3.1.2.1 Recover from M the value "c" that s' maps to
                3.1.2.2 Update m by adding the pair (s,c)
          3.1.3 If no:
                3.1.3.1 Get the type "t" of s in sig1
                3.1.3.2 Translate t along m; call this new type "t1"
                3.1.3.3 Update sig by adding the declaration s : t1
                        (in case the name s is already contained in sig,
                        we generate a fresh name "s1" and add the declaration
                        s1 : t and pair (s,s1) to sig and m respectively.
    3.3 : Add m to M
-}

module DFOL.Colimit (
    sigColimit
  ) where

import DFOL.AS_DFOL
import DFOL.Sign
import DFOL.Morphism
import Common.Result
import Common.Id
import Common.Lib.Graph
import qualified Data.Graph.Inductive.Graph as Graph
import qualified Common.Lib.Rel as Rel
import qualified Data.Map as Map
import qualified Data.Set as Set
import qualified Data.IntMap as IntMap

-- main functions
sigColimit :: Gr Sign (Int, Morphism) -> Result (Sign, Map.Map Int Morphism)
sigColimit :: Gr Sign (Int, Morphism) -> Result (Sign, Map Int Morphism)
sigColimit gr :: Gr Sign (Int, Morphism)
gr =
  let sigs :: [LNode Sign]
sigs = Gr Sign (Int, Morphism) -> [LNode Sign]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LNode a]
Graph.labNodes Gr Sign (Int, Morphism)
gr
      rel :: Rel (Int, NAME)
rel = Gr Sign (Int, Morphism) -> Rel (Int, NAME)
computeRel Gr Sign (Int, Morphism)
gr
      (sig :: Sign
sig, maps :: IntMap (Map NAME NAME)
maps) = Sign
-> IntMap (Map NAME NAME)
-> Set (Int, NAME)
-> Rel (Int, NAME)
-> [LNode Sign]
-> (Sign, IntMap (Map NAME NAME))
addSig Sign
emptySig IntMap (Map NAME NAME)
forall a. IntMap a
IntMap.empty Set (Int, NAME)
forall a. Set a
Set.empty Rel (Int, NAME)
rel [LNode Sign]
sigs
      maps1 :: IntMap Morphism
maps1 = (Int -> Map NAME NAME -> Morphism)
-> IntMap (Map NAME NAME) -> IntMap Morphism
forall a b. (Int -> a -> b) -> IntMap a -> IntMap b
IntMap.mapWithKey (\ i :: Int
i m :: Map NAME NAME
m -> let Just sig1 :: Sign
sig1 = Gr Sign (Int, Morphism) -> Int -> Maybe Sign
forall (gr :: * -> * -> *) a b.
Graph gr =>
gr a b -> Int -> Maybe a
Graph.lab Gr Sign (Int, Morphism)
gr Int
i
                                              in Sign -> Sign -> Map NAME NAME -> Morphism
Morphism Sign
sig1 Sign
sig Map NAME NAME
m
                                )
                                IntMap (Map NAME NAME)
maps
      maps2 :: Map Int Morphism
maps2 = [(Int, Morphism)] -> Map Int Morphism
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList ([(Int, Morphism)] -> Map Int Morphism)
-> [(Int, Morphism)] -> Map Int Morphism
forall a b. (a -> b) -> a -> b
$ IntMap Morphism -> [(Int, Morphism)]
forall a. IntMap a -> [(Int, a)]
IntMap.toList IntMap Morphism
maps1
      in [Diagnosis]
-> Maybe (Sign, Map Int Morphism)
-> Result (Sign, Map Int Morphism)
forall a. [Diagnosis] -> Maybe a -> Result a
Result [] (Maybe (Sign, Map Int Morphism) -> Result (Sign, Map Int Morphism))
-> Maybe (Sign, Map Int Morphism)
-> Result (Sign, Map Int Morphism)
forall a b. (a -> b) -> a -> b
$ (Sign, Map Int Morphism) -> Maybe (Sign, Map Int Morphism)
forall a. a -> Maybe a
Just (Sign
sig, Map Int Morphism
maps2)

-- preparation for computing the colimit
addSig :: Sign -> IntMap.IntMap (Map.Map NAME NAME) -> Set.Set (Int, NAME) ->
          Rel.Rel (Int, NAME) -> [(Int, Sign)] ->
          (Sign, IntMap.IntMap (Map.Map NAME NAME))
addSig :: Sign
-> IntMap (Map NAME NAME)
-> Set (Int, NAME)
-> Rel (Int, NAME)
-> [LNode Sign]
-> (Sign, IntMap (Map NAME NAME))
addSig sig :: Sign
sig maps :: IntMap (Map NAME NAME)
maps _ _ [] = (Sign
sig, IntMap (Map NAME NAME)
maps)
addSig sig :: Sign
sig maps :: IntMap (Map NAME NAME)
maps doneSyms :: Set (Int, NAME)
doneSyms rel :: Rel (Int, NAME)
rel ((i :: Int
i, Sign ds :: [DECL]
ds) : sigs :: [LNode Sign]
sigs) =
  Sign
-> IntMap (Map NAME NAME)
-> Map NAME NAME
-> Int
-> [SDECL]
-> Set (Int, NAME)
-> Rel (Int, NAME)
-> [LNode Sign]
-> (Sign, IntMap (Map NAME NAME))
processSig Sign
sig IntMap (Map NAME NAME)
maps Map NAME NAME
forall k a. Map k a
Map.empty Int
i ([DECL] -> [SDECL]
expandDecls [DECL]
ds) Set (Int, NAME)
doneSyms Rel (Int, NAME)
rel [LNode Sign]
sigs

-- main function for computing the colimit
processSig :: Sign ->                        -- the signature determined so far
       IntMap.IntMap (Map.Map NAME NAME) ->  -- the morphisms determined so far
       Map.Map NAME NAME ->                  -- the current map
       Int ->                                -- the number or the current sig
       [SDECL] ->                            -- the declarations to be processed
       Set.Set (Int, NAME) ->                -- the symbols done so far
       Rel.Rel (Int, NAME) ->                -- the equality relation
       [(Int, Sign)] ->                      -- the signatures to be processed
       (Sign, IntMap.IntMap (Map.Map NAME NAME))     -- the determined colimit

processSig :: Sign
-> IntMap (Map NAME NAME)
-> Map NAME NAME
-> Int
-> [SDECL]
-> Set (Int, NAME)
-> Rel (Int, NAME)
-> [LNode Sign]
-> (Sign, IntMap (Map NAME NAME))
processSig sig :: Sign
sig maps :: IntMap (Map NAME NAME)
maps m :: Map NAME NAME
m i :: Int
i [] doneSyms :: Set (Int, NAME)
doneSyms rel :: Rel (Int, NAME)
rel sigs :: [LNode Sign]
sigs =
  let maps1 :: IntMap (Map NAME NAME)
maps1 = Int
-> Map NAME NAME
-> IntMap (Map NAME NAME)
-> IntMap (Map NAME NAME)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i Map NAME NAME
m IntMap (Map NAME NAME)
maps
      in Sign
-> IntMap (Map NAME NAME)
-> Set (Int, NAME)
-> Rel (Int, NAME)
-> [LNode Sign]
-> (Sign, IntMap (Map NAME NAME))
addSig Sign
sig IntMap (Map NAME NAME)
maps1 Set (Int, NAME)
doneSyms Rel (Int, NAME)
rel [LNode Sign]
sigs

processSig sig :: Sign
sig maps :: IntMap (Map NAME NAME)
maps m :: Map NAME NAME
m i :: Int
i ((n :: NAME
n, t :: TYPE
t) : ds :: [SDECL]
ds) doneSyms :: Set (Int, NAME)
doneSyms rel :: Rel (Int, NAME)
rel sigs :: [LNode Sign]
sigs =
  let n1 :: (Int, NAME)
n1 = (Int
i, NAME
n)
      eqSyms :: Set (Int, NAME)
eqSyms = ((Int, NAME) -> Bool) -> Set (Int, NAME) -> Set (Int, NAME)
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ k :: (Int, NAME)
k -> (Int, NAME) -> (Int, NAME) -> Rel (Int, NAME) -> Bool
forall a. Ord a => a -> a -> Rel a -> Bool
Rel.member (Int, NAME)
n1 (Int, NAME)
k Rel (Int, NAME)
rel) Set (Int, NAME)
doneSyms
      in if Set (Int, NAME) -> Bool
forall a. Set a -> Bool
Set.null Set (Int, NAME)
eqSyms
            then let mt :: Map NAME TERM
mt = Map NAME NAME -> Map NAME TERM
toTermMap Map NAME NAME
m
                     syms :: Set NAME
syms = Sign -> Set NAME
getSymbols Sign
sig
                     t1 :: TYPE
t1 = Map NAME TERM -> Set NAME -> TYPE -> TYPE
forall a. Translatable a => Map NAME TERM -> Set NAME -> a -> a
translate Map NAME TERM
mt Set NAME
syms TYPE
t
                     n2 :: NAME
n2 = NAME -> Set NAME -> NAME
toName NAME
n Set NAME
syms
                     sig1 :: Sign
sig1 = DECL -> Sign -> Sign
addSymbolDecl ([NAME
n2], TYPE
t1) Sign
sig
                     m1 :: Map NAME NAME
m1 = NAME -> NAME -> Map NAME NAME -> Map NAME NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NAME
n NAME
n2 Map NAME NAME
m
                     doneSyms1 :: Set (Int, NAME)
doneSyms1 = (Int, NAME) -> Set (Int, NAME) -> Set (Int, NAME)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Int, NAME)
n1 Set (Int, NAME)
doneSyms
                     in Sign
-> IntMap (Map NAME NAME)
-> Map NAME NAME
-> Int
-> [SDECL]
-> Set (Int, NAME)
-> Rel (Int, NAME)
-> [LNode Sign]
-> (Sign, IntMap (Map NAME NAME))
processSig Sign
sig1 IntMap (Map NAME NAME)
maps Map NAME NAME
m1 Int
i [SDECL]
ds Set (Int, NAME)
doneSyms1 Rel (Int, NAME)
rel [LNode Sign]
sigs
            else let k :: (Int, NAME)
k = Set (Int, NAME) -> (Int, NAME)
forall a. Set a -> a
Set.findMin Set (Int, NAME)
eqSyms
                     c :: NAME
c = (Int, NAME) -> IntMap (Map NAME NAME) -> NAME
findValue (Int, NAME)
k (IntMap (Map NAME NAME) -> NAME) -> IntMap (Map NAME NAME) -> NAME
forall a b. (a -> b) -> a -> b
$ Int
-> Map NAME NAME
-> IntMap (Map NAME NAME)
-> IntMap (Map NAME NAME)
forall a. Int -> a -> IntMap a -> IntMap a
IntMap.insert Int
i Map NAME NAME
m IntMap (Map NAME NAME)
maps
                     m1 :: Map NAME NAME
m1 = NAME -> NAME -> Map NAME NAME -> Map NAME NAME
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert NAME
n NAME
c Map NAME NAME
m
                     doneSyms1 :: Set (Int, NAME)
doneSyms1 = (Int, NAME) -> Set (Int, NAME) -> Set (Int, NAME)
forall a. Ord a => a -> Set a -> Set a
Set.insert (Int, NAME)
n1 Set (Int, NAME)
doneSyms
                     in Sign
-> IntMap (Map NAME NAME)
-> Map NAME NAME
-> Int
-> [SDECL]
-> Set (Int, NAME)
-> Rel (Int, NAME)
-> [LNode Sign]
-> (Sign, IntMap (Map NAME NAME))
processSig Sign
sig IntMap (Map NAME NAME)
maps Map NAME NAME
m1 Int
i [SDECL]
ds Set (Int, NAME)
doneSyms1 Rel (Int, NAME)
rel [LNode Sign]
sigs

-- helper functions
findValue :: (Int, NAME) -> IntMap.IntMap (Map.Map NAME NAME) -> NAME
findValue :: (Int, NAME) -> IntMap (Map NAME NAME) -> NAME
findValue (i :: Int
i, k :: NAME
k) maps :: IntMap (Map NAME NAME)
maps = let Just m :: Map NAME NAME
m = Int -> IntMap (Map NAME NAME) -> Maybe (Map NAME NAME)
forall a. Int -> IntMap a -> Maybe a
IntMap.lookup Int
i IntMap (Map NAME NAME)
maps
                           in NAME -> NAME -> Map NAME NAME -> NAME
forall k a. Ord k => a -> k -> Map k a -> a
Map.findWithDefault NAME
k NAME
k Map NAME NAME
m

toName :: NAME -> Set.Set NAME -> NAME
toName :: NAME -> Set NAME -> NAME
toName n :: NAME
n names :: Set NAME
names =
  if NAME -> Set NAME -> Bool
forall a. Ord a => a -> Set a -> Bool
Set.notMember NAME
n Set NAME
names
     then NAME
n
     else let s :: String
s = NAME -> String
tokStr NAME
n
              n1 :: NAME
n1 = String -> Range -> NAME
Token ("gn_" String -> String -> String
forall a. [a] -> [a] -> [a]
++ String
s) Range
nullRange
              in NAME -> Set NAME -> NAME
getNewName NAME
n1 Set NAME
names

computeRel :: Gr Sign (Int, Morphism) -> Rel.Rel (Int, NAME)
computeRel :: Gr Sign (Int, Morphism) -> Rel (Int, NAME)
computeRel gr :: Gr Sign (Int, Morphism)
gr =
  let morphs :: [LEdge (Int, Morphism)]
morphs = Gr Sign (Int, Morphism) -> [LEdge (Int, Morphism)]
forall (gr :: * -> * -> *) a b. Graph gr => gr a b -> [LEdge b]
Graph.labEdges Gr Sign (Int, Morphism)
gr
      rel :: Rel (Int, NAME)
rel = (Rel (Int, NAME) -> LEdge (Int, Morphism) -> Rel (Int, NAME))
-> Rel (Int, NAME) -> [LEdge (Int, Morphism)] -> Rel (Int, NAME)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ r1 :: Rel (Int, NAME)
r1 (i :: Int
i, j :: Int
j, (_, m :: Morphism
m)) ->
                     let syms :: [NAME]
syms = Set NAME -> [NAME]
forall a. Set a -> [a]
Set.toList (Set NAME -> [NAME]) -> Set NAME -> [NAME]
forall a b. (a -> b) -> a -> b
$ Sign -> Set NAME
getSymbols (Sign -> Set NAME) -> Sign -> Set NAME
forall a b. (a -> b) -> a -> b
$ Morphism -> Sign
source Morphism
m
                         in (Rel (Int, NAME) -> NAME -> Rel (Int, NAME))
-> Rel (Int, NAME) -> [NAME] -> Rel (Int, NAME)
forall (t :: * -> *) b a.
Foldable t =>
(b -> a -> b) -> b -> t a -> b
foldl (\ r2 :: Rel (Int, NAME)
r2 s :: NAME
s ->
                                   let t :: NAME
t = Morphism -> NAME -> NAME
mapSymbol Morphism
m NAME
s
                                   in (Int, NAME) -> (Int, NAME) -> Rel (Int, NAME) -> Rel (Int, NAME)
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair (Int
i, NAME
s) (Int
j, NAME
t)
                                          (Rel (Int, NAME) -> Rel (Int, NAME))
-> Rel (Int, NAME) -> Rel (Int, NAME)
forall a b. (a -> b) -> a -> b
$ (Int, NAME) -> (Int, NAME) -> Rel (Int, NAME) -> Rel (Int, NAME)
forall a. Ord a => a -> a -> Rel a -> Rel a
Rel.insertPair (Int
j, NAME
t) (Int
i, NAME
s) Rel (Int, NAME)
r2
                                  )
                                  Rel (Int, NAME)
r1
                                  [NAME]
syms
                  )
                  Rel (Int, NAME)
forall a. Rel a
Rel.empty
                  [LEdge (Int, Morphism)]
morphs
     in Rel (Int, NAME) -> Rel (Int, NAME)
forall a. Ord a => Rel a -> Rel a
Rel.transClosure Rel (Int, NAME)
rel