5253N/A{- |

5253N/AModule : $Header$

5253N/ADescription : Signature colimits for first-order logic with dependent

5253N/A types (DFOL)

5253N/ACopyright : (c) Kristina Sojakova, DFKI Bremen 2009

5253N/ALicense : GPLv2 or higher

5253N/A

5253N/AMaintainer : k.sojakova@jacobs-university.de

5253N/AStability : experimental

5253N/APortability : portable

5253N/A

5253N/AAlgorithm description:

5253N/A

5253N/AInput : graph where nodes are signatures and edges are morphisms

5253N/AOutput : a signature "sig" and for each input signature "sig1" a morphism

5253N/A m : sig1 -> sig

5253N/A

5253N/A1 : Compute the transitive and symmetric closure of the relation R induced

5253N/A by the morphisms in the graph

5253N/A

5253N/A2 : Initialize the output signature "sig" and collection of morphisms "M" to

5253N/A empty

5342N/A Initialize the set of analyzed symbols to empty

5253N/A

5253N/A3 : For each input signature sig1 :

5254N/A 3.1 : Initialize the output map "m" to empty

5254N/A 3.2 : For each symbol "s" in sig1 (keeping the order in which they are

5254N/A defined) :

6429N/A 3.1.1 Check if s R s' for any already analyzed symbol "s'"

6429N/A 3.1.2 If yes:

5253N/A 3.1.2.1 Recover from M the value "c" that s' maps to

5253N/A 3.1.2.2 Update m by adding the pair (s,c)

5253N/A 3.1.3 If no:

5253N/A 3.1.3.1 Get the type "t" of s in sig1

7016N/A 3.1.3.2 Translate t along m; call this new type "t1"

5253N/A 3.1.3.3 Update sig by adding the declaration s : t1

6429N/A (in case the name s is already contained in sig,

5253N/A we generate a fresh name "s1" and add the declaration

7016N/A s1 : t and pair (s,s1) to sig and m respectively.

6429N/A 3.3 : Add m to M

5253N/A-}

5305N/A

5253N/Amodule DFOL.Colimit (

7016N/A sigColimit

5525N/A ) where

7016N/A

5253N/Aimport DFOL.AS_DFOL

5253N/Aimport DFOL.Sign

5253N/Aimport DFOL.Morphism

5253N/Aimport Common.Result

5525N/Aimport Common.Id

5256N/Aimport Common.Lib.Graph

6429N/Aimport qualified Data.Graph.Inductive.Graph as Graph

6429N/Aimport qualified Common.Lib.Rel as Rel

5256N/Aimport qualified Data.Map as Map

5256N/Aimport qualified Data.Set as Set

6429N/Aimport qualified Data.IntMap as IntMap

5256N/A

7016N/A-- main functions

7016N/AsigColimit :: Gr Sign (Int, Morphism) -> Result (Sign, Map.Map Int Morphism)

5253N/AsigColimit gr =

7016N/A let sigs = Graph.labNodes gr

5525N/A rel = computeRel gr

6429N/A (sig,maps) = addSig emptySig IntMap.empty Set.empty rel sigs

7016N/A maps1 = IntMap.mapWithKey (\ i m -> let Just sig1 = Graph.lab gr i

5525N/A in Morphism sig1 sig m

5253N/A )

5253N/A maps

5253N/A maps2 = Map.fromList $ IntMap.toList maps1

5253N/A in Result [] $ Just (sig,maps2)

7016N/A

7016N/A-- preparation for computing the colimit

6429N/AaddSig :: Sign -> IntMap.IntMap (Map.Map NAME NAME) -> Set.Set (Int, NAME) ->

5525N/A Rel.Rel (Int, NAME) -> [(Int, Sign)] ->

5530N/A (Sign, IntMap.IntMap (Map.Map NAME NAME))

5530N/AaddSig sig maps _ _ [] = (sig,maps)

6429N/AaddSig sig maps doneSyms rel ((i, Sign ds):sigs) =

7016N/A processSig sig maps Map.empty i (expandDecls ds) doneSyms rel sigs

7016N/A

7016N/A-- main function for computing the colimit

7016N/AprocessSig :: Sign -> -- the signature determined so far

7016N/A IntMap.IntMap (Map.Map NAME NAME) -> -- the morphisms determined so far

7016N/A Map.Map NAME NAME -> -- the current map

7016N/A Int -> -- the number or the current sig

5530N/A [DECL] -> -- the declarations to be processed

5413N/A Set.Set (Int, NAME) -> -- the symbols done so far

5413N/A Rel.Rel (Int, NAME) -> -- the equality relation

5413N/A [(Int, Sign)] -> -- the signatures to be processed

5413N/A (Sign, IntMap.IntMap (Map.Map NAME NAME)) -- the determined colimit

5413N/A

5413N/AprocessSig sig maps m i [] doneSyms rel sigs =

5413N/A let maps1 = IntMap.insert i m maps

5413N/A in addSig sig maps1 doneSyms rel sigs

6452N/A

6452N/AprocessSig sig maps m i (([n],t):ds) doneSyms rel sigs =

7013N/A let n1 = (i,n)

7013N/A eqSyms = Set.filter (\ k -> Rel.member n1 k rel) doneSyms

5253N/A in if (Set.null eqSyms)

5305N/A then let mt = toTermMap m

5305N/A syms = getSymbols sig

5253N/A t1 = translate mt syms t

5305N/A n2 = toName n syms

5305N/A sig1 = addSymbolDecl ([n2],t1) sig

5525N/A m1 = Map.insert n n2 m

5305N/A doneSyms1 = Set.insert n1 doneSyms

5305N/A in processSig sig1 maps m1 i ds doneSyms1 rel sigs

5305N/A else let k = Set.findMin eqSyms

5305N/A c = findValue k $ IntMap.insert i m maps

5305N/A m1 = Map.insert n c m

5305N/A doneSyms1 = Set.insert n1 doneSyms

5305N/A in processSig sig maps m1 i ds doneSyms1 rel sigs

5305N/A

5305N/AprocessSig _ _ _ _ _ _ _ _ = (emptySig, IntMap.empty)

5305N/A

5305N/A-- helper functions

5305N/AfindValue :: (Int, NAME) -> IntMap.IntMap (Map.Map NAME NAME) -> NAME

5305N/AfindValue (i,k) maps = let Just m = IntMap.lookup i maps

5305N/A in Map.findWithDefault k k m

5305N/A

5305N/AtoName :: NAME -> Set.Set NAME -> NAME

5305N/AtoName n names =

5305N/A if (Set.notMember n names)

5305N/A then n

5305N/A else let s = tokStr n

5305N/A n1 = Token ("gn_" ++ s) nullRange

5305N/A in getNewName n1 names

5305N/A

5305N/AcomputeRel :: Gr Sign (Int, Morphism) -> Rel.Rel (Int, NAME)

5305N/AcomputeRel gr =

5253N/A let morphs = Graph.labEdges gr

5342N/A rel = foldl (\ r1 (i,j,(_,m)) ->

5342N/A let syms = Set.toList $ getSymbols $ source m

5342N/A in foldl (\ r2 s -> let t = mapSymbol m s

5253N/A in Rel.insert (i,s) (j,t)

7013N/A $ Rel.insert (j,t) (i,s) r2

7013N/A )

7013N/A r1

7013N/A syms

7013N/A )

5253N/A Rel.empty

5253N/A morphs

5525N/A in Rel.transClosure rel

5525N/A