{- |

Module : $Header$

Description : Symbols and signature morphisms for the CASL logic

Copyright : (c) Christian Maeder, Till Mossakowski and Uni Bremen 2002-2004

License : similar to LGPL, see HetCATS/LICENSE.txt or LIZENZ.txt

Maintainer : Christian.Maeder@dfki.de

Stability : provisional

Portability : portable

Symbols and signature morphisms for the CASL logic

-}

{-

todo:

issue warning for symbols lists like __ * __, __ + __: Elem * Elem -> Elem

the qualification only applies to __+__ !

possibly reuse SYMB_KIND for Kind

-}

module CASL.Morphism where

import CASL.Sign

import CASL.AS_Basic_CASL

import qualified Data.Map as Map

import qualified Data.Set as Set

import qualified Common.Lib.Rel as Rel

import Common.Doc

import Common.DocUtils

import Common.Id

import Common.Keywords

import Common.Result

import Control.Exception (assert)

type SymbolSet = Set.Set Symbol

type SymbolMap = Map.Map Symbol Symbol

data RawSymbol = ASymbol Symbol | AnID Id | AKindedId Kind Id

deriving (Show, Eq, Ord)

instance PosItem RawSymbol where

getRange rs =

case rs of

ASymbol s -> getRange s

AnID i -> getRange i

AKindedId _ i -> getRange i

type RawSymbolSet = Set.Set RawSymbol

type RawSymbolMap = Map.Map RawSymbol RawSymbol

data Kind = SortKind | FunKind | PredKind deriving (Show, Eq, Ord)

type Sort_map = Map.Map SORT SORT

-- always use the partial profile as key!

type Fun_map = Map.Map (Id,OpType) (Id, FunKind)

type Pred_map = Map.Map (Id,PredType) Id

data Morphism f e m = Morphism

{ msource :: Sign f e

, mtarget :: Sign f e

, sort_map :: Sort_map

, fun_map :: Fun_map

, pred_map :: Pred_map

, extended_map :: m

} deriving (Eq, Show)

mapSort :: Sort_map -> SORT -> SORT

mapSort sorts s = Map.findWithDefault s s sorts

mapOpType :: Sort_map -> OpType -> OpType

mapOpType sorts t = if Map.null sorts then t else

t { opArgs = map (mapSort sorts) $ opArgs t

, opRes = mapSort sorts $ opRes t }

mapOpTypeK :: Sort_map -> FunKind -> OpType -> OpType

mapOpTypeK sorts k t = makeTotal k $ mapOpType sorts t

makeTotal :: FunKind -> OpType -> OpType

makeTotal fk t = case fk of

Total -> t { opKind = Total }

_ -> t

mapOpSym :: Sort_map -> Fun_map -> (Id, OpType) -> (Id, OpType)

mapOpSym sMap fMap (i, ot) = let mot = mapOpType sMap ot in

case Map.lookup (i, ot {opKind = Partial} ) fMap of

Nothing -> (i, mot)

Just (j, k) -> (j, makeTotal k mot)

-- | Check if two OpTypes are equal modulo totality or partiality

compatibleOpTypes :: OpType -> OpType -> Bool

compatibleOpTypes ot1 ot2 = opArgs ot1 == opArgs ot2 && opRes ot1 == opRes ot2

mapPredType :: Sort_map -> PredType -> PredType

mapPredType sorts t = if Map.null sorts then t else

t { predArgs = map (mapSort sorts) $ predArgs t }

mapPredSym :: Sort_map -> Pred_map -> (Id, PredType) -> (Id, PredType)

mapPredSym sMap fMap (i, pt) =

(Map.findWithDefault i (i, pt) fMap, mapPredType sMap pt)

embedMorphism :: m -> Sign f e -> Sign f e -> Morphism f e m

embedMorphism extEm a b = Morphism

{ msource = a

, mtarget = b

, sort_map = Map.empty

, fun_map = Map.empty

, pred_map = Map.empty

, extended_map = extEm }

symbTypeToKind :: SymbType -> Kind

symbTypeToKind st = case st of

OpAsItemType _ -> FunKind

PredAsItemType _ -> PredKind

SortAsItemType -> SortKind

symbolToRaw :: Symbol -> RawSymbol

symbolToRaw sym = ASymbol sym

idToRaw :: Id -> RawSymbol

idToRaw x = AnID x

rawSymName :: RawSymbol -> Id

rawSymName rs = case rs of

ASymbol sym -> symName sym

AnID i -> i

AKindedId _ i -> i

symOf :: Sign f e -> SymbolSet

symOf sigma = let

sorts = Set.map idToSortSymbol $ sortSet sigma

ops = Set.fromList $

concatMap (\ (i, ts) -> map ( \ t -> idToOpSymbol i t) $ Set.toList ts)

$ Map.toList $ opMap sigma

preds = Set.fromList $

concatMap (\ (i, ts) -> map ( \ t -> idToPredSymbol i t)

$ Set.toList ts) $ Map.toList $ predMap sigma

in Set.unions [sorts, ops, preds]

statSymbMapItems :: [SYMB_MAP_ITEMS] -> Result RawSymbolMap

statSymbMapItems sl = do

ls <- sequence $ map s1 sl

foldl insertRsys (return Map.empty) (concat ls)

where

s1 (Symb_map_items kind l _) = sequence (map (symbOrMapToRaw kind) l)

insertRsys m (rsy1,rsy2) = do

m1 <- m

case Map.lookup rsy1 m1 of

Nothing -> return $ Map.insert rsy1 rsy2 m1

Just rsy3 ->

plain_error m1 ("Symbol " ++ showDoc rsy1 " mapped twice to "

++ showDoc rsy2 " and " ++ showDoc rsy3 "") nullRange

symbOrMapToRaw :: SYMB_KIND -> SYMB_OR_MAP -> Result (RawSymbol, RawSymbol)

symbOrMapToRaw k sm = do

let (u, v) = case sm of

Symb s -> (s, s)

Symb_map s t _ -> (s, t)

w <- symbToRaw k u

x <- symbToRaw k v

return (w, x)

statSymbItems :: [SYMB_ITEMS] -> Result [RawSymbol]

statSymbItems sl =

fmap concat (sequence (map s1 sl))

where s1 (Symb_items kind l _) = sequence (map (symbToRaw kind) l)

symbToRaw :: SYMB_KIND -> SYMB -> Result RawSymbol

symbToRaw k si = case si of

Symb_id idt -> return $ symbKindToRaw k idt

Qual_id idt t _ -> typedSymbKindToRaw k idt t

symbKindToRaw :: SYMB_KIND -> Id -> RawSymbol

symbKindToRaw sk idt = case sk of

Implicit -> AnID idt

_ -> AKindedId (case sk of

Sorts_kind -> SortKind

Preds_kind -> PredKind

_ -> FunKind) idt

typedSymbKindToRaw :: SYMB_KIND -> Id -> TYPE -> Result RawSymbol

typedSymbKindToRaw k idt t = let

err = plain_error (AnID idt)

(showDoc idt ":" ++ showDoc t

"does not have kind" ++ showDoc k "") nullRange

aSymb = ASymbol $ case t of

O_type ot -> idToOpSymbol idt $ toOpType ot

P_type pt -> idToPredSymbol idt $ toPredType pt

-- in case of ambiguity, return a constant function type

-- this deviates from the CASL summary !!!

A_type s ->

let ot = OpType {opKind = Total, opArgs = [], opRes = s}

in idToOpSymbol idt ot

in case k of

Implicit -> return aSymb

Sorts_kind -> err

Ops_kind -> case t of

P_type _ -> err

_ -> return aSymb

Preds_kind -> case t of

O_type _ -> err

A_type s -> return $ ASymbol $

let pt = PredType {predArgs = [s]}

in idToPredSymbol idt pt

P_type _ -> return aSymb

symbMapToMorphism :: m -> Sign f e -> Sign f e

-> SymbolMap -> Result (Morphism f e m)

symbMapToMorphism extEm sigma1 sigma2 smap = let

sort_map1 = Set.fold mapMSort Map.empty (sortSet sigma1)

mapMSort s m =

case Map.lookup (Symbol {symName = s, symbType = SortAsItemType}) smap

of Just sym -> let t = symName sym in if s == t then m else

Map.insert s t m

Nothing -> m

fun_map1 = Map.foldWithKey mapFun Map.empty (opMap sigma1)

pred_map1 = Map.foldWithKey mapPred Map.empty (predMap sigma1)

mapFun i ots m = Set.fold (insFun i) m ots

insFun i ot m =

case Map.lookup (Symbol {symName = i, symbType = OpAsItemType ot}) smap

of Just sym -> let j = symName sym in case symbType sym of

OpAsItemType oty -> let k = opKind oty in

if j == i && opKind ot == k then m

else Map.insert (i, ot {opKind = Partial}) (j, k) m

_ -> m

_ -> m

mapPred i pts m = Set.fold (insPred i) m pts

insPred i pt m =

case Map.lookup (Symbol {symName = i, symbType = PredAsItemType pt}) smap

of Just sym -> let j = symName sym in case symbType sym of

PredAsItemType _ -> if i == j then m else Map.insert (i, pt) j m

_ -> m

_ -> m

in return (embedMorphism extEm sigma1 sigma2)

{ sort_map = sort_map1

, fun_map = fun_map1

, pred_map = pred_map1 }

morphismToSymbMap :: Morphism f e m -> SymbolMap

morphismToSymbMap mor = let

src = msource mor

sorts = sort_map mor

ops = fun_map mor

preds = pred_map mor

sortSymMap = Set.fold ( \ s -> Map.insert (idToSortSymbol s) $

idToSortSymbol $ mapSort sorts s)

Map.empty $ sortSet src

opSymMap = Map.foldWithKey

( \ i s m -> Set.fold

( \ t -> Map.insert (idToOpSymbol i t)

$ uncurry idToOpSymbol $ mapOpSym sorts ops (i, t)) m s)

Map.empty $ opMap src

predSymMap = Map.foldWithKey

( \ i s m -> Set.fold

( \ t -> Map.insert (idToPredSymbol i t)

$ uncurry idToPredSymbol $ mapPredSym sorts preds (i, t)) m s)

Map.empty $ predMap src

in

foldr Map.union sortSymMap [opSymMap, predSymMap]

matches :: Symbol -> RawSymbol -> Bool

matches x@(Symbol idt k) rs = case rs of

ASymbol y -> x == y

AnID di -> idt == di

AKindedId rk di -> let res = idt == di in case (k, rk) of

(SortAsItemType, SortKind) -> res

(OpAsItemType _, FunKind) -> res

(PredAsItemType _, PredKind) -> res

_ -> False

idMor :: m -> Sign f e -> Morphism f e m

idMor extEm sigma = embedMorphism extEm sigma sigma

compose :: (Eq e, Eq f) => (m -> m -> m)

-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)

compose comp mor1 mor2 = if mtarget mor1 == msource mor2 then

let sMap1 = sort_map mor1

src = msource mor1

tar = mtarget mor2

fMap1 = fun_map mor1

pMap1 = pred_map mor1

sMap2 = sort_map mor2

fMap2 = fun_map mor2

pMap2 = pred_map mor2

sMap = if Map.null sMap2 then sMap1 else

Set.fold ( \ i ->

let j = mapSort sMap2 (mapSort sMap1 i) in

if i == j then id else Map.insert i j)

Map.empty $ sortSet src

in return (embedMorphism (error "CASL.Morphism.compose") src tar)

{ sort_map = sMap

, fun_map = if Map.null fMap2 then fMap1 else

Map.foldWithKey ( \ i t m ->

Set.fold ( \ ot ->

let (ni, nt) = mapOpSym sMap2 fMap2 $

mapOpSym sMap1 fMap1 (i, ot)

k = opKind nt

in assert (mapOpTypeK sMap k ot == nt) $

if i == ni && opKind ot == k then id else

Map.insert (i, ot {opKind = Partial }) (ni, k)) m t)

Map.empty $ opMap src

, pred_map = if Map.null pMap2 then pMap1 else

Map.foldWithKey ( \ i t m ->

Set.fold ( \ pt ->

let (ni, nt) = mapPredSym sMap2 pMap2 $

mapPredSym sMap1 pMap1 (i, pt)

in assert (mapPredType sMap pt == nt) $

if i == ni then id else Map.insert (i, pt) ni) m t)

Map.empty $ predMap src

, extended_map = comp (extended_map mor1) (extended_map mor2) }

else fail "target of first and source of second morphism are different"

legalSign :: Sign f e -> Bool

legalSign sigma =

Map.foldWithKey (\s sset b -> b && legalSort s && all legalSort

(Set.toList sset))

True (Rel.toMap (sortRel sigma))

&& Map.fold (\ts b -> b && all legalOpType (Set.toList ts))

True (opMap sigma)

&& Map.fold (\ts b -> b && all legalPredType (Set.toList ts))

True (predMap sigma)

where sorts = sortSet sigma

legalSort s = Set.member s sorts

legalOpType t = legalSort (opRes t)

&& all legalSort (opArgs t)

legalPredType t = all legalSort (predArgs t)

legalMor :: Morphism f e m -> Bool

legalMor mor =

let s1 = msource mor

s2 = mtarget mor

smap = sort_map mor

msorts = Set.map (mapSort smap) $ sortSet s1

mops = Map.foldWithKey ( \ i ->

flip $ Set.fold ( \ ot ->

let (j, nt) = mapOpSym smap (fun_map mor) (i, ot)

in Rel.setInsert j nt)) Map.empty $ opMap s1

mpreds = Map.foldWithKey ( \ i ->

flip $ Set.fold ( \ pt ->

let (j, nt) = mapPredSym smap (pred_map mor) (i, pt)

in Rel.setInsert j nt)) Map.empty $ predMap s1

in legalSign s1

&& Set.isSubsetOf msorts (sortSet s2)

&& isSubOpMap mops (opMap s2)

&& isSubMapSet mpreds (predMap s2)

&& legalSign s2

sigInclusion :: m -- ^ compute extended morphism

-> (e -> e -> Bool) -- ^ subsignature test of extensions

-> Sign f e -> Sign f e -> Result (Morphism f e m)

sigInclusion extEm isSubExt sigma1 sigma2 =

assert (isSubSig isSubExt sigma1 sigma2) $

return (embedMorphism extEm sigma1 sigma2)

morphismUnion :: (m -> m -> m) -- ^ join morphism extensions

-> (e -> e -> e) -- ^ join signature extensions

-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)

-- consider identity mappings but filter them eventually

morphismUnion uniteM addSigExt mor1 mor2 =

let smap1 = sort_map mor1

smap2 = sort_map mor2

s1 = msource mor1

s2 = msource mor2

us1 = Set.difference (sortSet s1) $ Map.keysSet smap1

us2 = Set.difference (sortSet s2) $ Map.keysSet smap2

omap1 = fun_map mor1

omap2 = fun_map mor2

uo1 = foldr delOp (opMap s1) $ Map.keys omap1

uo2 = foldr delOp (opMap s2) $ Map.keys omap2

delOp (n, ot) m = diffMapSet m $ Map.singleton n $

Set.fromList [ot {opKind = Partial}, ot {opKind =Total}]

uo = addMapSet uo1 uo2

pmap1 = pred_map mor1

pmap2 = pred_map mor2

up1 = foldr delPred (predMap s1) $ Map.keys pmap1

up2 = foldr delPred (predMap s2) $ Map.keys pmap2

up = addMapSet up1 up2

delPred (n, pt) m = diffMapSet m $ Map.singleton n $ Set.singleton pt

(sds, smap) = foldr ( \ (i, j) (ds, m) -> case Map.lookup i m of

Nothing -> (ds, Map.insert i j m)

Just k -> if j == k then (ds, m) else

(Diag Error

("incompatible mapping of sort " ++ showId i " to "

++ showId j " and " ++ showId k "")

nullRange : ds, m)) ([], smap1)

(Map.toList smap2 ++ map (\ a -> (a, a))

(Set.toList $ Set.union us1 us2))

(ods, omap) = foldr ( \ (isc@(i, ot), jsc@(j, t)) (ds, m) ->

case Map.lookup isc m of

Nothing -> (ds, Map.insert isc jsc m)

Just (k, p) -> if j == k then if p == t then (ds, m)

else (ds, Map.insert isc (j, Total) m) else

(Diag Error

("incompatible mapping of op " ++ showId i ":"

++ showDoc ot { opKind = t } " to "

++ showId j " and " ++ showId k "") nullRange : ds, m))

(sds, omap1) (Map.toList omap2 ++ concatMap

( \ (a, s) -> map ( \ ot -> ((a, ot {opKind = Partial}),

(a, opKind ot)))

$ Set.toList s) (Map.toList uo))

(pds, pmap) = foldr ( \ (isc@(i, pt), j) (ds, m) ->

case Map.lookup isc m of

Nothing -> (ds, Map.insert isc j m)

Just k -> if j == k then (ds, m) else

(Diag Error

("incompatible mapping of pred " ++ showId i ":"

++ showDoc pt " to " ++ showId j " and "

++ showId k "") nullRange : ds, m)) (ods, pmap1)

(Map.toList pmap2 ++ concatMap ( \ (a, s) -> map

( \ pt -> ((a, pt), a)) $ Set.toList s) (Map.toList up))

s3 = addSig addSigExt s1 s2

o3 = opMap s3 in

if null pds then Result [] $ Just

(embedMorphism (error "CASL.Morphism.morphismUnion")

s3 $ addSig addSigExt (mtarget mor1) $ mtarget mor2)

{ sort_map = Map.filterWithKey (/=) smap

, fun_map = Map.filterWithKey

(\ (i, ot) (j, k) -> i /= j || k == Total && Set.member ot

(Map.findWithDefault Set.empty i o3)) omap

, pred_map = Map.filterWithKey (\ (i, _) j -> i /= j) pmap

, extended_map = uniteM (extended_map mor1) $ extended_map mor2 }

else Result pds Nothing

isSortInjective :: Morphism f e m -> Bool

isSortInjective m =

null [() | k1 <- src, k2 <-src, k1 /= k2,

(Map.lookup k1 sm::Maybe SORT)==Map.lookup k2 sm]

where sm = sort_map m

src = Map.keys sm

isInjective :: Morphism f e m -> Bool

isInjective m =

null [() | k1 <- src, k2 <-src, k1 /= k2,

(Map.lookup k1 symmap::Maybe Symbol)==Map.lookup k2 symmap]

where src = Map.keys symmap

symmap = morphismToSymbMap m

instance Pretty Kind where

pretty k = keyword $ case k of

SortKind -> sortS

FunKind -> opS

PredKind -> predS

instance Pretty RawSymbol where

pretty rsym = case rsym of

ASymbol sy -> pretty sy

AnID i -> pretty i

AKindedId k i -> pretty k <+> pretty i

printMorphism :: (f->Doc) -> (e->Doc) -> (m->Doc) -> Morphism f e m -> Doc

printMorphism fF fE fM mor =

pretty (Map.filterWithKey (/=) $ morphismToSymbMap mor)

$+$ fM (extended_map mor) $+$ colon $+$

specBraces (space <> printSign fF fE (msource mor) <> space)

$+$ text funS $+$

specBraces (space <> printSign fF fE (mtarget mor) <> space)

instance (Pretty e, Pretty f, Pretty m) =>

Pretty (Morphism f e m) where

pretty = printMorphism pretty pretty pretty