97a9a944b5887e91042b019776c41d5dd74557aferikabele{- |

97a9a944b5887e91042b019776c41d5dd74557aferikabeleModule : $Header$

97a9a944b5887e91042b019776c41d5dd74557aferikabeleDescription : symbol map analysis for the CASL logic.

a945f35eff8b6a88009ce73de6d4c862ce58de3csliveCopyright : (c) Till Mossakowski, C. Maeder and Uni Bremen 2002-2005

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

a945f35eff8b6a88009ce73de6d4c862ce58de3cslive

5a58787efeb02a1c3f06569d019ad81fd2efa06endMaintainer : Christian.Maeder@dfki.de

5a58787efeb02a1c3f06569d019ad81fd2efa06endStability : provisional

5a58787efeb02a1c3f06569d019ad81fd2efa06endPortability : portable

5a58787efeb02a1c3f06569d019ad81fd2efa06end

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowenSymbol map analysis for the CASL logic.

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen Follows Sect. III:4.1 of the CASL Reference Manual.

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen-}

d29d9ab4614ff992b0e8de6e2b88d52b6f1f153erbowen

5a58787efeb02a1c3f06569d019ad81fd2efa06endmodule CASL.SymbolMapAnalysis

5a58787efeb02a1c3f06569d019ad81fd2efa06end ( inducedFromMorphism

5a58787efeb02a1c3f06569d019ad81fd2efa06end , inducedFromToMorphism

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen , inducedFromMorphismExt

3f08db06526d6901aa08c110b5bc7dde6bc39905nd , inducedFromToMorphismExt

5a58787efeb02a1c3f06569d019ad81fd2efa06end , cogeneratedSign

5a58787efeb02a1c3f06569d019ad81fd2efa06end , generatedSign

5a58787efeb02a1c3f06569d019ad81fd2efa06end , finalUnion

3f08db06526d6901aa08c110b5bc7dde6bc39905nd , constMorphExt

5a58787efeb02a1c3f06569d019ad81fd2efa06end ) where

a63f0ab647ad2ab72efc9bea7a66e24e9ebc5cc2nd

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport CASL.Sign

ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7ndimport CASL.AS_Basic_CASL

ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7ndimport CASL.Morphism

e1e8390280254f7f0580d701e583f670643d4f3fnilgunimport CASL.Overload (leqF, leqP)

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung

3b3b7fc78d1f5bfc2769903375050048ff41ff26ndimport qualified Data.Map as Map

5a58787efeb02a1c3f06569d019ad81fd2efa06endimport qualified Data.Set as Set

5a58787efeb02a1c3f06569d019ad81fd2efa06endimport qualified Common.Lib.Rel as Rel

5a58787efeb02a1c3f06569d019ad81fd2efa06endimport Common.Doc

5a58787efeb02a1c3f06569d019ad81fd2efa06endimport Common.DocUtils

5a58787efeb02a1c3f06569d019ad81fd2efa06endimport Common.ExtSign

5a58787efeb02a1c3f06569d019ad81fd2efa06endimport Common.Id

5a58787efeb02a1c3f06569d019ad81fd2efa06endimport Common.Result

06ba4a61654b3763ad65f52283832ebf058fdf1cslive

ced7ef1f8c0df1805da0e87dbc5a1b6282910573ndimport Data.List (partition, find)

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveimport Data.Maybe (catMaybes, isJust)

ced7ef1f8c0df1805da0e87dbc5a1b6282910573nd

b21197dc8e6b8c764fdcc24d4bae8b0eebb6bc4end{-

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveinducedFromMorphism :: RawSymbolMap -> sign -> Result morphism

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveHere is Bartek Klin's algorithm that has benn used for CATS.

97a9a944b5887e91042b019776c41d5dd74557aferikabeleOur algorithm deviates from it. The exact details need to be checked.

f8396ed8364b56ec8adeaa49cac35a929758a29eslive

ffb01336be79c64046b636e59fa8ddca8ec029edsfInducing morphism from raw symbol map and signature

f8396ed8364b56ec8adeaa49cac35a929758a29eslive

f8396ed8364b56ec8adeaa49cac35a929758a29esliveInput: raw symbol map "Rsm"

5a58787efeb02a1c3f06569d019ad81fd2efa06end signature "Sigma1"

5a58787efeb02a1c3f06569d019ad81fd2efa06endOutput: morphims "Mrph": Sigma1 -> "Sigma2".

5a58787efeb02a1c3f06569d019ad81fd2efa06end

5a58787efeb02a1c3f06569d019ad81fd2efa06end//preparation

deeee6bb6fd94c0ba5f3730b58abd9d299c89ccdnd1. let "Ssm" be an empty list of pairs (symbol, raw symbol).

4db28ee269aa06f7c6232e11cd01f58c3349af23noodl2. for each pair "Rsym1,Rsym2" in Rsm do:

117c1f888a14e73cdd821dc6c23eb0411144a41cnd 2.1. if there is no symbol in Sigma1 matching Rsym1, return error.

117c1f888a14e73cdd821dc6c23eb0411144a41cnd 2.2. for each symbol "Sym" from Sigma1 matching Rsym1

4a31db3c3a0202003c1b9f87affa7cc143e120e5sf 2.2.1. add a pair "Sym,Rsym2" to Ssm.

117c1f888a14e73cdd821dc6c23eb0411144a41cnd//computing the "sort part" of the morphism

ffb01336be79c64046b636e59fa8ddca8ec029edsf3. let Sigma2 be an empty signature.

117c1f888a14e73cdd821dc6c23eb0411144a41cnd4. let Mrph be an empty "morphism" from Sigma1 to Sigma2.

117c1f888a14e73cdd821dc6c23eb0411144a41cnd5. for each pair "Sym,Rsym2" in Ssm such that Sym is a sort symbol

117c1f888a14e73cdd821dc6c23eb0411144a41cnd 5.1. if Rsym2 is not a sort raw symbol, return error.

2bc7f1cf720973a67f8ff7a8d523e40569ae5b6cnd 5.2. if in Mrph there is a mapping of sort in Sym to sort with

117c1f888a14e73cdd821dc6c23eb0411144a41cnd name other than that in Rsym2, return error.

117c1f888a14e73cdd821dc6c23eb0411144a41cnd 5.3. if in Mrph there is no mappinh of sort in Sym

117c1f888a14e73cdd821dc6c23eb0411144a41cnd 5.3.1. add sort from Rsym2 to Sigma2

117c1f888a14e73cdd821dc6c23eb0411144a41cnd 5.3.2. add mapping from sort(Sym) to sort(Rsym2) to Mrph.

117c1f888a14e73cdd821dc6c23eb0411144a41cnd6. for each sort symbol "S" in Sigma1

117c1f888a14e73cdd821dc6c23eb0411144a41cnd 6.1. if S is not mapped by Mrph,

87ffb6e33f3cbef3b9bb406cc2d27039fa336eaatrawick 6.1.1. add sort S to Sigma2

4db28ee269aa06f7c6232e11cd01f58c3349af23noodl 6.1.2. add mapping from S to S to Mrph.

5a58787efeb02a1c3f06569d019ad81fd2efa06end//computing the "function/predicate part" of the morphism

5a58787efeb02a1c3f06569d019ad81fd2efa06end7. for each pair "Sym,Rsym2" in Ssm such that Sym is a function/predicate

5a58787efeb02a1c3f06569d019ad81fd2efa06end symbol

5a58787efeb02a1c3f06569d019ad81fd2efa06end 7.1. let "F" be name contained in Sym, let "Fprof" be the profile.

5a58787efeb02a1c3f06569d019ad81fd2efa06end 7.2. let "Fprof1" be the value of Fprof via Mrph

5a58787efeb02a1c3f06569d019ad81fd2efa06end (it can be computed, as we already have the "sort" part of

654d8eb036bedc99e90e11910ee02d3421417697rbowen morphism)

30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh 7.3. if Rsym2 is not of appriopriate type, return error, otherwise

5a58787efeb02a1c3f06569d019ad81fd2efa06end let "F2" be the name of the symbol.

5a58787efeb02a1c3f06569d019ad81fd2efa06end 7.4. if Rsym2 enforces the profile of the symbol (i.e., it is not

5a58787efeb02a1c3f06569d019ad81fd2efa06end an implicit symbol), compare the profile to Fprof1. If it is

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf not equal, return error.

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick 7.5. if in Mrph there is a mapping of F1 with profile Fprof to

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick some name different than F2, return error.

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick 7.6. add an operation/predicate with name F2 and profile Fprof1 to

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick Sigma2. If it is a partial function and if in Sigma2 there

06ba4a61654b3763ad65f52283832ebf058fdf1cslive exists a total function with the same name and profile, do not

654d8eb036bedc99e90e11910ee02d3421417697rbowen add it. Otherwise if it is a total function and if in Sigma2

06ba4a61654b3763ad65f52283832ebf058fdf1cslive there exists a partial function with the same name and profile,

06ba4a61654b3763ad65f52283832ebf058fdf1cslive add the total function removing the partial one.

06ba4a61654b3763ad65f52283832ebf058fdf1cslive 7.7. add to Mrph a mapping from operation/predicate of name F1 and

b1b0d8ff12f69d873f28a9bf79dfba6b67b45a4bigalic profile Fprof to name F2.

97a9a944b5887e91042b019776c41d5dd74557aferikabele8. for each operation/predicate symbol "F" with profile "Fprof" in Sigma1

654d8eb036bedc99e90e11910ee02d3421417697rbowen that is not mapped by Mrph,

92510838f2eb125726e15c5eb4f7a23c7a0396e4slive 8.1. as in 7.2

97a9a944b5887e91042b019776c41d5dd74557aferikabele 8.2. as in 7.6, replacing F2 with F1.

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive 8.3. as in 7.7, replacing F2 with F1.

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive9. for each sort relation "S1,S2" in Sigma1,

92510838f2eb125726e15c5eb4f7a23c7a0396e4slive 9.1. compute S3=(S1 via Mrph) and S4=(S2 via Mrph)

92510838f2eb125726e15c5eb4f7a23c7a0396e4slive 9.2. add sort relation "S3,S4" in Sigma2.

ffb01336be79c64046b636e59fa8ddca8ec029edsf10. Compute transitive closure of subsorting relation in Sigma2.

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick-}

ffb01336be79c64046b636e59fa8ddca8ec029edsf

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawicktype InducedMorphism e m = RawSymbolMap -> e -> Result m

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawickconstMorphExt :: m -> InducedMorphism e m

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawickconstMorphExt m _ _ = return m

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfinducedFromMorphism :: (Pretty e, Show f) => m -> RawSymbolMap -> Sign f e

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick -> Result (Morphism f e m)

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsfinducedFromMorphism =

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf inducedFromMorphismExt (\ _ _ _ _ -> extendedInfo) . constMorphExt

ffb01336be79c64046b636e59fa8ddca8ec029edsf

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawickinducedFromMorphismExt :: (Pretty e, Show f) => InducedSign f e m e

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf -> InducedMorphism e m

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick -> RawSymbolMap -> Sign f e -> Result (Morphism f e m)

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawickinducedFromMorphismExt extInd extEm rmap sigma = do

77c77cf89621f21c8e2bbad63058b5eaa5f88d4ajim -- ??? Missing: check preservation of overloading relation

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick -- compute the sort map (as a Map)

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf sort_Map <- Set.fold (\ s m -> do

ced7ef1f8c0df1805da0e87dbc5a1b6282910573nd s' <- sortFun rmap s

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick m1 <- m

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf return $ if s' == s then m1 else Map.insert s s' m1)

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf (return Map.empty) (sortSet sigma)

9a58dc6a2b26ec128b1270cf48810e705f1a90dbsf -- compute the op map (as a Map)

ced7ef1f8c0df1805da0e87dbc5a1b6282910573nd op_Map <- Map.foldWithKey (opFun sigma rmap sort_Map)

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick (return Map.empty) (opMap sigma)

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick -- compute the pred map (as a Map)

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick pred_Map <- Map.foldWithKey (predFun sigma rmap sort_Map)

4a31db3c3a0202003c1b9f87affa7cc143e120e5sf (return Map.empty) (predMap sigma)

4a31db3c3a0202003c1b9f87affa7cc143e120e5sf em <- extEm rmap $ extendedInfo sigma

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick -- return assembled morphism

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick return (embedMorphism em sigma $ closeSortRel

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick $ inducedSignAux extInd sort_Map op_Map pred_Map em sigma)

ffb01336be79c64046b636e59fa8ddca8ec029edsf { sort_map = sort_Map

8a6d5edcb07aeccca7afba02a17dd6904d6b206ctrawick , op_map = op_Map

92510838f2eb125726e15c5eb4f7a23c7a0396e4slive , pred_map = pred_Map }

92510838f2eb125726e15c5eb4f7a23c7a0396e4slive

97a9a944b5887e91042b019776c41d5dd74557aferikabele -- the sorts of the source signature

92510838f2eb125726e15c5eb4f7a23c7a0396e4slive -- sortFun is the sort map as a Haskell function

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalicsortFun :: RawSymbolMap -> Id -> Result Id

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalicsortFun rmap s =

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic -- rsys contains the raw symbols to which s is mapped to

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic if Set.null rsys then return s -- use default = identity mapping

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic else if Set.null $ Set.deleteMin rsys then

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic return $ rawSymName $ Set.findMin rsys -- take the unique rsy

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic else plain_error s -- ambiguity! generate an error

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic ("sort " ++ showId s

f0fa55ff14fa0bf8fd72d989f6625de6dc3260c8igalic " is mapped ambiguously: " ++ showDoc rsys "")

06ba4a61654b3763ad65f52283832ebf058fdf1cslive $ getRange rsys

e8d485701957d5c6de870111c112e168a894d49and where

e8d485701957d5c6de870111c112e168a894d49and -- get all raw symbols to which s is mapped to

654d8eb036bedc99e90e11910ee02d3421417697rbowen rsys = Set.fromList $ catMaybes $ map (flip Map.lookup rmap)

654d8eb036bedc99e90e11910ee02d3421417697rbowen [ ASymbol $ idToSortSymbol s

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive , AKindedSymb Implicit s ]

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive

9bcfc3697a91b5215893a7d0206865b13fc72148nd {- to a Op_map, add everything resulting from mapping (id, ots)

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive according to rmap -}

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7sliveopFun :: Sign f e -> RawSymbolMap -> Sort_map -> Id -> Set.Set OpType

06ba4a61654b3763ad65f52283832ebf058fdf1cslive -> Result Op_map -> Result Op_map

4a31db3c3a0202003c1b9f87affa7cc143e120e5sfopFun src rmap sort_Map ide ots m =

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive -- first consider all directly mapped profiles

9b6a3a558cc90ffdaa0b50bd02546ffec424ded7slive let otls = Rel.partSet (leqF src) ots

709e3a21ba73b8433462959cd56c773454b34441trawick m1 = foldr (directOpMap rmap sort_Map ide) m otls

709e3a21ba73b8433462959cd56c773454b34441trawick -- now try the remaining ones with (un)kinded raw symbol

709e3a21ba73b8433462959cd56c773454b34441trawick in case (Map.lookup (AKindedSymb Ops_kind ide) rmap,

709e3a21ba73b8433462959cd56c773454b34441trawick Map.lookup (AKindedSymb Implicit ide) rmap) of

709e3a21ba73b8433462959cd56c773454b34441trawick (Just rsy1, Just rsy2) -> let

709e3a21ba73b8433462959cd56c773454b34441trawick m2 = Set.fold (insertmapOpSym sort_Map ide rsy1) m1 ots

709e3a21ba73b8433462959cd56c773454b34441trawick in Set.fold (insertmapOpSym sort_Map ide rsy2) m2 ots

5a58787efeb02a1c3f06569d019ad81fd2efa06end (Just rsy, Nothing) ->

5a58787efeb02a1c3f06569d019ad81fd2efa06end Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots

3b3b7fc78d1f5bfc2769903375050048ff41ff26nd (Nothing, Just rsy) ->

ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7nd Set.fold (insertmapOpSym sort_Map ide rsy) m1 ots

ad74a0524a06bfe11b7de9e3b4ce7233ab3bd3f7nd -- Anything not mapped explicitly is left unchanged

e1e8390280254f7f0580d701e583f670643d4f3fnilgun (Nothing, Nothing) -> m1

f086b4b402fa9a2fefc7dda85de2a3cc1cd0a654rjung

727872d18412fc021f03969b8641810d8896820bhumbedooh -- try to map an operation symbol directly

0d0ba3a410038e179b695446bb149cce6264e0abnd -- collect all opTypes that cannot be mapped directly

727872d18412fc021f03969b8641810d8896820bhumbedoohdirectOpMap :: RawSymbolMap -> Sort_map -> Id -> Set.Set OpType

cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh -> Result Op_map -> Result Op_map

0d0ba3a410038e179b695446bb149cce6264e0abnddirectOpMap rmap sort_Map ide' ots m' =

cc7e1025de9ac63bd4db6fe7f71c158b2cf09fe4humbedooh let ol = Set.toList ots

727872d18412fc021f03969b8641810d8896820bhumbedooh rl = map (lookupOpSymbol rmap ide') ol

0d0ba3a410038e179b695446bb149cce6264e0abnd in case catMaybes rl of

0d0ba3a410038e179b695446bb149cce6264e0abnd [] -> m'

0d0ba3a410038e179b695446bb149cce6264e0abnd rsy : _ -> foldr (\ (ot, mrsy) m ->

ac082aefa89416cbdc9a1836eaf3bed9698201c8humbedooh insertmapOpSym sort_Map ide'

0d0ba3a410038e179b695446bb149cce6264e0abnd (case mrsy of

0d0ba3a410038e179b695446bb149cce6264e0abnd Nothing -> AKindedSymb Implicit $ rawSymName rsy

0d0ba3a410038e179b695446bb149cce6264e0abnd Just rsy2 -> rsy2) ot m) m' $ zip ol rl

727872d18412fc021f03969b8641810d8896820bhumbedooh

0d0ba3a410038e179b695446bb149cce6264e0abndlookupOpSymbol :: RawSymbolMap -> Id -> OpType -> Maybe RawSymbol

0d0ba3a410038e179b695446bb149cce6264e0abndlookupOpSymbol rmap ide' ot = let mkS = idToOpSymbol ide' in

30471a4650391f57975f60bbb6e4a90be7b284bfhumbedooh case Map.lookup (ASymbol (mkS $ mkPartial ot)) rmap of

1a1356f375e36db7bee379ea0684ab389579f798rbowen Nothing -> Map.lookup

af33a4994ae2ff15bc67d19ff1a7feb906745bf8rbowen (ASymbol (mkS $ mkTotal ot)) rmap

0d0ba3a410038e179b695446bb149cce6264e0abnd res -> res

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd

7fec19672a491661b2fe4b29f685bc7f4efa64d4nd -- map op symbol (ide, ot) to raw symbol rsy

7fec19672a491661b2fe4b29f685bc7f4efa64d4ndmappedOpSym :: Sort_map -> Id -> OpType -> RawSymbol -> Result (Id, OpKind)

5a58787efeb02a1c3f06569d019ad81fd2efa06endmappedOpSym sort_Map ide ot rsy =

let opSym = "operation symbol " ++ showDoc (idToOpSymbol ide ot)

" is mapped to "

kind = opKind ot

in case rsy of

ASymbol (Symbol ide' (OpAsItemType ot')) ->

if compatibleOpTypes (mapOpType sort_Map ot) ot'

then return (ide', opKind ot')

else plain_error (ide, kind)

(opSym ++ "type " ++ showDoc ot'

" but should be mapped to type " ++

showDoc (mapOpType sort_Map ot)"") $ getRange rsy

AKindedSymb k ide' | elem k [Implicit, Ops_kind] -> return (ide', kind)

_ -> plain_error (ide, kind)

(opSym ++ "symbol of wrong kind: " ++ showDoc rsy "")

$ getRange rsy

-- insert mapping of op symbol (ide, ot) to raw symbol rsy into m

insertmapOpSym :: Sort_map -> Id -> RawSymbol -> OpType

-> Result Op_map -> Result Op_map

insertmapOpSym sort_Map ide rsy ot m = do

m1 <- m

(ide', kind') <- mappedOpSym sort_Map ide ot rsy

let otsy = Symbol ide $ OpAsItemType ot

pos = getRange rsy

m2 = Map.insert (ide, mkPartial ot) (ide', kind') m1

case Map.lookup (ide, mkPartial ot) m1 of

Nothing -> if ide == ide' && kind' == opKind ot then

case rsy of

ASymbol _ -> return m1

_ -> hint m1 ("identity mapping of "

++ showDoc otsy "") pos

else return m2

Just (ide'', kind'') -> if ide' == ide'' then

warning (if kind' < kind'' then m2 else m1)

("ignoring duplicate mapping of " ++ showDoc otsy "")

pos

else plain_error m1

("conflicting mapping of " ++ showDoc otsy " to " ++

show ide' ++ " and " ++ show ide'') pos

{- to a Pred_map, add evering resulting from mapping (ide,pts)

according to rmap -}

predFun :: Sign f e -> RawSymbolMap -> Sort_map -> Id -> Set.Set PredType

-> Result Pred_map -> Result Pred_map

predFun src rmap sort_Map ide pts m =

-- first consider all directly mapped profiles

let ptls = Rel.partSet (leqP src) pts

m1 = foldr (directPredMap rmap sort_Map ide) m ptls

-- now try the remaining ones with (un)kinded raw symbol

in case (Map.lookup (AKindedSymb Preds_kind ide) rmap,

Map.lookup (AKindedSymb Implicit ide) rmap) of

(Just rsy1, Just rsy2) -> let

m2 = Set.fold (insertmapPredSym sort_Map ide rsy1) m1 pts

in Set.fold (insertmapPredSym sort_Map ide rsy2) m2 pts

(Just rsy, Nothing) ->

Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts

(Nothing, Just rsy) ->

Set.fold (insertmapPredSym sort_Map ide rsy) m1 pts

-- Anything not mapped explicitly is left unchanged

(Nothing, Nothing) -> m1

-- try to map a predicate symbol directly

-- collect all predTypes that cannot be mapped directly

directPredMap :: RawSymbolMap -> Sort_map -> Id -> Set.Set PredType

-> Result Pred_map -> Result Pred_map

directPredMap rmap sort_Map ide pts m' =

let pl = Set.toList pts

rl = map (\ pt -> Map.lookup (ASymbol $ idToPredSymbol ide pt) rmap) pl

in case catMaybes rl of

[] -> m'

rsy : _ -> foldr (\ (pt, mrsy) m ->

insertmapPredSym sort_Map ide

(case mrsy of

Nothing -> AKindedSymb Implicit $ rawSymName rsy

Just rsy2 -> rsy2) pt m) m' $ zip pl rl

-- map pred symbol (ide,pt) to raw symbol rsy

mappedPredSym :: Sort_map -> Id -> PredType -> RawSymbol -> Result Id

mappedPredSym sort_Map ide pt rsy =

let predSym = "predicate symbol " ++ showDoc (idToPredSymbol ide pt)

" is mapped to "

in case rsy of

ASymbol (Symbol ide' (PredAsItemType pt')) ->

if mapPredType sort_Map pt == pt'

then return ide'

else plain_error ide

(predSym ++ "type " ++ showDoc pt'

" but should be mapped to type " ++

showDoc (mapPredType sort_Map pt) "") $ getRange rsy

AKindedSymb k ide' | elem k [Implicit, Preds_kind] -> return ide'

_ -> plain_error ide

(predSym ++ "symbol of wrong kind: " ++ showDoc rsy "")

$ getRange rsy

-- insert mapping of pred symbol (ide,pt) to raw symbol rsy into m

insertmapPredSym :: Sort_map -> Id -> RawSymbol -> PredType

-> Result Pred_map -> Result Pred_map

insertmapPredSym sort_Map ide rsy pt m = do

m1 <- m

ide' <- mappedPredSym sort_Map ide pt rsy

let ptsy = Symbol ide $ PredAsItemType pt

pos = getRange rsy

m2 = Map.insert (ide, pt) ide' m1

case Map.lookup (ide, pt) m1 of

Nothing -> if ide == ide' then

case rsy of

ASymbol _ -> return m1

_ -> hint m1 ("identity mapping of "

++ showDoc ptsy "") pos

else return m2

Just ide'' -> if ide' == ide'' then

warning m1

("ignoring duplicate mapping of " ++ showDoc ptsy "") pos

else plain_error m1

("conflicting mapping of " ++ showDoc ptsy " to " ++

show ide' ++ " and " ++ show ide'') pos

{-

inducedFromToMorphism :: RawSymbolMap -> sign -> sign -> Result morphism

Algorithm adapted from Bartek Klin's algorithm for CATS.

Inducing morphisms from raw symbol map and source and target signature.

This problem is NP-hard (The problem of 3-colouring can be reduced to it).

This means that we have exponential runtime in the worst case.

However, in many cases the runtime can be kept rather short by

using some basic principles of constraint programming.

We use a depth-first search with some weak form of constraint

propagation and MRV (minimum remaining values), see

Stuart Russell and Peter Norvig:

Artificial Intelligence - A Modern Approach.

Prentice Hall International

The algorithm has additionally to take care of default values (i.e.

symbol names are mapped identically be default, and the number of

identitically mapped names should be maximized). Moreover, it does

not suffice to find just one solution, but also its uniqueness

(among those maximizing he number of identitically mapped names)

must be checked (still, MRV is useful here).

The algorithm

Input: raw symbol map "rmap"

signatures "sigma1,sigma2"

Output: morphism "mor": sigma1 -> sigma2

1. compute the morphism mor1 induced by rmap and sigma1 (i.e. the renaming)

1.1. if target mor1 is a subsignature of sigma2, return the composition

of this inclusion with mor1

(cf. Theorem 6 of Bartek Klin's Master's Thesis)

otherwise some heuristics is needed, because merely forgetting one renaming

may lead to unacceptable run-time for signatures with just about 10 symbols

-}

-- the main function

inducedFromToMorphism :: (Eq e, Show f, Pretty e, Pretty m)

=> m -- ^ extended morphism

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

-> (e -> e -> e) -- ^ difference of extensions

-> RawSymbolMap

-> ExtSign (Sign f e) Symbol

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

inducedFromToMorphism =

inducedFromToMorphismExt (\ _ _ _ _ -> extendedInfo) . constMorphExt

inducedFromToMorphismExt :: (Eq e, Show f, Pretty e, Pretty m)

=> InducedSign f e m e

-> InducedMorphism e m -- ^ compute extended morphism

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

-> (e -> e -> e) -- ^ difference of extensions

-> RawSymbolMap

-> ExtSign (Sign f e) Symbol

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

inducedFromToMorphismExt extInd extEm isSubExt diffExt rmap sig1@(ExtSign _ sy1)

sig2@(ExtSign _ sy2) =

let iftm rm = (inducedFromToMorphismAuxExt extInd extEm isSubExt diffExt

rm sig1 sig2, rm)

isOk = isJust . resultToMaybe

res = fst $ iftm rmap

pos = concatMapRange getRange $ Map.keys rmap

in if isOk res then res else

let ss1 = Set.filter (\ s -> Set.null $ Set.filter (\ s2 ->

compatibleSymbols True (s, s2)) sy2)

$ Set.filter (\ s -> not $ any (matches s) $ Map.keys rmap)

$ sy1

combs = pairs (map ASymbol $ Set.toList ss1)

$ map ASymbol $ Set.toList sy2

fcombs = filter (all compatibleRawSymbs) combs

in if null (drop 170 combs) && null (drop 20 fcombs) then

case filter (isOk . fst) $ map (iftm . Map.union rmap . Map.fromList)

fcombs of

[(r, m)] -> (if length fcombs > 1 then warning else hint)

() ("derived symbol map:\n" ++ showDoc m "") pos >> r

(_, m1) : (_, m2) : _ -> fatal_error

("ambiguous symbol map1:\n" ++ showDoc m1 "\n"

++ "ambiguous symbol map2:\n" ++ showDoc m2 "") pos

[] -> res

else warning () "too many possibilities for symbol maps" pos >> res

compatibleSymbTypes :: (SymbType, SymbType) -> Bool

compatibleSymbTypes p = case p of

(SortAsItemType, SortAsItemType) -> True

(OtherTypeKind s1, OtherTypeKind s2) -> s1 == s2

(OpAsItemType t1, OpAsItemType t2) ->

length (opArgs t1) == length (opArgs t2)

(PredAsItemType p1, PredAsItemType p2) ->

length (predArgs p1) == length (predArgs p2)

_ -> False

compatibleSymbols :: Bool -> (Symbol, Symbol) -> Bool

compatibleSymbols alsoId (Symbol i1 k1, Symbol i2 k2) =

compatibleSymbTypes (k1, k2) && (not alsoId || i1 == i2)

compatibleRawSymbs :: (RawSymbol, RawSymbol) -> Bool

compatibleRawSymbs p = case p of

(ASymbol s1, ASymbol s2) -> compatibleSymbols False (s1, s2)

_ -> False -- irrelevant

pairs :: [a] -> [a] -> [[(a, a)]]

pairs l1 = map (zip l1) . takeKFromN l1

takeKFromN :: [b] -> [a] -> [[a]]

takeKFromN s l = case s of

[] -> [[]]

_ : r -> [ a : b | a <- l, b <- takeKFromN r l]

inducedFromToMorphismAuxExt :: (Eq e, Show f, Pretty e, Pretty m)

=> InducedSign f e m e

-> InducedMorphism e m -- ^ compute extended morphism

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

-> (e -> e -> e) -- ^ difference of extensions

-> RawSymbolMap

-> ExtSign (Sign f e) Symbol

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

inducedFromToMorphismAuxExt extInd extEm isSubExt diffExt rmap

(ExtSign sigma1 _) (ExtSign sigma2 _) = do

-- 1. use rmap to get a renaming...

mor1 <- inducedFromMorphismExt extInd extEm rmap sigma1

-- 1.1 ... is the renamed source signature contained in the target signature?

let inducedSign = mtarget mor1

em = extended_map mor1

if isSubSig isSubExt inducedSign sigma2

-- yes => we are done

then composeM (\ _ _ -> return em) mor1 $ idOrInclMorphism

$ embedMorphism em inducedSign sigma2

-- here the empty mapping should be used, but it will be overwritten

-- by the first argument of composeM

else fatal_error

("No signature morphism for symbol map found.\n" ++

"The following mapped symbols are missing in the target signature:\n"

++ showDoc (diffSig diffExt inducedSign sigma2) "")

$ concatMapRange getRange $ Map.keys rmap

{-

Computing signature generated by a symbol set.

Algorithm adapted from Bartek Klin's algorithm for CATS.

Input: symbol set "Syms"

signature "Sigma"

Output: signature "Sigma1"<=Sigma.

1. get a set "Sigma_symbols" of symbols in Sigma.

2. if Syms is not a subset of Sigma_symbols, return error.

3. let Sigma1 be an empty signature.

4. for each symbol "Sym" in Syms do:

4.1. if Sym is a:

4.1.1. sort "S": add sort S to Sigma1.

4.1.2. total function "F" with profile "Fargs,Fres":

4.1.2.1. add all sorts from Fargs to Sigma1.

4.1.2.2. add sort Fres to Sigma1.

4.1.2.3. add F with the needed profile to Sigma1.

4.1.3. partial function: as in 4.1.2.

4.1.4. predicate: as in 4.1.2., except that Fres is omitted.

5. get a list "Sig_sub" of subsort relations in Sigma.

6. for each pair "S1,S2" in Sig_sub do:

6.1. if S1,S2 are sorts in Sigma1, add "S1,S2" to sort relations in

Sigma1.

7. return the inclusion of sigma1 into sigma.

-}

generatedSign :: m -> SymbolSet -> Sign f e

-> Result (Morphism f e m)

generatedSign extEm sys sigma =

if not (sys `Set.isSubsetOf` symset) -- 2.

then let diffsyms = sys Set.\\ symset in

fatal_error ("Revealing: The following symbols "

++ showDoc diffsyms " are not in the signature")

$ getRange diffsyms

else return $ idOrInclMorphism $ embedMorphism extEm sigma2 sigma

-- 7.

where

symset = symOf sigma -- 1.

sigma1 = Set.fold revealSym (sigma { sortSet = Set.empty

, opMap = Map.empty

, predMap = Map.empty }) sys -- 4.

sigma2 = sigma1

{ sortRel = sortRel sigma `Rel.restrict` sortSet sigma1

, emptySortSet = Set.intersection (sortSet sigma1) $ emptySortSet sigma }

revealSym :: Symbol -> Sign f e -> Sign f e

revealSym sy sigma1 = case symbType sy of -- 4.1.

SortAsItemType -> -- 4.1.1.

sigma1 {sortSet = Set.insert (symName sy) $ sortSet sigma1}

OpAsItemType ot -> -- 4.1.2./4.1.3.

sigma1 { sortSet = foldr Set.insert (sortSet sigma1)

$ opRes ot : opArgs ot

, opMap = Rel.setInsert (symName sy) ot $ opMap sigma1 }

PredAsItemType pt -> -- 4.1.4.

sigma1 { sortSet = foldr Set.insert (sortSet sigma1) $ predArgs pt

, predMap = Rel.setInsert (symName sy) pt $ predMap sigma1 }

_ -> sigma1 -- extend this for the type variable e

-- 5./6.

{-

Computing signature co-generated by a raw symbol set.

Algorithm adapted from Bartek Klin's algorithm for CATS.

Input: symbol set "Syms"

signature "Sigma"

Output: signature "Sigma1"<=Sigma.

1. get a set "Sigma_symbols" of symbols in Sigma.

2. if Syms is not a subset of Sigma_symbols, return error.

3. for each symbol "Sym" in Syms do:

3.1. if Sym is a:

3.1.1. sort "S":

3.1.1.1. Remove S from Sigma_symbols

3.1.1.2. For each function/predicate symbol in

Sigma_symbols, if its profile contains S

remove it from Sigma_symbols.

3.1.2. any other symbol: remove if from Sigma_symbols.

4. let Sigma1 be a signature generated by Sigma_symbols in Sigma.

5. return the inclusion of sigma1 into sigma.

-}

cogeneratedSign :: m -> SymbolSet -> Sign f e

-> Result (Morphism f e m)

cogeneratedSign extEm symset sigma =

if Set.isSubsetOf symset symset0 -- 2.

then generatedSign extEm symset1 sigma -- 4./5.

else let diffsyms = symset Set.\\ symset0 in

fatal_error ("Hiding: The following symbols "

++ showDoc diffsyms " are not in the signature")

$ getRange diffsyms

where

symset0 = symOf sigma -- 1.

symset1 = Set.fold revealSym' symset0 symset -- 3.

revealSym' sy symset1' = case symbType sy of -- 3.1.

SortAsItemType -> -- 3.1.1.

Set.filter (not . profileContains (symName sy) . symbType)

$ Set.delete sy symset1'

OpAsItemType _ -> -- 3.1.2

Set.delete sy symset1'

PredAsItemType _ -> -- 3.1.2

Set.delete sy symset1'

_ -> symset1'

profileContains s symbT = elem s $ case symbT of

OpAsItemType ot -> opRes ot : opArgs ot

PredAsItemType pt -> predArgs pt

_ -> [] -- for other kinds the profiles need to be looked up

leCl :: Ord a => (a -> a -> Bool) -> Map.Map Id (Set.Set a)

-> Map.Map Id [Set.Set a]

leCl eq = Map.map (Rel.partSet eq)

mkp :: Map.Map Id (Set.Set OpType) -> Map.Map Id (Set.Set OpType)

mkp = Map.map makePartial

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

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

finalUnion addSigExt s1 s2 =

let extP = Map.map (map $ \ s -> (s, [], False))

o1 = extP $ leCl (leqF s1) $ mkp $ opMap s1

o2 = extP $ leCl (leqF s2) $ mkp $ opMap s2

p1 = extP $ leCl (leqP s1) $ predMap s1

p2 = extP $ leCl (leqP s2) $ predMap s2

s3 = addSig addSigExt s1 s2

o3 = leCl (leqF s3) $ mkp $ opMap s3

p3 = leCl (leqP s3) $ predMap s3

d1 = Map.differenceWith (listOfSetDiff True) o1 o3

d2 = Map.union d1 $ Map.differenceWith (listOfSetDiff False) o2 o3

e1 = Map.differenceWith (listOfSetDiff True) p1 p3

e2 = Map.union e1 $ Map.differenceWith (listOfSetDiff False) p2 p3

prL (s, l, b) = fsep

$ text ("(" ++ (if b then "left" else "right")

++ " side of union)")

: map pretty l ++ [mapsto <+> pretty s]

prM str = ppMap ((text str <+>) . pretty)

(vcat . map prL) id vcat (\ v1 v2 -> sep [v1, v2])

in if Map.null d2 && Map.null e2 then return s3

else fail $ "illegal overload relation identifications for profiles of:\n"

++ show (prM "op" d2 $+$ prM "pred" e2)

listOfSetDiff :: Ord a => Bool -> [(Set.Set a, [Set.Set a], Bool)]

-> [Set.Set a]-> Maybe [(Set.Set a, [Set.Set a], Bool)]

listOfSetDiff b rl1 l2 = let

fst3 (s, _, _) = s

l1 = map fst3 rl1 in

(\ l3 -> if null l3 then Nothing else Just l3)

$ fst $ foldr

(\ s (l, r) ->

let sIn = Set.isSubsetOf s

(r1, r2) = partition sIn r in

case r1 of

[] -> case find sIn l2 of

Nothing -> error "CASL.finalUnion.listOfSetDiff1"

Just s2 -> (if elem s2 $ map fst3 l then l else

(s2, filter (flip Set.isSubsetOf s2) l1, b) : l, r)

[_] -> (l, r2)

_ -> error "CASL.finalUnion.listOfSetDiff2")

([], l2) l1