18c2aff776a775d34a4c9893a4c72e0434d68e36artem{- |

18c2aff776a775d34a4c9893a4c72e0434d68e36artemModule : $Header$

18c2aff776a775d34a4c9893a4c72e0434d68e36artemDescription : Signature colimits for first-order logic with dependent

18c2aff776a775d34a4c9893a4c72e0434d68e36artem types (DFOL)

18c2aff776a775d34a4c9893a4c72e0434d68e36artemCopyright : (c) Kristina Sojakova, DFKI Bremen 2009

18c2aff776a775d34a4c9893a4c72e0434d68e36artemLicense : GPLv2 or higher

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artemMaintainer : k.sojakova@jacobs-university.de

18c2aff776a775d34a4c9893a4c72e0434d68e36artemStability : experimental

18c2aff776a775d34a4c9893a4c72e0434d68e36artemPortability : portable

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artemAlgorithm description:

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artemInput : graph where nodes are signatures and edges are morphisms

18c2aff776a775d34a4c9893a4c72e0434d68e36artemOutput : a signature "sig" and for each input signature "sig1" a morphism

18c2aff776a775d34a4c9893a4c72e0434d68e36artem m : sig1 -> sig

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artem1 : Compute the transitive and symmetric closure of the relation R induced

18c2aff776a775d34a4c9893a4c72e0434d68e36artem by the morphisms in the graph

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artem2 : Initialize the output signature "sig" and collection of morphisms "M" to

18c2aff776a775d34a4c9893a4c72e0434d68e36artem empty

18c2aff776a775d34a4c9893a4c72e0434d68e36artem Initialize the set of analyzed symbols to empty

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artem3 : For each input signature sig1 :

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.1 : Initialize the output map "m" to empty

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.2 : For each symbol "s" in sig1 (keeping the order in which they are

18c2aff776a775d34a4c9893a4c72e0434d68e36artem defined) :

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.1.1 Check if s R s' for any already analyzed symbol "s'"

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.1.2 If yes:

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.1.2.1 Recover from M the value "c" that s' maps to

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.1.2.2 Update m by adding the pair (s,c)

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.1.3 If no:

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.1.3.1 Get the type "t" of s in sig1

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.1.3.2 Translate t along m; call this new type "t1"

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.1.3.3 Update sig by adding the declaration s : t1

18c2aff776a775d34a4c9893a4c72e0434d68e36artem (in case the name s is already contained in sig,

18c2aff776a775d34a4c9893a4c72e0434d68e36artem we generate a fresh name "s1" and add the declaration

18c2aff776a775d34a4c9893a4c72e0434d68e36artem s1 : t and pair (s,s1) to sig and m respectively.

18c2aff776a775d34a4c9893a4c72e0434d68e36artem 3.3 : Add m to M

18c2aff776a775d34a4c9893a4c72e0434d68e36artem-}

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artemmodule DFOL.Colimit (

18c2aff776a775d34a4c9893a4c72e0434d68e36artem sigColimit

18c2aff776a775d34a4c9893a4c72e0434d68e36artem ) where

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport DFOL.AS_DFOL

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport DFOL.Sign

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport DFOL.Morphism

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport Common.Result

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport Common.Id

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport Common.Lib.Graph

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport qualified Data.Graph.Inductive.Graph as Graph

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport qualified Common.Lib.Rel as Rel

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport qualified Data.Map as Map

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport qualified Data.Set as Set

18c2aff776a775d34a4c9893a4c72e0434d68e36artemimport qualified Data.IntMap as IntMap

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- main functions

18c2aff776a775d34a4c9893a4c72e0434d68e36artemsigColimit :: Gr Sign (Int, Morphism) -> Result (Sign, Map.Map Int Morphism)

18c2aff776a775d34a4c9893a4c72e0434d68e36artemsigColimit gr =

18c2aff776a775d34a4c9893a4c72e0434d68e36artem let sigs = Graph.labNodes gr

18c2aff776a775d34a4c9893a4c72e0434d68e36artem rel = computeRel gr

18c2aff776a775d34a4c9893a4c72e0434d68e36artem (sig,maps) = addSig emptySig IntMap.empty Set.empty rel sigs

18c2aff776a775d34a4c9893a4c72e0434d68e36artem maps1 = IntMap.mapWithKey (\ i m -> let Just sig1 = Graph.lab gr i

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in Morphism sig1 sig m

18c2aff776a775d34a4c9893a4c72e0434d68e36artem )

18c2aff776a775d34a4c9893a4c72e0434d68e36artem maps

18c2aff776a775d34a4c9893a4c72e0434d68e36artem maps2 = Map.fromList $ IntMap.toList maps1

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in Result [] $ Just (sig,maps2)

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- preparation for computing the colimit

18c2aff776a775d34a4c9893a4c72e0434d68e36artemaddSig :: Sign -> IntMap.IntMap (Map.Map NAME NAME) -> Set.Set (Int, NAME) ->

18c2aff776a775d34a4c9893a4c72e0434d68e36artem Rel.Rel (Int, NAME) -> [(Int, Sign)] ->

18c2aff776a775d34a4c9893a4c72e0434d68e36artem (Sign, IntMap.IntMap (Map.Map NAME NAME))

18c2aff776a775d34a4c9893a4c72e0434d68e36artemaddSig sig maps _ _ [] = (sig,maps)

18c2aff776a775d34a4c9893a4c72e0434d68e36artemaddSig sig maps doneSyms rel ((i, Sign ds):sigs) =

18c2aff776a775d34a4c9893a4c72e0434d68e36artem processSig sig maps Map.empty i (expandDecls ds) doneSyms rel sigs

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- main function for computing the colimit

18c2aff776a775d34a4c9893a4c72e0434d68e36artemprocessSig :: Sign -> -- the signature determined so far

18c2aff776a775d34a4c9893a4c72e0434d68e36artem IntMap.IntMap (Map.Map NAME NAME) -> -- the morphisms determined so far

18c2aff776a775d34a4c9893a4c72e0434d68e36artem Map.Map NAME NAME -> -- the current map

18c2aff776a775d34a4c9893a4c72e0434d68e36artem Int -> -- the number or the current sig

18c2aff776a775d34a4c9893a4c72e0434d68e36artem [DECL] -> -- the declarations to be processed

18c2aff776a775d34a4c9893a4c72e0434d68e36artem Set.Set (Int, NAME) -> -- the symbols done so far

18c2aff776a775d34a4c9893a4c72e0434d68e36artem Rel.Rel (Int, NAME) -> -- the equality relation

18c2aff776a775d34a4c9893a4c72e0434d68e36artem [(Int, Sign)] -> -- the signatures to be processed

18c2aff776a775d34a4c9893a4c72e0434d68e36artem (Sign, IntMap.IntMap (Map.Map NAME NAME)) -- the determined colimit

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artemprocessSig sig maps m i [] doneSyms rel sigs =

18c2aff776a775d34a4c9893a4c72e0434d68e36artem let maps1 = IntMap.insert i m maps

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in addSig sig maps1 doneSyms rel sigs

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artemprocessSig sig maps m i (([n],t):ds) doneSyms rel sigs =

18c2aff776a775d34a4c9893a4c72e0434d68e36artem let n1 = (i,n)

18c2aff776a775d34a4c9893a4c72e0434d68e36artem eqSyms = Set.filter (\ k -> Rel.member n1 k rel) doneSyms

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in if (Set.null eqSyms)

18c2aff776a775d34a4c9893a4c72e0434d68e36artem then let mt = toTermMap m

18c2aff776a775d34a4c9893a4c72e0434d68e36artem syms = getSymbols sig

18c2aff776a775d34a4c9893a4c72e0434d68e36artem t1 = translate mt syms t

18c2aff776a775d34a4c9893a4c72e0434d68e36artem n2 = toName n syms

18c2aff776a775d34a4c9893a4c72e0434d68e36artem sig1 = addSymbolDecl ([n2],t1) sig

18c2aff776a775d34a4c9893a4c72e0434d68e36artem m1 = Map.insert n n2 m

18c2aff776a775d34a4c9893a4c72e0434d68e36artem doneSyms1 = Set.insert n1 doneSyms

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in processSig sig1 maps m1 i ds doneSyms1 rel sigs

18c2aff776a775d34a4c9893a4c72e0434d68e36artem else let k = Set.findMin eqSyms

18c2aff776a775d34a4c9893a4c72e0434d68e36artem c = findValue k $ IntMap.insert i m maps

18c2aff776a775d34a4c9893a4c72e0434d68e36artem m1 = Map.insert n c m

18c2aff776a775d34a4c9893a4c72e0434d68e36artem doneSyms1 = Set.insert n1 doneSyms

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in processSig sig maps m1 i ds doneSyms1 rel sigs

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artemprocessSig _ _ _ _ _ _ _ _ = (emptySig, IntMap.empty)

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artem-- helper functions

18c2aff776a775d34a4c9893a4c72e0434d68e36artemfindValue :: (Int, NAME) -> IntMap.IntMap (Map.Map NAME NAME) -> NAME

18c2aff776a775d34a4c9893a4c72e0434d68e36artemfindValue (i,k) maps = let Just m = IntMap.lookup i maps

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in Map.findWithDefault k k m

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artemtoName :: NAME -> Set.Set NAME -> NAME

18c2aff776a775d34a4c9893a4c72e0434d68e36artemtoName n names =

18c2aff776a775d34a4c9893a4c72e0434d68e36artem if (Set.notMember n names)

18c2aff776a775d34a4c9893a4c72e0434d68e36artem then n

18c2aff776a775d34a4c9893a4c72e0434d68e36artem else let s = tokStr n

18c2aff776a775d34a4c9893a4c72e0434d68e36artem n1 = Token ("gn_" ++ s) nullRange

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in getNewName n1 names

18c2aff776a775d34a4c9893a4c72e0434d68e36artem

18c2aff776a775d34a4c9893a4c72e0434d68e36artemcomputeRel :: Gr Sign (Int, Morphism) -> Rel.Rel (Int, NAME)

18c2aff776a775d34a4c9893a4c72e0434d68e36artemcomputeRel gr =

18c2aff776a775d34a4c9893a4c72e0434d68e36artem let morphs = Graph.labEdges gr

18c2aff776a775d34a4c9893a4c72e0434d68e36artem rel = foldl (\ r1 (i,j,(_,m)) ->

18c2aff776a775d34a4c9893a4c72e0434d68e36artem let syms = Set.toList $ getSymbols $ source m

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in foldl (\ r2 s -> let t = mapSymbol m s

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in Rel.insert (i,s) (j,t)

18c2aff776a775d34a4c9893a4c72e0434d68e36artem $ Rel.insert (j,t) (i,s) r2

18c2aff776a775d34a4c9893a4c72e0434d68e36artem )

18c2aff776a775d34a4c9893a4c72e0434d68e36artem r1

18c2aff776a775d34a4c9893a4c72e0434d68e36artem syms

18c2aff776a775d34a4c9893a4c72e0434d68e36artem )

18c2aff776a775d34a4c9893a4c72e0434d68e36artem Rel.empty

18c2aff776a775d34a4c9893a4c72e0434d68e36artem morphs

18c2aff776a775d34a4c9893a4c72e0434d68e36artem in Rel.transClosure rel

18c2aff776a775d34a4c9893a4c72e0434d68e36artem