{- |
Module      :  ./CASL/SymbolMapAnalysis.hs
Description :  symbol map analysis for the CASL logic.
Copyright   :  (c) Till Mossakowski, C. Maeder and Uni Bremen 2002-2005
License     :  GPLv2 or higher, see LICENSE.txt

Maintainer  :  Christian.Maeder@dfki.de
Stability   :  provisional
Portability :  portable

Symbol map analysis for the CASL logic.
  Follows Sect. III:4.1 of the CASL Reference Manual.
-}

module CASL.SymbolMapAnalysis
    ( inducedFromMorphism
    , inducedFromToMorphism
    , inducedFromMorphismExt
    , inducedFromToMorphismExt
    , cogeneratedSign
    , generatedSign
    , finalUnion
    , constMorphExt
    , revealSym
    , profileContainsSort
    ) where

import CASL.Sign
import CASL.AS_Basic_CASL
import CASL.Morphism
import CASL.Overload (leqF, leqP)

import qualified Common.Lib.MapSet as MapSet
import qualified Common.Lib.Rel as Rel
import Common.Doc
import Common.DocUtils
import Common.ExtSign
import Common.Id
import Common.Result
import qualified Control.Monad.Fail as Fail

import Data.List (partition, find)
import Data.Maybe
import qualified Data.Map as Map
import qualified Data.Set as Set

{-
inducedFromMorphism :: RawSymbolMap -> sign -> Result morphism

Here is Bartek Klin's algorithm that has benn used for CATS.
Our algorithm deviates from it. The exact details need to be checked.

Inducing morphism from raw symbol map and signature

Input:  raw symbol map "Rsm"
        signature "Sigma1"
Output: morphims "Mrph": Sigma1 -> "Sigma2".

//preparation
1. let "Ssm" be an empty list of pairs (symbol, raw symbol).
2. for each pair "Rsym1,Rsym2" in Rsm do:
        2.1. if there is no symbol in Sigma1 matching Rsym1, return error.
        2.2. for each symbol "Sym" from Sigma1 matching Rsym1
                2.2.1. add a pair "Sym,Rsym2" to Ssm.
//computing the "sort part" of the morphism
3. let Sigma2 be an empty signature.
4. let Mrph be an empty "morphism" from Sigma1 to Sigma2.
5. for each pair "Sym,Rsym2" in Ssm such that Sym is a sort symbol
        5.1. if Rsym2 is not a sort raw symbol, return error.
        5.2. if in Mrph there is a mapping of sort in Sym to sort with
                name other than that in Rsym2, return error.
        5.3. if in Mrph there is no mappinh of sort in Sym
                5.3.1. add sort from Rsym2 to Sigma2
                5.3.2. add mapping from sort(Sym) to sort(Rsym2) to Mrph.
6. for each sort symbol "S" in Sigma1
        6.1. if S is not mapped by Mrph,
                6.1.1. add sort S to Sigma2
                6.1.2. add mapping from S to S to Mrph.
//computing the "function/predicate part" of the morphism
7. for each pair "Sym,Rsym2" in Ssm such that Sym is a function/predicate
   symbol
        7.1. let "F" be name contained in Sym, let "Fprof" be the profile.
        7.2. let "Fprof1" be the value of Fprof via Mrph
                (it can be computed, as we already have the "sort" part of
                 morphism)
        7.3. if Rsym2 is not of appriopriate type, return error, otherwise
             let "F2" be the name of the symbol.
        7.4. if Rsym2 enforces the profile of the symbol (i.e., it is not
             an implicit symbol), compare the profile to Fprof1. If it is
             not equal, return error.
        7.5. if in Mrph there is a mapping of F1 with profile Fprof to
             some name different than F2, return error.
        7.6. add an operation/predicate with name F2 and profile Fprof1 to
             Sigma2. If it is a partial function and if in Sigma2 there
             exists a total function with the same name and profile, do not
             add it. Otherwise if it is a total function and if in Sigma2
             there exists a partial function with the same name and profile,
             add the total function removing the partial one.
        7.7. add to Mrph a mapping from operation/predicate of name F1 and
             profile Fprof to name F2.
8. for each operation/predicate symbol "F" with profile "Fprof" in Sigma1
   that is not mapped by Mrph,
        8.1. as in 7.2
        8.2. as in 7.6, replacing F2 with F1.
        8.3. as in 7.7, replacing F2 with F1.
9. for each sort relation "S1,S2" in Sigma1,
        9.1. compute S3=(S1 via Mrph) and S4=(S2 via Mrph)
        9.2. add sort relation "S3,S4" in Sigma2.
10. Compute transitive closure of subsorting relation in Sigma2.
-}

type InducedMorphism e m = RawSymbolMap -> e -> Result m

constMorphExt :: m -> InducedMorphism e m
constMorphExt :: m -> InducedMorphism e m
constMorphExt m :: m
m _ _ = m -> Result m
forall (m :: * -> *) a. Monad m => a -> m a
return m
m

{- | function and preds in the overloading relation are mapped in the same way
thus preserving the overload-relation -}
inducedFromMorphism :: (Pretty e, Show f) => m -> RawSymbolMap -> Sign f e
                    -> Result (Morphism f e m)
inducedFromMorphism :: m -> RawSymbolMap -> Sign f e -> Result (Morphism f e m)
inducedFromMorphism =
  InducedSign f e m e
-> InducedMorphism e m
-> RawSymbolMap
-> Sign f e
-> Result (Morphism f e m)
forall e f m.
(Pretty e, Show f) =>
InducedSign f e m e
-> InducedMorphism e m
-> RawSymbolMap
-> Sign f e
-> Result (Morphism f e m)
inducedFromMorphismExt (\ _ _ _ _ -> Sign f e -> e
forall f e. Sign f e -> e
extendedInfo) (InducedMorphism e m
 -> RawSymbolMap -> Sign f e -> Result (Morphism f e m))
-> (m -> InducedMorphism e m)
-> m
-> RawSymbolMap
-> Sign f e
-> Result (Morphism f e m)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. m -> InducedMorphism e m
forall m e. m -> InducedMorphism e m
constMorphExt

inducedFromMorphismExt :: (Pretty e, Show f) => InducedSign f e m e
                       -> InducedMorphism e m
                       -> RawSymbolMap -> Sign f e -> Result (Morphism f e m)
inducedFromMorphismExt :: InducedSign f e m e
-> InducedMorphism e m
-> RawSymbolMap
-> Sign f e
-> Result (Morphism f e m)
inducedFromMorphismExt extInd :: InducedSign f e m e
extInd extEm :: InducedMorphism e m
extEm rmap :: RawSymbolMap
rmap sigma :: Sign f e
sigma = do
  -- compute the sort map (as a Map)
  Map Id Id
sort_Map <- (Id -> Result (Map Id Id) -> Result (Map Id Id))
-> Result (Map Id Id) -> Set Id -> Result (Map Id Id)
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (\ s :: Id
s m :: Result (Map Id Id)
m -> do
                Id
s' <- RawSymbolMap -> Id -> Result Id
sortFun RawSymbolMap
rmap Id
s
                Map Id Id
m1 <- Result (Map Id Id)
m
                Map Id Id -> Result (Map Id Id)
forall (m :: * -> *) a. Monad m => a -> m a
return (Map Id Id -> Result (Map Id Id))
-> Map Id Id -> Result (Map Id Id)
forall a b. (a -> b) -> a -> b
$ if Id
s' Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
s then Map Id Id
m1 else Id -> Id -> Map Id Id -> Map Id Id
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert Id
s Id
s' Map Id Id
m1)
              (Map Id Id -> Result (Map Id Id)
forall (m :: * -> *) a. Monad m => a -> m a
return Map Id Id
forall k a. Map k a
Map.empty) (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
sigma)
  -- compute the op map (as a Map)
  Op_map
op_Map <- (Id -> Set OpType -> Result Op_map -> Result Op_map)
-> Result Op_map -> Map Id (Set OpType) -> Result Op_map
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (Sign f e
-> RawSymbolMap
-> Map Id Id
-> Id
-> Set OpType
-> Result Op_map
-> Result Op_map
forall f e.
Sign f e
-> RawSymbolMap
-> Map Id Id
-> Id
-> Set OpType
-> Result Op_map
-> Result Op_map
opFun Sign f e
sigma RawSymbolMap
rmap Map Id Id
sort_Map)
              (Op_map -> Result Op_map
forall (m :: * -> *) a. Monad m => a -> m a
return Op_map
forall k a. Map k a
Map.empty) (MapSet Id OpType -> Map Id (Set OpType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet Id OpType -> Map Id (Set OpType))
-> MapSet Id OpType -> Map Id (Set OpType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
sigma)
  -- compute the pred map (as a Map)
  Pred_map
pred_Map <- (Id -> Set PredType -> Result Pred_map -> Result Pred_map)
-> Result Pred_map -> Map Id (Set PredType) -> Result Pred_map
forall k a b. (k -> a -> b -> b) -> b -> Map k a -> b
Map.foldrWithKey (Sign f e
-> RawSymbolMap
-> Map Id Id
-> Id
-> Set PredType
-> Result Pred_map
-> Result Pred_map
forall f e.
Sign f e
-> RawSymbolMap
-> Map Id Id
-> Id
-> Set PredType
-> Result Pred_map
-> Result Pred_map
predFun Sign f e
sigma RawSymbolMap
rmap Map Id Id
sort_Map)
              (Pred_map -> Result Pred_map
forall (m :: * -> *) a. Monad m => a -> m a
return Pred_map
forall k a. Map k a
Map.empty) (MapSet Id PredType -> Map Id (Set PredType)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap (MapSet Id PredType -> Map Id (Set PredType))
-> MapSet Id PredType -> Map Id (Set PredType)
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
sigma)
  m
em <- InducedMorphism e m
extEm RawSymbolMap
rmap (e -> Result m) -> e -> Result m
forall a b. (a -> b) -> a -> b
$ Sign f e -> e
forall f e. Sign f e -> e
extendedInfo Sign f e
sigma
  -- return assembled morphism
  Morphism f e m -> Result (Morphism f e m)
forall (m :: * -> *) a. Monad m => a -> m a
return (m -> Sign f e -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism m
em Sign f e
sigma
          (Sign f e -> Morphism f e m) -> Sign f e -> Morphism f e m
forall a b. (a -> b) -> a -> b
$ InducedSign f e m e -> InducedSign f e m (Sign f e)
forall f e m. InducedSign f e m e -> InducedSign f e m (Sign f e)
inducedSignAux InducedSign f e m e
extInd Map Id Id
sort_Map Op_map
op_Map Pred_map
pred_Map m
em Sign f e
sigma)
    { sort_map :: Map Id Id
sort_map = Map Id Id
sort_Map
    , op_map :: Op_map
op_map = Op_map
op_Map
    , pred_map :: Pred_map
pred_map = Pred_map
pred_Map }

  {- the sorts of the source signature
  sortFun is the sort map as a Haskell function -}
sortFun :: RawSymbolMap -> Id -> Result Id
sortFun :: RawSymbolMap -> Id -> Result Id
sortFun rmap :: RawSymbolMap
rmap s :: Id
s
    -- rsys contains the raw symbols to which s is mapped to
  | Set RawSymbol -> Bool
forall a. Set a -> Bool
Set.null Set RawSymbol
rsys = Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return Id
s -- use default = identity mapping
  | Set RawSymbol -> Bool
forall a. Set a -> Bool
Set.null (Set RawSymbol -> Bool) -> Set RawSymbol -> Bool
forall a b. (a -> b) -> a -> b
$ Set RawSymbol -> Set RawSymbol
forall a. Set a -> Set a
Set.deleteMin Set RawSymbol
rsys =
          Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return (Id -> Result Id) -> Id -> Result Id
forall a b. (a -> b) -> a -> b
$ RawSymbol -> Id
rawSymName (RawSymbol -> Id) -> RawSymbol -> Id
forall a b. (a -> b) -> a -> b
$ Set RawSymbol -> RawSymbol
forall a. Set a -> a
Set.findMin Set RawSymbol
rsys -- take the unique rsy
  | Bool
otherwise = Id -> String -> Range -> Result Id
forall a. a -> String -> Range -> Result a
plain_error Id
s  -- ambiguity! generate an error
                 ("sort " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String -> String
showId Id
s
                  " is mapped ambiguously: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set RawSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Set RawSymbol
rsys "")
                 (Range -> Result Id) -> Range -> Result Id
forall a b. (a -> b) -> a -> b
$ Set RawSymbol -> Range
forall a. GetRange a => a -> Range
getRange Set RawSymbol
rsys
    where
    -- get all raw symbols to which s is mapped to
    rsys :: Set RawSymbol
rsys = [RawSymbol] -> Set RawSymbol
forall a. Ord a => [a] -> Set a
Set.fromList ([RawSymbol] -> Set RawSymbol) -> [RawSymbol] -> Set RawSymbol
forall a b. (a -> b) -> a -> b
$ (RawSymbol -> Maybe RawSymbol) -> [RawSymbol] -> [RawSymbol]
forall a b. (a -> Maybe b) -> [a] -> [b]
mapMaybe (RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
`Map.lookup` RawSymbolMap
rmap)
               [ Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> Symbol
idToSortSymbol Id
s
               , SYMB_KIND -> Id -> RawSymbol
AKindedSymb SYMB_KIND
Implicit Id
s ]

  {- to a Op_map, add everything resulting from mapping (id, ots)
  according to rmap -}
opFun :: Sign f e -> RawSymbolMap -> Sort_map -> Id -> Set.Set OpType
      -> Result Op_map -> Result Op_map
opFun :: Sign f e
-> RawSymbolMap
-> Map Id Id
-> Id
-> Set OpType
-> Result Op_map
-> Result Op_map
opFun src :: Sign f e
src rmap :: RawSymbolMap
rmap sort_Map :: Map Id Id
sort_Map ide :: Id
ide ots :: Set OpType
ots m :: Result Op_map
m =
    -- first consider all directly mapped profiles
    let otls :: [Set OpType]
otls = (OpType -> OpType -> Bool) -> Set OpType -> [Set OpType]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet (Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF Sign f e
src) Set OpType
ots
        m1 :: Result Op_map
m1 = (Set OpType -> Result Op_map -> Result Op_map)
-> Result Op_map -> [Set OpType] -> Result Op_map
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (RawSymbolMap
-> Map Id Id -> Id -> Set OpType -> Result Op_map -> Result Op_map
directOpMap RawSymbolMap
rmap Map Id Id
sort_Map Id
ide) Result Op_map
m [Set OpType]
otls
    -- now try the remaining ones with (un)kinded raw symbol
    in case (RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SYMB_KIND -> Id -> RawSymbol
AKindedSymb SYMB_KIND
Ops_kind Id
ide) RawSymbolMap
rmap,
                RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SYMB_KIND -> Id -> RawSymbol
AKindedSymb SYMB_KIND
Implicit Id
ide) RawSymbolMap
rmap) of
       (Just rsy1 :: RawSymbol
rsy1, Just rsy2 :: RawSymbol
rsy2) -> let
          m2 :: Result Op_map
m2 = (OpType -> Result Op_map -> Result Op_map)
-> Result Op_map -> Set OpType -> Result Op_map
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Map Id Id
-> Id -> RawSymbol -> OpType -> Result Op_map -> Result Op_map
insertmapOpSym Map Id Id
sort_Map Id
ide RawSymbol
rsy1) Result Op_map
m1 Set OpType
ots
          in (OpType -> Result Op_map -> Result Op_map)
-> Result Op_map -> Set OpType -> Result Op_map
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Map Id Id
-> Id -> RawSymbol -> OpType -> Result Op_map -> Result Op_map
insertmapOpSym Map Id Id
sort_Map Id
ide RawSymbol
rsy2) Result Op_map
m2 Set OpType
ots
       (Just rsy :: RawSymbol
rsy, Nothing) ->
          (OpType -> Result Op_map -> Result Op_map)
-> Result Op_map -> Set OpType -> Result Op_map
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Map Id Id
-> Id -> RawSymbol -> OpType -> Result Op_map -> Result Op_map
insertmapOpSym Map Id Id
sort_Map Id
ide RawSymbol
rsy) Result Op_map
m1 Set OpType
ots
       (Nothing, Just rsy :: RawSymbol
rsy) ->
          (OpType -> Result Op_map -> Result Op_map)
-> Result Op_map -> Set OpType -> Result Op_map
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Map Id Id
-> Id -> RawSymbol -> OpType -> Result Op_map -> Result Op_map
insertmapOpSym Map Id Id
sort_Map Id
ide RawSymbol
rsy) Result Op_map
m1 Set OpType
ots
       -- Anything not mapped explicitly is left unchanged
       (Nothing, Nothing) -> Result Op_map
m1

    {- try to map an operation symbol directly
    collect all opTypes that cannot be mapped directly -}
directOpMap :: RawSymbolMap -> Sort_map -> Id -> Set.Set OpType
            -> Result Op_map -> Result Op_map
directOpMap :: RawSymbolMap
-> Map Id Id -> Id -> Set OpType -> Result Op_map -> Result Op_map
directOpMap rmap :: RawSymbolMap
rmap sort_Map :: Map Id Id
sort_Map ide :: Id
ide ots :: Set OpType
ots m :: Result Op_map
m =
  let ol :: [OpType]
ol = Set OpType -> [OpType]
forall a. Set a -> [a]
Set.toList Set OpType
ots
      rl :: [Maybe RawSymbol]
rl = (OpType -> Maybe RawSymbol) -> [OpType] -> [Maybe RawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (RawSymbolMap -> Id -> OpType -> Maybe RawSymbol
lookupOpSymbol RawSymbolMap
rmap Id
ide) [OpType]
ol
      (ms :: [(Maybe RawSymbol, OpType)]
ms, os :: [(Maybe RawSymbol, OpType)]
os) = ((Maybe RawSymbol, OpType) -> Bool)
-> [(Maybe RawSymbol, OpType)]
-> ([(Maybe RawSymbol, OpType)], [(Maybe RawSymbol, OpType)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe RawSymbol -> Bool
forall a. Maybe a -> Bool
isJust (Maybe RawSymbol -> Bool)
-> ((Maybe RawSymbol, OpType) -> Maybe RawSymbol)
-> (Maybe RawSymbol, OpType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe RawSymbol, OpType) -> Maybe RawSymbol
forall a b. (a, b) -> a
fst) ([(Maybe RawSymbol, OpType)]
 -> ([(Maybe RawSymbol, OpType)], [(Maybe RawSymbol, OpType)]))
-> [(Maybe RawSymbol, OpType)]
-> ([(Maybe RawSymbol, OpType)], [(Maybe RawSymbol, OpType)])
forall a b. (a -> b) -> a -> b
$ [Maybe RawSymbol] -> [OpType] -> [(Maybe RawSymbol, OpType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe RawSymbol]
rl [OpType]
ol
  in case [(Maybe RawSymbol, OpType)]
ms of
       l :: [(Maybe RawSymbol, OpType)]
l@((Just rsy :: RawSymbol
rsy, _) : rs :: [(Maybe RawSymbol, OpType)]
rs) ->
         ((Maybe RawSymbol, OpType) -> Result Op_map -> Result Op_map)
-> Result Op_map -> [(Maybe RawSymbol, OpType)] -> Result Op_map
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (_, ot :: OpType
ot) ->
           Map Id Id
-> Id -> RawSymbol -> OpType -> Result Op_map -> Result Op_map
insertmapOpSym Map Id Id
sort_Map Id
ide
              (Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> OpType -> Symbol
idToOpSymbol (RawSymbol -> Id
rawSymName RawSymbol
rsy)
                       (OpType -> Symbol) -> OpType -> Symbol
forall a b. (a -> b) -> a -> b
$ Map Id Id -> OpType -> OpType
mapOpType Map Id Id
sort_Map OpType
ot) OpType
ot)
         (((Maybe RawSymbol, OpType) -> Result Op_map -> Result Op_map)
-> Result Op_map -> [(Maybe RawSymbol, OpType)] -> Result Op_map
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (rsy2 :: Maybe RawSymbol
rsy2, ot :: OpType
ot) ->
           Map Id Id
-> Id -> RawSymbol -> OpType -> Result Op_map -> Result Op_map
insertmapOpSym Map Id Id
sort_Map Id
ide (Maybe RawSymbol -> RawSymbol
forall a. HasCallStack => Maybe a -> a
fromJust Maybe RawSymbol
rsy2) OpType
ot) Result Op_map
m [(Maybe RawSymbol, OpType)]
l)
         ([(Maybe RawSymbol, OpType)] -> Result Op_map)
-> [(Maybe RawSymbol, OpType)] -> Result Op_map
forall a b. (a -> b) -> a -> b
$ [(Maybe RawSymbol, OpType)]
rs [(Maybe RawSymbol, OpType)]
-> [(Maybe RawSymbol, OpType)] -> [(Maybe RawSymbol, OpType)]
forall a. [a] -> [a] -> [a]
++ [(Maybe RawSymbol, OpType)]
os
       _ -> Result Op_map
m

lookupOpSymbol :: RawSymbolMap -> Id -> OpType -> Maybe RawSymbol
lookupOpSymbol :: RawSymbolMap -> Id -> OpType -> Maybe RawSymbol
lookupOpSymbol rmap :: RawSymbolMap
rmap ide' :: Id
ide' ot :: OpType
ot = let mkS :: OpType -> Symbol
mkS = Id -> OpType -> Symbol
idToOpSymbol Id
ide' in
  case RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Symbol -> RawSymbol
ASymbol (OpType -> Symbol
mkS (OpType -> Symbol) -> OpType -> Symbol
forall a b. (a -> b) -> a -> b
$ OpType -> OpType
mkPartial OpType
ot)) RawSymbolMap
rmap of
    Nothing -> RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup
      (Symbol -> RawSymbol
ASymbol (OpType -> Symbol
mkS (OpType -> Symbol) -> OpType -> Symbol
forall a b. (a -> b) -> a -> b
$ OpType -> OpType
mkTotal OpType
ot)) RawSymbolMap
rmap
    res :: Maybe RawSymbol
res -> Maybe RawSymbol
res

    -- map op symbol (ide, ot) to raw symbol rsy
mappedOpSym :: Sort_map -> Id -> OpType -> RawSymbol -> Result (Id, OpKind)
mappedOpSym :: Map Id Id -> Id -> OpType -> RawSymbol -> Result (Id, OpKind)
mappedOpSym sort_Map :: Map Id Id
sort_Map ide :: Id
ide ot :: OpType
ot rsy :: RawSymbol
rsy =
    let opSym :: String
opSym = "operation symbol " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc (Id -> OpType -> Symbol
idToOpSymbol Id
ide OpType
ot)
                " is mapped to "
        kind :: OpKind
kind = OpType -> OpKind
opKind OpType
ot
        ot2 :: OpType
ot2 = Map Id Id -> OpType -> OpType
mapOpType Map Id Id
sort_Map OpType
ot
    in case RawSymbol
rsy of
      ASymbol (Symbol ide' :: Id
ide' (OpAsItemType ot' :: OpType
ot')) ->
        if OpType -> OpType -> Bool
compatibleOpTypes OpType
ot2 OpType
ot'
           then (Id, OpKind) -> Result (Id, OpKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id
ide', OpType -> OpKind
opKind OpType
ot')
           else (Id, OpKind) -> String -> Range -> Result (Id, OpKind)
forall a. a -> String -> Range -> Result a
plain_error (Id
ide, OpKind
kind)
             (String
opSym String -> String -> String
forall a. [a] -> [a] -> [a]
++ "type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ OpType -> String -> String
forall a. Pretty a => a -> String -> String
showDoc OpType
ot'
              " but should be mapped to type " String -> String -> String
forall a. [a] -> [a] -> [a]
++
              OpType -> String -> String
forall a. Pretty a => a -> String -> String
showDoc OpType
ot2 "") (Range -> Result (Id, OpKind)) -> Range -> Result (Id, OpKind)
forall a b. (a -> b) -> a -> b
$ RawSymbol -> Range
forall a. GetRange a => a -> Range
getRange RawSymbol
rsy
      AKindedSymb k :: SYMB_KIND
k ide' :: Id
ide' | SYMB_KIND -> [SYMB_KIND] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem SYMB_KIND
k [SYMB_KIND
Implicit, SYMB_KIND
Ops_kind] -> (Id, OpKind) -> Result (Id, OpKind)
forall (m :: * -> *) a. Monad m => a -> m a
return (Id
ide', OpKind
kind)
      _ -> (Id, OpKind) -> String -> Range -> Result (Id, OpKind)
forall a. a -> String -> Range -> Result a
plain_error (Id
ide, OpKind
kind)
               (String
opSym String -> String -> String
forall a. [a] -> [a] -> [a]
++ "symbol of wrong kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RawSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc RawSymbol
rsy "")
               (Range -> Result (Id, OpKind)) -> Range -> Result (Id, OpKind)
forall a b. (a -> b) -> a -> b
$ RawSymbol -> Range
forall a. GetRange a => a -> Range
getRange RawSymbol
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 :: Map Id Id
-> Id -> RawSymbol -> OpType -> Result Op_map -> Result Op_map
insertmapOpSym sort_Map :: Map Id Id
sort_Map ide :: Id
ide rsy :: RawSymbol
rsy ot :: OpType
ot m :: Result Op_map
m = do
      Op_map
m1 <- Result Op_map
m
      (ide' :: Id
ide', kind' :: OpKind
kind') <- Map Id Id -> Id -> OpType -> RawSymbol -> Result (Id, OpKind)
mappedOpSym Map Id Id
sort_Map Id
ide OpType
ot RawSymbol
rsy
      let otsy :: Symbol
otsy = Id -> SymbType -> Symbol
Symbol Id
ide (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ OpType -> SymbType
OpAsItemType OpType
ot
          pos :: Range
pos = RawSymbol -> Range
forall a. GetRange a => a -> Range
getRange RawSymbol
rsy
          m2 :: Op_map
m2 = (Id, OpType) -> (Id, OpKind) -> Op_map -> Op_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id
ide, OpType -> OpType
mkPartial OpType
ot) (Id
ide', OpKind
kind') Op_map
m1
      case (Id, OpType) -> Op_map -> Maybe (Id, OpKind)
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Id
ide, OpType -> OpType
mkPartial OpType
ot) Op_map
m1 of
        Nothing -> if Id
ide Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
ide' Bool -> Bool -> Bool
&& OpKind
kind' OpKind -> OpKind -> Bool
forall a. Eq a => a -> a -> Bool
== OpType -> OpKind
opKind OpType
ot then
            case RawSymbol
rsy of
              ASymbol _ -> Op_map -> Result Op_map
forall (m :: * -> *) a. Monad m => a -> m a
return Op_map
m1
              _ -> Op_map -> String -> Range -> Result Op_map
forall a. a -> String -> Range -> Result a
hint Op_map
m1 ("identity mapping of "
                               String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Symbol
otsy "") Range
pos
            else Op_map -> Result Op_map
forall (m :: * -> *) a. Monad m => a -> m a
return Op_map
m2
        Just (ide'' :: Id
ide'', kind'' :: OpKind
kind'') -> if Id
ide' Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
ide'' then
             Op_map -> String -> Range -> Result Op_map
forall a. a -> String -> Range -> Result a
warning (if OpKind
kind' OpKind -> OpKind -> Bool
forall a. Ord a => a -> a -> Bool
< OpKind
kind'' then Op_map
m2 else Op_map
m1)
             ("ignoring duplicate mapping of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Symbol
otsy "")
             Range
pos
            else Op_map -> String -> Range -> Result Op_map
forall a. a -> String -> Range -> Result a
plain_error Op_map
m1
             ("conflicting mapping of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Symbol
otsy " to " String -> String -> String
forall a. [a] -> [a] -> [a]
++
               Id -> String
forall a. Show a => a -> String
show Id
ide' String -> String -> String
forall a. [a] -> [a] -> [a]
++ " and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
ide'') Range
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 :: Sign f e
-> RawSymbolMap
-> Map Id Id
-> Id
-> Set PredType
-> Result Pred_map
-> Result Pred_map
predFun src :: Sign f e
src rmap :: RawSymbolMap
rmap sort_Map :: Map Id Id
sort_Map ide :: Id
ide pts :: Set PredType
pts m :: Result Pred_map
m =
    -- first consider all directly mapped profiles
    let ptls :: [Set PredType]
ptls = (PredType -> PredType -> Bool) -> Set PredType -> [Set PredType]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet (Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP Sign f e
src) Set PredType
pts
        m1 :: Result Pred_map
m1 = (Set PredType -> Result Pred_map -> Result Pred_map)
-> Result Pred_map -> [Set PredType] -> Result Pred_map
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (RawSymbolMap
-> Map Id Id
-> Id
-> Set PredType
-> Result Pred_map
-> Result Pred_map
directPredMap RawSymbolMap
rmap Map Id Id
sort_Map Id
ide) Result Pred_map
m [Set PredType]
ptls
    -- now try the remaining ones with (un)kinded raw symbol
    in case (RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SYMB_KIND -> Id -> RawSymbol
AKindedSymb SYMB_KIND
Preds_kind Id
ide) RawSymbolMap
rmap,
                RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (SYMB_KIND -> Id -> RawSymbol
AKindedSymb SYMB_KIND
Implicit Id
ide) RawSymbolMap
rmap) of
       (Just rsy1 :: RawSymbol
rsy1, Just rsy2 :: RawSymbol
rsy2) -> let
          m2 :: Result Pred_map
m2 = (PredType -> Result Pred_map -> Result Pred_map)
-> Result Pred_map -> Set PredType -> Result Pred_map
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Map Id Id
-> Id
-> RawSymbol
-> PredType
-> Result Pred_map
-> Result Pred_map
insertmapPredSym Map Id Id
sort_Map Id
ide RawSymbol
rsy1) Result Pred_map
m1 Set PredType
pts
          in (PredType -> Result Pred_map -> Result Pred_map)
-> Result Pred_map -> Set PredType -> Result Pred_map
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Map Id Id
-> Id
-> RawSymbol
-> PredType
-> Result Pred_map
-> Result Pred_map
insertmapPredSym Map Id Id
sort_Map Id
ide RawSymbol
rsy2) Result Pred_map
m2 Set PredType
pts
       (Just rsy :: RawSymbol
rsy, Nothing) ->
          (PredType -> Result Pred_map -> Result Pred_map)
-> Result Pred_map -> Set PredType -> Result Pred_map
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Map Id Id
-> Id
-> RawSymbol
-> PredType
-> Result Pred_map
-> Result Pred_map
insertmapPredSym Map Id Id
sort_Map Id
ide RawSymbol
rsy) Result Pred_map
m1 Set PredType
pts
       (Nothing, Just rsy :: RawSymbol
rsy) ->
          (PredType -> Result Pred_map -> Result Pred_map)
-> Result Pred_map -> Set PredType -> Result Pred_map
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold (Map Id Id
-> Id
-> RawSymbol
-> PredType
-> Result Pred_map
-> Result Pred_map
insertmapPredSym Map Id Id
sort_Map Id
ide RawSymbol
rsy) Result Pred_map
m1 Set PredType
pts
       -- Anything not mapped explicitly is left unchanged
       (Nothing, Nothing) -> Result Pred_map
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 :: RawSymbolMap
-> Map Id Id
-> Id
-> Set PredType
-> Result Pred_map
-> Result Pred_map
directPredMap rmap :: RawSymbolMap
rmap sort_Map :: Map Id Id
sort_Map ide :: Id
ide pts :: Set PredType
pts m :: Result Pred_map
m =
  let pl :: [PredType]
pl = Set PredType -> [PredType]
forall a. Set a -> [a]
Set.toList Set PredType
pts
      rl :: [Maybe RawSymbol]
rl = (PredType -> Maybe RawSymbol) -> [PredType] -> [Maybe RawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map (\ pt :: PredType
pt -> RawSymbol -> RawSymbolMap -> Maybe RawSymbol
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> PredType -> Symbol
idToPredSymbol Id
ide PredType
pt) RawSymbolMap
rmap) [PredType]
pl
      (ms :: [(Maybe RawSymbol, PredType)]
ms, ps :: [(Maybe RawSymbol, PredType)]
ps) = ((Maybe RawSymbol, PredType) -> Bool)
-> [(Maybe RawSymbol, PredType)]
-> ([(Maybe RawSymbol, PredType)], [(Maybe RawSymbol, PredType)])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition (Maybe RawSymbol -> Bool
forall a. Maybe a -> Bool
isJust (Maybe RawSymbol -> Bool)
-> ((Maybe RawSymbol, PredType) -> Maybe RawSymbol)
-> (Maybe RawSymbol, PredType)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Maybe RawSymbol, PredType) -> Maybe RawSymbol
forall a b. (a, b) -> a
fst) ([(Maybe RawSymbol, PredType)]
 -> ([(Maybe RawSymbol, PredType)], [(Maybe RawSymbol, PredType)]))
-> [(Maybe RawSymbol, PredType)]
-> ([(Maybe RawSymbol, PredType)], [(Maybe RawSymbol, PredType)])
forall a b. (a -> b) -> a -> b
$ [Maybe RawSymbol] -> [PredType] -> [(Maybe RawSymbol, PredType)]
forall a b. [a] -> [b] -> [(a, b)]
zip [Maybe RawSymbol]
rl [PredType]
pl
  in case [(Maybe RawSymbol, PredType)]
ms of
       l :: [(Maybe RawSymbol, PredType)]
l@((Just rsy :: RawSymbol
rsy, _) : rs :: [(Maybe RawSymbol, PredType)]
rs) ->
         ((Maybe RawSymbol, PredType) -> Result Pred_map -> Result Pred_map)
-> Result Pred_map
-> [(Maybe RawSymbol, PredType)]
-> Result Pred_map
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (_, pt :: PredType
pt) ->
           Map Id Id
-> Id
-> RawSymbol
-> PredType
-> Result Pred_map
-> Result Pred_map
insertmapPredSym Map Id Id
sort_Map Id
ide
              (Symbol -> RawSymbol
ASymbol (Symbol -> RawSymbol) -> Symbol -> RawSymbol
forall a b. (a -> b) -> a -> b
$ Id -> PredType -> Symbol
idToPredSymbol (RawSymbol -> Id
rawSymName RawSymbol
rsy)
                       (PredType -> Symbol) -> PredType -> Symbol
forall a b. (a -> b) -> a -> b
$ Map Id Id -> PredType -> PredType
mapPredType Map Id Id
sort_Map PredType
pt) PredType
pt)
         (((Maybe RawSymbol, PredType) -> Result Pred_map -> Result Pred_map)
-> Result Pred_map
-> [(Maybe RawSymbol, PredType)]
-> Result Pred_map
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr (\ (rsy2 :: Maybe RawSymbol
rsy2, pt :: PredType
pt) ->
           Map Id Id
-> Id
-> RawSymbol
-> PredType
-> Result Pred_map
-> Result Pred_map
insertmapPredSym Map Id Id
sort_Map Id
ide (Maybe RawSymbol -> RawSymbol
forall a. HasCallStack => Maybe a -> a
fromJust Maybe RawSymbol
rsy2) PredType
pt) Result Pred_map
m [(Maybe RawSymbol, PredType)]
l)
         ([(Maybe RawSymbol, PredType)] -> Result Pred_map)
-> [(Maybe RawSymbol, PredType)] -> Result Pred_map
forall a b. (a -> b) -> a -> b
$ [(Maybe RawSymbol, PredType)]
rs [(Maybe RawSymbol, PredType)]
-> [(Maybe RawSymbol, PredType)] -> [(Maybe RawSymbol, PredType)]
forall a. [a] -> [a] -> [a]
++ [(Maybe RawSymbol, PredType)]
ps
       _ -> Result Pred_map
m

    -- map pred symbol (ide, pt) to raw symbol rsy
mappedPredSym :: Sort_map -> Id -> PredType -> RawSymbol -> Result Id
mappedPredSym :: Map Id Id -> Id -> PredType -> RawSymbol -> Result Id
mappedPredSym sort_Map :: Map Id Id
sort_Map ide :: Id
ide pt :: PredType
pt rsy :: RawSymbol
rsy =
    let predSym :: String
predSym = "predicate symbol " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc (Id -> PredType -> Symbol
idToPredSymbol Id
ide PredType
pt)
                  " is mapped to "
        pt2 :: PredType
pt2 = Map Id Id -> PredType -> PredType
mapPredType Map Id Id
sort_Map PredType
pt
    in case RawSymbol
rsy of
      ASymbol (Symbol ide' :: Id
ide' (PredAsItemType pt' :: PredType
pt')) ->
        if PredType
pt2 PredType -> PredType -> Bool
forall a. Eq a => a -> a -> Bool
== PredType
pt'
           then Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return Id
ide'
           else Id -> String -> Range -> Result Id
forall a. a -> String -> Range -> Result a
plain_error Id
ide
             (String
predSym String -> String -> String
forall a. [a] -> [a] -> [a]
++ "type " String -> String -> String
forall a. [a] -> [a] -> [a]
++ PredType -> String -> String
forall a. Pretty a => a -> String -> String
showDoc PredType
pt'
              " but should be mapped to type " String -> String -> String
forall a. [a] -> [a] -> [a]
++
              PredType -> String -> String
forall a. Pretty a => a -> String -> String
showDoc PredType
pt2 "") (Range -> Result Id) -> Range -> Result Id
forall a b. (a -> b) -> a -> b
$ RawSymbol -> Range
forall a. GetRange a => a -> Range
getRange RawSymbol
rsy
      AKindedSymb k :: SYMB_KIND
k ide' :: Id
ide' | SYMB_KIND -> [SYMB_KIND] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem SYMB_KIND
k [SYMB_KIND
Implicit, SYMB_KIND
Preds_kind] -> Id -> Result Id
forall (m :: * -> *) a. Monad m => a -> m a
return Id
ide'
      _ -> Id -> String -> Range -> Result Id
forall a. a -> String -> Range -> Result a
plain_error Id
ide
               (String
predSym String -> String -> String
forall a. [a] -> [a] -> [a]
++ "symbol of wrong kind: " String -> String -> String
forall a. [a] -> [a] -> [a]
++ RawSymbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc RawSymbol
rsy "")
               (Range -> Result Id) -> Range -> Result Id
forall a b. (a -> b) -> a -> b
$ RawSymbol -> Range
forall a. GetRange a => a -> Range
getRange RawSymbol
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 :: Map Id Id
-> Id
-> RawSymbol
-> PredType
-> Result Pred_map
-> Result Pred_map
insertmapPredSym sort_Map :: Map Id Id
sort_Map ide :: Id
ide rsy :: RawSymbol
rsy pt :: PredType
pt m :: Result Pred_map
m = do
      Pred_map
m1 <- Result Pred_map
m
      Id
ide' <- Map Id Id -> Id -> PredType -> RawSymbol -> Result Id
mappedPredSym Map Id Id
sort_Map Id
ide PredType
pt RawSymbol
rsy
      let ptsy :: Symbol
ptsy = Id -> SymbType -> Symbol
Symbol Id
ide (SymbType -> Symbol) -> SymbType -> Symbol
forall a b. (a -> b) -> a -> b
$ PredType -> SymbType
PredAsItemType PredType
pt
          pos :: Range
pos = RawSymbol -> Range
forall a. GetRange a => a -> Range
getRange RawSymbol
rsy
          m2 :: Pred_map
m2 = (Id, PredType) -> Id -> Pred_map -> Pred_map
forall k a. Ord k => k -> a -> Map k a -> Map k a
Map.insert (Id
ide, PredType
pt) Id
ide' Pred_map
m1
      case (Id, PredType) -> Pred_map -> Maybe Id
forall k a. Ord k => k -> Map k a -> Maybe a
Map.lookup (Id
ide, PredType
pt) Pred_map
m1 of
        Nothing -> if Id
ide Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
ide' then
            case RawSymbol
rsy of
              ASymbol _ -> Pred_map -> Result Pred_map
forall (m :: * -> *) a. Monad m => a -> m a
return Pred_map
m1
              _ -> Pred_map -> String -> Range -> Result Pred_map
forall a. a -> String -> Range -> Result a
hint Pred_map
m1 ("identity mapping of "
                               String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Symbol
ptsy "") Range
pos
            else Pred_map -> Result Pred_map
forall (m :: * -> *) a. Monad m => a -> m a
return Pred_map
m2
        Just ide'' :: Id
ide'' -> if Id
ide' Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
ide'' then
            Pred_map -> String -> Range -> Result Pred_map
forall a. a -> String -> Range -> Result a
warning Pred_map
m1
             ("ignoring duplicate mapping of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Symbol
ptsy "") Range
pos
            else Pred_map -> String -> Range -> Result Pred_map
forall a. a -> String -> Range -> Result a
plain_error Pred_map
m1
             ("conflicting mapping of " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Symbol
ptsy " to " String -> String -> String
forall a. [a] -> [a] -> [a]
++
               Id -> String
forall a. Show a => a -> String
show Id
ide' String -> String -> String
forall a. [a] -> [a] -> [a]
++ " and " String -> String -> String
forall a. [a] -> [a] -> [a]
++ Id -> String
forall a. Show a => a -> String
show Id
ide'') Range
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 :: m
-> (e -> e -> Bool)
-> (e -> e -> e)
-> RawSymbolMap
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphism m :: m
m =
  InducedSign f e m e
-> InducedMorphism e m
-> (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Bool)
-> (e -> e -> e)
-> RawSymbolMap
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
InducedSign f e m e
-> InducedMorphism e m
-> (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Bool)
-> (e -> e -> e)
-> RawSymbolMap
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphismExt (\ _ _ _ _ -> Sign f e -> e
forall f e. Sign f e -> e
extendedInfo) (m -> InducedMorphism e m
forall m e. m -> InducedMorphism e m
constMorphExt m
m)
  (\ _ _ -> m -> Result m
forall (m :: * -> *) a. Monad m => a -> m a
return m
m)

inducedFromToMorphismExt
  :: (Eq e, Show f, Pretty e, Pretty m)
  => InducedSign f e m e
  -> InducedMorphism e m -- ^ compute extended morphism
  -> (Morphism f e m -> Morphism f e m -> Result m)
     -- ^ composition of extensions
  -> (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 :: InducedSign f e m e
-> InducedMorphism e m
-> (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Bool)
-> (e -> e -> e)
-> RawSymbolMap
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphismExt extInd :: InducedSign f e m e
extInd extEm :: InducedMorphism e m
extEm compM :: Morphism f e m -> Morphism f e m -> Result m
compM isSubExt :: e -> e -> Bool
isSubExt diffExt :: e -> e -> e
diffExt rmap :: RawSymbolMap
rmap
  sig1 :: ExtSign (Sign f e) Symbol
sig1@(ExtSign _ sy1 :: Set Symbol
sy1) sig2 :: ExtSign (Sign f e) Symbol
sig2@(ExtSign _ sy2 :: Set Symbol
sy2) =
    let iftm :: RawSymbolMap -> (Result (Morphism f e m), RawSymbolMap)
iftm rm :: RawSymbolMap
rm = (InducedSign f e m e
-> InducedMorphism e m
-> (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Bool)
-> (e -> e -> e)
-> RawSymbolMap
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
forall e f m.
(Eq e, Show f, Pretty e, Pretty m) =>
InducedSign f e m e
-> InducedMorphism e m
-> (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Bool)
-> (e -> e -> e)
-> RawSymbolMap
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphismAuxExt InducedSign f e m e
extInd InducedMorphism e m
extEm Morphism f e m -> Morphism f e m -> Result m
compM e -> e -> Bool
isSubExt
                   e -> e -> e
diffExt RawSymbolMap
rm ExtSign (Sign f e) Symbol
sig1 ExtSign (Sign f e) Symbol
sig2, RawSymbolMap
rm)
        isOk :: Result a -> Bool
isOk = Maybe a -> Bool
forall a. Maybe a -> Bool
isJust (Maybe a -> Bool) -> (Result a -> Maybe a) -> Result a -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Result a -> Maybe a
forall a. Result a -> Maybe a
resultToMaybe
        res :: Result (Morphism f e m)
res = (Result (Morphism f e m), RawSymbolMap) -> Result (Morphism f e m)
forall a b. (a, b) -> a
fst ((Result (Morphism f e m), RawSymbolMap)
 -> Result (Morphism f e m))
-> (Result (Morphism f e m), RawSymbolMap)
-> Result (Morphism f e m)
forall a b. (a -> b) -> a -> b
$ RawSymbolMap -> (Result (Morphism f e m), RawSymbolMap)
iftm RawSymbolMap
rmap
        pos :: Range
pos = (RawSymbol -> Range) -> [RawSymbol] -> Range
forall a. (a -> Range) -> [a] -> Range
concatMapRange RawSymbol -> Range
forall a. GetRange a => a -> Range
getRange ([RawSymbol] -> Range) -> [RawSymbol] -> Range
forall a b. (a -> b) -> a -> b
$ RawSymbolMap -> [RawSymbol]
forall k a. Map k a -> [k]
Map.keys RawSymbolMap
rmap
    in if Result (Morphism f e m) -> Bool
forall a. Result a -> Bool
isOk Result (Morphism f e m)
res then Result (Morphism f e m)
res else
       let ss1 :: Set Symbol
ss1 = (Symbol -> Bool) -> Set Symbol -> Set Symbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ s :: Symbol
s -> Set Symbol -> Bool
forall a. Set a -> Bool
Set.null (Set Symbol -> Bool) -> Set Symbol -> Bool
forall a b. (a -> b) -> a -> b
$ (Symbol -> Bool) -> Set Symbol -> Set Symbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter
                             (Bool -> Symbol -> Symbol -> Bool
compatibleSymbols Bool
True Symbol
s) Set Symbol
sy2)
             (Set Symbol -> Set Symbol) -> Set Symbol -> Set Symbol
forall a b. (a -> b) -> a -> b
$ (Symbol -> Bool) -> Set Symbol -> Set Symbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (\ s :: Symbol
s -> Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ (RawSymbol -> Bool) -> [RawSymbol] -> Bool
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Bool
any (Symbol -> RawSymbol -> Bool
matches Symbol
s) ([RawSymbol] -> Bool) -> [RawSymbol] -> Bool
forall a b. (a -> b) -> a -> b
$ RawSymbolMap -> [RawSymbol]
forall k a. Map k a -> [k]
Map.keys RawSymbolMap
rmap)
                 Set Symbol
sy1
           fcombs :: [[(RawSymbol, RawSymbol)]]
fcombs = (RawSymbol -> RawSymbol -> Bool)
-> [RawSymbol] -> [RawSymbol] -> [[(RawSymbol, RawSymbol)]]
forall a b. (a -> b -> Bool) -> [a] -> [b] -> [[(a, b)]]
filteredPairs RawSymbol -> RawSymbol -> Bool
compatibleRawSymbs
                    ((Symbol -> RawSymbol) -> [Symbol] -> [RawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> RawSymbol
ASymbol ([Symbol] -> [RawSymbol]) -> [Symbol] -> [RawSymbol]
forall a b. (a -> b) -> a -> b
$ Set Symbol -> [Symbol]
forall a. Set a -> [a]
Set.toList Set Symbol
ss1)
                    ([RawSymbol] -> [[(RawSymbol, RawSymbol)]])
-> [RawSymbol] -> [[(RawSymbol, RawSymbol)]]
forall a b. (a -> b) -> a -> b
$ (Symbol -> RawSymbol) -> [Symbol] -> [RawSymbol]
forall a b. (a -> b) -> [a] -> [b]
map Symbol -> RawSymbol
ASymbol ([Symbol] -> [RawSymbol]) -> [Symbol] -> [RawSymbol]
forall a b. (a -> b) -> a -> b
$ Set Symbol -> [Symbol]
forall a. Set a -> [a]
Set.toList Set Symbol
sy2
       in if [[(RawSymbol, RawSymbol)]] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null (Int -> [[(RawSymbol, RawSymbol)]] -> [[(RawSymbol, RawSymbol)]]
forall a. Int -> [a] -> [a]
drop 20 [[(RawSymbol, RawSymbol)]]
fcombs) then
          case ((Result (Morphism f e m), RawSymbolMap) -> Bool)
-> [(Result (Morphism f e m), RawSymbolMap)]
-> [(Result (Morphism f e m), RawSymbolMap)]
forall a. (a -> Bool) -> [a] -> [a]
filter (Result (Morphism f e m) -> Bool
forall a. Result a -> Bool
isOk (Result (Morphism f e m) -> Bool)
-> ((Result (Morphism f e m), RawSymbolMap)
    -> Result (Morphism f e m))
-> (Result (Morphism f e m), RawSymbolMap)
-> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Result (Morphism f e m), RawSymbolMap) -> Result (Morphism f e m)
forall a b. (a, b) -> a
fst) ([(Result (Morphism f e m), RawSymbolMap)]
 -> [(Result (Morphism f e m), RawSymbolMap)])
-> [(Result (Morphism f e m), RawSymbolMap)]
-> [(Result (Morphism f e m), RawSymbolMap)]
forall a b. (a -> b) -> a -> b
$ ([(RawSymbol, RawSymbol)]
 -> (Result (Morphism f e m), RawSymbolMap))
-> [[(RawSymbol, RawSymbol)]]
-> [(Result (Morphism f e m), RawSymbolMap)]
forall a b. (a -> b) -> [a] -> [b]
map (RawSymbolMap -> (Result (Morphism f e m), RawSymbolMap)
iftm (RawSymbolMap -> (Result (Morphism f e m), RawSymbolMap))
-> ([(RawSymbol, RawSymbol)] -> RawSymbolMap)
-> [(RawSymbol, RawSymbol)]
-> (Result (Morphism f e m), RawSymbolMap)
forall b c a. (b -> c) -> (a -> b) -> a -> c
. RawSymbolMap -> RawSymbolMap -> RawSymbolMap
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union RawSymbolMap
rmap (RawSymbolMap -> RawSymbolMap)
-> ([(RawSymbol, RawSymbol)] -> RawSymbolMap)
-> [(RawSymbol, RawSymbol)]
-> RawSymbolMap
forall b c a. (b -> c) -> (a -> b) -> a -> c
. [(RawSymbol, RawSymbol)] -> RawSymbolMap
forall k a. Ord k => [(k, a)] -> Map k a
Map.fromList)
               [[(RawSymbol, RawSymbol)]]
fcombs of
            [] -> Result (Morphism f e m)
res
            [(r :: Result (Morphism f e m)
r, m :: RawSymbolMap
m)] -> (if [[(RawSymbol, RawSymbol)]] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length [[(RawSymbol, RawSymbol)]]
fcombs Int -> Int -> Bool
forall a. Ord a => a -> a -> Bool
> 1 then () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning else () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
hint)
              () ("derived symbol map:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ RawSymbolMap -> String -> String
forall a. Pretty a => a -> String -> String
showDoc RawSymbolMap
m "") Range
pos Result () -> Result (Morphism f e m) -> Result (Morphism f e m)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result (Morphism f e m)
r
            l :: [(Result (Morphism f e m), RawSymbolMap)]
l -> String -> Range -> Result (Morphism f e m)
forall a. String -> Range -> Result a
fatal_error
              ("ambiguous symbol maps:\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show
                  ([Doc] -> Doc
vcat ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ ((Result (Morphism f e m), RawSymbolMap) -> Doc)
-> [(Result (Morphism f e m), RawSymbolMap)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (RawSymbolMap -> Doc
forall a. Pretty a => a -> Doc
pretty (RawSymbolMap -> Doc)
-> ((Result (Morphism f e m), RawSymbolMap) -> RawSymbolMap)
-> (Result (Morphism f e m), RawSymbolMap)
-> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. (Result (Morphism f e m), RawSymbolMap) -> RawSymbolMap
forall a b. (a, b) -> b
snd) [(Result (Morphism f e m), RawSymbolMap)]
l)) Range
pos
          else () -> String -> Range -> Result ()
forall a. a -> String -> Range -> Result a
warning () "too many possibilities for symbol maps" Range
pos Result () -> Result (Morphism f e m) -> Result (Morphism f e m)
forall (m :: * -> *) a b. Monad m => m a -> m b -> m b
>> Result (Morphism f e m)
res

compatibleSymbTypes :: SymbType -> SymbType -> Bool
compatibleSymbTypes :: SymbType -> SymbType -> Bool
compatibleSymbTypes s1 :: SymbType
s1 s2 :: SymbType
s2 = case (SymbType
s1, SymbType
s2) of
  (SortAsItemType, SortAsItemType) -> Bool
True
  (OpAsItemType t1 :: OpType
t1, OpAsItemType t2 :: OpType
t2) ->
     [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OpType -> [Id]
opArgs OpType
t1) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (OpType -> [Id]
opArgs OpType
t2)
  (PredAsItemType p1 :: PredType
p1, PredAsItemType p2 :: PredType
p2) ->
      [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PredType -> [Id]
predArgs PredType
p1) Int -> Int -> Bool
forall a. Eq a => a -> a -> Bool
== [Id] -> Int
forall (t :: * -> *) a. Foldable t => t a -> Int
length (PredType -> [Id]
predArgs PredType
p2)
  _ -> Bool
False

compatibleSymbols :: Bool -> Symbol -> Symbol -> Bool
compatibleSymbols :: Bool -> Symbol -> Symbol -> Bool
compatibleSymbols alsoId :: Bool
alsoId (Symbol i1 :: Id
i1 k1 :: SymbType
k1) (Symbol i2 :: Id
i2 k2 :: SymbType
k2) =
  SymbType -> SymbType -> Bool
compatibleSymbTypes SymbType
k1 SymbType
k2 Bool -> Bool -> Bool
&& (Bool -> Bool
not Bool
alsoId Bool -> Bool -> Bool
|| Id
i1 Id -> Id -> Bool
forall a. Eq a => a -> a -> Bool
== Id
i2)

compatibleRawSymbs :: RawSymbol -> RawSymbol -> Bool
compatibleRawSymbs :: RawSymbol -> RawSymbol -> Bool
compatibleRawSymbs r1 :: RawSymbol
r1 r2 :: RawSymbol
r2 = case (RawSymbol
r1, RawSymbol
r2) of
  (ASymbol s1 :: Symbol
s1, ASymbol s2 :: Symbol
s2) -> Bool -> Symbol -> Symbol -> Bool
compatibleSymbols Bool
False Symbol
s1 Symbol
s2
  _ -> Bool
False -- irrelevant

filteredPairs :: (a -> b -> Bool) -> [a] -> [b] -> [[(a, b)]]
filteredPairs :: (a -> b -> Bool) -> [a] -> [b] -> [[(a, b)]]
filteredPairs p :: a -> b -> Bool
p s :: [a]
s l :: [b]
l = [[(a, b)]] -> [[(a, b)]]
forall (t :: * -> *) (m :: * -> *) a.
(Traversable t, Monad m) =>
t (m a) -> m (t a)
sequence [[(a
a, b
b) | b
b <- (b -> Bool) -> [b] -> [b]
forall a. (a -> Bool) -> [a] -> [a]
filter (a -> b -> Bool
p a
a) [b]
l] | a
a <- [a]
s]
-- http://www.haskell.org/pipermail/haskell-cafe/2009-December/069957.html

inducedFromToMorphismAuxExt
  :: (Eq e, Show f, Pretty e, Pretty m)
  => InducedSign f e m e
  -> InducedMorphism e m -- ^ compute extended morphism
  -> (Morphism f e m -> Morphism f e m -> Result m)
     -- ^ composition of extensions
  -> (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 :: InducedSign f e m e
-> InducedMorphism e m
-> (Morphism f e m -> Morphism f e m -> Result m)
-> (e -> e -> Bool)
-> (e -> e -> e)
-> RawSymbolMap
-> ExtSign (Sign f e) Symbol
-> ExtSign (Sign f e) Symbol
-> Result (Morphism f e m)
inducedFromToMorphismAuxExt extInd :: InducedSign f e m e
extInd extEm :: InducedMorphism e m
extEm compM :: Morphism f e m -> Morphism f e m -> Result m
compM isSubExt :: e -> e -> Bool
isSubExt diffExt :: e -> e -> e
diffExt rmap :: RawSymbolMap
rmap
  (ExtSign sigma1 :: Sign f e
sigma1 _) (ExtSign sigma2 :: Sign f e
sigma2 _) = do
  -- 1. use rmap to get a renaming...
  Morphism f e m
mor1 <- InducedSign f e m e
-> InducedMorphism e m
-> RawSymbolMap
-> Sign f e
-> Result (Morphism f e m)
forall e f m.
(Pretty e, Show f) =>
InducedSign f e m e
-> InducedMorphism e m
-> RawSymbolMap
-> Sign f e
-> Result (Morphism f e m)
inducedFromMorphismExt InducedSign f e m e
extInd InducedMorphism e m
extEm RawSymbolMap
rmap Sign f e
sigma1
  -- 1.1 ... is the renamed source signature contained in the target signature?
  let inducedSign :: Sign f e
inducedSign = Morphism f e m -> Sign f e
forall f e m. Morphism f e m -> Sign f e
mtarget Morphism f e m
mor1
      em :: m
em = Morphism f e m -> m
forall f e m. Morphism f e m -> m
extended_map Morphism f e m
mor1
  if (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
forall e f. (e -> e -> Bool) -> Sign f e -> Sign f e -> Bool
isSubSig e -> e -> Bool
isSubExt Sign f e
inducedSign Sign f e
sigma2
   -- yes => we are done
   then (Morphism f e m -> Morphism f e m -> Result m)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
forall e f m.
Eq e =>
(Morphism f e m -> Morphism f e m -> Result m)
-> Morphism f e m -> Morphism f e m -> Result (Morphism f e m)
composeM Morphism f e m -> Morphism f e m -> Result m
compM Morphism f e m
mor1 (Morphism f e m -> Result (Morphism f e m))
-> Morphism f e m -> Result (Morphism f e m)
forall a b. (a -> b) -> a -> b
$ Morphism f e m -> Morphism f e m
forall f e m. Morphism f e m -> Morphism f e m
idOrInclMorphism
     (Morphism f e m -> Morphism f e m)
-> Morphism f e m -> Morphism f e m
forall a b. (a -> b) -> a -> b
$ m -> Sign f e -> Sign f e -> Morphism f e m
forall m f e. m -> Sign f e -> Sign f e -> Morphism f e m
embedMorphism m
em Sign f e
inducedSign Sign f e
sigma2
     {- here the empty mapping should be used, but it will be overwritten
     by the first argument of composeM -}
   else String -> Range -> Result (Morphism f e m)
forall a. String -> Range -> Result a
fatal_error
         ("No signature morphism for symbol map found.\n" String -> String -> String
forall a. [a] -> [a] -> [a]
++
          "The following mapped symbols are missing in the target signature:\n"
          String -> String -> String
forall a. [a] -> [a] -> [a]
++ Sign f e -> String -> String
forall a. Pretty a => a -> String -> String
showDoc ((e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
diffSig e -> e -> e
diffExt Sign f e
inducedSign Sign f e
sigma2) "")
          (Range -> Result (Morphism f e m))
-> Range -> Result (Morphism f e m)
forall a b. (a -> b) -> a -> b
$ (RawSymbol -> Range) -> [RawSymbol] -> Range
forall a. (a -> Range) -> [a] -> Range
concatMapRange RawSymbol -> Range
forall a. GetRange a => a -> Range
getRange ([RawSymbol] -> Range) -> [RawSymbol] -> Range
forall a b. (a -> b) -> a -> b
$ RawSymbolMap -> [RawSymbol]
forall k a. Map k a -> [k]
Map.keys RawSymbolMap
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 :: m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign extEm :: m
extEm sys :: Set Symbol
sys sigma :: Sign f e
sigma = let
  symset :: Set Symbol
symset = Sign f e -> Set Symbol
forall f e. Sign f e -> Set Symbol
symsetOf Sign f e
sigma   -- 1.
  sigma1 :: Sign f e
sigma1 = (Symbol -> Sign f e -> Sign f e)
-> Sign f e -> Set Symbol -> Sign f e
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Symbol -> Sign f e -> Sign f e
forall f e. Symbol -> Sign f e -> Sign f e
revealSym Sign f e
sigma
    { sortRel :: Rel Id
sortRel = Rel Id
forall a. Rel a
Rel.empty
    , opMap :: MapSet Id OpType
opMap = MapSet Id OpType
forall a b. MapSet a b
MapSet.empty
    , predMap :: MapSet Id PredType
predMap = MapSet Id PredType
forall a b. MapSet a b
MapSet.empty } Set Symbol
sys  -- 4.
  sigma2 :: Sign f e
sigma2 = Sign f e
sigma1
    { sortRel :: Rel Id
sortRel = Sign f e -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel Sign f e
sigma Rel Id -> Set Id -> Rel Id
forall a. Ord a => Rel a -> Set a -> Rel a
`Rel.restrict` Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
sigma1
    , emptySortSet :: Set Id
emptySortSet = Set Id -> Set Id -> Set Id
forall a. Ord a => Set a -> Set a -> Set a
Set.intersection (Sign f e -> Set Id
forall f e. Sign f e -> Set Id
sortSet Sign f e
sigma1) (Set Id -> Set Id) -> Set Id -> Set Id
forall a b. (a -> b) -> a -> b
$ Sign f e -> Set Id
forall f e. Sign f e -> Set Id
emptySortSet Sign f e
sigma }
  in if Bool -> Bool
not (Bool -> Bool) -> Bool -> Bool
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Set Symbol -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set Symbol
sys Set Symbol
symset   -- 2.
   then let diffsyms :: Set Symbol
diffsyms = Set Symbol
sys Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Symbol
symset in
        String -> Range -> Result (Morphism f e m)
forall a. String -> Range -> Result a
fatal_error ("Revealing: The following symbols "
                     String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Set Symbol
diffsyms " are not in the signature")
        (Range -> Result (Morphism f e m))
-> Range -> Result (Morphism f e m)
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Range
forall a. GetRange a => a -> Range
getRange Set Symbol
diffsyms
   else m -> Sign f e -> Sign f e -> Result (Morphism f e m)
forall m f e. m -> Sign f e -> Sign f e -> Result (Morphism f e m)
sigInclusion m
extEm Sign f e
sigma2 Sign f e
sigma  -- 7.

revealSym :: Symbol -> Sign f e -> Sign f e
revealSym :: Symbol -> Sign f e -> Sign f e
revealSym sy :: Symbol
sy sigma1 :: Sign f e
sigma1 = let
  n :: Id
n = Symbol -> Id
symName Symbol
sy
  insSort :: Id -> Rel Id -> Rel Id
insSort = Id -> Rel Id -> Rel Id
forall a. Ord a => a -> Rel a -> Rel a
Rel.insertKey
  in case Symbol -> SymbType
symbType Symbol
sy of
    SortAsItemType ->      -- 4.1.1.
      Sign f e
sigma1 {sortRel :: Rel Id
sortRel = Id -> Rel Id -> Rel Id
insSort Id
n (Rel Id -> Rel Id) -> Rel Id -> Rel Id
forall a b. (a -> b) -> a -> b
$ Sign f e -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel Sign f e
sigma1}
    SubsortAsItemType _ -> Sign f e
sigma1 -- ignore
    OpAsItemType ot :: OpType
ot ->     -- 4.1.2./4.1.3.
      Sign f e
sigma1 { sortRel :: Rel Id
sortRel = (Id -> Rel Id -> Rel Id) -> Rel Id -> [Id] -> Rel Id
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> Rel Id -> Rel Id
insSort (Sign f e -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel Sign f e
sigma1)
               ([Id] -> Rel Id) -> [Id] -> Rel Id
forall a b. (a -> b) -> a -> b
$ OpType -> [Id]
opSorts OpType
ot
             , opMap :: MapSet Id OpType
opMap = Id -> OpType -> MapSet Id OpType -> MapSet Id OpType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
n OpType
ot (MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
sigma1 }
    PredAsItemType pt :: PredType
pt ->   -- 4.1.4.
      Sign f e
sigma1 { sortRel :: Rel Id
sortRel = (Id -> Rel Id -> Rel Id) -> Rel Id -> [Id] -> Rel Id
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr Id -> Rel Id -> Rel Id
insSort (Sign f e -> Rel Id
forall f e. Sign f e -> Rel Id
sortRel Sign f e
sigma1) ([Id] -> Rel Id) -> [Id] -> Rel Id
forall a b. (a -> b) -> a -> b
$ PredType -> [Id]
predArgs PredType
pt
             , predMap :: MapSet Id PredType
predMap = Id -> PredType -> MapSet Id PredType -> MapSet Id PredType
forall a b. (Ord a, Ord b) => a -> b -> MapSet a b -> MapSet a b
MapSet.insert Id
n PredType
pt (MapSet Id PredType -> MapSet Id PredType)
-> MapSet Id PredType -> MapSet Id PredType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
sigma1 }

{-
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 :: m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
cogeneratedSign extEm :: m
extEm symset :: Set Symbol
symset sigma :: Sign f e
sigma = let
  symset0 :: Set Symbol
symset0 = Sign f e -> Set Symbol
forall f e. Sign f e -> Set Symbol
symsetOf Sign f e
sigma   -- 1.
  symset1 :: Set Symbol
symset1 = (Symbol -> Set Symbol -> Set Symbol)
-> Set Symbol -> Set Symbol -> Set Symbol
forall a b. (a -> b -> b) -> b -> Set a -> b
Set.fold Symbol -> Set Symbol -> Set Symbol
hideSym Set Symbol
symset0 Set Symbol
symset  -- 3.
  in if Set Symbol -> Set Symbol -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set Symbol
symset Set Symbol
symset0   -- 2.
   then m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
forall m f e.
m -> Set Symbol -> Sign f e -> Result (Morphism f e m)
generatedSign m
extEm Set Symbol
symset1 Sign f e
sigma -- 4./5.
   else let diffsyms :: Set Symbol
diffsyms = Set Symbol
symset Set Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => Set a -> Set a -> Set a
Set.\\ Set Symbol
symset0 in
        String -> Range -> Result (Morphism f e m)
forall a. String -> Range -> Result a
fatal_error ("Hiding: The following symbols "
            String -> String -> String
forall a. [a] -> [a] -> [a]
++ Set Symbol -> String -> String
forall a. Pretty a => a -> String -> String
showDoc Set Symbol
diffsyms " are not in the signature")
        (Range -> Result (Morphism f e m))
-> Range -> Result (Morphism f e m)
forall a b. (a -> b) -> a -> b
$ Set Symbol -> Range
forall a. GetRange a => a -> Range
getRange Set Symbol
diffsyms

hideSym :: Symbol -> Set.Set Symbol -> Set.Set Symbol
hideSym :: Symbol -> Set Symbol -> Set Symbol
hideSym sy :: Symbol
sy set1 :: Set Symbol
set1 = let set2 :: Set Symbol
set2 = Symbol -> Set Symbol -> Set Symbol
forall a. Ord a => a -> Set a -> Set a
Set.delete Symbol
sy Set Symbol
set1 in case Symbol -> SymbType
symbType Symbol
sy of
    SortAsItemType ->      -- 3.1.1.
      (Symbol -> Bool) -> Set Symbol -> Set Symbol
forall a. (a -> Bool) -> Set a -> Set a
Set.filter (Bool -> Bool
not (Bool -> Bool) -> (Symbol -> Bool) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Id -> SymbType -> Bool
profileContainsSort (Symbol -> Id
symName Symbol
sy) (SymbType -> Bool) -> (Symbol -> SymbType) -> Symbol -> Bool
forall b c a. (b -> c) -> (a -> b) -> a -> c
. Symbol -> SymbType
symbType) Set Symbol
set2
    _ -> Set Symbol
set2    -- 3.1.2

profileContainsSort :: SORT -> SymbType -> Bool
profileContainsSort :: Id -> SymbType -> Bool
profileContainsSort s :: Id
s symbT :: SymbType
symbT = Id -> [Id] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Id
s ([Id] -> Bool) -> [Id] -> Bool
forall a b. (a -> b) -> a -> b
$ case SymbType
symbT of
    OpAsItemType ot :: OpType
ot -> OpType -> [Id]
opSorts OpType
ot
    PredAsItemType pt :: PredType
pt -> PredType -> [Id]
predArgs PredType
pt
    SubsortAsItemType t :: Id
t -> [Id
t]
    SortAsItemType -> []

leCl :: Ord a => (a -> a -> Bool) -> MapSet.MapSet Id a
     -> Map.Map Id [Set.Set a]
leCl :: (a -> a -> Bool) -> MapSet Id a -> Map Id [Set a]
leCl f :: a -> a -> Bool
f = (Set a -> [Set a]) -> Map Id (Set a) -> Map Id [Set a]
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((a -> a -> Bool) -> Set a -> [Set a]
forall a. Ord a => (a -> a -> Bool) -> Set a -> [Set a]
Rel.partSet a -> a -> Bool
f) (Map Id (Set a) -> Map Id [Set a])
-> (MapSet Id a -> Map Id (Set a)) -> MapSet Id a -> Map Id [Set a]
forall b c a. (b -> c) -> (a -> b) -> a -> c
. MapSet Id a -> Map Id (Set a)
forall a b. MapSet a b -> Map a (Set b)
MapSet.toMap

mkp :: OpMap -> OpMap
mkp :: MapSet Id OpType -> MapSet Id OpType
mkp = (Set OpType -> Set OpType) -> MapSet Id OpType -> MapSet Id OpType
forall a b c. Ord a => (Set b -> Set c) -> MapSet a b -> MapSet a c
MapSet.mapSet Set OpType -> Set OpType
makePartial

finalUnion :: (e -> e -> e) -- ^ join signature extensions
           -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion :: (e -> e -> e) -> Sign f e -> Sign f e -> Result (Sign f e)
finalUnion addSigExt :: e -> e -> e
addSigExt s1 :: Sign f e
s1 s2 :: Sign f e
s2 =
 let extP :: Map k [a] -> Map k [(a, [a], Bool)]
extP = ([a] -> [(a, [a], Bool)]) -> Map k [a] -> Map k [(a, [a], Bool)]
forall a b k. (a -> b) -> Map k a -> Map k b
Map.map ((a -> (a, [a], Bool)) -> [a] -> [(a, [a], Bool)]
forall a b. (a -> b) -> [a] -> [b]
map ((a -> (a, [a], Bool)) -> [a] -> [(a, [a], Bool)])
-> (a -> (a, [a], Bool)) -> [a] -> [(a, [a], Bool)]
forall a b. (a -> b) -> a -> b
$ \ s :: a
s -> (a
s, [], Bool
False))
     o1 :: Map Id [(Set OpType, [a], Bool)]
o1 = Map Id [Set OpType] -> Map Id [(Set OpType, [a], Bool)]
forall k a a. Map k [a] -> Map k [(a, [a], Bool)]
extP (Map Id [Set OpType] -> Map Id [(Set OpType, [a], Bool)])
-> Map Id [Set OpType] -> Map Id [(Set OpType, [a], Bool)]
forall a b. (a -> b) -> a -> b
$ (OpType -> OpType -> Bool)
-> MapSet Id OpType -> Map Id [Set OpType]
forall a.
Ord a =>
(a -> a -> Bool) -> MapSet Id a -> Map Id [Set a]
leCl (Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF Sign f e
s1) (MapSet Id OpType -> Map Id [Set OpType])
-> MapSet Id OpType -> Map Id [Set OpType]
forall a b. (a -> b) -> a -> b
$ MapSet Id OpType -> MapSet Id OpType
mkp (MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
s1
     o2 :: Map Id [(Set OpType, [a], Bool)]
o2 = Map Id [Set OpType] -> Map Id [(Set OpType, [a], Bool)]
forall k a a. Map k [a] -> Map k [(a, [a], Bool)]
extP (Map Id [Set OpType] -> Map Id [(Set OpType, [a], Bool)])
-> Map Id [Set OpType] -> Map Id [(Set OpType, [a], Bool)]
forall a b. (a -> b) -> a -> b
$ (OpType -> OpType -> Bool)
-> MapSet Id OpType -> Map Id [Set OpType]
forall a.
Ord a =>
(a -> a -> Bool) -> MapSet Id a -> Map Id [Set a]
leCl (Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF Sign f e
s2) (MapSet Id OpType -> Map Id [Set OpType])
-> MapSet Id OpType -> Map Id [Set OpType]
forall a b. (a -> b) -> a -> b
$ MapSet Id OpType -> MapSet Id OpType
mkp (MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
s2
     p1 :: Map Id [(Set PredType, [a], Bool)]
p1 = Map Id [Set PredType] -> Map Id [(Set PredType, [a], Bool)]
forall k a a. Map k [a] -> Map k [(a, [a], Bool)]
extP (Map Id [Set PredType] -> Map Id [(Set PredType, [a], Bool)])
-> Map Id [Set PredType] -> Map Id [(Set PredType, [a], Bool)]
forall a b. (a -> b) -> a -> b
$ (PredType -> PredType -> Bool)
-> MapSet Id PredType -> Map Id [Set PredType]
forall a.
Ord a =>
(a -> a -> Bool) -> MapSet Id a -> Map Id [Set a]
leCl (Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP Sign f e
s1) (MapSet Id PredType -> Map Id [Set PredType])
-> MapSet Id PredType -> Map Id [Set PredType]
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
s1
     p2 :: Map Id [(Set PredType, [a], Bool)]
p2 = Map Id [Set PredType] -> Map Id [(Set PredType, [a], Bool)]
forall k a a. Map k [a] -> Map k [(a, [a], Bool)]
extP (Map Id [Set PredType] -> Map Id [(Set PredType, [a], Bool)])
-> Map Id [Set PredType] -> Map Id [(Set PredType, [a], Bool)]
forall a b. (a -> b) -> a -> b
$ (PredType -> PredType -> Bool)
-> MapSet Id PredType -> Map Id [Set PredType]
forall a.
Ord a =>
(a -> a -> Bool) -> MapSet Id a -> Map Id [Set a]
leCl (Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP Sign f e
s2) (MapSet Id PredType -> Map Id [Set PredType])
-> MapSet Id PredType -> Map Id [Set PredType]
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
s2
     s3 :: Sign f e
s3 = (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
forall e f. (e -> e -> e) -> Sign f e -> Sign f e -> Sign f e
addSig e -> e -> e
addSigExt Sign f e
s1 Sign f e
s2
     o3 :: Map Id [Set OpType]
o3 = (OpType -> OpType -> Bool)
-> MapSet Id OpType -> Map Id [Set OpType]
forall a.
Ord a =>
(a -> a -> Bool) -> MapSet Id a -> Map Id [Set a]
leCl (Sign f e -> OpType -> OpType -> Bool
forall f e. Sign f e -> OpType -> OpType -> Bool
leqF Sign f e
s3) (MapSet Id OpType -> Map Id [Set OpType])
-> MapSet Id OpType -> Map Id [Set OpType]
forall a b. (a -> b) -> a -> b
$ MapSet Id OpType -> MapSet Id OpType
mkp (MapSet Id OpType -> MapSet Id OpType)
-> MapSet Id OpType -> MapSet Id OpType
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id OpType
forall f e. Sign f e -> MapSet Id OpType
opMap Sign f e
s3
     p3 :: Map Id [Set PredType]
p3 = (PredType -> PredType -> Bool)
-> MapSet Id PredType -> Map Id [Set PredType]
forall a.
Ord a =>
(a -> a -> Bool) -> MapSet Id a -> Map Id [Set a]
leCl (Sign f e -> PredType -> PredType -> Bool
forall f e. Sign f e -> PredType -> PredType -> Bool
leqP Sign f e
s3) (MapSet Id PredType -> Map Id [Set PredType])
-> MapSet Id PredType -> Map Id [Set PredType]
forall a b. (a -> b) -> a -> b
$ Sign f e -> MapSet Id PredType
forall f e. Sign f e -> MapSet Id PredType
predMap Sign f e
s3
     d1 :: Map Id [(Set OpType, [Set OpType], Bool)]
d1 = ([(Set OpType, [Set OpType], Bool)]
 -> [Set OpType] -> Maybe [(Set OpType, [Set OpType], Bool)])
-> Map Id [(Set OpType, [Set OpType], Bool)]
-> Map Id [Set OpType]
-> Map Id [(Set OpType, [Set OpType], Bool)]
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith (Bool
-> [(Set OpType, [Set OpType], Bool)]
-> [Set OpType]
-> Maybe [(Set OpType, [Set OpType], Bool)]
forall a.
Ord a =>
Bool
-> [(Set a, [Set a], Bool)]
-> [Set a]
-> Maybe [(Set a, [Set a], Bool)]
listOfSetDiff Bool
True) Map Id [(Set OpType, [Set OpType], Bool)]
forall a. Map Id [(Set OpType, [a], Bool)]
o1 Map Id [Set OpType]
o3
     d2 :: Map Id [(Set OpType, [Set OpType], Bool)]
d2 = Map Id [(Set OpType, [Set OpType], Bool)]
-> Map Id [(Set OpType, [Set OpType], Bool)]
-> Map Id [(Set OpType, [Set OpType], Bool)]
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Id [(Set OpType, [Set OpType], Bool)]
d1 (Map Id [(Set OpType, [Set OpType], Bool)]
 -> Map Id [(Set OpType, [Set OpType], Bool)])
-> Map Id [(Set OpType, [Set OpType], Bool)]
-> Map Id [(Set OpType, [Set OpType], Bool)]
forall a b. (a -> b) -> a -> b
$ ([(Set OpType, [Set OpType], Bool)]
 -> [Set OpType] -> Maybe [(Set OpType, [Set OpType], Bool)])
-> Map Id [(Set OpType, [Set OpType], Bool)]
-> Map Id [Set OpType]
-> Map Id [(Set OpType, [Set OpType], Bool)]
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith (Bool
-> [(Set OpType, [Set OpType], Bool)]
-> [Set OpType]
-> Maybe [(Set OpType, [Set OpType], Bool)]
forall a.
Ord a =>
Bool
-> [(Set a, [Set a], Bool)]
-> [Set a]
-> Maybe [(Set a, [Set a], Bool)]
listOfSetDiff Bool
False) Map Id [(Set OpType, [Set OpType], Bool)]
forall a. Map Id [(Set OpType, [a], Bool)]
o2 Map Id [Set OpType]
o3
     e1 :: Map Id [(Set PredType, [Set PredType], Bool)]
e1 = ([(Set PredType, [Set PredType], Bool)]
 -> [Set PredType] -> Maybe [(Set PredType, [Set PredType], Bool)])
-> Map Id [(Set PredType, [Set PredType], Bool)]
-> Map Id [Set PredType]
-> Map Id [(Set PredType, [Set PredType], Bool)]
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith (Bool
-> [(Set PredType, [Set PredType], Bool)]
-> [Set PredType]
-> Maybe [(Set PredType, [Set PredType], Bool)]
forall a.
Ord a =>
Bool
-> [(Set a, [Set a], Bool)]
-> [Set a]
-> Maybe [(Set a, [Set a], Bool)]
listOfSetDiff Bool
True) Map Id [(Set PredType, [Set PredType], Bool)]
forall a. Map Id [(Set PredType, [a], Bool)]
p1 Map Id [Set PredType]
p3
     e2 :: Map Id [(Set PredType, [Set PredType], Bool)]
e2 = Map Id [(Set PredType, [Set PredType], Bool)]
-> Map Id [(Set PredType, [Set PredType], Bool)]
-> Map Id [(Set PredType, [Set PredType], Bool)]
forall k a. Ord k => Map k a -> Map k a -> Map k a
Map.union Map Id [(Set PredType, [Set PredType], Bool)]
e1 (Map Id [(Set PredType, [Set PredType], Bool)]
 -> Map Id [(Set PredType, [Set PredType], Bool)])
-> Map Id [(Set PredType, [Set PredType], Bool)]
-> Map Id [(Set PredType, [Set PredType], Bool)]
forall a b. (a -> b) -> a -> b
$ ([(Set PredType, [Set PredType], Bool)]
 -> [Set PredType] -> Maybe [(Set PredType, [Set PredType], Bool)])
-> Map Id [(Set PredType, [Set PredType], Bool)]
-> Map Id [Set PredType]
-> Map Id [(Set PredType, [Set PredType], Bool)]
forall k a b.
Ord k =>
(a -> b -> Maybe a) -> Map k a -> Map k b -> Map k a
Map.differenceWith (Bool
-> [(Set PredType, [Set PredType], Bool)]
-> [Set PredType]
-> Maybe [(Set PredType, [Set PredType], Bool)]
forall a.
Ord a =>
Bool
-> [(Set a, [Set a], Bool)]
-> [Set a]
-> Maybe [(Set a, [Set a], Bool)]
listOfSetDiff Bool
False) Map Id [(Set PredType, [Set PredType], Bool)]
forall a. Map Id [(Set PredType, [a], Bool)]
p2 Map Id [Set PredType]
p3
     prL :: (a, [a], Bool) -> Doc
prL (s :: a
s, l :: [a]
l, b :: Bool
b) = [Doc] -> Doc
fsep
       ([Doc] -> Doc) -> [Doc] -> Doc
forall a b. (a -> b) -> a -> b
$ String -> Doc
text ("(" String -> String -> String
forall a. [a] -> [a] -> [a]
++ (if Bool
b then "left" else "right")
               String -> String -> String
forall a. [a] -> [a] -> [a]
++ " side of union)")
       Doc -> [Doc] -> [Doc]
forall a. a -> [a] -> [a]
: (a -> Doc) -> [a] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map a -> Doc
forall a. Pretty a => a -> Doc
pretty [a]
l [Doc] -> [Doc] -> [Doc]
forall a. [a] -> [a] -> [a]
++ [Doc
mapsto Doc -> Doc -> Doc
<+> a -> Doc
forall a. Pretty a => a -> Doc
pretty a
s]
     prM :: String -> Map a [(a, [a], Bool)] -> Doc
prM str :: String
str = (a -> Doc)
-> ([(a, [a], Bool)] -> Doc)
-> (CSize -> Doc -> Doc)
-> ([Doc] -> Doc)
-> (Doc -> Doc -> Doc)
-> Map a [(a, [a], Bool)]
-> Doc
forall a b.
(a -> Doc)
-> (b -> Doc)
-> (CSize -> Doc -> Doc)
-> ([Doc] -> Doc)
-> (Doc -> Doc -> Doc)
-> Map a b
-> Doc
ppMap ((String -> Doc
text String
str Doc -> Doc -> Doc
<+>) (Doc -> Doc) -> (a -> Doc) -> a -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. a -> Doc
forall a. Pretty a => a -> Doc
pretty)
               ([Doc] -> Doc
vcat ([Doc] -> Doc)
-> ([(a, [a], Bool)] -> [Doc]) -> [(a, [a], Bool)] -> Doc
forall b c a. (b -> c) -> (a -> b) -> a -> c
. ((a, [a], Bool) -> Doc) -> [(a, [a], Bool)] -> [Doc]
forall a b. (a -> b) -> [a] -> [b]
map (a, [a], Bool) -> Doc
forall a a. (Pretty a, Pretty a) => (a, [a], Bool) -> Doc
prL) ((Doc -> Doc) -> CSize -> Doc -> Doc
forall a b. a -> b -> a
const Doc -> Doc
forall a. a -> a
id) [Doc] -> Doc
vcat (\ v1 :: Doc
v1 v2 :: Doc
v2 -> [Doc] -> Doc
sep [Doc
v1, Doc
v2])
 in if Map Id [(Set OpType, [Set OpType], Bool)] -> Bool
forall k a. Map k a -> Bool
Map.null Map Id [(Set OpType, [Set OpType], Bool)]
d2 Bool -> Bool -> Bool
&& Map Id [(Set PredType, [Set PredType], Bool)] -> Bool
forall k a. Map k a -> Bool
Map.null Map Id [(Set PredType, [Set PredType], Bool)]
e2 then Sign f e -> Result (Sign f e)
forall (m :: * -> *) a. Monad m => a -> m a
return Sign f e
s3
    else String -> Result (Sign f e)
forall (m :: * -> *) a. MonadFail m => String -> m a
Fail.fail (String -> Result (Sign f e)) -> String -> Result (Sign f e)
forall a b. (a -> b) -> a -> b
$ "illegal overload relation identifications for profiles of:\n"
         String -> String -> String
forall a. [a] -> [a] -> [a]
++ Doc -> String
forall a. Show a => a -> String
show (String -> Map Id [(Set OpType, [Set OpType], Bool)] -> Doc
forall a a a.
(Pretty a, Pretty a, Pretty a) =>
String -> Map a [(a, [a], Bool)] -> Doc
prM "op" Map Id [(Set OpType, [Set OpType], Bool)]
d2 Doc -> Doc -> Doc
$+$ String -> Map Id [(Set PredType, [Set PredType], Bool)] -> Doc
forall a a a.
(Pretty a, Pretty a, Pretty a) =>
String -> Map a [(a, [a], Bool)] -> Doc
prM "pred" Map Id [(Set PredType, [Set PredType], Bool)]
e2)

listOfSetDiff :: Ord a => Bool -> [(Set.Set a, [Set.Set a], Bool)]
              -> [Set.Set a] -> Maybe [(Set.Set a, [Set.Set a], Bool)]
listOfSetDiff :: Bool
-> [(Set a, [Set a], Bool)]
-> [Set a]
-> Maybe [(Set a, [Set a], Bool)]
listOfSetDiff b :: Bool
b rl1 :: [(Set a, [Set a], Bool)]
rl1 l2 :: [Set a]
l2 = let
  fst3 :: (a, b, c) -> a
fst3 (s :: a
s, _, _) = a
s
  l1 :: [Set a]
l1 = ((Set a, [Set a], Bool) -> Set a)
-> [(Set a, [Set a], Bool)] -> [Set a]
forall a b. (a -> b) -> [a] -> [b]
map (Set a, [Set a], Bool) -> Set a
forall a b c. (a, b, c) -> a
fst3 [(Set a, [Set a], Bool)]
rl1 in
  (\ l3 :: [(Set a, [Set a], Bool)]
l3 -> if [(Set a, [Set a], Bool)] -> Bool
forall (t :: * -> *) a. Foldable t => t a -> Bool
null [(Set a, [Set a], Bool)]
l3 then Maybe [(Set a, [Set a], Bool)]
forall a. Maybe a
Nothing else [(Set a, [Set a], Bool)] -> Maybe [(Set a, [Set a], Bool)]
forall a. a -> Maybe a
Just [(Set a, [Set a], Bool)]
l3)
  ([(Set a, [Set a], Bool)] -> Maybe [(Set a, [Set a], Bool)])
-> [(Set a, [Set a], Bool)] -> Maybe [(Set a, [Set a], Bool)]
forall a b. (a -> b) -> a -> b
$ ([(Set a, [Set a], Bool)], [Set a]) -> [(Set a, [Set a], Bool)]
forall a b. (a, b) -> a
fst (([(Set a, [Set a], Bool)], [Set a]) -> [(Set a, [Set a], Bool)])
-> ([(Set a, [Set a], Bool)], [Set a]) -> [(Set a, [Set a], Bool)]
forall a b. (a -> b) -> a -> b
$ (Set a
 -> ([(Set a, [Set a], Bool)], [Set a])
 -> ([(Set a, [Set a], Bool)], [Set a]))
-> ([(Set a, [Set a], Bool)], [Set a])
-> [Set a]
-> ([(Set a, [Set a], Bool)], [Set a])
forall (t :: * -> *) a b.
Foldable t =>
(a -> b -> b) -> b -> t a -> b
foldr
  (\ s :: Set a
s (l :: [(Set a, [Set a], Bool)]
l, r :: [Set a]
r) ->
         let sIn :: Set a -> Bool
sIn = Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
Set.isSubsetOf Set a
s
             (r1 :: [Set a]
r1, r2 :: [Set a]
r2) = (Set a -> Bool) -> [Set a] -> ([Set a], [Set a])
forall a. (a -> Bool) -> [a] -> ([a], [a])
partition Set a -> Bool
sIn [Set a]
r in
         case [Set a]
r1 of
           [] -> case (Set a -> Bool) -> [Set a] -> Maybe (Set a)
forall (t :: * -> *) a. Foldable t => (a -> Bool) -> t a -> Maybe a
find Set a -> Bool
sIn [Set a]
l2 of
             Nothing -> String -> ([(Set a, [Set a], Bool)], [Set a])
forall a. HasCallStack => String -> a
error "CASL.finalUnion.listOfSetDiff1"
             Just s2 :: Set a
s2 -> (if Set a -> [Set a] -> Bool
forall (t :: * -> *) a. (Foldable t, Eq a) => a -> t a -> Bool
elem Set a
s2 ([Set a] -> Bool) -> [Set a] -> Bool
forall a b. (a -> b) -> a -> b
$ ((Set a, [Set a], Bool) -> Set a)
-> [(Set a, [Set a], Bool)] -> [Set a]
forall a b. (a -> b) -> [a] -> [b]
map (Set a, [Set a], Bool) -> Set a
forall a b c. (a, b, c) -> a
fst3 [(Set a, [Set a], Bool)]
l then [(Set a, [Set a], Bool)]
l else
                         (Set a
s2, (Set a -> Bool) -> [Set a] -> [Set a]
forall a. (a -> Bool) -> [a] -> [a]
filter (Set a -> Set a -> Bool
forall a. Ord a => Set a -> Set a -> Bool
`Set.isSubsetOf` Set a
s2) [Set a]
l1, Bool
b) (Set a, [Set a], Bool)
-> [(Set a, [Set a], Bool)] -> [(Set a, [Set a], Bool)]
forall a. a -> [a] -> [a]
: [(Set a, [Set a], Bool)]
l, [Set a]
r)
           [_] -> ([(Set a, [Set a], Bool)]
l, [Set a]
r2)
           _ -> String -> ([(Set a, [Set a], Bool)], [Set a])
forall a. HasCallStack => String -> a
error "CASL.finalUnion.listOfSetDiff2")
  ([], [Set a]
l2) [Set a]
l1