{-# LANGUAGE FlexibleInstances, FlexibleContexts #-}

{- |

Module : $Header$

Description : CASL signatures colimits

Copyright : (c) Mihai Codescu, and Uni Bremen 2002-2006

License : GPLv2 or higher, see LICENSE.txt

Maintainer : mcodescu@informatik.uni-bremen.de

Stability : provisional

Portability : non-portable

CASL signature colimits, computed component-wise.

Supposed to be working for CASL extensions as well.

based on

<http://www.informatik.uni-bremen.de/~till/papers/colimits.ps>

-}

module CASL.ColimSign (signColimit, extCASLColimit) where

import CASL.Sign

import CASL.Morphism

import CASL.Overload

import CASL.AS_Basic_CASL

import Common.Id

import Common.SetColimit

import Common.Utils (number, nubOrd)

import Common.Lib.Graph

import qualified Common.Lib.Rel as Rel

import qualified Common.Lib.MapSet as MapSet

import Data.Graph.Inductive.Graph as Graph

import qualified Data.Map as Map

import qualified Data.Set as Set

import Data.List

import Logic.Logic

extCASLColimit :: Gr () (Int, ()) ->

Map.Map Int CASLMor ->

((), Map.Map Int ())

extCASLColimit graph _ = ((), Map.fromList $ zip (nodes graph) (repeat ()))

-- central function for computing CASL signature colimits

signColimit :: (Category (Sign f e) (Morphism f e m)) =>

Gr (Sign f e) (Int, Morphism f e m) ->

( Gr e (Int, m) ->

Map.Map Int (Morphism f e m)

-> (e, Map.Map Int m)

)

->

(Sign f e, Map.Map Int (Morphism f e m))

signColimit graph extColimit =

case labNodes graph of

[] -> error "empty graph"

(n, sig) : [] -> (sig, Map.fromAscList [(n, ide sig)])

_ -> let

getSortMap (x, phi) = (x, sort_map phi)

sortGraph = emap getSortMap $ nmap sortSet graph

(setSort0, funSort0) = computeColimitSet sortGraph

(setSort, funSort) = addIntToSymbols (setSort0, funSort0)

sigmaSort = (emptySign $ error "err")

{ sortRel = Rel.fromKeysSet setSort }

phiSort = Map.fromList

$ map (\ (node, s) -> (node, (embedMorphism (error "err") s sigmaSort)

{sort_map = Map.findWithDefault (error "sort_map") node funSort}))

$ labNodes graph

relS = computeSubsorts graph funSort

sigmaRel = sigmaSort {sortRel = Rel.union relS $ sortRel sigmaSort }

phiRel = Map.map (\ phi -> phi {mtarget = sigmaRel}) phiSort

(sigmaOp, phiOp) = computeColimitOp graph sigmaRel phiRel

(sigmaPred, phiPred) = computeColimitPred graph sigmaOp phiOp

(sigAssoc, phiAssoc) = colimitAssoc graph sigmaPred phiPred

extGraph = emap (\ (i, phi) -> (i, extended_map phi)) $

nmap extendedInfo graph

(extInfo, extMaps) = extColimit extGraph phiAssoc

sigmaExt = sigAssoc {extendedInfo = extInfo}

phiExt = Map.mapWithKey

(\ node phi -> phi {mtarget = sigmaExt,

sort_map = Map.filterWithKey (/=) $ sort_map phi,

extended_map = Map.findWithDefault (error "ext_map")

node extMaps})

phiAssoc

in (sigmaExt, phiExt)

{- computing subsorts in the colimit

the subsort relation in the colimit is the transitive closure

of the subsort relations in the diagram

mapped along the structural morphisms of the colimit -}

computeSubsorts :: Gr (Sign f e) (Int, Morphism f e m) ->

Map.Map Node (EndoMap Id) -> Rel.Rel Id

computeSubsorts graph funSort = let

getPhiSort (x, phi) = (x, sort_map phi)

graph1 = nmap sortSet $ emap getPhiSort graph

rels = Map.fromList $ map (\ (node, sign) -> (node, sortRel sign)) $

labNodes graph

in subsorts (nodes graph1) graph1 rels funSort Rel.empty

{- rels is a function assigning to each node

the subsort relation of its label's elements -}

subsorts :: [Node] -> Gr (Set.Set SORT) (Int, Sort_map) ->

Map.Map Node (Rel.Rel SORT) -> Map.Map Node (EndoMap Id) -> Rel.Rel SORT ->

Rel.Rel SORT

subsorts listNode graph rels colimF rel =

case listNode of

[] -> rel

x : xs -> case lab graph x of

Nothing -> subsorts xs graph rels colimF rel

Just set -> let

f = Map.findWithDefault (error "subsorts") x colimF

genRel = Rel.fromList [ (

Map.findWithDefault (error "f(m)") m f,

Map.findWithDefault (error "f(n)") n f

)

| m <- Set.elems set, n <- Set.elems set,

Rel.member m n (Map.findWithDefault

(error "rels(x)") x rels) ]

in subsorts xs graph rels colimF (Rel.transClosure $

Rel.union rel genRel)

-- CASL signatures colimit on operation symbols

{- algorithm description:

1. project the graph on operation symbols

i.e. set of (Id, OpType)s in nodes and corresponding maps on edges

2. compute colimit in Set of the graph => a set of ((Id, OpType), Node)

3. build the overloading relation in colimit

two symbols are overloaded in the colimit

if there is some node and two opsymbols there

that are mapped in them and are overloaded

collect the names entering each symbol (try to keep names)

collect information about totality: a symbol must be total in the colimit

if we have a total symbol in the graph which is mapped to it

4. assign names to each partition, in order of size

(i.e. the equivalence class with most symbols

will be prefered to keep name):

if there is available a name of a symbol entering the class,

then assign that name to the class, otherwise generate a name

also the morphisms have to be built -}

computeColimitOp :: Gr (Sign f e) (Int, Morphism f e m) ->

Sign f e -> Map.Map Node (Morphism f e m) ->

(Sign f e, Map.Map Node (Morphism f e m))

computeColimitOp graph sigmaRel phiSRel = let

graph' = buildOpGraph graph

(colim, morMap') = computeColimitSet graph'

(ovrl, names, totalOps) = buildColimOvrl graph graph' colim morMap'

(colim1, morMap1) = nameSymbols graph' morMap' phiSRel names ovrl totalOps

morMap2 = Map.map (Map.map (\ ((i, o), _) -> (i, opKind o))) morMap1

morMap3 = Map.map (Map.fromAscList . map

(\ ((i, o), y) -> ((i, mkPartial o), y)) . Map.toList) morMap2

sigmaOps = sigmaRel {opMap = colim1}

phiOps = Map.mapWithKey

(\ n phi -> phi {op_map =

Map.findWithDefault (error "op_map") n morMap3})

phiSRel

in (sigmaOps, phiOps)

buildOpGraph :: Gr (Sign f e) (Int, Morphism f e m) ->

Gr (Set.Set (Id, OpType))

(Int, Map.Map (Id, OpType) (Id, OpType))

buildOpGraph graph = let

getOps = mapSetToList . opMap

getOpFun mor = let

ssign = msource mor

smap = sort_map mor

omap = op_map mor

in foldl (\ f x -> let y = mapOpSym smap omap x

in if x == y then f else Map.insert x y f)

Map.empty $ getOps ssign

in nmap (Set.fromList . getOps) $ emap (\ (i, m) -> (i, getOpFun m)) graph

buildColimOvrl :: Gr (Sign f e) (Int, Morphism f e m) ->

Gr (Set.Set (Id, OpType)) (Int, EndoMap (Id, OpType)) ->

Set.Set ((Id, OpType), Int) ->

Map.Map Int (Map.Map (Id, OpType) ((Id, OpType), Int)) ->

(Rel.Rel ((Id, OpType), Int),

Map.Map ((Id, OpType), Int)

(Map.Map Id Int),

Map.Map ((Id, OpType), Int) Bool)

buildColimOvrl graph graph' colim morMap = let

(ovrl, names) = (Rel.empty, Map.fromList $ zip (Set.toList colim) $

repeat Map.empty )

(ovrl', names', totalF') = buildOvrlAtNode graph' colim morMap

ovrl names Map.empty $ labNodes graph

in (Rel.transClosure ovrl', names', totalF')

buildOvrlAtNode :: Gr (Set.Set (Id, OpType)) (Int, EndoMap (Id, OpType)) ->

Set.Set ((Id, OpType), Int) ->

Map.Map Int (Map.Map (Id, OpType) ((Id, OpType), Int)) ->

Rel.Rel ((Id, OpType), Int) ->

Map.Map ((Id, OpType), Int) (Map.Map Id Int) ->

Map.Map ((Id, OpType), Int) Bool ->

[(Int, Sign f e)] ->

(Rel.Rel ((Id, OpType), Int),

Map.Map ((Id, OpType), Int) (Map.Map Id Int),

Map.Map ((Id, OpType), Int) Bool )

buildOvrlAtNode graph' colim morMap ovrl names totalF nodeList =

case nodeList of

[] -> (ovrl, names, totalF)

(n, sig) : lists -> let

Just oSet = lab graph' n

names' = foldl (\ g x@(idN, _) -> let

y = Map.findWithDefault (x, n) x $

Map.findWithDefault (error $ show n)

n morMap

altF v = case v of

Nothing -> Just 1

Just m -> Just $ m + 1

in Map.adjust (Map.alter altF idN) y g)

names $ Set.toList oSet

equivF (id1, ot1) (id2, ot2) = (id1 == id2) && leqF sig ot1 ot2

parts = Rel.leqClasses equivF oSet

addParts rel =

foldl (\ (r, f) l -> let l1 = map (\ x -> Map.findWithDefault (x, n)

x $ Map.findWithDefault

(error "morMap(n)") n morMap) l

in case l1 of

[] -> error "addParts"

x : xs -> let

(r', ly) = foldl

(\ (rl, lx) y -> (Rel.insertPair lx y rl, y))

(r, x) xs

f' = foldl (\ g ((_i, o), ((i', o'), n')) ->

if isTotal o then

Map.insert ((i', mkPartial o'), n')

True g

else g ) f $ zip l l1

in (Rel.insertPair ly x r', f')

) (rel, totalF)

(ovrl', totalF') = addParts ovrl parts

in buildOvrlAtNode graph' colim morMap ovrl' names' totalF' lists

assignName :: (Set.Set ((Id, OpType), Int), Int) -> [Id] ->

Map.Map ((Id, OpType), Int) (Map.Map Id Int) ->

(Id, [Id])

assignName (opSet, idx) givenNames namesFun =

let opSetNames = Set.fold (\ x f -> Map.unionWith (+) f

(Map.findWithDefault (error "namesFun") x

namesFun)) Map.empty opSet

availNames = filter (`notElem` givenNames) $

Map.keys opSetNames

in case availNames of

[] -> let

-- must generate name with the most frequent name idx and an origin

sndOrd x y = compare

(Map.findWithDefault (error "assignName") x opSetNames)

(Map.findWithDefault (error "assignName") y opSetNames)

avail' = sortBy sndOrd $ Map.keys opSetNames

idN = head avail'

in (appendNumber idN idx, givenNames)

_ -> {- must take the most frequent available name and give it to the class

and this name becomes given -}

let

sndOrd x y = compare

(Map.findWithDefault (error "assignName") x opSetNames)

(Map.findWithDefault (error "assignName") y opSetNames)

avail' = sortBy sndOrd availNames

idN = last avail'

in (idN, idN : givenNames)

nameSymbols :: Gr (Set.Set (Id, OpType))

(Int, Map.Map (Id, OpType) (Id, OpType)) ->

Map.Map Int (Map.Map (Id, OpType) ((Id, OpType), Int)) ->

Map.Map Int (Morphism f e m) ->

Map.Map ((Id, OpType), Int) (Map.Map Id Int) ->

Rel.Rel ((Id, OpType), Int) ->

Map.Map ((Id, OpType), Int) Bool ->

(OpMap, Map.Map Int (Map.Map (Id, OpType) ((Id, OpType), Int)))

nameSymbols graph morMap phi names ovrl totalOps = let

colimOvrl = Rel.sccOfClosure ovrl

nameClass opFun gNames (set, idx) morFun = let

(newName, gNames') = assignName (set, idx) gNames names

opTypes = Set.map (\ ((oldId, ot), i) -> let

oKind' = if Map.findWithDefault False

((oldId, mkPartial ot), i)

totalOps

then Total else Partial

imor = Map.findWithDefault (error "imor") i phi

in mapOpType (sort_map imor) $ setOpKind oKind' ot) set

renameSymbols n f = let

Just opSyms = lab graph n

setKeys = filter (\ x -> let y = Map.findWithDefault (x, n) x f

in Set.member y set) $ Set.toList opSyms

updateAtKey (i, o) ((i', o'), n') = let

nmor = Map.findWithDefault (error "nmor") n phi

o'' = mapOpType (sort_map nmor) o'

oKind = if Map.findWithDefault False

((i', mkPartial o'), n')

totalOps

then Total else Partial

z = (newName, setOpKind oKind o'')

in if (i, o) == z then

Nothing

else

Just (z, n')

in foldl (\ g x -> Map.update (updateAtKey x) x g)

f setKeys

{- -- i have to map symbols entering set

-- to (newName, their otype mapped) -}

morFun' = Map.mapWithKey renameSymbols morFun

in (MapSet.update (const opTypes) newName opFun, gNames', morFun')

colimOvrl' = sortBy (\ s1 s2 -> compare (Set.size s2) (Set.size s1)) colimOvrl

(opFuns, _, renMap) = foldl (\ (oF, gN, mM) x -> nameClass oF gN x mM)

(MapSet.empty, [], morMap)

$ number colimOvrl'

in (opFuns , renMap)

{- -CASL signatures colimit on predicate symbols

almost identical with operation symbols,

only minor changes because of different types

- -}

computeColimitPred :: Gr (Sign f e) (Int, Morphism f e m) -> Sign f e ->

Map.Map Node (Morphism f e m) -> (Sign f e, Map.Map Node (Morphism f e m))

computeColimitPred graph sigmaOp phiOp = let

graph' = buildPredGraph graph

(colim, morMap') = computeColimitSet graph'

(ovrl, names) = buildPColimOvrl graph graph' colim morMap'

(colim1, morMap1) = namePSymbols graph' morMap' phiOp names ovrl

morMap2 = Map.map (Map.map (\ ((i, _p), _) -> i)) morMap1

sigmaPreds = sigmaOp {predMap = colim1}

phiPreds = Map.mapWithKey

(\ n phi -> phi {pred_map =

Map.findWithDefault (error "pred_map") n morMap2})

phiOp

in (sigmaPreds, phiPreds)

buildPredGraph :: Gr (Sign f e) (Int, Morphism f e m) ->

Gr (Set.Set (Id, PredType))

(Int, Map.Map (Id, PredType) (Id, PredType))

buildPredGraph graph = let

getPreds = mapSetToList . predMap

getPredFun mor = let

ssign = msource mor

smap = sort_map mor

pmap = pred_map mor

in foldl (\ f x -> let y = mapPredSym smap pmap x

in if x == y then f else Map.insert x y f)

Map.empty $ getPreds ssign

in nmap (Set.fromList . getPreds) $ emap (\ (i, m) -> (i, getPredFun m)) graph

buildPColimOvrl :: Gr (Sign f e) (Int, Morphism f e m) ->

Gr (Set.Set (Id, PredType)) (Int, EndoMap (Id, PredType)) ->

Set.Set ((Id, PredType), Int) ->

Map.Map Int (Map.Map (Id, PredType) ((Id, PredType), Int)) ->

(Rel.Rel ((Id, PredType), Int),

Map.Map ((Id, PredType), Int) (Map.Map Id Int))

buildPColimOvrl graph graph' colim morMap = let

(ovrl, names) = (Rel.empty, Map.fromList $ zip (Set.toList colim) $

repeat Map.empty )

(ovrl', names') = buildPOvrlAtNode graph' colim morMap

ovrl names $ labNodes graph

in (Rel.transClosure ovrl', names')

buildPOvrlAtNode :: Gr (Set.Set (Id, PredType)) (Int, EndoMap (Id, PredType)) ->

Set.Set ((Id, PredType), Int) ->

Map.Map Int (Map.Map (Id, PredType) ((Id, PredType), Int)) ->

Rel.Rel ((Id, PredType), Int) ->

Map.Map ((Id, PredType), Int) (Map.Map Id Int) ->

[(Int, Sign f e)] ->

(Rel.Rel ((Id, PredType), Int),

Map.Map ((Id, PredType), Int) (Map.Map Id Int))

buildPOvrlAtNode graph' colim morMap ovrl names nodeList =

case nodeList of

[] -> (ovrl, names)

(n, sig) : lists -> let

Just pSet = lab graph' n

names' = foldl (\ g x@(idN, _) -> let

y = Map.findWithDefault (x, n) x $

Map.findWithDefault (error $ show n)

n morMap

altF v = case v of

Nothing -> Just 1

Just m -> Just $ m + 1

in Map.adjust (Map.alter altF idN)

y g)

names $ Set.toList pSet

equivP (id1, pt1) (id2, pt2) = (id1 == id2) && leqP sig pt1 pt2

parts = Rel.leqClasses equivP pSet

nmor = Map.findWithDefault (error "buildAtNode") n morMap

addParts =

foldl (\ r l -> let l1 = map (\ x ->

Map.findWithDefault (x, n) x nmor) l

in case l1 of

[] -> error "addParts"

x : xs -> let

(r', ly) = foldl

(\ (rl, lx) y -> (Rel.insertPair lx y rl, y))

(r, x) xs

in Rel.insertPair ly x r'

)

ovrl' = addParts ovrl parts

in buildPOvrlAtNode graph' colim morMap ovrl' names' lists

assignPName :: (Set.Set ((Id, PredType), Int), Int) -> [Id] ->

Map.Map ((Id, PredType), Int) (Map.Map Id Int) ->

(Id, [Id])

assignPName (pSet, idx) givenNames namesFun =

let pSetNames = Set.fold (\ x f -> Map.unionWith (+) f

(Map.findWithDefault (error "pname") x namesFun))

Map.empty pSet

availNames = filter (`notElem` givenNames) $ Map.keys pSetNames

in case availNames of

[] -> let

-- must generate name with the most frequent name idx and an origin

sndOrd x y = compare (pSetNames Map.! x) (pSetNames Map.! y)

avail' = sortBy sndOrd $ Map.keys pSetNames

idN = head avail'

in (appendNumber idN idx, givenNames)

_ -> {- must take the most frequent available name and give it to the class

and this name becomes given -}

let

sndOrd x y = compare (pSetNames Map.! x) (pSetNames Map.! y)

avail' = sortBy sndOrd availNames

idN = last avail'

in (idN, idN : givenNames)

namePSymbols :: Gr (Set.Set (Id, PredType))

(Int, Map.Map (Id, PredType) (Id, PredType)) ->

Map.Map Int (Map.Map (Id, PredType) ((Id, PredType), Int)) ->

Map.Map Int (Morphism f e m) ->

Map.Map ((Id, PredType), Int) (Map.Map Id Int) ->

Rel.Rel ((Id, PredType), Int) ->

(PredMap, Map.Map Int (Map.Map (Id, PredType)

((Id, PredType), Int)))

namePSymbols graph morMap phi names ovrl = let

colimOvrl = Rel.sccOfClosure ovrl

nameClass pFun gNames (set, idx) morFun = let

(newName, gNames') = assignPName (set, idx) gNames names

pTypes = Set.map (\ ((_oldId, pt), i) -> let

in mapPredType (sort_map $ phi Map.! i) pt) set

renameSymbols n f = let

Just pSyms = lab graph n

setKeys = filter (\ x -> let y = Map.findWithDefault (x, n) x f

in Set.member y set) $ Set.toList pSyms

updateAtKey (i, p) ((_i', p'), n') = let

p'' = mapPredType (sort_map $ phi Map.! n) p'

z = (newName, p'')

in if (i, p) == z then

Nothing

else

Just (z, n')

in foldl (\ g x -> Map.update (updateAtKey x) x g)

f setKeys

{- -- i have to map symbols entering set

-- to (newName, their predtype mapped) -}

morFun' = Map.mapWithKey renameSymbols morFun

in (MapSet.update (const pTypes) newName pFun, gNames', morFun')

colimOvrl' = sortBy (\ s1 s2 -> compare (Set.size s2) (Set.size s1)) colimOvrl

(pFuns, _, renMap) = foldl (\ (pF, gN, mM) x -> nameClass pF gN x mM)

(MapSet.empty, [], morMap)

$ number colimOvrl'

in (pFuns , renMap)

applyMor :: Morphism f e m -> (Id, OpType) -> (Id, OpType)

applyMor phi (i, optype) = mapOpSym (sort_map phi) (op_map phi) (i, optype)

-- associative operations

assocSymbols :: Sign f e -> [(Id, OpType)]

assocSymbols = mapSetToList . assocOps

colimitAssoc :: Gr (Sign f e) (Int, Morphism f e m) -> Sign f e ->

Map.Map Int (Morphism f e m) -> (Sign f e, Map.Map Int (Morphism f e m))

colimitAssoc graph sig morMap = let

assocOpList = nubOrd $ concatMap

(\ (node, sigma) -> map (applyMor ((Map.!) morMap node)) $

assocSymbols sigma ) $ labNodes graph

idList = nubOrd $ map fst assocOpList

sig1 = sig {assocOps = MapSet.fromList $

map (\ sb -> (sb, map snd $ filter (\ (i, _) -> i == sb)

assocOpList )) idList}

morMap1 = Map.map (\ phi -> phi {mtarget = sig1}) morMap

in (sig1, morMap1)